diff options
| -rw-r--r-- | grammar/tacextend.mlp | 142 | ||||
| -rw-r--r-- | grammar/vernacextend.mlp | 16 | ||||
| -rw-r--r-- | intf/extend.ml | 9 | ||||
| -rw-r--r-- | lib/genarg.ml | 13 | ||||
| -rw-r--r-- | lib/genarg.mli | 3 | ||||
| -rw-r--r-- | plugins/ltac/g_eqdecide.ml4 | 1 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 76 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.mli | 19 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 135 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 12 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 98 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 8 | ||||
| -rw-r--r-- | plugins/nsatz/g_nsatz.ml4 | 1 |
13 files changed, 309 insertions, 224 deletions
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 6c072e36a..525be6432 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -13,15 +13,6 @@ open Q_util open Argextend -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>) - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - let plugin_name = <:expr< __coq_plugin_name >> let mlexpr_of_ident id = @@ -29,112 +20,33 @@ let mlexpr_of_ident id = let id = "$" ^ id in <:expr< Names.Id.of_string_soft $str:id$ >> -let rec make_patt = function - | [] -> <:patt< [] >> - | ExtNonTerminal (_, Some p) :: l -> - <:patt< [ $lid:p$ :: $make_patt l$ ] >> - | _::l -> make_patt l - -let rec make_let raw e = function - | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> - | ExtNonTerminal (g, Some p) :: l -> - let t = type_of_user_symbol g in - let loc = MLast.loc_of_expr e in - 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< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in - <:expr< let $lid:p$ = $v$ in $e$ >> - | _::l -> make_let raw e l - -let make_clause (pt,e) = - (make_patt pt, - ploc_vala None, - make_let false e pt) - -let make_fun_clauses loc s l = - let map c = make_fun loc [make_clause c] in - mlexpr_of_list map l - -let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> - let rec mlexpr_of_symbol = function -| Ulist1 s -> <:expr< Extend.Ulist1 $mlexpr_of_symbol s$ >> -| Ulist1sep (s,sep) -> <:expr< Extend.Ulist1sep $mlexpr_of_symbol s$ $str:sep$ >> -| Ulist0 s -> <:expr< Extend.Ulist0 $mlexpr_of_symbol s$ >> -| Ulist0sep (s,sep) -> <:expr< Extend.Ulist0sep $mlexpr_of_symbol s$ $str:sep$ >> -| Uopt s -> <:expr< Extend.Uopt $mlexpr_of_symbol s$ >> +| Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> +| Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> +| Ulist0 s -> <:expr< Extend.TUlist0 $mlexpr_of_symbol s$ >> +| Ulist0sep (s,sep) -> <:expr< Extend.TUlist0sep $mlexpr_of_symbol s$ $str:sep$ >> +| Uopt s -> <:expr< Extend.TUopt $mlexpr_of_symbol s$ >> | Uentry e -> - let arg = get_argt <:expr< $lid:"wit_"^e$ >> in - <:expr< Extend.Uentry (Genarg.ArgT.Any $arg$) >> + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentry (Genarg.get_arg_tag $wit$) >> | Uentryl (e, l) -> assert (e = "tactic"); - let arg = get_argt <:expr< Tacarg.wit_tactic >> in - <:expr< Extend.Uentryl (Genarg.ArgT.Any $arg$) $mlexpr_of_int l$>> - -let make_prod_item = function - | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >> - | ExtNonTerminal (g, id) -> - <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >> - -let mlexpr_of_clause cl = - mlexpr_of_list (fun (a,_) -> mlexpr_of_list make_prod_item a) cl - -(** Special treatment of constr entries *) -let is_constr_gram = function -| ExtTerminal _ -> false -| ExtNonTerminal (Uentry "constr", _) -> true -| _ -> false - -let make_var = function - | ExtNonTerminal (_, p) -> p - | _ -> assert false - -let declare_tactic loc tacname ~level clause = match clause with -| [(ExtTerminal name) :: rem, tac] when List.for_all is_constr_gram rem -> - (** The extension is only made of a name followed by constr entries: we do not - add any grammar nor printing rule and add it as a true Ltac definition. *) - let patt = make_patt rem in - let vars = List.map make_var rem in - let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in - let entry = mlexpr_of_string tacname in - let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in - let name = mlexpr_of_string name in - let tac = match rem with - | [] -> - (** Special handling of tactics without arguments: such tactics do not do - a Proofview.Goal.nf_enter to compute their arguments. It matters for some - whole-prof tactics like [shelve_unifiable]. *) - <:expr< fun _ $lid:"ist"$ -> $tac$ >> - | _ -> - let f = make_fun loc [patt, ploc_vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in - <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> - in - (** Arguments are not passed directly to the ML tactic in the TacML node, - the ML tactic retrieves its arguments in the [ist] environment instead. - This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) - let body = <:expr< Tacexpr.TacFun ($vars$, Tacexpr.TacML (Loc.tag ( $ml$ , []))) >> in - let name = <:expr< Names.Id.of_string $name$ >> in - declare_str_items loc - [ <:str_item< do { - let obj () = Tacenv.register_ltac True False $name$ $body$ in - let () = Tacenv.register_ml_tactic $se$ [|$tac$|] in - Mltop.declare_cache_obj obj $plugin_name$ } >> - ] -| _ -> - (** Otherwise we add parsing and printing rules to generate a call to a - TacML tactic. *) - let entry = mlexpr_of_string tacname in - let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in - let gl = mlexpr_of_clause clause in - let level = mlexpr_of_int level in - let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in - declare_str_items loc - [ <:str_item< do { - Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$); - Mltop.declare_cache_obj $obj$ $plugin_name$; } >> - ] + let wit = <:expr< $lid:"wit_"^e$ >> in + <:expr< Extend.TUentryl (Genarg.get_arg_tag $wit$) $mlexpr_of_int l$>> + +let rec mlexpr_of_clause = function +| [] -> <:expr< TyNil >> +| ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> +| ExtNonTerminal(g,None) :: cl -> + <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >> +| ExtNonTerminal(g,Some id) :: cl -> + <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >> + +let rec binders_of_clause e = function +| [] -> <:expr< fun ist -> $e$ >> +| ExtNonTerminal(_,None) :: cl -> binders_of_clause e cl +| ExtNonTerminal(_,Some id) :: cl -> <:expr< fun $lid:id$ -> $binders_of_clause e cl$ >> +| _ :: cl -> binders_of_clause e cl open Pcaml @@ -146,13 +58,17 @@ EXTEND OPT "|"; l = LIST1 tacrule SEP "|"; "END" -> let level = match level with Some i -> int_of_string i | None -> 0 in - declare_tactic loc s ~level l ] ] + let level = mlexpr_of_int level in + let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in + declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ] ; tacrule: [ [ "["; l = LIST1 tacargs; "]"; - "->"; "["; e = Pcaml.expr; "]" -> (l,e) + "->"; "["; e = Pcaml.expr; "]" -> + <:expr< TyML($mlexpr_of_clause l$, $binders_of_clause e l$) >> ] ] ; + tacargs: [ [ e = LIDENT; "("; s = LIDENT; ")" -> let e = parse_user_entry e "" in diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 24ee0042b..a2872d07f 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -12,7 +12,6 @@ open Q_util open Argextend -open Tacextend type rule = { r_head : string option; @@ -27,6 +26,21 @@ type rule = { (** Whether this entry is deprecated *) } +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>) + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) + +let rec make_patt = function + | [] -> <:patt< [] >> + | ExtNonTerminal (_, Some p) :: l -> + <:patt< [ $lid:p$ :: $make_patt l$ ] >> + | _::l -> make_patt l + let rec make_let e = function | [] -> e | ExtNonTerminal (g, Some p) :: l -> diff --git a/intf/extend.ml b/intf/extend.ml index 10c9b3dc1..734b859f6 100644 --- a/intf/extend.ml +++ b/intf/extend.ml @@ -85,6 +85,15 @@ type 'a user_symbol = | Uentry of 'a | Uentryl of 'a * int +type ('a,'b,'c) ty_user_symbol = +| TUlist1 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol +| TUlist1sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0 : ('a,'b,'c) ty_user_symbol -> ('a list,'b list,'c list) ty_user_symbol +| TUlist0sep : ('a,'b,'c) ty_user_symbol * string -> ('a list,'b list,'c list) ty_user_symbol +| TUopt : ('a,'b,'c) ty_user_symbol -> ('a option, 'b option, 'c option) ty_user_symbol +| TUentry : ('a, 'b, 'c) Genarg.ArgT.tag -> ('a,'b,'c) ty_user_symbol +| TUentryl : ('a, 'b, 'c) Genarg.ArgT.tag * int -> ('a,'b,'c) ty_user_symbol + (** {5 Type-safe grammar extension} *) type ('self, 'a) symbol = diff --git a/lib/genarg.ml b/lib/genarg.ml index cf3a2bee7..209d1b271 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -174,19 +174,22 @@ sig val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option end +let get_arg_tag = function +| ExtraArg s -> s +| _ -> assert false + module Register (M : GenObj) = struct module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end) let arg0_map = ref GenMap.empty - let register0 arg f = match arg with - | ExtraArg s -> + let register0 arg f = + let s = get_arg_tag arg in if GenMap.mem s !arg0_map then let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) ++ str "." in CErrors.anomaly msg else arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map - | _ -> assert false let get_obj0 name = try @@ -199,8 +202,6 @@ struct (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) - let obj t = match t with - | ExtraArg s -> get_obj0 s - | _ -> assert false + let obj t = get_obj0 @@ get_arg_tag t end diff --git a/lib/genarg.mli b/lib/genarg.mli index d49cb334a..bb85f99e3 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -159,6 +159,9 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type This is boilerplate code used here and there in the code of Coq. *) +val get_arg_tag : ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c) ArgT.tag +(** Works only on base objects (ExtraArg), otherwise fails badly. *) + module type GenObj = sig type ('raw, 'glb, 'top) obj diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index b3bcc9984..2251a6620 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -15,6 +15,7 @@ (************************************************************************) open Eqdecide +open Stdarg DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4665ff9ed..2c7ebb745 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -16,6 +16,7 @@ open Misctypes open Genarg open Stdarg open Geninterp +open Pp exception CannotCoerceTo of string @@ -94,6 +95,38 @@ let to_option v = prj Val.typ_opt v let to_pair v = prj Val.typ_pair v +let cast_error wit v = + let pr_v = Pptactic.pr_value Pptactic.ltop v in + let Val.Dyn (tag, _) = v in + let tag = Val.pr tag in + CErrors.user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag + ++ 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 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 -> cast_error t v + | Some Refl -> x +let rec tag_of_arg : type a b c. (a, b, c) genarg_type -> c Val.tag = fun wit -> match wit with +| ExtraArg _ -> Geninterp.val_tag (topwit 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 val_cast arg v = prj (tag_of_arg arg) v + +let cast (Topwit wit) v = val_cast wit v + end let is_variable env id = @@ -334,3 +367,46 @@ let coerce_to_int_or_var_list v = | Some l -> let map n = ArgArg (coerce_to_int n) in List.map map l + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +(* Values for interpretation *) +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = + let wit = Genarg.create_arg "tacvalue" in + let () = register_val0 wit None in + let () = Genprint.register_val_print0 (base_val_typ wit) + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in + wit + +let pr_argument_type arg = + let Val.Dyn (tag, _) = arg in + Val.pr tag + +(** TODO: unify printing of generic Ltac values in case of coercion failure. *) + +(* Displays a value *) +let pr_value env v = + let pr_with_env pr = + match env with + | Some (env,sigma) -> pr env sigma + | None -> str "a value of type" ++ spc () ++ pr_argument_type v in + let open Genprint in + match generic_val_print v with + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) + +let error_ltac_variable ?loc id env v s = + CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++ + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + strbrk "which cannot be coerced to " ++ str s ++ str".") diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index ce05d70e8..1fa5e3c07 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -42,6 +42,7 @@ sig val to_list : t -> t list option val to_option : t -> t option option val to_pair : t -> (t * t) option + val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a end (** {5 Coercion functions} *) @@ -92,3 +93,21 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type + +val error_ltac_variable : ?loc:Loc.t -> Id.t -> + (Environ.env * Evd.evar_map) option -> Value.t -> string -> 'a + +(** Abstract application, to print ltac functions *) +type appl = + | UnnamedAppl (** For generic applications: nothing is printed *) + | GlbAppl of (Names.KerName.t * Val.t list) list + (** For calls to global constants, some may alias other. *) + +type tacvalue = + | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + Name.t list * Tacexpr.glob_tactic_expr + | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr + +val wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type + +val pr_value : (Environ.env * Evd.evar_map) option -> Geninterp.Val.t -> Pp.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 42f2abd73..566fc2873 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -554,3 +554,138 @@ let () = AnyEntry Pltac.tactic_arg; ] in register_grammars_by_name "tactic" entries + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu -> + match tu with + | TUlist1 l -> Ulist1(untype_user_symbol l) + | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s) + | TUlist0 l -> Ulist0(untype_user_symbol l) + | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s) + | TUopt(o) -> Uopt(untype_user_symbol o) + | TUentry a -> Uentry (Genarg.ArgT.Any a) + | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i) + +let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list = + fun sign -> match sign with + | TyNil -> [] + | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' + | TyArg ((loc,(a,id)),sig') -> + TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg ((loc,a),sig') -> + TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + +let clause_of_ty_ml = function + | TyML (t,_) -> clause_of_sign t + +let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function + | TUentry a -> ExtraArg a + | TUentryl (a,l) -> ExtraArg a + | TUopt(o) -> OptArg (prj o) + | TUlist1 l -> ListArg (prj l) + | TUlist1sep (l,_) -> ListArg (prj l) + | TUlist0 l -> ListArg (prj l) + | TUlist0sep (l,_) -> ListArg (prj l) + +let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = + fun sign tac -> + match sign with + | TyNil -> + begin fun vals ist -> match vals with + | [] -> tac ist + | _ :: _ -> assert false + end + | TyIdent (s, sig') -> eval_sign sig' tac + | TyArg ((_loc,(a,id)), sig') -> + let f = eval_sign sig' in + begin fun tac vals ist -> match vals with + | [] -> assert false + | v :: vals -> + let v' = Taccoerce.Value.cast (topwit (prj a)) v in + f (tac v') vals ist + end tac + | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + +let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function + | TyML (t,tac) -> eval_sign t tac + +let is_constr_entry = function +| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr +| _ -> false + +let rec only_constr : type a. a ty_sig -> bool = function +| TyNil -> true +| TyIdent(_,_) -> false +| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false + +let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function +| TyNil -> [] +| TyIdent (_,s) -> mk_sign_vars s +| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s +| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s + +let dummy_id = Id.of_string "_" + +let lift_constr_tac_to_ml_tac vars tac = + let tac _ ist = Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Tacmach.New.project gl in + let map = function + | Anonymous -> None + | Name id -> + let c = Id.Map.find id ist.Geninterp.lfun in + try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c) + with Taccoerce.CannotCoerceTo ty -> + Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty + in + let args = List.map_filter map vars in + tac args ist + end in + tac + +let tactic_extend plugin_name tacname ~level sign = + let open Tacexpr in + let ml_tactic_name = + { mltac_tactic = tacname; + mltac_plugin = plugin_name } + in + match sign with + | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s -> + (** The extension is only made of a name followed by constr entries: we do not + add any grammar nor printing rule and add it as a true Ltac definition. *) + (* + let patt = make_patt rem in + let vars = List.map make_var rem in + let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in + *) + let vars = mk_sign_vars s in + let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in + let tac = match s with + | TyNil -> eval ml_tac + (** Special handling of tactics without arguments: such tactics do not do + a Proofview.Goal.nf_enter to compute their arguments. It matters for some + whole-prof tactics like [shelve_unifiable]. *) + | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac) + in + (** Arguments are not passed directly to the ML tactic in the TacML node, + the ML tactic retrieves its arguments in the [ist] environment instead. + This is the rôle of the [lift_constr_tac_to_ml_tac] function. *) + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true false id body in + let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in + Mltop.declare_cache_obj obj plugin_name + | _ -> + let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in + Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); + Mltop.declare_cache_obj obj plugin_name diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 02e2f0f60..3f804ee8d 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -67,3 +67,15 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.reference -> unit (** Display the absolute name of a tactic. *) + +type _ ty_sig = +| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig +| TyIdent : string * 'r ty_sig -> 'r ty_sig +| TyArg : + (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig +| TyAnonArg : + ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + +type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml + +val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index cd9d9bac2..991afe9c6 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -79,9 +79,6 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) -let base_val_typ wit = - match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") - let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -93,11 +90,6 @@ let safe_msgnl s = type value = Val.t -(** Abstract application, to print ltac functions *) -type appl = - | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.KerName.t * Val.t list) list - (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with | UnnamedAppl -> UnnamedAppl @@ -121,19 +113,6 @@ let combine_appl appl1 appl2 = | UnnamedAppl,a | a,UnnamedAppl -> a | GlbAppl l1 , GlbAppl l2 -> GlbAppl (l2@l1) -(* Values for interpretation *) -type tacvalue = - | VFun of appl*ltac_trace * value Id.Map.t * - Name.t list * glob_tactic_expr - | VRec of value Id.Map.t ref * glob_tactic_expr - -let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = - let wit = Genarg.create_arg "tacvalue" in - let () = register_val0 wit None in - let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in - wit - let of_tacvalue v = in_gen (topwit wit_tacvalue) v let to_tacvalue v = out_gen (topwit wit_tacvalue) v @@ -169,39 +148,6 @@ 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 = Pptactic.pr_value Pptactic.ltop v in - let Val.Dyn (tag, _) = v in - let tag = Val.pr tag in - user_err (str "Type error: value " ++ pr_v ++ str " is a " ++ tag - ++ 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 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 -> cast_error t v - | Some Refl -> 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 val_cast arg v = prj (tag_of_arg arg) v - - let cast (Topwit wit) v = val_cast wit v - end let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -233,21 +179,6 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with | None -> DebugOff | Some level -> level -(** TODO: unify printing of generic Ltac values in case of coercion failure. *) - -(* Displays a value *) -let pr_value env v = - let pr_with_env pr = - match env with - | Some (env,sigma) -> pr env sigma - | None -> str "a value of type" ++ spc () ++ pr_argument_type v in - let open Genprint in - match generic_val_print v with - | TopPrinterBasic pr -> pr () - | TopPrinterNeedsContext pr -> pr_with_env pr - | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> - pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) - let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in let pr_sep () = fnl () in @@ -360,15 +291,11 @@ let debugging_exception_step ist signal_anomaly e pp = debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) -let error_ltac_variable ?loc id env v s = - user_err ?loc (str "Ltac variable " ++ Id.print id ++ - strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ - strbrk "which cannot be coerced to " ++ str s ++ str".") - (* Raise Not_found if not in interpretation sign *) let try_interp_ltac_var coerce ist env {loc;v=id} = let v = Id.Map.find id ist.lfun in - try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s + try coerce v with CannotCoerceTo s -> + Taccoerce.error_ltac_variable ?loc id env v s let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid @@ -2090,27 +2017,6 @@ let _ = in Pretyping.register_constr_interp0 wit_tactic eval -(** Used in tactic extension **) - -let dummy_id = Id.of_string "_" - -let lift_constr_tac_to_ml_tac vars tac = - let tac _ ist = Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let map = function - | Anonymous -> None - | Name id -> - let c = Id.Map.find id ist.lfun in - try Some (coerce_to_closed_constr env c) - with CannotCoerceTo ty -> - error_ltac_variable dummy_id (Some (env,sigma)) c ty - in - let args = List.map_filter map vars in - tac args ist - end in - tac - let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 3f3b8e555..bd44bdbea 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -133,13 +133,5 @@ val interp_int : interp_sign -> lident -> int val interp_int_or_var : interp_sign -> int or_var -> int -val error_ltac_variable : ?loc:Loc.t -> Id.t -> - (Environ.env * Evd.evar_map) option -> value -> string -> 'a - -(** Transforms a constr-expecting tactic into a tactic finding its arguments in - the Ltac environment according to the given names. *) -val lift_constr_tac_to_ml_tac : Name.t list -> - (constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic - val default_ist : unit -> Geninterp.interp_sign (** Empty ist with debug set on the current value. *) diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index c8112eaa9..4ac49adb9 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -9,6 +9,7 @@ (************************************************************************) open Ltac_plugin +open Stdarg DECLARE PLUGIN "nsatz_plugin" |