mise au point Declare et avancee dans Astterm

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

8 files changed, 96 insertions, 47 deletions

diff --git a/.depend b/.depend
index 72955e7971..654c9c5f2e 100644
--- a/.depend
+++ b/.depend
@@ -18,6 +18,7 @@ kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.cmi \
 kernel/names.cmi: lib/pp.cmi 
 kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi 
+kernel/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 kernel/safe_typing.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi 
@@ -88,7 +89,6 @@ pretyping/rawterm.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \
 pretyping/recordops.cmi: pretyping/classops.cmi kernel/generic.cmi \
     library/libobject.cmi library/library.cmi kernel/names.cmi \
     kernel/term.cmi 
-pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi 
 proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \
     kernel/term.cmi lib/util.cmi 
@@ -288,6 +288,8 @@ library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \
     kernel/names.cmx library/nametab.cmx kernel/reduction.cmx kernel/sign.cmx \
     library/summary.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     library/declare.cmi 
+library/discharge.cmo: library/declare.cmi library/discharge.cmi 
+library/discharge.cmx: library/declare.cmx library/discharge.cmi 
 library/global.cmo: kernel/environ.cmi kernel/generic.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \
     kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
@@ -351,15 +353,17 @@ parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
     kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx lib/util.cmx parsing/ast.cmi 
 parsing/astterm.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
-    library/impargs.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
-    pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/sign.cmi \
-    kernel/term.cmi lib/util.cmi toplevel/vernac.cmi parsing/astterm.cmi 
+    kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+    kernel/generic.cmi library/global.cmi library/impargs.cmi \
+    kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi pretyping/pretyping.cmi \
+    pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi toplevel/vernac.cmi parsing/astterm.cmi 
 parsing/astterm.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \
-    library/impargs.cmx kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx \
-    pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/sign.cmx \
-    kernel/term.cmx lib/util.cmx toplevel/vernac.cmx parsing/astterm.cmi 
+    kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \
+    kernel/generic.cmx library/global.cmx library/impargs.cmx \
+    kernel/names.cmx parsing/pcoq.cmi lib/pp.cmx pretyping/pretyping.cmx \
+    pretyping/rawterm.cmi kernel/sign.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx toplevel/vernac.cmx parsing/astterm.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi 
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/esyntax.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
@@ -412,12 +416,12 @@ pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \
     proofs/tacred.cmx kernel/term.cmx lib/util.cmx pretyping/classops.cmi 
 pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \
     pretyping/evarconv.cmi kernel/evd.cmi kernel/generic.cmi kernel/names.cmi \
-    pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+    pretyping/recordops.cmi kernel/reduction.cmi kernel/retyping.cmi \
     kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \
     pretyping/coercion.cmi 
 pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
     pretyping/evarconv.cmx kernel/evd.cmx kernel/generic.cmx kernel/names.cmx \
-    pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmi \
+    pretyping/recordops.cmx kernel/reduction.cmx kernel/retyping.cmi \
     kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
     pretyping/coercion.cmi 
 pretyping/evarconv.cmo: pretyping/classops.cmi kernel/environ.cmi \
@@ -448,7 +452,7 @@ pretyping/pretyping.cmo: parsing/ast.cmi pretyping/classops.cmi \
     library/indrec.cmi kernel/inductive.cmi kernel/instantiate.cmi \
     pretyping/multcase.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/pretype_errors.cmi pretyping/rawterm.cmi \
-    pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \
+    pretyping/recordops.cmi kernel/reduction.cmi kernel/retyping.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi \
     lib/util.cmi pretyping/pretyping.cmi 
 pretyping/pretyping.cmx: parsing/ast.cmx pretyping/classops.cmx \
@@ -457,7 +461,7 @@ pretyping/pretyping.cmx: parsing/ast.cmx pretyping/classops.cmx \
     library/indrec.cmx kernel/inductive.cmx kernel/instantiate.cmx \
     pretyping/multcase.cmi kernel/names.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx pretyping/rawterm.cmi \
-    pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmi \
+    pretyping/recordops.cmx kernel/reduction.cmx kernel/retyping.cmi \
     kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx \
     lib/util.cmx pretyping/pretyping.cmi 
 pretyping/recordops.cmo: pretyping/classops.cmi library/lib.cmi \
@@ -509,15 +513,13 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \
     parsing/pcoq.cmi lib/pp.cmx proofs/proof_trees.cmx library/summary.cmx \
     kernel/term.cmx lib/util.cmx proofs/macros.cmi 
 proofs/pfedit.cmo: kernel/constant.cmi library/declare.cmi lib/edit.cmi \
-    kernel/evd.cmi kernel/generic.cmi library/global.cmi library/library.cmi \
+    kernel/evd.cmi kernel/generic.cmi library/global.cmi library/lib.cmi \
     kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \
-    library/states.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \
-    proofs/pfedit.cmi 
+    proofs/tacmach.cmi kernel/term.cmi lib/util.cmi proofs/pfedit.cmi 
 proofs/pfedit.cmx: kernel/constant.cmx library/declare.cmx lib/edit.cmx \
-    kernel/evd.cmx kernel/generic.cmx library/global.cmx library/library.cmx \
+    kernel/evd.cmx kernel/generic.cmx library/global.cmx library/lib.cmx \
     kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx \
-    library/states.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \
-    proofs/pfedit.cmi 
+    proofs/tacmach.cmx kernel/term.cmx lib/util.cmx proofs/pfedit.cmi 
 proofs/proof_trees.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \
     kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/pretty.cmi \
     parsing/printer.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \
diff --git a/library/declare.ml b/library/declare.ml
index bcfc312dff..067274aa73 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -24,8 +24,19 @@ let make_strength = function
 
 (* Variables. *)
 
-let cache_variable (_,obj) = 
-  Global.push_var obj
+type variable_declaration = identifier * constr * strength * bool
+
+let vartab = ref (Spmap.empty : variable_declaration Spmap.t)
+
+let _ = Summary.declare_summary "VARIABLE"
+	  { Summary.freeze_function = (fun () -> !vartab);
+	    Summary.unfreeze_function = (fun ft -> vartab := ft);
+	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
+
+let cache_variable (sp,((id,ty,_,_) as vd)) = 
+  Global.push_var (id,ty);
+  Nametab.push id sp;
+  vartab := Spmap.add sp vd !vartab
 
 let load_variable _ = 
   anomaly "we shouldn't load a variable"
@@ -44,11 +55,10 @@ let (in_variable, out_variable) =
     specification_function = specification_variable } in
   declare_object ("VARIABLE", od)
 
-let declare_variable id c =
-  let obj = (id,c) in
-  Global.push_var obj;
-  let _ = add_leaf id CCI (in_variable obj) in
-  ()
+let declare_variable ((id,ty,_,_) as obj) =
+  Global.push_var (id,ty);
+  let sp = add_leaf id CCI (in_variable obj) in
+  Nametab.push id sp
 
 (* Parameters. *)
 
@@ -76,6 +86,15 @@ let declare_parameter id c =
  
 (* Constants. *)
 
+type constant_declaration = identifier * constant_entry * strength * bool
+
+let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
+
+let _ = Summary.declare_summary "CONSTANT"
+	  { Summary.freeze_function = (fun () -> !vartab);
+	    Summary.unfreeze_function = (fun ft -> vartab := ft);
+	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
+
 let cache_constant (sp,ce) =
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
@@ -95,7 +114,7 @@ let (in_constant, out_constant) =
     specification_function = specification_constant } in
   declare_object ("CONSTANT", od)
 
-let declare_constant id ce =
+let declare_constant ((id,ce,_,_) as cd) =
   let sp = add_leaf id CCI (in_constant ce) in
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
@@ -176,12 +195,23 @@ let out_syntax_constant id = Idmap.find id !syntax_table
 
 (* Test and access functions. *)
 
-let is_constant sp = failwith "TODO"
+let is_constant sp = 
+  try let _ = Global.lookup_constant sp in true with Not_found -> false
+
 let constant_strength sp = failwith "TODO"
 
-let is_variable id = failwith "TODO"
-let out_variable sp = failwith "TODO"
-let variable_strength id = failwith "TODO"
+let is_variable id = 
+  let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
+  
+let out_variable sp = 
+  let (id,_,str,sticky) = Spmap.find sp !vartab in
+  let (_,ty) = Global.lookup_var id in
+  (id,ty,str,sticky)
+
+let variable_strength id =
+  let sp = Nametab.sp_of_id CCI id in 
+  let (_,_,str,_) = Spmap.find sp !vartab in
+  str
 
 (* Global references. *)
 
@@ -263,8 +293,10 @@ let declare_eliminations sp =
   let redmind = minductype_spec env sigma mind in
   let mindstr = string_of_id mindid in
   let declare na c =
-    declare_constant (id_of_string na) 
-      { const_entry_body = c; const_entry_type = None } in
+    declare_constant 
+      (id_of_string na, { const_entry_body = c; const_entry_type = None },
+       false, NeverDischarge)
+  in
   let mispec = Global.lookup_mind_specif redmind in 
   let elim_scheme = 
     strip_all_casts (mis_make_indrec env sigma [] mispec).(0) in
diff --git a/library/declare.mli b/library/declare.mli
index 8a75172b63..952fa0500b 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -20,16 +20,24 @@ type strength =
   | DischargeAt of section_path 
   | NeverDischarge
 
-val declare_variable : identifier -> constr -> unit
+type variable_declaration = identifier * constr * strength * bool
+
+val declare_variable : variable_declaration -> unit
+
+
+type constant_declaration = identifier * constant_entry * strength * bool
+
+val declare_constant : constant_declaration -> unit
 
 val declare_parameter : identifier -> constr -> unit
 
-val declare_constant : identifier -> constant_entry -> unit
 
 val declare_mind : mutual_inductive_entry -> unit
 
+
 val declare_eliminations : section_path -> unit
 
+
 val declare_syntax_constant : identifier -> constr -> unit
 
 val make_strength : string list -> strength
@@ -40,7 +48,7 @@ val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
 
 val is_variable : identifier -> bool
-val out_variable : section_path -> identifier * typed_type * strength
+val out_variable : section_path -> identifier * typed_type * strength * bool
 val variable_strength : identifier -> strength
 
 val out_syntax_constant : identifier -> constr
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index f2befc1d26..d06be7d625 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -9,9 +9,12 @@ open Generic
 open Term
 open Environ
 open Evd
+open Reduction
 open Impargs
 open Rawterm
+open Typing
 open Pretyping
+open Evarutil
 open Ast
 open Coqast
 
@@ -614,8 +617,7 @@ let ast_adjust_consts sigma = (* locations are kept *)
   dbrec
 
 let globalize_command ast =
-  let env = Global.unsafe_env () in
-  let sign = Environ.var_context env in
+  let sign = Global.var_context () in
   ast_adjust_consts Evd.empty (gLOB sign) ast
 
 (* Avoid globalizing in non command ast for tactics *)
@@ -708,7 +710,7 @@ let constr_of_com_casted sigma env com typ =
   let c = raw_constr_of_com sigma sign com in
   let isevars = ref sigma in
   try
-    let j = unsafe_fmachine
+    let j = unsafe_machine
 	      (mk_tycon (nf_ise1 sigma typ)) false isevars [] env c in
     (j_apply (process_evars true !isevars) j).uj_val
   with e -> 
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index ea83e68b1f..35e37290bf 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -46,7 +46,7 @@ let print_typed_value_in_env env (trm,typ) =
   [< term0 (gLOB sign) trm ; 'fNL ;
      'sTR "     : "; term0 (gLOB sign) typ ; 'fNL >]
 
-let print_typed_value x = print_typed_value_in_env (Global.unsafe_env()) x
+let print_typed_value x = print_typed_value_in_env (Global.env()) x
 			  		  
 let print_recipe = function
   | Some c -> prterm c
@@ -131,7 +131,7 @@ let print_mutual sp mib =
   let pk = kind_of_path sp in
   let pterm,pterminenv =
     if pk = FW then (fprterm,fterm0) else (prterm,term0) in
-  let env = Global.unsafe_env () in
+  let env = Global.env () in
   let evd = Evd.empty in
   let {mind_packets=mipv; mind_nparams=nparams} = mib in 
   let (lpars,_) = decomp_n_prod env evd nparams mipv.(0).mind_arity.body in
@@ -218,7 +218,7 @@ let print_leaf_entry with_values sep (spopt,lobj) =
   let tag = object_tag lobj in
   match (spopt,tag) with
     | (_,"VARIABLE") ->
-	let (name,typ,_) = out_variable spopt in
+	let (name,typ,_,_) = out_variable spopt in
 	let l = implicits_of_var (kind_of_path spopt) name in
 	[< print_var (string_of_id name) typ; print_impl_args l; 'fNL >]
  
@@ -359,7 +359,7 @@ let crible (fn:string -> unit assumptions -> constr -> unit) name =
     | (spopt,Lib.Leaf lobj)::rest ->
 	(match (spopt,object_tag lobj) with
 	   | (_,"VARIABLE") ->
-	       let (namec,typ,_) = out_variable spopt in 
+	       let (namec,typ,_,_) = out_variable spopt in 
                if (head_const typ.body) = const then  
                  fn (string_of_id namec) hyps typ.body;
                crible_rec rest
@@ -437,7 +437,7 @@ let print_name name =
 
 let print_opaque_name name = 
   let sigma = Evd.empty in
-  let env = Global.unsafe_env () in
+  let env = Global.env () in
   let sign = Global.var_context () in
   try 
     match global_reference CCI name with
@@ -466,7 +466,7 @@ let print_local_context () =
     | [] -> [< >]
     | (sp,Lib.Leaf lobj)::rest ->
 	if "VARIABLE" = object_tag lobj then
-          let (name,typ,_) = out_variable sp in 
+          let (name,typ,_,_) = out_variable sp in 
 	  [< print_var_rec rest;
              print_var (string_of_id name) typ >]
 	else 
@@ -500,7 +500,7 @@ let fprint_judge {uj_val=trm;uj_type=typ} =
 
 let unfold_head_fconst = 
   let rec unfrec = function
-    | DOPN(Const _,_) as k -> constant_value (Global.unsafe_env()) k 
+    | DOPN(Const _,_) as k -> constant_value (Global.env()) k 
     | DOP2(Lambda,t,DLAM(na,b)) -> DOP2(Lambda,t,DLAM(na,unfrec b))
     | DOPN(AppL,v) -> DOPN(AppL,array_cons (unfrec (array_hd v)) (array_tl v))
     | x -> x
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index c12f9bb34f..44af99e19f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -136,6 +136,9 @@ let safe_machine env sigma constr =
   let mf = { fix = false; nocheck = false } in
   execute mf env sigma constr
 
+let unsafe_machine env sigma constr =
+  let mf = { fix = false; nocheck = true } in
+  execute mf env sigma constr
 
 (* Type of a constr *)
 
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 80fcc5ec99..ee68e518f4 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -10,6 +10,8 @@ open Evd
 (* This module provides the typing machine with existential variables
    (but without universes). *)
 
+val unsafe_machine : env -> 'a evar_map -> constr -> unsafe_judgment
+
 val type_of : env -> 'a evar_map -> constr -> constr
 
 val execute_type : env -> 'a evar_map -> constr -> typed_type
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 02620168c1..9d2d5ec92a 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -13,7 +13,7 @@ open Type_errors
 open Safe_typing
 open G_minicoq
 
-let (env : environment ref) = ref empty_environment
+let (env : safe_environment ref) = ref empty_environment
 
 let lookup_var id =
   let rec look n = function