diff options
41 files changed, 391 insertions, 375 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"<genarg:"++pr_argument_type(genarg_tag arg)++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/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/tactics/ftactic.ml b/engine/ftactic.ml index 588709873e..588709873e 100644 --- a/tactics/ftactic.ml +++ b/engine/ftactic.ml diff --git a/tactics/ftactic.mli b/engine/ftactic.mli index 19041f1698..19041f1698 100644 --- a/tactics/ftactic.mli +++ b/engine/ftactic.mli 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 diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index dca3e1656f..3b7e180c6f 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 @@ -118,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 @@ -147,20 +150,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..b8f97e77c3 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,47 @@ 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" - -let wit_ref = Genarg.make0 "ref" + make0 ~dyn:(val_tag (topwit wit_ident)) "var" -let wit_quant_hyp = Genarg.make0 "quant_hyp" +let wit_ref = make0 "ref" -let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = - Genarg.make0 "sort" +let wit_quant_hyp = make0 "quant_hyp" 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..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,14 +55,12 @@ 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, (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..2a7d52e3af 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" @@ -21,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/lib/genarg.ml b/lib/genarg.ml index ef0de89afb..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,52 +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 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 - - 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 ")" - -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 @@ -202,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 93665fd45d..b8bb6af04a 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -86,36 +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 tag * 'a -> t - - val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option - val repr : 'a typ -> string - val pr : 'a tag -> Pp.std_ppcmds - -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} *) @@ -180,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..79f80260fa 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) @@ -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 ] @@ -938,10 +944,6 @@ type cmp = type 'i test = | Test of cmp * 'i * 'i -let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp" -let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type = - Genarg.make0 "tactest" - let pr_cmp = function | Eq -> Pp.str"=" | Lt -> Pp.str"<" @@ -964,7 +966,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/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/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/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 9b41a276b9..31bccd019d 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 @@ -48,18 +49,35 @@ 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_list tag v = + let tag = match tag with Val.Base tag -> tag | _ -> assert false in + 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 + | _ -> 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 + | _ -> 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) @@ -109,7 +127,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 @@ -152,47 +172,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.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.typ_pair 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 @@ -1144,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 @@ -1553,30 +1546,23 @@ 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.typ_list, 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.typ_opt, 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.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 -> - 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 (Val.Dyn (Val.typ_pair, (p, q))) | ExtraArg s -> - Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x) + Geninterp.interp wit ist x (** returns [true] for genargs which have the same meaning independently of goals. *) @@ -1587,7 +1573,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 } @@ -1597,7 +1583,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" *) @@ -2055,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 @@ -2062,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 @@ -2103,33 +2097,31 @@ 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_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'; () 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/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/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/ltac/tauto.ml b/ltac/tauto.ml index a86fdb98a9..7cda8d9147 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 @@ -54,12 +55,13 @@ type tauto_flags = { strict_unit : bool; } -let wit_tauto_flags : tauto_flags uniform_genarg_type = - Genarg.create_arg "tauto_flags" +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 @@ -256,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.Dyn (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)]))) 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/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/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 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 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 7949bafcbb..9ab6895f3b 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 @@ -97,23 +98,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.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 + 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 @@ -1349,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 @@ -1378,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)) 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/auto.ml b/tactics/auto.ml index fc6ff03b4b..6b58baa997 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -156,11 +156,16 @@ let conclPattern concl pat tac = constr_bindings env sigma >>= fun constr_bindings -> let open Genarg in let open Geninterp in - let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in + let inj c = match val_tag (topwit Constrarg.wit_constr) with + | Val.Base tag -> Val.Dyn (tag, c) + | _ -> assert false + in let fold id c accu = Id.Map.add id (inj c) accu in let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in let ist = { lfun; extra = TacStore.empty } in - Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) + match tac with + | GenArg (Glbwit wit, tac) -> + Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ()) end } (***********************************************************) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 4816f8a452..950eeef520 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -106,9 +106,9 @@ let one_base general_rewrite_maybe_in tac_main bas = let lrul = List.map (fun h -> let tac = match h.rew_tac with | None -> Proofview.tclUNIT () - | Some tac -> + | Some (Genarg.GenArg (Genarg.Glbwit wit, tac)) -> let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in - Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) + Ftactic.run (Geninterp.interp wit ist tac) (fun _ -> Proofview.tclUNIT ()) in (h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in Tacticals.New.tclREPEAT_MAIN (Proofview.tclPROGRESS (List.fold_left (fun tac (ctx,csr,dir,tc) -> diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml deleted file mode 100644 index 0080758000..0000000000 --- a/tactics/geninterp.ml +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Names -open Genarg - -module TacStore = Store.Make(struct end) - -type interp_sign = { - lfun : Val.t Id.Map.t; - extra : TacStore.t } - -type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t - -module InterpObj = -struct - type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun - let name = "interp" - let default _ = None -end - -module Interp = Register(InterpObj) - -let interp = Interp.obj -let register_interp0 = Interp.register0 - -let generic_interp ist (GenArg (Glbwit wit, v)) = - let open Ftactic.Notations in - interp wit ist v >>= fun ans -> - Ftactic.return (Val.Dyn (val_tag (topwit wit), ans)) diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli deleted file mode 100644 index 0992db7a29..0000000000 --- a/tactics/geninterp.mli +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(** Interpretation functions for generic arguments. *) - -open Names -open Genarg - -module TacStore : Store.S - -type interp_sign = { - lfun : Val.t Id.Map.t; - extra : TacStore.t } - -type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t - -val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun - -val generic_interp : (glob_generic_argument, Val.t) interp_fun - -val register_interp0 : - ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 358f6d6468..d53c1cc04a 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -14,15 +14,25 @@ open Misctypes open Genarg open Stdarg open Constrarg +open Geninterp exception CannotCoerceTo of string let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) = - Genarg.create_arg "constr_context" + let wit = Genarg.create_arg "constr_context" in + let () = register_val0 wit None in + wit (* includes idents known to be bound and references *) let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = - Genarg.create_arg "constr_under_binders" + let wit = Genarg.create_arg "constr_under_binders" in + let () = register_val0 wit None in + wit + +(** All the types considered here are base types *) +let val_tag wit = match val_tag wit with +| Val.Base t -> t +| _ -> assert false let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> let Val.Dyn (t, _) = v in @@ -30,7 +40,7 @@ let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v w | None -> false | Some Refl -> true -let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> +let prj : type a. a Val.typ -> Val.t -> a option = fun t v -> let Val.Dyn (t', x) = v in match Val.eq t t' with | None -> None @@ -74,23 +84,11 @@ let to_int v = Some (out_gen (topwit wit_int) v) else None -let to_list v = - let v = normalize v in - let Val.Dyn (tag, v) = v in - match tag with - | Val.List t -> Some (List.map (fun x -> Val.Dyn (t, x)) v) - | _ -> None - -let of_list t v = Val.Dyn (Val.List t, v) +let to_list v = prj Val.typ_list v -let to_option v = - let v = normalize v in - let Val.Dyn (tag, v) = v in - match tag with - | Val.Opt t -> Some (Option.map (fun x -> Val.Dyn (t, x)) v) - | _ -> None +let to_option v = prj Val.typ_opt v -let of_option t v = Val.Dyn (Val.Opt t, v) +let to_pair v = prj Val.typ_pair v end diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 87137fd2e7..7a963f95f3 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -12,6 +12,7 @@ open Term open Misctypes open Pattern open Genarg +open Geninterp (** Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return @@ -41,9 +42,8 @@ sig val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option - val of_list : 'a Val.tag -> 'a list -> t val to_option : t -> t option option - val of_option : 'a Val.tag -> 'a option -> t + val to_pair : t -> (t * t) option end (** {5 Coercion functions} *) diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index ab8069225d..48722f655a 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,5 +1,3 @@ -Ftactic -Geninterp Dnet Dn Btermdn |