diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/detyping.ml | 3 | ||||
-rw-r--r-- | pretyping/pattern.ml | 22 | ||||
-rw-r--r-- | pretyping/pattern.mli | 2 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 6 | ||||
-rw-r--r-- | pretyping/rawterm.ml | 8 | ||||
-rw-r--r-- | pretyping/rawterm.mli | 8 | ||||
-rw-r--r-- | pretyping/tacred.ml | 17 | ||||
-rw-r--r-- | pretyping/tacred.mli | 5 |
8 files changed, 42 insertions, 29 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f1da217a6..d46fd226e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -658,7 +658,8 @@ let rec subst_rawconstr subst raw = if ref' == ref then raw else RHole (loc,InternalHole) | RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole | - TomatchTypeParameter _ | GoalEvar | ImpossibleCase)) -> raw + TomatchTypeParameter _ | GoalEvar | ImpossibleCase | MatchingVar _)) -> + raw | RCast (loc,r1,k) -> (match k with diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 7b8c62360..105672564 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -92,6 +92,7 @@ let head_of_constr_reference c = match kind_of_term c with open Evd let pattern_of_constr sigma t = + let ctx = ref [] in let rec pattern_of_constr t = match kind_of_term t with | Rel n -> PRel n @@ -106,9 +107,11 @@ let pattern_of_constr sigma t = | App (f,a) -> (match match kind_of_term f with - Evar (evk,args) -> + Evar (evk,args as ev) -> (match snd (Evd.evar_source evk sigma) with - MatchingVar (true,n) -> Some n + MatchingVar (true,id) -> + ctx := (id,None,existential_type sigma ev)::!ctx; + Some id | _ -> None) | _ -> None with @@ -117,9 +120,11 @@ let pattern_of_constr sigma t = | 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 (evk,ctxt) -> + | Evar (evk,ctxt as ev) -> (match snd (Evd.evar_source evk sigma) with - | MatchingVar (b,n) -> assert (not b); PMeta (Some n) + | MatchingVar (b,id) -> + ctx := (id,None,existential_type sigma ev)::!ctx; + assert (not b); PMeta (Some id) | GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt) | _ -> PMeta None) | Case (ci,p,a,br) -> @@ -129,8 +134,11 @@ let pattern_of_constr sigma t = pattern_of_constr p,pattern_of_constr a, Array.map pattern_of_constr br) | Fix f -> PFix f - | CoFix f -> PCoFix f - in pattern_of_constr t + | CoFix f -> PCoFix f in + let p = pattern_of_constr t in + (* side-effect *) + (* Warning: the order of dependencies in ctx is not ensured *) + (!ctx,p) (* To process patterns, we need a translation without typing at all. *) @@ -167,7 +175,7 @@ let rec subst_pattern subst pat = | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else - pattern_of_constr Evd.empty t + snd (pattern_of_constr Evd.empty t) | PVar _ | PEvar _ | PRel _ -> pat diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 0e87025fc..e7460377b 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 : Evd.evar_map -> constr -> constr_pattern +val pattern_of_constr : Evd.evar_map -> constr -> named_context * 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.mllib b/pretyping/pretyping.mllib index b40476c97..e847894a5 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -11,6 +11,9 @@ Typing Evarutil Term_dnet Recordops +Rawterm +Pattern +Matching Tacred Evarconv Typeclasses_errors @@ -19,11 +22,8 @@ Classops Coercion Unification Clenv -Rawterm -Pattern Detyping Indrec Cases Pretyping -Matching diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 727ac117c..16421b2a7 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -344,10 +344,10 @@ let no_occurrences_expr = (true,[]) type 'a with_occurrences = occurrences_expr * 'a -type ('a,'b) red_expr_gen = +type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf - | Simpl of 'a with_occurrences option + | Simpl of 'c with_occurrences option | Cbv of 'b raw_red_flag | Lazy of 'b raw_red_flag | Unfold of 'b with_occurrences list @@ -356,8 +356,8 @@ type ('a,'b) red_expr_gen = | ExtraRedExpr of string | CbvVm -type ('a,'b) may_eval = +type ('a,'b,'c) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a,'b) red_expr_gen * 'a + | ConstrEval of ('a,'b,'c) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 5cf227440..ac4f0dec6 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -155,10 +155,10 @@ val no_occurrences_expr : occurrences_expr type 'a with_occurrences = occurrences_expr * 'a -type ('a,'b) red_expr_gen = +type ('a,'b,'c) red_expr_gen = | Red of bool | Hnf - | Simpl of 'a with_occurrences option + | Simpl of 'c with_occurrences option | Cbv of 'b raw_red_flag | Lazy of 'b raw_red_flag | Unfold of 'b with_occurrences list @@ -167,8 +167,8 @@ type ('a,'b) red_expr_gen = | ExtraRedExpr of string | CbvVm -type ('a,'b) may_eval = +type ('a,'b,'c) may_eval = | ConstrTerm of 'a - | ConstrEval of ('a,'b) red_expr_gen * 'a + | ConstrEval of ('a,'b,'c) red_expr_gen * 'a | ConstrContext of (loc * identifier) * 'a | ConstrTypeOf of 'a diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 7079b937b..a103c49b6 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -23,6 +23,8 @@ open Closure open Reductionops open Cbv open Rawterm +open Pattern +open Matching (* Errors *) @@ -733,10 +735,10 @@ let simpl env sigma c = strong whd_simpl env sigma c (* Reduction at specific subterms *) -let is_head c t = +let matches_head c t = match kind_of_term t with - | App (f,_) -> f = c - | _ -> false + | App (f,_) -> matches c f + | _ -> raise PatternMatchingFailure let contextually byhead ((nowhere_except_in,locs),c) f env sigma t = let maxocc = List.fold_right max locs 0 in @@ -744,22 +746,23 @@ let contextually byhead ((nowhere_except_in,locs),c) f env sigma t = let rec traverse (env,c as envc) t = if nowhere_except_in & (!pos > maxocc) then t else - if (not byhead & eq_constr c t) or (byhead & is_head c t) then + try + let subst = if byhead then matches_head c t else matches c t in let ok = if nowhere_except_in then List.mem !pos locs else not (List.mem !pos locs) in incr pos; if ok then - f env sigma t + f subst env sigma t else if byhead then (* find other occurrences of c in t; TODO: ensure left-to-right *) let (f,l) = destApp t in mkApp (f, array_map_left (traverse envc) l) else t - else + with PatternMatchingFailure -> map_constr_with_binders_left_to_right - (fun d (env,c) -> (push_rel d env,lift 1 c)) + (fun d (env,c) -> (push_rel d env,lift_pattern 1 c)) traverse envc t in let t' = traverse (env,c) t in diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 80eca2bcc..2bba87a75 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -17,6 +17,7 @@ open Reductionops open Closure open Rawterm open Termops +open Pattern (*i*) type reduction_tactic_error = @@ -92,5 +93,5 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> Libnames.global_reference -> types -> types -val contextually : bool -> occurrences * constr -> reduction_function - -> reduction_function +val contextually : bool -> occurrences * constr_pattern -> + (patvar_map -> reduction_function) -> reduction_function |