diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 1 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 | ||||
| -rw-r--r-- | pretyping/pattern.ml | 29 | ||||
| -rw-r--r-- | pretyping/pattern.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 39 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 7 |
6 files changed, 54 insertions, 25 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 0d9a51ba37..ccba1d2cc1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -32,6 +32,7 @@ type hole_kind = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase + | MatchingVar of bool * identifier (* The type of mappings for existential variables *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 3974e65b42..b82e6d998d 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -94,6 +94,7 @@ type hole_kind = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase + | MatchingVar of bool * identifier (*********************************************************************) (*** Existential variables and unification states ***) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 9acdd15855..7b8c623607 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -89,7 +89,10 @@ let head_of_constr_reference c = match kind_of_term c with | Var id -> VarRef id | _ -> anomaly "Not a rigid reference" -let rec pattern_of_constr t = +open Evd + +let pattern_of_constr sigma t = + let rec pattern_of_constr t = match kind_of_term t with | Rel n -> PRel n | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n))) @@ -100,11 +103,25 @@ let rec pattern_of_constr t = | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) | Lambda (na,c,b) -> PLambda (na,pattern_of_constr c,pattern_of_constr b) - | App (f,a) -> PApp (pattern_of_constr f,Array.map pattern_of_constr a) + | App (f,a) -> + (match + match kind_of_term f with + Evar (evk,args) -> + (match snd (Evd.evar_source evk sigma) with + MatchingVar (true,n) -> Some n + | _ -> None) + | _ -> None + with + | Some n -> PSoApp (n,Array.to_list (Array.map pattern_of_constr a)) + | None -> PApp (pattern_of_constr f,Array.map (pattern_of_constr) a)) | Const sp -> PRef (ConstRef (constant_of_kn(canonical_con sp))) | Ind sp -> PRef (canonical_gr (IndRef sp)) | Construct sp -> PRef (canonical_gr (ConstructRef sp)) - | Evar (n,ctxt) -> PEvar (n,Array.map pattern_of_constr ctxt) + | Evar (evk,ctxt) -> + (match snd (Evd.evar_source evk sigma) with + | MatchingVar (b,n) -> assert (not b); PMeta (Some n) + | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt) + | _ -> PMeta None) | Case (ci,p,a,br) -> let cip = ci.ci_pp_info in let no = Some (ci.ci_npar,cip.ind_nargs) in @@ -113,6 +130,7 @@ let rec pattern_of_constr t = Array.map pattern_of_constr br) | Fix f -> PFix f | CoFix f -> PCoFix f + in pattern_of_constr t (* To process patterns, we need a translation without typing at all. *) @@ -144,11 +162,12 @@ let rec liftn_pattern k n = function let lift_pattern k = liftn_pattern k 1 -let rec subst_pattern subst pat = match pat with +let rec subst_pattern subst pat = + match pat with | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - pattern_of_constr t + pattern_of_constr Evd.empty t | PVar _ | PEvar _ | PRel _ -> pat diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index b0229ab618..0e87025fc8 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -66,7 +66,7 @@ val head_of_constr_reference : Term.constr -> global_reference a pattern; currently, no destructor (Cases, Fix, Cofix) and no existential variable are allowed in [c] *) -val pattern_of_constr : constr -> constr_pattern +val pattern_of_constr : Evd.evar_map -> constr -> constr_pattern (* [pattern_of_rawconstr l c] translates a term [c] with metavariables into a pattern; variables bound in [l] are replaced by the pattern to which they diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 288eb9da22..cfe028aa51 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -108,15 +108,16 @@ sig (* Generic call to the interpreter from rawconstr to constr, failing unresolved holes in the rawterm cannot be instantiated. - In [understand_ltac sigma env ltac_env constraint c], + In [understand_ltac expand_evars sigma env ltac_env constraint c], + expand_evars : expand inferred evars by their value if any sigma : initial set of existential variables (typically dependent subgoals) ltac_env : partial substitution of variables (used for the tactic language) constraint : tell if interpreted as a possibly constrained term or a type *) val understand_ltac : - evar_map -> env -> var_map * unbound_ltac_var_map -> + bool -> evar_map -> env -> var_map * unbound_ltac_var_map -> typing_constraint -> rawconstr -> evar_map * constr (* Standard call to get a constr from a rawconstr, resolving implicit args *) @@ -156,7 +157,7 @@ sig rawconstr -> unsafe_type_judgment val pretype_gen : - bool -> bool -> evar_map ref -> env -> + bool -> bool -> bool -> evar_map ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr @@ -307,7 +308,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env evdref j tycon | RPatVar (loc,(someta,n)) -> - anomaly "Found a pattern variable in a rawterm to type" + let ty = + match tycon with + | Some (None, ty) -> ty + | None | Some _ -> + e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in + let k = MatchingVar (someta,n) in + { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty } | RHole (loc,k) -> let ty = @@ -418,7 +425,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in let t = Retyping.get_type_of env sigma c in - make_judge c t + make_judge c (* use this for keeping evars: resj.uj_val *) t | _ -> resj end | _ -> resj in inh_conv_coerce_to_tycon loc env evdref resj tycon @@ -661,7 +668,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct error_unexpected_type_loc (loc_of_rawconstr c) env !evdref tj.utj_val v - let pretype_gen fail_evar resolve_classes evdref env lvar kind c = + let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c = let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in @@ -673,7 +680,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct evdref := Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:fail_evar env !evdref; - let c = nf_evar !evdref c' in + let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; c @@ -701,30 +708,30 @@ module Pretyping_F (Coercion : Coercion.S) = struct fail on unresolved evars; the unsafe_judgment list allows us to extend env with some bindings *) - let ise_pretype_gen fail_evar resolve_classes sigma env lvar kind c = + let ise_pretype_gen expand_evar fail_evar resolve_classes sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in - let c = pretype_gen fail_evar resolve_classes evdref env lvar kind c in + let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in !evdref, c (** Entry points of the high-level type synthesis algorithm *) let understand_gen kind sigma env c = - snd (ise_pretype_gen true true sigma env ([],[]) kind c) + snd (ise_pretype_gen true true true sigma env ([],[]) kind c) let understand sigma env ?expected_type:exptyp c = - snd (ise_pretype_gen true true sigma env ([],[]) (OfType exptyp) c) + snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c) let understand_type sigma env c = - snd (ise_pretype_gen true true sigma env ([],[]) IsType c) + snd (ise_pretype_gen true true true sigma env ([],[]) IsType c) - let understand_ltac sigma env lvar kind c = - ise_pretype_gen false false sigma env lvar kind c + let understand_ltac expand_evar sigma env lvar kind c = + ise_pretype_gen expand_evar false false sigma env lvar kind c let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c = - ise_pretype_gen false resolve_classes sigma env ([],[]) (OfType exptyp) c + ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c = - pretype_gen fail_evar resolve_classes evdref env ([],[]) kind c + pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c end module Default : S = Pretyping_F(Coercion.Default) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e3b18f73cb..75bd7874e7 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -51,15 +51,16 @@ sig (* Generic call to the interpreter from rawconstr to constr, failing unresolved holes in the rawterm cannot be instantiated. - In [understand_ltac sigma env ltac_env constraint c], + In [understand_ltac expand_evars sigma env ltac_env constraint c], + expand_evars : expand inferred evars by their value if any sigma : initial set of existential variables (typically dependent subgoals) ltac_env : partial substitution of variables (used for the tactic language) constraint : tell if interpreted as a possibly constrained term or a type *) val understand_ltac : - evar_map -> env -> var_map * unbound_ltac_var_map -> + bool -> evar_map -> env -> var_map * unbound_ltac_var_map -> typing_constraint -> rawconstr -> evar_map * constr (* Standard call to get a constr from a rawconstr, resolving implicit args *) @@ -97,7 +98,7 @@ sig rawconstr -> unsafe_type_judgment val pretype_gen : - bool -> bool -> evar_map ref -> env -> + bool -> bool -> bool -> evar_map ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr |