From 34dd34065111c5abe68e88a79a77e482e79489a7 Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Wed, 7 Jun 2017 14:25:07 +0200 Subject: Put "ssreflect" behind "API". --- .gitignore | 3 +++ API/API.mli | 26 ++++++++++++++++++++++++-- API/grammar_API.mli | 1 + plugins/ssr/ssrast.mli | 3 ++- plugins/ssr/ssrbwd.ml | 1 + plugins/ssr/ssrbwd.mli | 2 ++ plugins/ssr/ssrcommon.ml | 8 +++++--- plugins/ssr/ssrcommon.mli | 11 ++++++----- plugins/ssr/ssrelim.ml | 1 + plugins/ssr/ssrelim.mli | 1 + plugins/ssr/ssrequality.ml | 3 ++- plugins/ssr/ssrequality.mli | 1 + plugins/ssr/ssrfwd.ml | 1 + plugins/ssr/ssrfwd.mli | 1 + plugins/ssr/ssripats.ml | 1 + plugins/ssr/ssripats.mli | 1 + plugins/ssr/ssrparser.ml4 | 2 ++ plugins/ssr/ssrparser.mli | 3 +++ plugins/ssr/ssrprinters.ml | 1 + plugins/ssr/ssrprinters.mli | 1 + plugins/ssr/ssrtacticals.ml | 1 + plugins/ssr/ssrtacticals.mli | 2 ++ plugins/ssr/ssrvernac.ml4 | 2 ++ plugins/ssr/ssrview.ml | 1 + plugins/ssr/ssrview.mli | 1 + 25 files changed, 67 insertions(+), 12 deletions(-) diff --git a/.gitignore b/.gitignore index fe5f59b94..84fe89d1e 100644 --- a/.gitignore +++ b/.gitignore @@ -180,3 +180,6 @@ test-suite/.nra.cache # these files are generated from plugins/micromega/MExtraction.v plugins/micromega/micromega.ml plugins/micromega/micromega.mli + +plugins/ssr/ssrparser.ml +plugins/ssr/ssrvernac.ml diff --git a/API/API.mli b/API/API.mli index 2661badc5..d844e8bf5 100644 --- a/API/API.mli +++ b/API/API.mli @@ -809,6 +809,7 @@ sig val mkNamedLambda : Names.Id.t -> types -> constr -> constr val mkNamedProd : Names.Id.t -> types -> types -> types + val isCast : Evd.evar_map -> t -> bool val isEvar : Prelude.evar_map -> constr -> bool val isInd : Prelude.evar_map -> constr -> bool val isRel : Prelude.evar_map -> constr -> bool @@ -827,6 +828,7 @@ sig val destConst : Prelude.evar_map -> constr -> Names.Constant.t * EInstance.t val destConstruct : Prelude.evar_map -> constr -> Names.constructor * EInstance.t val destFix : Evd.evar_map -> t -> (t, t) Term.pfixpoint + val destCast : Evd.evar_map -> t -> t * Term.cast_kind * t val mkConstruct : Names.constructor -> constr @@ -866,6 +868,8 @@ sig val substl : constr list -> constr -> constr val lift : int -> constr -> constr val liftn : int -> int -> t -> t + val subst_var : Names.Id.t -> t -> t + val subst_vars : Names.Id.t list -> t -> t end val fresh_global : @@ -907,6 +911,7 @@ val of_named_decl : (Term.constr, Term.types) Context.Named.Declaration.pt -> (c val mkConstU : Names.Constant.t * EInstance.t -> t val isProd : Evd.evar_map -> t -> bool val mkConstructUi : (Names.inductive * EInstance.t) * int -> t + val isLambda : Evd.evar_map -> t -> bool end module Mod_subst : @@ -3262,10 +3267,11 @@ end module Proof_type : sig type goal = Evar.t + type rule = Proof_type.prim_rule = + | Cut of bool * bool * Names.Id.t * Term.types + | Refine of Term.constr type tactic = goal Evd.sigma -> goal list Evd.sigma - - type rule = Proof_type.rule end module Redexpr : @@ -3333,6 +3339,8 @@ sig val pf_nth_hyp_id : Proof_type.goal sigma -> int -> Names.Id.t + val sig_it : 'a sigma -> 'a + module New : sig val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a @@ -3467,6 +3475,11 @@ sig val tclREPEAT : Proof_type.tactic -> Proof_type.tactic val tclORELSE : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic val tclFAIL : int -> Pp.std_ppcmds -> Proof_type.tactic + val tclIDTAC : Proof_type.tactic + val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic + val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic + val tclTRY : Proof_type.tactic -> Proof_type.tactic + val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic end module Termops : @@ -4031,9 +4044,13 @@ sig val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(EConstr.constr option) -> Names.Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (EConstr.constr -> EConstr.constr list -> unit Proofview.tactic) -> unit Proofview.tactic + val apply_type : EConstr.constr -> EConstr.constr list -> unit Proofview.tactic + val hnf_in_concl : unit Proofview.tactic + val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic module New : sig + val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic val reduce_after_refine : unit Proofview.tactic end module Simple : @@ -4061,7 +4078,12 @@ sig val tclTHENS : tactic -> tactic list -> tactic val tclFIRST : tactic list -> tactic val tclTHENFIRST : tactic -> tactic -> tactic + val tclTHENLAST : tactic -> tactic -> tactic + val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic + val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic + val tclSOLVE : tactic list -> tactic + val onClause : (Names.Id.t option -> tactic) -> Locus.clause -> tactic val onAllHypsAndConcl : (Names.Id.t option -> tactic) -> tactic val onLastHypId : (Names.Id.t -> tactic) -> tactic val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic diff --git a/API/grammar_API.mli b/API/grammar_API.mli index 350457f6c..44aae771f 100644 --- a/API/grammar_API.mli +++ b/API/grammar_API.mli @@ -177,6 +177,7 @@ sig val parse_string : 'a Gram.Entry.e -> string -> 'a val (!@) : Ploc.t -> Loc.t val set_command_entry : API.Vernacexpr.vernac_expr Gram.Entry.e -> unit + val to_coqloc : Ploc.t -> Loc.t end module CLexer : diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 69202ae2d..4ddd38365 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Ltac_plugin @@ -78,7 +79,7 @@ type ssripat = | IPatView of ssrterm list (* /view *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl - | IPatNewHidden of identifier list + | IPatNewHidden of Id.t list (* | IPatVarsForAbstract of Id.t list *) and ssripats = ssripat list diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index cc0e86684..3988f00ba 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Printer open Pretyping open Globnames diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index 8bf785a21..b0e98bdb4 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API + val apply_top_tac : Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma val inner_ssrapplytac : diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e90be92cf..38ee4be45 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API open Util open Names open Evd @@ -689,7 +691,7 @@ let pf_merge_uc_of sigma gl = let rec constr_name sigma c = match EConstr.kind sigma c with | Var id -> Name id | Cast (c', _, _) -> constr_name sigma c' - | Const (cn,_) -> Name (id_of_label (con_label cn)) + | Const (cn,_) -> Name (Label.to_id (con_label cn)) | App (c', _) -> constr_name sigma c' | _ -> Anonymous @@ -701,9 +703,9 @@ let pf_mkprod gl c ?(name=constr_name (project gl) c) cl = let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project gl) c cl) (** look up a name in the ssreflect internals module *) -let ssrdirpath = make_dirpath [id_of_string "ssreflect"] +let ssrdirpath = DirPath.make [id_of_string "ssreflect"] let ssrqid name = Libnames.make_qualid ssrdirpath (id_of_string name) -let ssrtopqid name = Libnames.make_short_qualid (id_of_string name) +let ssrtopqid name = Libnames.qualid_of_ident (id_of_string name) let locate_reference qid = Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 834b7b722..1b6a700b2 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Environ open Proof_type @@ -173,12 +174,12 @@ val pf_type_id : Proof_type.goal Evd.sigma -> EConstr.types -> Id.t val pf_abs_evars : Proof_type.goal Evd.sigma -> evar_map * EConstr.t -> - int * EConstr.t * Constr.existential_key list * + int * EConstr.t * Evar.t list * Evd.evar_universe_context val pf_abs_evars2 : (* ssr2 *) Proof_type.goal Evd.sigma -> Evar.t list -> evar_map * EConstr.t -> - int * EConstr.t * Constr.existential_key list * + int * EConstr.t * Evar.t list * Evd.evar_universe_context val pf_abs_cterm : Proof_type.goal Evd.sigma -> int -> EConstr.t -> EConstr.t @@ -214,7 +215,7 @@ val pf_mkSsrConst : string -> Proof_type.goal Evd.sigma -> EConstr.t * Proof_type.goal Evd.sigma -val new_wild_id : tac_ctx -> Names.identifier * tac_ctx +val new_wild_id : tac_ctx -> Names.Id.t * tac_ctx val pf_fresh_global : @@ -228,7 +229,7 @@ val is_tagged : string -> string -> bool val has_discharged_tag : string -> bool val ssrqid : string -> Libnames.qualid val new_tmp_id : - tac_ctx -> (Names.identifier * Names.name ref) * tac_ctx + tac_ctx -> (Names.Id.t * Names.name ref) * tac_ctx val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : Proof_type.goal Evd.sigma -> @@ -252,7 +253,7 @@ val red_product_skip_id : env -> evar_map -> EConstr.t -> EConstr.t val ssrautoprop_tac : - (Constr.existential_key Evd.sigma -> Constr.existential_key list Evd.sigma) ref + (Evar.t Evd.sigma -> Evar.t list Evd.sigma) ref val mkProt : EConstr.t -> diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 832044909..bd9a05891 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Util open Names open Printer diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli index fb1b58ac3..8dc28d8b7 100644 --- a/plugins/ssr/ssrelim.mli +++ b/plugins/ssr/ssrelim.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrmatching_plugin val ssrelim : diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index af315aac5..dbe13aec9 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ltac_plugin open Util open Names @@ -343,7 +344,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = Term.destConst elim in let mp,dp,l = repr_con (constant_of_kn (canonical_con elim)) in - let l' = label_of_id (Nameops.add_suffix (id_of_label l) "_r") in + let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (canonical_con (make_con mp dp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli index 9c5fd4983..f712002c1 100644 --- a/plugins/ssr/ssrequality.mli +++ b/plugins/ssr/ssrequality.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrmatching_plugin open Ssrast diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 663bca15e..2b10f2f35 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Tacmach diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 6fb97d524..ead361745 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Ltac_plugin diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index b850b0e95..96a75ba27 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Pp open Term diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index e90e75552..5f5c7f34a 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrmatching_plugin open Ssrast open Ssrcommon diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 1fba39150..5fd377233 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API open Names open Pp open Pcoq diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index bf6f44f11..154820666 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -8,6 +8,9 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API + val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index e865ef706..427109c1b 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Pp open Names open Printer diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 56ec145ad..9207b9e43 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrast val pp_term : diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 0fe8fdc26..67b705190 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Names open Constr open Termops diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli index b8e95b2b1..1d1887138 100644 --- a/plugins/ssr/ssrtacticals.mli +++ b/plugins/ssr/ssrtacticals.mli @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API + val tclSEQAT : Ltac_plugin.Tacinterp.interp_sign -> Ltac_plugin.Tacinterp.Value.t -> diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index b154cf217..6fbfbf03c 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -8,6 +8,8 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API +open Grammar_API open Names open Term open Termops diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 3c995b1bb..91e40f368 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Util open Names open Term diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli index 6fd906ff4..8a7bd5d6e 100644 --- a/plugins/ssr/ssrview.mli +++ b/plugins/ssr/ssrview.mli @@ -8,6 +8,7 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +open API open Ssrast open Ssrcommon -- cgit v1.2.3