diff options
| -rw-r--r-- | contrib/cc/cctac.ml4 | 20 | ||||
| -rw-r--r-- | contrib/field/field.ml4 | 10 | ||||
| -rw-r--r-- | contrib/funind/tacinvutils.ml | 16 | ||||
| -rw-r--r-- | contrib/interface/pbp.ml | 24 | ||||
| -rw-r--r-- | contrib/omega/coq_omega.ml | 9 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 10 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 9 | ||||
| -rw-r--r-- | interp/coqlib.ml | 123 | ||||
| -rw-r--r-- | interp/coqlib.mli | 6 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 20 |
10 files changed, 99 insertions, 148 deletions
diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4 index ca4a24968..420d0e4db 100644 --- a/contrib/cc/cctac.ml4 +++ b/contrib/cc/cctac.ml4 @@ -32,13 +32,13 @@ exception Not_an_eq let fail()=raise Not_an_eq -let constr_of_string s () = - constr_of_reference (Nametab.locate (qualid_of_string s)) -let eq2eqT_theo = constr_of_string "Coq.Logic.Eqdep_dec.eq2eqT" -let eqT2eq_theo = constr_of_string "Coq.Logic.Eqdep_dec.eqT2eq" -let congr_theo = constr_of_string "Coq.cc.CC.Congr_nodep" -let congr_dep_theo = constr_of_string "Coq.cc.CC.Congr_dep" +let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) + +let eq2eqT_theo = constant ["Logic";"Eqdep_dec"] "eq2eqT" +let eqT2eq_theo = constant ["Logic";"Eqdep_dec"] "eqT2eq" +let congr_theo = constant ["cc";"CC"] "Congr_nodep" +let congr_dep_theo = constant ["cc";"CC"] "Congr_dep" let fresh_id1=id_of_string "eq1" and fresh_id2=id_of_string "eq2" @@ -104,7 +104,7 @@ let st_wrap theo tac= (* generate an adhoc tactic following the proof tree *) let rec proof_tac uf axioms=function - Ax id->(fun gl->(st_wrap (eq2eqT_theo ()) (exact_check (mkVar id)) gl)) + Ax id->(fun gl->(st_wrap (Lazy.force eq2eqT_theo) (exact_check (mkVar id)) gl)) | Refl t->reflexivity | Trans (p1,p2)->let t=(make_term (snd (type_proof uf axioms p1))) in (tclTHENS (transitivity t) @@ -118,14 +118,14 @@ let rec proof_tac uf axioms=function and ts2=(make_term s2) and tt2=(make_term t2) in let typ1=pf_type_of gl ts1 and typ2=pf_type_of gl ts2 in let (typb,_,_)=(eq_type_of_term gl.it.evar_concl) in - let act=mkApp ((congr_theo ()),[|typ2;typb;ts1;tt1;ts2;tt2|]) in + let act=mkApp ((Lazy.force congr_theo),[|typ2;typb;ts1;tt1;ts2;tt2|]) in tclORELSE (tclTHENS (apply act) [(proof_tac uf axioms p1);(proof_tac uf axioms p2)]) (tclTHEN (let p=mkLambda(destProd typ1) in - let acdt=mkApp((congr_dep_theo ()),[|typ2;p;ts1;tt1;ts2|]) in + let acdt=mkApp((Lazy.force congr_dep_theo),[|typ2;p;ts1;tt1;ts2|]) in apply acdt) (proof_tac uf axioms p1)) gl) @@ -139,7 +139,7 @@ let cc_tactic gl_sg= match (cc_proof prb) with None->errorlabstrm "CC" [< str "CC couldn't solve goal" >] | Some (p,uf,axioms)->let tac=proof_tac uf axioms p in - (tclORELSE (st_wrap (eqT2eq_theo ()) tac) + (tclORELSE (st_wrap (Lazy.force eqT2eq_theo) tac) (fun _->errorlabstrm "CC" [< str "CC doesn't know how to handle dependent equality." >]) gl_sg) diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index c67dea9aa..6f5668b19 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -26,15 +26,7 @@ open Tacexpr let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c (* Construction of constants *) -let constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"field"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Field: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) +let constant dir s = Coqlib.gen_constant "Field" ("field"::dir) s (* To deal with the optional arguments *) let constr_of_opt a opt = diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index f99b548ee..d90b06419 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -66,22 +66,12 @@ let prNamedLConstr s lc = prNamedLConstr_aux lc end - -(* tire de const\_omega.ml *) -let constant dir s = - try - Declare.global_absolute_reference - (Libnames.make_path - (Names.make_dirpath (List.map Names.id_of_string (List.rev dir))) - (Names.id_of_string s)) - with e -> print_endline (String.concat "." dir); print_endline s; - raise e -(* fin const\_omega.ml *) +let constant =Coqlib.gen_constant "Funind" let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) let mkRefl typ c1 = - mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), + mkApp ((constant ["Init"; "Logic"] "refl_equal"), [| typ; c1|]) let rec popn i c = if i<=0 then c else pop (popn (i-1) c) @@ -183,7 +173,7 @@ let nth_dep_constructor indtype n = build_dependent_constructor cstr_sum, cstr_sum.cs_nargs -let coq_refl_equal = lazy(constant ["Coq"; "Init"; "Logic"] "refl_equal") +let coq_refl_equal = lazy(constant ["Init"; "Logic"] "refl_equal") let rec buildrefl_from_eqs eqs = match eqs with diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index b5d6601c6..9b1602ad4 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -222,29 +222,21 @@ let (imply_elim2: pbp_rule) = function make_clears clear_names])) | _ -> None;; -let reference dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"Init"::[dir]))) in - let id = id_of_string s in - try - Nametab.absolute_reference (Libnames.make_path dir id) - with Not_found -> - anomaly ("Coqlib: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) - -let constant dir s = constr_of_reference (reference dir s);; +let reference dir s = Coqlib.gen_reference "Pbp" ("Init"::dir) s + +let constant dir s = Coqlib.gen_constant "Pbp" ("Init"::dir) s let andconstr: unit -> constr = Coqlib.build_coq_and;; -let prodconstr () = constant "Datatypes" "prod";; +let prodconstr () = constant ["Datatypes"] "prod";; let exconstr = Coqlib.build_coq_ex;; -let exTconstr () = constant "Logic_Type" "exT";; -let sigconstr () = constant "Specif" "sig";; +let exTconstr () = constant ["Logic_Type"] "exT";; +let sigconstr () = constant ["Specif"] "sig";; let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ;; let orconstr = Coqlib.build_coq_or;; let sumboolconstr = Coqlib.build_coq_sumbool;; -let sumconstr() = constant "Datatypes" "sum";; +let sumconstr() = constant ["Datatypes"] "sum";; let notconstr = Coqlib.build_coq_not;; -let notTconstr () = constant "Logic_Type" "notT";; +let notTconstr () = constant ["Logic_Type"] "notT";; let is_matching_local a b = is_matching (pattern_of_constr a) b;; diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 93408cbc4..6f988076e 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -193,14 +193,7 @@ let recognize_number t = To use the constant Zplus, one must type "Lazy.force coq_Zplus" This is the right way to access to Coq constants in tactics ML code *) -let constant dir s = - let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Coq_omega: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) +let constant = Coqlib.gen_constant "Omega" let arith_constant dir = constant ("Arith"::dir) let zarith_constant dir = constant ("ZArith"::dir) diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index a2798d7a7..393eff193 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -119,15 +119,7 @@ open Tacexpr We do that lazily, because this code can be linked before the constants are loaded in the environment *) -let constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"ring"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Quote: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) +let constant dir s = Coqlib.gen_constant "Quote" ("ring"::dir) s let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index f4848c729..c360f795a 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -38,14 +38,7 @@ open Quote let mt_evd = Evd.empty let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c -let constant dir s = - let dir = make_dirpath (List.map id_of_string (List.rev ("Coq"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Ring: cannot find "^ - (Libnames.string_of_qualid (Libnames.make_qualid dir id))) +let constant = Coqlib.gen_constant "Ring" (* Ring theory *) let coq_Ring_Theory = lazy (constant ["ring";"Ring_theory"] "Ring_Theory") diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 86857a17c..7c49c18c2 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -17,6 +17,22 @@ 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 = id_of_string s in + try + Nametab.absolute_reference (Libnames.make_path dir id) + with Not_found -> + anomaly (locstr^": cannot find "^(string_of_qualid (make_qualid dir id))) + +let gen_constant locstr dir s = + constr_of_reference (gen_reference locstr dir s) + +let init_reference dir s=gen_reference "Coqlib" ("Init"::dir) s + +let init_constant dir s=gen_constant "Coqlib" ("Init"::dir) s + let coq_id = id_of_string "Coq" let init_id = id_of_string "Init" let arith_id = id_of_string "Arith" @@ -45,16 +61,6 @@ 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) -let reference dir s = - let dir = make_dir ("Coq"::"Init"::[dir]) in - let id = id_of_string s in - try - Nametab.absolute_reference (Libnames.make_path dir id) - with Not_found -> - anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id))) - -let constant dir s = constr_of_reference (reference dir s) - type coq_sigma_data = { proj1 : constr; proj2 : constr; @@ -65,18 +71,18 @@ type coq_sigma_data = { 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" } + { 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 = constant "Specif" "projT1"; - proj2 = constant "Specif" "projT2"; - elim = constant "Specif" "sigT_rec"; - intro = constant "Specif" "existT"; - typ = constant "Specif" "sigT" } + { 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 = { @@ -87,16 +93,16 @@ type coq_leibniz_eq_data = { congr: constr delayed; sym : constr delayed } -let constant dir id = lazy (constant dir id) +let lazy_init_constant dir id = lazy (init_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 coq_eq_eq = lazy_init_constant ["Logic"] "eq" +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 = (fun () -> Lazy.force coq_eq_eq); @@ -110,15 +116,16 @@ 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 coq_sumbool = lazy_init_constant ["Specif"] "sumbool" let build_coq_sumbool () = Lazy.force coq_sumbool (* Equality on Type *) -let coq_eqT_eq = constant "Logic" "eq" -let coq_eqT_ind = constant "Logic" "eq_ind" -let coq_eqT_congr =constant "Logic" "f_equal" -let coq_eqT_sym = constant "Logic" "sym_eq" + +let coq_eqT_eq = lazy_init_constant ["Logic"] "eq" +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 = (fun () -> Lazy.force coq_eqT_eq); @@ -132,12 +139,12 @@ 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 coq_idT_eq = lazy_init_constant ["Logic_Type"] "identityT" +let coq_idT_ind = lazy_init_constant ["Logic_Type"] "identityT_ind" +let coq_idT_rec = lazy_init_constant ["Logic_Type"] "identityT_rec" +let coq_idT_rect = lazy_init_constant ["Logic_Type"] "identityT_rect" +let coq_idT_congr = lazy_init_constant ["Logic_Type"] "congr_idT" +let coq_idT_sym = lazy_init_constant ["Logic_Type"] "sym_idT" let build_coq_idT_data = { eq = (fun () -> Lazy.force coq_idT_eq); @@ -148,24 +155,24 @@ let build_coq_idT_data = { sym = (fun () -> Lazy.force coq_idT_sym) } (* Empty Type *) -let coq_EmptyT = constant "Logic_Type" "EmptyT" +let coq_EmptyT = lazy_init_constant ["Logic_Type"] "EmptyT" (* Unit Type and its unique inhabitant *) -let coq_UnitT = constant "Logic_Type" "UnitT" -let coq_IT = constant "Logic_Type" "IT" +let coq_UnitT = lazy_init_constant ["Logic_Type"] "UnitT" +let coq_IT = lazy_init_constant ["Logic_Type"] "IT" (* The False proposition *) -let coq_False = constant "Logic" "False" +let coq_False = lazy_init_constant ["Logic"] "False" (* The True proposition and its unique proof *) -let coq_True = constant "Logic" "True" -let coq_I = constant "Logic" "I" +let coq_True = lazy_init_constant ["Logic"] "True" +let coq_I = lazy_init_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" +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 @@ -216,15 +223,15 @@ let coq_eqdec_pattern = *) (* 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" "eq") -let coq_idT_ref = lazy (reference "Logic_Type" "identityT") -let coq_existS_ref = lazy (reference "Specif" "existS") -let coq_existT_ref = lazy (reference "Specif" "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") -let coq_sig_ref = lazy (reference "Specif" "sig") +let coq_eq_ref = lazy (init_reference ["Logic"] "eq") +let coq_eqT_ref = lazy (init_reference ["Logic"] "eq") +let coq_idT_ref = lazy (init_reference ["Logic_Type"] "identityT") +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") (* Pattern "(sig ?1 ?2)" *) let coq_sig_pattern = diff --git a/interp/coqlib.mli b/interp/coqlib.mli index dbe99e399..2c035cc34 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -19,6 +19,12 @@ open Pattern (*s This module collects the global references, constructions and patterns of the standard library used in ocaml files *) +(*s Some utilities, the first argument is used for error messages. + Must be used lazyly. s*) + +val gen_reference : string->string list -> string -> global_reference +val gen_constant : string->string list -> string -> constr + (*s Global references *) (* Modules *) diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 4468fd4d3..e397cd0cf 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -47,23 +47,9 @@ type morphism = let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c -let constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"Setoids"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id))) - -let global_constant dir s = - let dir = make_dirpath - (List.map id_of_string (List.rev ("Coq"::"Init"::dir))) in - let id = id_of_string s in - try - Declare.global_reference_in_absolute_module dir id - with Not_found -> - anomaly ("Setoid: cannot find "^(string_of_qualid (make_qualid dir id))) +let constant dir s = Coqlib.gen_constant "Setoid_replace" ("Setoids"::dir) s + +let global_constant dir s =Coqlib.gen_constant "Setoid_replace" ("Init"::dir) s let current_constant id = try |