aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/engine.mllib2
-rw-r--r--engine/ftactic.ml106
-rw-r--r--engine/ftactic.mli79
-rw-r--r--engine/geninterp.ml98
-rw-r--r--engine/geninterp.mli67
5 files changed, 352 insertions, 0 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 70b74edca3..9ce5af8195 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -7,3 +7,5 @@ Sigma
Proofview_monad
Evarutil
Proofview
+Ftactic
+Geninterp
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
new file mode 100644
index 0000000000..588709873e
--- /dev/null
+++ b/engine/ftactic.ml
@@ -0,0 +1,106 @@
+(************************************************************************)
+(* 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/engine/ftactic.mli b/engine/ftactic.mli
new file mode 100644
index 0000000000..19041f1698
--- /dev/null
+++ b/engine/ftactic.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(* 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/engine/geninterp.ml b/engine/geninterp.ml
new file mode 100644
index 0000000000..45b0aa2316
--- /dev/null
+++ b/engine/geninterp.ml
@@ -0,0 +1,98 @@
+(************************************************************************)
+(* 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)
+
+(** Dynamic toplevel values *)
+
+module ValT = Dyn.Make(struct end)
+
+module Val =
+struct
+
+ type 'a typ = 'a ValT.tag
+
+ type _ tag =
+ | Base : 'a typ -> 'a tag
+ | List : 'a tag -> 'a list tag
+ | Opt : 'a tag -> 'a option tag
+ | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+ type t = Dyn : 'a typ * 'a -> t
+
+ let eq = ValT.eq
+ let repr = ValT.repr
+ let create = ValT.create
+
+ let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t)
+
+ let typ_list = ValT.create "list"
+ let typ_opt = ValT.create "option"
+ let typ_pair = ValT.create "pair"
+
+ let rec inject : type a. a tag -> a -> t = fun tag x -> match tag with
+ | Base t -> Dyn (t, x)
+ | List tag -> Dyn (typ_list, List.map (fun x -> inject tag x) x)
+ | Opt tag -> Dyn (typ_opt, Option.map (fun x -> inject tag x) x)
+ | Pair (tag1, tag2) ->
+ Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x)))
+
+end
+
+module ValReprObj =
+struct
+ type ('raw, 'glb, 'top) obj = 'top Val.tag
+ let name = "valrepr"
+ let default _ = None
+end
+
+module ValRepr = Register(ValReprObj)
+
+let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
+| ListArg t -> Val.List (val_tag t)
+| OptArg t -> Val.Opt (val_tag t)
+| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2)
+| ExtraArg s -> ValRepr.obj (ExtraArg s)
+
+let val_tag = function Topwit t -> val_tag t
+
+let register_val0 wit tag =
+ let tag = match tag with
+ | None ->
+ let name = match wit with
+ | ExtraArg s -> ArgT.repr s
+ | _ -> assert false
+ in
+ Val.Base (Val.create name)
+ | Some tag -> tag
+ in
+ ValRepr.register0 wit tag
+
+(** Interpretation functions *)
+
+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, Val.t) interp_fun
+ let name = "interp"
+ let default _ = None
+end
+
+module Interp = Register(InterpObj)
+
+let interp = Interp.obj
+
+let register_interp0 = Interp.register0
diff --git a/engine/geninterp.mli b/engine/geninterp.mli
new file mode 100644
index 0000000000..42e1e3784c
--- /dev/null
+++ b/engine/geninterp.mli
@@ -0,0 +1,67 @@
+(************************************************************************)
+(* 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
+
+(** {6 Dynamic toplevel values} *)
+
+module Val :
+sig
+ type 'a typ
+
+ val create : string -> 'a typ
+
+ type _ tag =
+ | Base : 'a typ -> 'a tag
+ | List : 'a tag -> 'a list tag
+ | Opt : 'a tag -> 'a option tag
+ | Pair : 'a tag * 'b tag -> ('a * 'b) tag
+
+ type t = Dyn : 'a typ * 'a -> t
+
+ val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option
+ val repr : 'a typ -> string
+ val pr : 'a typ -> Pp.std_ppcmds
+
+ val typ_list : t list typ
+ val typ_opt : t option typ
+ val typ_pair : (t * t) typ
+
+ val inject : 'a tag -> 'a -> t
+
+end
+(** Dynamic types for toplevel values. While the generic types permit to relate
+ objects at various levels of interpretation, toplevel values are wearing
+ their own type regardless of where they came from. This allows to use the
+ same runtime representation for several generic types. *)
+
+val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
+(** Retrieve the dynamic type associated to a toplevel genarg. *)
+
+val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit
+(** Register the representation of a generic argument. If no tag is given as
+ argument, a new fresh tag with the same name as the argument is associated
+ to the generic type. *)
+
+(** {6 Interpretation functions} *)
+
+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, Val.t) interp_fun
+
+val register_interp0 :
+ ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:06:10 +0000