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
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
{-# LANGUAGE NoImplicitPrelude #-}
-- declarations of builtin functions and data types used by the compiler
module Internals where
-- used for type annotations
typeAnn x = x
undefined :: forall (a :: Type) . a
primFix :: forall (a :: Type) . (a -> a) -> a
data Unit = TT
data String
data Empty (a :: String)
-- TODO: generate?
data Tuple0 = Tuple0
data Tuple1 a = Tuple1 a
data Tuple2 a b = Tuple2 a b
data Tuple3 a b c = Tuple3 a b c
data Tuple4 a b c d = Tuple4 a b c d
data Tuple5 a b c d e = Tuple5 a b c d e
-- ... TODO
-- builtin used for overlapping instances
parEval :: forall a -> a -> a -> a
type family JoinTupleType t1 t2 where
-- TODO
JoinTupleType a () = a
JoinTupleType a (b, c) = (a, b, c)
JoinTupleType a (b, c, d) = (a, b, c, d)
JoinTupleType a (b, c, d, e) = (a, b, c, d, e)
JoinTupleType a b = (a, b)
-- conjuction of constraints
type family T2 a b
-- equality constraints
type family EqCT (t :: Type) (a :: t) (b :: t)
type EqCTt = EqCT Type
--type instance EqCT t (a, b) (JoinTupleType a' b') = T2 (EqCT Type a a') (EqCT Type b b')
-- builtin conjuction of constraint witnesses
t2C :: Unit -> Unit -> Unit
-- builtin type constructors
data Int
data Word
data Float
data Char
data Bool = False | True
data Ordering = LT | EQ | GT
data Nat = Zero | Succ Nat
-- builtin primitives
primIntToWord :: Int -> Word
primIntToFloat :: Int -> Float
primIntToNat :: Int -> Nat
primCompareInt :: Int -> Int -> Ordering
primCompareWord :: Word -> Word -> Ordering
primCompareFloat :: Float -> Float -> Ordering
primCompareChar :: Char -> Char -> Ordering
primCompareString :: String -> String -> Ordering
primNegateInt :: Int -> Int
primNegateWord :: Word -> Word
primNegateFloat :: Float -> Float
primAddInt :: Int -> Int -> Int
primSubInt :: Int -> Int -> Int
primModInt :: Int -> Int -> Int
primSqrtFloat :: Float -> Float
primRound :: Float -> Int
primIfThenElse :: Bool -> a -> a -> a
primIfThenElse True a b = a
primIfThenElse False a b = b
isEQ EQ = True
isEQ _ = False
-- fromInt is needed for integer literal
class Num a where
fromInt :: Int -> a
compare :: a -> a -> Ordering
negate :: a -> a
instance Num Int where
fromInt = \x -> x
compare = primCompareInt
negate = primNegateInt
instance Num Word where
fromInt = primIntToWord
compare = primCompareWord
negate = primNegateWord
instance Num Float where
fromInt = primIntToFloat
compare = primCompareFloat
negate = primNegateFloat
instance Num Nat where
fromInt = primIntToNat --if isEQ (primCompareInt n zero') then Zero else Succ (fromInt (primSubInt n one'))
compare = undefined
negate = undefined
class Eq a where
(==) :: a -> a -> Bool -- todo: use (==) sign
infix 4 ==
instance Eq String where a == b = isEQ (primCompareString a b)
instance Eq Char where a == b = isEQ (primCompareChar a b)
instance Eq Int where a == b = isEQ (primCompareInt a b)
instance Eq Float where a == b = isEQ (primCompareFloat a b)
instance Eq Bool where
True == True = True
False == False = True
_ == _ = False
instance Eq Nat where
Zero == Zero = True
Succ a == Succ b = a == b
_ == _ = False
data List a = Nil | Cons a (List a)
infixr 5 :
|
