aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2stdlib.ml37
-rw-r--r--src/tac2tactics.ml54
-rw-r--r--src/tac2tactics.mli27
-rw-r--r--src/tac2types.mli17
4 files changed, 98 insertions, 37 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 13f150381a..4bcbe69b07 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Locus
open Globnames
open Genredexpr
open Tac2expr
@@ -47,13 +46,11 @@ let to_constr_with_bindings v = match Value.to_tuple v with
| [| c; bnd |] -> (Value.to_constr c, to_bindings bnd)
| _ -> assert false
-let to_int_or_var i = Misctypes.ArgArg (Value.to_int i)
-
-let to_occurrences f = function
+let to_occurrences = function
| ValInt 0 -> AllOccurrences
-| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list f vl)
+| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list Value.to_int vl)
| ValInt 1 -> NoOccurrences
-| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list f vl)
+| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list Value.to_int vl)
| _ -> assert false
let to_hyp_location_flag v = match Value.to_int v with
@@ -66,11 +63,11 @@ let to_clause v = match Value.to_tuple v with
| [| hyps; concl |] ->
let cast v = match Value.to_tuple v with
| [| hyp; occ; flag |] ->
- ((to_occurrences to_int_or_var occ, Value.to_ident hyp), to_hyp_location_flag flag)
+ (Value.to_ident hyp, to_occurrences occ, to_hyp_location_flag flag)
| _ -> assert false
in
let hyps = Value.to_option (fun h -> Value.to_list cast h) hyps in
- { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
+ { onhyps = hyps; concl_occs = to_occurrences concl; }
| _ -> assert false
let to_red_flag v = match Value.to_tuple v with
@@ -87,10 +84,10 @@ let to_red_flag v = match Value.to_tuple v with
| _ -> assert false
let to_pattern_with_occs pat =
- to_pair Value.to_pattern (fun occ -> to_occurrences to_int_or_var occ) pat
+ to_pair Value.to_pattern to_occurrences pat
let to_constr_with_occs c =
- to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) c
+ to_pair Value.to_constr to_occurrences c
let rec to_intro_pattern v = match Value.to_block v with
| (0, [| b |]) -> IntroForthcoming (Value.to_bool b)
@@ -259,11 +256,11 @@ end
let () = define_prim1 "tac_generalize" begin fun cl ->
let cast v = match Value.to_tuple v with
| [| c; occs; na |] ->
- ((to_occurrences Value.to_int occs, Value.to_constr c), to_name na)
+ (Value.to_constr c, to_occurrences occs, to_name na)
| _ -> assert false
in
let cl = Value.to_list cast cl in
- Tactics.new_generalize_gen cl
+ Tac2tactics.generalize cl
end
let () = define_prim1 "tac_assert" begin fun ast ->
@@ -291,7 +288,7 @@ let () = define_prim3 "tac_set" begin fun ev p cl ->
Proofview.tclEVARMAP >>= fun sigma ->
thaw p >>= fun p ->
let (na, c) = to_pair to_name Value.to_constr p in
- Tactics.letin_pat_tac ev None na (sigma, c) cl
+ Tac2tactics.letin_pat_tac ev None na (sigma, c) cl
end
let () = define_prim5 "tac_remember" begin fun ev na c eqpat cl ->
@@ -326,12 +323,12 @@ end
let () = define_prim1 "tac_red" begin fun cl ->
let cl = to_clause cl in
- Tactics.reduce (Red false) cl
+ Tac2tactics.reduce (Red false) cl
end
let () = define_prim1 "tac_hnf" begin fun cl ->
let cl = to_clause cl in
- Tactics.reduce Hnf cl
+ Tac2tactics.reduce Hnf cl
end
let () = define_prim3 "tac_simpl" begin fun flags where cl ->
@@ -360,7 +357,7 @@ let () = define_prim2 "tac_lazy" begin fun flags cl ->
end
let () = define_prim2 "tac_unfold" begin fun refs cl ->
- let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
+ let map v = to_pair Value.to_reference to_occurrences v in
let refs = Value.to_list map refs in
let cl = to_clause cl in
Tac2tactics.unfold refs cl
@@ -369,7 +366,7 @@ end
let () = define_prim2 "tac_fold" begin fun args cl ->
let args = Value.to_list Value.to_constr args in
let cl = to_clause cl in
- Tactics.reduce (Fold args) cl
+ Tac2tactics.reduce (Fold args) cl
end
let () = define_prim2 "tac_pattern" begin fun where cl ->
@@ -442,7 +439,7 @@ let () = define_red2 "eval_lazy" begin fun flags c ->
end
let () = define_red2 "eval_unfold" begin fun refs c ->
- let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
+ let map v = to_pair Value.to_reference to_occurrences v in
let refs = Value.to_list map refs in
let c = Value.to_constr c in
Tac2tactics.eval_unfold refs c
@@ -455,7 +452,7 @@ let () = define_red2 "eval_fold" begin fun args c ->
end
let () = define_red2 "eval_pattern" begin fun where c ->
- let where = Value.to_list (fun p -> to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) p) where in
+ let where = Value.to_list (fun p -> to_pair Value.to_constr to_occurrences p) where in
let c = Value.to_constr c in
Tac2tactics.eval_pattern where c
end
@@ -569,7 +566,7 @@ end
let () = define_prim1 "tac_symmetry" begin fun cl ->
let cl = to_clause cl in
- Tactics.intros_symmetry cl
+ Tac2tactics.symmetry cl
end
let () = define_prim2 "tac_split" begin fun ev bnd ->
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 42916a9578..b55bd5c1b8 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -67,6 +67,23 @@ and mk_or_and_intro_pattern = function
let mk_intro_patterns ipat = List.map mk_intro_pattern ipat
+let mk_occurrences f = function
+| AllOccurrences -> Locus.AllOccurrences
+| AllOccurrencesBut l -> Locus.AllOccurrencesBut (List.map f l)
+| NoOccurrences -> Locus.NoOccurrences
+| OnlyOccurrences l -> Locus.OnlyOccurrences (List.map f l)
+
+let mk_occurrences_expr occ =
+ mk_occurrences (fun i -> Misctypes.ArgArg i) occ
+
+let mk_hyp_location (id, occs, h) =
+ ((mk_occurrences_expr occs, id), h)
+
+let mk_clause cl = {
+ Locus.onhyps = Option.map (fun l -> List.map mk_hyp_location l) cl.onhyps;
+ Locus.concl_occs = mk_occurrences_expr cl.concl_occs;
+}
+
let intros_patterns ev ipat =
let ipat = mk_intro_patterns ipat in
Tactics.intro_patterns ev ipat
@@ -93,6 +110,7 @@ let mk_destruction_arg = function
let mk_induction_clause (arg, eqn, as_, occ) =
let eqn = Option.map (fun ipat -> Loc.tag @@ mk_intro_pattern_naming ipat) eqn in
let as_ = Option.map (fun ipat -> Loc.tag @@ mk_or_and_intro_pattern ipat) as_ in
+ let occ = Option.map mk_clause occ in
((None, mk_destruction_arg arg), (eqn, as_), occ)
let induction_destruct isrec ev (ic : induction_clause list) using =
@@ -105,6 +123,11 @@ let elim ev c copt =
let copt = Option.map mk_with_bindings copt in
Tactics.elim ev None c copt
+let generalize pl =
+ let mk_occ occs = mk_occurrences (fun i -> i) occs in
+ let pl = List.map (fun (c, occs, na) -> (mk_occ occs, c), na) pl in
+ Tactics.new_generalize_gen pl
+
let general_case_analysis ev c =
let c = mk_with_bindings c in
Tactics.general_case_analysis ev None c
@@ -131,9 +154,14 @@ let rewrite ev rw cl by =
(Option.default true orient, repeat, None, delayed_of_tactic c)
in
let rw = List.map map_rw rw in
+ let cl = mk_clause cl in
let by = Option.map (fun tac -> Tacticals.New.tclCOMPLETE tac, Equality.Naive) by in
Equality.general_multi_rewrite ev rw cl by
+let symmetry cl =
+ let cl = mk_clause cl in
+ Tactics.intros_symmetry cl
+
let forward fst tac ipat c =
let ipat = Option.map mk_intro_pattern ipat in
Tactics.forward fst tac ipat c
@@ -148,6 +176,7 @@ let assert_ = function
let letin_pat_tac ev ipat na c cl =
let ipat = Option.map (fun (b, ipat) -> (b, Loc.tag @@ mk_intro_pattern_naming ipat)) ipat in
+ let cl = mk_clause cl in
Tactics.letin_pat_tac ev ipat na c cl
(** Ltac interface treats differently global references than other term
@@ -155,9 +184,9 @@ let letin_pat_tac ev ipat na c cl =
Instead, we parse indifferently any pattern and dispatch when the tactic is
called. *)
let map_pattern_with_occs (pat, occ) = match pat with
-| Pattern.PRef (ConstRef cst) -> (occ, Inl (EvalConstRef cst))
-| Pattern.PRef (VarRef id) -> (occ, Inl (EvalVarRef id))
-| _ -> (occ, Inr pat)
+| Pattern.PRef (ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst))
+| Pattern.PRef (VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id))
+| _ -> (mk_occurrences_expr occ, Inr pat)
let get_evaluable_reference = function
| VarRef id -> Proofview.tclUNIT (EvalVarRef id)
@@ -167,44 +196,57 @@ let get_evaluable_reference = function
Nametab.pr_global_env Id.Set.empty r ++ spc () ++
str "to an evaluable reference.")
+let reduce r cl =
+ let cl = mk_clause cl in
+ Tactics.reduce r cl
+
let simpl flags where cl =
let where = Option.map map_pattern_with_occs where in
+ let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Simpl (flags, where)) cl
let cbv flags cl =
+ let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Cbv flags) cl
let cbn flags cl =
+ let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Cbn flags) cl
let lazy_ flags cl =
+ let cl = mk_clause cl in
Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
let flags = { flags with rConst } in
Tactics.reduce (Lazy flags) cl
let unfold occs cl =
+ let cl = mk_clause cl in
let map (gr, occ) =
+ let occ = mk_occurrences_expr occ in
get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
in
Proofview.Monad.List.map map occs >>= fun occs ->
Tactics.reduce (Unfold occs) cl
let pattern where cl =
- let where = List.map (fun (c, occ) -> (occ, c)) where in
+ let where = List.map (fun (c, occ) -> (mk_occurrences_expr occ, c)) where in
+ let cl = mk_clause cl in
Tactics.reduce (Pattern where) cl
let vm where cl =
let where = Option.map map_pattern_with_occs where in
+ let cl = mk_clause cl in
Tactics.reduce (CbvVm where) cl
let native where cl =
let where = Option.map map_pattern_with_occs where in
+ let cl = mk_clause cl in
Tactics.reduce (CbvNative where) cl
let eval_fun red c =
@@ -244,6 +286,7 @@ let eval_lazy flags c =
let eval_unfold occs c =
let map (gr, occ) =
+ let occ = mk_occurrences_expr occ in
get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
in
Proofview.Monad.List.map map occs >>= fun occs ->
@@ -253,7 +296,7 @@ let eval_fold cl c =
eval_fun (Fold cl) c
let eval_pattern where c =
- let where = List.map (fun (pat, occ) -> (occ, pat)) where in
+ let where = List.map (fun (pat, occ) -> (mk_occurrences_expr occ, pat)) where in
eval_fun (Pattern where) c
let eval_vm where c =
@@ -303,6 +346,7 @@ let injection ev ipat arg =
let autorewrite ~all by ids cl =
let conds = if all then Some Equality.AllMatches else None in
let ids = List.map Id.to_string ids in
+ let cl = mk_clause cl in
match by with
| None -> Autorewrite.auto_multi_rewrite ?conds ids cl
| Some by -> Autorewrite.auto_multi_rewrite_with ?conds by ids cl
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 842b09c22f..3d64e7ec8c 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Locus
open Globnames
open Tac2expr
open EConstr
@@ -31,6 +30,8 @@ val elim : evars_flag -> constr_with_bindings -> constr_with_bindings option ->
val general_case_analysis : evars_flag -> constr_with_bindings -> unit tactic
+val generalize : (constr * occurrences * Name.t) list -> unit tactic
+
val constructor_tac : evars_flag -> int option -> int -> bindings -> unit tactic
val left_with_bindings : evars_flag -> bindings -> unit tactic
@@ -40,6 +41,8 @@ val split_with_bindings : evars_flag -> bindings -> unit tactic
val rewrite :
evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
+val symmetry : clause -> unit tactic
+
val forward : bool -> unit tactic option option ->
intro_pattern option -> constr -> unit tactic
@@ -48,8 +51,10 @@ val assert_ : assertion -> unit tactic
val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option ->
Name.t -> (Evd.evar_map * constr) -> clause -> unit tactic
+val reduce : Redexpr.red_expr -> clause -> unit tactic
+
val simpl : global_reference glob_red_flag ->
- (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+ (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
val cbv : global_reference glob_red_flag -> clause -> unit tactic
@@ -57,20 +62,20 @@ val cbn : global_reference glob_red_flag -> clause -> unit tactic
val lazy_ : global_reference glob_red_flag -> clause -> unit tactic
-val unfold : (global_reference * occurrences_expr) list -> clause -> unit tactic
+val unfold : (global_reference * occurrences) list -> clause -> unit tactic
-val pattern : (constr * occurrences_expr) list -> clause -> unit tactic
+val pattern : (constr * occurrences) list -> clause -> unit tactic
-val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+val vm : (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
-val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+val native : (Pattern.constr_pattern * occurrences) option -> clause -> unit tactic
val eval_red : constr -> constr tactic
val eval_hnf : constr -> constr tactic
val eval_simpl : global_reference glob_red_flag ->
- (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+ (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
val eval_cbv : global_reference glob_red_flag -> constr -> constr tactic
@@ -78,15 +83,15 @@ val eval_cbn : global_reference glob_red_flag -> constr -> constr tactic
val eval_lazy : global_reference glob_red_flag -> constr -> constr tactic
-val eval_unfold : (global_reference * occurrences_expr) list -> constr -> constr tactic
+val eval_unfold : (global_reference * occurrences) list -> constr -> constr tactic
val eval_fold : constr list -> constr -> constr tactic
-val eval_pattern : (EConstr.t * occurrences_expr) list -> constr -> constr tactic
+val eval_pattern : (EConstr.t * occurrences) list -> constr -> constr tactic
-val eval_vm : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_vm : (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
-val eval_native : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+val eval_native : (Pattern.constr_pattern * occurrences) option -> constr -> constr tactic
val discriminate : evars_flag -> destruction_arg option -> unit tactic
diff --git a/src/tac2types.mli b/src/tac2types.mli
index 6845de8c7c..1cacbefc88 100644
--- a/src/tac2types.mli
+++ b/src/tac2types.mli
@@ -53,11 +53,26 @@ and or_and_intro_pattern =
| IntroOrPattern of intro_pattern list list
| IntroAndPattern of intro_pattern list
+type occurrences =
+| AllOccurrences
+| AllOccurrencesBut of int list
+| NoOccurrences
+| OnlyOccurrences of int list
+
+type hyp_location_flag = Locus.hyp_location_flag =
+| InHyp | InHypTypeOnly | InHypValueOnly
+
+type hyp_location = Id.t * occurrences * hyp_location_flag
+
+type clause =
+ { onhyps : hyp_location list option;
+ concl_occs : occurrences }
+
type induction_clause =
destruction_arg *
intro_pattern_naming option *
or_and_intro_pattern option *
- Locus.clause option
+ clause option
type multi = Misctypes.multi =
| Precisely of int
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 08:50:09 +0000