Commit 724b99ca authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

ignore f_quant over an empty list of variables

parent b3e92d1d
......@@ -960,7 +960,7 @@ let f_let v t1 f2 =
let t_eps v f = t_eps v (f_abst_single v f)
let f_quant q vl tl f =
let f_quant q vl tl f = if vl = [] then f else
let i = ref (-1) in
let add m v = incr i; Mvs.add v !i m in
let m = List.fold_left add Mvs.empty vl in
......@@ -1248,7 +1248,7 @@ let ps_neq =
create_psymbol (id_fresh "<>") [v; v]
(* FIXME: is it right to do so? *)
let f_app p tl =
let f_app p tl =
if p == ps_neq then f_not (f_app ps_equ tl) else f_app p tl
let f_equ t1 t2 = f_app ps_equ [t1; t2]
......
......@@ -181,7 +181,7 @@ let create_logic ldl =
check_fv fd;
match fd.f_node with
| Fquant (Fforall, fq) -> f_open_quant fq
| _ -> raise (MalformedDefinition fd)
| _ -> ([],[],fd)
in
let check_ax (_,f) =
check_fv f;
......
......@@ -47,7 +47,7 @@ let rec print_term fmt t = match t.t_node with
| Tvar n ->
print_ident fmt n.vs_name
| Tconst _ ->
assert false
fprintf fmt "[const]"
| Tapp (s, tl) ->
fprintf fmt "(%a(%a@,)@ : %a@,@,)"
print_ident s.fs_name (print_list comma print_term) tl
......@@ -118,11 +118,11 @@ let print_vsymbol fmt {vs_name = vs_name; vs_ty = vs_ty} =
let print_logic_decl fmt = function
| Lfunction (fs,None) -> fprintf fmt "logic %a@." print_fsymbol fs
| Lfunction (fs,Some fd) ->
fprintf fmt "logic %a @: %a@." print_ident fs.fs_name
fprintf fmt "logic %a :@ %a@." print_ident fs.fs_name
print_fmla fd
| Lpredicate (fs,None) -> fprintf fmt "logic %a@." print_psymbol fs
| Lpredicate (ps,Some fd) ->
fprintf fmt "logic %a @: %a@." print_ident ps.ps_name
fprintf fmt "logic %a :@ %a@." print_ident ps.ps_name
print_fmla fd
| Linductive _ -> assert false (*TODO*)
......
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