-
Notifications
You must be signed in to change notification settings - Fork 2
/
Test1.spad
55 lines (46 loc) · 1015 Bytes
/
Test1.spad
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
)abbrev domain TEST1 Test1
Test1() : Exports == Implementation where
NNI ==> NonNegativeInteger
PI ==> PositiveInteger
I ==> Integer
F ==> Float
S ==> String
Exports ==> with
foo : I -> I
foo : F -> F
bar : (I, I) -> I
fib : NNI -> NNI
Implementation ==> add
import F
import PI
import NNI
import I
foo (a : I) ==
a2 := a * a
ma := - a
r :=
if a >= 0
then ma * 2
else a2 + 2
r + 3
-- [BUG] Type checker should remember that {foo : I -> I} has been already
-- defined.
-- foo a == a + 1
foo (a : F) == a + 1.0
baz : (I, I) -> I
bar (x, y) ==
if x > 0 then
y := -10
nx := baz(x, y)
else
nx := -x
nx + y
-- a global value :)
magic := 2
baz (x, y) ==
bar := x * y -- bar already defined earlier as a function
bar - magic
fib n ==
n = 0 => 0
n = 1 => 1
fib((n - 1) :: NNI) + fib((n - 2) :: NNI)