Find_subterm API using EConstr.

6 files changed, 39 insertions, 32 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 4b9cf415f..d7f2d54aa 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -11,7 +11,7 @@ open Util
 open CErrors
 open Names
 open Locus
-open Term
+open EConstr
 open Nameops
 open Termops
 open Pretype_errors
@@ -63,7 +63,10 @@ let proceed_with_occurrences f occs x =
 
 let map_named_declaration_with_hyploc f hyploc acc decl =
   let open Context.Named.Declaration in
-  let f = f (Some (NamedDecl.get_id decl, hyploc)) in
+  let f acc typ =
+    let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc (EConstr.of_constr typ) in
+    acc, EConstr.Unsafe.to_constr typ
+  in
   match decl,hyploc with
   | LocalAssum (id,_), InHypValueOnly ->
       error_occurrences_error (IncorrectInValueOccurrence id)
@@ -82,10 +85,10 @@ let map_named_declaration_with_hyploc f hyploc acc decl =
 
 exception SubtermUnificationError of subterm_unification_error
 
-exception NotUnifiable of (constr * constr * unification_error) option
+exception NotUnifiable of (Constr.t * Constr.t * unification_error) option
 
 type 'a testing_function = {
-  match_fun : 'a -> constr -> 'a;
+  match_fun : 'a -> EConstr.constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
@@ -130,7 +133,8 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
     with NotUnifiable _ ->
       subst_below k t
   and subst_below k t =
-    map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t
+    let substrec i c = EConstr.Unsafe.to_constr (substrec i (EConstr.of_constr c)) in
+    EConstr.of_constr (map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k (EConstr.Unsafe.to_constr t))
   in
   let t' = substrec 0 t in
   (!pos, t')
@@ -138,8 +142,8 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
 let replace_term_occ_modulo occs test bywhat t =
   let occs',like_first =
     match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
-  proceed_with_occurrences
-    (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t
+  EConstr.Unsafe.to_constr (proceed_with_occurrences
+    (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t)
 
 let replace_term_occ_decl_modulo occs test bywhat d =
   let (plocs,hyploc),like_first =
@@ -154,11 +158,12 @@ let replace_term_occ_decl_modulo occs test bywhat d =
 
 let make_eq_univs_test env evd c =
   { match_fun = (fun evd c' ->
-    let b, cst = Universes.eq_constr_universes_proj env c c' in
-      if b then
+    match EConstr.eq_constr_universes_proj env evd c c' with
+    | None -> raise (NotUnifiable None)
+    | Some cst ->
 	try Evd.add_universe_constraints evd cst
 	with Evd.UniversesDiffer -> raise (NotUnifiable None)
-      else raise (NotUnifiable None));
+    );
   merge_fun = (fun evd _ -> evd);
   testing_state = evd;
   last_found = None
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index c741ab048..49a5dd7f2 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -26,7 +26,7 @@ exception SubtermUnificationError of subterm_unification_error
     with None. *)
 
 type 'a testing_function = {
-  match_fun : 'a -> constr -> 'a;
+  match_fun : 'a -> EConstr.constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
   mutable last_found : position_reporting option
@@ -34,7 +34,7 @@ type 'a testing_function = {
 
 (** This is the basic testing function, looking for exact matches of a
     closed term *)
-val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
+val make_eq_univs_test : env -> evar_map -> EConstr.constr -> evar_map testing_function
 
 (** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm
     modulo a testing function [test] and replaces successfully
@@ -42,26 +42,26 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function
     ()]; it turns a NotUnifiable exception raised by the testing
     function into a SubtermUnificationError. *)
 val replace_term_occ_modulo : occurrences or_like_first ->
-  'a testing_function -> (unit -> constr) -> constr -> constr
+  'a testing_function -> (unit -> EConstr.constr) -> EConstr.constr -> constr
 
 (** [replace_term_occ_decl_modulo] is similar to
     [replace_term_occ_modulo] but for a named_declaration. *)
 val replace_term_occ_decl_modulo :
   (occurrences * hyp_location_flag) or_like_first ->
-  'a testing_function -> (unit -> constr) ->
+  'a testing_function -> (unit -> EConstr.constr) ->
   Context.Named.Declaration.t -> Context.Named.Declaration.t
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
     unifying universes which results in a set of constraints. *)
 val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
-  constr -> constr -> constr * evar_map
+  EConstr.constr -> EConstr.constr -> constr * evar_map
 
 (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of 
     closed [c] at positions [occl] by [Rel 1] in [decl]. *)
 val subst_closed_term_occ_decl : env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
-  constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map
+  EConstr.constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map
 
 (** Miscellaneous *)
 val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 5b0958695..f8f6d44bf 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -27,7 +27,7 @@ type unification_error =
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
-type position_reporting = (position * int) * constr
+type position_reporting = (position * int) * EConstr.t
 
 type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 73f81923f..b015add79 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -28,7 +28,7 @@ type unification_error =
 
 type position = (Id.t * Locus.hyp_location_flag) option
 
-type position_reporting = (position * int) * constr
+type position_reporting = (position * int) * EConstr.t
 
 type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index c1e9573d2..290d77b1b 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1150,13 +1150,14 @@ let compute = cbv_betadeltaiota
  * the specified occurrences. *)
 
 let abstract_scheme env (locc,a) (c, sigma) =
-  let ta = Retyping.get_type_of env sigma (EConstr.of_constr a) in
+  let a = EConstr.of_constr a in
+  let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env ta Anonymous in
   if occur_meta sigma (EConstr.of_constr ta) then error "Cannot find a type for the generalisation.";
-  if occur_meta sigma (EConstr.of_constr a) then
+  if occur_meta sigma a then
     mkLambda (na,ta,c), sigma
   else
-    let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in
+    let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a (EConstr.of_constr c) in
       mkLambda (na,ta,c'), sigma'
 
 let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 848a2f4a8..8865e69ef 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -89,7 +89,7 @@ let abstract_scheme env evd c l lname_typ =
        else *) 
        if occur_meta evd (EConstr.of_constr a) then mkLambda_name env (na,ta,t), evd
        else
-	 let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in
+	 let t', evd' = Find_subterm.subst_closed_term_occ env evd locc (EConstr.of_constr a) (EConstr.of_constr t) in
 	   mkLambda_name env (na,ta,t'), evd')
     (c,evd)
     (List.rev l)
@@ -1544,20 +1544,21 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     else default_matching_flags pending in
   let n = List.length (snd (decompose_app c)) in
   let matching_fun _ t =
+    let open EConstr in
     try
       let t',l2 =
         if from_prefix_of_ind then
           (* We check for fully applied subterms of the form "u u1 .. un" *)
           (* of inductive type knowing only a prefix "u u1 .. ui" *)
-          let t,l = decompose_app t in
+          let t,l = decompose_app sigma t in
           let l1,l2 =
             try List.chop n l with Failure _ -> raise (NotUnifiable None) in
-          if not (List.for_all closed0 l2) then raise (NotUnifiable None)
+          if not (List.for_all (fun c -> Vars.closed0 sigma c) l2) then raise (NotUnifiable None)
           else
             applist (t,l1), l2
         else t, [] in
-      let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in
-      let ty = Retyping.get_type_of env sigma (EConstr.of_constr t) in
+      let sigma = w_typed_unify env sigma Reduction.CONV flags c (EConstr.Unsafe.to_constr t') in
+      let ty = Retyping.get_type_of env sigma t in
       if not (is_correct_type ty) then raise (NotUnifiable None);
       Some(sigma, t, l2)
     with
@@ -1568,7 +1569,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   let merge_fun c1 c2 =
     match c1, c2 with
     | Some (evd,c1,x), Some (_,c2,_) ->
-      let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
+      let (evd,b) = infer_conv ~pb:CONV env evd (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
       if b then Some (evd, c1, x) else raise (NotUnifiable None)
     | Some _, None -> c1
     | None, Some _ -> c2
@@ -1578,13 +1579,13 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   (fun test -> match test.testing_state with
   | None -> None
   | Some (sigma,_,l) ->
-     let c = applist (nf_evar sigma (local_strong whd_meta sigma (EConstr.of_constr c)),l) in
+     let c = applist (nf_evar sigma (local_strong whd_meta sigma (EConstr.of_constr c)), List.map (EConstr.to_constr sigma) l) in
      let univs, subst = nf_univ_variables sigma in
      Some (sigma,subst_univs_constr subst c))
 
 let make_eq_test env evd c =
   let out cstr =
-    match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, c)
+    match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, EConstr.Unsafe.to_constr c)
   in
   (make_eq_univs_test env evd c, out)
 
@@ -1601,7 +1602,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       x
   in
   let likefirst = clause_with_generic_occurrences occs in
-  let mkvarid () = mkVar id in
+  let mkvarid () = EConstr.mkVar id in
   let compute_dependency _ d (sign,depdecls) =
     let hyp = NamedDecl.get_id d in
     match occurrences_of_hyp hyp occs with
@@ -1630,7 +1631,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
       | NoOccurrences -> concl
       | occ ->
           let occ = if likefirst then LikeFirst else AtOccs occ in
-          replace_term_occ_modulo occ test mkvarid concl
+          replace_term_occ_modulo occ test mkvarid (EConstr.of_constr concl)
     in
     let lastlhyp =
       if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
@@ -1674,7 +1675,7 @@ let make_abstraction env evd ccl abs =
         env evd (snd c) None occs check_occs ccl
   | AbstractExact (name,c,ty,occs,check_occs) ->
       make_abstraction_core name
-        (make_eq_test env evd c)
+        (make_eq_test env evd (EConstr.of_constr c))
         env evd c ty occs check_occs ccl
 
 let keyed_unify env evd kop =