-
Notifications
You must be signed in to change notification settings - Fork 510
Expand file tree
/
Copy pathnub.golden.pir
More file actions
52 lines (52 loc) · 1.58 KB
/
Copy pathnub.golden.pir
File metadata and controls
52 lines (52 loc) · 1.58 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
letrec
!go : list integer -> list integer -> list integer
= \(l : list integer) (xs : list integer) ->
case
(list integer)
l
[ (\(y : integer) ->
letrec
!go : list integer -> bool
= \(xs : list integer) ->
case
bool
xs
[ (\(x : integer) (xs : list integer) ->
case
(all dead. bool)
(equalsInteger x y)
[(/\dead -> go xs), (/\dead -> True)]
{all dead. dead})
, False ]
in
\(ys : list integer) ->
case
(all dead. list integer)
(go xs)
[ (/\dead ->
mkCons {integer} y (go ys (mkCons {integer} y xs)))
, (/\dead -> go ys xs) ]
{all dead. dead})
, [] ]
in
\(xs : list integer) ->
let
!eta : list integer
= (let
b = list integer
in
\(f : integer -> b -> b) (acc : b) ->
letrec
!go : list integer -> b
= \(xs : list integer) ->
case
b
xs
[(\(x : integer) (xs : list integer) -> f x (go xs)), acc]
in
go)
(mkCons {integer})
xs
xs
in
go eta []