{- $Id: test.xsg,v 1.1.2.22 2009/02/20 18:00:05 orlov Exp $ -}
{- vim: set syntax=xsg expandtab tabstop=4: -}
mytest : 0, 1
mytest, ?x = myg, x = myf, x
myg : 0, 1
myg, ?x
undef : 0,1
undef, A = B, A
myf : 0, 1
myf, undef
EQ: 1
PARSE: 2
----------------------------- tests ---------------------------------
test1, test2, test3, test4, test5, test6 : 0,1
--test1 , ?x = show exp, ?y = parse x, cons x y --doesn't work? :(
test6, parse ?x = ?y, PARSE x EQ y
myundef : 0,1
myundef, !y
--test1: 0,2
--test1, ?x1 = myundef, ?x2 = myundef, x1 = x2, (_0) cons x1 x2
-- , ?x1 = myundef, ?x2 = myundef, (_2) cons x1 x2
-- , ?x = myundef, x = id x, (_3) x
-- , @x = myundef, x = id x, (_4) x
-- , sum' _2 (I I I I !y) = I I I I ?x, (_5) x
--test1, ?x = myundef, x
test1, @x = undef, true
test2, ?x = undef, true
test3, sum _5 _6
test4, sum _3 I I I I undef = I I I I I I ?y, y
test5, sum' _3 I I I I undef = I I I I I I ?y, y
sum, sum': int int, int
sum @x @y, sum' x y -- sum is a strict version of sum'
sum' O O, O
O ?x, x = I ?x', x
?x O, x = I ?x', x
I ?x I ?y, I I sum' x y
----------------------------------SL = Stupid Language-----------------------------------------------------
sl_assign: sl_exp sl_exp sl_stmt -- lhs rhs next
sl_print: sl_exp sl_stmt -- output next
sl_var: string
sl_const: integer
-- sl_undef:
sl_bind: string integer sl_bind -- var value next
sl_nil:
X:
Y:
Z:
sl_neq: 2,1
sl_neq X Y, true
X Z, true
Y Z, true
Y X, true
Z X, true
Z Y, true
-- need # ??
sl_prog1: , sl_prog
sl_prog1, sl_assign sl_var X sl_const _2
sl_assign sl_var Y sl_var X
sl_assign sl_var X sl_const _1
sl_print sl_var X
sl_print sl_var Y
sl_print sl_const _3
sl_nil
sl_run: sl_prog, integer_list
sl_run ?prog, sl_eval prog env_empty
sl_eval: 2,1
sl_eval sl_nil ?env, nil
sl_assign ?lhs ?rhs ?next ?env, sl_eval next (env_update env lhs rhs)
sl_print ?output ?next ?env, cons (env_value env output) sl_eval next env
env_empty: 0,1
env_empty, sl_nil
env_concat: 2,1
env_concat env_empty ?env, env
sl_bind ?var ?value ?next ?env, sl_bind var value env_concat next env
env_value: 2,1
env_value ?env sl_const ?const, const
env_concat ?env1 sl_bind ?var ?value ?env2 sl_var var, value
env_update: 3,1
env_update ?env (sl_var ?var) ?rhs
, env_undef env var = true
, ?value = env_value env rhs
, sl_bind var value env
?env (sl_var ?var) ?rhs
, env = env_concat ?env1 sl_bind var ?value ?env2
, ?value = env_value env rhs
, env_concat env1 sl_bind var value env2
env_undef: 2,1
env_undef env_empty ?var, true
sl_bind ?var1 ?value ?next ?var2, sl_neq var1 var2 = true, env_undef next var2 = true, true
sl_get_next: 1,1
sl_get_next (sl_assign ?lhs ?rhs ?next), next
(sl_print ?output ?next), next
sl_unget_next: 1,1
sl_unget_next (sl_get_next ?next), next
sl_prints_vars: 1,1
sl_prints_vars (sl_print sl_var ?var ?next), true
(sl_unget_next ?next), sl_prints_vars next
sl_test1: 0,1
sl_test1, sl_run sl_prog1
sl_test2: 0,2
sl_test2, sl_run ?prog = ?res, prog res
sl_test3: 0,2
sl_test3, sl_run ?prog = ?res, sl_prints_vars prog = true, prog res
---------------------------------------------------------------------------------------
op_plus: 2
op_minus: 2
op_var: 1
op_const: 1
exp : 0, 1
exp, op_plus op_minus op_var _1 op_const _3 op_var _2
str1 : 0,1
str1, cons (sym_var (cons A nil)) cons sym_minus cons (sym_const (I I I O)) cons sym_plus cons (sym_var (cons B nil)) nil
-- X1 - 3 + X2
sym_plus:
sym_minus:
sym_open:
sym_close:
sym_const: 1
sym_var: 1
sym2op: exp1 exp2 sym, exp
sym2op ?e1 ?e2 sym_plus, op_plus e1 e2
?e1 ?e2 sym_minus, op_minus e1 e2
delay : int a, a
delay O ?x, x
I ?n ?x, delay n x
show : exp, string
show op_const ?value, cons sym_const value nil
op_var ?name, cons sym_var name nil
sym2op ?e1 ?e2 ?sym, concat show e1 cons sym show e2
-- ?e, delay _10 cons sym_open concat show e cons sym_close nil
parse : string, exp
parse (show ?e), e
-- exp ::= term | term + exp | term - exp
-- term ::= var | const | ( exp )
exp_token :
term_token :
eval : 1 , 2
eval exp_token, eval term_token
exp_token, ?x1 ?y1 = eval term_token, ?x2 ?y2 = eval exp_token,
concat x1 cons sym_plus x2 op_plus y1 y2
exp_token, ?x1 ?y1 = eval term_token, ?x2 ?y2 = eval exp_token,
concat x1 cons sym_minus x2 op_minus y1 y2
term_token, ?x1 ?y1 = eval exp_token,
cons sym_open concat x1 sym_close y1
term_token, cons sym_var ?x nil op_var x
term_token, cons sym_const ?x nil op_const x
parse' : 1,1
parse' ?x, eval exp_token = x ?y, y
---------------------------------------------------------------------
period : integer char, string
period ?n ?c, ?x = concat take n repeat c x, x
perm : integer, integer_list
perm O , cons O nil
-- ?n, n = I ?m, ?xs ?ys = split (perm m), concat xs (cons n ys)
?n, ?m = sub n _1 = integer, ?xs ?ys = split (perm m), concat xs (cons n ys)
-- ?n, ?m defined = sub2 n _1, ?xs ?ys = split (perm m), concat xs (cons n ys)
integer : , integer
integer , O
, I integer
defined:
sub2 : integer ingteger, integer bool
sub2 ?x O , x defined
I ?x I ?y, sub x y defined
-- eqSet : list list, bool
-- eqSet ?x ?y, isSubSet x y = true, isSubSet y x = true, true
isSubSet : list list, bool
isSubSet nil ?ys, true
cons ?x ?xs ?ys, isElem x ys = true, isSubSet xs ys = true, true
integerList : , integer_list
integerList , integerList' O
integerList' : integer, integer_list
integerList' ?n, cons n integerList' I n
perm' : integer, integer_list
perm' ?n, ?x, length x = n, isSubSet (take n integerList) x = true, x
--main : , _
--main , length (concat (cons A nil) nil)
A:
B:
C:
D:
abcd : , string
abcd , cons A cons B cons C cons D nil
abcba : , string
abcba , cons A cons B cons C cons B cons A nil
isPolyndrom : string , bool
isPolyndrom ?x, x = reverse x, true
reverse : a_list , a_list
reverse nil
cons ?x nil
cons ?x concat ?xs cons ?y nil, cons y concat reverse xs cons x nil
reverse' : a_list , a_list
reverse' ?x, reverse'' x nil
reverse'' : _ _ , _
reverse'' nil ?ys, ys
cons ?x ?xs ?ys, reverse'' xs cons x ys
--------------------------- hack? -------------------------------------
cons : 2
nil : 0
--nil : , _
-- cons : _ _ , _
{-
cons' : a a_list integer
nil, cons' ?x ?xs O
cons ?x ?xs, xs = cons' ?y ?ys ?n, cons' x xs I n
length' : a_list, integer
length' cons' ?x ?xs ?n, n
-}
isNil : 1, 1
isNil nil, true
isEq : 2, 1
isEq ?x ?y, x = y, true
_node : key left right
node : _, _
node ?x, _node x ?l ?r
link: _ _, _
link ?xs ?ys, xs = _node ?cx ?lx ?rx, ys = _node ?cy ?ly ?ry, ly = xs, rx = ys, true
link': _ _, _
link' ?xs ?ys, link xs ys = true, xs
link'': _ _, _
link'' ?xs ?ys, xs = _node ?cx ?lx ?rx, ys = _node ?cy ?ly ?ry, ly = xs, rx = ys, xs
--cons ?c nil, x = node c x x, x
-- ?c ?xs, xs = node ?d ?l ?r, ?x = node c xs
--unbind node ?c ?l ?r,
-- cons ?c (__list ?h ?t), ?x = __list (__node c x h) t, x
----------------------------------------------------------------------
hang : 0, 1
hang , hang
id : a, a
id ?x, x
dup : a, a a
dup ?x, x x
swap : a b, b a
swap ?x ?y, y x
fst : a b, a
fst ?x ?y, x
snd : a b, b
snd ?x ?y, y
------------------------------ bool -----------------------------------
true :
false :
or : bool bool , bool
or { true ?x, true; ?x true, true; false false, false; }
and : bool bool , bool
and false ?x , false
?x false, false
true true , true
-------------------------------- list ---------------------------------
head : a_list, a
head (cons ?x ?y), x
tail : a_list, a_list
tail (cons ?x ?y), y
repeat : a, a_list
repeat ?x, ?y = cons x y, y
repeat' : a, a_list
repeat' ?x, cons x repeat' x
concat : a_list a_list, a_list
concat (nil ) ?ys, ys
(cons ?x ?xs) ?ys, cons x (concat xs ys)
cycle : a_list, a_list
cycle nil, nil
?xs, xs = cons ?a ?b, ?ys = concat xs ys, ys
split' : a_list, a_list a_list
split' (concat ?xs ?ys), xs ys
split : a_list, a_list a_list
split ?xs , nil xs
cons ?x ?xs, ?ys ?zs = split xs, (cons x ys) zs
isElem : a a_list, bool
isElem ?x (concat ?xs cons x ?ys), true
elem : a_list, a
elem (concat ?xs cons ?x ?ys), ?x
some: list_a, a
some cons ?x ?xs, x
cons ?x ?xs, some xs
lookup: 2,1
lookup ?ps ?x, cons x ?y = some ps, y
zip : a_list b_list, ab_list
zip (nil ) (nil ), nil
(cons ?x ?xs) (cons ?y ?ys), cons (cons x y) (zip xs ys)
-- too poor zip, cannot generate a cycle given 2 cycles
zip2 : a_list b_list, ab_list
zip2 ?x ?y, zip2' emptyqs x y
zip2' : abc_pairs a_list b_list, ab_list
zip2' ?qs (nil) (nil), nil
?qs (cons ?u ?v) (nil), nil
?qs (nil) (cons ?u ?v), nil
?qs (?x ) (?y ), x = cons ?u ?v, y = cons ?u ?v, findqs qs x y
?qs (?x ) (?y ), x = cons ?xu ?xv, y = cons ?yu ?yv, ?z = cons cons xu yu (zip2' (addqs qs x y z) xv yv), z
zip3 : a_list b_list, ab_list
zip3 (concat ?x0 cycle ?x1) (concat ?y0 cycle ?y1), length x0 = length y0, length x1 = length y1,
concat (zip x0 y0) cycle (zip x1 y1)
emptyqs : 0, 1
emptyqs, nil
findqs : 3, 1
findqs ?q ?x ?y, lookup q cons x y
addqs : 4, 1
addqs ?qs ?x ?y ?z, cons cons cons x y z qs
test7 : 0, 1
test7, ?x = cons A x, ?y = cons B cons C y, zip2 x y
------------------------------- integer ---------------------------------
O : 0
I : 1
_0 : , integer
_0 , O
_1 : , integer
_1 , I O
_2 : , integer
_2 , I I O
_3 : , integer
_3 , I I I O
_4 : , integer
_4 , I I I I O
_5 : , integer
_5 , I I I I I O
_6 : , integer
_6 , I I I I I I O
_7 : , integer
_7 , I I I I I I I O
_8 : , integer
_8 , I I I I I I I I O
_9 : , integer
_9 , I I I I I I I I I O
_10 : , integer
_10 , I I I I I I I I I I O
add : integer integer, integer
add O ?y, y
I ?x ?y, I add x y
mul : integer integer, integer
mul O ?y, O
I ?x ?y, add y mul x y
sub : integer integer, integer
sub ?x O , x
I ?x I ?y, sub x y
sub' : integer integer, integer
sub' (add ?x ?y) x, y
sub'' : integer integer, integer
sub'' (add ?x ?y) y, x
greater : integer integer, bool
greater I ?n O , true
O ?n , false
I ?n I ?m, greater n m
greater' : integer integer, bool
greater' ?x ?y, sub x y = I ?z, true
isNotPrime : integer, bool
isNotPrime ?x, x = mul ?y ?z, greater' y _1 = true, greater' z _1 = true, true
eq : a a, bool
eq O O, true
(I ?x) O, false
O (I ?x), false
(I ?x) (I ?y), eq x y
nil nil , true
(cons ?a ?b) nil, false
nil (cons ?a ?b), false
(cons ?a ?b) (cons ?c ?d), and (eq a b) (eq c d)
----------------------------- rational! ----------------------------------
Q0, Q1: 1
q0, q1: 0
_1_3: 0,1
_1_3, ?x = Q0 Q1 x, x
----------------------------- list + integer -----------------------------
length : a_list, integer
length (nil ), O
(cons ?x ?xs), I length xs
take : integer a_list, a_list
take (O ) (?xs ), nil
(I ?n) (cons ?x ?xs), cons x take n xs
drop : integer a_list, a_list
drop (O ) (?xs ), xs
(I ?n) (cons ?x ?xs), drop n xs
splitAt : integer a_list, a_list a_list
splitAt (O ) (?xs ), nil xs
(I ?n) (cons ?x ?xs), cons x splitAt n xs
takeAt : integer a_list, a
takeAt (O ) (cons ?x ?xs), x
(I ?n) (cons ?x ?xs), takeAt n xs
take' : integer a_list, a_list
take' length ?xs concat xs ?ys, xs
drop' : integer a_list, a_list
drop' length ?xs concat xs ?ys, ys
splitAt' : integer a_list, a_list a_list
splitAt' length ?xs concat xs ?ys, xs ys
splitAt'' : a_list integer, a_list a_list
splitAt'' concat ?xs ?ys length xs, xs ys
takeAt' : integer a_list, a
takeAt' length ?xs (concat xs cons ?y ?ys), y
elemIndices : a a_list, integer
elemIndices ?x (concat ?xs cons x ?ys), length xs
combs : integer integer, i_list
combs O O , nil
?k (I ?n), cons A (combs k n)
(I ?k) (I ?n), cons B (combs k n)
---------------------- BrainFuck -----------------------
bf_stop: 0
bf_left, bf_right, bf_inc, bf_dec, bf_in, bf_out: 1
bf_if: 2
bf_eval: bf_prog list list bf_inputs, bf_outputs
bf_eval bf_left ?prog (cons ?x ?xs) ?ys ?i, bf_eval prog xs (cons x ys) i
bf_right ?prog ?xs (cons ?y ?ys) ?i, bf_eval prog (cons y xs) ys i
bf_inc ?prog ?xs (cons ?y ?ys) ?i, bf_eval prog xs (cons I y ys) i
bf_dec ?prog ?xs (cons I ?y ?ys) ?i, bf_eval prog xs (cons y ys) i
bf_out ?prog ?xs ?ys ?i, cons (head ys) (bf_eval prog xs ys i)
bf_in ?prog ?xs (cons ?y ?ys) (cons ?i ?is), bf_eval prog xs (cons i ys) is
bf_if ?prog1 ?prog2 ?xs ?ys ?i, head ys = O, bf_eval prog2 xs ys i
bf_if ?prog1 ?prog2 ?xs ?ys ?i, head ys = I ?n, bf_eval prog1 xs ys i
bf_stop ?xs ?ys ?i, nil
-- choose ?prog O, prog ?x
-- ?prog I ?n, ?x prog
-- bf_eval bf_if (choose ?prog head ?ys) ?xs ys, bf_eval prog xs ys
bf_p1: , bf_prog
bf_p1, ?p = bf_if bf_dec bf_right bf_inc bf_left p bf_right bf_out bf_stop, bf_inc bf_inc p
bf_int: bf_prog bf_inputs, bf_outputs
bf_int ?prog ?i, bf_eval prog (repeat O) (repeat O) i
blabla: 0,1
blabla, !y
f : 0, 1
--f, _2
f , f
g : 2, 1
g ?x x, x = id x, O
ff : 0, 1
ff, ?x = f, (g x x)
ff' : 1, 2
ff' ?y, ?x = f, (g x y) x
ff'' : 0, 1
ff'', ff' ?y = ?z y, z
---------------------- Sequence -----------------------
X1,X2,X3,X4,X5,X6,X7,X8,X9 : 0
_27 : , integer
_27 , I I I I I I I I I I I I I I I I I I I I I I I I I I I O
sequence, sequence2 : , list
sequence, ?x = cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w nil,
x = concat ?w cons X9 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X9 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X9 ?w,
x = concat ?w cons X8 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X8 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X8 ?w,
x = concat ?w cons X7 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X7 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X7 ?w,
x = concat ?w cons X6 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X6 cons ?w cons ?w cons ?w cons ?w cons ?w cons ?w cons X6 ?w,
x = concat ?w cons X5 cons ?w cons ?w cons ?w cons ?w cons ?w cons X5 cons ?w cons ?w cons ?w cons ?w cons ?w cons X5 ?w,
x = concat ?w cons X4 cons ?w cons ?w cons ?w cons ?w cons X4 cons ?w cons ?w cons ?w cons ?w cons X4 ?w,
x = concat ?w cons X3 cons ?w cons ?w cons ?w cons X3 cons ?w cons ?w cons ?w cons X3 ?w,
x = concat ?w cons X2 cons ?w cons ?w cons X2 cons ?w cons ?w cons X2 ?w,
x = concat ?w cons X1 cons ?w cons X1 cons ?w cons X1 ?w,
x
sequence2, length ?x = _27,
x = concat ?a1 cons X9 concat ?a2 cons X9 concat ?a3 cons X9 ?a4, length a2 = length a3 = _9,
x = concat ?a1 cons X8 concat ?a2 cons X8 concat ?a3 cons X8 ?a4, length a2 = length a3 = _8,
x = concat ?a1 cons X7 concat ?a2 cons X7 concat ?a3 cons X7 ?a4, length a2 = length a3 = _7,
x = concat ?a1 cons X6 concat ?a2 cons X6 concat ?a3 cons X6 ?a4, length a2 = length a3 = _6,
x = concat ?a1 cons X5 concat ?a2 cons X5 concat ?a3 cons X5 ?a4, length a2 = length a3 = _5,
x = concat ?a1 cons X4 concat ?a2 cons X4 concat ?a3 cons X4 ?a4, length a2 = length a3 = _4,
x = concat ?a1 cons X3 concat ?a2 cons X3 concat ?a3 cons X3 ?a4, length a2 = length a3 = _3,
x = concat ?a1 cons X2 concat ?a2 cons X2 concat ?a3 cons X2 ?a4, length a2 = length a3 = _2,
x = concat ?a1 cons X1 concat ?a2 cons X1 concat ?a3 cons X1 ?a4, length a2 = length a3 = _1,
x
---------------------- Flock of geese -----------------------------------------------------
half: 1, 1
half add ?x x, x
flock: 0, 1
flock, add ?x (add x (add half x (add (half half x) _1))) = mul _10 _10, x
----------------------- Spies --------------------------------
spies : 0,1
spies, ?xs = cons ?x0 cons ?x1 cons ?x2 cons ?x3 cons ?x4 cons ?x5 cons ?x6 nil,
takeAt x0 xs = _1,
takeAt x1 xs = _2,
takeAt x2 xs = _3,
takeAt x3 xs = _4,
takeAt x4 xs = _5,
takeAt x5 xs = _6,
takeAt x6 xs = _0,
xs
----------------------- Fish puzzle --------------------------------
True : 0
checkOne : 6, 1
checkOne ?a1 ?a2 ?a3 ?a4 ?a5 a1, True
?a1 ?a2 ?a3 ?a4 ?a5 a2, True
?a1 ?a2 ?a3 ?a4 ?a5 a3, True
?a1 ?a2 ?a3 ?a4 ?a5 a4, True
?a1 ?a2 ?a3 ?a4 ?a5 a5, True
listCheck : 10, 1
listCheck ?a1 ?a2 ?a3 ?a4 ?a5 ?b1 ?b2 ?b3 ?b4 ?b5,
checkOne a1 a2 a3 a4 a5 b1 = True,
checkOne a1 a2 a3 a4 a5 b2 = True,
checkOne a1 a2 a3 a4 a5 b3 = True,
checkOne a1 a2 a3 a4 a5 b4 = True,
checkOne a1 a2 a3 a4 a5 b5 = True,
True
samePlace : 2, 2
samePlace Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a1 b1
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a2 b2
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a3 b3
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a4 b4
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a5 b5
near : 2, 2
near Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a1 b2
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a2 b3
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a3 b4
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a4 b5
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a2 b1
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a3 b2
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a4 b3
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5 Quintuple ?b1 ?b2 ?b3 ?b4 ?b5, a5 b4
leftOf : 1, 2
leftOf Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a1 a2
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a1 a3
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a1 a4
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a1 a5
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a2 a3
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a2 a4
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a2 a5
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a3 a4
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a3 a5
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a4 a5
leftOf' : 1, 2
leftOf' Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a1 a2
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a2 a3
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a3 a4
Quintuple ?a1 ?a2 ?a3 ?a4 ?a5, a4 a5
Yellow, Red, Green, Blue, White : 0
Norwegian, Dane, Brit, German, Swede : 0
Dunhill, Blend, PallMall, Prince, Bluemaster : 0
Cat, Horse, Bird, Fish, Dog : 0
Water, Tea, Milk, Coffee, Beer : 0
Quintuple : 5
fish : 0, 5
fish, listCheck ?c1 ?c2 ?c3 ?c4 ?c5 Yellow Red Green Blue White = True,
listCheck ?n1 ?n2 ?n3 ?n4 ?n5 Norwegian Dane Brit German Swede = True,
listCheck ?s1 ?s2 ?s3 ?s4 ?s5 Dunhill Blend PallMall Prince Bluemaster = True,
listCheck ?d1 ?d2 ?d3 ?d4 ?d5 Water Tea Milk Coffee Beer = True,
listCheck ?p1 ?p2 ?p3 ?p4 ?p5 Cat Horse Bird Fish Dog = True,
?c = Quintuple c1 c2 c3 c4 c5,
?n = Quintuple n1 n2 n3 n4 n5,
?s = Quintuple s1 s2 s3 s4 s5,
?d = Quintuple d1 d2 d3 d4 d5,
?p = Quintuple p1 p2 p3 p4 p5,
samePlace n c = Brit Red,
samePlace n p = Swede Dog,
samePlace n d = Dane Tea,
leftOf' c = Green White,
samePlace c d = Green Coffee,
samePlace s p = PallMall Bird,
samePlace c s = Yellow Dunhill,
d3 = Milk,
near s p = Blend Cat,
n1 = Norwegian,
near p s = Horse Dunhill,
samePlace s d = Bluemaster Beer,
samePlace n s = German Prince,
near n c = Norwegian Blue,
near s d = Blend Water,
Quintuple c1 n1 s1 d1 p1
Quintuple c2 n2 s2 d2 p2
Quintuple c3 n3 s3 d3 p3
Quintuple c4 n4 s4 d4 p4
Quintuple c5 n5 s5 d5 p5
------------------ Driving task form Andrei Nemytykh ---------------------------
drive2 : 0, 1
drive2, concat ?eX concat ?eQ cons B cons ?sV concat ?eP cons A ?eY =
concat eY concat eP cons A cons sV concat eQ cons B eX
NIL : 0
Symbol : 1
Concat : 2
concat2 : 2, 1
concat2 NIL ?eY, eY
?eX ?eY, Concat eX eY
(Concat ?eX ?eY) ?eZ, Concat eX (concat2 eY eZ)
drive : 0, 1
drive, concat2 ?eX concat2 ?eQ Concat (Symbol B) Concat (Symbol ?sV) concat2 ?eP Concat (Symbol A) ?eY =
concat2 eY concat2 eP Concat (Symbol A) Concat (Symbol sV) concat2 eQ Concat (Symbol B) eX