diff options
Diffstat (limited to 'interp/coqlib.ml')
| -rw-r--r-- | interp/coqlib.ml | 294 |
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") |