Commit f5a07e19 authored by Sylvain Dailler's avatar Sylvain Dailler

Adding a known_id function for prineter in Ident.

Adding a forgeting function for printing variables on exceptions.
Should do the same at least for patterns.
Adding printing functions from why3printer.
Changing exception in transformation so that they
return terms not strings.
parent e0d6b38d
......@@ -219,6 +219,12 @@ let create_ident_printer ?(sanitizer = same) sl =
sanitizer = sanitizer;
blacklist = sl }
let known_id printer id =
try
(let _ = Hid.find printer.values id in true)
with Not_found ->
false
let id_unique printer ?(sanitizer = same) id =
try
Hid.find printer.values id
......
......@@ -127,6 +127,10 @@ val id_unique_label :
val string_unique : ident_printer -> string -> string
(** Uniquify string *)
val known_id: ident_printer -> ident -> bool
(** Returns true if the printer already knows the id.
false if it does not. *)
val forget_id : ident_printer -> ident -> unit
(** forget an ident *)
......
......@@ -729,9 +729,9 @@ let callback_update_tree_transform cont status =
| [] -> ())
| _ -> ()
end;
| TSfailed e ->
message_zone#buffer#set_text
(Pp.sprintf "%a" Exn_printer.exn_printer e)
| TSfailed (id, e) ->
message_zone#buffer#set_text
(Pp.sprintf "%a" (get_exception_message cont.controller_session id) e)
| _ -> ()
let rec apply_transform cont t args =
......
......@@ -95,6 +95,20 @@ let rec print_ty_node inn tables fmt ty = match ty.ty_node with
let print_ty = print_ty_node false
let print_vsty tables fmt v =
fprintf fmt "%a:@,%a" (print_vs tables) v (print_ty tables) v.vs_ty
(** Forgetting function for stability of errors *)
let print_forget_vsty tables fmt v =
if (Ident.known_id tables.printer v.vs_name) then
fprintf fmt "%a:@,%a" (print_vs tables) v (print_ty tables) v.vs_ty
else
begin
fprintf fmt "%a:@,%a" (print_vs tables) v (print_ty tables) v.vs_ty;
forget_var tables v
end
(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
let rec lookup v ty = match ty.ty_node with
......@@ -132,9 +146,6 @@ let rec print_pat_node pri tables fmt p = match p.pat_node with
let print_pat = print_pat_node 0
let print_vsty tables fmt v =
fprintf fmt "%a:@,%a" (print_vs tables) v (print_ty tables) v.vs_ty
let print_const = Pretty.print_const
let print_quant = Pretty.print_quant
let print_binop = Pretty.print_binop
......
val print_decl: Task.name_tables -> Format.formatter -> Decl.decl -> unit
(*
TODO not implemented yet as forgetting functions.
TODO only vars implemented as forgetting. We assume it is
not necessary for others.
When printing for errors reporting, we can have to print things that
are not already in the task. So, printing those things will change
the printer.
Lets say that "tac" is a transformation that fails on "task" and that
the error message is about a new variable "n". Then if you call "tac"
several times on the same "task" (which is possible), you will get
error messages with "n1" then "n2" then "n3" then...
So we have these functions that should print elements inside term/variable...
And they should forget the new printed things they just created.
So the function printing all these should then forget all the ids that were
recorded after it has printed everything.
*)
open Ident
val print_ls : Task.name_tables -> Format.formatter -> Term.lsymbol -> unit
val print_tv : Task.name_tables -> Format.formatter -> Ty.tvsymbol -> unit
val print_ts : Task.name_tables -> Format.formatter -> Ty.tysymbol -> unit
val print_forget_vsty : Task.name_tables -> Format.formatter -> Term.vsymbol -> unit
val print_pr : Task.name_tables -> Format.formatter -> Decl.prsymbol -> unit
val print_pat : Task.name_tables -> Format.formatter -> Term.pattern -> unit
val print_ty : Task.name_tables -> Format.formatter -> Ty.ty -> unit
val print_term : Task.name_tables -> Format.formatter -> Term.term -> unit
val print_decl : Task.name_tables -> Format.formatter -> Decl.decl -> unit
......@@ -35,7 +35,7 @@ let print_status fmt st =
| Uninstalled pr -> fprintf fmt "Prover %a is uninstalled" Whyconf.print_prover pr
type transformation_status =
| TSscheduled | TSdone of transID | TSfailed of exn
| TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
let print_trans_status fmt st =
match st with
......@@ -437,7 +437,7 @@ let schedule_transformation_r c id name args ~callback =
begin
match subtasks with
| [t'] when Task.task_equal t' task ->
callback (TSfailed Noprogress)
callback (TSfailed (id, Noprogress))
| _ ->
let tid = graft_transf c.controller_session id name args subtasks in
callback (TSdone tid)
......@@ -446,7 +446,7 @@ let schedule_transformation_r c id name args ~callback =
(* Format.eprintf
"@[Exception raised in Trans.apply_transform %s:@ %a@.@]"
name Exn_printer.exn_printer e; TODO *)
callback (TSfailed e)
callback (TSfailed (id, e))
end;
false
in
......
......@@ -26,7 +26,10 @@ type proof_attempt_status =
val print_status : Format.formatter -> proof_attempt_status -> unit
type transformation_status = TSscheduled | TSdone of transID | TSfailed of exn
type transformation_status =
TSscheduled
| TSdone of transID
| TSfailed of (proofNodeID * exn)
val print_trans_status : Format.formatter -> transformation_status -> unit
......
......@@ -451,3 +451,173 @@ let parse_prover_name config name args :
limit_steps = 0})
| _ -> (*Format.eprintf "Parse_prover_name. Should not happen. Please report@."; *) None
end
(****** Exception handling *********)
let print_term s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_term tables fmt t
let print_type s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ty tables fmt t
let print_ts s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ts tables fmt t
let print_ls s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_ls tables fmt t
let print_tv s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_tv tables fmt t
let print_vsty s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_forget_vsty tables fmt t
let print_pr s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pr tables fmt t
let print_pat s id fmt t =
let tables = match (Session_itp.get_tables s id) with
| None -> Args_wrapper.build_name_tables (Session_itp.get_task s id)
| Some tables -> tables in
Why3printer.print_pat tables fmt t
(* Exception reporting *)
(* TODO remove references to id.id_string in this function *)
let bypass_pretty s id =
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
| Ty.BadTypeArity ({Ty.ts_args = []} as ts, _) ->
fprintf fmt "Type symbol %a expects no arguments" (print_ts s id) 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
| Ty.DuplicateTypeVar tv ->
fprintf fmt "Type variable %a is used twice" (print_tv s id) tv
| Ty.UnboundTypeVar tv ->
fprintf fmt "Unbound type variable: %a" (print_tv s id) 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
| 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
| Term.EmptyCase ->
fprintf fmt "Empty match expression"
| Term.DuplicateVar vs ->
fprintf fmt "Variable %a is used twice" (print_vsty s id) vs
| Term.UncoveredVar vs ->
fprintf fmt "Variable %a uncovered in \"or\"-pattern" (print_vsty s id) vs
| Term.FunctionSymbolExpected ls ->
fprintf fmt "Not a function symbol: %a" (print_ls s id) ls
| Term.PredicateSymbolExpected ls ->
fprintf fmt "Not a predicate symbol: %a" (print_ls s id) 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
| Term.TermExpected t ->
fprintf fmt "Not a term: %a" (print_term s id) t
| Term.FmlaExpected t ->
fprintf fmt "Not a formula: %a" (print_term s id) 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
| Pattern.NonExhaustive pl ->
fprintf fmt "Pattern not covered by a match:@\n @[%a@]"
(print_pat s id) (List.hd pl)
| Decl.BadConstructor ls ->
fprintf fmt "Bad constructor: %a" (print_ls s id) ls
| Decl.BadRecordField ls ->
fprintf fmt "Not a record field: %a" (print_ls s id) ls
| Decl.RecordFieldMissing (_cs,ls) ->
fprintf fmt "Field %a is missing" (print_ls s id) ls
| Decl.DuplicateRecordField (_cs,ls) ->
fprintf fmt "Field %a is used twice in the same constructor" (print_ls s id) ls
| Decl.IllegalTypeAlias ts ->
fprintf fmt
"Type symbol %a is a type alias and cannot be declared as algebraic"
(print_ts s id) ts
| Decl.NonFoundedTypeDecl ts ->
fprintf fmt "Cannot construct a value of type %a" (print_ts s id) 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
| Decl.InvalidIndDecl (_ls, pr) ->
fprintf fmt "Ill-formed inductive clause %a"
(print_pr s id) 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
| 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
| Decl.UnboundVar vs ->
fprintf fmt "Unbound variable: %a" (print_vsty s id) 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
| Decl.EmptyIndDecl ls ->
fprintf fmt "Inductive predicate %a has no constructors" (print_ls s id) ls
| Decl.KnownIdent id ->
fprintf fmt "Ident %s is already declared" id.Ident.id_string
| Decl.UnknownIdent id ->
fprintf fmt "Ident %s is not yet declared" id.Ident.id_string
| Decl.RedeclaredIdent 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
| _ -> Format.fprintf fmt "Uncaught: %a" Exn_printer.exn_printer exn
end
let get_exception_message ses id fmt e =
match e with
| Case.Arg_trans_type (s, ty1, ty2) ->
Format.fprintf fmt "Error in transformation %s during unification of the following terms:\n %a \n %a"
s (print_type ses id) ty1 (print_type ses id) ty2
| Case.Arg_trans_term (s, t1, t2) ->
Format.fprintf fmt "Error in transformation %s during unification of following two terms:\n %a \n %a" s
(print_term ses id) t1 (print_term ses id) t2
| Case.Arg_trans (s) ->
Format.fprintf fmt "Error in transformation function: %s \n" s
| Case.Arg_hyp_not_found (s) ->
Format.fprintf fmt "Following hypothesis was not found: %s \n" s
| Args_wrapper.Arg_theory_not_found (s) ->
Format.fprintf fmt "Theory not found: %s" s
| e ->
bypass_pretty ses id fmt e
......@@ -8,21 +8,10 @@ open Args_wrapper
open Reduction_engine
exception Arg_trans of string
exception Arg_trans_term of (string * string * string)
exception Arg_trans_type of (string * string * string)
exception Arg_trans_term of (string * Term.term * Term.term)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_hyp_not_found of string
exception Arg_bad_hypothesis of (string * string)
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Arg_trans_type (s, s1, s2) ->
Format.fprintf fmt "Error in transformation %s during unification of the following terms:\n %s \n %s" s s1 s2
| Arg_trans_term (s, s1, s2) ->
Format.fprintf fmt "Error in transformation %s during unification of following two terms:\n %s \n %s" s s1 s2
| Arg_trans (s) -> Format.fprintf fmt "Error in transformation function: %s \n" s
| Arg_hyp_not_found (s) -> Format.fprintf fmt "Following hypothesis was not found: %s \n" s
| Arg_theory_not_found (s) -> Format.fprintf fmt "Theory not found: %s" s
| e -> raise e)
exception Arg_bad_hypothesis of (string * Term.term)
let debug_matching = Debug.register_info_flag "print_match"
~desc:"Print@ terms@ that@ were@ not@ successfully@ matched@ by@ ITP@ tactic@ apply."
......@@ -68,9 +57,7 @@ let subst_quant c tq x : term =
t_quant_close c tl tr new_t)
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("subst_quant",
Pp.string_of Pretty.print_ty ty1,
Pp.string_of Pretty.print_ty ty2)))
raise (Arg_trans_type ("subst_quant", ty1, ty2)))
| [] -> failwith "subst_quant: Should not happen, please report")
(* Transform the term (exists v, f) into f[x/v] *)
......@@ -180,7 +167,7 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
(if (Debug.test_flag debug_matching) then
Format.printf "Term %a and %a can not be matched. Failure in matching@."
Pretty.print_term t1 Pretty.print_term t2
else ()); raise (Arg_trans_term ("apply", Pp.string_of Pretty.print_term t1, Pp.string_of Pretty.print_term t2))
else ()); raise (Arg_trans_term ("apply", t1, t2))
| Reduction_engine.NoMatch None -> raise (Arg_trans ("apply"))
in
let inst_nt = t_subst subst nt in
......@@ -190,9 +177,7 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
(create_prsymbol (gen_ident "G")) ng)) nlp in
lt
else
raise (Arg_trans_term ("apply",
Pp.string_of Pretty.print_term inst_nt,
Pp.string_of Pretty.print_term g)))
raise (Arg_trans_term ("apply", inst_nt, g)))
(*(Format.printf
"Term %a and %a are not equal. Failure in matching @."
......@@ -265,7 +250,7 @@ let rewrite_in rev h h1 =
| Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
(* Support to rewrite from the right *)
if rev then (t1, t2) else (t2, t1)
| _ -> raise (Arg_bad_hypothesis ("rewrite", Pp.string_of Pretty.print_term f))) in
| _ -> raise (Arg_bad_hypothesis ("rewrite", f))) in
Some (lp, lv, t1, t2)
| _ -> acc) None in
(* Return instantiated premises and the hypothesis correctly rewritten *)
......@@ -310,9 +295,7 @@ let rewrite rev h h1 = Trans.bind (find_target_prop h1) (rewrite_in (not rev) h)
(* Replace occurences of t1 with t2 in h *)
let replace t1 t2 h =
if not (Ty.ty_equal (t_type t1) (t_type t2)) then
raise (Arg_trans_term ("replace",
Pp.string_of Pretty.print_term t1,
Pp.string_of Pretty.print_term t2))
raise (Arg_trans_term ("replace", t1, t2))
else
(* Create a new goal for equality of the two terms *)
let g = Decl.create_prop_decl Decl.Pgoal (create_prsymbol (gen_ident "G")) (t_app_infer ps_equ [t1; t2]) in
......@@ -409,9 +392,7 @@ let destruct pr : Task.task Trans.tlist =
[[d; x_decl; new_decl]]
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("destruct_exists",
Pp.string_of Pretty.print_ty ty1,
Pp.string_of Pretty.print_ty ty2)))
raise (Arg_trans_type ("destruct_exists", ty1, ty2)))
| [] -> raise (Arg_trans ("destruct_exists"))
end
| _ -> raise (Arg_trans ("destruct"))
......
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