diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-24 14:35:25 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-25 17:42:55 +0200 |
commit | bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 (patch) | |
tree | 49bf826bd68429694abb86df757d54147fb80554 /pretyping | |
parent | 0897d0f642c19419c513f9609782436bebf28f5b (diff) |
[general] Remove Econstr dependency from `intf`
To this extent we factor out the relevant bits to a new file,
ltac_pretype.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/cases.ml | 3 | ||||
-rw-r--r-- | pretyping/cases.mli | 7 | ||||
-rw-r--r-- | pretyping/constr_matching.ml | 1 | ||||
-rw-r--r-- | pretyping/constr_matching.mli | 1 | ||||
-rw-r--r-- | pretyping/detyping.ml | 1 | ||||
-rw-r--r-- | pretyping/detyping.mli | 1 | ||||
-rw-r--r-- | pretyping/glob_ops.ml | 1 | ||||
-rw-r--r-- | pretyping/glob_ops.mli | 4 | ||||
-rw-r--r-- | pretyping/ltac_pretype.ml | 68 | ||||
-rw-r--r-- | pretyping/patternops.mli | 1 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 1 | ||||
-rw-r--r-- | pretyping/pretyping.mli | 1 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
-rw-r--r-- | pretyping/tacred.mli | 1 |
14 files changed, 86 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 08ce72932..aefa09dbe 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -33,6 +33,7 @@ open Evarsolve open Evarconv open Evd open Context.Rel.Declaration +open Ltac_pretype module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -245,7 +246,7 @@ let push_history_pattern n pci cont = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 7bdc604b8..cbf5788e4 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -14,6 +14,7 @@ open EConstr open Inductiveops open Glob_term open Evarutil +open Ltac_pretype (** {5 Compilation of pattern-matching } *) @@ -101,7 +102,7 @@ and pattern_continuation = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -119,11 +120,11 @@ val prepare_predicate : ?loc:Loc.t -> Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> - Glob_term.ltac_var_map -> + Ltac_pretype.ltac_var_map -> (types * tomatch_type) list -> (rel_context * rel_context) list -> constr option -> glob_constr option -> (Evd.evar_map * Names.name list * constr) list val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name -> - Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map + Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 0973d73ee..9128d4042 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -22,6 +22,7 @@ open Pattern open Patternops open Misctypes open Context.Rel.Declaration +open Ltac_pretype (*i*) (* Given a term with second-order variables in it, diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 1d7019d09..34c62043e 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -13,6 +13,7 @@ open Term open EConstr open Environ open Pattern +open Ltac_pretype type binding_bound_vars = Id.Set.t diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f3e8e72bb..c02fc5aaf 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -27,6 +27,7 @@ open Mod_subst open Misctypes open Decl_kinds open Context.Named.Declaration +open Ltac_pretype type _ delay = | Now : 'a delay diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index b70bfd83c..f03bde68e 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -15,6 +15,7 @@ open Termops open Mod_subst open Misctypes open Evd +open Ltac_pretype type _ delay = | Now : 'a delay diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 7804cc679..055fd68f6 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -13,6 +13,7 @@ open Globnames open Misctypes open Glob_term open Evar_kinds +open Ltac_pretype (* Untyped intermediate terms, after ASTs and before constr. *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 49ea9727c..f27928662 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name -val empty_lvar : Glob_term.ltac_var_map +val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name +val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml new file mode 100644 index 000000000..be8579c2e --- /dev/null +++ b/pretyping/ltac_pretype.ml @@ -0,0 +1,68 @@ +open Names +open Glob_term + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * EConstr.constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = EConstr.constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } + +(** Ltac variable maps *) +type var_map = constr_under_binders Id.Map.t +type uconstr_var_map = closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 3a1faf1c7..ffe0186af 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -12,6 +12,7 @@ open Glob_term open Mod_subst open Misctypes open Pattern +open Ltac_pretype (** {5 Functions on patterns} *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ea1f2de53..30783bfad 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,6 +43,7 @@ open Glob_term open Glob_ops open Evarconv open Misctypes +open Ltac_pretype module NamedDecl = Context.Named.Declaration diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 5822f5add..6537d1ecf 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -18,6 +18,7 @@ open Evd open EConstr open Glob_term open Evarutil +open Ltac_pretype (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d04dcb8e3..9904b7354 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,3 +1,4 @@ +Ltac_pretype Locusops Pretype_errors Reductionops diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 91726e8c6..a6b8262f7 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -15,6 +15,7 @@ open Pattern open Globnames open Locus open Univ +open Ltac_pretype type reduction_tactic_error = InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) |