diff options
Diffstat (limited to 'contrib/dp/dp_simplify.ml')
| -rw-r--r-- | contrib/dp/dp_simplify.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml index c330b9617..0a7bd0701 100644 --- a/contrib/dp/dp_simplify.ml +++ b/contrib/dp/dp_simplify.ml @@ -66,12 +66,20 @@ let rec print_predicate fmt p = | Exists _ -> assert false (*TODO*) +let rec string_of_type_list = function + | [] -> "" + | e :: l' -> e ^ " -> " ^ (string_of_type_list l') + let print_query fmt (decls,concl) = let print_decl = function - | DeclVar (id, _, _) -> - fprintf fmt "@[;; %s: <var>@]@\n" id - | DeclPred (id, _) -> - fprintf fmt "@[;; %s: <predicate>@]@\n" id + | DeclVar (id, [], t) -> + fprintf fmt "@[;; %s: %s@]@\n" id t + | DeclVar (id, l, t) -> + fprintf fmt "@[;; %s: %s%s@]@\n" + id (string_of_type_list l) t + | DeclPred (id, l) -> + fprintf fmt "@[;; %s: %sBOOLEAN@]@\n" + id (string_of_type_list l) | DeclType id -> fprintf fmt "@[;; %s: TYPE@]@\n" id | Assert (id, f) -> |