aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml9
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/ftactic.ml106
-rw-r--r--tactics/ftactic.mli79
-rw-r--r--tactics/geninterp.ml35
-rw-r--r--tactics/geninterp.mli27
-rw-r--r--tactics/taccoerce.ml34
-rw-r--r--tactics/taccoerce.mli4
-rw-r--r--tactics/tactics.mllib2
9 files changed, 27 insertions, 273 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fc6ff03b4b..6b58baa997 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -156,11 +156,16 @@ let conclPattern concl pat tac =
constr_bindings env sigma >>= fun constr_bindings ->
let open Genarg in
let open Geninterp in
- let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in
+ let inj c = match val_tag (topwit Constrarg.wit_constr) with
+ | Val.Base tag -> Val.Dyn (tag, c)
+ | _ -> assert false
+ in
let fold id c accu = Id.Map.add id (inj c) accu in
let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in
let ist = { lfun; extra = TacStore.empty } in
- Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
+ match tac with
+ | GenArg (Glbwit wit, tac) ->
+ Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
end }
(***********************************************************)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4816f8a452..950eeef520 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -106,9 +106,9 @@ let one_base general_rewrite_maybe_in tac_main bas =
let lrul = List.map (fun h ->
let tac = match h.rew_tac with
| None -> Proofview.tclUNIT ()
- | Some tac ->
+ | Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) ->
let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
- Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ())
+ Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ())
in
(h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in
Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) ->
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
deleted file mode 100644
index 588709873e..0000000000
--- a/tactics/ftactic.ml
+++ /dev/null
@@ -1,106 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Proofview.Notations
-
-(** Focussing tactics *)
-
-type 'a focus =
-| Uniform of 'a
-| Depends of 'a list
-
-(** Type of tactics potentially goal-dependent. If it contains a [Depends],
- then the length of the inner list is guaranteed to be the number of
- currently focussed goals. Otherwise it means the tactic does not depend
- on the current set of focussed goals. *)
-type 'a t = 'a focus Proofview.tactic
-
-let return (x : 'a) : 'a t = Proofview.tclUNIT (Uniform x)
-
-let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
-| Uniform x -> f x
-| Depends l ->
- let f arg = f arg >>= function
- | Uniform x ->
- (** We dispatch the uniform result on each goal under focus, as we know
- that the [m] argument was actually dependent. *)
- Proofview.Goal.goals >>= fun l ->
- let ans = List.map (fun _ -> x) l in
- Proofview.tclUNIT ans
- | Depends l -> Proofview.tclUNIT l
- in
- Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
- Proofview.tclUNIT (Depends (List.concat l))
-
-let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
-let set_sigma r =
- let Sigma.Sigma (ans, sigma, _) = r in
- Proofview.Unsafe.tclEVARS (Sigma.to_evar_map sigma) >>= fun () -> ans
-
-let nf_enter f =
- bind goals
- (fun gl ->
- gl >>= fun gl ->
- Proofview.Goal.normalize gl >>= fun nfgl ->
- Proofview.V82.wrap_exceptions (fun () -> f.enter nfgl))
-
-let nf_s_enter f =
- bind goals
- (fun gl ->
- gl >>= fun gl ->
- Proofview.Goal.normalize gl >>= fun nfgl ->
- Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter nfgl)))
-
-let enter f =
- bind goals
- (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f.enter gl))
-
-let s_enter f =
- bind goals
- (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> set_sigma (f.s_enter gl)))
-
-let with_env t =
- t >>= function
- | Uniform a ->
- Proofview.tclENV >>= fun env -> Proofview.tclUNIT (Uniform (env,a))
- | Depends l ->
- Proofview.Goal.goals >>= fun gs ->
- Proofview.Monad.(List.map (map Proofview.Goal.env) gs) >>= fun envs ->
- Proofview.tclUNIT (Depends (List.combine envs l))
-
-let lift (type a) (t:a Proofview.tactic) : a t =
- Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x))
-
-(** If the tactic returns unit, we can focus on the goals if necessary. *)
-let run m k = m >>= function
-| Uniform v -> k v
-| Depends l ->
- let tacs = List.map k l in
- Proofview.tclDISPATCH tacs
-
-let (>>=) = bind
-
-let (<*>) = fun m n -> bind m (fun () -> n)
-
-module Self =
-struct
- type 'a t = 'a focus Proofview.tactic
- let return = return
- let (>>=) = bind
- let (>>) = (<*>)
- let map f x = x >>= fun a -> return (f a)
-end
-
-module Ftac = Monad.Make(Self)
-module List = Ftac.List
-
-module Notations =
-struct
- let (>>=) = bind
- let (<*>) = fun m n -> bind m (fun () -> n)
-end
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
deleted file mode 100644
index 19041f1698..0000000000
--- a/tactics/ftactic.mli
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Proofview.Notations
-
-(** Potentially focussing tactics *)
-
-type +'a focus
-
-type +'a t = 'a focus Proofview.tactic
-(** The type of focussing tactics. A focussing tactic is like a normal tactic,
- except that it is able to remember it have entered a goal. Whenever this is
- the case, each subsequent effect of the tactic is dispatched on the
- focussed goals. This is a monad. *)
-
-(** {5 Monadic interface} *)
-
-val return : 'a -> 'a t
-(** The unit of the monad. *)
-
-val bind : 'a t -> ('a -> 'b t) -> 'b t
-(** The bind of the monad. *)
-
-(** {5 Operations} *)
-
-val lift : 'a Proofview.tactic -> 'a t
-(** Transform a tactic into a focussing tactic. The resulting tactic is not
- focussed. *)
-
-val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
-(** Given a continuation producing a tactic, evaluates the focussing tactic. If
- the tactic has not focussed, then the continuation is evaluated once.
- Otherwise it is called in each of the currently focussed goals. *)
-
-(** {5 Focussing} *)
-
-val nf_enter : ([ `NF ], 'a t) enter -> 'a t
-(** Enter a goal. The resulting tactic is focussed. *)
-
-val enter : ([ `LZ ], 'a t) enter -> 'a t
-(** Enter a goal, without evar normalization. The resulting tactic is
- focussed. *)
-
-val s_enter : ([ `LZ ], 'a t) s_enter -> 'a t
-(** Enter a goal and put back an evarmap. The resulting tactic is focussed. *)
-
-val nf_s_enter : ([ `NF ], 'a t) s_enter -> 'a t
-(** Enter a goal, without evar normalization and put back an evarmap. The
- resulting tactic is focussed. *)
-
-val with_env : 'a t -> (Environ.env*'a) t
-(** [with_env t] returns, in addition to the return type of [t], an
- environment, which is the global environment if [t] does not focus on
- goals, or the local goal environment if [t] focuses on goals. *)
-
-(** {5 Notations} *)
-
-val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
-(** Notation for {!bind}. *)
-
-val (<*>) : unit t -> 'a t -> 'a t
-(** Sequence. *)
-
-(** {5 List operations} *)
-
-module List : Monad.ListS with type 'a t := 'a t
-
-(** {5 Notations} *)
-
-module Notations :
-sig
- val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
- val (<*>) : unit t -> 'a t -> 'a t
-end
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
deleted file mode 100644
index 0080758000..0000000000
--- a/tactics/geninterp.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Genarg
-
-module TacStore = Store.Make(struct end)
-
-type interp_sign = {
- lfun : Val.t Id.Map.t;
- extra : TacStore.t }
-
-type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
-
-module InterpObj =
-struct
- type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun
- let name = "interp"
- let default _ = None
-end
-
-module Interp = Register(InterpObj)
-
-let interp = Interp.obj
-let register_interp0 = Interp.register0
-
-let generic_interp ist (GenArg (Glbwit wit, v)) =
- let open Ftactic.Notations in
- interp wit ist v >>= fun ans ->
- Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli
deleted file mode 100644
index 0992db7a29..0000000000
--- a/tactics/geninterp.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Interpretation functions for generic arguments. *)
-
-open Names
-open Genarg
-
-module TacStore : Store.S
-
-type interp_sign = {
- lfun : Val.t Id.Map.t;
- extra : TacStore.t }
-
-type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
-
-val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun
-
-val generic_interp : (glob_generic_argument, Val.t) interp_fun
-
-val register_interp0 :
- ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 358f6d6468..d53c1cc04a 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -14,15 +14,25 @@ open Misctypes
open Genarg
open Stdarg
open Constrarg
+open Geninterp
exception CannotCoerceTo of string
let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
- Genarg.create_arg "constr_context"
+ let wit = Genarg.create_arg "constr_context" in
+ let () = register_val0 wit None in
+ wit
(* includes idents known to be bound and references *)
let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
- Genarg.create_arg "constr_under_binders"
+ let wit = Genarg.create_arg "constr_under_binders" in
+ let () = register_val0 wit None in
+ wit
+
+(** All the types considered here are base types *)
+let val_tag wit = match val_tag wit with
+| Val.Base t -> t
+| _ -> assert false
let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
let Val.Dyn (t, _) = v in
@@ -30,7 +40,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w
| None -> false
| Some Refl -> true
-let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+let prj : type a. a Val.typ -> Val.t -> a option = fun t v ->
let Val.Dyn (t', x) = v in
match Val.eq t t' with
| None -> None
@@ -74,23 +84,11 @@ let to_int v =
Some (out_gen (topwit wit_int) v)
else None
-let to_list v =
- let v = normalize v in
- let Val.Dyn (tag, v) = v in
- match tag with
- | Val.List t -> Some (List.map (fun x -> Val.Dyn (t, x)) v)
- | _ -> None
-
-let of_list t v = Val.Dyn (Val.List t, v)
+let to_list v = prj Val.typ_list v
-let to_option v =
- let v = normalize v in
- let Val.Dyn (tag, v) = v in
- match tag with
- | Val.Opt t -> Some (Option.map (fun x -> Val.Dyn (t, x)) v)
- | _ -> None
+let to_option v = prj Val.typ_opt v
-let of_option t v = Val.Dyn (Val.Opt t, v)
+let to_pair v = prj Val.typ_pair v
end
diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli
index 87137fd2e7..7a963f95f3 100644
--- a/tactics/taccoerce.mli
+++ b/tactics/taccoerce.mli
@@ -12,6 +12,7 @@ open Term
open Misctypes
open Pattern
open Genarg
+open Geninterp
(** Coercions from highest level generic arguments to actual data used by Ltac
interpretation. Those functions examinate dynamic types and try to return
@@ -41,9 +42,8 @@ sig
val of_int : int -> t
val to_int : t -> int option
val to_list : t -> t list option
- val of_list : 'a Val.tag -> 'a list -> t
val to_option : t -> t option option
- val of_option : 'a Val.tag -> 'a option -> t
+ val to_pair : t -> (t * t) option
end
(** {5 Coercion functions} *)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index ab8069225d..48722f655a 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,3 @@
-Ftactic
-Geninterp
Dnet
Dn
Btermdn
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-11 05:19:37 +0000