Constr_matching API using EConstr.

1 files changed, 62 insertions, 43 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 1261844a0..ecf6b1121 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -57,14 +57,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 (EConstr.of_constr 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, EConstr.Unsafe.to_constr m) terms)
 
 let add_binders na1 na2 binding_vars (names, terms as subst) =
   match na1, na2 with
@@ -82,8 +83,9 @@ let add_binders na1 na2 binding_vars (names, terms as subst) =
 let rec build_lambda sigma vars ctx m = match vars with
 | [] ->
   let len = List.length ctx in
-  lift (-1 * len) m
+  EConstr.Vars.lift (-1 * len) m
 | n :: vars ->
+  let open EConstr in
   (* change [ x1 ... xn y z1 ... zm |- t ] into
      [ x1 ... xn z1 ... zm |- lam y. t ] *)
   let len = List.length ctx in
@@ -92,7 +94,7 @@ let rec build_lambda sigma vars ctx m = match vars with
     else if Int.equal i (pred n) then mkRel 1
     else mkRel (i + 1)
   in
-  let m = substl (List.init len init) m in
+  let m = Vars.substl (List.init len init) m in
   let pre, suf = List.chop (pred n) ctx in
   match suf with
   | [] -> assert false
@@ -100,7 +102,7 @@ let rec build_lambda sigma vars ctx m = match vars with
     let map i = if i > n then pred i else i in
     let vars = List.map map vars in
     (** Check that the abstraction is legal *)
-    let frels = free_rels sigma (EConstr.of_constr t) in
+    let frels = free_rels sigma t in
     let brels = List.fold_right Int.Set.add vars Int.Set.empty in
     let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in
     (** Create the abstraction *)
@@ -123,41 +125,55 @@ 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 local_assum (na, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalAssum (na, inj t)
+
+let local_def (na, b, t) =
+  let inj = EConstr.Unsafe.to_constr in
+  LocalDef (na, inj b, inj t)
+
+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 sigma (EConstr.of_constr cT) in
+    let open EConstr 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'
@@ -165,12 +181,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 (EConstr.of_constr c') (EConstr.of_constr 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 sigma (EConstr.of_constr t) in
-    match p,kind_of_term cT with
+    let cT = EConstr.of_constr (strip_outer_cast sigma t) in
+    match p, EConstr.kind sigma cT with
       | PSoApp (n,args),m ->
         let fold (ans, seen) = function
         | PRel n ->
@@ -179,9 +195,9 @@ 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 sigma (EConstr.of_constr cT) in
+        let frels = free_rels sigma cT in
         if Int.Set.subset frels relset then
-          constrain n ([], build_lambda sigma relargs ctx cT) subst
+          constrain sigma n ([], build_lambda sigma relargs ctx cT) subst
         else
           raise PatternMatchingFailure
 
@@ -219,15 +235,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
               | 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 (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr args2) in
-		     sorec ctx env subst p term
+	      (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in
+		     sorec ctx env subst p (EConstr.of_constr term)
 	       with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 	    | _ -> 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
@@ -237,8 +253,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	    with Invalid_argument _ -> raise PatternMatchingFailure
 	  else raise PatternMatchingFailure
 	| _, Proj (pr,c) when not (Projection.unfolded pr) ->
-	  (try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c) (Array.map_to_list EConstr.of_constr arg2) in
-		 sorec ctx env subst p term
+	  (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in
+		 sorec ctx env subst p (EConstr.of_constr term)
 	   with Retyping.RetypeError _ -> raise PatternMatchingFailure)	    
 	| _, _ ->
           try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2
@@ -249,32 +265,32 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	raise PatternMatchingFailure
 	
       | PApp (c, args), Proj (pr, c2) ->
-	(try let term = Retyping.expand_projection env sigma pr (EConstr.of_constr c2) [] in
-	       sorec ctx env subst p term
+	(try let term = Retyping.expand_projection env sigma pr c2 [] in
+	       sorec ctx env subst p (EConstr.of_constr term)
 	 with Retyping.RetypeError _ -> raise PatternMatchingFailure)
 
       | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 ->
           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) (Environ.push_rel (local_assum (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) (Environ.push_rel (local_assum (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)
+	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (local_def (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
-            let f l (LocalAssum (na,t) | LocalDef (na,_,t)) = (Anonymous,na,t)::l in
+	  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,EConstr.of_constr 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
@@ -306,8 +322,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
@@ -328,13 +344,14 @@ type matching_result =
     { m_sub : bound_ident_map * patvar_map;
       m_ctx : constr; }
 
-let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) )
+let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=EConstr.Unsafe.to_constr 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
@@ -345,6 +362,7 @@ let matches_head env sigma pat c =
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
 let authorized_occ env sigma partial_app closed pat c mk_ctx =
+  let open EConstr in
   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)
@@ -356,9 +374,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))
@@ -370,21 +389,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' = Environ.push_rel (local_assum (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' = Environ.push_rel (local_assum (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' = Environ.push_rel (local_def (x,c1,t)) env in
       try_aux [(env, c1); (env', c2)] next_mk_ctx next
   | App (c1,lc) ->
         let topdown = true in
@@ -440,8 +459,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
     let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
       if partial_app then
 	try 
-	  let term = Retyping.expand_projection env sigma p (EConstr.of_constr c') [] in
-	    aux env term mk_ctx next
+	  let term = Retyping.expand_projection env sigma p c' [] in
+	    aux env (EConstr.of_constr term) mk_ctx next
 	with Retyping.RetypeError _ -> next ()
       else
       try_aux [env, c'] next_mk_ctx next