diff options
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 75 |
1 files changed, 54 insertions, 21 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 579acffa..41783faa 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: himsg.ml 11150 2008-06-19 11:38:27Z msozeau $ *) +(* $Id: himsg.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -392,7 +392,7 @@ let explain_cannot_unify env m n = let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str "with" ++ brk(1,1) ++ pn + str "with" ++ brk(1,1) ++ pn ++ str "." let explain_cannot_unify_local env m n subn = let pm = pr_lconstr_env env m in @@ -400,34 +400,31 @@ let explain_cannot_unify_local env m n subn = let psubn = pr_lconstr_env env subn in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ str "with" ++ brk(1,1) ++ pn ++ spc () ++ str "as" ++ brk(1,1) ++ - psubn ++ str " contains local variables" + psubn ++ str " contains local variables." let explain_refiner_cannot_generalize env ty = str "Cannot find a well-typed generalisation of the goal with type: " ++ - pr_lconstr_env env ty + pr_lconstr_env env ty ++ str "." let explain_no_occurrence_found env c id = str "Found no subterm matching " ++ pr_lconstr_env env c ++ str " in " ++ (match id with | Some id -> pr_id id - | None -> str"the current goal") + | None -> str"the current goal") ++ str "." let explain_cannot_unify_binding_type env m n = let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ - str "which should be unifiable with" ++ brk(1,1) ++ pn + str "which should be unifiable with" ++ brk(1,1) ++ pn ++ str "." let explain_cannot_find_well_typed_abstraction env p l = - let la,lc = list_chop (List.length l - 1) l in str "Abstracting over the " ++ str (plural (List.length l) "term") ++ spc () ++ - hov 0 (prlist_with_sep pr_coma (pr_lconstr_env env) la ++ - (if la<>[] then str " and" ++ spc () else mt()) ++ - pr_lconstr_env env (List.hd lc)) ++ spc () ++ + hov 0 (pr_enum (pr_lconstr_env env) l) ++ spc () ++ str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++ - str "which is ill-typed" + str "which is ill-typed." let explain_type_error env err = let env = make_all_name_different env in @@ -487,11 +484,11 @@ let explain_pretype_error env err = (* Typeclass errors *) let explain_not_a_class env c = - pr_constr_env env c ++ str" is not a declared type class" + pr_constr_env env c ++ str" is not a declared type class." let explain_unbound_method env cid id = str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ str"of class" ++ spc () ++ - pr_global cid + pr_global cid ++ str "." let pr_constr_exprs exprs = hv 0 (List.fold_right @@ -532,7 +529,7 @@ let explain_unsatisfiable_constraints env evd constr = let explain_mismatched_contexts env c i j = str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++ - hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_named_context env j) ++ fnl () ++ brk (1,1) ++ + hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env j) ++ fnl () ++ brk (1,1) ++ hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i) let explain_typeclass_error env err = @@ -549,21 +546,20 @@ let explain_refiner_bad_type arg ty conclty = str "Refiner was given an argument" ++ brk(1,1) ++ pr_lconstr arg ++ spc () ++ str "of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++ - str "instead of" ++ brk(1,1) ++ pr_lconstr conclty + str "instead of" ++ brk(1,1) ++ pr_lconstr conclty ++ str "." let explain_refiner_unresolved_bindings l = - let l = map_succeed (function Name id -> id | _ -> failwith "") l in str "Unable to find an instance for the " ++ str (plural (List.length l) "variable") ++ spc () ++ - prlist_with_sep pr_coma pr_id l + prlist_with_sep pr_coma pr_name l ++ str"." let explain_refiner_cannot_apply t harg = - str "In refiner, a term of type " ++ brk(1,1) ++ + str "In refiner, a term of type" ++ brk(1,1) ++ pr_lconstr t ++ spc () ++ str "could not be applied to" ++ brk(1,1) ++ - pr_lconstr harg + pr_lconstr harg ++ str "." let explain_refiner_not_well_typed c = - str "The term " ++ pr_lconstr c ++ str " is not well-typed" + str "The term " ++ pr_lconstr c ++ str " is not well-typed." let explain_intro_needs_product () = str "Introduction tactics needs products." @@ -706,7 +702,7 @@ let explain_bad_constructor env cstr ind = str "is expected." let decline_string n s = - if n = 0 then "no "^s + if n = 0 then "no "^s^"s" else if n = 1 then "1 "^s else (string_of_int n^" "^s^"s") @@ -781,3 +777,40 @@ let explain_reduction_tactic_error = function str "The abstracted term" ++ spc () ++ pr_lconstr_env_at_top env c ++ spc () ++ str "is not well typed." ++ fnl () ++ explain_type_error env' e + +let explain_ltac_call_trace (last,trace,loc) = + let calls = last :: List.rev (List.map snd trace) in + let pr_call = function + | Proof_type.LtacNotationCall s -> quote (str s) + | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst) + | Proof_type.LtacVarCall (id,t) -> + quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ + Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" + | Proof_type.LtacAtomCall (te,otac) -> quote + (Pptactic.pr_glob_tactic (Global.env()) + (Tacexpr.TacAtom (dummy_loc,te))) + ++ (match !otac with + | Some te' when (Obj.magic te' <> te) -> + strbrk " (expanded to " ++ quote + (Pptactic.pr_tactic (Global.env()) + (Tacexpr.TacAtom (dummy_loc,te'))) + ++ str ")" + | _ -> mt ()) + | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) -> + let filter = + function (id,None) -> None | (id,Some id') -> Some(id,mkVar id') in + let unboundvars = list_map_filter filter unboundvars in + quote (pr_rawconstr_env (Global.env()) c) ++ + (if unboundvars <> [] or vars <> [] then + strbrk " (with " ++ prlist_with_sep pr_coma (fun (id,c) -> + pr_id id ++ str ":=" ++ Printer.pr_lconstr c) + (List.rev vars @ unboundvars) + else mt()) ++ str ")" in + if calls <> [] then + let kind_of_last_call = match list_last calls with + | Proof_type.LtacConstrInterp _ -> ", last term evaluation failed." + | _ -> ", last call failed." in + hov 0 (str "In nested Ltac calls to " ++ + pr_enum pr_call calls ++ strbrk kind_of_last_call) + else + mt () |