Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib) et suppression Stock

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

4 files changed, 380 insertions, 32 deletions

diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
new file mode 100644
index 0000000000..94c23ef197
--- /dev/null
+++ b/parsing/coqlib.ml
@@ -0,0 +1,267 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Term
+open Declare
+open Pattern
+
+let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI
+let myvar_path =
+  make_path ["Coq";"Arith";"Arith"] (id_of_string "My_special_variable") CCI
+
+let glob_nat = IndRef (nat_path,0)
+
+let glob_O = ConstructRef ((nat_path,0),1)
+let glob_S = ConstructRef ((nat_path,0),2)
+
+let glob_My_special_variable_nat = ConstRef myvar_path
+
+let reference dir s =
+  let dir = "Coq"::"Init"::[dir] in
+  try 
+    Nametab.locate_in_absolute_module dir (id_of_string s)
+  with Not_found ->
+    anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir s)))
+
+let constant dir s =
+  Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s)
+
+type coq_sigma_data = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  typ   : constr }
+
+type 'a delayed = unit -> 'a
+
+let build_sigma_set () =
+  { proj1 = constant "Specif" "projS1";
+    proj2 = constant "Specif" "projS2";
+    elim = constant "Specif" "sigS_rec";
+    intro = constant "Specif" "existS";
+    typ = constant "Specif" "sigS" }
+
+let build_sigma_type () =
+  { proj1 = constant "Logic_Type" "projT1";
+    proj2 = constant "Logic_Type" "projT2";
+    elim = constant "Logic_Type" "sigT_rec";
+    intro = constant "Logic_Type" "existT";
+    typ = constant "Logic_Type" "sigT" }
+
+(* Equalities *)
+type coq_leibniz_eq_data = {
+  eq   : constr delayed;
+  ind  : constr delayed;
+  rrec : constr delayed option;
+  rect : constr delayed option;
+  congr: constr delayed;
+  sym  : constr delayed }
+
+let constant dir id = lazy (constant dir id)
+
+(* Equality on Set *)
+let coq_eq_eq = constant "Logic" "eq"
+let coq_eq_ind = constant "Logic" "eq_ind"
+let coq_eq_rec = constant "Logic" "eq_rec"
+let coq_eq_rect = constant "Logic" "eq_rect"
+let coq_eq_congr = constant "Logic" "f_equal"
+let coq_eq_sym  = constant "Logic" "sym_eq"
+let coq_f_equal2 = constant "Logic" "f_equal2"
+
+let build_coq_eq_data = {
+  eq = (fun () -> Lazy.force coq_eq_eq);
+  ind = (fun () -> Lazy.force coq_eq_ind);
+  rrec = Some (fun () -> Lazy.force coq_eq_rec);
+  rect = Some (fun () -> Lazy.force coq_eq_rect);
+  congr = (fun () -> Lazy.force coq_eq_congr);
+  sym  = (fun () -> Lazy.force coq_eq_sym) }
+
+let build_coq_eq = build_coq_eq_data.eq
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+(* Specif *)
+let coq_sumbool  = constant "Specif" "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type *)
+let coq_eqT_eq = constant "Logic_Type" "eqT"
+let coq_eqT_ind = constant "Logic_Type" "eqT_ind"
+let coq_eqT_congr =constant "Logic_Type" "congr_eqT"
+let coq_eqT_sym  = constant "Logic_Type" "sym_eqT"
+
+let build_coq_eqT_data = {
+  eq = (fun () -> Lazy.force coq_eqT_eq);
+  ind = (fun () -> Lazy.force coq_eqT_ind);
+  rrec = None;
+  rect = None;
+  congr = (fun () -> Lazy.force coq_eqT_congr);
+  sym  = (fun () -> Lazy.force coq_eqT_sym) }
+
+let build_coq_eqT = build_coq_eqT_data.eq
+let build_coq_sym_eqT = build_coq_eqT_data.sym
+
+(* Equality on Type as a Type *)
+let coq_idT_eq = constant "Logic_Type" "identityT"
+let coq_idT_ind = constant "Logic_Type" "identityT_ind"
+let coq_idT_rec = constant "Logic_Type" "identityT_rec"
+let coq_idT_rect = constant "Logic_Type" "identityT_rect"
+let coq_idT_congr = constant "Logic_Type" "congr_idT"
+let coq_idT_sym = constant "Logic_Type" "sym_idT"
+
+let build_coq_idT_data = {
+  eq = (fun () -> Lazy.force coq_idT_eq);
+  ind = (fun () -> Lazy.force coq_idT_ind);
+  rrec = Some (fun () -> Lazy.force coq_idT_rec);
+  rect = Some (fun () -> Lazy.force coq_idT_rect);
+  congr = (fun () -> Lazy.force coq_idT_congr);
+  sym  = (fun () -> Lazy.force coq_idT_sym) }
+
+(* Empty Type *)
+let coq_EmptyT = constant "Logic_Type" "EmptyT"
+
+(* Unit Type and its unique inhabitant *)
+let coq_UnitT  = constant "Logic_Type" "UnitT"
+let coq_IT     = constant "Logic_Type" "IT"
+
+(* The False proposition *)
+let coq_False  = constant "Logic" "False"
+
+(* The True proposition and its unique proof *)
+let coq_True   = constant "Logic" "True"
+let coq_I      = constant "Logic" "I"
+
+(* Connectives *)
+let coq_not = constant "Logic" "not"
+let coq_and = constant "Logic" "and"
+let coq_or = constant "Logic" "or"
+let coq_ex = constant "Logic" "ex"
+
+(* Runtime part *)
+let build_coq_EmptyT () = Lazy.force coq_EmptyT
+let build_coq_UnitT () = Lazy.force coq_UnitT
+let build_coq_IT ()    = Lazy.force coq_IT
+
+let build_coq_True ()  = Lazy.force coq_True
+let build_coq_I ()     = Lazy.force coq_I
+
+let build_coq_False () = Lazy.force coq_False
+let build_coq_not ()   = Lazy.force coq_not
+let build_coq_and ()   = Lazy.force coq_and
+let build_coq_or ()   = Lazy.force coq_or
+let build_coq_ex ()   = Lazy.force coq_ex
+
+(****************************************************************************)
+(*                             Patterns                                     *)
+(* This needs to have interp_constrpattern available ...
+let parse_astconstr s =
+  try 
+    Pcoq.parse_string Pcoq.Constr.constr_eoi s 
+  with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) ->
+    error "Syntax error : not a construction"
+
+let parse_pattern s =
+  Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_astconstr s)
+
+let coq_eq_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic.eq ?1 ?2 ?3)"))
+let coq_eqT_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.eqT ?1 ?2 ?3)"))
+let coq_idT_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.identityT ?1 ?2 ?3)"))
+let coq_existS_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Specif.existS ?1 ?2 ?3 ?4)"))
+let coq_existT_pattern = 
+  lazy (snd (parse_pattern "(Coq.Init.Logic_Type.existT ?1 ?2 ?3 ?4)"))
+let coq_not_pattern =
+  lazy (snd (parse_pattern "(Coq.Init.Logic.not ?)"))
+let coq_imp_False_pattern =
+  lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_imp_False_pattern =
+  lazy (snd (parse_pattern "? -> Coq.Init.Logic.False"))
+let coq_eqdec_partial_pattern
+  lazy (snd (parse_pattern "(sumbool (eq ?1 ?2 ?3) ?4)"))
+let coq_eqdec_pattern
+  lazy (snd (parse_pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"))
+*)
+
+(* The following is less readable but does not depend on parsing *)
+let coq_eq_ref      = lazy (reference "Logic" "eq")
+let coq_eqT_ref     = lazy (reference "Logic_Type" "eqT")
+let coq_idT_ref     = lazy (reference "Logic_Type" "identityT")
+let coq_existS_ref  = lazy (reference "Specif" "existS")
+let coq_existT_ref  = lazy (reference "Logic_Type" "existT")
+let coq_not_ref     = lazy (reference "Logic" "not")
+let coq_False_ref   = lazy (reference "Logic" "False")
+let coq_sumbool_ref = lazy (reference "Specif" "sumbool")
+
+(* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *)
+let coq_eq_pattern_gen eq = 
+  lazy (PApp(PRef (Lazy.force eq), Array.init 3 (fun i -> PMeta (Some (i+1)))))
+let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
+let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref
+let coq_idT_pattern = coq_eq_pattern_gen coq_idT_ref
+
+(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
+let coq_ex_pattern_gen ex =
+  lazy (PApp(PRef (Lazy.force ex), Array.init 4 (fun i -> PMeta (Some (i+1)))))
+let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref
+let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
+
+(* Patterns "~ ?", "? -> False" and "(?1 -> ?2)" *)
+let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|]))
+let imp a b = PProd (Anonymous, a, b)
+let coq_imp_False_pattern =
+  lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref)))
+let coq_arrow_pattern = lazy (imp (PMeta (Some 1)) (PMeta (Some 2)))
+
+(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *)
+let coq_eqdec_partial_pattern =
+  lazy
+    (PApp
+       (PRef (Lazy.force coq_sumbool_ref),
+	[| Lazy.force coq_eq_pattern; PMeta (Some 4) |]))
+
+(* The expected form of the goal for the tactic Decide Equality *)
+
+(* Pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" *)
+(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *)
+let x = Name (id_of_string "x")
+let y = Name (id_of_string "y")
+let coq_eqdec_pattern =
+  lazy
+    (PProd (x, PMeta (Some 1), PProd (y, PMeta (Some 1), 
+    PApp (PRef (Lazy.force coq_sumbool_ref),
+	  [| PApp (PRef (Lazy.force coq_eq_ref),
+		   [| PMeta (Some 1); PRel 2; PRel 1 |]);
+	     PApp (PRef (Lazy.force coq_not_ref), 
+		   [|PApp (PRef (Lazy.force coq_eq_ref),
+ 			   [| PMeta (Some 1); PRel 2; PRel 1 |])|]) |]))))
+
+(* "(A : ?)(x:A)(? A x x)" and "(x : ?)(? x x)" *)
+let name_A = Name (id_of_string "A")
+let coq_refl_rel1_pattern =
+  lazy
+    (PProd
+       (name_A, PMeta None,
+	PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|]))))
+let coq_refl_rel2_pattern =
+  lazy
+    (PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|])))
+
+
+let build_coq_eq_pattern () = Lazy.force coq_eq_pattern
+let build_coq_eqT_pattern () = Lazy.force coq_eqT_pattern
+let build_coq_idT_pattern () = Lazy.force coq_idT_pattern
+let build_coq_existS_pattern () = Lazy.force coq_existS_pattern
+let build_coq_existT_pattern () = Lazy.force coq_existT_pattern
+let build_coq_not_pattern () = Lazy.force coq_not_pattern
+let build_coq_imp_False_pattern () = Lazy.force coq_imp_False_pattern
+let build_coq_eqdec_partial_pattern () = Lazy.force coq_eqdec_partial_pattern
+let build_coq_eqdec_pattern () = Lazy.force coq_eqdec_pattern
+let build_coq_arrow_pattern () = Lazy.force coq_arrow_pattern
+let build_coq_refl_rel1_pattern () = Lazy.force coq_refl_rel1_pattern
+let build_coq_refl_rel2_pattern () = Lazy.force coq_refl_rel2_pattern
diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli
new file mode 100644
index 0000000000..c835eeffa3
--- /dev/null
+++ b/parsing/coqlib.mli
@@ -0,0 +1,113 @@
+
+(* $Id$ *)
+
+(*i*)
+open Term
+open Pattern
+(*i*)
+
+(*s This module collects the global references of the standard library
+    used in ocaml files *)
+
+(* Natural numbers *)
+val glob_nat : global_reference
+val glob_O : global_reference
+val glob_S : global_reference
+
+(* Special variable for pretty-printing of constant naturals *)
+val glob_My_special_variable_nat : global_reference
+
+(*s For Equality tactics *)
+type coq_sigma_data = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  typ   : constr }
+
+val build_sigma_set : unit -> coq_sigma_data
+val build_sigma_type : unit -> coq_sigma_data
+
+type 'a delayed = unit -> 'a
+
+type coq_leibniz_eq_data = {
+  eq   : constr delayed;
+  ind  : constr delayed;
+  rrec : constr delayed option;
+  rect : constr delayed option;
+  congr: constr delayed;
+  sym  : constr delayed }
+
+val build_coq_eq_data : coq_leibniz_eq_data
+val build_coq_eqT_data : coq_leibniz_eq_data
+val build_coq_idT_data : coq_leibniz_eq_data
+
+val build_coq_f_equal2 : constr delayed
+val build_coq_eqT : constr delayed
+val build_coq_sym_eqT : constr delayed
+
+(* Empty Type *)
+val build_coq_EmptyT : constr delayed
+
+(* Unit Type and its unique inhabitant *)
+val build_coq_UnitT : constr delayed
+val build_coq_IT : constr delayed
+
+(* Specif *)
+val build_coq_sumbool : constr delayed
+
+(*s Connectives *)
+(* The False proposition *)
+val build_coq_False : constr delayed
+
+(* The True proposition and its unique proof *)
+val build_coq_True : constr delayed
+val build_coq_I : constr delayed
+
+(* Negation *)
+val build_coq_not : constr delayed
+
+(* Conjunction *)
+val build_coq_and : constr delayed
+
+(* Disjunction *)
+val build_coq_or : constr delayed
+
+(* Existential quantifier *)
+val build_coq_ex : constr delayed
+
+(**************************** Patterns ************************************)
+(* ["(eq ?1 ?2 ?3)"] *)
+val build_coq_eq_pattern : constr_pattern delayed
+
+(* ["(eqT ?1 ?2 ?3)"] *)
+val build_coq_eqT_pattern : constr_pattern delayed
+
+(* ["(identityT ?1 ?2 ?3)"] *)
+val build_coq_idT_pattern : constr_pattern delayed
+
+(* ["(existS ?1 ?2 ?3 ?4)"] *)
+val build_coq_existS_pattern : constr_pattern delayed
+
+(* ["(existT ?1 ?2 ?3 ?4)"] *)
+val build_coq_existT_pattern : constr_pattern delayed
+
+(* ["(not ?)"] *)
+val build_coq_not_pattern : constr_pattern delayed
+
+(* ["? -> False"] *)
+val build_coq_imp_False_pattern : constr_pattern delayed
+
+(* ["(sumbool (eq ?1 ?2 ?3) ?4)"] *)
+val build_coq_eqdec_partial_pattern : constr_pattern delayed
+
+(* ["! (x,y:?1). (sumbool (eq ?1 x y) ~(eq ?1 x y))"] *)
+val build_coq_eqdec_pattern : constr_pattern delayed
+
+(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *)
+val build_coq_refl_rel1_pattern : constr_pattern delayed
+val build_coq_refl_rel2_pattern : constr_pattern delayed
+
+(* ["(?1 -> ?2)"] *)
+val build_coq_arrow_pattern : constr_pattern delayed
+
diff --git a/parsing/stdlib.ml b/parsing/stdlib.ml
deleted file mode 100644
index 8c4e2bf681..0000000000
--- a/parsing/stdlib.ml
+++ /dev/null
@@ -1,17 +0,0 @@
-
-(* $Id$ *)
-
-open Names
-open Term
-open Declare
-
-let nat_path = make_path ["Coq";"Init";"Datatypes"] (id_of_string "nat") CCI
-let myvar_path =
-  make_path ["Coq";"Arith";"Arith"] (id_of_string "My_special_variable") CCI
-
-let glob_nat = IndRef (nat_path,0)
-
-let glob_O = ConstructRef ((nat_path,0),1)
-let glob_S = ConstructRef ((nat_path,0),2)
-
-let glob_My_special_variable_nat = ConstRef myvar_path
diff --git a/parsing/stdlib.mli b/parsing/stdlib.mli
deleted file mode 100644
index 7bb890d18d..0000000000
--- a/parsing/stdlib.mli
+++ /dev/null
@@ -1,15 +0,0 @@
-
-(* $Id$ *)
-
-open Term
-
-(*s This module collects the global references of the standard library
-    used in ocaml files *)
-
-(* Natural numbers *)
-val glob_nat : global_reference
-val glob_O : global_reference
-val glob_S : global_reference
-
-(* Special variable for pretty-printing of constant naturals *)
-val glob_My_special_variable_nat : global_reference