-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathprelude.tls
118 lines (88 loc) · 2.79 KB
/
prelude.tls
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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
;;Foreign functions
;;Print function is reexported, so we can later redefine it
;;for each different datatype
(print a = _print a)
(eq a b = _eq a b)
;;Booleans
;;Shorthands for the data constructors of the boolean datatypes
(true = Bool True)
(false = Bool False)
;;(print (Bool a) = a)
;;Define the if clause, using pattern matching
;;(Only the relevant clause is evaluated, because the language is lazy)
(if (:literal true) a b = a)
(if (:literal false) a b = b)
;;We can define a little function we can use to test stuff
(assertEqual a b = (if (eq a b) () (print (Error a Is-not-equal-to b))))
;;Check if the booleans work :)
(assertEqual (if true Foo Bar) Foo)
(assertEqual (if false Foo Bar) Bar)
;;Some other boolean functions
(and (:literal true) (:literal true) = true)
(and (Bool a) (Bool a) = false)
(or (:literal false) (:literal false) = false)
(or (Bool a) (Bool a) = true)
(not (:literal false) = true)
(not (:literal true) = false)
;;Test those, using DeMorgan's laws (or the other way around)
(test-demorgan (Bool a) (Bool b) = (
(one = not (and (Bool a) (Bool b)))
(two = or (not (Bool a)) (not (Bool b)))
(assertEqual one two)
))
(test-demorgan true false)
(test-demorgan true true)
(test-demorgan false true)
(test-demorgan false false)
;;
;;Pairs
;;
;; Define the pair datatype
(cons a b = Pair a b)
(car (Pair a b) = a)
(cdr (Pair a b) = b)
;;(print (Pair a b) = print a . b)
;; Check if they work as well
(assertEqual (car (cons Foo Bar)) Foo)
(assertEqual (cdr (cons Foo Bar)) Bar)
;; Peano arithmetic
;; Define the Peano axioms
(0 = Nat Zero)
(+1 (Nat a) = Nat (Succ a))
;; Shortcuts for some numbers
(1 = +1 0)
(2 = +1 1)
(3 = +1 2)
(4 = +1 3)
(assertEqual (+1 1) 2)
(assertEqual (+1 2) 3)
;; The plus function
(+ (:literal 0) (Nat a) = Nat a)
(+ (Nat (Succ a)) (Nat b) = (+1 (+ (Nat a) (Nat b))))
(assertEqual (+ 0 0) 0)
(assertEqual (+ 0 1) 1)
;; May be occasionally useful
(assertEqual (+ 1 1) 2)
(assertEqual (+ 2 2) 4)
;; Lambdas
(map a (:lambda fun) = fun a)
;;Pass an existing function
(this-is a = (This Is a))
(assertEqual (map Foo this-is) (This Is Foo))
;;Pass an inline function (but be sure to give it a name)
(assertEqual (map Bar (fun a = (This Is a))) (This Is Bar))
;;Lists (WIP)
;; Define the list datatype
(list (:list elements) = elements)
(a-list = (list a b c d))
;; Some helper functions
(head (List list-head (:list list-tail)) = list-head)
(tail (List list-head (:list list-tail)) = list-tail)
(assertEqual (head (list A B C)) A)
(assertEqual (tail (list A B C)) (list B C))
;;(map (:lambda fun) (List list-head) = (list (fun list-head)) )
;;(map (:lambda fun) (List list-head (:rest list-tail)) = (List (fun list-head) (:rest (map fun list-tail))))
;;assetEqual (map (fun a = a a) (List a b c)) (List (a a) (b b) (c c))
(print (All systems go))
(foo a = a)
(foo bar)