Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 294 insertions, 0 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
new file mode 100644
index 00000000..8ce9bfaf
--- /dev/null
+++ b/interp/coqlib.ml
@@ -0,0 +1,294 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: coqlib.ml,v 1.14.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+open Util
+open Pp
+open Names
+open Term
+open Libnames
+open Pattern
+open Nametab
+
+let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+
+let gen_reference locstr dir s =
+  let dir = make_dir ("Coq"::dir) in
+  let id = Constrextern.id_of_v7_string s in
+  let sp = Libnames.make_path dir id in
+  try
+    Nametab.absolute_reference sp
+  with Not_found ->
+    anomaly (locstr^": cannot find "^(string_of_path sp))
+    
+let gen_constant locstr dir s = 
+  constr_of_reference (gen_reference locstr dir s)
+
+let list_try_find f = 
+  let rec try_find_f = function
+    | [] -> raise Not_found
+    | h::t -> try f h with Not_found -> try_find_f t
+  in 
+  try_find_f
+
+let has_suffix_in_dirs dirs ref =
+  let dir = dirpath (sp_of_global ref) in
+  List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+
+let gen_constant_in_modules locstr dirs s =
+  let dirs = List.map make_dir dirs in
+  let id = Constrextern.id_of_v7_string s in
+  let all = Nametab.locate_all (make_short_qualid id) in
+  let these = List.filter (has_suffix_in_dirs dirs) all in
+  match these with
+    | [x] -> constr_of_reference x
+    | [] ->
+	anomalylabstrm "" (str (locstr^": cannot find "^s^
+	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	prlist_with_sep pr_coma pr_dirpath dirs)
+    | l ->
+	anomalylabstrm "" 
+	(str (locstr^": found more than once object of name "^s^
+	" in module"^(if List.length dirs > 1 then "s " else " ")) ++
+	prlist_with_sep pr_coma pr_dirpath dirs)
+
+let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s
+
+let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s  
+
+let arith_dir = ["Coq";"Arith"]
+let arith_modules = [arith_dir]
+
+let narith_dir = ["Coq";"NArith"]
+
+let zarith_dir = ["Coq";"ZArith"]
+let zarith_base_modules = [narith_dir;zarith_dir]
+
+let init_dir = ["Coq";"Init"]
+let init_modules = [
+  init_dir@["Datatypes"];
+  init_dir@["Logic"];
+  init_dir@["Specif"];
+  init_dir@["Logic_Type"];
+  init_dir@["Peano"];
+  init_dir@["Wf"]
+]
+  
+let coq_id = id_of_string "Coq"
+let init_id = id_of_string "Init"
+let arith_id = id_of_string "Arith"
+let datatypes_id = id_of_string "Datatypes"
+
+let logic_module = make_dir ["Coq";"Init";"Logic"]
+let logic_type_module = make_dir ["Coq";"Init";"Logic_Type"]
+let datatypes_module = make_dir ["Coq";"Init";"Datatypes"]
+let arith_module = make_dir ["Coq";"Arith";"Arith"]
+
+(* TODO: temporary hack *)
+let make_path dir id = Libnames.encode_kn dir id
+
+let nat_path = make_path datatypes_module (id_of_string "nat")
+
+let glob_nat = IndRef (nat_path,0)
+
+let path_of_O = ((nat_path,0),1)
+let path_of_S = ((nat_path,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
+
+let eq_path = make_path logic_module (id_of_string "eq")
+let eqT_path = make_path logic_module (id_of_string "eq")
+
+let glob_eq = IndRef (eq_path,0)
+let glob_eqT = IndRef (eqT_path,0)
+
+type coq_sigma_data = {
+  proj1 : constr;
+  proj2 : constr;
+  elim  : constr;
+  intro : constr;
+  typ   : constr }
+
+type 'a delayed = unit -> 'a
+
+let build_sigma_set () =
+  { proj1 = init_constant ["Specif"] "projS1";
+    proj2 = init_constant ["Specif"] "projS2";
+    elim = init_constant ["Specif"] "sigS_rec";
+    intro = init_constant ["Specif"] "existS";
+    typ = init_constant ["Specif"] "sigS" }
+
+let build_sigma_type () =
+  { proj1 = init_constant ["Specif"] "projT1";
+    proj2 = init_constant ["Specif"] "projT2";
+    elim = init_constant ["Specif"] "sigT_rec";
+    intro = init_constant ["Specif"] "existT";
+    typ = init_constant ["Specif"] "sigT" }
+
+(* Equalities *)
+type coq_leibniz_eq_data = {
+  eq   : constr;
+  refl : constr;
+  ind  : constr;
+  rrec : constr option;
+  rect : constr option;
+  congr: constr;
+  sym  : constr }
+
+let lazy_init_constant dir id = lazy (init_constant dir id)
+
+(* Equality on Set *)
+let coq_eq_eq = lazy_init_constant ["Logic"] "eq"
+let coq_eq_refl = lazy_init_constant ["Logic"] "refl_equal"
+let coq_eq_ind = lazy_init_constant ["Logic"] "eq_ind"
+let coq_eq_rec = lazy_init_constant ["Logic"] "eq_rec"
+let coq_eq_rect = lazy_init_constant ["Logic"] "eq_rect"
+let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
+let coq_eq_sym  = lazy_init_constant ["Logic"] "sym_eq"
+let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
+
+let build_coq_eq_data () = {
+  eq = Lazy.force coq_eq_eq;
+  refl = Lazy.force coq_eq_refl;
+  ind = Lazy.force coq_eq_ind;
+  rrec = Some (Lazy.force coq_eq_rec);
+  rect = Some (Lazy.force coq_eq_rect);
+  congr = Lazy.force coq_eq_congr;
+  sym  = Lazy.force coq_eq_sym }
+
+let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+(* Specif *)
+let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type *)
+
+let coq_eqT_eq = lazy_init_constant ["Logic"] "eq"
+let coq_eqT_refl = lazy_init_constant ["Logic"] "refl_equal"
+let coq_eqT_ind = lazy_init_constant ["Logic"] "eq_ind"
+let coq_eqT_congr =lazy_init_constant ["Logic"] "f_equal"
+let coq_eqT_sym  = lazy_init_constant ["Logic"] "sym_eq"
+
+let build_coq_eqT_data () = {
+  eq = Lazy.force coq_eqT_eq;
+  refl = Lazy.force coq_eqT_refl;
+  ind = Lazy.force coq_eqT_ind;
+  rrec = None;
+  rect = None;
+  congr = Lazy.force coq_eqT_congr;
+  sym  = Lazy.force coq_eqT_sym }
+
+let build_coq_eqT () = Lazy.force coq_eqT_eq
+let build_coq_sym_eqT () = Lazy.force coq_eqT_sym
+
+(* Equality on Type as a Type *)
+let coq_idT_eq = lazy_init_constant ["Datatypes"] "identity"
+let coq_idT_refl = lazy_init_constant ["Datatypes"] "refl_identity"
+let coq_idT_ind = lazy_init_constant ["Datatypes"] "identity_ind"
+let coq_idT_rec = lazy_init_constant ["Datatypes"] "identity_rec"
+let coq_idT_rect = lazy_init_constant ["Datatypes"] "identity_rect"
+let coq_idT_congr = lazy_init_constant ["Logic_Type"] "congr_id"
+let coq_idT_sym = lazy_init_constant ["Logic_Type"] "sym_id"
+
+let build_coq_idT_data () = {
+  eq = Lazy.force coq_idT_eq;
+  refl = Lazy.force coq_idT_refl;
+  ind = Lazy.force coq_idT_ind;
+  rrec = Some (Lazy.force coq_idT_rec);
+  rect = Some (Lazy.force coq_idT_rect);
+  congr = Lazy.force coq_idT_congr;
+  sym  = Lazy.force coq_idT_sym }
+
+let lazy_init_constant_v7 d id id7 =
+  if !Options.v7 then lazy_init_constant d id else 
+  lazy (anomaly
+   (id7^" does no longer exist in V8 new syntax, use "^id
+    ^" instead (probably an error in ML contributed code)"))
+
+(* Empty Type *)
+let coq_EmptyT = lazy_init_constant_v7 ["Logic"] "False" "EmptyT"
+
+(* Unit Type and its unique inhabitant *)
+let coq_UnitT  = lazy_init_constant_v7 ["Datatypes"] "unit" "UnitT"
+let coq_IT     = lazy_init_constant_v7 ["Datatypes"] "tt" "IT"
+
+(* The False proposition *)
+let coq_False  = lazy_init_constant ["Logic"] "False"
+
+(* The True proposition and its unique proof *)
+let coq_True   = lazy_init_constant ["Logic"] "True"
+let coq_I      = lazy_init_constant ["Logic"] "I"
+
+(* Connectives *)
+let coq_not = lazy_init_constant ["Logic"] "not"
+let coq_and = lazy_init_constant ["Logic"] "and"
+let coq_or = lazy_init_constant ["Logic"] "or"
+let coq_ex = lazy_init_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_constr 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 =
+  Constrintern.interp_constrpattern Evd.empty (Global.env()) (parse_constr 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.eq ?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.Specif.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 (init_reference ["Logic"] "eq")
+let coq_eqT_ref     = coq_eq_ref
+let coq_idT_ref     = lazy (init_reference ["Datatypes"] "identity")
+let coq_existS_ref  = lazy (init_reference ["Specif"] "existS")
+let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
+let coq_not_ref     = lazy (init_reference ["Logic"] "not")
+let coq_False_ref   = lazy (init_reference ["Logic"] "False")
+let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
+let coq_sig_ref = lazy (init_reference ["Specif"] "sig")