Typing API using EConstr.

7 files changed, 78 insertions, 56 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 04f50d50ed..882c052f60 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1381,7 +1381,7 @@ and match_current pb (initial,tomatch) =
 	  let case =
 	    make_case_or_project pb.env indf ci pred current brvals
 	  in
-	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
+	  Typing.check_allowed_sort pb.env !(pb.evdref) mind (EConstr.of_constr current) (EConstr.of_constr pred);
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist typ inst }
 
@@ -1684,7 +1684,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 	(lift (n'-n) impossible_case_type, mkSort u)
     | Some t ->
         let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in
-        let evd,tt = Typing.type_of extenv !evdref t in
+        let evd,tt = Typing.type_of extenv !evdref (EConstr.of_constr t) in
         evdref := evd;
         (t,tt) in
   let b = e_cumul env evdref (EConstr.of_constr tt) (EConstr.mkSort s) (* side effect *) in
@@ -1920,7 +1920,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   assert (len == 0);
   let p = predicate 0 c in
   let env' = List.fold_right push_rel_context arsign env in
-  try let sigma' = fst (Typing.type_of env' sigma p) in
+  try let sigma' = fst (Typing.type_of env' sigma (EConstr.of_constr p)) in
         Some (sigma', p)
   with e when precatchable_exception e -> None
 
@@ -2041,7 +2041,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (EConstr.of_constr (lift (-(List.length realargs)) ty))
 	  with Not_found -> error_case_not_inductive env !evdref
-	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty}
+	    {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref (EConstr.of_constr ty)}
 	in
 	let (ind,u), params = dest_ind_family indf in
 	if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind;
@@ -2242,7 +2242,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon (EConstr.of_constr tycon)) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
+	 let _btype = evd_comb1 (Typing.type_of env) evdref (EConstr.of_constr bbody) in
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
 	 let branch =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0ea6758a70..04e235cc53 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -188,7 +188,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		  aux (hdy :: tele) (subst1 hdx restT) 
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	else Some (fun x -> 
-	  let term = co x in
+	  let term = EConstr.of_constr (co x) in
 	    Typing.e_solve_evars env evdref term)
       in
 	if isEvar c || isEvar c' || not (Program.is_program_generalized_coercion ()) then
@@ -297,16 +297,16 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		   let evm = !evdref in
 		     (try subco ()
 		      with NoSubtacCoercion ->
-			let typ = Typing.unsafe_type_of env evm c in
-			let typ' = Typing.unsafe_type_of env evm c' in
+			let typ = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
+			let typ' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
 			  coerce_application typ typ' c c' l l')
 		 else
 		   subco ()
 	   | x, y when Constr.equal c c' ->
 	       if Int.equal (Array.length l) (Array.length l') then
 		 let evm =  !evdref in
-		 let lam_type = Typing.unsafe_type_of env evm c in
-		 let lam_type' = Typing.unsafe_type_of env evm c' in
+		 let lam_type = Typing.unsafe_type_of env evm (EConstr.of_constr c) in
+		 let lam_type' = Typing.unsafe_type_of env evm (EConstr.of_constr c') in
 		   coerce_application lam_type lam_type' c c' l l'
 	       else subco ()
 	   | _ -> subco ())
@@ -337,7 +337,7 @@ let app_coercion env evdref coercion v =
   match coercion with
   | None -> v
   | Some f ->
-     let v' = Typing.e_solve_evars env evdref (f v) in
+     let v' = Typing.e_solve_evars env evdref (EConstr.of_constr (f v)) in
      whd_betaiota !evdref (EConstr.of_constr v')
 
 let coerce_itf loc env evd v t c1 =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 570f95324a..28ba60812b 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -507,7 +507,7 @@ let pretype_ref loc evdref env ref us =
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
-    let ty = Typing.unsafe_type_of env.ExtraEnv.env evd c in
+    let ty = Typing.unsafe_type_of env.ExtraEnv.env evd (EConstr.of_constr c) in
       make_judge c ty
 
 let judge_of_Type loc evd s =
@@ -644,7 +644,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
 	      uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
         ctxtv vdef in
-      Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj;
+      Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names (Array.map EConstr.of_constr ftys) vdefj;
       let ftys = Array.map (nf_evar !evdref) ftys in
       let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
       let fixj = match fixkind with
@@ -898,7 +898,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    let fj = pretype (mk_tycon (EConstr.of_constr fty)) env_f evdref lvar d in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p);
 		obj ind p cj.uj_val fj.uj_val
 	    in
 	      { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
@@ -917,7 +917,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	    let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 	    let v =
 	      let ind,_ = dest_ind_family indf in
-		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+		Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr p);
 		obj ind p cj.uj_val fj.uj_val
 	    in { uj_val = v; uj_type = ccl })
 
@@ -981,7 +981,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let ind,_ = dest_ind_family indf in
 	let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
 	let pred = nf_evar !evdref pred in
-	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
+	  Typing.check_allowed_sort env.ExtraEnv.env !evdref ind (EConstr.of_constr cj.uj_val) (EConstr.of_constr pred);
 	  mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
       let cj = { uj_val = v; uj_type = p } in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 290d77b1b3..a3983737d2 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1164,7 +1164,7 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
   let sigma = Sigma.to_evar_map sigma in
   let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (EConstr.Unsafe.to_constr c,sigma) in
   try
-    let _ = Typing.unsafe_type_of env sigma abstr_trm in
+    let _ = Typing.unsafe_type_of env sigma (EConstr.of_constr abstr_trm) in
     Sigma.Unsafe.of_pair (applist(abstr_trm, List.map snd loccs_trm), sigma)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 64264cf087..c948f9b9a7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -20,6 +20,11 @@ open Typeops
 open Arguments_renaming
 open Context.Rel.Declaration
 
+let push_rec_types pfix env =
+  let (i, c, t) = pfix in
+  let inj c = EConstr.Unsafe.to_constr c in
+  push_rec_types (i, Array.map inj c, Array.map inj t) env
+
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
@@ -28,12 +33,12 @@ let meta_type evd mv =
 
 let constant_type_knowing_parameters env cst jl =
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  type_of_constant_knowing_parameters_in env cst paramstyp
+  EConstr.of_constr (type_of_constant_knowing_parameters_in env cst paramstyp)
 
 let inductive_type_knowing_parameters env (ind,u) jl =
   let mspec = lookup_mind_specif env ind in
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
+  EConstr.of_constr (Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp)
 
 let e_type_judgment env evdref j =
   match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref (EConstr.of_constr j.uj_type))) with
@@ -44,7 +49,7 @@ let e_type_judgment env evdref j =
     | _ -> error_not_type env j
 
 let e_assumption_of_judgment env evdref j =
-  try (e_type_judgment env evdref j).utj_val
+  try EConstr.of_constr (e_type_judgment env evdref j).utj_val
   with TypeError _ ->
     error_assumption env j
 
@@ -84,27 +89,28 @@ let max_sort l =
   if Sorts.List.mem InSet l then InSet else InProp
 
 let e_is_correct_arity env evdref c pj ind specif params =
+  let open EConstr in
   let arsign = make_arity_signature env true (make_ind_family (ind,params)) in
   let allowed_sorts = elim_sorts specif in
   let error () = error_elim_arity env ind allowed_sorts c pj None in
   let rec srec env pt ar =
-    let pt' = whd_all env !evdref (EConstr.of_constr pt) in
-    match kind_of_term pt', ar with
+    let pt' = EConstr.of_constr (whd_all env !evdref pt) in
+    match EConstr.kind !evdref pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-        if not (Evarconv.e_cumul env evdref (EConstr.of_constr a1) (EConstr.of_constr a1')) then error ();
-        srec (push_rel (LocalAssum (na1,a1)) env) t ar'
+        if not (Evarconv.e_cumul env evdref a1 (EConstr.of_constr a1')) then error ();
+        srec (push_rel (LocalAssum (na1,EConstr.Unsafe.to_constr a1)) env) t ar'
     | Sort s, [] ->
         if not (Sorts.List.mem (Sorts.family s) allowed_sorts)
         then error ()
     | Evar (ev,_), [] ->
         let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
-        evdref := Evd.define ev (mkSort s) evd
+        evdref := Evd.define ev (Constr.mkSort s) evd
     | _, (LocalDef _ as d)::ar' ->
-        srec (push_rel d env) (lift 1 pt') ar'
+        srec (push_rel d env) (Vars.lift 1 pt') ar'
     | _ ->
         error ()
   in
-  srec env pj.uj_type (List.rev arsign)
+  srec env (EConstr.of_constr pj.uj_type) (List.rev arsign)
 
 let e_type_case_branches env evdref (ind,largs) pj c =
   let specif = lookup_mind_specif env (fst ind) in
@@ -128,24 +134,25 @@ let e_judge_of_case env evdref ci pj cj lfj =
     uj_type = rslty }
 
 let check_type_fixpoint loc env evdref lna lar vdefj =
+  let open EConstr in
   let lt = Array.length vdefj in
     if Int.equal (Array.length lar) lt then
       for i = 0 to lt-1 do
         if not (Evarconv.e_cumul env evdref (EConstr.of_constr (vdefj.(i)).uj_type)
-		  (EConstr.of_constr (lift lt lar.(i)))) then
+		  (Vars.lift lt lar.(i))) then
           Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
-            i lna vdefj lar
+            i lna vdefj (Array.map EConstr.Unsafe.to_constr lar)
       done
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
-  let pj = Retyping.get_judgment_of env sigma (EConstr.of_constr p) in
+  let pj = Retyping.get_judgment_of env sigma p in
   let ksort = family_of_sort (sort_of_arity env sigma (EConstr.of_constr pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
     let s = inductive_sort_family (snd specif) in
-    error_elim_arity env ind sorts c pj
+    error_elim_arity env ind sorts (EConstr.Unsafe.to_constr c) pj
       (Some(ksort,s,error_elim_explain ksort s))
 
 let e_judge_of_cast env evdref cj k tj =
@@ -160,21 +167,36 @@ let enrich_env env evdref =
   let penv' = Pre_env.({ penv with env_stratification =
     { penv.env_stratification with env_universes = Evd.universes !evdref } }) in
   Environ.env_of_pre_env penv'
+
+let check_fix env sigma pfix =
+  let inj c = EConstr.to_constr sigma c in
+  let (idx, (ids, cs, ts)) = pfix in
+  check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let check_cofix env sigma pcofix =
+  let inj c = EConstr.to_constr sigma c in
+  let (idx, (ids, cs, ts)) = pcofix in
+  check_cofix env (idx, (ids, Array.map inj cs, Array.map inj ts))
+
+let make_judge c ty =
+  make_judge (EConstr.Unsafe.to_constr c) (EConstr.Unsafe.to_constr ty)
 			  
 (* The typing machine with universes and existential variables. *)
 
 (* cstr must be in n.f. w.r.t. evars and execute returns a judgement
    where both the term and type are in n.f. *)
 let rec execute env evdref cstr =
-  match kind_of_term cstr with
+  let open EConstr in
+  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 = meta_type !evdref n }
+        { uj_val = EConstr.Unsafe.to_constr cstr; uj_type = meta_type !evdref n }
 
     | Evar ev ->
-	let ty = Evd.existential_type !evdref ev in
-	let jty = execute env evdref (whd_evar !evdref ty) in
+	let ty = EConstr.existential_type !evdref ev in
+	let jty = execute env evdref ty in
 	let jty = e_assumption_of_judgment env evdref jty in
-	{ uj_val = cstr; uj_type = jty }
+	{ uj_val = EConstr.Unsafe.to_constr cstr; uj_type = EConstr.Unsafe.to_constr jty }
 
     | Rel n ->
 	judge_of_relative env n
@@ -183,13 +205,13 @@ let rec execute env evdref cstr =
         judge_of_variable env id
 
     | Const c ->
-        make_judge cstr (rename_type_of_constant env c)
+        make_judge cstr (EConstr.of_constr (rename_type_of_constant env c))
 
     | Ind ind ->
-	make_judge cstr (rename_type_of_inductive env ind)
+	make_judge cstr (EConstr.of_constr (rename_type_of_inductive env ind))
 
     | Construct cstruct ->
-	make_judge cstr (rename_type_of_constructor env cstruct)
+	make_judge cstr (EConstr.of_constr (rename_type_of_constructor env cstruct))
 
     | Case (ci,p,c,lf) ->
         let cj = execute env evdref c in
@@ -200,13 +222,13 @@ let rec execute env evdref cstr =
     | Fix ((vn,i as vni),recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
-        check_fix env fix;
+        check_fix env !evdref fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
         let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
-        check_cofix env cofix;
+        check_cofix env !evdref cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->
@@ -222,7 +244,7 @@ let rec execute env evdref cstr =
     | App (f,args) ->
         let jl = execute_array env evdref args in
 	let j =
-	  match kind_of_term f with
+	  match EConstr.kind !evdref f with
 	    | Ind ind when Environ.template_polymorphic_pind ind env ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
@@ -273,7 +295,7 @@ and execute_recdef env evdref (names,lar,vdef) =
   let lara = Array.map (e_assumption_of_judgment env evdref) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
   let vdefj = execute_array env1 evdref vdef in
-  let vdefv = Array.map j_val vdefj in
+  let vdefv = Array.map (j_val %> EConstr.of_constr) vdefj in
   let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
   (names,lara,vdefv)
 
@@ -282,8 +304,8 @@ and execute_array env evdref = Array.map (execute env evdref)
 let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
-  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) (EConstr.of_constr t)) then
-    error_actual_type env j (nf_evar !evdref t)
+  if not (Evarconv.e_cumul env evdref (EConstr.of_constr j.uj_type) t) then
+    error_actual_type env j (EConstr.to_constr !evdref t)
 
 (* Type of a constr *)
 
@@ -328,4 +350,4 @@ let e_solve_evars env evdref c =
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref (EConstr.Unsafe.to_constr c)))
+let _ = Evarconv.set_solve_evars (fun env evdref c -> EConstr.of_constr (e_solve_evars env evdref c))
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 04e5e40bc2..3c1c4324dd 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -14,33 +14,33 @@ open Evd
     and universes. *)
 
 (** Typecheck a term and return its type. May trigger an evarmap leak. *)
-val unsafe_type_of : env -> evar_map -> constr -> types
+val unsafe_type_of : env -> evar_map -> EConstr.constr -> types
 
 (** Typecheck a term and return its type + updated evars, optionally refreshing
     universes *)
-val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
+val type_of : ?refresh:bool -> env -> evar_map -> EConstr.constr -> evar_map * types
 
 (** Variant of [type_of] using references instead of state-passing. *)
-val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
+val e_type_of : ?refresh:bool -> env -> evar_map ref -> EConstr.constr -> types
 
 (** Typecheck a type and return its sort *)
-val e_sort_of : env -> evar_map ref -> types -> sorts
+val e_sort_of : env -> evar_map ref -> EConstr.types -> sorts
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
-val e_check   : env -> evar_map ref -> constr -> types -> unit
+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
 
 (** Solve existential variables using typing *)
-val e_solve_evars : env -> evar_map ref -> constr -> constr
+val e_solve_evars : env -> evar_map ref -> EConstr.constr -> constr
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)
-val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
+val check_allowed_sort : env -> evar_map -> pinductive -> EConstr.constr -> EConstr.constr ->
   unit
 
 (** Raise an error message if bodies have types not unifiable with the
     expected ones *)
 val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
-  Names.Name.t array -> types array -> unsafe_judgment array -> unit
+  Names.Name.t array -> EConstr.types array -> unsafe_judgment array -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ac2f140519..f418dc6a94 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -102,7 +102,7 @@ let abstract_list_all env evd typ c l =
   let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in
   let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in
   let evd,typp =
-    try Typing.type_of env evd p
+    try Typing.type_of env evd (EConstr.of_constr p)
     with
     | UserError _ ->
         error_cannot_find_well_typed_abstraction env evd p (List.map EConstr.of_constr l) None
@@ -1214,7 +1214,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
       | _ -> error "Apply_Head_Then"
   in
-    apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
+    apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) (EConstr.of_constr c)) Sigma.refl evd
 
 let is_mimick_head ts f =
   match kind_of_term f with