Clenv API using EConstr.

8 files changed, 43 insertions, 18 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 77e91095fc..ee6355736b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-module CVars = Vars
-
 open CErrors
 open Util
 open Names
@@ -184,10 +182,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
       | None -> raise Not_found
       | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in
   let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
-  let c' = EConstr.of_constr (CVars.subst_univs_level_constr subst c) in
-  let t' = CVars.subst_univs_level_constr subst t' in
-  let bs' = List.map (CVars.subst_univs_level_constr subst %> EConstr.of_constr) bs in
-  let h, _ = decompose_app_vect sigma (EConstr.of_constr t') in
+  let c = EConstr.of_constr c in
+  let c' = subst_univs_level_constr subst c in
+  let t' = EConstr.of_constr t' in
+  let t' = subst_univs_level_constr subst t' in
+  let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in
+  let h, _ = decompose_app_vect sigma t' in
     ctx',(EConstr.of_constr h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1),
     (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
     (n, Stack.zip sigma (t2,sk2))
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 142e430ff8..7fe81c9a43 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -58,3 +58,16 @@ let map_red_expr_gen f g h = function
   | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
   | Cbn flags -> Cbn (map_flags g flags)
   | ExtraRedExpr _ | Red _ | Hnf as x -> x
+
+(** Mapping bindings *)
+
+let map_explicit_bindings f l =
+  let map (loc, hyp, x) = (loc, hyp, f x) in
+  List.map map l
+
+let map_bindings f = function
+| ImplicitBindings l -> ImplicitBindings (List.map f l)
+| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl)
+| NoBindings -> NoBindings
+
+let map_with_bindings f (x, bl) = (f x, map_bindings f bl)
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 337473a6fd..f30dc1a4b6 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -27,3 +27,8 @@ val intro_pattern_naming_eq :
 
 val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
   ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
+
+(** Mapping bindings *)
+
+val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
+val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0e0b807441..0dd615bfb7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1588,9 +1588,11 @@ let meta_instance sigma b =
   if Metaset.is_empty fm then b.rebus
   else
     let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    instance sigma c_sigma (EConstr.of_constr b.rebus)
+    EConstr.of_constr (instance sigma c_sigma b.rebus)
 
-let nf_meta sigma c = meta_instance sigma (mk_freelisted c)
+let nf_meta sigma c =
+  let cl = mk_freelisted c in
+  EConstr.Unsafe.to_constr (meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus })
 
 (* Instantiate metas that create beta/iota redexes *)
 
@@ -1652,7 +1654,7 @@ let meta_reducible_instance evd b =
     | _ -> EConstr.map evd irec u
   in
   if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
-  else EConstr.Unsafe.to_constr (irec (EConstr.of_constr b.rebus))
+  else irec b.rebus
 
 
 let head_unfold_under_prod ts env sigma c =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c3b82729d5..864b1a625c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -295,6 +295,6 @@ val whd_betaiota_deltazeta_for_iota_state :
   state * Cst_stack.t
 
 (** {6 Meta-related reduction functions } *)
-val meta_instance : evar_map -> constr freelisted -> constr
+val meta_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
 val nf_meta       : evar_map -> constr -> constr
-val meta_reducible_instance : evar_map -> constr freelisted -> constr
+val meta_reducible_instance : evar_map -> EConstr.constr freelisted -> EConstr.constr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cf58a0b668..29697260f7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -40,6 +40,7 @@ let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv)) in
+  let ty = Evd.map_fl EConstr.of_constr ty in
   meta_instance evd ty
 
 let constant_type_knowing_parameters env sigma cst jl =
@@ -256,7 +257,7 @@ let rec execute env evdref cstr =
   let cstr = EConstr.of_constr (whd_evar !evdref (EConstr.Unsafe.to_constr cstr)) in
   match EConstr.kind !evdref cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = EConstr.of_constr (meta_type !evdref n) }
+        { uj_val = cstr; uj_type = meta_type !evdref n }
 
     | Evar ev ->
 	let ty = EConstr.existential_type !evdref ev in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 1fb414906b..94a56b6e11 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -31,7 +31,7 @@ val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts
 val e_check   : env -> evar_map ref -> EConstr.constr -> EConstr.types -> unit
 
 (** Returns the instantiated type of a metavariable *)
-val meta_type : evar_map -> metavariable -> types
+val meta_type : evar_map -> metavariable -> EConstr.types
 
 (** Solve existential variables using typing *)
 val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 483fefaf2e..2b2069ec45 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -617,10 +617,10 @@ let subst_defined_metas_evars sigma (bl,el) c =
   in try Some (substrec c) with Not_found -> None
 
 let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM tyN =
-  match subst_defined_metas_evars sigma (metasubst,[]) (EConstr.of_constr tyM) with
+  match subst_defined_metas_evars sigma (metasubst,[]) tyM with
   | None -> sigma
   | Some m ->
-  match subst_defined_metas_evars sigma (metasubst,[]) (EConstr.of_constr tyN) with
+  match subst_defined_metas_evars sigma (metasubst,[]) tyN with
   | None -> sigma
   | Some n ->
     if is_ground_term sigma m && is_ground_term sigma n then
@@ -705,6 +705,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 		(try
                    let tyM = Typing.meta_type sigma k in
                    let tyN = get_type_of curenv ~lax:true sigma cN in
+                   let tyN = EConstr.of_constr tyN in
                      check_compatibility curenv CUMUL flags substn tyN tyM
 		 with RetypeError _ ->
                    (* Renounce, maybe metas/evars prevents typing *) sigma)
@@ -724,6 +725,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	    if opt.with_types && flags.check_applied_meta_types then
               (try
                  let tyM = get_type_of curenv ~lax:true sigma cM in
+                 let tyM = EConstr.of_constr tyM in
                  let tyN = Typing.meta_type sigma k in
                    check_compatibility curenv CUMUL flags substn tyM tyN
                with RetypeError _ ->
@@ -977,6 +979,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	     try (* Ensure we call conversion on terms of the same type *)
 	       let tyM = get_type_of curenv ~lax:true sigma m1 in
 	       let tyN = get_type_of curenv ~lax:true sigma n1 in
+	       let tyM = EConstr.of_constr tyM in
+	       let tyN = EConstr.of_constr tyN in
 	       check_compatibility curenv CUMUL flags substn tyM tyN
 	     with RetypeError _ ->
 	       (* Renounce, maybe metas/evars prevents typing *) sigma
@@ -1265,7 +1269,7 @@ let w_coerce_to_type env evd c cty mvty =
 let w_coerce env evd mv c =
   let cty = get_type_of env evd c in
   let mvty = Typing.meta_type evd mv in
-  w_coerce_to_type env evd c (EConstr.of_constr cty) (EConstr.of_constr mvty)
+  w_coerce_to_type env evd c (EConstr.of_constr cty) mvty
 
 let unify_to_type env sigma flags c status u =
   let sigma, c = refresh_universes (Some false) env sigma c in
@@ -1275,6 +1279,7 @@ let unify_to_type env sigma flags c status u =
 
 let unify_type env sigma flags mv status c =
   let mvty = Typing.meta_type sigma mv in
+  let mvty = EConstr.Unsafe.to_constr mvty in
   let mvty = nf_meta sigma mvty in
     unify_to_type env sigma 
       (set_flags_for_type flags)
@@ -1923,7 +1928,6 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
   let flags = { flags with core_unify_flags = flags.subterm_unify_flags } in
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
-  let typp = EConstr.of_constr typp in
   let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
   let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in
   if not b then
@@ -1942,7 +1946,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
 
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
   let typp = Typing.meta_type evd p in
-  let evd, pred = abstract_list_all_with_dependencies env evd (EConstr.of_constr typp) typ oplist in
+  let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
   let pred = EConstr.of_constr pred in
   w_merge env false flags.merge_unify_flags
     (evd,[p,pred,(Conv,TypeProcessed)],[])