aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/constr_matching.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/constr_matching.ml')
-rw-r--r--pretyping/constr_matching.ml107
1 files changed, 62 insertions, 45 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 3c47cfdc4..d55350622 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -16,6 +16,7 @@ open Nameops
open Termops
open Reductionops
open Term
+open EConstr
open Vars
open Pattern
open Patternops
@@ -45,6 +46,7 @@ open Context.Rel.Declaration
*)
+type binding_bound_vars = Id.Set.t
type bound_ident_map = Id.t Id.Map.t
exception PatternMatchingFailure
@@ -56,14 +58,15 @@ let warn_meta_collision =
strbrk " and a metavariable of same name.")
-let constrain n (ids, m as x) (names, terms as subst) =
+let constrain sigma n (ids, m) (names, terms as subst) =
+ let open EConstr in
try
let (ids', m') = Id.Map.find n terms in
- if List.equal Id.equal ids ids' && eq_constr m m' then subst
+ if List.equal Id.equal ids ids' && eq_constr sigma m m' then subst
else raise PatternMatchingFailure
with Not_found ->
let () = if Id.Map.mem n names then warn_meta_collision n in
- (names, Id.Map.add n x terms)
+ (names, Id.Map.add n (ids, m) terms)
let add_binders na1 na2 binding_vars (names, terms as subst) =
match na1, na2 with
@@ -78,9 +81,9 @@ let add_binders na1 na2 binding_vars (names, terms as subst) =
(names, terms)
| _ -> subst
-let rec build_lambda vars ctx m = match vars with
+let rec build_lambda sigma vars ctx m = match vars with
| [] ->
- if Vars.closed0 m then m else raise PatternMatchingFailure
+ if Vars.closed0 sigma m then m else raise PatternMatchingFailure
| n :: vars ->
(* change [ x1 ... xn y z1 ... zm |- t ] into
[ x1 ... xn z1 ... zm |- lam y. t ] *)
@@ -95,7 +98,7 @@ let rec build_lambda vars ctx m = match vars with
let is_nondep t clear = match clear with
| [] -> true
| _ ->
- let rels = free_rels t in
+ let rels = free_rels sigma t in
let check i b = b || not (Int.Set.mem i rels) in
List.for_all_i check 1 clear
in
@@ -144,7 +147,7 @@ let rec build_lambda vars ctx m = match vars with
let vars = List.map map vars in
(** Create the abstraction *)
let m = mkLambda (na, Vars.lift keep t, m) in
- build_lambda vars (pre @ suf) m
+ build_lambda sigma vars (pre @ suf) m
let rec extract_bound_aux k accu frels ctx = match ctx with
| [] -> accu
@@ -162,41 +165,46 @@ let rec extract_bound_aux k accu frels ctx = match ctx with
let extract_bound_vars frels ctx =
extract_bound_aux 1 Id.Set.empty frels ctx
-let dummy_constr = mkProp
+let dummy_constr = EConstr.mkProp
let make_renaming ids = function
| (Name id, Name _, _) ->
begin
- try mkRel (List.index Id.equal id ids)
+ try EConstr.mkRel (List.index Id.equal id ids)
with Not_found -> dummy_constr
end
| _ -> dummy_constr
-let merge_binding allow_bound_rels ctx n cT subst =
+let to_fix (idx, (nas, cs, ts)) =
+ let inj = EConstr.of_constr in
+ (idx, (nas, Array.map inj cs, Array.map inj ts))
+
+let merge_binding sigma allow_bound_rels ctx n cT subst =
let c = match ctx with
| [] -> (* Optimization *)
([], cT)
| _ ->
- let frels = free_rels cT in
+ let frels = free_rels sigma cT in
if allow_bound_rels then
let vars = extract_bound_vars frels ctx in
let ordered_vars = Id.Set.elements vars in
let rename binding = make_renaming ordered_vars binding in
let renaming = List.map rename ctx in
- (ordered_vars, substl renaming cT)
+ (ordered_vars, Vars.substl renaming cT)
else
let depth = List.length ctx in
let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in
if depth < min_elt then
- ([], lift (- depth) cT)
+ ([], Vars.lift (- depth) cT)
else raise PatternMatchingFailure
in
- constrain n c subst
+ constrain sigma n c subst
let matches_core env sigma convert allow_partial_app allow_bound_rels
(binding_vars,pat) c =
+ let open EConstr in
let convref ref c =
- match ref, kind_of_term c with
+ match ref, EConstr.kind sigma c with
| VarRef id, Var id' -> Names.id_eq id id'
| ConstRef c, Const (c',_) -> Names.eq_constant c c'
| IndRef i, Ind (i', _) -> Names.eq_ind i i'
@@ -204,12 +212,12 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| _, _ ->
(if convert then
let sigma,c' = Evd.fresh_global env sigma ref in
- is_conv env sigma c' c
+ is_conv env sigma (EConstr.of_constr c') c
else false)
in
let rec sorec ctx env subst p t =
- let cT = strip_outer_cast t in
- match p,kind_of_term cT with
+ let cT = strip_outer_cast sigma t in
+ match p, EConstr.kind sigma cT with
| PSoApp (n,args),m ->
let fold (ans, seen) = function
| PRel n ->
@@ -218,13 +226,13 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| _ -> error "Only bound indices allowed in second order pattern matching."
in
let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
- let frels = free_rels cT in
+ let frels = free_rels sigma cT in
if Int.Set.subset frels relset then
- constrain n ([], build_lambda relargs ctx cT) subst
+ constrain sigma n ([], build_lambda sigma relargs ctx cT) subst
else
raise PatternMatchingFailure
- | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst
+ | PMeta (Some n), m -> merge_binding sigma allow_bound_rels ctx n cT subst
| PMeta None, m -> subst
@@ -236,11 +244,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PRel n1, Rel n2 when Int.equal n1 n2 -> subst
- | PSort GProp, Sort (Prop Null) -> subst
-
- | PSort GSet, Sort (Prop Pos) -> subst
+ | PSort ps, Sort s ->
- | PSort (GType _), Sort (Type _) -> subst
+ begin match ps, ESorts.kind sigma s with
+ | GProp, Prop Null -> subst
+ | GSet, Prop Pos -> subst
+ | GType _, Type _ -> subst
+ | _ -> raise PatternMatchingFailure
+ end
| PApp (p, [||]), _ -> sorec ctx env subst p t
@@ -255,10 +266,10 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
let subst =
match meta with
| None -> subst
- | Some n -> merge_binding allow_bound_rels ctx n c subst in
+ | Some n -> merge_binding sigma allow_bound_rels ctx n c subst in
Array.fold_left2 (sorec ctx env) subst args1 args22
else (* Might be a projection on the right *)
- match kind_of_term c2 with
+ match EConstr.kind sigma c2 with
| Proj (pr, c) when not (Projection.unfolded pr) ->
(try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
sorec ctx env subst p term
@@ -266,7 +277,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| _ -> raise PatternMatchingFailure)
| PApp (c1,arg1), App (c2,arg2) ->
- (match c1, kind_of_term c2 with
+ (match c1, EConstr.kind sigma c2 with
| PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr))
|| Projection.unfolded pr ->
raise PatternMatchingFailure
@@ -296,29 +307,33 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
sorec ctx env subst c1 c2
| PProd (na1,c1,d1), Prod(na2,c2,d2) ->
- sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env)
+ sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PLambda (na1,c1,d1), Lambda(na2,c2,d2) ->
- sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env)
+ sorec ((na1,na2,c2)::ctx) (EConstr.push_rel (LocalAssum (na2,c2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
- | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
- sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env)
+ | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) ->
+ sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
+ (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2
+
+ | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) ->
+ sorec ((na1,na2,t2)::ctx) (EConstr.push_rel (LocalDef (na2,c2,t2)) env)
(add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
| PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
- let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in
- let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in
+ let ctx_b2,b2 = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(0) b2 in
+ let ctx_b2',b2' = decompose_lam_n_decls sigma ci.ci_cstr_ndecls.(1) b2' in
let n = Context.Rel.length ctx_b2 in
let n' = Context.Rel.length ctx_b2' in
- if noccur_between 1 n b2 && noccur_between 1 n' b2' then
+ if Vars.noccur_between sigma 1 n b2 && Vars.noccur_between sigma 1 n' b2' then
let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in
let ctx_br = List.fold_left f ctx ctx_b2 in
let ctx_br' = List.fold_left f ctx ctx_b2' in
let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in
- sorec ctx_br' (Environ.push_rel_context ctx_b2' env)
- (sorec ctx_br (Environ.push_rel_context ctx_b2 env)
+ sorec ctx_br' (push_rel_context ctx_b2' env)
+ (sorec ctx_br (push_rel_context ctx_b2 env)
(sorec ctx env subst a1 a2) b1 b2) b1' b2'
else
raise PatternMatchingFailure
@@ -345,8 +360,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
List.fold_left chk_branch chk_head br1
- | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst
- | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst
+ | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst
+ | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
| _ -> raise PatternMatchingFailure
in
@@ -372,8 +387,9 @@ let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
let isPMeta = function PMeta _ -> true | _ -> false
let matches_head env sigma pat c =
+ let open EConstr in
let head =
- match pat, kind_of_term c with
+ match pat, EConstr.kind sigma c with
| PApp (c1,arg1), App (c2,arg2) ->
if isPMeta c1 then c else
let n1 = Array.length arg1 in
@@ -386,7 +402,7 @@ let matches_head env sigma pat c =
let authorized_occ env sigma partial_app closed pat c mk_ctx =
try
let subst = matches_core_closed env sigma false partial_app pat c in
- if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst)
+ if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
then (fun next -> next ())
else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
with PatternMatchingFailure -> (fun next -> next ())
@@ -395,9 +411,10 @@ let subargs env v = Array.map_to_list (fun c -> (env, c)) v
(* Tries to match a subterm of [c] with [pat] *)
let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
+ let open EConstr in
let rec aux env c mk_ctx next =
let here = authorized_occ env sigma partial_app closed pat c mk_ctx in
- let next () = match kind_of_term c with
+ let next () = match EConstr.kind sigma c with
| Cast (c1,k,c2) ->
let next_mk_ctx = function
| [c1] -> mk_ctx (mkCast (c1, k, c2))
@@ -409,21 +426,21 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
| [c1; c2] -> mk_ctx (mkLambda (x, c1, c2))
| _ -> assert false
in
- let env' = Environ.push_rel (LocalAssum (x,c1)) env in
+ let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
try_aux [(env, c1); (env', c2)] next_mk_ctx next
| Prod (x,c1,c2) ->
let next_mk_ctx = function
| [c1; c2] -> mk_ctx (mkProd (x, c1, c2))
| _ -> assert false
in
- let env' = Environ.push_rel (LocalAssum (x,c1)) env in
+ let env' = EConstr.push_rel (LocalAssum (x,c1)) env in
try_aux [(env, c1); (env', c2)] next_mk_ctx next
| LetIn (x,c1,t,c2) ->
let next_mk_ctx = function
| [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
| _ -> assert false
in
- let env' = Environ.push_rel (LocalDef (x,c1,t)) env in
+ let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in
try_aux [(env, c1); (env', c2)] next_mk_ctx next
| App (c1,lc) ->
let topdown = true in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:26:54 +0000