@@ -47,15 +47,26 @@ pred len.aux o:list A, o:int.
4747% When `N` is bound, we count down from `N` to `0`, removing one element of
4848% `Ls` with each unit of `N` removed. If we arrive at `[]` and `0` at the
4949% same time, we are done, and cannot possibly have more conclusions (thus the cut).
50+ len _ N :-
51+ ground_term N,
52+ N < 0,
53+ std.fatal-error "len with negative number".
5054len Ls N :-
51- if (var N)
52- ( ( len.aux Ls N
53- & pi L M M' \
54- len.aux L M :- M' is M + 1, len.aux [_|L] M'
55- ) => len.aux [] 0 )
56- ( ( len.aux [] 0
57- & pi T M M' \ len.aux [_|T] M :- M' is M - 1 , len.aux T M'
58- ) => len.aux Ls N, ! ).
55+ var Ls, var N,
56+ ( ( len.aux Ls N
57+ & pi L M M' \
58+ len.aux L M :- M' is M + 1, len.aux [_|L] M'
59+ ) => len.aux [] 0
60+ ).
61+ len Ls N :-
62+ not (var Ls),
63+ std.length Ls N,
64+ ! .
65+ len Ls N :-
66+ not (var N),
67+ ( ( len.aux [] 0
68+ & pi T M M' \ len.aux [_|T] M :- M' is M - 1 , len.aux T M'
69+ ) => len.aux Ls N, ! ).
5970
6071% When `N` is free, then we count up, starting from `0` to `N`, constructing
6172% a list by adding a free variable to our list each time a unit is added to
@@ -233,7 +244,7 @@ rotate Ls N Ls' :- if (N > 0)
233244
234245% 1.20
235246pred select-nth i:int, i:list A, o:A, o:list A.
236- select-nth N Ls X Rest :- len Prefix {calc (N - 1)}
247+ select-nth N Ls X Rest :- len Prefix N
237248 & std.append Prefix [X|Suffix] Ls
238249 & std.append Prefix Suffix Rest
239250 .
@@ -255,35 +266,38 @@ range N N' [N|Ns] :- range {util.succ N} N' Ns.
255266pred select-rnd i:int, i:list A, o:list A.
256267pred select-rnd.aux i:int, i:int, i:list A, o:list A.
257268select-rnd N Ls Xs :-
258- random.self_init,
259- ( select-rnd.aux N _ _ Xs
260- & select-rnd.aux _ 0 _ Xs
269+ ( (select-rnd.aux N _ _ Xs :- !)
270+ & (select-rnd.aux _ 0 _ Xs :- !)
261271 & pi M M' Len Len' Opts Acc X Rest Idx\
262- select-rnd.aux M Len Opts Acc :-
263- random.int Len Idx,
264- select-nth Idx Opts X Rest,
265- util.succ M M' ,
266- util.succ Len' Len,
267- select-rnd.aux M' Len' Rest [X|Acc]
268- ) => select-rnd.aux 0 {len Ls} Ls []
272+ select-rnd.aux M Len Opts Acc :-
273+ random.int Len Idx,
274+ select-nth Idx Opts X Rest,
275+ util.succ M M' ,
276+ util.succ Len' Len,
277+ select-rnd.aux M' Len' Rest [X|Acc]
278+ ) => (
279+ std.length Ls Len0,
280+ select-rnd.aux 0 Len0 Ls []
281+ )
269282 .
270283
271284% 1.24
272285pred lotto i:int, i:int, o:list int.
273286pred lotto.draw i:int, o:list int.
274287lotto Draws Limit Nums :-
275- random.self_init,
276288 ( lotto.draw Draws Nums
277289 & pi Draw Draw' N Acc\
278- lotto.draw Draw Acc :-
279- random.int Limit N,
280- util.succ Draw Draw' ,
281- lotto.draw Draw' [N| Acc]
290+ lotto.draw Draw Acc :-
291+ random.int Limit N,
292+ util.succ Draw Draw' ,
293+ lotto.draw Draw' [N| Acc]
282294 ) => lotto.draw 0 []
283295 .
284296
285297
286- % TODO: 1.25
298+ % 1.25
299+ pred rnd- permu i: list int, o: list int.
300+ rnd- permu Ls Permutation :- select- rnd {std.length Ls} Ls Permutation.
287301
288302}
289303
@@ -299,7 +313,8 @@ test P :- Msg is "Test '" ^ {term_to_string P} ^ "' FAILED!"
299313shorten list.{ ls, el, one, many }.
300314
301315pred tests.
302- tests :- test (list.last [1 , 2 , 3 , 4 ] (some 4 ))
316+ tests :- random.self_init
317+ & test (list.last [1 , 2 , 3 , 4 ] (some 4 ))
303318 & test (list.second- last [1 ,2 ,3 ,4 ] (some 3 ))
304319 & test (list.nth [1 ,2 ,3 ,4 ] 2 (some 3 ))
305320 & test (list.len [1 ,2 ,3 ,4 ] 4 )
@@ -332,11 +347,14 @@ tests :- test (list.last [1, 2, 3, 4] (some 4))
332347 & test (list.slice 4 8 [1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ,9 ,10 ] [5 ,6 ,7 ,8 ,9 ])
333348 & test (list.rotate [1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ] 3 [4 ,5 ,6 ,7 ,8 ,1 ,2 ,3 ])
334349 & test (list.rotate [1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ] - 2 [7 ,8 ,1 ,2 ,3 ,4 ,5 ,6 ])
335- & test (list.select- nth 2 [1 ,2 ,3 ,4 ] 2 [1 ,3 ,4 ])
350+ & test (list.select- nth 2 [1 ,2 ,3 ,4 ] 3 [1 ,2 ,4 ])
336351 & test (list.insert- at 10 2 [1 ,2 ,3 ,4 ] [1 ,2 ,10 ,3 ,4 ])
337352 & test (list.range 4 9 [4 ,5 ,6 ,7 ,8 ,9 ])
338353 & test (list.select- rnd 3 [1 ,2 ,3 ,4 ,5 ,6 ,7 ,8 ] [_, _, _])
339- & test (list.lotto 3 10 LottoDraw, std.forall LottoDraw (x\x < 10 ))
354+ & test ( list.lotto 3 10 LottoDraw,
355+ std.forall LottoDraw (x\x < 10 ))
356+ & test ( list.rnd- permu [1 ,2 ,3 ,4 ] RndPermu,
357+ std.forall RndPermu (x\ std.mem [1 ,2 ,3 ,4 ] x))
340358 .
341359
342360pred main.
0 commit comments