diff options
-rw-r--r-- | dev/top_printers.ml | 23 | ||||
-rw-r--r-- | lib/genarg.ml | 21 | ||||
-rw-r--r-- | lib/genarg.mli | 3 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 74 |
4 files changed, 64 insertions, 57 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e3efd196c..89e2d7ddd 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -348,29 +348,6 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let pploc x = let (l,r) = Loc.unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" -(* extendable tactic arguments *) -let rec pr_argument_type = function - (* Basic types *) - | IntOrVarArgType -> str"int-or-var" - | IdentArgType true -> str"ident" - | IdentArgType false -> str"pattern_ident" - | VarArgType -> str"var" - | RefArgType -> str"ref" - (* Specific types *) - | GenArgType -> str"genarg" - | ConstrArgType -> str"constr" - | ConstrMayEvalArgType -> str"constr-may-eval" - | QuantHypArgType -> str"qhyp" - | OpenConstrArgType _ -> str"open-constr" - | ConstrWithBindingsArgType -> str"constr-with-bindings" - | BindingsArgType -> str"bindings" - | RedExprArgType -> str"redexp" - | ListArgType t -> pr_argument_type t ++ str" list" - | OptArgType t -> pr_argument_type t ++ str" opt" - | PairArgType (t1,t2) -> - str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")" - | ExtraArgType s -> str"\"" ++ str s ++ str "\"" - let pp_argument_type t = pp (pr_argument_type t) let pp_generic_argument arg = diff --git a/lib/genarg.ml b/lib/genarg.ml index 8e18be3d0..98287d184 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -49,6 +49,27 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2 | _ -> false +let rec pr_argument_type = function +| IntOrVarArgType -> str "int_or_var" +| IdentArgType true -> str "ident" +| IdentArgType false -> str "pattern_ident" +| VarArgType -> str "var" +| RefArgType -> str "ref" +| GenArgType -> str "genarg" +| ConstrArgType -> str "constr" +| ConstrMayEvalArgType -> str "constr_may_eval" +| QuantHypArgType -> str "qhyp" +| OpenConstrArgType _ -> str "open_constr" +| ConstrWithBindingsArgType -> str "constr_with_bindings" +| BindingsArgType -> str "bindings" +| RedExprArgType -> str "redexp" +| ListArgType t -> pr_argument_type t ++ spc () ++ str "list" +| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" +| PairArgType (t1, t2) -> + str "("++ pr_argument_type t1 ++ spc () ++ + str "*" ++ spc () ++ pr_argument_type t2 ++ str ")" +| ExtraArgType s -> str s + type ('raw, 'glob, 'top) genarg_type = argument_type type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type diff --git a/lib/genarg.mli b/lib/genarg.mli index b8dd08f96..e2654fcf5 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -210,6 +210,9 @@ type argument_type = val argument_type_eq : argument_type -> argument_type -> bool +val pr_argument_type : argument_type -> Pp.std_ppcmds +(** Print a human-readable representation for a given type. *) + val genarg_tag : 'a generic_argument -> argument_type val unquote : ('a, 'co) abstract_argument_type -> argument_type diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 30813d530..1918ddc0c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -112,24 +112,55 @@ let check_is_value v = | _ -> () else () -(* Displays a value *) -let rec pr_value env v = str "a tactic" +(** TODO: unify printing of generic Ltac values in case of coercion failure. *) +(* Displays a value *) let pr_value env v = let v = Value.normalize v in - if has_type v (topwit wit_tacvalue) then - pr_value env (to_tacvalue v) + if has_type v (topwit wit_tacvalue) then str "a tactic" else if has_type v (topwit wit_constr_context) then let c = out_gen (topwit wit_constr_context) v in - match env with Some env -> pr_lconstr_env env c | _ -> str "a term" + match env with + | Some env -> pr_lconstr_env env c + | _ -> str "a term" else if has_type v (topwit wit_constr) then let c = out_gen (topwit wit_constr) v in - match env with Some env -> pr_lconstr_env env c | _ -> str "a term" + match env with + | Some env -> pr_lconstr_env env c + | _ -> str "a term" else if has_type v (topwit wit_constr_under_binders) then let c = out_gen (topwit wit_constr_under_binders) v in - match env with Some env -> pr_lconstr_under_binders_env env c | _ -> str "a term" + match env with + | Some env -> pr_lconstr_under_binders_env env c + | _ -> str "a term" else - str "an unknown type" (** TODO *) + str "a value of type" ++ spc () ++ pr_argument_type (genarg_tag v) + +let pr_inspect env expr result = + let pp_expr = Pptactic.pr_glob_tactic env expr in + let pp_result = + if has_type result (topwit wit_tacvalue) then + match to_tacvalue result with + | VRTactic _ -> str "a VRTactic" + | VFun (_, il, ul, b) -> + let pp_body = Pptactic.pr_glob_tactic env b in + let pr_sep () = str ", " in + let pr_iarg (id, _) = pr_id id in + let pr_uarg = function + | None -> str "_" + | Some id -> pr_id id + in + let pp_iargs = prlist_with_sep pr_sep pr_iarg (Id.Map.bindings il) in + let pp_uargs = prlist_with_sep pr_sep pr_uarg ul in + str "a VFun with body " ++ fnl() ++ pp_body ++ fnl() ++ + str "instantiated arguments " ++ fnl() ++ pp_iargs ++ fnl () ++ + str "uninstantiated arguments " ++ fnl() ++ pp_uargs + | VRec _ -> str "a VRec" + else + let pp_type = pr_argument_type (genarg_tag result) in + str "an object of type" ++ spc () ++ pp_type + in + pp_expr ++ fnl() ++ str "this is " ++ pp_result (* Transforms an id into a constr if possible, or fails with Not_found *) let constr_of_id env id = @@ -1542,32 +1573,7 @@ and interp_ltac_constr ist gl e = with CannotCoerceTo _ -> errorlabstrm "" (str "Must evaluate to a closed term" ++ fnl() ++ - str "offending expression: " ++ fnl() ++ - Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++ - (if has_type result (topwit wit_tacvalue) then match to_tacvalue result with - | VRTactic _ -> str "VRTactic" - | VFun (_,il,ul,b) -> - (str "VFun with body " ++ fnl() ++ - Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++ - str "instantiated arguments " ++ fnl() ++ - Id.Map.fold - (fun i v s -> str (Id.to_string i) ++ str ", " ++ s) - il (str "") ++ - str "uninstantiated arguments " ++ fnl() ++ - List.fold_right - (fun opt_id s -> - (match opt_id with - Some id -> str (Id.to_string id) - | None -> str "_") ++ str ", " ++ s) - ul (mt())) -(* | VVoid -> str "VVoid" *) -(* | VInteger _ -> str "VInteger" *) -(* | VConstr _ -> str "VConstr" *) -(* | VIntroPattern _ -> str "VIntroPattern" *) -(* | VConstr_context _ -> str "VConstrr_context" *) - | VRec _ -> str "VRec" -(* | VList _ -> str "VList"*) - else str "unknown object") ++ str".") + str "offending expression: " ++ fnl() ++ pr_inspect (pf_env gl) e result) (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac gl = |