git.iko.soy/Idris-dev
on 96db606 help sign in
Idris-dev/src/Idris/Primitives.hs
287 lines 11 kB history raw
1{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
3module Idris.Primitives(elabPrims) where
5import Idris.ElabDecls
6import Idris.ElabTerm
7import Idris.AbsSyntax
9import IRTS.Lang
11import Core.TT
12import Core.Evaluate
14data Prim = Prim { p_name :: Name,
15 p_type :: Type,
16 p_arity :: Int,
17 p_def :: [Value] -> Maybe Value,
18 p_lexp :: (Int, PrimFn),
19 p_total :: Totality
20 }
22ty [] x = Constant x
23ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
25believeTy = Bind (UN "a") (Pi (Set (UVar (-2))))
26 (Bind (UN "b") (Pi (Set (UVar (-2))))
27 (Bind (UN "x") (Pi (V 1)) (V 1)))
29total = Total []
30partial = Partial NotCovering
32primitives =
33 -- operators
34 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
35 (2, LPlus) total,
36 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
37 (2, LMinus) total,
38 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
39 (2, LTimes) total,
40 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
41 (2, LDiv) partial,
42 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
43 (2, LEq) total,
44 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
45 (2, LLt) total,
46 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
47 (2, LLe) total,
48 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
49 (2, LGt) total,
50 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
51 (2, LGe) total,
52 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
53 (2, LEq) total,
54 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
55 (2, LLt) total,
56 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
57 (2, LLe) total,
58 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
59 (2, LGt) total,
60 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
61 (2, LGe) total,
62 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
64 (2, LBPlus) total,
65 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
66 (2, LBMinus) total,
67 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
68 (2, LBTimes) total,
69 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
70 (2, LBDiv) partial,
71 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
72 (2, LBEq) total,
73 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
74 (2, LBLt) total,
75 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
76 (2, LBLe) total,
77 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
78 (2, LBGt) total,
79 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
80 (2, LBGe) total,
81 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
82 (2, LFPlus) total,
83 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
84 (2, LFMinus) total,
85 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
86 (2, LFTimes) total,
87 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
88 (2, LFDiv) total,
89 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
90 (2, LFEq) total,
91 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
92 (2, LFLt) total,
93 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
94 (2, LFLe) total,
95 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
96 (2, LFGt) total,
97 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
98 (2, LFGe) total,
99 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
100 (2, LStrConcat) total,
101 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
102 (2, LStrEq) total,
103 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
104 (2, LStrLt) total,
105 -- Conversions
106 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
107 (1, LStrInt) total,
108 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
109 (1, LIntStr) total,
110 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
111 (1, LNoOp) total,
112 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
113 (1, LNoOp) total,
114 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
115 (1, LIntBig) total,
116 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)
117 (1, LBigInt) total,
118 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
119 (1, LStrBig) total,
120 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
121 (1, LBigStr) total,
122 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
123 (1, LStrFloat) total,
124 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
125 (1, LFloatStr) total,
126 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
127 (1, LIntFloat) total,
128 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
129 (1, LFloatInt) total,
131 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
132 (1, LFExp) total,
133 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
134 (1, LFLog) total,
135 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
136 (1, LFSin) total,
137 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
138 (1, LFCos) total,
139 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
140 (1, LFTan) total,
141 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
142 (1, LFASin) total,
143 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
144 (1, LFACos) total,
145 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
146 (1, LFATan) total,
147 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
148 (1, LFSqrt) total,
149 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
150 (1, LFFloor) total,
151 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
152 (1, LFCeil) total,
154 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
155 (1, LStrHead) partial,
156 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
157 (1, LStrTail) partial,
158 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
159 (2, LStrCons) total,
160 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
161 (2, LStrIndex) partial,
162 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
163 (1, LStrRev) total,
164 Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
165 (1, LReadStr) partial,
166 Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)
167 (0, LVMPtr) total,
168 -- Streams
169 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
170 (0, LStdIn) partial,
171 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
172 (3, LNoOp) total -- ahem
173 ]
175p_believeMe [_,_,x] = Just x
176p_believeMe _ = Nothing
178iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
179iBin _ _ = Nothing
181bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
182bBin _ _ = Nothing
184bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
185bBini _ _ = Nothing
187biBin op = iBin (\x y -> if (op x y) then 1 else 0)
188bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
190fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
191fBin _ _ = Nothing
193bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
194 Just $ VConstant (I i)
195bfBin _ _ = Nothing
197bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
198 Just $ VConstant (I i)
199bcBin _ _ = Nothing
201bsBin op [VConstant (Str x), VConstant (Str y)]
202 = let i = (if op x y then 1 else 0) in
203 Just $ VConstant (I i)
204bsBin _ _ = Nothing
206sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
207sBin _ _ = Nothing
209c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
210c_intToStr _ = Nothing
211c_strToInt [VConstant (Str x)] = case reads x of
212 [(n,"")] -> Just $ VConstant (I n)
213 _ -> Just $ VConstant (I 0)
214c_strToInt _ = Nothing
216c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
217c_intToChar _ = Nothing
218c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
219c_charToInt _ = Nothing
221c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
222c_intToBigInt _ = Nothing
223c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))
224c_bigIntToInt _ = Nothing
226c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
227c_bigIntToStr _ = Nothing
228c_strToBigInt [VConstant (Str x)] = case reads x of
229 [(n,"")] -> Just $ VConstant (BI n)
230 _ -> Just $ VConstant (BI 0)
231c_strToBigInt _ = Nothing
233c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
234c_floatToStr _ = Nothing
235c_strToFloat [VConstant (Str x)] = case reads x of
236 [(n,"")] -> Just $ VConstant (Fl n)
237 _ -> Just $ VConstant (Fl 0)
238c_strToFloat _ = Nothing
240c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
241c_floatToInt _ = Nothing
243c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))
244c_intToFloat _ = Nothing
246p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
247p_fPrim f _ = Nothing
249p_floatExp = p_fPrim exp
250p_floatLog = p_fPrim log
251p_floatSin = p_fPrim sin
252p_floatCos = p_fPrim cos
253p_floatTan = p_fPrim tan
254p_floatASin = p_fPrim asin
255p_floatACos = p_fPrim acos
256p_floatATan = p_fPrim atan
257p_floatSqrt = p_fPrim sqrt
258p_floatFloor = p_fPrim (fromInteger . floor)
259p_floatCeil = p_fPrim (fromInteger . ceiling)
261p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
262p_strHead _ = Nothing
263p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
264p_strTail _ = Nothing
265p_strIndex [VConstant (Str xs), VConstant (I i)]
266 | i < length xs = Just $ VConstant (Ch (xs!!i))
267p_strIndex _ = Nothing
268p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
269p_strCons _ = Nothing
270p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
271p_strRev _ = Nothing
273p_cantreduce _ = Nothing
275elabPrim :: Prim -> Idris ()
276elabPrim (Prim n ty i def sc tot)
277 = do updateContext (addOperator n ty i def)
278 setTotality n tot
279 i <- getIState
280 putIState i { idris_scprims = (n, sc) : idris_scprims i }
282elabPrims :: Idris ()
283elabPrims = do mapM_ (elabDecl EAll toplevel)
284 (map (PData "" defaultSyntax (FC "builtin" 0) False)
285 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
286 mapM_ elabPrim primitives