Added a function in typing.ml to solve evars of a constr w/o going back down to rawconstr

Also cleaned a bit typing.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12902 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 102 insertions, 72 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 370904a68..b43e6e999 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -17,8 +17,6 @@ open Reduction
 open Reductionops
 open Termops
 open Environ
-open Typing
-open Classops
 open Recordops
 open Evarutil
 open Libnames
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index e847894a5..cea33c1e9 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -7,15 +7,15 @@ Inductiveops
 Retyping
 Cbv
 Pretype_errors
-Typing
 Evarutil
 Term_dnet
 Recordops
+Evarconv
+Typing
 Rawterm
 Pattern
 Matching
 Tacred
-Evarconv
 Typeclasses_errors
 Typeclasses
 Classops
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 13f2aef26..d94da115a 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -18,7 +18,6 @@ open Termops
 open Typeops
 open Libobject
 open Library
-open Classops
 open Mod_subst
 open Reductionops
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f4d032bf1..831787a06 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -35,54 +35,93 @@ let inductive_type_knowing_parameters env ind jl =
   let paramstyp = Array.map (fun j -> j.uj_type) jl in
   Inductive.type_of_inductive_knowing_parameters env mip paramstyp
 
+let e_judge_of_apply env evdref funj argjv =
+  let rec apply_rec n typ = function
+  | [] ->
+      { uj_val  = mkApp (j_val funj, Array.map j_val argjv);
+        uj_type = typ }
+  | hj::restjl ->
+      match kind_of_term (whd_betadeltaiota env !evdref typ) with
+      | Prod (_,c1,c2) ->
+	 if Evarconv.e_cumul env evdref hj.uj_type c1 then
+	   apply_rec (n+1) (subst1 hj.uj_val c2) restjl
+	 else
+	   error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv
+      | _ ->
+	  error_cant_apply_not_functional env funj argjv
+  in
+  apply_rec 1 funj.uj_type (Array.to_list argjv)
+
+let check_branch_types env evdref cj (lfj,explft) =
+  if Array.length lfj <> Array.length explft then
+    error_number_branches env cj (Array.length explft);
+  for i = 0 to Array.length explft - 1 do
+    if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then
+      error_ill_formed_branch env cj.uj_val i lfj.(i).uj_type explft.(i)
+  done
+
+let e_judge_of_case env evdref ci pj cj lfj =
+  let indspec =
+    try find_mrectype env !evdref cj.uj_type
+    with Not_found -> error_case_not_inductive env cj in
+  let _ = check_case_info env (fst indspec) ci in
+  let (bty,rslty,univ) = type_case_branches env indspec pj cj.uj_val in
+  check_branch_types env evdref cj (lfj,bty);
+  { uj_val  = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
+    uj_type = rslty }
+
+let e_judge_of_cast env evdref cj k tj =
+  let expected_type = tj.utj_val in
+  if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then
+    error_actual_type env cj expected_type;
+  { uj_val = mkCast (cj.uj_val, k, expected_type);
+    uj_type = expected_type }
+
 (* The typing machine without information, without universes but with
    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 evd cstr =
+let rec execute env evdref cstr =
   match kind_of_term cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = nf_evar evd (meta_type evd n) }
+        { uj_val = cstr; uj_type = meta_type !evdref n }
 
     | Evar ev ->
-        let sigma =  evd in
-	let ty = Evd.existential_type sigma ev in
-	let jty = execute env evd (nf_evar evd ty) in
+	let ty = Evd.existential_type !evdref ev in
+	let jty = execute env evdref (whd_evar !evdref ty) in
 	let jty = assumption_of_judgment env jty in
 	{ uj_val = cstr; uj_type = jty }
 
     | Rel n ->
-	j_nf_evar evd (judge_of_relative env n)
+	judge_of_relative env n
 
     | Var id ->
-        j_nf_evar evd (judge_of_variable env id)
+        judge_of_variable env id
 
     | Const c ->
-        make_judge cstr (nf_evar evd (type_of_constant env c))
+        make_judge cstr (type_of_constant env c)
 
     | Ind ind ->
-	make_judge cstr (nf_evar evd (type_of_inductive env ind))
+	make_judge cstr (type_of_inductive env ind)
 
     | Construct cstruct ->
-	make_judge cstr
-          (nf_evar evd (type_of_constructor env cstruct))
+	make_judge cstr (type_of_constructor env cstruct)
 
     | Case (ci,p,c,lf) ->
-        let cj = execute env evd c in
-        let pj = execute env evd p in
-        let lfj = execute_array env evd lf in
-        let (j,_) = judge_of_case env ci pj cj lfj in
-        j
+        let cj = execute env evdref c in
+        let pj = execute env evdref p in
+        let lfj = execute_array env evdref lf in
+        e_judge_of_case env evdref ci pj cj lfj
 
     | Fix ((vn,i as vni),recdef) ->
-        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
+        let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
 	let fix = (vni,recdef') in
         check_fix env fix;
 	make_judge (mkFix fix) tys.(i)
 
     | CoFix (i,recdef) ->
-        let (_,tys,_ as recdef') = execute_recdef env evd recdef in
+        let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
         let cofix = (i,recdef') in
         check_cofix env cofix;
 	make_judge (mkCoFix cofix) tys.(i)
@@ -94,96 +133,93 @@ let rec execute env evd cstr =
 	judge_of_type u
 
     | App (f,args) ->
-        let jl = execute_array env evd args in
+        let jl = execute_array env evdref args in
 	let j =
 	  match kind_of_term f with
 	    | Ind ind ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (inductive_type_knowing_parameters env ind
-		    (jv_nf_evar evd jl))
+		    (jv_nf_evar !evdref jl))
 	    | Const cst ->
 		(* Sort-polymorphism of inductive types *)
 		make_judge f
 		  (constant_type_knowing_parameters env cst
-		    (jv_nf_evar evd jl))
+		    (jv_nf_evar !evdref jl))
 	    | _ ->
-		execute env evd f
+		execute env evdref f
 	in
-	fst (judge_of_apply env j jl)
+	e_judge_of_apply env evdref j jl
 
     | Lambda (name,c1,c2) ->
-        let j = execute env evd c1 in
+        let j = execute env evdref c1 in
 	let var = type_judgment env j in
 	let env1 = push_rel (name,None,var.utj_val) env in
-        let j' = execute env1 evd c2 in
+        let j' = execute env1 evdref c2 in
         judge_of_abstraction env1 name var j'
 
     | Prod (name,c1,c2) ->
-        let j = execute env evd c1 in
+        let j = execute env evdref c1 in
         let varj = type_judgment env j in
 	let env1 = push_rel (name,None,varj.utj_val) env in
-        let j' = execute env1 evd c2 in
+        let j' = execute env1 evdref c2 in
         let varj' = type_judgment env1 j' in
 	judge_of_product env name varj varj'
 
      | LetIn (name,c1,c2,c3) ->
-        let j1 = execute env evd c1 in
-        let j2 = execute env evd c2 in
+        let j1 = execute env evdref c1 in
+        let j2 = execute env evdref c2 in
         let j2 = type_judgment env j2 in
         let _ =  judge_of_cast env j1 DEFAULTcast j2 in
         let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
-        let j3 = execute env1 evd c3 in
+        let j3 = execute env1 evdref c3 in
         judge_of_letin env name j1 j2 j3
 
     | Cast (c,k,t) ->
-        let cj = execute env evd c in
-        let tj = execute env evd t in
+        let cj = execute env evdref c in
+        let tj = execute env evdref t in
 	let tj = type_judgment env tj in
-        let j, _ = judge_of_cast env cj k tj in
-	j
+        e_judge_of_cast env evdref cj k tj
 
-and execute_recdef env evd (names,lar,vdef) =
-  let larj = execute_array env evd lar in
+and execute_recdef env evdref (names,lar,vdef) =
+  let larj = execute_array env evdref lar in
   let lara = Array.map (assumption_of_judgment env) larj in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let vdefj = execute_array env1 evd vdef in
+  let vdefj = execute_array env1 evdref vdef in
   let vdefv = Array.map j_val vdefj in
   let _ = type_fixpoint env1 names lara vdefj in
   (names,lara,vdefv)
 
-and execute_array env evd = Array.map (execute env evd)
+and execute_array env evdref = Array.map (execute env evdref)
 
-and execute_list env evd = List.map (execute env evd)
+and execute_list env evdref = List.map (execute env evdref)
 
-let mcheck env evd c t =
-  let sigma =  evd in
-  let j = execute env evd (nf_evar sigma c) in
-  if not (is_conv_leq env sigma j.uj_type t) then
-    error_actual_type env j (nf_evar sigma t)
+let check env evd c t =
+  let evdref = ref evd in
+  let j = execute env evdref c in
+  if not (Evarconv.e_cumul env evdref j.uj_type t) then
+    error_actual_type env j (nf_evar evd t)
 
 (* Type of a constr *)
 
-let mtype_of env evd c =
-  let j = execute env evd (nf_evar evd c) in
+let type_of env evd c =
+  let j = execute env (ref evd) c in
   (* We are outside the kernel: we take fresh universes *)
   (* to avoid tactics and co to refresh universes themselves *)
   Termops.refresh_universes j.uj_type
 
-let msort_of env evd c =
-  let j = execute env evd (nf_evar evd c) in
+(* Sort of a type *)
+
+let sort_of env evd c =
+  let j = execute env (ref evd) c in
   let a = type_judgment env j in
   a.utj_type
 
-let type_of env sigma c =
-  mtype_of env (Evd.create_evar_defs sigma) c
-let sort_of env sigma c =
-  msort_of env (Evd.create_evar_defs sigma) c
-let check env sigma c   =
-  mcheck env (Evd.create_evar_defs sigma) c
-
-(* The typed type of a judgment. *)
+(* Try to solve the existential variables by typing *)
 
-let mtype_of_type env evd constr =
-  let j = execute env evd (nf_evar evd constr) in
-  assumption_of_judgment env j
+let solve_evars env evd c =
+  let evdref = ref evd in
+  let c = (execute env evdref c).uj_val in
+  (* side-effect on evdref *)
+  nf_evar !evdref c
+  
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 9a40d01ec..e3b3e9482 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -21,14 +21,11 @@ open Evd
 val type_of : env -> evar_map -> constr -> types
 (* Typecheck a type and return its sort *)
 val sort_of : env -> evar_map -> types -> sorts
-(* Typecheck a term has a given type (assuming the type is OK *)
+(* Typecheck a term has a given type (assuming the type is OK) *)
 val check   : env -> evar_map -> constr -> types -> unit
 
-(* The same but with metas... *)
-val mtype_of : env -> evar_map -> constr -> types
-val msort_of : env -> evar_map -> types -> sorts
-val mcheck   : env -> evar_map -> constr -> types -> unit
+(* Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
-(* unused typing function... *)
-val mtype_of_type : env -> evar_map -> types -> types
+(* Solve existential variables using typing *)
+val solve_evars : env -> evar_map -> constr -> constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ea491b9da..648dcee0c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -61,7 +61,7 @@ let abstract_list_all env evd typ c l =
   let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
   let p = abstract_scheme env c l_with_all_occs ctxt in
   try
-    if is_conv_leq env evd (Typing.mtype_of env evd p) typ then p
+    if is_conv_leq env evd (Typing.type_of env evd p) typ then p
     else error "abstract_list_all"
   with UserError _ | Type_errors.TypeError _ ->
     error_cannot_find_well_typed_abstraction env evd p l