summaryrefslogtreecommitdiff
path: root/plugins/subtac/subtac_utils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac/subtac_utils.ml')
-rw-r--r--plugins/subtac/subtac_utils.ml127
1 files changed, 64 insertions, 63 deletions
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 06a80f68..689b110f 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -1,3 +1,5 @@
+(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
+
open Evd
open Libnames
open Coqlib
@@ -18,14 +20,14 @@ let utils_module = "Utils"
let fixsub_module = subtac_dir @ [fix_sub_module]
let utils_module = subtac_dir @ [utils_module]
let tactics_module = subtac_dir @ ["Tactics"]
-let init_constant dir s = gen_constant contrib_name dir s
-let init_reference dir s = gen_reference contrib_name dir s
+let init_constant dir s () = gen_constant contrib_name dir s
+let init_reference dir s () = gen_reference contrib_name dir s
-let fixsub = lazy (init_constant fixsub_module "Fix_sub")
-let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
-let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
+let fixsub = init_constant fixsub_module "Fix_sub"
+let ex_pi1 = init_constant utils_module "ex_pi1"
+let ex_pi2 = init_constant utils_module "ex_pi2"
-let make_ref l s = lazy (init_reference l s)
+let make_ref l s = init_reference l s
let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
let acc_ref = make_ref ["Init";"Wf"] "Acc"
let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv"
@@ -41,68 +43,67 @@ let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
let build_sig () =
- { proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
- proj2 = init_constant ["Init"; "Specif"] "proj2_sig";
- elim = init_constant ["Init"; "Specif"] "sig_rec";
- intro = init_constant ["Init"; "Specif"] "exist";
- typ = init_constant ["Init"; "Specif"] "sig" }
+ { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" ();
+ proj2 = init_constant ["Init"; "Specif"] "proj2_sig" ();
+ elim = init_constant ["Init"; "Specif"] "sig_rec" ();
+ intro = init_constant ["Init"; "Specif"] "exist" ();
+ typ = init_constant ["Init"; "Specif"] "sig" () }
-let sig_ = lazy (build_sig ())
+let sig_ = build_sig
-let fix_proto = lazy (init_constant tactics_module "fix_proto")
+let fix_proto = init_constant tactics_module "fix_proto"
let fix_proto_ref () =
match Nametab.global (make_ref "Program.Tactics.fix_proto") with
| ConstRef c -> c
| _ -> assert false
-let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
-let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
-let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect")
-let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
-let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
-let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
+let eq_ind = init_constant ["Init"; "Logic"] "eq"
+let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
+let eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
+let eq_refl = init_constant ["Init"; "Logic"] "refl_equal"
+let eq_ind_ref = init_reference ["Init"; "Logic"] "eq"
+let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal"
-let not_ref = lazy (init_constant ["Init"; "Logic"] "not")
+let not_ref = init_constant ["Init"; "Logic"] "not"
-let and_typ = lazy (Coqlib.build_coq_and ())
+let and_typ = Coqlib.build_coq_and
-let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
-let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
-let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
-let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
+let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep"
+let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec"
+let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep"
+let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"
let jmeq_ind =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq")
+ init_constant ["Logic";"JMeq"] "JMeq"
+
let jmeq_rec =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq_rec")
+ init_constant ["Logic";"JMeq"] "JMeq_rec"
+
let jmeq_refl =
- lazy (check_required_library ["Coq";"Logic";"JMeq"];
- init_constant ["Logic";"JMeq"] "JMeq_refl")
+ init_constant ["Logic";"JMeq"] "JMeq_refl"
-let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
-let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
+let ex_ind = init_constant ["Init"; "Logic"] "ex"
+let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"
-let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
-let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
+let proj1 = init_constant ["Init"; "Logic"] "proj1"
+let proj2 = init_constant ["Init"; "Logic"] "proj2"
-let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
-let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
-let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
-let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
-let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
+let boolind = init_constant ["Init"; "Datatypes"] "bool"
+let sumboolind = init_constant ["Init"; "Specif"] "sumbool"
+let natind = init_constant ["Init"; "Datatypes"] "nat"
+let intind = init_constant ["ZArith"; "binint"] "Z"
+let existSind = init_constant ["Init"; "Specif"] "sigS"
-let existS = lazy (build_sigma_type ())
+let existS = build_sigma_type
-let prod = lazy (build_prod ())
+let prod = build_prod
(* orders *)
-let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
-let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
-let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
-let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
+let well_founded = init_constant ["Init"; "Wf"] "well_founded"
+let fix = init_constant ["Init"; "Wf"] "Fix"
+let acc = init_constant ["Init"; "Wf"] "Acc"
+let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv"
let extconstr = Constrextern.extern_constr true (Global.env ())
let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
@@ -151,8 +152,8 @@ let wf_relations = Hashtbl.create 10
let std_relations () =
let add k v = Hashtbl.add wf_relations k v in
- add (init_constant ["Init"; "Peano"] "lt")
- (lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
+ add (init_constant ["Init"; "Peano"] "lt" ())
+ (init_constant ["Arith"; "Wf_nat"] "lt_wf")
let std_relations = Lazy.lazy_from_fun std_relations
@@ -226,7 +227,6 @@ let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixp
open Tactics
open Tacticals
-let id x = x
let filter_map f l =
let rec aux acc = function
hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
@@ -257,51 +257,51 @@ let build_dependent_sum l =
(fun typ ->
let tex = mkLambda (Name n, t, typ) in
conttype
- (mkApp (Lazy.force ex_ind, [| t; tex |])))
+ (mkApp (ex_ind (), [| t; tex |])))
in
aux (mkVar n :: names) conttac conttype tl
| (n, t) :: [] ->
(conttac intros, conttype t)
| [] -> raise (Invalid_argument "build_dependent_sum")
- in aux [] id id (List.rev l)
+ in aux [] identity identity (List.rev l)
open Proof_type
open Tacexpr
let mkProj1 a b c =
- mkApp (Lazy.force proj1, [| a; b; c |])
+ mkApp (delayed_force proj1, [| a; b; c |])
let mkProj2 a b c =
- mkApp (Lazy.force proj2, [| a; b; c |])
+ mkApp (delayed_force proj2, [| a; b; c |])
let mk_ex_pi1 a b c =
- mkApp (Lazy.force ex_pi1, [| a; b; c |])
+ mkApp (delayed_force ex_pi1, [| a; b; c |])
let mk_ex_pi2 a b c =
- mkApp (Lazy.force ex_pi2, [| a; b; c |])
+ mkApp (delayed_force ex_pi2, [| a; b; c |])
let mkSubset name typ prop =
- mkApp ((Lazy.force sig_).typ,
+ mkApp ((delayed_force sig_).typ,
[| typ; mkLambda (name, typ, prop) |])
-let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |])
let unsafe_fold_right f = function
hd :: tl -> List.fold_right f tl hd
| [] -> raise (Invalid_argument "unsafe_fold_right")
let mk_conj l =
- let conj_typ = Lazy.force and_typ in
+ let conj_typ = delayed_force and_typ in
unsafe_fold_right
(fun c conj ->
mkApp (conj_typ, [| c ; conj |]))
l
let mk_not c =
- let notc = Lazy.force not_ref in
+ let notc = delayed_force not_ref in
mkApp (notc, [| c |])
let and_tac l hook =
@@ -336,7 +336,7 @@ let destruct_ex ext ex =
match kind_of_term c with
App (f, args) ->
(match kind_of_term f with
- Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
+ Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
let (dom, rng) =
try (args.(0), args.(1))
with _ -> assert(false)
@@ -477,6 +477,7 @@ let pr_evar_map evd =
let contrib_tactics_path =
make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
+
let tactics_tac s =
lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 21:41:56 +0000