Commit faf5d3e0 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: convert formulas to boolean terms

parent 25b47bc9
......@@ -803,8 +803,11 @@ let ps_equ =
let t_equ t1 t2 = ps_app ps_equ [t1; t2]
let t_neq t1 t2 = t_not (ps_app ps_equ [t1; t2])
let fs_true = create_fsymbol (id_fresh "True") [] ty_bool
let fs_false = create_fsymbol (id_fresh "False") [] ty_bool
let fs_bool_true = create_fsymbol (id_fresh "True") [] ty_bool
let fs_bool_false = create_fsymbol (id_fresh "False") [] ty_bool
let t_bool_true = fs_app fs_bool_true [] ty_bool
let t_bool_false = fs_app fs_bool_false [] ty_bool
let fs_tuple_ids = Hid.create 17
......
......@@ -294,8 +294,11 @@ val t_neq : term -> term -> term
val t_equ_simp : term -> term -> term
val t_neq_simp : term -> term -> term
val fs_true : lsymbol
val fs_false: lsymbol
val fs_bool_true : lsymbol
val fs_bool_false : lsymbol
val t_bool_true : term
val t_bool_false : term
val fs_tuple : int -> lsymbol (* n-tuple *)
val t_tuple : term list -> term
......
......@@ -762,7 +762,7 @@ let create_theory ?(path=[]) n =
let bool_theory =
let uc = empty_theory (id_fresh "Bool") [] in
let uc = add_data_decl uc [ts_bool, [fs_true,[]; fs_false,[]]] in
let uc = add_data_decl uc [ts_bool, [fs_bool_true,[]; fs_bool_false,[]]] in
close_theory uc
let highord_theory =
......
......@@ -510,6 +510,9 @@ let e_plapp pls el ity =
| vtv::vtvl, ({ e_node = Elogic t } as e)::argl ->
let tvs = add_expr_tvs tvs e in
let regs = add_expr_regs regs e in
let t = match t.t_ty with
| Some _ -> t
| None -> t_if t t_bool_true t_bool_false in
let evtv = match e.e_vty with
| VTvalue vtv -> vtv
| VTarrow _ -> assert false 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