Commit 25315953 authored by DAILLER Sylvain's avatar DAILLER Sylvain
Browse files

Merge branch '219_apply2' into 'master'

fix #219 Use snapshot of printers to display messages. Improve error.

Closes #219

See merge request !49
parents cc0497fd 053bf85e
......@@ -254,6 +254,12 @@ let create_ident_printer ?(sanitizer = same) sl =
sanitizer = sanitizer;
blacklist = sl }
let duplicate_ident_printer id_printer =
{id_printer with
indices = Hstr.copy id_printer.indices;
values = Hid.copy id_printer.values;
}
let known_id printer id =
try
(let _ = Hid.find printer.values id in true)
......
......@@ -115,6 +115,13 @@ val create_ident_printer :
?sanitizer : (string -> string) -> string list -> ident_printer
(** start a new printer with a sanitizing function and a blacklist *)
val duplicate_ident_printer: ident_printer -> ident_printer
(** This is used to avoid editing the current (mutable) printer when raising
exception or printing information messages for the user.
This should be avoided for any other usage including display of the whole
task.
*)
val id_unique :
ident_printer -> ?sanitizer : (string -> string) -> ident -> string
(** use ident_printer to generate a unique name for ident
......
......@@ -743,7 +743,7 @@ let schedule_transformation c id name args ~callback ~notification =
| NoProgress ->
(* if result is same as input task, consider it as a failure *)
callback (TSfailed (id, NoProgress))
| (Arg_trans _ | Arg_trans_decl _
| (Arg_trans _ | Arg_trans_decl _ | Arg_trans_missing _
| Arg_trans_term _ | Arg_trans_term2 _
| Arg_trans_pattern _ | Arg_trans_type _ | Arg_bad_hypothesis _
| Cannot_infer_type _ | Unnecessary_terms _ | Parse_error _
......
......@@ -78,132 +78,109 @@ let unproven_goals_below_id cont id =
let p s id =
let _,tables = Session_itp.get_task_name_table s id in
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
(* We use snapshots of printers to avoid registering new values inside it
only for exception messages.
*)
let pr = Ident.duplicate_ident_printer tables.Trans.printer in
let apr = Ident.duplicate_ident_printer tables.Trans.aprinter in
(Pretty.create pr apr pr pr false)
let print_term s id fmt t =
let module P = (val (p s id)) in P.print_term fmt t
let print_type s id fmt t =
let module P = (val (p s id)) in P.print_ty fmt t
let print_opt_type s id fmt t =
let print_opt_type ~print_type fmt t =
match t with
| None -> Format.fprintf fmt "bool"
| Some t -> print_type s id fmt t
let print_ts s id fmt t =
let module P = (val (p s id)) in P.print_ts fmt t
let print_ls s id fmt t =
let module P = (val (p s id)) in P.print_ls fmt t
let print_tv s id fmt t =
let module P = (val (p s id)) in P.print_tv fmt t
let print_vsty s id fmt t =
let module P = (val (p s id)) in P.print_vsty fmt t
let print_pr s id fmt t =
let module P = (val (p s id)) in P.print_pr fmt t
let print_pat s id fmt t =
let module P = (val (p s id)) in P.print_pat fmt t
let print_tdecl s id fmt t =
let module P = (val (p s id)) in P.print_tdecl fmt t
| Some t -> print_type fmt t
(* Exception reporting *)
(* TODO remove references to id.id_string in this function *)
let bypass_pretty s id =
let module P = (val (p s id)) in
begin fun fmt exn -> match exn with
| Ty.TypeMismatch (t1,t2) ->
fprintf fmt "Type mismatch between %a and %a"
(print_type s id) t1 (print_type s id) t2
P.print_ty t1 P.print_ty t2
| Ty.BadTypeArity ({Ty.ts_args = []} as ts, _) ->
fprintf fmt "Type symbol %a expects no arguments" (print_ts s id) ts
fprintf fmt "Type symbol %a expects no arguments" P.print_ts ts
| Ty.BadTypeArity (ts, app_arg) ->
let i = List.length ts.Ty.ts_args in
fprintf fmt "Type symbol %a expects %i argument%s but is applied to %i"
(print_ts s id) ts i (if i = 1 then "" else "s") app_arg
P.print_ts ts i (if i = 1 then "" else "s") app_arg
| Ty.DuplicateTypeVar tv ->
fprintf fmt "Type variable %a is used twice" (print_tv s id) tv
fprintf fmt "Type variable %a is used twice" P.print_tv tv
| Ty.UnboundTypeVar tv ->
fprintf fmt "Unbound type variable: %a" (print_tv s id) tv
fprintf fmt "Unbound type variable: %a" P.print_tv tv
| Ty.UnexpectedProp ->
fprintf fmt "Unexpected propositional type"
| Term.BadArity ({Term.ls_args = []} as ls, _) ->
fprintf fmt "%s %a expects no arguments"
(if ls.Term.ls_value = None then "Predicate" else "Function") (print_ls s id) ls
(if ls.Term.ls_value = None then "Predicate" else "Function") P.print_ls ls
| Term.BadArity (ls, app_arg) ->
let i = List.length ls.Term.ls_args in
fprintf fmt "%s %a expects %i argument%s but is applied to %i"
(if ls.Term.ls_value = None then "Predicate" else "Function")
(print_ls s id) ls i (if i = 1 then "" else "s") app_arg
P.print_ls ls i (if i = 1 then "" else "s") app_arg
| Term.EmptyCase ->
fprintf fmt "Empty match expression"
| Term.DuplicateVar vs ->
fprintf fmt "Variable %a is used twice" (print_vsty s id) vs
fprintf fmt "Variable %a is used twice" P.print_vsty vs
| Term.UncoveredVar vs ->
fprintf fmt "Variable %a uncovered in \"or\"-pattern" (print_vsty s id) vs
fprintf fmt "Variable %a uncovered in \"or\"-pattern" P.print_vsty vs
| Term.FunctionSymbolExpected ls ->
fprintf fmt "Not a function symbol: %a" (print_ls s id) ls
fprintf fmt "Not a function symbol: %a" P.print_ls ls
| Term.PredicateSymbolExpected ls ->
fprintf fmt "Not a predicate symbol: %a" (print_ls s id) ls
fprintf fmt "Not a predicate symbol: %a" P.print_ls ls
| Term.ConstructorExpected ls ->
fprintf fmt "%s %a is not a constructor"
(if ls.Term.ls_value = None then "Predicate" else "Function") (print_ls s id) ls
(if ls.Term.ls_value = None then "Predicate" else "Function") P.print_ls ls
| Term.TermExpected t ->
fprintf fmt "Not a term: %a" (print_term s id) t
fprintf fmt "Not a term: %a" P.print_term t
| Term.FmlaExpected t ->
fprintf fmt "Not a formula: %a" (print_term s id) t
fprintf fmt "Not a formula: %a" P.print_term t
| Pattern.ConstructorExpected (ls,ty) ->
fprintf fmt "%s %a is not a constructor of type %a"
(if ls.Term.ls_value = None then "Predicate" else "Function") (print_ls s id) ls
(print_type s id) ty
(if ls.Term.ls_value = None then "Predicate" else "Function") P.print_ls ls
P.print_ty ty
| Pattern.NonExhaustive pl ->
fprintf fmt "Pattern not covered by a match:@\n @[%a@]"
(print_pat s id) (List.hd pl)
P.print_pat (List.hd pl)
| Decl.BadConstructor ls ->
fprintf fmt "Bad constructor: %a" (print_ls s id) ls
fprintf fmt "Bad constructor: %a" P.print_ls ls
| Decl.BadRecordField ls ->
fprintf fmt "Not a record field: %a" (print_ls s id) ls
fprintf fmt "Not a record field: %a" P.print_ls ls
| Decl.RecordFieldMissing ls ->
fprintf fmt "Field %a is missing" (print_ls s id) ls
fprintf fmt "Field %a is missing" P.print_ls ls
| Decl.DuplicateRecordField ls ->
fprintf fmt "Field %a is used twice in the same constructor" (print_ls s id) ls
fprintf fmt "Field %a is used twice in the same constructor" P.print_ls ls
| Decl.IllegalTypeAlias ts ->
fprintf fmt
"Type symbol %a is a type alias and cannot be declared as algebraic"
(print_ts s id) ts
P.print_ts ts
| Decl.NonFoundedTypeDecl ts ->
fprintf fmt "Cannot construct a value of type %a" (print_ts s id) ts
fprintf fmt "Cannot construct a value of type %a" P.print_ts ts
| Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
fprintf fmt "Constructor %a \
contains a non strictly positive occurrence of type %a"
(print_ls s id) ls (print_type s id) ty
P.print_ls ls P.print_ty ty
| Decl.InvalidIndDecl (_ls, pr) ->
fprintf fmt "Ill-formed inductive clause %a"
(print_pr s id) pr
P.print_pr pr
| Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
fprintf fmt "Inductive clause %a contains \
a non strictly positive occurrence of symbol %a"
(print_pr s id) pr (print_ls s id) ls1
P.print_pr pr P.print_ls ls1
| Decl.BadLogicDecl (ls1,ls2) ->
fprintf fmt "Ill-formed definition: symbols %a and %a are different"
(print_ls s id) ls1 (print_ls s id) ls2
P.print_ls ls1 P.print_ls ls2
| Decl.UnboundVar vs ->
fprintf fmt "Unbound variable:\n%a" (print_vsty s id) vs
fprintf fmt "Unbound variable:\n%a" P.print_vsty vs
| Decl.ClashIdent id ->
fprintf fmt "Ident %s is defined twice" id.Ident.id_string
| Decl.EmptyDecl ->
fprintf fmt "Empty declaration"
| Decl.EmptyAlgDecl ts ->
fprintf fmt "Algebraic type %a has no constructors" (print_ts s id) ts
fprintf fmt "Algebraic type %a has no constructors" P.print_ts ts
| Decl.EmptyIndDecl ls ->
fprintf fmt "Inductive predicate %a has no constructors" (print_ls s id) ls
fprintf fmt "Inductive predicate %a has no constructors" P.print_ls ls
| Decl.KnownIdent id ->
fprintf fmt "Ident %s is already declared" id.Ident.id_string
| Decl.UnknownIdent id ->
......@@ -212,11 +189,12 @@ let bypass_pretty s id =
fprintf fmt "Ident %s is already declared, with a different declaration"
id.Ident.id_string
| Decl.NoTerminationProof ls ->
fprintf fmt "Cannot prove the termination of %a" (print_ls s id) ls
fprintf fmt "Cannot prove the termination of %a" P.print_ls ls
| _ -> Format.fprintf fmt "Uncaught: %a" Exn_printer.exn_printer exn
end
let get_exception_message ses id e =
let module P = (val (p ses id)) in
match e with
| Session_itp.NoProgress ->
Pp.sprintf "Transformation made no progress\n", Loc.dummy_position, ""
......@@ -224,23 +202,27 @@ let get_exception_message ses id e =
Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_decl (s, ld) ->
Pp.sprintf "Error in transformation %s during inclusion of following declarations:\n%a" s
(Pp.print_list (fun fmt () -> Format.fprintf fmt "\n") (print_tdecl ses id)) ld,
(Pp.print_list (fun fmt () -> Format.fprintf fmt "\n") P.print_tdecl) ld,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_term (s, t) ->
Pp.sprintf "Error in transformation %s during with term:\n %a : %a " s
(print_term ses id) t (print_opt_type ses id) t.Term.t_ty,
P.print_term t (print_opt_type ~print_type:P.print_ty) t.Term.t_ty,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_term2 (s, t1, t2) ->
Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a" s
(print_term ses id) t1 (print_opt_type ses id) t1.Term.t_ty
(print_term ses id) t2 (print_opt_type ses id) t2.Term.t_ty,
P.print_term t1 (print_opt_type ~print_type:P.print_ty) t1.Term.t_ty
P.print_term t2 (print_opt_type ~print_type:P.print_ty) t2.Term.t_ty,
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_pattern (s, pa1, pa2) ->
Pp.sprintf "Error in transformation %s during unification of the following terms:\n %a \n %a"
s (print_pat ses id) pa1 (print_pat ses id) pa2, Loc.dummy_position, ""
s P.print_pat pa1 P.print_pat pa2, Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_type (s, ty1, ty2) ->
Pp.sprintf "Error in transformation %s during unification of the following types:\n %a \n %a"
s (print_type ses id) ty1 (print_type ses id) ty2, Loc.dummy_position, ""
s P.print_ty ty1 P.print_ty ty2, Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_trans_missing (s, svs) ->
Pp.sprintf "Error in transformation function: %s %a\n" s
(Pp.print_list Pp.space P.print_vs) (Term.Svs.elements svs),
Loc.dummy_position, ""
| Generic_arg_trans_utils.Arg_bad_hypothesis ("rewrite", _t) ->
Pp.sprintf "Not a rewrite hypothesis", Loc.dummy_position, ""
| Generic_arg_trans_utils.Cannot_infer_type s ->
......@@ -248,7 +230,7 @@ let get_exception_message ses id e =
| Args_wrapper.Arg_qid_not_found q ->
Pp.sprintf "Following hypothesis was not found: %a \n" Typing.print_qualid q, Loc.dummy_position, ""
| Args_wrapper.Arg_pr_not_found pr ->
Pp.sprintf "Property not found: %a" (print_pr ses id) pr, Loc.dummy_position, ""
Pp.sprintf "Property not found: %a" P.print_pr pr, Loc.dummy_position, ""
| Args_wrapper.Arg_error s ->
Pp.sprintf "Transformation raised a general error: %s \n" s, Loc.dummy_position, ""
| Args_wrapper.Arg_theory_not_found s ->
......@@ -261,7 +243,7 @@ let get_exception_message ses id e =
| Generic_arg_trans_utils.Unnecessary_terms l ->
Pp.sprintf "First arguments were parsed and typed correctly but the last following are useless:\n%a"
(Pp.print_list Pp.newline
(fun fmt s -> Format.fprintf fmt "%a" (print_term ses id) s)) l, Loc.dummy_position, ""
(fun fmt s -> Format.fprintf fmt "%a" P.print_term s)) l, Loc.dummy_position, ""
| Args_wrapper.Arg_expected_none s ->
Pp.sprintf "An argument was expected of type %s, none were given" s, Loc.dummy_position, ""
| e ->
......
......@@ -151,8 +151,11 @@ let print_id s tables =
let d = (* Not_found should not happend *)
Ident.Mid.find (symbol_name table_id) km
in
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
(* We use snapshots of printers to avoid registering new value insides it only
to print info messages to the user.
*)
let pr = Ident.duplicate_ident_printer tables.Trans.printer in
let apr = Ident.duplicate_ident_printer tables.Trans.aprinter in
let module P = (val Pretty.create pr apr pr pr false) in
(* Different constructs are printed differently *)
match d.Decl.d_node, table_id with
......@@ -217,11 +220,15 @@ let search ~search_both s tables =
(List.length ids)
(Pp.print_list Pp.space (fun fmt id -> Pp.string fmt id.Ident.id_string))
ids
else let l = Decl.Sdecl.elements l in
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
let module P = (val Pretty.create pr apr pr pr false) in
Pp.string_of (Pp.print_list Pp.newline2 P.print_decl) l
else
let l = Decl.Sdecl.elements l in
(* We use snapshots of printers to avoid registering new value insides it
only to print info messages to the user.
*)
let pr = Ident.duplicate_ident_printer tables.Trans.printer in
let apr = Ident.duplicate_ident_printer tables.Trans.aprinter in
let module P = (val Pretty.create pr apr pr pr false) in
Pp.string_of (Pp.print_list Pp.newline2 P.print_decl) l
let print_id _cont task args =
match args with
......
......@@ -84,9 +84,9 @@ let with_terms ~trans_name subst_ty subst lv withed_terms =
^ " terms in with are useless"))
| _ when diff > 0 ->
Debug.dprintf debug_matching "Not enough withed terms@.";
raise (Arg_trans (trans_name ^ ": there are " ^
raise (Arg_trans_missing (trans_name ^ ": there are " ^
string_of_int diff
^ " terms missing"))
^ " terms missing:", slv))
| _ (* when diff = 0 *) ->
let new_subst_ty, new_subst =
try first_order_matching slv lv withed_terms with
......
......@@ -19,6 +19,7 @@ exception Arg_trans_term of (string * term)
exception Arg_trans_term2 of (string * term * term)
exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_trans_missing of (string * Svs.t)
exception Arg_bad_hypothesis of (string * term)
exception Cannot_infer_type of string
exception Unnecessary_terms of term list
......
......@@ -17,6 +17,7 @@ exception Arg_trans_term of (string * term)
exception Arg_trans_term2 of (string * term * term)
exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_trans_missing of (string * Svs.t)
exception Arg_bad_hypothesis of (string * term)
exception Cannot_infer_type of string
exception Unnecessary_terms of term list
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment