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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
module Map
use int.Int
use list.List
use list.Map
use coma.Std
use coma.List
let case (l: list int) (cons (h: int) (t: list int)) (nil)
= unList <int> {l} cons nil
let map3 (l: list int) (f: int -> int) (return (r: list int))
= loop {l} return
[ loop (l: list int) {} (ret (r: list int) {r = map f l}) =
case {l}
(fun (h: int) (t: list int) ->
(! loop {t} . fun (r: list int) ->
ret {Cons (f h) r}))
(ret {Nil: list int})
]
let map2 (l: list int) (f: int -> int) {} (return (r: list int) {r = map f l})
= loop {l} return
[ loop (l: list int) {} (ret (r: list int) {r = map f l}) =
case {l}
(fun (h: int) (t: list int) ->
(! loop {t} . fun (r: list int) ->
ret {Cons (f h) r}))
(ret {Nil: list int})
]
let test2 {} (return (r: list int) {r = Cons 1 (Cons 1 (Cons 1 Nil))})
= map2 {Cons 0 (Cons 0 (Cons 0 Nil))}
{fun (x:int) -> x + 1}
return
let test3 {} (return (r: list int) {r = Cons 1 (Cons 1 (Cons 1 Nil))})
= map3 {Cons 0 (Cons 0 (Cons 0 Nil))}
{fun (x:int) -> x + 1}
return
-- let test4 (l: list int) (f : int -> int) (return (r: list int))
-- =
-- -{ f 0 = 1 }-
-- -{ for_all (fun x -> x = 0) l }-
-- (! map2 {l} {f} ret)
-- [ ret (r: list int) -> { for_all (fun x -> x = 1) r } (! return {r})]
end
module MapS
use int.Int
use seq.Seq
use seq.FreeMonoid
use coma.Std
predicate is_map (f: int -> int) (l1 l2: seq int) =
length l1 = length l2 /\
forall i. 0 <= i < length l1 -> (f l1[i]) = l2[i]
let map2 (l: seq int) (f: int -> int) {} (return (r: seq int) {is_map f l r})
= loop {0}
[ loop (i: int)
{ 0 <= i <= length l }
{ length l = length res }
{ forall j. 0 <= j < i -> (f l[j]) = res[j] } =
if {i = length l}
(-> return {res})
(-> [ &res <- set res i (f l[i]) ] loop {i+1})
]
[ &res: seq int = create (length l) (fun x -> 0) ]
-- predicate pre_f (x: int)
-- let map (l: seq int) {} (f [ext...] (x: int) {pre_f x} (ret (xx: int) {})) (return (r: seq int) {}) --{is_map f l r})
-- = loop {0}
-- [ loop (i: int)
-- { 0 <= i <= length l }
-- { length l = length res } =
-- -- { forall j. 0 <= j < i -> (f l[j]) = res[j] } =
-- if {i = length l}
-- (-> return {res})
-- (-> f {l[i]} (fun (r: int) -> [ &res <- set res i r ] loop {i+1}))
-- ]
-- [ &res: seq int = create (length l) (fun x -> 0) ]
let test4 (l: seq int) (f : int -> int) (return (r: seq int))
=
-{ f 0 = 1 }-
-{ forall i. 0 <= i < length l -> l[i] = 0 }-
(! map2 {l} {f} ret)
[ ret (r: seq int) -> { forall i. 0 <= i < length r -> r[i] = 1 } (! return {r})]
end
|
