- Typing -> Safe_typing

 - proofs/Typing_ev -> pretyping/Typing
 - env -> sign
 - fonctions var_context


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

1 files changed, 155 insertions, 0 deletions

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
new file mode 100644
index 000000000..c12f9bb34
--- /dev/null
+++ b/pretyping/typing.ml
@@ -0,0 +1,155 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+open Environ
+open Reduction
+open Type_errors
+open Typeops
+
+let vect_lift = Array.mapi lift
+let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+
+type 'a mach_flags = {
+  fix : bool;
+  nocheck : bool }
+
+(* The typing machine without information, without universes but with
+   existential variables. *)
+
+let rec execute mf env sigma cstr =
+  match kind_of_term cstr with
+    | IsMeta n ->
+	error "execute: found a non-instanciated goal"
+
+    | IsEvar _ ->
+	let ty = type_of_existential env sigma cstr in
+	let jty = execute mf env sigma ty in
+	{ uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type }
+	
+    | IsRel n -> 
+	relative env n
+
+    | IsVar id -> 
+	make_judge cstr (snd (lookup_var id env))
+	  
+    | IsAbst _ ->
+        if evaluable_abst env cstr then 
+	  execute mf env sigma (abst_value env cstr)
+        else 
+	  error "Cannot typecheck an unevaluable abstraction"
+	      
+    | IsConst _ ->
+        make_judge cstr (type_of_constant env sigma cstr)
+	  
+    | IsMutInd _ ->
+	make_judge cstr (type_of_inductive env sigma cstr)
+	  
+    | IsMutConstruct _ -> 
+	let (typ,kind) = destCast (type_of_constructor env sigma cstr) in
+        { uj_val = cstr; uj_type = typ; uj_kind = kind }
+	  
+    | IsMutCase (_,p,c,lf) ->
+        let cj = execute mf env sigma c in
+        let pj = execute mf env sigma p in
+        let lfj = execute_array mf env sigma lf in
+        type_of_case env sigma pj cj lfj
+  
+    | IsFix (vn,i,lar,lfi,vdef) ->
+        if (not mf.fix) && array_exists (fun n -> n < 0) vn then
+          error "General Fixpoints not allowed";
+        let larv,vdefv = execute_fix mf env sigma lar lfi vdef in
+        let fix = mkFix vn i larv lfi vdefv in
+        check_fix env sigma fix;
+	make_judge fix larv.(i)
+	  
+    | IsCoFix (i,lar,lfi,vdef) ->
+        let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in
+        let cofix = mkCoFix i larv lfi vdefv in
+        check_cofix env sigma cofix;
+	make_judge cofix larv.(i)
+	  
+    | IsSort (Prop c) -> 
+	make_judge_of_prop_contents c
+
+    | IsSort (Type u) ->
+	let (j,_) = make_judge_of_type u in j
+	  
+    | IsAppL (f,args) ->
+	let j = execute mf env sigma f in
+        let jl = execute_list mf env sigma args in
+	let (j,_) = apply_rel_list env sigma mf.nocheck jl j in
+	j
+	    
+    | IsLambda (name,c1,c2) -> 
+        let j = execute mf env sigma c1 in
+        let var = assumption_of_judgment env sigma j in
+	let env1 = push_rel (name,var) env in
+        let j' = execute mf env1 sigma c2 in 
+        let (j,_) = abs_rel env1 sigma name var j' in
+	j
+	  
+    | IsProd (name,c1,c2) ->
+        let j = execute mf env sigma c1 in
+        let var = assumption_of_judgment env sigma j in
+	let env1 = push_rel (name,var) env in
+        let j' = execute mf env1 sigma c2 in
+	let (j,_) = gen_rel env1 sigma name var j' in
+	j
+	  
+    | IsCast (c,t) ->
+        let cj = execute mf env sigma c in
+        let tj = execute mf env sigma t in
+        cast_rel env sigma cj tj
+	  
+      | _ -> error_cant_execute CCI env cstr
+	  
+and execute_fix mf env sigma lar lfi vdef =
+  let larj = execute_array mf env sigma lar in
+  let lara = Array.map (assumption_of_judgment env sigma) larj in
+  let nlara = 
+    List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in
+  let env1 = 
+    List.fold_left (fun env nvar -> push_rel nvar env) env nlara in
+  let vdefj = execute_array mf env1 sigma vdef in
+  let vdefv = Array.map j_val_only vdefj in
+  let cst3 = type_fixpoint env1 sigma lfi lara vdefj in
+  (lara,vdefv)
+
+and execute_array mf env sigma v =
+  let jl = execute_list mf env sigma (Array.to_list v) in
+  Array.of_list jl
+
+and execute_list mf env sigma = function
+  | [] -> 
+      []
+  | c::r -> 
+      let j = execute mf env sigma c in 
+      let jr = execute_list mf env sigma r in
+      j::jr
+
+
+let safe_machine env sigma constr = 
+  let mf = { fix = false; nocheck = false } in
+  execute mf env sigma constr
+
+
+(* Type of a constr *)
+
+let type_of env sigma c = 
+  let j = safe_machine env sigma c in 
+  nf_betaiota env sigma j.uj_type
+
+(* The typed type of a judgment. *)
+
+let execute_type env sigma constr = 
+  let j = execute { fix=false; nocheck=true } env sigma constr in
+  assumption_of_judgment env sigma j
+
+let execute_rec_type env sigma constr = 
+  let j = execute { fix=false; nocheck=false } env sigma constr in
+  assumption_of_judgment env sigma j
+