essai de typage des instantiations d\'evars

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

1 files changed, 28 insertions, 33 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 2f34957022..dd2d781d54 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -18,6 +18,7 @@ open Pretype_errors
 open Inductive
 open Inductiveops
 open Typeops
+open Evd
 
 let meta_type env mv =
   let ty =
@@ -31,44 +32,36 @@ let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
 (* The typing machine without information, without universes but with
    existential variables. *)
 
-let assumption_of_judgment env evd j =
-  assumption_of_judgment env (j_nf_evar (Evd.evars_of evd) j)
-
-let type_judgment env evd j =
-  type_judgment env (j_nf_evar (Evd.evars_of evd) j)
-
-let check_type env evd j ty =
-  let sigma = Evd.evars_of evd in
-  if not (is_conv_leq env sigma j.uj_type ty) then
-    error_actual_type env (j_nf_evar sigma j) (nf_evar sigma ty)
-
+(* 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 =
   match kind_of_term cstr with
     | Meta n ->
-        { uj_val = cstr; uj_type = meta_type evd n }
+        { uj_val = cstr; uj_type = nf_evar (evars_of evd) (meta_type evd n) }
 
     | Evar ev ->
         let sigma = Evd.evars_of evd in
 	let ty = Evd.existential_type sigma ev in
-	let jty = execute env evd ty in
-	let jty = assumption_of_judgment env evd jty in
+	let jty = execute env evd (nf_evar (evars_of evd) ty) in
+	let jty = assumption_of_judgment env jty in
 	{ uj_val = cstr; uj_type = jty }
 	
     | Rel n -> 
-	judge_of_relative env n
+	j_nf_evar (evars_of evd) (judge_of_relative env n)
 
     | Var id -> 
-        judge_of_variable env id
+        j_nf_evar (evars_of evd) (judge_of_variable env id)
 	  
     | Const c ->
-        make_judge cstr (constant_type env c)
+        make_judge cstr (nf_evar (evars_of evd) (constant_type env c))
 	  
     | Ind ind ->
-	make_judge cstr (type_of_inductive env ind)
+	make_judge cstr (nf_evar (evars_of evd) (type_of_inductive env ind))
 	  
     | Construct cstruct -> 
-	make_judge cstr (type_of_constructor env cstruct)
-	  
+	make_judge cstr
+          (nf_evar (evars_of evd) (type_of_constructor env cstruct))
+
     | Case (ci,p,c,lf) ->
         let cj = execute env evd c in
         let pj = execute env evd p in
@@ -102,23 +95,23 @@ let rec execute env evd cstr =
 	    
     | Lambda (name,c1,c2) -> 
         let j = execute env evd c1 in
-	let var = type_judgment env evd j 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 
         judge_of_abstraction env1 name var j'
 	  
     | Prod (name,c1,c2) ->
         let j = execute env evd c1 in
-        let varj = type_judgment env evd j 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 varj' = type_judgment env1 evd j' 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 j2 = type_judgment env evd j2 in
+        let j2 = type_judgment env j2 in
         let _ =  judge_of_cast env j1 j2 in
         let env1 = push_rel (name,Some j1.uj_val,j2.utj_val) env in
         let j3 = execute env1 evd c3 in
@@ -127,13 +120,13 @@ let rec execute env evd cstr =
     | Cast (c,t) ->
         let cj = execute env evd c in
         let tj = execute env evd t in
-	let tj = type_judgment env evd tj in
+	let tj = type_judgment env tj in
         let j, _ = judge_of_cast env cj tj in
 	j
 
 and execute_recdef env evd (names,lar,vdef) =
   let larj = execute_array env evd lar in
-  let lara = Array.map (assumption_of_judgment env evd) larj 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 vdefv = Array.map j_val vdefj in
@@ -153,19 +146,21 @@ and execute_list env evd = function
       j::jr
 
 let mcheck env evd c t =
-  let j = execute env evd c in
-  check_type env evd j t
+  let sigma = Evd.evars_of 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)
 
 (* Type of a constr *)
  
 let mtype_of env evd c =
-  let j = execute env evd c in
+  let j = execute env evd (nf_evar (evars_of evd) c) in
   (* No normalization: it breaks Pattern! *)
   (*nf_betaiota*) (body_of_type j.uj_type)
 
 let msort_of env evd c =
-  let j = execute env evd c in
-  let a = type_judgment env evd j in
+  let j = execute env evd (nf_evar (evars_of evd) c) in
+  let a = type_judgment env j in
   a.utj_type
 
 let type_of env sigma c =
@@ -178,5 +173,5 @@ let check env sigma c   =
 (* The typed type of a judgment. *)
 
 let mtype_of_type env evd constr =
-  let j = execute env evd constr in
-  assumption_of_judgment env evd j
+  let j = execute env evd (nf_evar (evars_of evd) constr) in
+  assumption_of_judgment env j