Commit a245cfc3 authored by Francois Bobot's avatar Francois Bobot

Ajout d'exception dans Trans que les transformations doivent utiliser

parent f6fbaaa4
......@@ -32,7 +32,7 @@ theory int.Int
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (-_) "(-%1)"
syntax logic (-_) "(- %1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
......
......@@ -6,8 +6,8 @@ prelude ";;; this is a prelude for Z3"
printer "smtv1"
filename "%f-%t-%g.smt"
valid "unsat"
unknown "unknown\\|sat\\|Fail" "Unknown"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
(* À discuter *)
transformation "simplify_recursive_definition"
......@@ -34,7 +34,7 @@ theory int.Int
syntax logic (_+_) "(+ %1 %2)"
syntax logic (_-_) "(- %1 %2)"
syntax logic (_*_) "(* %1 %2)"
syntax logic (-_) "(-%1)"
syntax logic (-_) "(- %1)"
syntax logic (_<=_) "(<= %1 %2)"
syntax logic (_< _) "(< %1 %2)"
......
......@@ -101,3 +101,32 @@ let decl_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) ->
Format.fprintf fmt
"@[<hov 3> The transformation doesn't support this expression :@\n\
%a@\n\
%s@]@\n" Pretty.print_expr e s
| UnsupportedDeclaration (d,s) ->
Format.fprintf fmt
"@[<hov 3> The transformation doesn't support this declaration :@\n\
%a@\n\
%s@]@\n" Pretty.print_decl d s
| NotImplemented (s) ->
Format.fprintf fmt
"@[<hov 3> Unimplemented features :@\n%s@]@\n" s
......@@ -57,3 +57,26 @@ val decl_l : (decl -> decl 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
......@@ -258,6 +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
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let print_th_namespace fmt th =
......
......@@ -70,9 +70,11 @@ let rec print_term drv fmt t = match t.t_node with
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
| Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
| None -> fprintf fmt "@[(%a %a)@]"
print_ident ls.ls_name (print_list space (print_term drv)) tl
end
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
| _ -> fprintf fmt "@[(%a %a)@]"
print_ident ls.ls_name (print_list space (print_term drv)) tl
end end
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
fprintf fmt "@[(let %a = %a@ in %a)@]" print_ident v.vs_name
......@@ -90,9 +92,11 @@ let rec print_fmla drv fmt f = match f.f_node with
print_ident fmt id
| Fapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
| Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
| None -> fprintf fmt "(%a %a)"
print_ident ls.ls_name (print_list space (print_term drv)) tl
end
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| _ -> fprintf fmt "(%a %a)"
print_ident ls.ls_name (print_list space (print_term drv)) tl
end end
| Fquant (q, fq) ->
let q = match q with Fforall -> "forall" | Fexists -> "exists" in
let vl, _tl, f = f_open_quant fq in
......
......@@ -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
| _ -> failwith uncompiled
| _ -> Trans.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
| _ -> failwith uncompiled
| _ -> Trans.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
| _ -> failwith uncompiled
| _ -> Trans.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 _ -> failwith uncompiled
| Tcase _ -> Trans.unsupportedExpression (Term t) uncompiled
| _ -> t_map (rewriteT kn state) (rewriteF kn state) t
and rewriteF kn state f = match f.f_node with
......@@ -76,14 +76,14 @@ and rewriteF kn state f = match f.f_node with
| [{ pat_node = Papp (cs,pl) }] ->
let add_var e p pj = match p.pat_node with
| Pvar v -> f_let v (t_app pj [t1] v.vs_ty) e
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Fmla f) 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
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Fmla f) uncompiled
in
let w,m = List.fold_left mk_br (None,Mls.empty) bl in
let find cs =
......@@ -95,10 +95,10 @@ and rewriteF kn state f = match f.f_node with
in
let ts = match t1.t_ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Fmla f) uncompiled
in
map_join_left find f_and_simp (find_constructors kn ts)
| Fcase _ -> failwith uncompiled
| Fcase _ -> Trans.unsupportedExpression (Fmla f) uncompiled
| _ -> f_map (rewriteT kn state) (rewriteF kn state) f
let add_type (state, task) ts csl =
......
......@@ -55,12 +55,12 @@ let rec add_fd kn task nm ls hd lm e = match e.t_node with
| [{ pat_node = Papp (cs,pl) }] ->
let mk_var p = match p.pat_node with
| Pvar v -> t_var v
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Term t) uncompiled
in
w, Mls.add cs (t_app cs (List.map mk_var pl) v.vs_ty, e) m
| [{ pat_node = Pwild }] ->
Some e, m
| _ -> failwith uncompiled
| _ -> Trans.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 ->
......@@ -71,7 +71,7 @@ let rec add_fd kn task nm ls hd lm e = match e.t_node with
in
let ts = match v.vs_ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Term t) uncompiled
in
let add_cs tsk cs =
let t,e = find cs in
......@@ -99,12 +99,12 @@ let rec add_pd kn task nm ls hd lm e = match e.f_node with
| [{ pat_node = Papp (cs,pl) }] ->
let mk_var p = match p.pat_node with
| Pvar v -> t_var v
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Fmla e) uncompiled
in
w, Mls.add cs (t_app cs (List.map mk_var pl) v.vs_ty, e) m
| [{ pat_node = Pwild }] ->
Some e, m
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Fmla e) 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 ->
......@@ -115,7 +115,7 @@ let rec add_pd kn task nm ls hd lm e = match e.f_node with
in
let ts = match v.vs_ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> failwith uncompiled
| _ -> Trans.unsupportedExpression (Term t) uncompiled
in
let add_cs tsk cs =
let t,e = find cs in
......
......@@ -36,7 +36,7 @@ let exi vl (_,f) =
| Fapp (_,tl) ->
let marry acc v t = f_and_simp acc (f_equ v t) in
List.fold_left2 marry f_true vl tl
| _ -> assert false
| _ -> Trans.unsupportedExpression (Fmla f) "eliminate_inductive"
in
descend f
......
......@@ -208,9 +208,9 @@ let rec rewrite_term tenv tvar vsvar t =
| Tlet (t1, b) -> let u,t2 = t_open_bound b in
let t1' = fnT t1 in let t2' = fnT t2 in
if t1' == t1 && t2' == t2 then t else t_let u t1' t2'
| Tcase _ -> assert false
| Teps _ -> assert false
| Tbvar _ -> assert false
| Tcase _ | Teps _ | Tbvar _ ->
Trans.unsupportedExpression
(Term t) "Encoding decorate : I can't encode this term"
and rewrite_fmla tenv tvar vsvar f =
let fnT = rewrite_term tenv tvar vsvar in
......@@ -268,15 +268,15 @@ let decl (tenv:tenv) d =
Hts.add tenv.trans_tsymbol ts tty;
tty in
[create_logic_decl [(tty,None)]]
| Dtype _ -> failwith ("Encoding_decorate : I can work only on abstract\
type which are not in recursive bloc")
| Dtype _ -> Trans.unsupportedDeclaration
d "encoding_decorate : I can work only on abstract\
type which are not in recursive bloc."
| Dlogic l ->
let fn = function
| _ls, Some _ ->
Format.eprintf "@[<hov 3>Encoding_decorate :@\n\
I can't encode definition such as %a@\n\
Perhaps you could use eliminate_definition@\n@]@." Pretty.print_decl d;
assert false
Trans.unsupportedDeclaration
d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
| ls, None ->
try
let ls = Hls.find tenv.trans_lsymbol ls in
......@@ -286,7 +286,8 @@ Perhaps you could use eliminate_definition@\n@]@." Pretty.print_decl d;
Hls.add tenv.trans_lsymbol ls ls_conv;
ls_conv,None in
[create_logic_decl (List.map fn l)]
| Dind _ -> failwith ("Encoding_decorate : I can't work on inductive")
| Dind _ -> Trans.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 *)
(* [create_ind_decl (List.map fn l)] *)
......
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