From 5da0f107cb3332d5cd87fc352aef112f6b74fc97 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Apr 2016 16:31:01 +0200 Subject: Moving Ftactic and Geninterp to the engine folder. --- engine/engine.mllib | 2 + engine/ftactic.ml | 106 ++++++++++++++++++++++++++++++++++++++++++++++++++ engine/ftactic.mli | 79 +++++++++++++++++++++++++++++++++++++ engine/geninterp.ml | 35 +++++++++++++++++ engine/geninterp.mli | 27 +++++++++++++ tactics/ftactic.ml | 106 -------------------------------------------------- tactics/ftactic.mli | 79 ------------------------------------- tactics/geninterp.ml | 35 ----------------- tactics/geninterp.mli | 27 ------------- tactics/tactics.mllib | 2 - 10 files changed, 249 insertions(+), 249 deletions(-) create mode 100644 engine/ftactic.ml create mode 100644 engine/ftactic.mli create mode 100644 engine/geninterp.ml create mode 100644 engine/geninterp.mli delete mode 100644 tactics/ftactic.ml delete mode 100644 tactics/ftactic.mli delete mode 100644 tactics/geninterp.ml delete mode 100644 tactics/geninterp.mli 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 *) +(* 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 *) +(* '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..0080758000 --- /dev/null +++ b/engine/geninterp.ml @@ -0,0 +1,35 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '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/engine/geninterp.mli b/engine/geninterp.mli new file mode 100644 index 0000000000..0992db7a29 --- /dev/null +++ b/engine/geninterp.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '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/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 *) -(* 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 *) -(* '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 *) -(* '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 *) -(* '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/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 -- cgit v1.2.3 From 011ac2d7db53f0df2849985ef9cc044574c0ddb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Apr 2016 16:44:42 +0200 Subject: Switching to an untyped toplevel representation for Ltac values. --- engine/geninterp.ml | 2 +- lib/genarg.ml | 43 ++++++++++------------------- lib/genarg.mli | 12 ++++++--- ltac/tacinterp.ml | 75 +++++++++++++++++++++++---------------------------- ltac/tauto.ml | 2 +- printing/pptactic.ml | 47 +++++++++++++++++++++----------- tactics/auto.ml | 2 +- tactics/taccoerce.ml | 29 ++++++++++---------- tactics/taccoerce.mli | 2 ++ 9 files changed, 107 insertions(+), 107 deletions(-) diff --git a/engine/geninterp.ml b/engine/geninterp.ml index 0080758000..0d67213674 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -32,4 +32,4 @@ 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)) + Ftactic.return (Val.inject (val_tag (topwit wit)) ans) diff --git a/lib/genarg.ml b/lib/genarg.ml index ef0de89afb..3ff9afa601 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -36,38 +36,23 @@ struct | Opt : 'a tag -> 'a option tag | Pair : 'a tag * 'b tag -> ('a * 'b) tag - type t = Dyn : 'a tag * 'a -> t - - let rec eq : type a b. a tag -> b tag -> (a, b) CSig.eq option = - fun t1 t2 -> match t1, t2 with - | Base t1, Base t2 -> ValT.eq t1 t2 - | List t1, List t2 -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> Some Refl - end - | Opt t1, Opt t2 -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> Some Refl - end - | Pair (t1, u1), Pair (t2, u2) -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> - match eq u1 u2 with - | None -> None - | Some Refl -> Some Refl - end - | _ -> None + type t = Dyn : 'a typ * 'a -> t + let eq = ValT.eq let repr = ValT.repr - let rec pr : type a. a tag -> std_ppcmds = function - | Base t -> str (repr t) - | List t -> pr t ++ spc () ++ str "list" - | Opt t -> pr t ++ spc () ++ str "option" - | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")" + let rec pr : type a. a typ -> std_ppcmds = fun t -> str (repr t) + + let list_tag = ValT.create "list" + let opt_tag = ValT.create "option" + let pair_tag = 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 (list_tag, List.map (fun x -> inject tag x) x) + | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x) + | Pair (tag1, tag2) -> + Dyn (pair_tag, (inject tag1 (fst x), inject tag2 (snd x))) end diff --git a/lib/genarg.mli b/lib/genarg.mli index 93665fd45d..04113ae289 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -96,11 +96,17 @@ sig | Opt : 'a tag -> 'a option tag | Pair : 'a tag * 'b tag -> ('a * 'b) tag - type t = Dyn : 'a tag * 'a -> t + type t = Dyn : 'a typ * 'a -> t - val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option + val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option val repr : 'a typ -> string - val pr : 'a tag -> Pp.std_ppcmds + val pr : 'a typ -> Pp.std_ppcmds + + val list_tag : t list typ + val opt_tag : t option typ + val pair_tag : (t * t) typ + + val inject : 'a tag -> 'a -> t end (** Dynamic types for toplevel values. While the generic types permit to relate diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 9b41a276b9..90784f5e84 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -48,18 +48,27 @@ let ltac_trace_info = Tactic_debug.ltac_trace_info let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> let Val.Dyn (t, _) = v in - match Val.eq t (val_tag wit) with + let t' = match val_tag wit with + | Val.Base t' -> t' + | _ -> assert false (** not used in this module *) + in + match Val.eq t t' with | 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 | Some Refl -> Some x -let in_gen wit v = Val.Dyn (val_tag wit, v) -let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x +let in_gen wit v = Val.inject (val_tag wit) v +let out_gen wit v = + let t = match val_tag wit with + | Val.Base t -> t + | _ -> assert false (** not used in this module *) + in + match prj t v with None -> assert false | Some x -> x let val_tag wit = val_tag (topwit wit) @@ -152,47 +161,31 @@ module Value = struct let Val.Dyn (tag, _) = v in let tag = Val.pr tag in errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag - ++ str " while type " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.") + ++ str " while type " ++ Val.pr wit ++ str " was expected.") + + let unbox wit v ans = match ans with + | None -> cast_error wit v + | Some x -> x - let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> + let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with + | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.list_tag v (to_list v)) + | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.opt_tag v (to_option v)) + | Val.Pair (tag1, tag2) -> + let (x, y) = unbox Val.pair_tag v (to_pair v) in + (prj tag1 x, prj tag2 y) + | Val.Base t -> let Val.Dyn (t', x) = v in match Val.eq t t' with - | None -> None - | Some Refl -> Some x + | None -> cast_error t v + | Some Refl -> x - let try_prj wit v = match prj (val_tag wit) v with - | None -> cast_error wit v - | Some x -> x + let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with + | ExtraArg _ -> val_tag wit + | ListArg t -> Val.List (tag_of_arg t) + | OptArg t -> Val.Opt (tag_of_arg t) + | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) - let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c = - fun wit v -> match wit with - | ExtraArg _ -> try_prj wit v - | ListArg t -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.List tag -> - let map x = val_cast t (Val.Dyn (tag, x)) in - List.map map v - | _ -> cast_error wit (Val.Dyn (tag, v)) - end - | OptArg t -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.Opt tag -> - let map x = val_cast t (Val.Dyn (tag, x)) in - Option.map map v - | _ -> cast_error wit (Val.Dyn (tag, v)) - end - | PairArg (t1, t2) -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.Pair (tag1, tag2) -> - let (v1, v2) = v in - let v1 = Val.Dyn (tag1, v1) in - let v2 = Val.Dyn (tag2, v2) in - (val_cast t1 v1, val_cast t2 v2) - | _ -> cast_error wit (Val.Dyn (tag, v)) - end + let rec val_cast arg v = prj (tag_of_arg arg) v let cast (Topwit wit) v = val_cast wit v @@ -1574,7 +1567,7 @@ and interp_genarg ist x : Val.t Ftactic.t = interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q -> let p = Value.cast (topwit wit1) p in let q = Value.cast (topwit wit2) q in - Ftactic.return (Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q))) + Ftactic.return (Value.of_pair (val_tag wit1) (val_tag wit2) (p, q)) | ExtraArg s -> Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x) diff --git a/ltac/tauto.ml b/ltac/tauto.ml index a86fdb98a9..b0958b3948 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -256,7 +256,7 @@ let tauto_power_flags = { let with_flags flags _ ist = let f = (loc, Id.of_string "f") in let x = (loc, Id.of_string "x") in - let arg = Val.Dyn (val_tag (topwit wit_tauto_flags), flags) in + let arg = Val.inject (val_tag (topwit wit_tauto_flags)) flags in let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)]))) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7949bafcbb..018e29cd29 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -97,23 +97,38 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) - let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with - | Val.List tag -> - pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x - | Val.Opt tag -> pr_opt_no_spc (fun x -> pr_value lev (Val.Dyn (tag, x))) x - | Val.Pair (tag1, tag2) -> - str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++ - pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")" - | Val.Base t -> - let name = Val.repr t in - let default = str "<" ++ str name ++ str ">" in - match ArgT.name name with - | None -> default - | Some (ArgT.Any arg) -> - let wit = ExtraArg arg in - match Val.eq (val_tag (Topwit wit)) (Val.Base t) with + let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with + | None -> false + | Some _ -> true + + let unbox : type a. Val.t -> a Val.typ -> a= fun (Val.Dyn (tag, x)) t -> + match Val.eq tag t with + | None -> assert false + | Some Refl -> x + + let rec pr_value lev v : std_ppcmds = + if has_type v Val.list_tag then + pr_sequence (fun x -> pr_value lev x) (unbox v Val.list_tag) + else if has_type v Val.opt_tag then + pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.opt_tag) + else if has_type v Val.pair_tag then + let (v1, v2) = unbox v Val.pair_tag in + str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")" + else + let Val.Dyn (tag, x) = v in + let name = Val.repr tag in + let default = str "<" ++ str name ++ str ">" in + match ArgT.name name with | None -> default - | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + | Some (ArgT.Any arg) -> + let wit = ExtraArg arg in + match val_tag (Topwit wit) with + | Val.Base t -> + begin match Val.eq t tag with + | None -> default + | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + end + | _ -> default let pr_with_occurrences pr (occs,c) = match occs with diff --git a/tactics/auto.ml b/tactics/auto.ml index fc6ff03b4b..d7ce0d4c1a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -156,7 +156,7 @@ 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 = Val.inject (val_tag (topwit Constrarg.wit_constr)) c 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 diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 358f6d6468..298257e45d 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -24,13 +24,18 @@ let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) = let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = Genarg.create_arg "constr_under_binders" +(** 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 match Val.eq t (val_tag wit) with | 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 +79,17 @@ 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 to_list v = prj Val.list_tag v -let of_list t v = Val.Dyn (Val.List t, v) +let of_list t v = Val.Dyn (Val.list_tag, List.map (fun v -> Val.inject t v) 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.opt_tag v + +let of_option t v = Val.Dyn (Val.opt_tag, Option.map (fun v -> Val.inject t v) v) + +let to_pair v = prj Val.pair_tag v -let of_option t v = Val.Dyn (Val.Opt t, v) +let of_pair t1 t2 (v1, v2) = Val.Dyn (Val.pair_tag, (Val.inject t1 v1, Val.inject t2 v2)) end diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 87137fd2e7..75a3b347d6 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -44,6 +44,8 @@ sig 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 + val of_pair : 'a Val.tag -> 'b Val.tag -> ('a * 'b) -> t end (** {5 Coercion functions} *) -- cgit v1.2.3 From 8ad2627de29639b21473783195905dca6bb1c6ae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 Apr 2016 18:33:28 +0200 Subject: Getting rid of the Geninterp.generic_interp function. --- engine/geninterp.ml | 5 ----- engine/geninterp.mli | 2 -- ltac/rewrite.ml | 6 ++++-- ltac/tacinterp.ml | 3 ++- tactics/auto.ml | 4 +++- tactics/autorewrite.ml | 4 ++-- 6 files changed, 11 insertions(+), 13 deletions(-) diff --git a/engine/geninterp.ml b/engine/geninterp.ml index 0d67213674..be4011cb64 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -28,8 +28,3 @@ 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.inject (val_tag (topwit wit)) ans) diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 0992db7a29..0e7ed18471 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -21,7 +21,5 @@ 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/ltac/rewrite.ml b/ltac/rewrite.ml index 97b2393a8d..cd8ce7e87a 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -613,8 +613,10 @@ let solve_remaining_by env sigma holes by = (** Only solve independent holes *) let indep = List.map_filter map holes in let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in - let solve_tac = Geninterp.generic_interp ist tac in - let solve_tac = Ftactic.run solve_tac (fun _ -> Proofview.tclUNIT ()) in + let solve_tac = match tac with + | Genarg.GenArg (Genarg.Glbwit tag, tac) -> + Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ()) + in let solve_tac = Tacticals.New.tclCOMPLETE solve_tac in let solve sigma evk = let evi = diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 90784f5e84..b9d074a3dc 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1569,7 +1569,8 @@ and interp_genarg ist x : Val.t Ftactic.t = let q = Value.cast (topwit wit2) q in Ftactic.return (Value.of_pair (val_tag wit1) (val_tag wit2) (p, q)) | ExtraArg s -> - Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x) + Geninterp.interp wit ist x >>= fun x -> + Ftactic.return (in_gen (Topwit wit) x) (** returns [true] for genargs which have the same meaning independently of goals. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index d7ce0d4c1a..46f484bf06 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -160,7 +160,9 @@ let conclPattern concl pat tac = 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) -> -- cgit v1.2.3 From d2f0db714bd2d393423cf2dcb4ed37913029e052 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 Apr 2016 20:28:57 +0200 Subject: Simplifying the code of Tacinterp. --- ltac/tacinterp.ml | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index b9d074a3dc..6e76b19106 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1546,28 +1546,21 @@ and interp_genarg ist x : Val.t Ftactic.t = let GenArg (Glbwit wit, x) = x in match wit with | ListArg wit -> - let map x = - interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x -> - Ftactic.return (Value.cast (topwit wit) x) - in + let map x = interp_genarg ist (Genarg.in_gen (glbwit wit) x) in Ftactic.List.map map x >>= fun l -> - Ftactic.return (Value.of_list (val_tag wit) l) + Ftactic.return (Val.Dyn (Val.list_tag, l)) | OptArg wit -> - let ans = match x with - | None -> Ftactic.return (Value.of_option (val_tag wit) None) + begin match x with + | None -> Ftactic.return (Val.Dyn (Val.opt_tag, None)) | Some x -> interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x -> - let x = Value.cast (topwit wit) x in - Ftactic.return (Value.of_option (val_tag wit) (Some x)) - in - ans + Ftactic.return (Val.Dyn (Val.opt_tag, Some x)) + end | PairArg (wit1, wit2) -> let (p, q) = x in interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p -> interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q -> - let p = Value.cast (topwit wit1) p in - let q = Value.cast (topwit wit2) q in - Ftactic.return (Value.of_pair (val_tag wit1) (val_tag wit2) (p, q)) + Ftactic.return (Val.Dyn (Val.pair_tag, (p, q))) | ExtraArg s -> Geninterp.interp wit ist x >>= fun x -> Ftactic.return (in_gen (Topwit wit) x) -- cgit v1.2.3 From de4b9b68445d9f3e48da789404cbdfcd89214585 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 18 Apr 2016 14:39:34 +0200 Subject: Moving the Val module to Geninterp. --- dev/printers.mllib | 2 ++ dev/top_printers.ml | 4 +-- engine/geninterp.ml | 67 +++++++++++++++++++++++++++++++++++++++++ engine/geninterp.mli | 42 ++++++++++++++++++++++++++ grammar/argextend.ml4 | 12 +++----- interp/constrarg.ml | 42 +++++++++++++++----------- interp/constrarg.mli | 2 +- interp/stdarg.ml | 6 ++++ lib/genarg.ml | 58 ++--------------------------------- lib/genarg.mli | 38 ++--------------------- ltac/extraargs.mli | 2 +- ltac/extratactics.ml4 | 4 ++- ltac/tacenv.ml | 3 +- ltac/tacenv.mli | 1 + ltac/tacinterp.ml | 5 ++- ltac/tacinterp.mli | 4 +-- ltac/tauto.ml | 5 ++- plugins/decl_mode/decl_expr.mli | 2 +- plugins/quote/g_quote.ml4 | 2 +- plugins/setoid_ring/newring.mli | 4 +-- pretyping/pretyping.ml | 2 +- pretyping/pretyping.mli | 2 +- printing/pptactic.ml | 1 + printing/pptactic.mli | 1 + printing/pptacticsig.mli | 1 + tactics/taccoerce.ml | 9 ++++-- tactics/taccoerce.mli | 1 + 27 files changed, 186 insertions(+), 136 deletions(-) diff --git a/dev/printers.mllib b/dev/printers.mllib index 9f25ba55e7..5d10f54fb2 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -146,6 +146,8 @@ Typeclasses_errors Logic_monad Proofview_monad Proofview +Ftactic +Geninterp Typeclasses Detyping Indrec diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 29ea08e025..f9c1971a82 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -467,8 +467,8 @@ let pp_generic_argument arg = pp(str"") let prgenarginfo arg = - let Val.Dyn (tag, _) = arg in - let tpe = Val.pr tag in + let Geninterp.Val.Dyn (tag, _) = arg in + let tpe = Geninterp.Val.pr tag in (** FIXME *) (* try *) (* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) diff --git a/engine/geninterp.ml b/engine/geninterp.ml index be4011cb64..9e866f0cf8 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -11,6 +11,73 @@ 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 list_tag = ValT.create "list" + let opt_tag = ValT.create "option" + let pair_tag = 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 (list_tag, List.map (fun x -> inject tag x) x) + | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x) + | Pair (tag1, tag2) -> + Dyn (pair_tag, (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 } diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 0e7ed18471..3c87b25121 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -11,6 +11,48 @@ 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 list_tag : t list typ + val opt_tag : t option typ + val pair_tag : (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 = { diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index dca3e1656f..2618e5d896 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -88,6 +88,7 @@ let check_type prefix s = function | Some _ -> warning_redundant prefix s let declare_tactic_argument loc s (typ, f, g, h) cl = + let se = mlexpr_of_string s in let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with | `Uniform (typ, pr) -> let typ = get_type "" s typ in @@ -147,20 +148,15 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = | Some f -> <:expr< $lid:f$>> in let dyn = match typ with | None -> <:expr< None >> - | Some typ -> - if is_self s typ then <:expr< None >> - else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >> + | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >> in - let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in declare_str_items loc - [ <:str_item< - value ($lid:"wit_"^s$) = - let dyn = $dyn$ in - Genarg.make0 ?dyn $se$ >>; + [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>; <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; + <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>; make_extend loc s cl wit; <:str_item< do { Pptactic.declare_extra_genarg_pprule diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 46be0b8a1f..99f0a2da64 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -11,6 +11,12 @@ open Tacexpr open Term open Misctypes open Genarg +open Geninterp + +let make0 ?dyn name = + let wit = Genarg.make0 name in + let () = Geninterp.register_val0 wit dyn in + wit (** This is a hack for now, to break the dependency of Genarg on constr-related types. We should use dedicated functions someday. *) @@ -20,50 +26,50 @@ let loc_of_or_by_notation f = function | ByNotation (loc,s,_) -> loc let wit_int_or_var = - Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" + make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = - Genarg.make0 "intropattern" + make0 "intropattern" let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = - Genarg.make0 "tactic" + make0 "tactic" -let wit_ltac = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" +let wit_ltac = make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" let wit_ident = - Genarg.make0 "ident" + make0 "ident" let wit_var = - Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) "var" + make0 ~dyn:(val_tag (topwit wit_ident)) "var" -let wit_ref = Genarg.make0 "ref" +let wit_ref = make0 "ref" -let wit_quant_hyp = Genarg.make0 "quant_hyp" +let wit_quant_hyp = make0 "quant_hyp" let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = - Genarg.make0 "sort" + make0 "sort" let wit_constr = - Genarg.make0 "constr" + make0 "constr" let wit_constr_may_eval = - Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval" + make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval" -let wit_uconstr = Genarg.make0 "uconstr" +let wit_uconstr = make0 "uconstr" -let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" +let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = Genarg.make0 "constr_with_bindings" +let wit_constr_with_bindings = make0 "constr_with_bindings" -let wit_bindings = Genarg.make0 "bindings" +let wit_bindings = make0 "bindings" let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = - Genarg.make0 "hyp_location_flag" + make0 "hyp_location_flag" -let wit_red_expr = Genarg.make0 "redexpr" +let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = - Genarg.make0 "clause_dft_concl" + make0 "clause_dft_concl" (** Aliases *) diff --git a/interp/constrarg.mli b/interp/constrarg.mli index d38b1183c5..6407b61afd 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -69,7 +69,7 @@ val wit_red_expr : (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type +val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Geninterp.Val.t) genarg_type (** [wit_ltac] is subtly different from [wit_tactic]: they only change for their toplevel interpretation. The one of [wit_ltac] forces the tactic and diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 244cdd0a70..9e85dbaf38 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -7,6 +7,12 @@ (************************************************************************) open Genarg +open Geninterp + +let make0 ?dyn name = + let wit = Genarg.make0 name in + let () = register_val0 wit dyn in + wit let wit_unit : unit uniform_genarg_type = make0 "unit" diff --git a/lib/genarg.ml b/lib/genarg.ml index 3ff9afa601..69408fb1a5 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -9,7 +9,6 @@ open Pp open Util -module ValT = Dyn.Make(struct end) module ArgT = struct module DYN = Dyn.Make(struct end) @@ -25,37 +24,6 @@ struct Some (Any (Obj.magic t)) (** All created tags are made of triples *) 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 rec pr : type a. a typ -> std_ppcmds = fun t -> str (repr t) - - let list_tag = ValT.create "list" - let opt_tag = ValT.create "option" - let pair_tag = 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 (list_tag, List.map (fun x -> inject tag x) x) - | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) x) - | Pair (tag1, tag2) -> - Dyn (pair_tag, (inject tag1 (fst x), inject tag2 (snd x))) - -end - type (_, _, _) genarg_type = | ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type @@ -187,36 +155,14 @@ struct include ArgT.Map(struct type 'a t = 'a pack end) end -type ('raw, 'glb, 'top) load = { - dyn : 'top Val.tag; -} - -module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end) - -let arg0_map = ref LoadMap.empty - -let create_arg ?dyn name = +let create_arg name = match ArgT.name name with + | None -> ExtraArg (ArgT.create name) | Some _ -> Errors.anomaly (str "generic argument already declared: " ++ str name) - | None -> - let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in - let obj = LoadMap.Pack { dyn; } in - let name = ArgT.create name in - let () = arg0_map := LoadMap.add name obj !arg0_map in - ExtraArg name let make0 = create_arg -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 -> - match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn - -let val_tag = function Topwit t -> val_tag t - (** Registering genarg-manipulating functions *) module type GenObj = diff --git a/lib/genarg.mli b/lib/genarg.mli index 04113ae289..b8bb6af04a 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -86,42 +86,14 @@ type (_, _, _) genarg_type = (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized one, and ['top] the internalized one. *) -module Val : -sig - type '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 list_tag : t list typ - val opt_tag : t option typ - val pair_tag : (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. *) - type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision when the three types agree. *) -val make0 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type +val make0 : string -> ('raw, 'glob, 'top) genarg_type (** Create a new generic type of argument: force to associate unique ML types at each of the three levels. *) -val create_arg : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type +val create_arg : string -> ('raw, 'glob, 'top) genarg_type (** Alias for [make0]. *) (** {5 Specialized types} *) @@ -186,12 +158,6 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that [out_gen t v] will not raise a dynamic type exception. *) -(** {6 Dynamic toplevel values} *) - -val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag -(** Retrieve the dynamic type associated to a toplevel genarg. Only works for - ground generic arguments. *) - (** {6 Type reification} *) type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 14aa69875f..4d1d8ba7fe 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -54,7 +54,7 @@ val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry val wit_by_arg_tac : (raw_tactic_expr option, glob_tactic_expr option, - Genarg.Val.t option) Genarg.genarg_type + Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 0b475340e2..eda530c265 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -258,7 +258,7 @@ END (**********************************************************************) (* Rewrite star *) -let rewrite_star ist clause orient occs c (tac : Val.t option) = +let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) = let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in with_delayed_uconstr ist c (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) @@ -939,8 +939,10 @@ type 'i test = | Test of cmp * 'i * 'i let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp" +let _ = Geninterp.register_val0 wit_cmp None let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = Genarg.make0 "tactest" +let _ = Geninterp.register_val0 wit_test None let pr_cmp = function | Eq -> Pp.str"=" diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index d2d3f3117f..f2dbb5b6c9 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -11,6 +11,7 @@ open Genarg open Pp open Names open Tacexpr +open Geninterp (** Tactic notations (TacAlias) *) @@ -32,7 +33,7 @@ let check_alias key = KNmap.mem key !alias_map (** ML tactic extensions (TacML) *) type ml_tactic = - Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic + Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic module MLName = struct diff --git a/ltac/tacenv.mli b/ltac/tacenv.mli index 88b54993b1..94e14223aa 100644 --- a/ltac/tacenv.mli +++ b/ltac/tacenv.mli @@ -9,6 +9,7 @@ open Genarg open Names open Tacexpr +open Geninterp (** This module centralizes the various ways of registering tactics. *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 6e76b19106..f39a42271b 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -30,6 +30,7 @@ open Term open Termops open Tacexpr open Genarg +open Geninterp open Stdarg open Constrarg open Printer @@ -118,7 +119,9 @@ type tacvalue = | VRec of value Id.Map.t ref * glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - Genarg.create_arg "tacvalue" + let wit = Genarg.create_arg "tacvalue" in + let () = register_val0 wit None in + wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 92f12fc8f7..8bb6ee4cdf 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -18,14 +18,14 @@ val ltac_trace_info : ltac_trace Exninfo.t module Value : sig - type t = Val.t + type t = Geninterp.Val.t val of_constr : constr -> t val to_constr : t -> constr option val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t - val cast : 'a typed_abstract_argument_type -> Val.t -> 'a + val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a end (** Values for interpretation *) diff --git a/ltac/tauto.ml b/ltac/tauto.ml index b0958b3948..c075d05bbf 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -11,6 +11,7 @@ open Hipattern open Names open Pp open Genarg +open Geninterp open Stdarg open Misctypes open Tacexpr @@ -55,7 +56,9 @@ type tauto_flags = { } let wit_tauto_flags : tauto_flags uniform_genarg_type = - Genarg.create_arg "tauto_flags" + let wit = Genarg.create_arg "tauto_flags" in + let () = register_val0 wit None in + wit let assoc_flags ist = let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 9d78a51ef6..29ecb94ca8 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -99,4 +99,4 @@ type proof_instr = (Term.constr statement, Term.constr, proof_pattern, - Genarg.Val.t) gen_proof_instr + Geninterp.Val.t) gen_proof_instr diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index a15b0eb05a..e4c8da93b1 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -24,7 +24,7 @@ let loc = Loc.ghost let cont = Id.of_string "cont" let x = Id.of_string "x" -let make_cont (k : Genarg.Val.t) (c : Constr.t) = +let make_cont (k : Val.t) (c : Constr.t) = let c = Tacinterp.Value.of_constr c in let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 07a1ae833b..ca6aba9a0f 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -45,7 +45,7 @@ val ic : constr_expr -> Evd.evar_map * constr val from_name : ring_info Spmap.t ref val ring_lookup : - Genarg.Val.t -> + Geninterp.Val.t -> constr list -> constr list -> constr -> unit Proofview.tactic @@ -73,6 +73,6 @@ val add_field_theory : val field_from_name : field_info Spmap.t ref val field_lookup : - Genarg.Val.t -> + Geninterp.Val.t -> constr list -> constr list -> constr -> unit Proofview.tactic diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5e6a3eac73..21eb100b4e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -49,7 +49,7 @@ open Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.Val.t Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; ltac_uconstrs : uconstr_var_map; diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 91320f20a5..824bb11aa4 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = Pattern.constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Genarg.Val.t Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 018e29cd29..a15fa772f8 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -14,6 +14,7 @@ open Util open Constrexpr open Tacexpr open Genarg +open Geninterp open Constrarg open Libnames open Ppextend diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 1608cae751..b1e650b872 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -11,6 +11,7 @@ open Pp open Genarg +open Geninterp open Names open Constrexpr open Tacexpr diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index d4858bac4f..d49bef1fd2 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -8,6 +8,7 @@ open Pp open Genarg +open Geninterp open Tacexpr open Ppextend open Environ diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 298257e45d..a03c529cc0 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -14,15 +14,20 @@ 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 diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 75a3b347d6..82e1910f7d 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 -- cgit v1.2.3 From a2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 Apr 2016 20:43:57 +0200 Subject: More toplevel value representation sharing. --- interp/stdarg.ml | 2 +- ltac/extratactics.ml4 | 8 +------- plugins/funind/g_indfun.ml4 | 1 + 3 files changed, 3 insertions(+), 8 deletions(-) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 9e85dbaf38..2a7d52e3af 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -27,7 +27,7 @@ let wit_string : string uniform_genarg_type = make0 "string" let wit_pre_ident : string uniform_genarg_type = - make0 "preident" + make0 ~dyn:(val_tag (topwit wit_string)) "preident" (** Aliases for compatibility *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index eda530c265..925c1679f2 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -938,12 +938,6 @@ type cmp = type 'i test = | Test of cmp * 'i * 'i -let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp" -let _ = Geninterp.register_val0 wit_cmp None -let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = - Genarg.make0 "tactest" -let _ = Geninterp.register_val0 wit_test None - let pr_cmp = function | Eq -> Pp.str"=" | Lt -> Pp.str"<" @@ -966,7 +960,7 @@ let pr_itest' _prc _prlc _prt = pr_itest -ARGUMENT EXTEND comparison TYPED AS cmp PRINTED BY pr_cmp' +ARGUMENT EXTEND comparison PRINTED BY pr_cmp' | [ "=" ] -> [ Eq ] | [ "<" ] -> [ Lt ] | [ "<=" ] -> [ Le ] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e93c395e3d..0ba18f568a 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -65,6 +65,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = ARGUMENT EXTEND fun_ind_using + TYPED AS constr_with_bindings option PRINTED BY pr_fun_ind_using_typed RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using -- cgit v1.2.3 From 1c999a9760f4f2287d11529600ec96567e630ce6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Apr 2016 15:09:07 +0200 Subject: Do not generate generic arguments for data which only requires toplevel values. --- ltac/tauto.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/ltac/tauto.ml b/ltac/tauto.ml index c075d05bbf..7cda8d9147 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -55,14 +55,13 @@ type tauto_flags = { strict_unit : bool; } -let wit_tauto_flags : tauto_flags uniform_genarg_type = - let wit = Genarg.create_arg "tauto_flags" in - let () = register_val0 wit None in - wit +let tag_tauto_flags : tauto_flags Val.typ = Val.create "tauto_flags" -let assoc_flags ist = - let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in - try Value.cast (topwit wit_tauto_flags) v with _ -> assert false +let assoc_flags ist : tauto_flags = + let Val.Dyn (tag, v) = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in + match Val.eq tag tag_tauto_flags with + | None -> assert false + | Some Refl -> v (* Whether inner not are unfolded *) let negation_unfolding = ref true @@ -259,7 +258,7 @@ let tauto_power_flags = { let with_flags flags _ ist = let f = (loc, Id.of_string "f") in let x = (loc, Id.of_string "x") in - let arg = Val.inject (val_tag (topwit wit_tauto_flags)) flags in + let arg = Val.Dyn (tag_tauto_flags, flags) in let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)]))) -- cgit v1.2.3 From 2aae561fe772a08b03ea8a96ee28372408bf233a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Apr 2016 15:15:35 +0200 Subject: Removing the Value.of_* API for parameterized types. Although still working, it is now bad practice to use it, and it is not widely spread anyway. --- ltac/tacinterp.ml | 8 ++++++-- tactics/taccoerce.ml | 6 ------ tactics/taccoerce.mli | 3 --- 3 files changed, 6 insertions(+), 11 deletions(-) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index f39a42271b..da4ddd4586 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -63,6 +63,9 @@ let prj : type a. a Val.typ -> Val.t -> a option = fun t v -> | None -> None | Some Refl -> Some x +let in_list tag v = + let tag = match tag with Val.Base tag -> tag | _ -> assert false in + Val.Dyn (Val.list_tag, List.map (fun x -> Val.Dyn (tag, x)) v) let in_gen wit v = Val.inject (val_tag wit) v let out_gen wit v = let t = match val_tag wit with @@ -1577,7 +1580,7 @@ and interp_genarg_constr_list ist x = let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in let (sigma,lc) = interp_constr_list ist env sigma lc in - let lc = Value.of_list (val_tag wit_constr) lc in + let lc = in_list (val_tag wit_constr) lc in Sigma.Unsafe.of_pair (Ftactic.return lc, sigma) end } @@ -1587,7 +1590,8 @@ and interp_genarg_var_list ist x = let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in let lc = interp_hyp_list ist env sigma lc in - Ftactic.return (Value.of_list (val_tag wit_var) lc) + let lc = in_list (val_tag wit_var) lc in + Ftactic.return lc end } (* Interprets tactic expressions : returns a "constr" *) diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index a03c529cc0..a6e7af16e9 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -86,16 +86,10 @@ let to_int v = let to_list v = prj Val.list_tag v -let of_list t v = Val.Dyn (Val.list_tag, List.map (fun v -> Val.inject t v) v) - let to_option v = prj Val.opt_tag v -let of_option t v = Val.Dyn (Val.opt_tag, Option.map (fun v -> Val.inject t v) v) - let to_pair v = prj Val.pair_tag v -let of_pair t1 t2 (v1, v2) = Val.Dyn (Val.pair_tag, (Val.inject t1 v1, Val.inject t2 v2)) - end let is_variable env id = diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 82e1910f7d..7a963f95f3 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -42,11 +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 - val of_pair : 'a Val.tag -> 'b Val.tag -> ('a * 'b) -> t end (** {5 Coercion functions} *) -- cgit v1.2.3 From 4740e82e4af6d38e9cc55dfe1a05db87f73bf1e6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Apr 2016 15:23:41 +0200 Subject: Removing external uses of Val.inject and making Geninterp.interp return Val.t --- engine/geninterp.ml | 6 +++++- engine/geninterp.mli | 2 +- ltac/tacinterp.ml | 21 +++++++-------------- tactics/auto.ml | 5 ++++- 4 files changed, 17 insertions(+), 17 deletions(-) diff --git a/engine/geninterp.ml b/engine/geninterp.ml index 9e866f0cf8..a3e494f5c0 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -93,5 +93,9 @@ end module Interp = Register(InterpObj) -let interp = Interp.obj +let interp wit ist v = + let f = Interp.obj wit in + let tag = val_tag (Topwit wit) in + Ftactic.bind (f ist v) (fun v -> Ftactic.return (Val.inject tag v)) + let register_interp0 = Interp.register0 diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 3c87b25121..c92181027e 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -61,7 +61,7 @@ type interp_sign = { type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t -val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun val register_interp0 : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index da4ddd4586..a3e6e0ebe0 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -66,7 +66,12 @@ let prj : type a. a Val.typ -> Val.t -> a option = fun t v -> let in_list tag v = let tag = match tag with Val.Base tag -> tag | _ -> assert false in Val.Dyn (Val.list_tag, List.map (fun x -> Val.Dyn (tag, x)) v) -let in_gen wit v = Val.inject (val_tag wit) v +let in_gen wit v = + let t = match val_tag wit with + | Val.Base t -> t + | _ -> assert false (** not used in this module *) + in + Val.Dyn (t, v) let out_gen wit v = let t = match val_tag wit with | Val.Base t -> t @@ -1143,17 +1148,6 @@ let rec read_match_rule lfun ist env sigma = function | [] -> [] -(* misc *) - -let interp_focussed wit f v = - Ftactic.nf_enter { enter = begin fun gl -> - let v = Genarg.out_gen (glbwit wit) v in - let env = Proofview.Goal.env gl in - let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in - let v = in_gen (topwit wit) (f env sigma v) in - Ftactic.return v - end } - (* Interprets an l-tac expression into a value *) let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftactic.t = (* The name [appl] of applied top-level Ltac names is ignored in @@ -1568,8 +1562,7 @@ and interp_genarg ist x : Val.t Ftactic.t = interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q -> Ftactic.return (Val.Dyn (Val.pair_tag, (p, q))) | ExtraArg s -> - Geninterp.interp wit ist x >>= fun x -> - Ftactic.return (in_gen (Topwit wit) x) + Geninterp.interp wit ist x (** returns [true] for genargs which have the same meaning independently of goals. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 46f484bf06..6b58baa997 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -156,7 +156,10 @@ let conclPattern concl pat tac = constr_bindings env sigma >>= fun constr_bindings -> let open Genarg in let open Geninterp in - let inj c = Val.inject (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 -- cgit v1.2.3 From 729d838838d8df06395726477817620e2ae998bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 20 Apr 2016 17:24:58 +0200 Subject: Interpretation function can return any untyped value. --- engine/geninterp.ml | 7 ++----- engine/geninterp.mli | 2 +- grammar/argextend.ml4 | 10 +++++---- ltac/tacinterp.ml | 45 ++++++++++++++++++++++++----------------- plugins/firstorder/g_ground.ml4 | 1 + 5 files changed, 36 insertions(+), 29 deletions(-) diff --git a/engine/geninterp.ml b/engine/geninterp.ml index a3e494f5c0..ffc22f2213 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -86,16 +86,13 @@ type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t module InterpObj = struct - type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun + type ('raw, 'glb, 'top) obj = ('glb, Val.t) interp_fun let name = "interp" let default _ = None end module Interp = Register(InterpObj) -let interp wit ist v = - let f = Interp.obj wit in - let tag = val_tag (Topwit wit) in - Ftactic.bind (f ist v) (fun v -> Ftactic.return (Val.inject tag v)) +let interp = Interp.obj let register_interp0 = Interp.register0 diff --git a/engine/geninterp.mli b/engine/geninterp.mli index c92181027e..5799862110 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -64,4 +64,4 @@ 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, 'top) interp_fun -> unit + ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 2618e5d896..3b7e180c6f 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -119,19 +119,21 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = let interp = match f with | None -> begin match globtyp with - | None -> <:expr< fun ist v -> Ftactic.return v >> + | None -> + let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in + <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >> | Some globtyp -> <:expr< fun ist x -> - Ftactic.bind - (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x)) - (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >> + Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >> end | Some f -> (** Compatibility layer, TODO: remove me *) + let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in <:expr< let f = $lid:f$ in fun ist v -> Ftactic.nf_s_enter { Proofview.Goal.s_enter = fun gl -> let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in Sigma.Unsafe.of_pair (Ftactic.return v, sigma) } >> in diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index a3e6e0ebe0..94c13a0e0e 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -2042,6 +2042,13 @@ let hide_interp global t ot = (***************************************************************************) (** Register standard arguments *) +let register_interp0 wit f = + let open Ftactic.Notations in + let interp ist v = + f ist v >>= fun v -> Ftactic.return (Val.inject (val_tag wit) v) + in + Geninterp.register_interp0 wit interp + let def_intern ist x = (ist, x) let def_subst _ x = x let def_interp ist x = Ftactic.return x @@ -2049,7 +2056,7 @@ let def_interp ist x = Ftactic.return x let declare_uniform t = Genintern.register_intern0 t def_intern; Genintern.register_subst0 t def_subst; - Geninterp.register_interp0 t def_interp + register_interp0 t def_interp let () = declare_uniform wit_unit @@ -2090,33 +2097,33 @@ let interp_constr_with_bindings' ist c = Ftactic.return { delayed = fun env sigm } let () = - Geninterp.register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); - Geninterp.register_interp0 wit_ref (lift interp_reference); - Geninterp.register_interp0 wit_ident (lift interp_ident); - Geninterp.register_interp0 wit_var (lift interp_hyp); - Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern); - Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause); - Geninterp.register_interp0 wit_constr (lifts interp_constr); - Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s)); - Geninterp.register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v); - Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr); - Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis); - Geninterp.register_interp0 wit_open_constr (lifts interp_open_constr); - Geninterp.register_interp0 wit_bindings interp_bindings'; - Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; - Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval); + register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); + register_interp0 wit_ref (lift interp_reference); + register_interp0 wit_ident (lift interp_ident); + register_interp0 wit_var (lift interp_hyp); + register_interp0 wit_intro_pattern (lifts interp_intro_pattern); + register_interp0 wit_clause_dft_concl (lift interp_clause); + register_interp0 wit_constr (lifts interp_constr); + register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s)); + register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v); + register_interp0 wit_red_expr (lifts interp_red_expr); + register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis); + register_interp0 wit_open_constr (lifts interp_open_constr); + register_interp0 wit_bindings interp_bindings'; + register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; + register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval); () let () = let interp ist tac = Ftactic.return (Value.of_closure ist tac) in - Geninterp.register_interp0 wit_tactic interp + register_interp0 wit_tactic interp let () = let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in - Geninterp.register_interp0 wit_ltac interp + register_interp0 wit_ltac interp let () = - Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl -> + register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c) end }) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 587d10d1cc..b04c4a50c9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -122,6 +122,7 @@ let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l ARGUMENT EXTEND firstorder_using + TYPED AS reference_list PRINTED BY pr_firstorder_using_typed RAW_TYPED AS reference_list RAW_PRINTED BY pr_firstorder_using_raw -- cgit v1.2.3 From c7fd62135403c1ea38194fcdd8035237ee108318 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 3 May 2016 20:49:01 +0200 Subject: Removing useless generic arguments. --- interp/constrarg.ml | 3 --- interp/constrarg.mli | 9 --------- ltac/extratactics.ml4 | 6 ++++++ ltac/tacintern.ml | 2 -- ltac/tacinterp.ml | 2 -- ltac/tacsubst.ml | 2 -- parsing/pcoq.ml | 2 -- printing/pptactic.ml | 7 ------- 8 files changed, 6 insertions(+), 27 deletions(-) diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 99f0a2da64..b8f97e77c3 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -46,9 +46,6 @@ let wit_ref = make0 "ref" let wit_quant_hyp = make0 "quant_hyp" -let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = - make0 "sort" - let wit_constr = make0 "constr" diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 6407b61afd..70c9c0de2c 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -38,15 +38,8 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val wit_sort : (glob_sort, glob_sort, sorts) genarg_type - val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_constr_may_eval : - ((constr_expr,reference or_by_notation,constr_expr) may_eval, - (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval, - constr) genarg_type - val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : @@ -62,8 +55,6 @@ val wit_bindings : glob_constr_and_expr bindings, constr bindings delayed_open) genarg_type -val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type - val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 925c1679f2..79f80260fa 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -393,6 +393,12 @@ open Leminv let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater +VERNAC ARGUMENT EXTEND sort +| [ "Set" ] -> [ GSet ] +| [ "Prop" ] -> [ GProp ] +| [ "Type" ] -> [ GType [] ] +END + VERNAC COMMAND EXTEND DeriveInversionClear | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] => [ seff na ] diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 15589d5c4a..977c56f38b 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -800,7 +800,6 @@ let () = Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg); - Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c)); Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)); @@ -808,7 +807,6 @@ let () = Genintern.register_intern0 wit_red_expr (lift intern_red_expr); Genintern.register_intern0 wit_bindings (lift intern_bindings); Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings); - Genintern.register_intern0 wit_constr_may_eval (lift intern_constr_may_eval); () (***************************************************************************) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 94c13a0e0e..a9baef79c7 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -2104,14 +2104,12 @@ let () = register_interp0 wit_intro_pattern (lifts interp_intro_pattern); register_interp0 wit_clause_dft_concl (lift interp_clause); register_interp0 wit_constr (lifts interp_constr); - register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s)); register_interp0 wit_tacvalue (fun ist v -> Ftactic.return v); register_interp0 wit_red_expr (lifts interp_red_expr); register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis); register_interp0 wit_open_constr (lifts interp_open_constr); register_interp0 wit_bindings interp_bindings'; register_interp0 wit_constr_with_bindings interp_constr_with_bindings'; - register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval); () let () = diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 438219f5a3..54d32f2666 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -301,7 +301,6 @@ let () = Genintern.register_subst0 wit_tactic subst_tactic; Genintern.register_subst0 wit_ltac subst_tactic; Genintern.register_subst0 wit_constr subst_glob_constr; - Genintern.register_subst0 wit_sort (fun _ v -> v); Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v); Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c); Genintern.register_subst0 wit_open_constr (fun subst c -> subst_glob_constr subst c); @@ -309,5 +308,4 @@ let () = Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis; Genintern.register_subst0 wit_bindings subst_bindings; Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings; - Genintern.register_subst0 wit_constr_may_eval subst_raw_may_eval; () diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index e60b470fdf..53d2089c04 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -730,9 +730,7 @@ let () = Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); Grammar.register0 wit_quant_hyp (Tactic.quantified_hypothesis); - Grammar.register0 wit_sort (Constr.sort); Grammar.register0 wit_constr (Constr.constr); - Grammar.register0 wit_constr_may_eval (Tactic.constr_may_eval); Grammar.register0 wit_uconstr (Tactic.uconstr); Grammar.register0 wit_open_constr (Tactic.open_constr); Grammar.register0 wit_constr_with_bindings (Tactic.constr_with_bindings); diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a15fa772f8..6fb68ddf42 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1365,8 +1365,6 @@ let () = (pr_clauses (Some true) pr_lident) (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; - Genprint.register_print0 Constrarg.wit_sort - pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 Constrarg.wit_constr Ppconstr.pr_constr_expr @@ -1394,11 +1392,6 @@ let () = (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it))); - Genprint.register_print0 Constrarg.wit_constr_may_eval - (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr) - (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr) - (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr)) - pr_constr; Genprint.register_print0 Constrarg.wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) -- cgit v1.2.3 From 8d3f0b614d7b2fb30f6e87b48a4fc5c0d286e49c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 4 May 2016 14:30:48 +0200 Subject: Normalizing the names of dynamic types to follow a typ_* scheme. --- engine/geninterp.ml | 12 ++++++------ engine/geninterp.mli | 6 +++--- ltac/tacinterp.ml | 16 ++++++++-------- printing/pptactic.ml | 12 ++++++------ tactics/taccoerce.ml | 6 +++--- 5 files changed, 26 insertions(+), 26 deletions(-) diff --git a/engine/geninterp.ml b/engine/geninterp.ml index ffc22f2213..45b0aa2316 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -34,16 +34,16 @@ struct let rec pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t) - let list_tag = ValT.create "list" - let opt_tag = ValT.create "option" - let pair_tag = ValT.create "pair" + 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 (list_tag, List.map (fun x -> inject tag x) x) - | Opt tag -> Dyn (opt_tag, Option.map (fun x -> inject tag x) 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 (pair_tag, (inject tag1 (fst x), inject tag2 (snd x))) + Dyn (typ_pair, (inject tag1 (fst x), inject tag2 (snd x))) end diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 5799862110..42e1e3784c 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -31,9 +31,9 @@ sig val repr : 'a typ -> string val pr : 'a typ -> Pp.std_ppcmds - val list_tag : t list typ - val opt_tag : t option typ - val pair_tag : (t * t) typ + val typ_list : t list typ + val typ_opt : t option typ + val typ_pair : (t * t) typ val inject : 'a tag -> 'a -> t diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index a9baef79c7..31bccd019d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -65,7 +65,7 @@ let prj : type a. a Val.typ -> Val.t -> a option = fun t v -> let in_list tag v = let tag = match tag with Val.Base tag -> tag | _ -> assert false in - Val.Dyn (Val.list_tag, List.map (fun x -> Val.Dyn (tag, x)) v) + Val.Dyn (Val.typ_list, List.map (fun x -> Val.Dyn (tag, x)) v) let in_gen wit v = let t = match val_tag wit with | Val.Base t -> t @@ -179,10 +179,10 @@ module Value = struct | Some x -> x let rec prj : type a. a Val.tag -> Val.t -> a = fun tag v -> match tag with - | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.list_tag v (to_list v)) - | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.opt_tag v (to_option v)) + | Val.List tag -> List.map (fun v -> prj tag v) (unbox Val.typ_list v (to_list v)) + | Val.Opt tag -> Option.map (fun v -> prj tag v) (unbox Val.typ_opt v (to_option v)) | Val.Pair (tag1, tag2) -> - let (x, y) = unbox Val.pair_tag v (to_pair v) in + let (x, y) = unbox Val.typ_pair v (to_pair v) in (prj tag1 x, prj tag2 y) | Val.Base t -> let Val.Dyn (t', x) = v in @@ -1548,19 +1548,19 @@ and interp_genarg ist x : Val.t Ftactic.t = | ListArg wit -> let map x = interp_genarg ist (Genarg.in_gen (glbwit wit) x) in Ftactic.List.map map x >>= fun l -> - Ftactic.return (Val.Dyn (Val.list_tag, l)) + Ftactic.return (Val.Dyn (Val.typ_list, l)) | OptArg wit -> begin match x with - | None -> Ftactic.return (Val.Dyn (Val.opt_tag, None)) + | None -> Ftactic.return (Val.Dyn (Val.typ_opt, None)) | Some x -> interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x -> - Ftactic.return (Val.Dyn (Val.opt_tag, Some x)) + Ftactic.return (Val.Dyn (Val.typ_opt, Some x)) end | PairArg (wit1, wit2) -> let (p, q) = x in interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p -> interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q -> - Ftactic.return (Val.Dyn (Val.pair_tag, (p, q))) + Ftactic.return (Val.Dyn (Val.typ_pair, (p, q))) | ExtraArg s -> Geninterp.interp wit ist x diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 6fb68ddf42..9ab6895f3b 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -108,12 +108,12 @@ module Make | Some Refl -> x let rec pr_value lev v : std_ppcmds = - if has_type v Val.list_tag then - pr_sequence (fun x -> pr_value lev x) (unbox v Val.list_tag) - else if has_type v Val.opt_tag then - pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.opt_tag) - else if has_type v Val.pair_tag then - let (v1, v2) = unbox v Val.pair_tag in + if has_type v Val.typ_list then + pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list) + else if has_type v Val.typ_opt then + pr_opt_no_spc (fun x -> pr_value lev x) (unbox v Val.typ_opt) + else if has_type v Val.typ_pair then + let (v1, v2) = unbox v Val.typ_pair in str "(" ++ pr_value lev v1 ++ str ", " ++ pr_value lev v2 ++ str ")" else let Val.Dyn (tag, x) = v in diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index a6e7af16e9..d53c1cc04a 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -84,11 +84,11 @@ let to_int v = Some (out_gen (topwit wit_int) v) else None -let to_list v = prj Val.list_tag v +let to_list v = prj Val.typ_list v -let to_option v = prj Val.opt_tag v +let to_option v = prj Val.typ_opt v -let to_pair v = prj Val.pair_tag v +let to_pair v = prj Val.typ_pair v end -- cgit v1.2.3