environnement sur

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

1 files changed, 92 insertions, 366 deletions

diff --git a/kernel/typing.ml b/kernel/typing.ml
index 2311fb9992..ebae3faf93 100644
--- a/kernel/typing.ml
+++ b/kernel/typing.ml
@@ -9,9 +9,11 @@ open Generic
 open Term
 open Reduction
 open Sign
+open Constant
+open Inductive
 open Environ
 open Type_errors
-open Machops
+open Typeops
 
 (* Fonctions temporaires pour relier la forme castée de la forme jugement *)
 
@@ -230,371 +232,95 @@ let unsafe_type_of_type env c =
   let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ)
 
 
+(*s Safe environments. *)
+
+type 'a environment = 'a unsafe_env
+
+let evar_map = evar_map
+let universes = universes
+let metamap = metamap
+let context = context
+
+let lookup_var = lookup_var
+let lookup_rel = lookup_rel
+let lookup_constant = lookup_constant
+let lookup_mind = lookup_mind
+let lookup_mind_specif = lookup_mind_specif
+let lookup_meta = lookup_meta
+
+let push_rel_or_var push (id,ty) env =
+  let (j,u) = safe_machine env ty.body in
+  let env' = set_universes u env in
+  let expty = DOP0(Sort ty.typ) in
+  match conv env' j.uj_type expty with
+    | Convertible u' -> push (id,ty) (set_universes u' env')
+    | NotConvertible -> error_actual_type CCI env ty.body j.uj_type expty
+
+let push_var nvar env = push_rel_or_var push_var nvar env
+
+let push_rel nrel env = push_rel_or_var push_rel nrel env
+
+let add_constant sp ce env =
+  let (jb,u) = safe_machine env ce.const_entry_body in
+  let env' = set_universes u env in
+  let (jt,u') = safe_machine env ce.const_entry_type in
+  let env'' = set_universes u' env' in
+  match conv env'' jb.uj_type jt.uj_val with
+    | Convertible u'' -> 
+	let cb = { 
+	  const_kind = kind_of_path sp;
+	  const_body = Some (ref (Cooked ce.const_entry_body));
+	  const_type = typed_type_of_judgment env'' jt;
+	  const_hyps = get_globals (context env);
+	  const_opaque = false;
+	  const_eval = None } 
+	in
+	add_constant sp cb (set_universes u'' env'')
+    | NotConvertible -> 
+	error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val
+
+let type_from_judgment env j =
+  match whd_betadeltaiota env j.uj_kind with
+    | DOP0(Sort s) -> { body = j.uj_type; typ = s }
+    | _ -> error_not_type CCI env j.uj_type (* shouldn't happen *)
+
+let add_parameter sp c env =
+  let (j,u) = safe_machine env c in
+  let env' = set_universes u env in
+  let cb = {
+    const_kind = kind_of_path sp;
+    const_body = Some (ref (Cooked c));
+    const_type = type_from_judgment env' j;
+    const_hyps = get_globals (context env);
+    const_opaque = false;
+    const_eval = None } 
+  in
+  Environ.add_constant sp cb env'
+
+let add_mind sp me env =
+  let name_params = 
+    List.map (fun (id,c) -> (Name id, c)) me.mind_entry_params in
+  (* just to check the params *)
+  let env_params =
+    List.fold_left 
+      (fun env (id,c) ->
+	 let (j,u) = safe_machine env c in
+	 let env' = set_universes u env in
+	 Environ.push_var (id, assumption_of_judgement env' j) env')
+      env me.mind_entry_params
+  in
+  let env_arities =
+    List.fold_left 
+      (fun env (id,ar,_) -> 
+	 let (j,u) = safe_machine env (prod_it ar name_params) in
+	 let env' = set_universes u env in
+	 Environ.push_var (id, assumption_of_judgement env' j) env')
+      env me.mind_entry_inds
+  in
+  env_arities
+
+type judgment = unsafe_judgment
+
 (*s Machines with information. *)
 
 type information = Logic | Inf of unsafe_judgment
-
-(*i
-let implicit_judgment = {body=mkImplicit;typ=implicit_sort}
-
-let add_inf_rel (na,inf) env =
-  match inf with
-      Logic -> add_rel (na,implicit_judgment) env
-    | Inf j -> add_rel (na,tjudge_of_judge j) env
-
-
-let fw_mutind sigma fenv k =
-  let (sp,x,args) = destMutInd k in
-  let mis = mind_specif_of_mind k in
-    match mis_singl mis with 
-	Some a -> Some (a,true)
-      | None ->
-	  if is_info_cast_type sigma (mis_arity mis) then
-	    let infK =
-              global_reference fenv (fwsp_of sp) (id_of_global (MutInd (sp,x)))
-	    in Some (infK,false)
-	  else None
-
-let inf_of_mind sigma fenv mind = 
-  try
-    match fw_mutind sigma fenv mind with
-        Some (infK,singl) -> Inf(cast_fmachine (sigma,[]) fenv infK)
-      | None -> Logic
-  with
-      Not_found | Failure _ -> 
-	anomaly "cannot convert an inductive to an finductive"
-
-let inf_mconstructor (sigma,metamap) fenv k = 
-  let (sp,x,i,cl) = destMutConstruct k in
-  let mind = mkMutInd sp x cl in 
-    (match fw_mutind sigma fenv mind with
-         None -> Logic
-       | Some(infi,singl) ->
-	   (match mind_lamexp mind with
-	      | Some clamexp ->
-		  if singl
-		  then Inf(cast_fmachine (sigma,[]) fenv clamexp)
-		  else
-		    let (infsp, infx, infcl) = destMutInd infi in
-		    let infmconstructor = mkMutConstruct infsp infx i infcl in
-		    let infval = subst1 infmconstructor clamexp in
-		      Inf (cast_fmachine (sigma,fst metamap) fenv infval)
-	      | _ -> assert false))
-
-
-exception DefinedExtraction
-
-(* when c is an evaluable constant with an extraction which 
-   contains an implicit, gives the value of the c constant
-   otherwise raise DefinedExtraction
-*)
-
-let value_implicit_const sigma c cinf = 
-  match c with DOPN(Const(_),_) -> 
-    if evaluable_const sigma c then 
-      let cv = const_value sigma cinf in 
-	if is_implicit cv (* or contains_implicit sigma cv *)
-	then const_value sigma c 
-	else raise DefinedExtraction
-    else raise DefinedExtraction
-    | _ -> raise DefinedExtraction
-
-let unsafe_infmachine (sigma,metamap) env fenv c = 
-  let rec infexec env fenv cstr = match cstr with
-       DOP2(Cast,c,DOP0(Sort(Prop(Null)))) -> Logic
-    |  DOP2(Cast,c,DOP2(Cast,_,DOP0(Sort(Prop(Null))))) -> Logic
-    |  DOP2(Cast,c,_) -> infexec env fenv c
-    |  DOP0(Meta n) ->
-         (match List.assoc n (snd metamap) with
-             Logic -> Logic
-           | Inf j -> Inf{uj_val=DOP0(Meta n);
-                          uj_type=j.uj_val;
-                          uj_kind = hnf_constr sigma j.uj_type})
-
-    | Rel n ->
-        inf_rel fenv
-          (contents_of_type sigma (snd (lookup_rel n env))) n
-
-    | VAR str ->
-        inf_var fenv
-          (contents_of_type sigma (snd(lookup_glob str env))) str
-
-    | DOPN(Const _,_) -> inf_of_const sigma (env,fenv) cstr
-
-    | DOPN(Abst _,_) ->
-        if evaluable_abst cstr then infexec env fenv (abst_value cstr)
-        else error "cannot extract from an unevaluable abstraction"
-
-    | DOP0(Sort s) -> inf_sort s
-
-    | DOPN(AppL,tl) ->
-        let c1 =  (hd_vect tl)
-        and cl = tl_vect tl in
-          let funinf = infexec env fenv c1 in
-            (match funinf with Logic -> Logic
-	      | Inf(j) -> let cinf = j.uj_val in
-             (* try to expand constants corresponding 
-		    to non extractable terms *)
-	      (try if is_extraction_expanded() then 
-		 let valcte = value_implicit_const sigma c1 cinf 
-		 in infexec env fenv (whd_betaiota (appvect(valcte,cl))) 
-	       else raise DefinedExtraction
-               with DefinedExtraction -> 
-		 let argsinf = Array.map (infexec env fenv) cl
-		 in it_vect inf_apply funinf argsinf))
-
-    | DOP2(Lambda,c1,DLAM(name,c2)) ->
-        let varinf = infexec env fenv c1 in
-        let bodyinf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
-                        (add_inf_rel (name,varinf) fenv) c2
-        in inf_abs_rel name bodyinf varinf
-
-    | DOP2(Prod,c1,DLAM(name,c2)) ->
-        let c1inf = infexec env fenv c1 in
-        let c2inf = infexec (add_rel (name,tjudge_of_cast sigma c1) env)
-                      (add_inf_rel (name,c1inf) fenv) c2
-        in inf_gen_rel name c2inf c1inf
-
-    | DOPN(MutInd _,_) -> inf_of_mind sigma fenv cstr
-
-    | DOPN(MutConstruct _,_) ->
-        inf_mconstructor (sigma,metamap) fenv cstr
-
-    | DOPN(Fix(vn,i),cl) ->
-        let lar = Array.sub cl 0 ((Array.length cl) - 1) in
-        let inflar = Array.map (infexec env fenv) lar in
-        let infAi = inflar.(i) in 
-          (match infAi with 
-              Logic   -> Logic 
-            | Inf aij ->
-                let (lfi,ldefs) = decomp_all_DLAMV_name (last_vect cl) in
-                let (new_env,new_fenv) =
-                  it_vect2
-                    (fun (ne,nfe) fk ak -> 
-                       (add_rel (fk,tjudge_of_cast sigma ak) ne,
-                        let infAk = infexec ne nfe ak
-                        in (add_inf_rel (fk,infAk) nfe)))
-                    (env,fenv)
-                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
-(* a special function to localize the recursive index in the extracted term *)
-                let rec exec_def ne nfe n def = 
-                  (match hnf_constr sigma def with 
-                      DOP2(Lambda,c1,DLAM(name,c2)) ->
-                        let varinf = infexec ne nfe c1 in
-                        let ne' = (add_rel (name,tjudge_of_cast sigma c1) ne) 
-                        and nfe' = add_inf_rel (name,varinf) nfe in
-                          if n = 0 then
-                            let infc2 = infexec ne' nfe' c2 
-                            in let infdef = inf_abs_rel name infc2 varinf
-                               and index =
-                                 if varinf = Logic then -1
-                        (* the recursive call was on a non-informative term *) 
-                                 else 0 in (infdef,index)
-                          else
-                            let bodyinf,countl = 
-                              exec_def (add_rel (name,tjudge_of_cast sigma c1) ne) 
-                                (add_inf_rel (name,varinf) nfe) (n-1) c2 in
-                            let (infabs,abs) =
-                              inf_abs_rel_count name bodyinf varinf
-                            in (infabs,
-                                if abs = ERASE then countl
-                                else if countl<0 then countl-1
-                                else countl+1)
-                    | _ -> anomaly "exec_def : should be a lambda") in
-                let infdefs_ind =
-                  map2_vect (exec_def new_env new_fenv) vn ldefs
-                in inf_fix sigma i aij.uj_type lfi inflar infdefs_ind)
-
-    | DOPN(CoFix i,cl) ->
-        let lar    = Array.sub cl 0 ((Array.length cl) - 1) in 
-        let inflar = Array.map (infexec env fenv) lar in
-        let infAi  = inflar.(i) in
-          (match infAi with 
-              Logic   -> Logic 
-            | Inf aij -> 
-                let lfi,ldefs = decomp_all_DLAMV_name (last_vect cl) in 
-                let (new_env,new_fenv) = 
-                  it_vect2 (fun (ne,nfe) fk ak -> 
-                              (add_rel (fk,tjudge_of_cast sigma ak) ne, 
-                               let infAk = infexec ne nfe ak
-                               in (add_inf_rel (fk,infAk) nfe)))
-                    (env,fenv) 
-                    (Array.of_list (List.rev lfi)) (vect_lift lar) in 
-                                   
-                let infdefs = Array.map (infexec new_env new_fenv) ldefs 
-                in  inf_cofix sigma i aij.uj_type lfi inflar infdefs)
-
-    | DOPN(MutCase _,_) ->
-        let (ci,p,c,lf) = destCase cstr in
-        let pinf = infexec env fenv p in 
-          (match pinf with
-              Logic  -> Logic 
-            | Inf pj -> 
-		if is_extraction_expanded() then 
-		  let (d,l) = whd_betadeltaiota_stack sigma c [] in 
-                 (match d with (DOPN(MutConstruct(_,_),_)) ->
-		    let cstr' = 
-		      DOPN(MutCase(ci),Array.append [|p;applist(d,l)|] lf)
-		    in infexec env fenv (whd_betaiota cstr')
-		    | _ -> 
-                  let cinf = infexec env fenv c
-                  and lfinf = Array.map (infexec env fenv) lf
-                  in inf_mutcase fenv sigma pj ci cinf lfinf
-		 )
-               else let cinf = infexec env fenv c
-                  and lfinf = Array.map (infexec env fenv) lf
-                  in inf_mutcase fenv sigma pj ci cinf lfinf)
-	 
-    | _ -> error "Cannot extract information"
-  in infexec env fenv c
-
-
-let core_infmachine meta env fenv c =
-  try unsafe_infmachine meta env fenv c
-  with (UserError _ | Failure _) -> Logic
-
-(* WITH INFORMATION *)
-(* does not check anymore that extracted terms are well-formed *)
-let judgement_infmachine meta env fenv c ct = 
-  try
-    match unsafe_infmachine meta env fenv c with
-        Inf infj ->
-          let inftyp =
-            try unsafe_infmachine meta env fenv ct
-            with (UserError _ | Failure _) ->
-              (warning "Failed to extract in type"; Logic)
-          in (match inftyp with
-                  Inf infjt ->
-                    Inf{uj_val=infj.uj_val;
-                        uj_type=infjt.uj_val;
-                        uj_kind=infj.uj_kind}
-                | Logic -> Inf infj)
-      | Logic -> Logic
-  with (UserError _ | Failure _) -> (warning "Failed to extract"; Logic)
-
-let infmachine_type nocheck (sigma,metamap) env fenv constr =
-  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
-  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
-  let t = core_fmachine_type nocheck (sigma,constr_metamap) env constr in
-  let inf = 
-    if is_info_type sigma t then (* Case the term is informative *)
-      let uniarc = get_uniarc () in
-      let infjt =
-        judgement_infmachine
-          (sigma,(constr_metamap,inf_metamap)) env fenv 
-	  t.body 
-	  (DOP0 (Sort t.typ)) in
-      let _ = set_uniarc uniarc in
-        infjt
-    else Logic
-
-  in hash_jpair_type
-       ({body = strip_all_casts t.body; typ = t.typ},
-        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
-                            uj_type = nf_beta j.uj_type;
-                            uj_kind = j.uj_kind }) inf))
-
-let infmachine nocheck (sigma,metamap) env fenv constr =
-  let constr_metamap = List.map (fun (id,(c,_)) -> (id,c)) metamap in
-  let inf_metamap = List.map (fun (id,(_,i)) -> (id,i)) metamap in
-  let j = core_fmachine nocheck (sigma,constr_metamap) env constr in
-  let inf = 
-    if is_info_judge sigma j then (* Case the term is informative *)
-      let uniarc = get_uniarc () in
-      let jt = cast_fmachine (sigma,constr_metamap) env j.uj_type in
-      let infjt =
-        judgement_infmachine
-          (sigma,(constr_metamap,inf_metamap)) env fenv j.uj_val jt.uj_val in
-      let _ = set_uniarc uniarc in
-        infjt
-    else Logic
-
-  in hash_jpair
-       ({uj_val = strip_all_casts j.uj_val;
-         uj_type = strip_all_casts j.uj_type;
-         uj_kind = j.uj_kind},
-        (inf_app (fun j -> {uj_val = nf_beta j.uj_val;
-                            uj_type = nf_beta j.uj_type;
-                            uj_kind = j.uj_kind }) inf))
-
-
-let jsign_of_sign sigma sign =
-  sign_it
-    (fun id a (sign,fsign) ->
-      let sign' = add_sign (id,a) sign in
-      let fsign' =
-        match infmachine_type true (sigma,[]) (gLOB sign) (gLOB fsign) a.body
- 	with
-          (_,Logic) -> fsign
-        | (_,Inf ft) -> add_sign (id,tjudge_of_judge ft) fsign
-      in (sign',fsign'))
-    sign (([],[]),([],[]))
-
-
-let fsign_of_sign sigma sign = snd (jsign_of_sign sigma sign)
-
-let infexemeta_type sigma metamap (env,fenv) c =
-  infmachine_type true (sigma,metamap) env fenv c
-
-let infexecute_rec_type sigma (env,fenv) c =
-  infmachine_type false (sigma,[]) env fenv c
-
-let infexecute_type sigma (sign,fsign) c =
-  infmachine_type false (sigma,[]) (gLOB sign) (gLOB fsign) c
-
-let infexemeta sigma metamap (env,fenv) c =
-  infmachine true (sigma,metamap) env fenv c
-
-let infexecute_rec sigma (env,fenv) c =
-  infmachine false (sigma,[]) env fenv c
-
-let infexecute sigma (sign,fsign) c =
-  infmachine false (sigma,[]) (gLOB sign) (gLOB fsign) c
-
-(* A adapter pour les nouveaux env
-let fvar_type sigma (sign,fsign) v = 
-  let na = destVar v in
-  let varty = (snd(lookup_sign na sign))
-  in match (snd(infexemeta sigma [] (gLOB sign, gLOB fsign) varty)) with
-      Inf ft -> ft.uj_val
-    | Logic -> invalid_arg "Fvar with a non-informative type (1)!"
-
-*)
-
-(* MACHINE WITH UNIVERSES *)
-(* Il vaudrait mieux typer dans le graphe d'univers de Constraintab,
-   recuperer le graphe local, et restaurer l'acien graphe global *)
-
-let whd_instuni = function
-    DOP0(Sort(Type(u))) ->
-      let u = (if u = dummy_univ then new_univ() else u)
-      in DOP0(Sort(Type(u)))
-  | c -> c
-
-(* Instantiate universes: replace all dummy_univ by fresh universes.
-   This is already done by the machine.
-   Indtypes instantiates the universes itself, because in the case of
-   large constructor, additionnal constraints must be considered. *)
-let instantiate_universes c = strong whd_instuni c
-
-
-(* sp est le nom de la constante pour laquelle il faut que c soit bien type.
-   Cela sert a eviter un clash entre le noms d'univers de 2 modules compiles
-   independamment.
-   Au lieu de sp, Lib.cwd() serait peut-etre suffisant.
-   Cela eviterai de donner un section-path quand on veut typer. *)
-let fexecute_type_with_univ sigma sign sp c =
-  with_universes (fexecute_type sigma sign) (sp,initial_universes,c) 
-
-
-let fexecute_with_univ sigma sign sp c =
-  with_universes (fexecute sigma sign) (sp,initial_universes,c) 
-
-
-let infexecute_type_with_univ sigma psign sp c =
-  with_universes (infexecute_type sigma psign) (sp,initial_universes,c) 
-
-
-let infexecute_with_univ sigma psign sp c =
-  with_universes (infexecute sigma psign) (sp,initial_universes,c) 
-i*)