blob: d8a08a332f72376d8fec8f269f76c52c7524a121 (
plain)
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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
|
{-# LANGUAGE NoImplicitPrelude #-}
-- declarations of builtin functions and data types used by the compiler
module Internals where
-- used for type annotations
typeAnn x = x
-- used for recognising double parenthesis
parens x = x
undefined :: forall (a :: Type) . a
primFix :: forall (a :: Type) . (a -> a) -> a
data Unit = TT
data String
data Empty (a :: String)
unsafeCoerce :: forall a b . a -> b
data Constraint where
CUnit :: Constraint
CEmpty :: String -> Constraint
type family CW (c :: Constraint) -- where
{-
CW 'CUnit = Unit
CW ('CEmpty s) = Empty s
-}
-- equality constraints
type family EqCT (t :: Type) (a :: t) (b :: t) :: Constraint
{-
coe :: forall (a :: Type) (b :: Type) -> EqCT Type a b -> a -> b
coe a b TT x = unsafeCoerce @a @b x
-}
-- ... TODO
-- builtin used for overlapping instances
parEval :: forall a -> a -> a -> a
-- conjuction of constraints
type family T2 (x :: Constraint) (y :: Constraint) :: Constraint
{-
type instance T2 'CUnit c = c
type instance T2 c 'CUnit = c
type instance T2 ('CEmpty s) ('CEmpty s') = 'CEmpty (s {- ++ s' TODO-})
-}
match'Type :: forall (m :: Type -> Type) -> m Type -> forall (t :: Type) -> m t -> m t
type EqCTt = EqCT _
-- 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 | (:) a (List a)
infixr 5 :
data HList :: [Type] -> Type where
HNil :: HList '[]
HCons :: x -> HList xs -> HList '(x: xs)
hlistNilCase :: forall c -> c -> HList Nil -> c
hlistConsCase
:: forall (e :: Type) (f :: List Type)
. forall c
-> (e -> HList f -> c)
-> HList (e: f)
-> c
{-
-}
|
