diff options
| -rw-r--r-- | dev/top_printers.ml | 12 | ||||
| -rw-r--r-- | grammar/argextend.ml4 | 2 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 4 | ||||
| -rw-r--r-- | lib/genarg.ml | 37 | ||||
| -rw-r--r-- | lib/genarg.mli | 5 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 4 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 6 | ||||
| -rw-r--r-- | tactics/geninterp.ml | 4 | ||||
| -rw-r--r-- | tactics/geninterp.mli | 4 | ||||
| -rw-r--r-- | tactics/taccoerce.ml | 37 | ||||
| -rw-r--r-- | tactics/taccoerce.mli | 6 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 160 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 5 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 4 |
18 files changed, 203 insertions, 95 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0e9002612..20c8f690b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -467,11 +467,13 @@ let pp_generic_argument arg = pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">") let prgenarginfo arg = - let tpe = pr_argument_type (genarg_tag arg) in - try - let data = Pptactic.pr_top_generic (Global.env ()) arg in - str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" - with _any -> + let Val.Dyn (tag, _) = arg in + let tpe = str (Val.repr tag) in + (** FIXME *) +(* try *) +(* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) +(* str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >" *) +(* with _any -> *) str "<genarg:" ++ tpe ++ str ">" let ppgenarginfo arg = pp (prgenarginfo arg) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index a49291d94..fff706857 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -194,7 +194,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = (Tacmach.pf_env gl) (Tacmach.project gl) (Tacmach.pf_concl gl) gl.Evd.it (Genarg.in_gen $make_globwit loc globtyp$ x) in - (sigma , out_gen $make_topwit loc globtyp$ a_interp)>> + (sigma , Tacinterp.Value.cast $make_topwit loc globtyp$ a_interp)>> end | Some f -> <:expr< $lid:f$>> in let subst = match h with diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index df2209606..01828267b 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -53,7 +53,7 @@ let rec make_let raw e = function let e = make_let raw e l in let v = if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >> - else <:expr< Genarg.out_gen $make_topwit loc t$ $lid:p$ >> in + else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l @@ -73,7 +73,7 @@ let check_unicity s l = let make_clause (pt,_,e) = (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr e) pt)), + vala None, make_let false e pt) let make_fun_clauses loc s l = diff --git a/lib/genarg.ml b/lib/genarg.ml index b6a2849ad..a43a798c4 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -197,6 +197,43 @@ let val_tag = function | OptArgType t -> assert false | PairArgType (t1, t2) -> assert false +exception CastError of argument_type * Val.t + +let prj : type a. a Val.tag -> 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 try_prj wit v = match prj (val_tag wit) v with +| None -> raise (CastError (wit, v)) +| Some x -> x + +let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = +fun wit v -> match unquote wit with +| IntOrVarArgType | IdentArgType +| VarArgType | GenArgType +| ConstrArgType | ConstrMayEvalArgType +| OpenConstrArgType | ExtraArgType _ -> try_prj wit v +| ListArgType t -> + let v = match prj list_val v with + | None -> raise (CastError (wit, v)) + | Some v -> v + in + Obj.magic (List.map (fun x -> val_cast t x) v) +| OptArgType t -> + let v = match prj option_val v with + | None -> raise (CastError (wit, v)) + | Some v -> v + in + Obj.magic (Option.map (fun x -> val_cast t x) v) +| PairArgType (t1, t2) -> + let (v1, v2) = match prj pair_val v with + | None -> raise (CastError (wit, v)) + | Some v -> v + in + Obj.magic (val_cast t1 v1, val_cast t2 v2) + (** Registering genarg-manipulating functions *) module type GenObj = diff --git a/lib/genarg.mli b/lib/genarg.mli index d52a24610..c431aa619 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -191,6 +191,8 @@ 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. *) +val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a + val option_val : Val.t option Val.tag val list_val : Val.t list Val.tag val pair_val : (Val.t * Val.t) Val.tag @@ -212,6 +214,9 @@ type argument_type = | PairArgType of argument_type * argument_type | ExtraArgType of string +exception CastError of argument_type * Val.t +(** Exception raised by {!val_cast} *) + val argument_type_eq : argument_type -> argument_type -> bool val pr_argument_type : argument_type -> Pp.std_ppcmds diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 2b07ba704..d596cf6fb 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -209,7 +209,7 @@ let get_res = let name = { mltac_plugin = "newring_plugin"; mltac_tactic = "get_res"; } in let entry = { mltac_name = name; mltac_index = 0 } in let tac args ist = - let n = Genarg.out_gen (Genarg.topwit Stdarg.wit_int) (List.hd args) in + let n = Tacinterp.Value.cast (Genarg.topwit Stdarg.wit_int) (List.hd args) in let init i = Id.Map.find (Id.of_string ("x" ^ string_of_int i)) ist.lfun in tactic_res := Array.init n init; Proofview.tclUNIT () diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ce6d18985..f5b89e789 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,7 +47,7 @@ open Misctypes 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.tlevel Genarg.generic_argument Id.Map.t +type unbound_ltac_var_map = Genarg.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 f8587d01c..8b76816ab 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.tlevel Genarg.generic_argument Id.Map.t +type unbound_ltac_var_map = Genarg.Val.t Id.Map.t type ltac_var_map = { ltac_constrs : var_map; @@ -152,5 +152,5 @@ val interp_sort : evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : - (types -> env -> evar_map -> Genarg.typed_generic_argument Id.Map.t -> + (types -> env -> evar_map -> unbound_ltac_var_map -> Genarg.glob_generic_argument -> constr * evar_map) Hook.t diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index 1c17d0492..d154e0b66 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -48,6 +48,12 @@ module type Pp = sig val pr_extend : env -> int -> ml_tactic_entry -> typed_generic_argument list -> std_ppcmds + val pr_extend_gen : + ('a -> std_ppcmds) -> int -> ml_tactic_entry -> 'a list -> std_ppcmds + + val pr_alias_gen : ('a -> std_ppcmds) -> + int -> Names.KerName.t -> 'a list -> std_ppcmds + val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds val pr_raw_tactic : raw_tactic_expr -> std_ppcmds diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml index d44c4ac3a..3da1d542b 100644 --- a/tactics/geninterp.ml +++ b/tactics/geninterp.ml @@ -12,7 +12,7 @@ open Genarg module TacStore = Store.Make(struct end) type interp_sign = { - lfun : tlevel generic_argument Id.Map.t; + lfun : Val.t Id.Map.t; extra : TacStore.t } type ('glb, 'top) interp_fun = interp_sign -> @@ -33,6 +33,6 @@ let register_interp0 = Interp.register0 let generic_interp ist gl v = let unpacker wit v = let (sigma, ans) = interp wit ist gl (glb v) in - (sigma, in_gen (topwit wit) ans) + (sigma, Val.Dyn (val_tag (topwit wit), ans)) in unpack { unpacker; } v diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli index 3c653697d..472ff1090 100644 --- a/tactics/geninterp.mli +++ b/tactics/geninterp.mli @@ -14,7 +14,7 @@ open Genarg module TacStore : Store.S type interp_sign = { - lfun : tlevel generic_argument Id.Map.t; + lfun : Val.t Id.Map.t; extra : TacStore.t } type ('glb, 'top) interp_fun = interp_sign -> @@ -22,7 +22,7 @@ type ('glb, 'top) interp_fun = interp_sign -> val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -val generic_interp : (glob_generic_argument, typed_generic_argument) 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 ab71f5f2e..f856fd842 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -24,15 +24,30 @@ 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 None "constr_under_binders" +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 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 + module Value = struct -type t = tlevel generic_argument +type t = Val.t -let rec normalize v = - if has_type v (topwit wit_genarg) then - normalize (out_gen (topwit wit_genarg) v) - else v +let rec normalize v = v (** FIXME *) +(* if has_type v (topwit wit_genarg) then *) +(* normalize (out_gen (topwit wit_genarg) v) *) +(* else v *) let of_constr c = in_gen (topwit wit_constr) c @@ -64,9 +79,15 @@ let to_int v = let to_list v = let v = normalize v in - let list_unpacker wit l = List.map (fun v -> in_gen (topwit wit) v) (top l) in - try Some (list_unpack { list_unpacker } v) - with Failure _ -> None + prj list_val v + +let of_list v = Val.Dyn (list_val, v) + +let to_option v = + let v = normalize v in + prj option_val v + +let of_option v = Val.Dyn (option_val, v) end diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli index 85bad364d..4d85ae709 100644 --- a/tactics/taccoerce.mli +++ b/tactics/taccoerce.mli @@ -29,8 +29,7 @@ exception CannotCoerceTo of string module Value : sig - type t = tlevel generic_argument - (** Tactics manipulate [tlevel generic_argument]. *) + type t = Val.t val normalize : t -> t (** Eliminated the leading dynamic type casts. *) @@ -42,6 +41,9 @@ sig val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option + val of_list : t list -> t + val to_option : t -> t option option + val of_option : t option -> t end (** {5 Coercion functions} *) diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index c1e4d72e3..d7ab2d71e 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -31,7 +31,7 @@ let check_alias key = KNmap.mem key !alias_map (** ML tactic extensions (TacML) *) type ml_tactic = - typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic + Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic module MLName = struct diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 47d9efda5..28fb13881 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -61,7 +61,7 @@ val ltac_entries : unit -> ltac_entry KNmap.t (** {5 ML tactic extensions} *) type ml_tactic = - typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic + Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic (** Type of external tactics, used by [TacML]. *) val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic array -> unit diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3295b932b..1760341d1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -43,25 +43,44 @@ open Taccoerce open Sigma.Notations open Proofview.Notations +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 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 pr_argument_type arg = + let Val.Dyn (tag, _) = arg in + Pp.str (Val.repr tag) + let safe_msgnl s = Proofview.NonLogical.catch (Proofview.NonLogical.print_debug (s++fnl())) (fun _ -> Proofview.NonLogical.print_warning (str "bug in the debugger: an exception is raised while printing debug information"++fnl())) -type value = tlevel generic_argument +type value = Val.t (** Abstract application, to print ltac functions *) type appl = | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.kernel_name * typed_generic_argument list) list + | GlbAppl of (Names.kernel_name * Val.t list) list (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with | UnnamedAppl -> UnnamedAppl | GlbAppl l -> GlbAppl (List.map (fun (h,vs) -> (h,vs@args)) l) -let pr_generic arg = - try Pptactic.pr_top_generic (Global.env ()) arg - with e when Errors.noncritical e -> str"<generic>" +let pr_generic arg = (** FIXME *) + let Val.Dyn (tag, _) = arg in + str"<" ++ str (Val.repr tag) ++ str ">" let pr_appl h vs = Pptactic.pr_ltac_constant h ++ spc () ++ Pp.prlist_with_sep spc pr_generic vs @@ -123,8 +142,25 @@ module Value = struct let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in of_tacvalue closure + let cast_error wit v = + let pr_v = mt () in (** FIXME *) + let Val.Dyn (tag, _) = v in + let tag = Val.repr tag in + errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ str tag + ++ str " while type " ++ Genarg.pr_argument_type wit ++ str " was expected.") + + let cast wit v = + try val_cast wit v with CastError (wit, v) -> cast_error wit v + end +let print_top_val env arg v = + let unpacker wit cst = + try val_cast (topwit wit) v; mt () + with CastError _ -> mt () + in + unpack { unpacker } arg + let dloc = Loc.ghost let catching_error call_trace fail (e, info) = @@ -176,13 +212,13 @@ let pr_value env v = | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c | _ -> str "a term" else - str "a value of type" ++ spc () ++ pr_argument_type (genarg_tag v) + str "a value of type" ++ spc () ++ pr_argument_type v let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in let pr_sep () = fnl () in let pr_iarg (id, arg) = - let arg = pr_argument_type (genarg_tag arg) in + let arg = pr_argument_type arg in hov 0 (pr_id id ++ spc () ++ str ":" ++ spc () ++ arg) in let pp_iargs = v 0 (prlist_with_sep pr_sep pr_iarg (Id.Map.bindings ist)) in @@ -199,7 +235,7 @@ let pr_inspect env expr result = | VRec (ist, body) -> str "a recursive closure" ++ fnl () ++ pr_closure env !ist body else - let pp_type = pr_argument_type (genarg_tag result) in + let pp_type = pr_argument_type result in str "an object of type" ++ spc () ++ pp_type in pp_expr ++ fnl() ++ str "this is " ++ pp_result @@ -809,7 +845,7 @@ let rec message_of_value v = Ftactic.List.map message_of_value l >>= fun l -> Ftactic.return (prlist_with_sep spc (fun x -> x) l) | None -> - let tag = pr_argument_type (genarg_tag v) in + let tag = pr_argument_type v in Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *) let interp_message_token ist = function @@ -1095,7 +1131,7 @@ let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c let pack_sigma (sigma,c) = {it=c;sigma=sigma;} (* Interprets an l-tac expression into a value *) -let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : typed_generic_argument Ftactic.t = +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 [value_interp]. It is installed in the second step by a call to [name_vfun], because it gives more opportunities to detect a @@ -1224,53 +1260,48 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let env = Proofview.Goal.env gl in match tag with | IntOrVarArgType -> - Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)) + Ftactic.return (mk_int_or_var_value ist (Genarg.out_gen (glbwit wit_int_or_var) x)) | IdentArgType -> Ftactic.return (value_of_ident (interp_ident ist env sigma - (out_gen (glbwit wit_ident) x))) + (Genarg.out_gen (glbwit wit_ident) x))) | VarArgType -> - Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x)) - | GenArgType -> f (out_gen (glbwit wit_genarg) x) + Ftactic.return (mk_hyp_value ist env sigma (Genarg.out_gen (glbwit wit_var) x)) + | GenArgType -> f (Genarg.out_gen (glbwit wit_genarg) x) | OpenConstrArgType -> let (sigma,v) = - Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x))) gl in + Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (Genarg.out_gen (glbwit wit_open_constr) x))) gl in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v) | ConstrMayEvalArgType -> let (sigma,c_interp) = interp_constr_may_eval ist env sigma - (out_gen (glbwit wit_constr_may_eval) x) + (Genarg.out_gen (glbwit wit_constr_may_eval) x) in Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp)) | ListArgType VarArgType -> let wit = glbwit (wit_list wit_var) in - Ftactic.return ( - let ans = List.map (mk_hyp_value ist env sigma) (out_gen wit x) in - in_gen (topwit (wit_list wit_genarg)) ans - ) + let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in + Ftactic.return (Value.of_list ans) | ListArgType IntOrVarArgType -> let wit = glbwit (wit_list wit_int_or_var) in - let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in - Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) + let ans = List.map (mk_int_or_var_value ist) (Genarg.out_gen wit x) in + Ftactic.return (Value.of_list ans) | ListArgType IdentArgType -> let wit = glbwit (wit_list wit_ident) in let mk_ident x = value_of_ident (interp_ident ist env sigma x) in - let ans = List.map mk_ident (out_gen wit x) in - Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans) + let ans = List.map mk_ident (Genarg.out_gen wit x) in + Ftactic.return (Value.of_list ans) | ListArgType t -> let open Ftactic in let list_unpacker wit l = - let map x = - f (in_gen (glbwit wit) x) >>= fun v -> - Ftactic.return (out_gen (topwit wit) v) - in + let map x = f (Genarg.in_gen (glbwit wit) x) in Ftactic.List.map map (glb l) >>= fun l -> - Ftactic.return (in_gen (topwit (wit_list wit)) l) + Ftactic.return (Value.of_list l) in list_unpack { list_unpacker } x | ExtraArgType _ -> (** Special treatment of tactics *) - if has_type x (glbwit wit_tactic) then - let tac = out_gen (glbwit wit_tactic) x in + if Genarg.has_type x (glbwit wit_tactic) then + let tac = Genarg.out_gen (glbwit wit_tactic) x in val_interp ist tac else let goal = Proofview.Goal.goal gl in @@ -1294,9 +1325,10 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.lift (tactic_of_value ist v) in let tac = - Ftactic.with_env interp_vars >>= fun (env,l) -> - let name () = Pptactic.pr_tactic env (TacAlias(loc,s,l)) in - Proofview.Trace.name_tactic name (tac l) + Ftactic.with_env interp_vars >>= fun (env, lr) -> + let l = List.map2 (fun (_, g) (_, t) -> print_top_val env g t) l lr in + let name () = Pptactic.pr_alias_gen (fun x -> x) 0 s l in + Proofview.Trace.name_tactic name (tac lr) (* spiwack: this use of name_tactic is not robust to a change of implementation of [Ftactic]. In such a situation, some more elaborate solution will have to be used. *) @@ -1317,7 +1349,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with let goal = Evar.unsafe_of_int (-1) in (* /dummy values *) let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in - let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in + let l = List.map2 (print_top_val env) l args in + let name () = Pptactic.pr_extend_gen (fun x -> x) 0 opn l in Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) | TacML (loc,opn,l) -> @@ -1334,12 +1367,13 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma in Proofview.Unsafe.tclEVARS sigma <*> - let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in + let l = List.map2 (print_top_val env) l args in + let name () = Pptactic.pr_extend_gen (fun x -> x) 0 opn l in Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist)) end } -and force_vrec ist v : typed_generic_argument Ftactic.t = +and force_vrec ist v : Val.t Ftactic.t = let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then let v = to_tacvalue v in @@ -1348,7 +1382,7 @@ and force_vrec ist v : typed_generic_argument Ftactic.t = | v -> Ftactic.return (of_tacvalue v) else Ftactic.return v -and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument Ftactic.t = +and interp_ltac_reference loc' mustbetac ist r : Val.t Ftactic.t = match r with | ArgVar (loc,id) -> let v = @@ -1368,7 +1402,7 @@ and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument Ftactic. let appl = GlbAppl[r,[]] in val_interp ~appl ist (Tacenv.interp_ltac r) -and interp_tacarg ist arg : typed_generic_argument Ftactic.t = +and interp_tacarg ist arg : Val.t Ftactic.t = match arg with | TacGeneric arg -> Ftactic.nf_enter begin fun gl -> @@ -1428,7 +1462,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t = | Tacexp t -> val_interp ist t (* Interprets an application node *) -and interp_app loc ist fv largs : typed_generic_argument Ftactic.t = +and interp_app loc ist fv largs : Val.t Ftactic.t = let (>>=) = Ftactic.bind in let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in let fv = Value.normalize fv in @@ -1607,22 +1641,22 @@ and interp_genarg ist env sigma concl gl x = match genarg_tag x with | IntOrVarArgType -> in_gen (topwit wit_int_or_var) - (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x))) + (ArgArg (interp_int_or_var ist (Genarg.out_gen (glbwit wit_int_or_var) x))) | IdentArgType -> in_gen (topwit wit_ident) - (interp_ident ist env sigma (out_gen (glbwit wit_ident) x)) + (interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x)) | VarArgType -> - in_gen (topwit wit_var) (interp_hyp ist env sigma (out_gen (glbwit wit_var) x)) + in_gen (topwit wit_var) (interp_hyp ist env sigma (Genarg.out_gen (glbwit wit_var) x)) | GenArgType -> - in_gen (topwit wit_genarg) (interp_genarg (out_gen (glbwit wit_genarg) x)) + interp_genarg (Genarg.out_gen (glbwit wit_genarg) x) | ConstrArgType -> let (sigma,c_interp) = - interp_constr ist env !evdref (out_gen (glbwit wit_constr) x) + interp_constr ist env !evdref (Genarg.out_gen (glbwit wit_constr) x) in evdref := sigma; in_gen (topwit wit_constr) c_interp | ConstrMayEvalArgType -> - let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (out_gen (glbwit wit_constr_may_eval) x) in + let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (Genarg.out_gen (glbwit wit_constr_may_eval) x) in evdref := sigma; in_gen (topwit wit_constr_may_eval) c_interp | OpenConstrArgType -> @@ -1630,7 +1664,7 @@ and interp_genarg ist env sigma concl gl x = in_gen (topwit wit_open_constr) (interp_open_constr ~expected_type ist env !evdref - (snd (out_gen (glbwit wit_open_constr) x))) + (snd (Genarg.out_gen (glbwit wit_open_constr) x))) | ListArgType ConstrArgType -> let (sigma,v) = interp_genarg_constr_list ist env !evdref x in evdref := sigma; @@ -1638,26 +1672,24 @@ and interp_genarg ist env sigma concl gl x = | ListArgType VarArgType -> interp_genarg_var_list ist env sigma x | ListArgType _ -> let list_unpacker wit l = - let map x = - out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x)) - in - in_gen (topwit (wit_list wit)) (List.map map (glb l)) + let map x = interp_genarg (Genarg.in_gen (glbwit wit) x) in + Value.of_list (List.map map (glb l)) in list_unpack { list_unpacker } x | OptArgType _ -> let opt_unpacker wit o = match glb o with - | None -> in_gen (topwit (wit_opt wit)) None + | None -> Value.of_option None | Some x -> - let x = out_gen (topwit wit) (interp_genarg (in_gen (glbwit wit) x)) in - in_gen (topwit (wit_opt wit)) (Some x) + let x = interp_genarg (Genarg.in_gen (glbwit wit) x) in + Value.of_option (Some x) in opt_unpack { opt_unpacker } x | PairArgType _ -> let pair_unpacker wit1 wit2 o = let (p, q) = glb o in - let p = out_gen (topwit wit1) (interp_genarg (in_gen (glbwit wit1) p)) in - let q = out_gen (topwit wit2) (interp_genarg (in_gen (glbwit wit2) q)) in - in_gen (topwit (wit_pair wit1 wit2)) (p, q) + let p = interp_genarg (Genarg.in_gen (glbwit wit1) p) in + let q = interp_genarg (Genarg.in_gen (glbwit wit2) q) in + Val.Dyn (pair_val, (p, q)) in pair_unpack { pair_unpacker } x | ExtraArgType s -> @@ -1682,14 +1714,16 @@ and global_genarg = fun x -> global_tag (genarg_tag x) and interp_genarg_constr_list ist env sigma x = - let lc = out_gen (glbwit (wit_list wit_constr)) x in + let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in let (sigma,lc) = interp_constr_list ist env sigma lc in - sigma , in_gen (topwit (wit_list wit_constr)) lc + let lc = List.map Value.of_constr lc in + sigma , Value.of_list lc and interp_genarg_var_list ist env sigma x = - let lc = out_gen (glbwit (wit_list wit_var)) x in + let lc = Genarg.out_gen (glbwit (wit_list wit_var)) x in let lc = interp_hyp_list ist env sigma lc in - in_gen (topwit (wit_list wit_var)) lc + let lc = List.map (fun id -> Val.Dyn (val_tag (topwit wit_var), id)) lc in + Value.of_list lc (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist e : constr Ftactic.t = @@ -2344,8 +2378,8 @@ let interp_redexp env sigma r = let _ = let eval ty env sigma lfun arg = let ist = { lfun = lfun; extra = TacStore.empty; } in - if has_type arg (glbwit wit_tactic) then - let tac = out_gen (glbwit wit_tactic) arg in + if Genarg.has_type arg (glbwit wit_tactic) then + let tac = Genarg.out_gen (glbwit wit_tactic) arg in let tac = interp_tactic ist tac in Pfedit.refine_by_tactic env sigma ty tac else diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 88802bf35..c67aa31a9 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -16,13 +16,14 @@ open Misctypes module Value : sig - type t = tlevel generic_argument + type t = 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 end (** Values for interpretation *) @@ -56,7 +57,7 @@ val get_debug : unit -> debug_info (* spiwack: the [Term.constr] argument is the conclusion of the goal, for "casted open constr" *) val interp_genarg : interp_sign -> Environ.env -> Evd.evar_map -> Term.constr -> Goal.goal -> - glob_generic_argument -> Evd.evar_map * typed_generic_argument + glob_generic_argument -> Evd.evar_map * Value.t (** Interprets any expression *) val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 537d10dd5..3aa9d6d79 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -59,7 +59,7 @@ let wit_tauto_flags : tauto_flags uniform_genarg_type = let assoc_flags ist = let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in - try Genarg.out_gen (topwit wit_tauto_flags) v with _ -> assert false + try Value.cast (topwit wit_tauto_flags) v with _ -> assert false (* Whether inner not are unfolded *) let negation_unfolding = ref true @@ -310,7 +310,7 @@ let simplif ist = let t_simplif = tacticIn simplif "simplif" let tauto_intuit flags t_reduce solver = - let flags = Genarg.in_gen (topwit wit_tauto_flags) flags in + let flags = Genarg.Val.Dyn (Genarg.val_tag (topwit wit_tauto_flags), flags) in let lfun = make_lfun [("t_solver", solver); ("tauto_flags", flags)] in let ist = { default_ist () with lfun = lfun; } in let vars = [Id.of_string "t_solver"] in |