Commit b30c3b94 authored by Laszlo Domoszlai's avatar Laszlo Domoszlai
Browse files

"Taut" works now

parent 39e97e7f
main = Taut.Start
Taut.Start::I = if (Taut.isTaut Taut.testProp) 1 0
Taut.testProp = Taut.Implies (Taut.foldr1 Taut.And (Taut.map Taut.imp Taut.names)) (Taut.Implies (Taut.Var (Flite.char 'q')) (Taut.foldr1 Taut.And (Taut.map Taut.Var Taut.names)))
Taut.names = Flite.str "abcdefghijklmnop"
Flite.str !_x_0 = select _x_0 ("" -> Flite.Nil) (_ -> Flite.Cons (Flite.char (string_select _x_0 0)) (Flite.str (<{StdString.%_10}> _x_0 (_Tuple2 1 (string_size _x_0)))))
<{StdString.%_10}> !str_0 !_x_1 = select _x_1 (_Tuple2 a b -> string_slice str_0 a b)
Flite.char::I !c_0::C = C2I c_0
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
:: Taut.Prop = Taut.Const a1::B | Taut.Var a1::I | Taut.Not a1 | Taut.And a1 a2 | Taut.Implies a1 a2
Taut.map f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons (f_0 x_1_0) (Taut.map f_0 xs_1_1))
Taut.foldr1 f_0 !_x_1 = select _x_1 (Flite.Cons x_1_0 xs_1_1 -> if (Taut.null xs_1_1) x_1_0 (f_0 x_1_0 (Taut.foldr1 f_0 xs_1_1)))
Taut.null::B !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False)
Taut.imp v_0::I = Taut.Implies (Taut.Var (Flite.char 'q')) (Taut.Var v_0)
Taut.isTaut::B !p_0 = Taut.and (Taut.map (Taut.flip Taut.eval p_0) (Taut.substs p_0))
Taut.substs !p_0 = let vs_1_0 = Taut.rmdups_26 (Taut.vars p_0) in Taut.map (Taut.zip vs_1_0) (Taut.bools (Taut.len vs_1_0))
Taut.len::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> addI 1 (Taut.len xs_1_1))
Taut.bools !n_0::I = if (eqI n_0 0) (Flite.Cons Flite.Nil Flite.Nil) (let m_1_0 = subI n_0 1 in Taut.append (Taut.map (Flite.Cons False) (Taut.bools m_1_0)) (Taut.map (Flite.Cons True) (Taut.bools m_1_0)))
Taut.append !_x_0 ys_1 = select _x_0 (Flite.Nil -> ys_1) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons x_1_0 (Taut.append xs_1_1 ys_1))
Taut.zip !_x_0 ys_1 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> select ys_1 (Flite.Nil -> Flite.Nil) (Flite.Cons y_2_0 ys_2_1 -> Flite.Cons (Flite.Pair x_1_0 y_2_0) (Taut.zip xs_1_1 ys_2_1)) )
:: Flite.Pair = Flite.Pair a1 a2
Taut.vars !_x_0 = select _x_0 (Taut.Const b_1_0 -> Flite.Nil) (Taut.Var x_1_0 -> Flite.Cons x_1_0 Flite.Nil) (Taut.Not p_1_0 -> Taut.vars p_1_0) (Taut.And p_1_0 q_1_1 -> Taut.append (Taut.vars p_1_0) (Taut.vars q_1_1)) (Taut.Implies p_1_0 q_1_1 -> Taut.append (Taut.vars p_1_0) (Taut.vars q_1_1))
Taut.rmdups_26 !_x_0 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Flite.Cons x_1_0 (Taut.rmdups_26 (Taut.filter (Taut.neq_27 x_1_0) xs_1_1)))
Taut.neq_27::B !x_0::I !y_1::I = <{Taut./=_28}> x_0 y_1
<{Taut./=_28}>::B !a_0::I !b_1::I = <{Taut.<>_29}> a_0 b_1
<{Taut.<>_29}>::B !x_0::I !y_1::I = not (eqI x_0 y_1)
Taut.filter p_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> if (p_0 x_1_0) (Flite.Cons x_1_0 (Taut.filter p_0 xs_1_1)) (Taut.filter p_0 xs_1_1))
Taut.eval::B s_0 !_x_1 = select _x_1 (Taut.Const b_1_0 -> b_1_0) (Taut.Var x_1_0 -> Taut.find_25 x_1_0 s_0) (Taut.Not p_1_0 -> if (Taut.eval s_0 p_1_0) False True) (Taut.And p_1_0 q_1_1 -> if (Taut.eval s_0 p_1_0) (Taut.eval s_0 q_1_1) False) (Taut.Implies p_1_0 q_1_1 -> if (Taut.eval s_0 p_1_0) (Taut.eval s_0 q_1_1) True)
Taut.find_25 !key_0::I !_x_1 = select _x_1 (Flite.Cons _x_1_0 t_1_1 -> select _x_1_0 (Flite.Pair k_2_0 v_2_1 -> if (eqI key_0 k_2_0) v_2_1 (Taut.find_25 key_0 t_1_1)) )
Taut.flip !f_0 y_1 x_2 = f_0 x_2 y_1
Taut.and::B !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons b_1_0 bs_1_1 -> if b_1_0 (Taut.and bs_1_1) False)
[1]
\ No newline at end of file
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