Skip to content
GitLab
Commit 4ac88b5e authored by Laszlo Domoszlai's avatar Laszlo Domoszlai
Browse files

more tests

parent 26d4142e
Hide whitespace changes
Inline Side-by-side
tests/CountDown.exp 0 → 100644
View file @ 4ac88b5e
[0]
\ No newline at end of file
tests/CountDown.sapl 0 → 100644
View file @ 4ac88b5e
main = CountDown.Start
CountDown.Start::I = CountDown.len (CountDown.solutions (Flite.Cons 1 (Flite.Cons 3 (Flite.Cons 7 (Flite.Cons 10 (Flite.Cons 25 Flite.Nil))))) 765)
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
CountDown.solutions !ns_0 n_1::I = CountDown.concatMap (CountDown.solns n_1) (CountDown.choices ns_0)
CountDown.choices !xs_0 = CountDown.concatMap CountDown.perms (CountDown.subs xs_0)
CountDown.subs !_x_0 = select _x_0 (Flite.Nil -> Flite.Cons Flite.Nil Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> let yss_2_0 = CountDown.subs xs_1_1 in CountDown.append yss_2_0 (CountDown.map (Flite.Cons x_1_0) yss_2_0))
CountDown.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) (CountDown.map f_0 xs_1_1))
CountDown.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 (CountDown.append xs_1_1 ys_1))
CountDown.perms !_x_0 = select _x_0 (Flite.Nil -> Flite.Cons Flite.Nil Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> CountDown.concatMap (CountDown.interleave x_1_0) (CountDown.perms xs_1_1))
CountDown.interleave x_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Cons (Flite.Cons x_0 Flite.Nil) Flite.Nil) (Flite.Cons y_1_0 ys_1_1 -> Flite.Cons (Flite.Cons x_0 (Flite.Cons y_1_0 ys_1_1)) (CountDown.map (Flite.Cons y_1_0) (CountDown.interleave x_0 ys_1_1)))
CountDown.concatMap f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> CountDown.append (f_0 x_1_0) (CountDown.concatMap f_0 xs_1_1))
CountDown.solns n_0::I !ns_1 = CountDown.preImage_47 n_0 (CountDown.results ns_1)
CountDown.results !_x_0 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons n_1_0 ns_1_1 -> if (CountDown.null ns_1_1) (Flite.Cons (Flite.Pair (CountDown.Val n_1_0) n_1_0) Flite.Nil) (CountDown.concatMap CountDown.combinedResults (CountDown.split (Flite.Cons n_1_0 ns_1_1))))
CountDown.split !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> if (CountDown.null xs_1_1) Flite.Nil (Flite.Cons (Flite.Pair (Flite.Cons x_1_0 Flite.Nil) xs_1_1) (CountDown.map (CountDown.cross (Flite.Pair (Flite.Cons x_1_0) CountDown.id)) (CountDown.split xs_1_1))))
CountDown.id !x_0 = x_0
:: Flite.Pair = Flite.Pair a1 a2
CountDown.cross !_x_0 !_x_1 = select _x_0 (Flite.Pair f_1_0 g_1_1 -> select _x_1 (Flite.Pair x_2_0 y_2_1 -> Flite.Pair (f_1_0 x_2_0) (g_1_1 y_2_1)) )
CountDown.null::B !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False)
CountDown.combinedResults !_x_0 = select _x_0 (Flite.Pair ls_1_0 rs_1_1 -> CountDown.concatProdWith CountDown.combine (CountDown.results ls_1_0) (CountDown.results rs_1_1))
CountDown.combine !_x_0 !_x_1 = select _x_0 (Flite.Pair l_1_0 x_1_1 -> select _x_1 (Flite.Pair r_2_0 y_2_1 -> CountDown.concatMap (CountDown.combi l_1_0 x_1_1 r_2_0 y_2_1) (Flite.Cons CountDown.Add (Flite.Cons CountDown.Sub (Flite.Cons CountDown.Mul (Flite.Cons CountDown.Div Flite.Nil))))) )
:: CountDown.Op = CountDown.Add | CountDown.Sub | CountDown.Mul | CountDown.Div
CountDown.combi l_0 x_1::I r_2 y_3::I !o_4 = if (CountDown.valid o_4 x_1 y_3) (Flite.Cons (Flite.Pair (CountDown.App o_4 l_0 r_2) (CountDown.apply o_4 x_1 y_3)) Flite.Nil) Flite.Nil
CountDown.apply::I !_x_0 !x_1::I !y_2::I = select _x_0 (CountDown.Add -> addI x_1 y_2) (CountDown.Sub -> subI x_1 y_2) (CountDown.Mul -> CountDown.mul x_1 y_2) (CountDown.Div -> CountDown.div_46 x_1 y_2)
CountDown.div_46::I !x_0::I !y_1::I = <{CountDown._c;71;11_66}> (CountDown.divMod_43 x_0 y_1)
CountDown.divMod_43 !x_0::I !y_1::I = let y2_1_0 = addI y_1 y_1 in <{CountDown._c;76;14_58}> (<{CountDown.<=_39}> y2_1_0 x_0) x_0 y2_1_0 y_1
<{CountDown.<=_39}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{CountDown._c;76;14_58}> !_x_0::B !x_1::I y2_2::I y_3::I = select _x_0 (True -> <{CountDown._c;77;23_57}> (CountDown.divMod_43 x_1 y2_2) y_3) (False -> if (<{CountDown.<=_41}> y_3 x_1) (Flite.Pair 1 (subI x_1 y_3)) (Flite.Pair 0 x_1))
<{CountDown.<=_41}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{CountDown._c;77;23_57}> !_x_0 !y_1::I = select _x_0 (Flite.Pair d2_1_0 m2_1_1 -> if (<{CountDown.<=_40}> y_1 m2_1_1) (Flite.Pair (addI 1 (addI d2_1_0 d2_1_0)) (subI m2_1_1 y_1)) (Flite.Pair (addI d2_1_0 d2_1_0) m2_1_1))
<{CountDown.<=_40}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{CountDown._c;71;11_66}>::I !_x_0 = select _x_0 (Flite.Pair d_1_0 m_1_1 -> d_1_0)
CountDown.mul::I !x_0::I !n_1::I = <{CountDown._c;89;11_62}> (eqI n_1 1) x_0 n_1
<{CountDown._c;89;11_62}>::I !_x_0::B !x_1::I n_2::I = select _x_0 (True -> x_1) (False -> <{CountDown._c;91;20_61}> (CountDown.divMod_43 n_2 2) x_1)
<{CountDown._c;91;20_61}>::I !_x_0 !x_1::I = select _x_0 (Flite.Pair d_1_0 m_1_1 -> addI (CountDown.mul (addI x_1 x_1) d_1_0) (<{CountDown._c;93;37_60}> (eqI m_1_1 0) x_1))
<{CountDown._c;93;37_60}>::I !_x_0::B x_1::I = select _x_0 (True -> 0) (False -> x_1)
:: CountDown.Expr = CountDown.Val a1::I | CountDown.App a1 a2 a3
CountDown.valid::B !_x_0 x_1::I y_2::I = select _x_0 (CountDown.Add -> True) (CountDown.Sub -> CountDown.inv (<{CountDown.<=_34}> x_1 y_2)) (CountDown.Mul -> True) (CountDown.Div -> eqI (CountDown.modu_42 x_1 y_2) 0)
CountDown.modu_42::I !x_0::I !y_1::I = <{CountDown._c;73;12_59}> (CountDown.divMod_43 x_0 y_1)
<{CountDown._c;73;12_59}>::I !_x_0 = select _x_0 (Flite.Pair d_1_0 m_1_1 -> m_1_1)
<{CountDown.<=_34}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
CountDown.inv::B !_x_0::B = if _x_0 False True
CountDown.concatProdWith f_0 !_x_1 ys_2 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> CountDown.append (CountDown.concatMap (f_0 x_1_0) ys_2) (CountDown.concatProdWith f_0 xs_1_1 ys_2))
CountDown.preImage_47 n_0::I !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons _x_1_0 ems_1_1 -> select _x_1_0 (Flite.Pair e_2_0 m_2_1 -> if (eqI m_2_1 n_0) (Flite.Cons e_2_0 (CountDown.preImage_47 n_0 ems_1_1)) (CountDown.preImage_47 n_0 ems_1_1)) )
CountDown.len::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> addI 1 (CountDown.len xs_1_1))
tests/OrdList.exp 0 → 100644
View file @ 4ac88b5e
[1]
\ No newline at end of file
tests/OrdList.sapl 0 → 100644
View file @ 4ac88b5e
main = OrdList.Start
OrdList.Start::I = <{OrdList._c;46;10_13}> (OrdList.top (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S (OrdList.S OrdList.Z)))))))))))))
:: OrdList.Nat = OrdList.Z | OrdList.S a1
OrdList.top::B !n_0 = OrdList.andList (OrdList.append (OrdList.map (OrdList.prop True) (OrdList.boolList n_0)) (OrdList.map (OrdList.prop False) (OrdList.boolList n_0)))
OrdList.boolList !_x_0 = select _x_0 (OrdList.Z -> OrdList.Cons OrdList.Nil OrdList.Nil) (OrdList.S n_1_0 -> OrdList.append (OrdList.boolList n_1_0) (OrdList.append (OrdList.map (OrdList.Cons False) (OrdList.boolList n_1_0)) (OrdList.map (OrdList.Cons True) (OrdList.boolList n_1_0))))
:: OrdList.List = OrdList.Nil | OrdList.Cons a1 a2
OrdList.map f_0 !_x_1 = select _x_1 (OrdList.Nil -> OrdList.Nil) (OrdList.Cons x_1_0 xs_1_1 -> OrdList.Cons (f_0 x_1_0) (OrdList.map f_0 xs_1_1))
OrdList.append !_x_0 ys_1 = select _x_0 (OrdList.Nil -> ys_1) (OrdList.Cons x_1_0 xs_1_1 -> OrdList.Cons x_1_0 (OrdList.append xs_1_1 ys_1))
OrdList.prop::B x_0::B !xs_1 = OrdList.implies (OrdList.ord xs_1) (OrdList.ord (OrdList.insert x_0 xs_1))
OrdList.insert x_0::B !_x_1 = select _x_1 (OrdList.Nil -> OrdList.Cons x_0 OrdList.Nil) (OrdList.Cons y_1_0 ys_1_1 -> if (OrdList.implies x_0 y_1_0) (OrdList.Cons x_0 (OrdList.Cons y_1_0 ys_1_1)) (OrdList.Cons y_1_0 (OrdList.insert x_0 ys_1_1)))
OrdList.implies::B !_x_0::B x_1::B = if _x_0 x_1 True
OrdList.ord::B !_x_0 = select _x_0 (OrdList.Nil -> True) (OrdList.Cons x_1_0 _x_1_1 -> select _x_1_1 (OrdList.Nil -> True) (OrdList.Cons y_2_0 ys_2_1 -> OrdList.and (OrdList.implies x_1_0 y_2_0) (OrdList.ord (OrdList.Cons y_2_0 ys_2_1))) )
OrdList.and::B !_x_0::B x_1::B = if _x_0 x_1 False
OrdList.andList::B !_x_0 = select _x_0 (OrdList.Nil -> True) (OrdList.Cons x_1_0 xs_1_1 -> OrdList.and x_1_0 (OrdList.andList xs_1_1))
<{OrdList._c;46;10_13}>::I !_x_0::B = select _x_0 (False -> 0) (True -> 1)
tests/Queens1.exp 0 → 100644
View file @ 4ac88b5e
[2680]
\ No newline at end of file
tests/Queens1.sapl 0 → 100644
View file @ 4ac88b5e
main = Queens.Start
Queens.Start::I = Queens.nsoln 11
Queens.nsoln::I !nq_0::I = Queens.len (Queens.gen nq_0 nq_0)
Queens.gen nq_0::I !n_1::I = if (eqI n_1 0) (Flite.Cons Flite.Nil Flite.Nil) (Queens.concatMap (Queens.gen1 nq_0) (Queens.gen nq_0 (subI n_1 1)))
Queens.gen1 !nq_0::I !b_1 = Queens.concatMap (Queens.gen2 b_1) (Queens.toOne nq_0)
Queens.toOne !n_0::I = if (eqI n_0 1) (Flite.Cons 1 Flite.Nil) (Flite.Cons n_0 (Queens.toOne (subI n_0 1)))
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
Queens.gen2 !b_0 q_1::I = if (Queens.safe q_1 1 b_0) (Flite.Cons (Flite.Cons q_1 b_0) Flite.Nil) Flite.Nil
Queens.safe::B x_0::I d_1::I !_x_2 = select _x_2 (Flite.Nil -> True) (Flite.Cons q_1_0 l_1_1 -> Queens.and (<{Queens./=_19}> x_0 q_1_0) (Queens.and (<{Queens./=_21}> x_0 (addI q_1_0 d_1)) (Queens.and (<{Queens./=_23}> x_0 (subI q_1_0 d_1)) (Queens.safe x_0 (addI d_1 1) l_1_1))))
<{Queens./=_23}>::B !a_0::I !b_1::I = <{Queens.<>_24}> a_0 b_1
<{Queens.<>_24}>::B !x_0::I !y_1::I = not (eqI x_0 y_1)
Queens.and::B !_x_0::B a_1::B = if _x_0 a_1 False
<{Queens./=_21}>::B !a_0::I !b_1::I = <{Queens.<>_22}> a_0 b_1
<{Queens.<>_22}>::B !x_0::I !y_1::I = not (eqI x_0 y_1)
<{Queens./=_19}>::B !a_0::I !b_1::I = <{Queens.<>_20}> a_0 b_1
<{Queens.<>_20}>::B !x_0::I !y_1::I = not (eqI x_0 y_1)
Queens.concatMap f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Queens.append (f_0 x_1_0) (Queens.concatMap f_0 xs_1_1))
Queens.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 (Queens.append xs_1_1 ys_1))
Queens.len::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> addI 1 (Queens.len xs_1_1))
tests/Queens2.exp 0 → 100644
View file @ 4ac88b5e
[2680]
\ No newline at end of file
tests/Queens2.sapl 0 → 100644
View file @ 4ac88b5e
main = Queens2.Start
Queens2.Start::I = Queens2.nqueens 11
Queens2.nqueens::I !n_0::I = Queens2.len (Queens2.solve n_0 (Queens2.replicate n_0 Flite.Nil))
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
Queens2.replicate !n_0::I x_1 = if (eqI n_0 0) Flite.Nil (Flite.Cons x_1 (Queens2.replicate (subI n_0 1) x_1))
Queens2.solve !n_0::I mask_1 = if (eqI n_0 0) (Flite.Cons Flite.Nil Flite.Nil) (Queens2.concatMap (Queens2.sol (subI n_0 1)) (Queens2.fill mask_1))
Queens2.fill !_x_0 = select _x_0 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Queens2.append (Queens2.lrd x_1_0 xs_1_1) (Queens2.map (Flite.Cons x_1_0) (Queens2.fill xs_1_1)))
Queens2.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) (Queens2.map f_0 xs_1_1))
Queens2.lrd !_x_0 ys_1 = select _x_0 (Flite.Nil -> Flite.Cons (Flite.Cons (Flite.Cons Queens2.l (Flite.Cons Queens2.r (Flite.Cons Queens2.d Flite.Nil))) ys_1) Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Flite.Nil)
Queens2.d::I = 2
Queens2.r::I = 1
Queens2.l::I = 0
Queens2.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 (Queens2.append xs_1_1 ys_1))
Queens2.sol !n_0::I row_1 = Queens2.map (Flite.Cons row_1) (Queens2.solve n_0 (Queens2.next row_1))
Queens2.next !mask_0 = Queens2.merge (Queens2.merge (Queens2.down mask_0) (Queens2.left mask_0)) (Queens2.right mask_0)
Queens2.right xs_0 = Flite.Cons Flite.Nil (Queens2.map (Queens2.onep (Queens2.eq_22 Queens2.r)) xs_0)
Queens2.eq_22::B !x_0::I !y_1::I = eqI x_0 y_1
Queens2.onep 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 Flite.Nil) (Queens2.onep p_0 xs_1_1))
Queens2.left !xs_0 = Queens2.map (Queens2.onep (Queens2.eq_22 Queens2.l)) (Queens2.tail xs_0)
Queens2.tail !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> xs_1_1)
Queens2.down !xs_0 = Queens2.map (Queens2.onep (Queens2.eq_22 Queens2.d)) xs_0
Queens2.merge !_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.Cons x_1_0 xs_1_1) (Flite.Cons y_2_0 ys_2_1 -> Flite.Cons (Queens2.append x_1_0 y_2_0) (Queens2.merge xs_1_1 ys_2_1)) )
Queens2.concatMap f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Queens2.append (f_0 x_1_0) (Queens2.concatMap f_0 xs_1_1))
Queens2.len::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> addI 1 (Queens2.len xs_1_1))
tests/broken/Clausify.sapl 0 → 100644
View file @ 4ac88b5e
main = Clausify.Start
Clausify.Start::I = let a_1_0 = Clausify.Sym 0 in Clausify.display (Clausify.clausify (Clausify.foldr Clausify.Con a_1_0 (Clausify.replicate 80 (Clausify.eqv (Clausify.eqv a_1_0 (Clausify.eqv a_1_0 a_1_0)) (Clausify.eqv (Clausify.eqv a_1_0 (Clausify.eqv a_1_0 a_1_0)) (Clausify.eqv a_1_0 (Clausify.eqv a_1_0 a_1_0)))))))
Clausify.eqv a_0 b_1 = Clausify.Con (Clausify.Dis (Clausify.Neg a_0) b_1) (Clausify.Dis (Clausify.Neg b_1) a_0)
:: Clausify.P = Clausify.Sym a1::I | Clausify.Neg a1 | Clausify.Con a1 a2 | Clausify.Dis a1 a2
Clausify.replicate !n_0::I a_1 = if (eqI n_0 0) Flite.Nil (Flite.Cons a_1 (Clausify.replicate (subI n_0 1) a_1))
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
Clausify.foldr f_0 z_1 !_x_2 = select _x_2 (Flite.Nil -> z_1) (Flite.Cons x_1_0 xs_1_1 -> f_0 x_1_0 (Clausify.foldr f_0 z_1 xs_1_1))
Clausify.clausify !p_0 = Clausify.uniq_43 (Clausify.nonTaut_39 (Clausify.clauses (Clausify.split (Clausify.disin (Clausify.negin p_0)))))
Clausify.negin !_x_0 = select _x_0 (Clausify.Neg _x_1_0 -> select _x_1_0 (Clausify.Con p_2_0 q_2_1 -> Clausify.Dis (Clausify.negin (Clausify.Neg p_2_0)) (Clausify.negin (Clausify.Neg q_2_1))) (Clausify.Dis p_2_0 q_2_1 -> Clausify.Con (Clausify.negin (Clausify.Neg p_2_0)) (Clausify.negin (Clausify.Neg q_2_1))) (Clausify.Neg p_2_0 -> Clausify.negin p_2_0) (Clausify.Sym s_2_0 -> Clausify.Neg (Clausify.Sym s_2_0)) ) (Clausify.Dis p_1_0 q_1_1 -> Clausify.Dis (Clausify.negin p_1_0) (Clausify.negin q_1_1)) (Clausify.Con p_1_0 q_1_1 -> Clausify.Con (Clausify.negin p_1_0) (Clausify.negin q_1_1)) (Clausify.Sym s_1_0 -> Clausify.Sym s_1_0)
Clausify.disin !_x_0 = select _x_0 (Clausify.Sym s_1_0 -> Clausify.Sym s_1_0) (Clausify.Neg p_1_0 -> Clausify.Neg p_1_0) (Clausify.Con p_1_0 q_1_1 -> Clausify.Con (Clausify.disin p_1_0) (Clausify.disin q_1_1)) (Clausify.Dis p_1_0 q_1_1 -> Clausify.din (Clausify.disin p_1_0) (Clausify.disin q_1_1))
Clausify.din !_x_0 r_1 = select _x_0 (Clausify.Con p_1_0 q_1_1 -> Clausify.Con (Clausify.din p_1_0 r_1) (Clausify.din q_1_1 r_1)) (Clausify.Dis p_1_0 q_1_1 -> Clausify.din2 (Clausify.Dis p_1_0 q_1_1) r_1) (Clausify.Neg p_1_0 -> Clausify.din2 (Clausify.Neg p_1_0) r_1) (Clausify.Sym s_1_0 -> Clausify.din2 (Clausify.Sym s_1_0) r_1)
Clausify.din2 p_0 !_x_1 = select _x_1 (Clausify.Con q_1_0 r_1_1 -> Clausify.Con (Clausify.din p_0 q_1_0) (Clausify.din p_0 r_1_1)) (Clausify.Dis q_1_0 r_1_1 -> Clausify.Dis p_0 (Clausify.Dis q_1_0 r_1_1)) (Clausify.Neg q_1_0 -> Clausify.Dis p_0 (Clausify.Neg q_1_0)) (Clausify.Sym s_1_0 -> Clausify.Dis p_0 (Clausify.Sym s_1_0))
Clausify.split !p_0 = Clausify.spl Flite.Nil p_0
Clausify.spl a_0 !_x_1 = select _x_1 (Clausify.Con p_1_0 q_1_1 -> Clausify.spl (Clausify.spl a_0 p_1_0) q_1_1) (Clausify.Dis p_1_0 q_1_1 -> Flite.Cons (Clausify.Dis p_1_0 q_1_1) a_0) (Clausify.Neg p_1_0 -> Flite.Cons (Clausify.Neg p_1_0) a_0) (Clausify.Sym s_1_0 -> Flite.Cons (Clausify.Sym s_1_0) a_0)
Clausify.clauses !ps_0 = Clausify.map (Clausify.clause (Flite.Pair Flite.Nil Flite.Nil)) ps_0
:: Flite.Pair = Flite.Pair a1 a2
Clausify.clause !_x_0 !_x_1 = select _x_0 (Flite.Pair c_1_0 a_1_1 -> select _x_1 (Clausify.Dis p_2_0 q_2_1 -> Clausify.clause (Clausify.clause (Flite.Pair c_1_0 a_1_1) p_2_0) q_2_1) (Clausify.Sym s_2_0 -> Flite.Pair (Clausify.ins_37 s_2_0 c_1_0) a_1_1) (Clausify.Neg _x_2_0 -> select _x_2_0 (Clausify.Sym s_3_0 -> Flite.Pair c_1_0 (Clausify.ins_37 s_3_0 a_1_1)) ) )
Clausify.ins_37 x_0::I !_x_1 = select _x_1 (Flite.Nil -> Flite.Cons x_0 Flite.Nil) (Flite.Cons y_1_0 ys_1_1 -> if (eqI x_0 y_1_0) (Flite.Cons y_1_0 ys_1_1) (if (<{Clausify.<=_38}> x_0 y_1_0) (Flite.Cons x_0 (Flite.Cons y_1_0 ys_1_1)) (Flite.Cons y_1_0 (Clausify.ins_37 x_0 ys_1_1))))
<{Clausify.<=_38}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
Clausify.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) (Clausify.map f_0 xs_1_1))
Clausify.nonTaut_39 !cs_0 = Clausify.filter Clausify.invTaut_40 cs_0
Clausify.invTaut_40::B !_x_0 = select _x_0 (Flite.Pair c_1_0 a_1_1 -> Clausify.null (Clausify.inter eqI c_1_0 a_1_1))
Clausify.inter eq_0 xs_1 !ys_2 = Clausify.filter (Clausify.contains eq_0 xs_1) ys_2
Clausify.contains::B eq_0 !_x_1 y_2 = select _x_1 (Flite.Nil -> False) (Flite.Cons x_1_0 xs_1_1 -> Clausify.or (eq_0 x_1_0 y_2) (Clausify.contains eq_0 xs_1_1 y_2))
Clausify.or::B !_x_0::B x_1::B = if _x_0 True x_1
Clausify.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 (Clausify.filter p_0 xs_1_1)) (Clausify.filter p_0 xs_1_1))
Clausify.null::B !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False)
Clausify.uniq_43 !xs_0 = Clausify.foldr (Clausify.comp (Clausify.union Clausify.eqClause_44) Clausify.singleton) Flite.Nil xs_0
Clausify.singleton x_0 = Flite.Cons x_0 Flite.Nil
Clausify.eqClause_44::B !_x_0 !_x_1 = select _x_0 (Flite.Pair a_1_0 b_1_1 -> select _x_1 (Flite.Pair c_2_0 d_2_1 -> Clausify.and (Clausify.eqList eqI a_1_0 c_2_0) (Clausify.eqList eqI b_1_1 d_2_1)) )
Clausify.eqList::B f_0 !_x_1 !_x_2 = select _x_1 (Flite.Nil -> select _x_2 (Flite.Nil -> True) (Flite.Cons y_2_0 ys_2_1 -> False) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Nil -> False) (Flite.Cons y_2_0 ys_2_1 -> Clausify.and (f_0 x_1_0 y_2_0) (Clausify.eqList f_0 xs_1_1 ys_2_1)) )
Clausify.and::B !_x_0::B x_1::B = if _x_0 x_1 False
Clausify.union eq_0 !xs_1 ys_2 = Clausify.append xs_1 (Clausify.filter (Clausify.comp Clausify.inv (Clausify.contains eq_0 xs_1)) ys_2)
Clausify.inv::B !_x_0::B = if _x_0 False True
Clausify.comp !f_0 g_1 x_2 = f_0 (g_1 x_2)
Clausify.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 (Clausify.append xs_1_1 ys_1))
Clausify.display::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons c_1_0 cs_1_1 -> addI (Clausify.emitClause c_1_0) (Clausify.display cs_1_1))
Clausify.emitClause::I !_x_0 = select _x_0 (Flite.Pair c_1_0 a_1_1 -> addI (Clausify.sum c_1_0) (Clausify.sum a_1_1))
Clausify.sum::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons x_1_0 xs_1_1 -> addI x_1_0 (Clausify.sum xs_1_1))
tests/broken/While.sapl 0 → 100644
View file @ 4ac88b5e
main = While.Start
While.Start::I = While.value_28 (While.ssos (While.Comp (While.Ass 4 (While.V 3)) (While.While (While.Neg (While.Eq (While.V 4) (While.N 0))) (While.Comp (While.Comp (While.Comp (While.Comp (While.Ass 0 (While.V 3)) (While.Ass 1 (While.V 4))) (While.While (While.Le (While.V 1) (While.V 0)) (While.Comp (While.Ass 0 (While.Sub (While.V 0) (While.V 1))) (While.Ass 2 (While.Add (While.V 2) (While.N 1)))))) (While.If (While.Eq (While.V 0) (While.N 0)) (While.Ass 5 (While.Add (While.V 5) (While.N 1))) While.Skip)) (While.Ass 4 (While.Sub (While.V 4) (While.N 1)))))) (Flite.Cons (Flite.Pair 0 0) (Flite.Cons (Flite.Pair 1 0) (Flite.Cons (Flite.Pair 2 0) (Flite.Cons (Flite.Pair 3 14000) (Flite.Cons (Flite.Pair 4 0) (Flite.Cons (Flite.Pair 5 0) Flite.Nil))))))) 5 While.id
While.id !x_0 = x_0
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
:: Flite.Pair = Flite.Pair a1 a2
:: While.Val = While.N a1::I | While.V a1::I | While.Add a1 a2 | While.Sub a1 a2
:: While.Stm = While.Ass a1::I a2 | While.Skip | While.Comp a1 a2 | While.If a1 a2 a3 | While.While a1 a2
:: While.BVal = While.TRUE | While.FALSE | While.Eq a1 a2 | While.Le a1 a2 | While.Neg a1 | While.And a1 a2
While.ssos !ss_0 s_1 = While.run (While.Inter ss_0 s_1)
:: While.State = While.Inter a1 a2 | While.Final a1
While.run !_x_0 = select _x_0 (While.Inter ss_1_0 s_1_1 -> While.run (While.sosstm ss_1_0 s_1_1)) (While.Final s_1_0 -> s_1_0)
While.sosstm !_x_0 s_1 = select _x_0 (While.Ass x_1_0 a_1_1 -> While.aval a_1_1 s_1 (While.update_32 s_1 x_1_0 While.Final)) (While.Skip -> While.Final s_1) (While.Comp ss1_1_0 ss2_1_1 -> <{While._c;60;3_33}> (While.sosstm ss1_1_0 s_1) ss2_1_1) (While.If b_1_0 ss1_1_1 ss2_1_2 -> While.bval b_1_0 s_1 (While.cond s_1 ss1_1_1 ss2_1_2)) (While.While b_1_0 ss_1_1 -> While.Inter (While.If b_1_0 (While.Comp ss_1_1 (While.While b_1_0 ss_1_1)) While.Skip) s_1)
While.cond s_0 ss1_1 ss2_2 !c_3::B = if c_3 (While.Inter ss1_1 s_0) (While.Inter ss2_2 s_0)
While.bval !_x_0 s_1 k_2 = select _x_0 (While.TRUE -> k_2 True) (While.FALSE -> k_2 False) (While.Eq a1_1_0 a2_1_1 -> While.seq (While.aval a1_1_0 s_1) (While.aval a2_1_1 s_1) (While.eq_29 k_2)) (While.Le a1_1_0 a2_1_1 -> While.seq (While.aval a1_1_0 s_1) (While.aval a2_1_1 s_1) (While.leq_30 k_2)) (While.Neg b_1_0 -> While.bval b_1_0 s_1 (While.invk k_2)) (While.And a1_1_0 a2_1_1 -> While.seq (While.bval a1_1_0 s_1) (While.bval a2_1_1 s_1) (While.andk k_2))
While.andk !k_0 !a_1::B b_2::B = While.bool (While.and a_1 b_2) k_0
While.and::B !_x_0::B x_1::B = if _x_0 x_1 False
While.bool !_x_0::B !k_1 = if _x_0 (k_1 True) (k_1 False)
While.seq !f_0 g_1 k_2 = f_0 (While.comp g_1 k_2)
While.comp !f_0 g_1 x_2 = f_0 (g_1 x_2)
While.invk !k_0 !a_1::B = While.bool (While.inv a_1) k_0
While.inv::B !_x_0::B = if _x_0 False True
While.leq_30 !k_0 !a_1::I !b_2::I = While.bool (<{While.<=_31}> a_1 b_2) k_0
<{While.<=_31}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
While.aval !_x_0 s_1 k_2 = select _x_0 (While.N n_1_0 -> k_2 n_1_0) (While.V x_1_0 -> While.value_28 s_1 x_1_0 k_2) (While.Add a1_1_0 a2_1_1 -> While.seq (While.aval a1_1_0 s_1) (While.aval a2_1_1 s_1) (While.add k_2)) (While.Sub a1_1_0 a2_1_1 -> While.seq (While.aval a1_1_0 s_1) (While.aval a2_1_1 s_1) (While.sub k_2))
While.sub !k_0 !a_1::I !b_2::I = While.int (subI a_1 b_2) k_0
While.int !n_0::I !k_1 = if (eqI n_0 0) (k_1 0) (k_1 n_0)
While.add !k_0 !a_1::I !b_2::I = While.int (addI a_1 b_2) k_0
While.value_28 !_x_0 !v_1::I !k_2 = select _x_0 (Flite.Cons _x_1_0 s_1_1 -> select _x_1_0 (Flite.Pair x_2_0 y_2_1 -> if (eqI x_2_0 v_1) (k_2 y_2_1) (While.value_28 s_1_1 v_1 k_2)) )
While.eq_29 !k_0 !a_1::I !b_2::I = While.bool (eqI a_1 b_2) k_0
<{While._c;60;3_33}> !_x_0 ss2_1 = select _x_0 (While.Inter ss10_1_0 s0_1_1 -> While.Inter (While.Comp ss10_1_0 ss2_1) s0_1_1) (While.Final s0_1_0 -> While.Inter ss2_1 s0_1_0)
While.update_32 !_x_0 v_1::I k_2 i_3 = select _x_0 (Flite.Nil -> k_2 Flite.Nil) (Flite.Cons _x_1_0 s_1_1 -> select _x_1_0 (Flite.Pair x_2_0 y_2_1 -> if (eqI x_2_0 v_1) (While.update_32 s_1_1 v_1 (While.upd k_2 v_1 i_3) i_3) (While.update_32 s_1_1 v_1 (While.upd k_2 x_2_0 y_2_1) i_3)) )
While.upd !k_0 x_1 y_2 s_3 = k_0 (Flite.Cons (Flite.Pair x_1 y_2) s_3)
tests/postponed/Cichelli.sapl 0 → 100644
View file @ 4ac88b5e
main = Cichelli.Start
Cichelli.Start::I = <{Cichelli._c;198;4_100}> (Cichelli.cichelli_67 (Flite.Cons (Flite.str "as") (Flite.Cons (Flite.str "case") (Flite.Cons (Flite.str "class") (Flite.Cons (Flite.str "data") (Flite.Cons (Flite.str "default") (Flite.Cons (Flite.str "deriving") (Flite.Cons (Flite.str "do") (Flite.Cons (Flite.str "else") (Flite.Cons (Flite.str "hiding") (Flite.Cons (Flite.str "if") (Flite.Cons (Flite.str "import") (Flite.Cons (Flite.str "in") (Flite.Cons (Flite.str "infix") (Flite.Cons (Flite.str "infixl") (Flite.Cons (Flite.str "infixr") (Flite.Cons (Flite.str "instance") (Flite.Cons (Flite.str "let") (Flite.Cons (Flite.str "module") (Flite.Cons (Flite.str "newtype") (Flite.Cons (Flite.str "of") (Flite.Cons (Flite.str "qualified") (Flite.Cons (Flite.str "then") (Flite.Cons (Flite.str "type") (Flite.Cons (Flite.str "where") Flite.Nil)))))))))))))))))))))))))
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
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 = toIntC c_0
Cichelli.cichelli_67 !ss_0 = <{Cichelli._c;165;15_99}> (Cichelli.freqSorted_68 (Cichelli.map Cichelli.enKey ss_0))
Cichelli.enKey k_0 = Cichelli.K k_0 (Cichelli.head k_0) (Cichelli.last k_0) (Cichelli.len k_0)
Cichelli.len::I !xs_0 = Cichelli.lenAcc 0 xs_0
Cichelli.lenAcc::I !acc_0::I !_x_1 = select _x_1 (Flite.Nil -> acc_0) (Flite.Cons x_1_0 xs_1_1 -> Cichelli.lenAcc (addI acc_0 1) xs_1_1)
Cichelli.last !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> if (Cichelli.null xs_1_1) x_1_0 (Cichelli.last xs_1_1))
Cichelli.null::B !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> False)
Cichelli.head !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> x_1_0)
:: Cichelli.K = Cichelli.K a1 a2 a3 a4
Cichelli.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) (Cichelli.map f_0 xs_1_1))
Cichelli.freqSorted_68 ks_0 = let ft_1_0 = Cichelli.freqTabOf_69 ks_0 in Flite.Pair (Cichelli.sorted (Cichelli.decreasingFrequencyIn_72 ft_1_0) ks_0) (Cichelli.len ft_1_0)
Cichelli.decreasingFrequencyIn_72::B !ft_0 !_x_1 !_x_2 = select _x_1 (Cichelli.K s0_1_0 a_1_1 x_1_2 n0_1_3 -> select _x_2 (Cichelli.K s1_2_0 b_2_1 y_2_2 n1_2_3 -> let freq_3_0 = Cichelli.flip Cichelli.assoc_73 ft_0 in Cichelli.gt_58 (addI (freq_3_0 a_1_1) (freq_3_0 x_1_2)) (addI (freq_3_0 b_2_1) (freq_3_0 y_2_2))) )
Cichelli.gt_58::B !m_0::I !n_1::I = if (<{Cichelli.<=_59}> m_0 n_1) False True
<{Cichelli.<=_59}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
Cichelli.assoc_73 !x_0::I !_x_1 = select _x_1 (Flite.Cons _x_1_0 yzs_1_1 -> select _x_1_0 (Flite.Pair y_2_0 z_2_1 -> if (eqI x_0 y_2_0) z_2_1 (Cichelli.assoc_73 x_0 yzs_1_1)) )
:: Flite.Pair = Flite.Pair a1 a2
Cichelli.flip !f_0 x_1 y_2 = f_0 y_2 x_1
Cichelli.sorted lt_0 = Cichelli.foldr (Cichelli.ordins lt_0) Flite.Nil
Cichelli.ordins lt_0 x_1 !_x_2 = select _x_2 (Flite.Nil -> Flite.Cons x_1 Flite.Nil) (Flite.Cons y_1_0 ys_1_1 -> if (lt_0 x_1 y_1_0) (Flite.Cons x_1 (Flite.Cons y_1_0 ys_1_1)) (Flite.Cons y_1_0 (Cichelli.ordins lt_0 x_1 ys_1_1)))
Cichelli.foldr f_0 z_1 !_x_2 = select _x_2 (Flite.Nil -> z_1) (Flite.Cons x_1_0 xs_1_1 -> f_0 x_1_0 (Cichelli.foldr f_0 z_1 xs_1_1))
Cichelli.freqTabOf_69 !ks_0 = Cichelli.histo_70 (Cichelli.concatMap Cichelli.ends ks_0)
Cichelli.ends !_x_0 = select _x_0 (Cichelli.K s_1_0 a_1_1 z_1_2 n_1_3 -> Flite.Cons a_1_1 (Flite.Cons z_1_2 Flite.Nil))
Cichelli.concatMap f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> Cichelli.append (f_0 x_1_0) (Cichelli.concatMap f_0 xs_1_1))
Cichelli.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 (Cichelli.append xs_1_1 ys_1))
Cichelli.histo_70 !xs_0 = Cichelli.foldr Cichelli.histins_71 Flite.Nil xs_0
Cichelli.histins_71 x_0::I !_x_1 = select _x_1 (Flite.Nil -> Flite.Cons (Flite.Pair x_0 1) Flite.Nil) (Flite.Cons yn_1_0 yns_1_1 -> <{Cichelli._c;72;3_95}> yn_1_0 x_0 yns_1_1)
<{Cichelli._c;72;3_95}> !yn_0 !x_1::I yns_2 = select yn_0 (Flite.Pair y_1_0 n_1_1 -> if (eqI x_1 y_1_0) (Flite.Cons (Flite.Pair y_1_0 (addI n_1_1 1)) yns_2) (Flite.Cons yn_0 (Cichelli.histins_71 x_1 yns_2)))
<{Cichelli._c;165;15_99}> !_x_0 = select _x_0 (Flite.Pair ks_1_0 mv_1_1 -> Cichelli.findhash_80 mv_1_1 (Cichelli.blocked_74 ks_1_0))
Cichelli.blocked_74 = Cichelli.blockedWith_75 Flite.Nil
Cichelli.blockedWith_75 ds_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons k_1_0 ks_1_1 -> let dsk_2_0 = Cichelli.union_76 ds_0 (Cichelli.ends k_1_0), eks_2_1 = Cichelli.endsSubset_78 dsk_2_0 in Flite.Cons k_1_0 (Cichelli.append (Cichelli.filter eks_2_1 ks_1_1) (Cichelli.blockedWith_75 dsk_2_0 (Cichelli.filter (Cichelli.non eks_2_1) ks_1_1))))
Cichelli.non::B !f_0 x_1 = if (f_0 x_1) False True
Cichelli.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 (Cichelli.filter p_0 xs_1_1)) (Cichelli.filter p_0 xs_1_1))
Cichelli.endsSubset_78::B !ds_0 !k_1 = Cichelli.subset_79 (Cichelli.ends k_1) ds_0
Cichelli.subset_79::B !_x_0 ys_1 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 xs_1_1 -> if (Cichelli.elem_64 x_1_0 ys_1) (Cichelli.subset_79 xs_1_1 ys_1) False)
Cichelli.elem_64::B x_0::I !_x_1 = select _x_1 (Flite.Nil -> False) (Flite.Cons y_1_0 ys_1_1 -> if (eqI x_0 y_1_0) True (Cichelli.elem_64 x_0 ys_1_1))
Cichelli.union_76 !xs_0 !ys_1 = Cichelli.foldr Cichelli.ins_77 xs_0 ys_1
Cichelli.ins_77 x_0::I !ys_1 = if (Cichelli.elem_64 x_0 ys_1) ys_1 (Flite.Cons x_0 ys_1)
Cichelli.findhash_80 mv_0::I !ks_1 = <{Cichelli._c;125;3_98}> (Cichelli.hashes_81 mv_0 (Cichelli.len ks_1) ks_1 (Cichelli.Hash (Cichelli.H Flite.Nothing Flite.Nothing Flite.Nil) Flite.Nil))
:: Flite.Maybe = Flite.Nothing | Flite.Just a1
:: Cichelli.H = Cichelli.H a1 a2 a3
:: Cichelli.Hash = Cichelli.Hash a1 a2
Cichelli.hashes_81 maxval_0::I nk_1::I !_x_2 h_3 = select _x_2 (Flite.Nil -> Flite.Cons h_3 Flite.Nil) (Flite.Cons k_1_0 ks_1_1 -> Cichelli.concatMap (Cichelli.hashes_81 maxval_0 nk_1 ks_1_1) (Cichelli.concatMap (Cichelli.insertKey_82 nk_1 k_1_0) (Cichelli.concatMap (Cichelli.assignUpto_84 maxval_0 (Cichelli.lastLetter k_1_0)) (Cichelli.assignUpto_84 maxval_0 (Cichelli.firstLetter k_1_0) h_3))))
Cichelli.firstLetter !_x_0 = select _x_0 (Cichelli.K s_1_0 a_1_1 z_1_2 n_1_3 -> a_1_1)
Cichelli.assignUpto_84 maxval_0::I c_1::I !h_2 = <{Cichelli._c;138;3_96}> (Cichelli.assocm_85 c_1 (Cichelli.hashAssoc h_2)) c_1 h_2 maxval_0
Cichelli.hashAssoc !_x_0 = select _x_0 (Cichelli.Hash hs_1_0 hf_1_1 -> hf_1_1)
Cichelli.assocm_85 x_0::I !_x_1 = select _x_1 (Flite.Nil -> Flite.Nothing) (Flite.Cons _x_1_0 yzs_1_1 -> select _x_1_0 (Flite.Pair y_2_0 z_2_1 -> if (eqI x_0 y_2_0) (Flite.Just z_2_1) (Cichelli.assocm_85 x_0 yzs_1_1)) )
<{Cichelli._c;138;3_96}> !_x_0 c_1::I h_2 maxval_3::I = select _x_0 (Flite.Nothing -> Cichelli.map (Cichelli.assign c_1 h_2) (Cichelli.enumFromTo 0 maxval_3)) (Flite.Just v_1_0 -> Flite.Cons h_2 Flite.Nil)
Cichelli.enumFromTo !m_0::I !n_1::I = if (<{Cichelli.<=_55}> m_0 n_1) (Flite.Cons m_0 (Cichelli.enumFromTo (addI m_0 1) n_1)) Flite.Nil
<{Cichelli.<=_55}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
Cichelli.assign c_0 !_x_1 v_2 = select _x_1 (Cichelli.Hash hs_1_0 hf_1_1 -> Cichelli.Hash hs_1_0 (Flite.Cons (Flite.Pair c_0 v_2) hf_1_1))
Cichelli.lastLetter !_x_0 = select _x_0 (Cichelli.K s_1_0 a_1_1 z_1_2 n_1_3 -> z_1_2)
Cichelli.insertKey_82 nk_0::I !k_1 !_x_2 = select _x_2 (Cichelli.Hash hs_1_0 hf_1_1 -> <{Cichelli._c;144;3_97}> (Cichelli.hinsert nk_0 (Cichelli.hash_83 hf_1_1 k_1) hs_1_0) hf_1_1)
Cichelli.hash_83::I !hf_0 !_x_1 = select _x_1 (Cichelli.K s_1_0 a_1_1 z_1_2 n_1_3 -> addI n_1_3 (addI (Cichelli.assoc_73 a_1_1 hf_0) (Cichelli.assoc_73 z_1_2 hf_0)))
Cichelli.hinsert nk_0::I !h_1::I !_x_2 = select _x_2 (Cichelli.H lo_1_0 hi_1_1 hs_1_2 -> <{Cichelli._c;155;5_91}> (Cichelli.elem_64 h_1 hs_1_2) lo_1_0 h_1 hi_1_1 nk_0 hs_1_2)
<{Cichelli._c;155;5_91}> !_x_0::B lo_1 h_2::I hi_3 nk_4::I hs_5 = select _x_0 (True -> Flite.Nothing) (False -> let newhi_2_0 = <{Cichelli._c;153;19_89}> hi_3 h_2, newlo_2_1 = <{Cichelli._c;152;19_88}> lo_1 h_2 in <{Cichelli._c;157;14_90}> (<{Cichelli.<=_65}> (subI (addI 1 newhi_2_0) newlo_2_1) nk_4) newlo_2_1 newhi_2_0 h_2 hs_5)
<{Cichelli.<=_65}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{Cichelli._c;157;14_90}> !_x_0::B newlo_1::I newhi_2::I h_3::I hs_4 = select _x_0 (False -> Flite.Nothing) (True -> Flite.Just (Cichelli.H (Flite.Just newlo_1) (Flite.Just newhi_2) (Flite.Cons h_3 hs_4)))
<{Cichelli._c;152;19_88}>::I !lo_0 !h_1::I = select lo_0 (Flite.Nothing -> h_1) (Flite.Just x_1_0 -> Cichelli.mini_60 x_1_0 h_1)
Cichelli.mini_60::I !m_0::I !n_1::I = if (<{Cichelli.<=_61}> m_0 n_1) m_0 n_1
<{Cichelli.<=_61}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{Cichelli._c;153;19_89}>::I !hi_0 !h_1::I = select hi_0 (Flite.Nothing -> h_1) (Flite.Just x_1_0 -> Cichelli.maxi_62 x_1_0 h_1)
Cichelli.maxi_62::I !m_0::I !n_1::I = if (<{Cichelli.<=_63}> m_0 n_1) n_1 m_0
<{Cichelli.<=_63}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{Cichelli._c;144;3_97}> !_x_0 hf_1 = select _x_0 (Flite.Nothing -> Flite.Nil) (Flite.Just hsNew_1_0 -> Flite.Cons (Cichelli.Hash hsNew_1_0 hf_1) Flite.Nil)
<{Cichelli._c;125;3_98}> !_x_0 = select _x_0 (Flite.Cons _x_1_0 hs_1_1 -> select _x_1_0 (Cichelli.Hash s_2_0 f_2_1 -> Flite.Just f_2_1) ) (Flite.Nil -> Flite.Nothing)
<{Cichelli._c;198;4_100}>::I !_x_0 = select _x_0 (Flite.Just hf_1_0 -> Cichelli.emitHashFun hf_1_0) (Flite.Nothing -> 0)
Cichelli.emitHashFun::I !_x_0 = select _x_0 (Flite.Nil -> 0) (Flite.Cons _x_1_0 hf_1_1 -> select _x_1_0 (Flite.Pair c_2_0 n_2_1 -> addI (addI c_2_0 n_2_1) (Cichelli.emitHashFun hf_1_1)) )
tests/postponed/Parselib.sapl 0 → 100644
View file @ 4ac88b5e
main = Parselib.Start
Parselib.Start = Parselib.parsetest 20
Parselib.parsetest !n_0 = if (eq n_0 0) Parselib.Nill (Parselib.Cons (Parselib.length1 (Parselib.filter1 Parselib.isSingle (Parselib.parseRules Parselib.prog100))) (Parselib.parsetest (sub n_0 1)))
Parselib.prog100 = Parselib.concat1 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 (Parselib.Cons Parselib.prog10 Parselib.Nill))))))))))
:: Parselib.List1 = Parselib.Nill | Parselib.Cons a1 a2
Parselib.prog10 = Parselib.concat1 (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog (Parselib.Cons Parselib.prog Parselib.Nill))))))))))
Parselib.prog = Parselib.concat1 (Parselib.list2List1 (StdList.map Parselib.list2List1 Parselib.pprog))
Parselib.pprog = _predefined._Cons Parselib.line1 (_predefined._Cons Parselib.line2 (_predefined._Cons Parselib.line3 (_predefined._Cons Parselib.line4 (_predefined._Cons Parselib.line5 (_predefined._Cons Parselib.line6 (_predefined._Cons Parselib.line7 (_predefined._Cons Parselib.line8 (_predefined._Cons Parselib.line9 (_predefined._Cons Parselib.line10 (_predefined._Cons Parselib.line11 (_predefined._Cons Parselib.line12 (_predefined._Cons Parselib.line13 (_predefined._Cons Parselib.line14 (_predefined._Cons Parselib.line15 (_predefined._Cons Parselib.line16 (_predefined._Cons Parselib.line17 _predefined._Nil))))))))))))))))
:: _predefined._List = _predefined._Cons a1 a2 | _predefined._Nil
Parselib.line17 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'c' (_predefined._Cons 'o' (_predefined._Cons 'r' (_predefined._Cons 'n' (_predefined._Cons 'e' (_predefined._Cons 'l' (_predefined._Cons 'i' (_predefined._Cons 'a' (_predefined._Cons ',' (_predefined._Cons 'n' (_predefined._Cons 'e' (_predefined._Cons 'l' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))))))
Parselib.line16 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 's' (_predefined._Cons 'i' (_predefined._Cons 'e' (_predefined._Cons 'm' (_predefined._Cons ',' (_predefined._Cons 'n' (_predefined._Cons 'e' (_predefined._Cons 'l' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))
Parselib.line15 = _predefined._Cons 'v' (_predefined._Cons 'o' (_predefined._Cons 'o' (_predefined._Cons 'r' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons ' ' (_predefined._Cons ':' (_predefined._Cons '-' (_predefined._Cons ' ' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '3' (_predefined._Cons ')' (_predefined._Cons ',' (_predefined._Cons 'v' (_predefined._Cons 'o' (_predefined._Cons 'o' (_predefined._Cons 'r' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '3' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))))))))))))))))))))))))))))))))))))
Parselib.line14 = _predefined._Cons 'v' (_predefined._Cons 'o' (_predefined._Cons 'o' (_predefined._Cons 'r' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons ' ' (_predefined._Cons ':' (_predefined._Cons '-' (_predefined._Cons ' ' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))))))))))))))))))))))))))
Parselib.line13 = _predefined._Cons 'g' (_predefined._Cons 'r' (_predefined._Cons 'o' (_predefined._Cons 'o' (_predefined._Cons 't' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons ' ' (_predefined._Cons ':' (_predefined._Cons '-' (_predefined._Cons ' ' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '3' (_predefined._Cons ')' (_predefined._Cons ',' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '3' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))))))))))))))))))))))))))))))))))))))))
Parselib.line12 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'n' (_predefined._Cons 'e' (_predefined._Cons 'l' (_predefined._Cons ',' (_predefined._Cons 'j' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))))))))
Parselib.line11 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'j' (_predefined._Cons 'o' (_predefined._Cons 'o' (_predefined._Cons 'p' (_predefined._Cons ',' (_predefined._Cons 'j' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))
Parselib.line10 = _predefined._Cons 'v' (_predefined._Cons 'a' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons ' ' (_predefined._Cons ':' (_predefined._Cons '-' (_predefined._Cons ' ' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons ',' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))))))))))))))))))))))))))))))
Parselib.line9 = _predefined._Cons 'm' (_predefined._Cons 'o' (_predefined._Cons 'e' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons ' ' (_predefined._Cons ':' (_predefined._Cons '-' (_predefined._Cons ' ' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ',' (_predefined._Cons 'X' (_predefined._Cons '2' (_predefined._Cons ')' (_predefined._Cons ',' (_predefined._Cons 'v' (_predefined._Cons 'r' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'w' (_predefined._Cons '(' (_predefined._Cons 'X' (_predefined._Cons '1' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))))))))))))))))))))))))))
Parselib.line8 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'g' (_predefined._Cons 'r' (_predefined._Cons 'i' (_predefined._Cons 'e' (_predefined._Cons 't' (_predefined._Cons ',' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'k' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))))))))))))))
Parselib.line7 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'g' (_predefined._Cons 'r' (_predefined._Cons 'i' (_predefined._Cons 'e' (_predefined._Cons 't' (_predefined._Cons ',' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'i' (_predefined._Cons 't' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))))))))
Parselib.line6 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'j' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons ',' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'i' (_predefined._Cons 't' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))))))))))
Parselib.line5 = _predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'd' (_predefined._Cons 'e' (_predefined._Cons 'r' (_predefined._Cons '(' (_predefined._Cons 'j' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons ',' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'k' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))
Parselib.line4 = _predefined._Cons 'v' (_predefined._Cons 'r' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'w' (_predefined._Cons '(' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'i' (_predefined._Cons 't' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))))))
Parselib.line3 = _predefined._Cons 'v' (_predefined._Cons 'r' (_predefined._Cons 'o' (_predefined._Cons 'u' (_predefined._Cons 'w' (_predefined._Cons '(' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'g' (_predefined._Cons 'r' (_predefined._Cons 'i' (_predefined._Cons 'e' (_predefined._Cons 't' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))))))))
Parselib.line2 = _predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons '(' (_predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'r' (_predefined._Cons 'k' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil)))))))))
Parselib.line1 = _predefined._Cons 'm' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons '(' (_predefined._Cons 'j' (_predefined._Cons 'a' (_predefined._Cons 'n' (_predefined._Cons ')' (_predefined._Cons '.' _predefined._Nil))))))))
Parselib.list2List1 !_x_0 = select _x_0 (_predefined._Nil -> Parselib.Nill) (_predefined._Cons x_1_0 xs_1_1 -> Parselib.Cons x_1_0 (Parselib.list2List1 xs_1_1))
StdList.map f_0 !_x_1 = select _x_1 (_predefined._Cons a_1_0 x_1_1 -> _predefined._Cons (f_0 a_1_0) (StdList.map f_0 x_1_1)) (_predefined._Nil -> _predefined._Nil)
Parselib.concat1 !_x_0 = select _x_0 (Parselib.Nill -> Parselib.Nill) (Parselib.Cons _x_1_0 xss_1_1 -> select _x_1_0 (Parselib.Nill -> Parselib.concat1 xss_1_1) (Parselib.Cons x_2_0 xs_2_1 -> Parselib.Cons x_2_0 (Parselib.concat1 (Parselib.Cons xs_2_1 xss_1_1))) )
Parselib.parseRules = Parselib.start (Parselib.pMany Parselib.pRule)
Parselib.pRule = Parselib.seqleft (Parselib.sequ (Parselib.seqapply Parselib.rule Parselib.pTerm) (Parselib.option Parselib.pRightHandSide Parselib.Nill)) (Parselib.pSymbol_127 '.')
Parselib.pSymbol_127 a_0 !_x_1 = select _x_1 (Parselib.Nill -> Parselib.Nill) (Parselib.Cons x_1_0 xs_1_1 -> if (Parselib.eqChar_128 x_1_0 a_0) (Parselib.Cons (Parselib.Tup x_1_0 xs_1_1) Parselib.Nill) Parselib.Nill)
:: Parselib.Tuptype = Parselib.Tup a1 a2
Parselib.eqChar_128 !a_0 !b_1 = eq a_0 b_1
Parselib.pRightHandSide = Parselib.seqright (Parselib.seqright (Parselib.pSymbol_127 ':') (Parselib.pSymbol_127 '-')) (Parselib.pListSep Parselib.pTerm Parselib.pComma)
Parselib.pComma = Parselib.pSymbol_127 ','
Parselib.pTerm = Parselib.choice (Parselib.choice Parselib.pCon Parselib.pVar) Parselib.pFun
Parselib.pFun = Parselib.sequ (Parselib.seqapply Parselib.fun Parselib.pIdentifier) (Parselib.choice (Parselib.pParens (Parselib.pListSep Parselib.pTerm Parselib.pComma)) (Parselib.pSucceed Parselib.Nill))
Parselib.pSucceed r_0 xs_1 = Parselib.Cons (Parselib.Tup r_0 xs_1) Parselib.Nill
Parselib.pListSep p_0 s_1 = Parselib.sequ (Parselib.seqapply Parselib.list p_0) (Parselib.pMany (Parselib.seqright s_1 p_0))
Parselib.seqright p_0 q_1 = Parselib.sequ (Parselib.seqapply Parselib.flip_122 p_0) q_1
Parselib.flip_122 a_0 !b_1 = StdFunc.const b_1 a_0
StdFunc.const !x_0 y_1 = x_0
Parselib.seqapply f_0 p_1 = Parselib.sequ (Parselib.pSucceed f_0) p_1
Parselib.sequ !p_0 q_1 xs_2 = Parselib.concat1 (Parselib.map1 (Parselib.do2 q_1) (p_0 xs_2))
Parselib.do2 !q_0 !_x_1 = select _x_1 (Parselib.Tup f_1_0 ys_1_1 -> Parselib.map1 (Parselib.do1 f_1_0) (q_0 ys_1_1))
Parselib.do1 f_0 !_x_1 = select _x_1 (Parselib.Tup x_1_0 zs_1_1 -> Parselib.Tup (f_0 x_1_0) zs_1_1)
Parselib.map1 f_0 !_x_1 = select _x_1 (Parselib.Nill -> Parselib.Nill) (Parselib.Cons x_1_0 xs_1_1 -> Parselib.Cons (f_0 x_1_0) (Parselib.map1 f_0 xs_1_1))
Parselib.pMany p_0 = Parselib.option (Parselib.sequ (Parselib.seqapply Parselib.list p_0) (Parselib.pMany p_0)) Parselib.Nill
Parselib.list x_0 xs_1 = Parselib.Cons x_0 xs_1
Parselib.option p_0 d_1 = Parselib.choice p_0 (Parselib.pSucceed d_1)
Parselib.choice !p_0 q_1 xs_2 = Parselib.append1 (p_0 xs_2) (q_1 xs_2)
Parselib.append1 !_x_0 ys_1 = select _x_0 (Parselib.Nill -> ys_1) (Parselib.Cons x_1_0 xs_1_1 -> Parselib.Cons x_1_0 (Parselib.append1 xs_1_1 ys_1))
Parselib.pParens p_0 = Parselib.pPack (Parselib.pSymbol_127 '(') p_0 (Parselib.pSymbol_127 ')')
Parselib.pPack p_0 r_1 q_2 = Parselib.seqleft (Parselib.seqright p_0 r_1) q_2
Parselib.seqleft p_0 q_1 = Parselib.sequ (Parselib.seqapply StdFunc.const p_0) q_1
Parselib.pIdentifier = Parselib.sequ (Parselib.seqapply Parselib.list (Parselib.pSatisfy StdChar.isAlpha)) (Parselib.greedy (Parselib.pSatisfy Parselib.isAlphaNum))
Parselib.isAlphaNum !c_0 = if (StdChar.isAlpha c_0) True (StdChar.isDigit c_0)
StdChar.isDigit !c_0 = and (ge c_0 '0') (ge '9' c_0)
StdChar.isAlpha !c_0 = or (StdChar.isLower c_0) (StdChar.isUpper c_0)
StdChar.isUpper !c_0 = and (ge c_0 'A') (ge 'Z' c_0)
StdChar.isLower !c_0 = and (ge c_0 'a') (ge 'z' c_0)
Parselib.pSatisfy p_0 !_x_1 = select _x_1 (Parselib.Nill -> Parselib.Nill) (Parselib.Cons x_1_0 xs_1_1 -> if (p_0 x_1_0) (Parselib.Cons (Parselib.Tup x_1_0 xs_1_1) Parselib.Nill) Parselib.Nill)
Parselib.greedy p_0 = Parselib.determ (Parselib.pMany p_0)
Parselib.determ !p_0 xs_1 = Parselib.dt (p_0 xs_1)
Parselib.dt !_x_0 = select _x_0 (Parselib.Nill -> Parselib.Nill) (Parselib.Cons r_1_0 xs_1_1 -> Parselib.Cons r_1_0 Parselib.Nill)
Parselib.fun n_0 ns_1 = Parselib.Fun n_0 ns_1
:: Parselib.Term = Parselib.Con a1 | Parselib.Var a1 | Parselib.Fun a1 a2
Parselib.pVar = Parselib.seqapply Parselib.var (Parselib.seqright (Parselib.pSymbol_127 'X') Parselib.pNatural)
Parselib.pNatural = Parselib.seqapply (Parselib.foldlp Parselib.makeNum 0) (Parselib.pMany1 Parselib.pDigAsInt_125)
Parselib.pDigAsInt_125 = Parselib.seqapply Parselib.dig2num_126 Parselib.pDigit
Parselib.pDigit = Parselib.pSatisfy StdChar.isDigit
Parselib.dig2num_126 !c_0 = sub (toInt_char c_0) (toInt_char '0')
Parselib.pMany1 p_0 = Parselib.sequ (Parselib.seqapply Parselib.list p_0) (Parselib.pMany p_0)
Parselib.makeNum !a_0 !b_1 = add (mult a_0 10) b_1
Parselib.foldlp f_0 z_1 !_x_2 = select _x_2 (Parselib.Nill -> z_1) (Parselib.Cons x_1_0 xs_1_1 -> Parselib.foldlp f_0 (f_0 z_1 x_1_0) xs_1_1)
Parselib.var n_0 = Parselib.Var n_0
Parselib.pCon = Parselib.seqapply Parselib.con Parselib.pNatural
Parselib.con n_0 = Parselib.Con n_0
Parselib.rule r_0 rs_1 = Parselib.Rule r_0 rs_1
:: Parselib.Rulet = Parselib.Rule a1 a2
Parselib.start !p_0 xs_1 = Parselib.fstp (Parselib.hd1 (p_0 (Parselib.filter1 Parselib.anon_130 xs_1)))
Parselib.anon_130 !x_0 = not (StdChar.isSpace x_0)
StdChar.isSpace !c_0 = select c_0 (' ' -> true) ('\t' -> true) ('\n' -> true) ('\r' -> true) ('\f' -> true) ('\r' -> true) (_ -> false)
Parselib.filter1 f_0 !_x_1 = select _x_1 (Parselib.Nill -> Parselib.Nill) (Parselib.Cons x_1_0 xs_1_1 -> if (f_0 x_1_0) (Parselib.Cons x_1_0 (Parselib.filter1 f_0 xs_1_1)) (Parselib.filter1 f_0 xs_1_1))
Parselib.hd1 !_x_0 = select _x_0 (Parselib.Cons x_1_0 xs_1_1 -> x_1_0)
Parselib.fstp !_x_0 = select _x_0 (Parselib.Tup f_1_0 s_1_1 -> f_1_0)
Parselib.isSingle !_x_0 = select _x_0 (Parselib.Rule _x_1_0 cs_1_1 -> select _x_1_0 (Parselib.Fun f_2_0 fs_2_1 -> if (eq (Parselib.length1 fs_2_1) 1) (eq (Parselib.length1 cs_1_1) 0) False) )
Parselib.length1 !_x_0 = select _x_0 (Parselib.Nill -> 0) (Parselib.Cons x_1_0 xs_1_1 -> add 1 (Parselib.length1 xs_1_1))
tests/postponed/PermSort.sapl 0 → 100644
View file @ 4ac88b5e
main = PermSort.Start
PermSort.Start::I = PermSort.head (PermSort.permSort_12 (Flite.Cons 10 (Flite.Cons 9 (Flite.Cons 8 (Flite.Cons 7 (Flite.Cons 6 (Flite.Cons 5 (Flite.Cons 4 (Flite.Cons 3 (Flite.Cons 2 (Flite.Cons 1 Flite.Nil)))))))))))
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
PermSort.permSort_12 !xs_0 = PermSort.head (PermSort.filter PermSort.ord_13 (PermSort.perm xs_0))
PermSort.perm !_x_0 = select _x_0 (Flite.Nil -> Flite.Cons Flite.Nil Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> PermSort.concatMap (PermSort.place x_1_0) (PermSort.perm xs_1_1))
PermSort.place x_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Cons (Flite.Cons x_0 Flite.Nil) Flite.Nil) (Flite.Cons y_1_0 ys_1_1 -> Flite.Cons (Flite.Cons x_0 (Flite.Cons y_1_0 ys_1_1)) (PermSort.map (Flite.Cons y_1_0) (PermSort.place x_0 ys_1_1)))
PermSort.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) (PermSort.map f_0 xs_1_1))
PermSort.concatMap f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> PermSort.append (f_0 x_1_0) (PermSort.concatMap f_0 xs_1_1))
PermSort.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 (PermSort.append xs_1_1 ys_1))
PermSort.ord_13::B !_x_0 = select _x_0 (Flite.Nil -> True) (Flite.Cons x_1_0 _x_1_1 -> select _x_1_1 (Flite.Nil -> True) (Flite.Cons y_2_0 ys_2_1 -> PermSort.and (<{PermSort.<=_14}> x_1_0 y_2_0) (PermSort.ord_13 (Flite.Cons y_2_0 ys_2_1))) )
<{PermSort.<=_14}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
PermSort.and::B !_x_0::B x_1::B = if _x_0 x_1 False
PermSort.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 (PermSort.filter p_0 xs_1_1)) (PermSort.filter p_0 xs_1_1))
PermSort.head !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> x_1_0)
tests/postponed/SumPuz.sapl 0 → 100644
View file @ 4ac88b5e
main = SumPuz.Start
SumPuz.Start::I = let words_1_0 = Flite.Cons (Flite.str "ANANAB") (Flite.Cons (Flite.str "ELPPA") (Flite.Cons (Flite.str "YRREHC") (Flite.Cons (Flite.str "HCAEP") (Flite.Cons (Flite.str "TOCIRPA") (Flite.Cons (Flite.str "EVILO") (Flite.Cons (Flite.str "NOMEL") (Flite.Cons (Flite.str "AVAUG") (Flite.Cons (Flite.str "ODACAVA") (Flite.Cons (Flite.str "AYAPAP") (Flite.Cons (Flite.str "IHCTIL") (Flite.Cons (Flite.str "NOLEM") Flite.Nil))))))))))) in SumPuz.count_45 words_1_0 words_1_0 words_1_0
SumPuz.count_45::I !xs_0 ys_1 zs_2 = SumPuz.sumMap (SumPuz.fx_46 ys_1 zs_2) xs_0
SumPuz.fx_46::I !ys_0 zs_1 x_2 = SumPuz.sumMap (SumPuz.fy_47 x_2 zs_1) ys_0
SumPuz.fy_47::I x_0 !zs_1 y_2 = SumPuz.sumMap (SumPuz.fz_48 x_0 y_2) zs_1
SumPuz.fz_48::I !x_0 !y_1 z_2 = if (SumPuz.valid_49 x_0 y_1 z_2) 1 0
SumPuz.valid_49::B !x_0 !y_1 z_2 = SumPuz.and (eqI (SumPuz.len x_0) (SumPuz.len y_1)) (SumPuz.and (eqI (SumPuz.len x_0) (SumPuz.len z_2)) (SumPuz.isSingleton (SumPuz.solutions_50 x_0 y_1 z_2 (Flite.Pair 0 Flite.Nil))))
:: Flite.List = Flite.Nil | Flite.Cons a1 a2
:: Flite.Pair = Flite.Pair a1 a2
SumPuz.solutions_50 !_x_0 yys_1 !_x_2 !clds_3 = select _x_0 (Flite.Nil -> select _x_2 (Flite.Nil -> <{SumPuz._c;78;3_69}> (eqI (SumPuz.fst clds_3) 0) clds_3) (Flite.Cons z_2_0 _x_2_1 -> select _x_2_1 (Flite.Nil -> <{SumPuz._c;83;3_70}> (eqI (SumPuz.fst clds_3) 1) z_2_0 clds_3) ) ) (Flite.Cons x_1_0 xs_1_1 -> select _x_2 (Flite.Cons z_2_0 zs_2_1 -> SumPuz.ofAll (SumPuz.solns_53 (SumPuz.fst clds_3) x_1_0 (SumPuz.head yys_1) z_2_0 (SumPuz.solutions_50 xs_1_1 (SumPuz.tail yys_1) zs_2_1)) (SumPuz.ofAll (SumPuz.bindings_51 (SumPuz.head yys_1) (SumPuz.fromTo (SumPuz.ifNull (SumPuz.tail yys_1) 1 0) 9)) (SumPuz.bindings_51 x_1_0 (SumPuz.fromTo (SumPuz.ifNull xs_1_1 1 0) 9) (SumPuz.snd clds_3)))) )
SumPuz.snd !_x_0 = select _x_0 (Flite.Pair x_1_0 y_1_1 -> y_1_1)
SumPuz.ifNull !_x_0 t_1 e_2 = select _x_0 (Flite.Nil -> t_1) (Flite.Cons x_1_0 xs_1_1 -> e_2)
SumPuz.fromTo n_0::I m_1::I = Flite.Cons n_0 (<{SumPuz._c;108;22_59}> (eqI n_0 m_1) n_0 m_1)
<{SumPuz._c;108;22_59}> !_x_0::B n_1::I m_2::I = select _x_0 (True -> Flite.Nil) (False -> SumPuz.fromTo (addI n_1 1) m_2)
SumPuz.bindings_51 l_0::I !ds_1 !lds_2 = <{SumPuz._c;56;3_68}> (SumPuz.lookup_52 l_0 lds_2) lds_2 l_0 ds_1
SumPuz.lookup_52 a_0::I !_x_1 = select _x_1 (Flite.Nil -> Flite.Nothing) (Flite.Cons _x_1_0 rest_1_1 -> select _x_1_0 (Flite.Pair b_2_0 c_2_1 -> <{SumPuz._c;17;3_67}> (eqI a_0 b_2_0) a_0 rest_1_1 c_2_1) )
<{SumPuz._c;17;3_67}> !_x_0::B a_1::I rest_2 c_3 = select _x_0 (False -> SumPuz.lookup_52 a_1 rest_2) (True -> Flite.Just c_3)
:: Flite.Maybe = Flite.Nothing | Flite.Just a1
<{SumPuz._c;56;3_68}> !_x_0 lds_1 l_2::I !ds_3 = select _x_0 (Flite.Nothing -> SumPuz.map (SumPuz.flip Flite.Cons lds_1) (SumPuz.zip (SumPuz.repeat l_2) (SumPuz.diff_41 ds_3 (SumPuz.rng lds_1)))) (Flite.Just d_1_0 -> if (SumPuz.member_43 d_1_0 ds_3) (Flite.Cons lds_1 Flite.Nil) Flite.Nil)
SumPuz.member_43::B x_0::I !_x_1 = select _x_1 (Flite.Nil -> False) (Flite.Cons y_1_0 ys_1_1 -> <{SumPuz._c;34;3_62}> (eqI x_0 y_1_0) x_0 ys_1_1)
<{SumPuz._c;34;3_62}>::B !_x_0::B x_1::I ys_2 = select _x_0 (False -> SumPuz.member_43 x_1 ys_2) (True -> True)
SumPuz.rng = SumPuz.map SumPuz.snd
SumPuz.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) (SumPuz.map f_0 xs_1_1))
SumPuz.diff_41 = SumPuz.foldl (SumPuz.flip SumPuz.del_42)
SumPuz.del_42 x_0::I !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons y_1_0 ys_1_1 -> <{SumPuz._c;27;3_63}> (eqI x_0 y_1_0) y_1_0 x_0 ys_1_1)
<{SumPuz._c;27;3_63}> !_x_0::B y_1::I x_2::I ys_3 = select _x_0 (False -> Flite.Cons y_1 (SumPuz.del_42 x_2 ys_3)) (True -> ys_3)
SumPuz.flip !f_0 x_1 y_2 = f_0 y_2 x_1
SumPuz.foldl f_0 a_1 !_x_2 = select _x_2 (Flite.Nil -> a_1) (Flite.Cons x_1_0 xs_1_1 -> SumPuz.foldl f_0 (f_0 a_1 x_1_0) xs_1_1)
SumPuz.repeat x_0 = Flite.Cons x_0 (SumPuz.repeat x_0)
SumPuz.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) (SumPuz.zip xs_1_1 ys_2_1)) )
SumPuz.tail !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> xs_1_1)
SumPuz.head !_x_0 = select _x_0 (Flite.Cons x_1_0 xs_1_1 -> x_1_0)
SumPuz.ofAll f_0 !_x_1 = select _x_1 (Flite.Nil -> Flite.Nil) (Flite.Cons x_1_0 xs_1_1 -> SumPuz.append (f_0 x_1_0) (SumPuz.ofAll f_0 xs_1_1))
SumPuz.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 (SumPuz.append xs_1_1 ys_1))
SumPuz.fst !_x_0 = select _x_0 (Flite.Pair x_1_0 y_1_1 -> x_1_0)
SumPuz.solns_53 c_0::I x_1::I y_2::I z_3::I f_4 !s_5 = let qr_1_0 = SumPuz.divMod10 (addI (addI (SumPuz.img_54 s_5 x_1) (SumPuz.img_54 s_5 y_2)) c_0) in SumPuz.ofAll (SumPuz.curry f_4 (SumPuz.fst qr_1_0)) (SumPuz.bindings_51 z_3 (Flite.Cons (SumPuz.snd qr_1_0) Flite.Nil) s_5)
SumPuz.curry !f_0 x_1 y_2 = f_0 (Flite.Pair x_1 y_2)
SumPuz.img_54 !lds_0 !l_1::I = SumPuz.fromJust (SumPuz.lookup_52 l_1 lds_0)
SumPuz.fromJust !_x_0 = select _x_0 (Flite.Just x_1_0 -> x_1_0)
SumPuz.divMod10 !n_0::I = <{SumPuz._c;100;3_61}> (<{SumPuz.<=_39}> n_0 9) n_0
<{SumPuz.<=_39}>::B !x_0::I !y_1::I = not (ltI y_1 x_0)
<{SumPuz._c;100;3_61}> !_x_0::B n_1::I = select _x_0 (True -> Flite.Pair 0 n_1) (False -> <{SumPuz._c;103;7_60}> (SumPuz.divMod10 (subI n_1 10)))
<{SumPuz._c;103;7_60}> !_x_0 = select _x_0 (Flite.Pair q_1_0 r_1_1 -> Flite.Pair (addI q_1_0 1) r_1_1)
<{SumPuz._c;83;3_70}> !_x_0::B z_1::I clds_2 = select _x_0 (False -> Flite.Nil) (True -> SumPuz.bindings_51 z_1 (Flite.Cons 1 Flite.Nil) (SumPuz.snd clds_2))
<{SumPuz._c;78;3_69}> !_x_0::B clds_1 = select _x_0 (False -> Flite.Nil) (True -> Flite.Cons (SumPuz.snd clds_1) Flite.Nil)
SumPuz.isSingleton::B !_x_0 = select _x_0 (Flite.Nil -> False) (Flite.Cons x_1_0 _x_1_1 -> select _x_1_1 (Flite.Nil -> True) (Flite.Cons y_2_0 ys_2_1 -> False) )
SumPuz.len::I !xs_0 = SumPuz.lenAcc 0 xs_0
SumPuz.lenAcc::I !acc_0::I !_x_1 = select _x_1 (Flite.Nil -> acc_0) (Flite.Cons x_1_0 xs_1_1 -> SumPuz.lenAcc (addI acc_0 1) xs_1_1)
SumPuz.and::B !_x_0::B x_1::B = if _x_0 x_1 False
SumPuz.sumMap::I f_0 !xs_1 = SumPuz.sumMapAcc_44 f_0 xs_1 0
SumPuz.sumMapAcc_44::I f_0 !_x_1 !acc_2::I = select _x_1 (Flite.Nil -> acc_2) (Flite.Cons x_1_0 xs_1_1 -> SumPuz.sumMapAcc_44 f_0 xs_1_1 (addI (f_0 x_1_0) acc_2))
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
tests/postponed/Taut.sapl 0 → 100644
View file @ 4ac88b5e
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)
Supports Markdown
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