diff options
Diffstat (limited to 'interp/coqlib.ml')
| -rw-r--r-- | interp/coqlib.ml | 202 |
1 files changed, 156 insertions, 46 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index ca758458..898369be 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqlib.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id$ *) open Util open Pp @@ -15,6 +15,7 @@ open Term open Libnames open Pattern open Nametab +open Smartlocate (************************************************************************) (* Generic functions to find Coq objects *) @@ -25,10 +26,8 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (id_of_string s) in - try - Nametab.absolute_reference sp - with Not_found -> - anomaly (locstr^": cannot find "^(string_of_path sp)) + try global_of_extended_global (Nametab.extended_global_of_path sp) + with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp)) let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = constr_of_global (coq_reference locstr dir s) @@ -37,25 +36,29 @@ let gen_reference = coq_reference let gen_constant = coq_constant let has_suffix_in_dirs dirs ref = - let dir = dirpath (sp_of_global ref) in + let dir = dirpath (path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs +let global_of_extended q = + try Some (global_of_extended_global q) with Not_found -> None + let gen_constant_in_modules locstr dirs s = let dirs = List.map make_dir dirs in let id = id_of_string s in - let all = Nametab.locate_all (make_short_qualid id) in + let all = Nametab.locate_extended_all (qualid_of_ident id) in + let all = list_uniquize (list_map_filter global_of_extended all) in let these = List.filter (has_suffix_in_dirs dirs) all in match these with | [x] -> constr_of_global 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) + prlist_with_sep pr_comma pr_dirpath dirs) | l -> - anomalylabstrm "" + 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) + prlist_with_sep pr_comma pr_dirpath dirs) (* For tactics/commands requiring vernacular libraries *) @@ -63,21 +66,29 @@ let gen_constant_in_modules locstr dirs s = let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in + let mp = (fst(Lib.current_prefix())) in + let current_dir = match mp with + | MPfile dp -> (dir=dp) + | _ -> false + in if not (Library.library_is_loaded dir) then + if not current_dir then (* Loading silently ... let m, prefix = list_sep_last d' in - read_library + read_library (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) *) (* or failing ...*) - error ("Library "^(string_of_dirpath dir)^" has to be required first.") + error ("Library "^(string_of_dirpath dir)^" has to be required first.") (************************************************************************) (* Specific Coq objects *) let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s -let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s +let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s + +let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s let arith_dir = ["Coq";"Arith"] let arith_modules = [arith_dir] @@ -96,7 +107,7 @@ let init_modules = [ 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" @@ -104,12 +115,21 @@ let datatypes_id = id_of_string "Datatypes" let logic_module_name = ["Coq";"Init";"Logic"] let logic_module = make_dir logic_module_name -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"] + +let logic_type_module_name = ["Coq";"Init";"Logic_Type"] +let logic_type_module = make_dir logic_type_module_name + +let datatypes_module_name = ["Coq";"Init";"Datatypes"] +let datatypes_module = make_dir datatypes_module_name + +let arith_module_name = ["Coq";"Arith";"Arith"] +let arith_module = make_dir arith_module_name + +let jmeq_module_name = ["Coq";"Logic";"JMeq"] +let jmeq_module = make_dir jmeq_module_name (* TODO: temporary hack *) -let make_kn dir id = Libnames.encode_kn dir id +let make_kn dir id = Libnames.encode_mind dir id let make_con dir id = Libnames.encode_con dir id (** Identity *) @@ -142,9 +162,14 @@ let glob_false = ConstructRef path_of_false (** Equality *) let eq_kn = make_kn logic_module (id_of_string "eq") - let glob_eq = IndRef (eq_kn,0) +let identity_kn = make_kn datatypes_module (id_of_string "identity") +let glob_identity = IndRef (identity_kn,0) + +let jmeq_kn = make_kn jmeq_module (id_of_string "JMeq") +let glob_jmeq = IndRef (jmeq_kn,0) + type coq_sigma_data = { proj1 : constr; proj2 : constr; @@ -159,7 +184,7 @@ type coq_bool_data = { type 'a delayed = unit -> 'a -let build_bool_type () = +let build_bool_type () = { andb = init_constant ["Datatypes"] "andb"; andb_prop = init_constant ["Datatypes"] "andb_prop"; andb_true_intro = init_constant ["Datatypes"] "andb_true_intro" } @@ -182,41 +207,93 @@ let build_prod () = typ = init_constant ["Datatypes"] "prod" } (* Equalities *) -type coq_leibniz_eq_data = { +type coq_eq_data = { eq : constr; - refl : constr; ind : constr; - rrec : constr option; - rect : constr option; - congr: constr; - sym : constr } + refl : constr; + sym : constr; + trans: constr; + congr: constr } + +(* Data needed for discriminate and injection *) +type coq_inversion_data = { + inv_eq : constr; (* : forall params, t -> Prop *) + inv_ind : constr; (* : forall params P y, eq params y -> P y *) + inv_congr: constr (* : forall params B (f:t->B) y, eq params y -> f c=f y *) +} let lazy_init_constant dir id = lazy (init_constant dir id) +let lazy_logic_constant dir id = lazy (logic_constant dir id) + +(* Leibniz equality on Type *) -(* 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_refl = lazy_init_constant ["Logic"] "eq_refl" 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_eq_sym = lazy_init_constant ["Logic"] "eq_sym" +let coq_eq_trans = lazy_init_constant ["Logic"] "eq_trans" let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2" +let coq_eq_congr_canonical = + lazy_init_constant ["Logic"] "f_equal_canonical_form" let build_coq_eq_data () = let _ = check_required_library logic_module_name in { 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 } + refl = Lazy.force coq_eq_refl; + sym = Lazy.force coq_eq_sym; + trans = Lazy.force coq_eq_trans; + congr = Lazy.force coq_eq_congr } let build_coq_eq () = Lazy.force coq_eq_eq -let build_coq_sym_eq () = Lazy.force coq_eq_sym +let build_coq_eq_refl () = Lazy.force coq_eq_refl +let build_coq_eq_sym () = Lazy.force coq_eq_sym let build_coq_f_equal2 () = Lazy.force coq_f_equal2 +let build_coq_sym_eq = build_coq_eq_sym (* compatibility *) + +let build_coq_inversion_eq_data () = + let _ = check_required_library logic_module_name in { + inv_eq = Lazy.force coq_eq_eq; + inv_ind = Lazy.force coq_eq_ind; + inv_congr = Lazy.force coq_eq_congr_canonical } + +(* Heterogenous equality on Type *) + +let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq" +let coq_jmeq_refl = lazy_logic_constant ["JMeq"] "JMeq_refl" +let coq_jmeq_ind = lazy_logic_constant ["JMeq"] "JMeq_ind" +let coq_jmeq_rec = lazy_logic_constant ["JMeq"] "JMeq_rec" +let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect" +let coq_jmeq_sym = lazy_logic_constant ["JMeq"] "JMeq_sym" +let coq_jmeq_congr = lazy_logic_constant ["JMeq"] "JMeq_congr" +let coq_jmeq_trans = lazy_logic_constant ["JMeq"] "JMeq_trans" +let coq_jmeq_congr_canonical = + lazy_logic_constant ["JMeq"] "JMeq_congr_canonical_form" + +let build_coq_jmeq_data () = + let _ = check_required_library jmeq_module_name in { + eq = Lazy.force coq_jmeq_eq; + ind = Lazy.force coq_jmeq_ind; + refl = Lazy.force coq_jmeq_refl; + sym = Lazy.force coq_jmeq_sym; + trans = Lazy.force coq_jmeq_trans; + congr = Lazy.force coq_jmeq_congr } + +let join_jmeq_types eq = + mkLambda(Name (id_of_string "A"),Termops.new_Type(), + mkLambda(Name (id_of_string "x"),mkRel 1, + mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|]))) + +let build_coq_inversion_jmeq_data () = + let _ = check_required_library logic_module_name in { + inv_eq = join_jmeq_types (Lazy.force coq_jmeq_eq); + inv_ind = Lazy.force coq_jmeq_ind; + inv_congr = Lazy.force coq_jmeq_congr_canonical } + (* Specif *) let coq_sumbool = lazy_init_constant ["Specif"] "sumbool" @@ -228,17 +305,38 @@ let coq_identity_refl = lazy_init_constant ["Datatypes"] "refl_identity" let coq_identity_ind = lazy_init_constant ["Datatypes"] "identity_ind" let coq_identity_rec = lazy_init_constant ["Datatypes"] "identity_rec" let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect" -let coq_identity_congr = lazy_init_constant ["Logic_Type"] "congr_id" -let coq_identity_sym = lazy_init_constant ["Logic_Type"] "sym_id" +let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr" +let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym" +let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans" +let coq_identity_congr_canonical = lazy_init_constant ["Logic_Type"] "identity_congr_canonical_form" -let build_coq_identity_data () = { +let build_coq_identity_data () = + let _ = check_required_library datatypes_module_name in { eq = Lazy.force coq_identity_eq; - refl = Lazy.force coq_identity_refl; ind = Lazy.force coq_identity_ind; - rrec = Some (Lazy.force coq_identity_rec); - rect = Some (Lazy.force coq_identity_rect); - congr = Lazy.force coq_identity_congr; - sym = Lazy.force coq_identity_sym } + refl = Lazy.force coq_identity_refl; + sym = Lazy.force coq_identity_sym; + trans = Lazy.force coq_identity_trans; + congr = Lazy.force coq_identity_congr } + +let build_coq_inversion_identity_data () = + let _ = check_required_library datatypes_module_name in + let _ = check_required_library logic_type_module_name in { + inv_eq = Lazy.force coq_identity_eq; + inv_ind = Lazy.force coq_identity_ind; + inv_congr = Lazy.force coq_identity_congr_canonical } + +(* Equality to true *) +let coq_eq_true_eq = lazy_init_constant ["Datatypes"] "eq_true" +let coq_eq_true_ind = lazy_init_constant ["Datatypes"] "eq_true_ind" +let coq_eq_true_congr = lazy_init_constant ["Logic"] "eq_true_congr" + +let build_coq_inversion_eq_true_data () = + let _ = check_required_library datatypes_module_name in + let _ = check_required_library logic_module_name in { + inv_eq = Lazy.force coq_eq_true_eq; + inv_ind = Lazy.force coq_eq_true_ind; + inv_congr = Lazy.force coq_eq_true_congr } (* The False proposition *) let coq_False = lazy_init_constant ["Logic"] "False" @@ -253,6 +351,10 @@ let coq_and = lazy_init_constant ["Logic"] "and" let coq_conj = lazy_init_constant ["Logic"] "conj" let coq_or = lazy_init_constant ["Logic"] "or" let coq_ex = lazy_init_constant ["Logic"] "ex" +let coq_iff = lazy_init_constant ["Logic"] "iff" + +let coq_iff_left_proj = lazy_init_constant ["Logic"] "proj1" +let coq_iff_right_proj = lazy_init_constant ["Logic"] "proj2" (* Runtime part *) let build_coq_True () = Lazy.force coq_True @@ -262,12 +364,19 @@ 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_conj () = Lazy.force coq_conj -let build_coq_or () = Lazy.force coq_or -let build_coq_ex () = Lazy.force coq_ex +let build_coq_or () = Lazy.force coq_or +let build_coq_ex () = Lazy.force coq_ex +let build_coq_iff () = Lazy.force coq_iff + +let build_coq_iff_left_proj () = Lazy.force coq_iff_left_proj +let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj + (* The following is less readable but does not depend on parsing *) let coq_eq_ref = lazy (init_reference ["Logic"] "eq") -let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") +let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity") +let coq_jmeq_ref = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq") +let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true") let coq_existS_ref = lazy (anomaly "use coq_existT_ref") let coq_existT_ref = lazy (init_reference ["Specif"] "existT") let coq_not_ref = lazy (init_reference ["Logic"] "not") @@ -275,4 +384,5 @@ 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") let coq_or_ref = lazy (init_reference ["Logic"] "or") +let coq_iff_ref = lazy (init_reference ["Logic"] "iff") |