Skip to content

GitLab

why3
why3
Commit 4caec4bf authored by Francois Bobot's avatar Francois Bobot
Browse files
Options

Rassemblement de Trans.Error et Printers_utils.Errror en Register.Error

parent 64bc823c
Hide whitespace changes
Inline Side-by-side
Showing with 135 additions and 203 deletions
Makefile.in
View file @ 4caec4bf
......@@ -108,7 +108,7 @@ LIB_TRANSFORM = simplify_recursive_definition inlining \
eliminate_constructs eliminate_if \
eliminate_definition
LIB_PRINTER = print_real printer_utils alt_ergo why3 smt coq
LIB_PRINTER = print_real alt_ergo why3 smt coq
LIBMODULES = src/config \
$(addprefix src/util/, $(LIB_UTIL)) \
......
src/core/trans.ml
View file @ 4caec4bf
......@@ -117,31 +117,3 @@ let tdecl_l fn =
map_l fn
let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
(** exception to use in a transformation *)
type error =
| UnsupportedExpression of expr * string
| UnsupportedDeclaration of decl * string
| NotImplemented of string
exception Error of error
let error e = raise (Error e)
let unsupportedExpression e s = error (UnsupportedExpression (e,s))
let unsupportedDeclaration e s = error (UnsupportedDeclaration (e,s))
let notImplemented s = error (NotImplemented s)
let report fmt = function
| UnsupportedExpression (e,s) ->
let msg = "The transformation doesn't support this expression" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_expr e s
| UnsupportedDeclaration (d,s) ->
let msg = "The transformation doesn't support this declaration" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_decl d s
| NotImplemented (s) ->
Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
src/core/trans.mli
View file @ 4caec4bf
......@@ -59,25 +59,3 @@ val tdecl : (decl -> tdecl list ) -> task -> task trans
val tdecl_l : (decl -> tdecl list list) -> task -> task tlist
val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
(** exception to use in a transformation *)
type error =
| UnsupportedExpression of expr * string
| UnsupportedDeclaration of decl * string
| NotImplemented of string
exception Error of error
val unsupportedExpression : expr -> string -> 'a
val unsupportedDeclaration : decl -> string -> 'a
(** - [expr] is the problematic formula
- [string] explain the problem and
possibly a way to solve it (such as applying another
transforamtion) *)
val notImplemented : string -> 'a
(** [string] explain what is not implemented *)
val report : Format.formatter -> error -> unit
src/driver/register.ml
View file @ 4caec4bf
......@@ -164,3 +164,60 @@ let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
let list_transforms_l () = Hashtbl.fold (fun k _ acc -> k::acc) transforms_l []
(** exception to use in a printer and transformation *)
open Term
open Decl
open Ty
type error =
| UnsupportedType of ty * string
| UnsupportedExpression of expr * string
| UnsupportedDeclaration of decl * string
| NotImplemented of string
exception Error of error
let error e = raise (Error e)
let unsupportedType e s = error (UnsupportedType (e,s))
let unsupportedExpression e s = error (UnsupportedExpression (e,s))
let unsupportedDeclaration e s = error (UnsupportedDeclaration (e,s))
let notImplemented s = error (NotImplemented s)
let report fmt = function
| UnsupportedType (e,s) ->
let msg = "This type isn't supported" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_ty e s
| UnsupportedExpression (e,s) ->
let msg = "This expression isn't supported" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_expr e s
| UnsupportedDeclaration (d,s) ->
let msg = "This declaration isn't supproted" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_decl d s
| NotImplemented (s) ->
Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
(** function which cath inner error *)
exception Unsupported of string
let unsupported s = raise (Unsupported s)
let catch_unsupportedtype f ty =
try f ty with Unsupported s -> unsupportedType ty s
let catch_unsupportedterm f t =
try f t with Unsupported s -> unsupportedExpression (Term t) s
let catch_unsupportedfmla f t =
try f t with Unsupported s -> unsupportedExpression (Fmla t) s
let catch_unsupportedDeclaration f d =
try f d with Unsupported s -> unsupportedDeclaration d s
src/driver/register.mli
View file @ 4caec4bf
......@@ -17,6 +17,9 @@
(* *)
(**************************************************************************)
(** Register printers and registered transformations, and create
registered transformations *)
open Env
open Task
open Trans
......@@ -38,7 +41,7 @@ val conv_res : ('a -> 'b) -> 'a trans_reg -> 'b trans_reg
val clear : 'a trans_reg -> unit
(** Store and apply *)
(** {2 Store and apply} *)
type query = Driver.driver_query
type clone = Theory.clone_map
......@@ -60,7 +63,7 @@ val apply_driver : 'a trans_reg -> Driver.driver -> task -> 'a
val apply_env : 'a trans_reg -> env -> task -> 'a
val apply : 'a trans_reg -> task -> 'a
(** Registration *)
(** {2 Registration} *)
type printer = query -> Format.formatter -> task -> unit
......@@ -76,3 +79,56 @@ val list_printers : unit -> string list
val list_transforms : unit -> string list
val list_transforms_l : unit -> string list
(** {2 exceptions to use in transformations and printers } *)
type error =
| UnsupportedType of Ty.ty * string
| UnsupportedExpression of Term.expr * string
| UnsupportedDeclaration of Decl.decl * string
| NotImplemented of string
exception Error of error
val unsupportedType : Ty.ty -> string -> 'a
(** [unsupportedType ty s]
- [ty] is the problematic formula
- [s] explain the problem and
possibly a way to solve it (such as applying another
transforamtion) *)
val unsupportedExpression : Term.expr -> string -> 'a
val unsupportedDeclaration : Decl.decl -> string -> 'a
val notImplemented : string -> 'a
(** [notImplemented s]. [s] explains what is not implemented *)
val report : Format.formatter -> error -> unit
(** Pretty print an error *)
(** {3 functions which catch inner error} *)
exception Unsupported of string
(** This exception must be raised only in a inside call of one of the above
catch_* function *)
val unsupported : string -> 'a
(** convenient function to raise the {! Unsupported} exception *)
val catch_unsupportedtype : (Ty.ty -> 'a) -> (Ty.ty -> 'a)
(** [catch_unsupportedtype f] return a function which applied on [arg] :
- return [f arg] if [f arg] doesn't raise the {!
Unsupported} exception.
- raise [unsupportedType (arg,s)] if [f arg] raises [Unsupported s]*)
val catch_unsupportedterm : (Term.term -> 'a) -> (Term.term -> 'a)
(** same as {! catch_unsupportedtype} but raise {!
UnsupportedExpression} instead of {! UnsupportedType}*)
val catch_unsupportedfmla : (Term.fmla -> 'a) -> (Term.fmla -> 'a)
(** same as {! catch_unsupportedtype} but raise {!
UnsupportedExpression} instead of {! UnsupportedType}*)
val catch_unsupportedDeclaration : (Decl.decl -> 'a) -> (Decl.decl -> 'a)
(** same as {! catch_unsupportedtype} but raise {!
UnsupportedDeclaration} instead of {! UnsupportedType}*)
src/main.ml
View file @ 4caec4bf
......@@ -258,10 +258,8 @@ let rec report fmt = function
fprintf fmt "Why config: %a" Whyconf.report e
| Prover.Error e ->
Prover.report fmt e
| Trans.Error e ->
Trans.report fmt e
| Printer_utils.Error e ->
Printer_utils.report fmt e
| Register.Error e ->
Register.report fmt e
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let print_th_namespace fmt th =
......
src/printer/alt_ergo.ml
View file @ 4caec4bf
......@@ -16,7 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Printer_utils
open Register
open Format
open Pp
open Ident
......@@ -204,7 +204,7 @@ let print_task drv fmt task =
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls)
let () = Register.register_printer "alt-ergo"
let () = register_printer "alt-ergo"
(fun drv fmt task ->
forget_all ident_printer;
print_task drv fmt task)
......
src/printer/printer_utils.ml deleted 100644 → 0
View file @ 64bc823c
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Term
open Decl
open Ty
(** exception to use in a printer *)
type error =
| UnsupportedType of ty * string
| UnsupportedExpression of expr * string
| UnsupportedDeclaration of decl * string
| NotImplemented of string
exception Error of error
let error e = raise (Error e)
let unsupportedType e s = error (UnsupportedType (e,s))
let unsupportedExpression e s = error (UnsupportedExpression (e,s))
let unsupportedDeclaration e s = error (UnsupportedDeclaration (e,s))
let notImplemented s = error (NotImplemented s)
let report fmt = function
| UnsupportedType (e,s) ->
let msg = "The printer doesn't support this type" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_ty e s
| UnsupportedExpression (e,s) ->
let msg = "The printer doesn't support this expression" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_expr e s
| UnsupportedDeclaration (d,s) ->
let msg = "The printer doesn't support this declaration" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_decl d s
| NotImplemented (s) ->
Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
(** function which cath inner error *)
exception Unsupported of string
let unsupported s = raise (Unsupported s)
let catch_unsupportedtype f ty =
try f ty with Unsupported s -> unsupportedType ty s
let catch_unsupportedterm f t =
try f t with Unsupported s -> unsupportedExpression (Term t) s
let catch_unsupportedfmla f t =
try f t with Unsupported s -> unsupportedExpression (Fmla t) s
let catch_unsupportedDeclaration f d =
try f d with Unsupported s -> unsupportedDeclaration d s
src/printer/printer_utils.mli deleted 100644 → 0
View file @ 64bc823c
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** Useful functions for printer *)
(** {2 exception to use in a transformation } *)
type error =
| UnsupportedType of Ty.ty * string
| UnsupportedExpression of Term.expr * string
| UnsupportedDeclaration of Decl.decl * string
| NotImplemented of string
exception Error of error
val unsupportedType : Ty.ty -> string -> 'a
val unsupportedExpression : Term.expr -> string -> 'a
val unsupportedDeclaration : Decl.decl -> string -> 'a
(** - [expr] is the problematic formula
- [string] explain the problem and
possibly a way to solve it (such as applying another
transforamtion) *)
val notImplemented : string -> 'a
(** [string] explain what is not implemented *)
val report : Format.formatter -> error -> unit
(** function which cath inner error *)
exception Unsupported of string
val unsupported : string -> 'a
val catch_unsupportedtype : (Ty.ty -> 'a) -> (Ty.ty -> 'a)
val catch_unsupportedterm : (Term.term -> 'a) -> (Term.term -> 'a)
val catch_unsupportedfmla : (Term.fmla -> 'a) -> (Term.fmla -> 'a)
val catch_unsupportedDeclaration : (Decl.decl -> 'a) -> (Decl.decl -> 'a)
src/printer/smt.ml
View file @ 4caec4bf
......@@ -16,8 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Printer_utils
open Register
open Format
open Pp
open Ident
......@@ -201,7 +200,7 @@ let print_task drv fmt task =
ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls);
fprintf fmt "@\n)@."
let () = Register.register_printer "smtv1"
let () = register_printer "smtv1"
(fun drv fmt task ->
forget_all ident_printer;
print_task drv fmt task)
src/transform/eliminate_algebraic.ml
View file @ 4caec4bf
......@@ -46,24 +46,24 @@ let rec rewriteT kn state t = match t.t_node with
| [{ pat_node = Papp (cs,pl) }] ->
let add_var e p pj = match p.pat_node with
| Pvar v -> t_let v (t_app pj [t1] v.vs_ty) e
| _ -> Trans.unsupportedExpression (Term t) uncompiled
| _ -> Register.unsupportedExpression (Term t) uncompiled
in
let pjl = Mls.find cs state.pj_map in
let e = List.fold_left2 add_var e pl pjl in
w, Mls.add cs e m
| [{ pat_node = Pwild }] ->
Some e, m
| _ -> Trans.unsupportedExpression (Term t) uncompiled
| _ -> Register.unsupportedExpression (Term t) uncompiled
in
let w,m = List.fold_left mk_br (None,Mls.empty) bl in
let find cs = try Mls.find cs m with Not_found -> of_option w in
let ts = match t1.t_ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> Trans.unsupportedExpression (Term t) uncompiled
| _ -> Register.unsupportedExpression (Term t) uncompiled
in
let tl = List.map find (find_constructors kn ts) in
t_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
| Tcase _ -> Trans.unsupportedExpression (Term t) uncompiled
| Tcase _ -> Register.unsupportedExpression (Term t) uncompiled
| _ -> t_map (rewriteT kn state) (rewriteF kn state true) t
and rewriteF kn state sign f = match f.f_node with
......@@ -76,12 +76,12 @@ and rewriteF kn state sign f = match f.f_node with
| [{ pat_node = Papp (cs,pl) }] ->
let get_var p = match p.pat_node with
| Pvar v -> v
| _ -> Trans.unsupportedExpression (Fmla f) uncompiled
| _ -> Register.unsupportedExpression (Fmla f) uncompiled
in
w, Mls.add cs (List.map get_var pl, e) m
| [{ pat_node = Pwild }] ->
Some e, m
| _ -> Trans.unsupportedExpression (Fmla f) uncompiled
| _ -> Register.unsupportedExpression (Fmla f) uncompiled
in
let w,m = List.fold_left mk_br (None,Mls.empty) bl in
let find cs =
......@@ -99,11 +99,11 @@ and rewriteF kn state sign f = match f.f_node with
in
let ts = match t1.t_ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> Trans.unsupportedExpression (Fmla f) uncompiled
| _ -> Register.unsupportedExpression (Fmla f) uncompiled
in
let op = if sign then f_and_simp else f_or_simp in
map_join_left find op (find_constructors kn ts)
| Fcase _ -> Trans.unsupportedExpression (Fmla f) uncompiled
| Fcase _ -> Register.unsupportedExpression (Fmla f) uncompiled
| _ -> f_map_sign (rewriteT kn state) (rewriteF kn state) sign f
let add_type (state, task) ts csl =
......
src/transform/eliminate_if.ml
View file @ 4caec4bf
......@@ -36,7 +36,7 @@ let rec elim_t case letl contT t = match t.t_node with
| Tcase _ ->
t_map_cont (elim_t (Some t) letl) elim_f contT t
| Tif _ when case <> None ->
Trans.unsupportedExpression (Term (of_option case))
Register.unsupportedExpression (Term (of_option case))
"cannot eliminate 'if-then-else' under 'match' in terms"
| Tif (f,t1,t2) ->
let f = elim_f (fun f -> f) f in
......
src/transform/encoding_decorate.ml
View file @ 4caec4bf
......@@ -241,7 +241,7 @@ let rec rewrite_term tenv tvar vsvar t =
let t1' = fnT vsvar t1 in let t2' = fnT vsvar t2 in
if t1' == t1 && t2' == t2 then t else t_let u t1' t2'
| Tcase _ | Teps _ | Tbvar _ ->
Trans.unsupportedExpression
Register.unsupportedExpression
(Term t) "Encoding decorate : I can't encode this term"
and rewrite_fmla tenv tvar vsvar f =
......@@ -296,13 +296,13 @@ let decl (tenv:tenv) d =
Hts.add tenv.trans_tsymbol ts tty;
tty in
[create_decl (create_logic_decl [(tty,None)])]
| Dtype _ -> Trans.unsupportedDeclaration
| Dtype _ -> Register.unsupportedDeclaration
d "encoding_decorate : I can work only on abstract\
type which are not in recursive bloc."
| Dlogic l ->
let fn = function
| _ls, Some _ ->
Trans.unsupportedDeclaration
Register.unsupportedDeclaration
d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
| ls, None ->
......@@ -314,7 +314,7 @@ Perhaps you could use eliminate_definition"
Hls.add tenv.trans_lsymbol ls ls_conv;
ls_conv,None in
[create_decl (create_logic_decl (List.map fn l))]
| Dind _ -> Trans.unsupportedDeclaration
| Dind _ -> Register.unsupportedDeclaration
d "encoding_decorate : I can't work on inductive"
(* let fn (pr,f) = pr, fnF f in *)
(* let fn (ps,l) = ps, List.map fn l in *)
......
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