diff options
Diffstat (limited to 'plugins/dp/dp_why.ml')
| -rw-r--r-- | plugins/dp/dp_why.ml | 37 |
1 files changed, 32 insertions, 5 deletions
diff --git a/plugins/dp/dp_why.ml b/plugins/dp/dp_why.ml index 4a1d70d41..9a62f39d0 100644 --- a/plugins/dp/dp_why.ml +++ b/plugins/dp/dp_why.ml @@ -48,6 +48,8 @@ let rec print_typ fmt = function | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x +let print_arg fmt (id,typ) = fprintf fmt "%a: %a" ident id print_typ typ + let rec print_term fmt = function | Cst n -> fprintf fmt "%s" (Big_int.string_of_big_int n) @@ -109,7 +111,30 @@ let rec print_predicate fmt p = | Exists (id, t, p) -> fprintf fmt "@[(exists %a:%a.@ %a)@]" ident id print_typ t pp p +let rec remove_iff args = function + Forall (id,t,p) -> remove_iff ((id,t)::args) p + | Iff(_,b) -> List.rev args, b + | _ -> raise Not_found + let print_query fmt (decls,concl) = + let find_declared_preds l = + function + DeclPred (id,_,args) -> (id,args) :: l + | _ -> l + in + let find_defined_preds declared l = function + Axiom(id,f) -> + (try + let _decl = List.assoc id declared in + (id,remove_iff [] f)::l + with Not_found -> l) + | _ -> l + in + let declared_preds = + List.fold_left find_declared_preds [] decls in + let defined_preds = + List.fold_left (find_defined_preds declared_preds) [] decls + in let print_dtype = function | DeclType (id, 0) -> fprintf fmt "@[type %a@]@\n@\n" ident id @@ -130,15 +155,19 @@ let print_query fmt (decls,concl) = | DeclFun (id, _, l, t) -> fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" ident id (print_list comma print_typ) l print_typ t - | DeclPred (id, _, []) -> + | DeclPred (id, _, []) when not (List.mem_assoc id defined_preds) -> fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id - | DeclPred (id, _, l) -> + | DeclPred (id, _, l) when not (List.mem_assoc id defined_preds) -> fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" ident id (print_list comma print_typ) l - | DeclType _ | Axiom _ -> + | DeclType _ | Axiom _ | DeclPred _ -> () in let print_assert = function + | Axiom(id,_) when List.mem_assoc id defined_preds -> + let args, def = List.assoc id defined_preds in + fprintf fmt "@[predicate %a(%a) =@\n%a@]@\n" ident id + (print_list comma print_arg) args print_predicate def | Axiom (id, f) -> fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f | DeclType _ | DeclFun _ | DeclPred _ -> @@ -155,5 +184,3 @@ let output_file f q = fprintf fmt "include \"real.why\"@."; fprintf fmt "@[%a@]@." print_query q; close_out c - - |