git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/Idris/Primitives.hs
291 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__modInt") (ty [IType, IType] IType) 2 (iBin (mod))
43 (2, LMod) partial,
44 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
45 (2, LEq) total,
46 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
47 (2, LLt) total,
48 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
49 (2, LLe) total,
50 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
51 (2, LGt) total,
52 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
53 (2, LGe) total,
54 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
55 (2, LEq) total,
56 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
57 (2, LLt) total,
58 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
59 (2, LLe) total,
60 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
61 (2, LGt) total,
62 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
63 (2, LGe) total,
64 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
66 (2, LBPlus) total,
67 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
68 (2, LBMinus) total,
69 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
70 (2, LBTimes) total,
71 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
72 (2, LBDiv) partial,
73 Prim (UN "prim__modBigInt") (ty [BIType, BIType] BIType) 2 (bBin (mod))
74 (2, LBMod) partial,
75 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
76 (2, LBEq) total,
77 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
78 (2, LBLt) total,
79 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
80 (2, LBLe) total,
81 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
82 (2, LBGt) total,
83 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
84 (2, LBGe) total,
85 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
86 (2, LFPlus) total,
87 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
88 (2, LFMinus) total,
89 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
90 (2, LFTimes) total,
91 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
92 (2, LFDiv) total,
93 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
94 (2, LFEq) total,
95 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
96 (2, LFLt) total,
97 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
98 (2, LFLe) total,
99 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
100 (2, LFGt) total,
101 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
102 (2, LFGe) total,
103 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
104 (2, LStrConcat) total,
105 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
106 (2, LStrEq) total,
107 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
108 (2, LStrLt) total,
109 -- Conversions
110 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
111 (1, LStrInt) total,
112 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
113 (1, LIntStr) total,
114 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
115 (1, LNoOp) total,
116 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
117 (1, LNoOp) total,
118 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
119 (1, LIntBig) total,
120 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)
121 (1, LBigInt) total,
122 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
123 (1, LStrBig) total,
124 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
125 (1, LBigStr) total,
126 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
127 (1, LStrFloat) total,
128 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
129 (1, LFloatStr) total,
130 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
131 (1, LIntFloat) total,
132 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
133 (1, LFloatInt) total,
135 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
136 (1, LFExp) total,
137 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
138 (1, LFLog) total,
139 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
140 (1, LFSin) total,
141 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
142 (1, LFCos) total,
143 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
144 (1, LFTan) total,
145 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
146 (1, LFASin) total,
147 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
148 (1, LFACos) total,
149 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
150 (1, LFATan) total,
151 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
152 (1, LFSqrt) total,
153 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
154 (1, LFFloor) total,
155 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
156 (1, LFCeil) total,
158 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
159 (1, LStrHead) partial,
160 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
161 (1, LStrTail) partial,
162 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
163 (2, LStrCons) total,
164 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
165 (2, LStrIndex) partial,
166 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
167 (1, LStrRev) total,
168 Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
169 (1, LReadStr) partial,
170 Prim (UN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)
171 (0, LVMPtr) total,
172 -- Streams
173 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
174 (0, LStdIn) partial,
175 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
176 (3, LNoOp) partial -- ahem
177 ]
179p_believeMe [_,_,x] = Just x
180p_believeMe _ = Nothing
182iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
183iBin _ _ = Nothing
185bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
186bBin _ _ = Nothing
188bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
189bBini _ _ = Nothing
191biBin op = iBin (\x y -> if (op x y) then 1 else 0)
192bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
194fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
195fBin _ _ = Nothing
197bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
198 Just $ VConstant (I i)
199bfBin _ _ = Nothing
201bcBin op [VConstant (Ch x), VConstant (Ch y)] = let i = (if op x y then 1 else 0) in
202 Just $ VConstant (I i)
203bcBin _ _ = Nothing
205bsBin op [VConstant (Str x), VConstant (Str y)]
206 = let i = (if op x y then 1 else 0) in
207 Just $ VConstant (I i)
208bsBin _ _ = Nothing
210sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
211sBin _ _ = Nothing
213c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
214c_intToStr _ = Nothing
215c_strToInt [VConstant (Str x)] = case reads x of
216 [(n,"")] -> Just $ VConstant (I n)
217 _ -> Just $ VConstant (I 0)
218c_strToInt _ = Nothing
220c_intToChar [VConstant (I x)] = Just $ VConstant (Ch (toEnum x))
221c_intToChar _ = Nothing
222c_charToInt [VConstant (Ch x)] = Just $ VConstant (I (fromEnum x))
223c_charToInt _ = Nothing
225c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
226c_intToBigInt _ = Nothing
227c_bigIntToInt [VConstant (BI x)] = Just $ VConstant (I (fromInteger x))
228c_bigIntToInt _ = Nothing
230c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
231c_bigIntToStr _ = Nothing
232c_strToBigInt [VConstant (Str x)] = case reads x of
233 [(n,"")] -> Just $ VConstant (BI n)
234 _ -> Just $ VConstant (BI 0)
235c_strToBigInt _ = Nothing
237c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
238c_floatToStr _ = Nothing
239c_strToFloat [VConstant (Str x)] = case reads x of
240 [(n,"")] -> Just $ VConstant (Fl n)
241 _ -> Just $ VConstant (Fl 0)
242c_strToFloat _ = Nothing
244c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
245c_floatToInt _ = Nothing
247c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))
248c_intToFloat _ = Nothing
250p_fPrim f [VConstant (Fl x)] = Just $ VConstant (Fl (f x))
251p_fPrim f _ = Nothing
253p_floatExp = p_fPrim exp
254p_floatLog = p_fPrim log
255p_floatSin = p_fPrim sin
256p_floatCos = p_fPrim cos
257p_floatTan = p_fPrim tan
258p_floatASin = p_fPrim asin
259p_floatACos = p_fPrim acos
260p_floatATan = p_fPrim atan
261p_floatSqrt = p_fPrim sqrt
262p_floatFloor = p_fPrim (fromInteger . floor)
263p_floatCeil = p_fPrim (fromInteger . ceiling)
265p_strHead [VConstant (Str (x:xs))] = Just $ VConstant (Ch x)
266p_strHead _ = Nothing
267p_strTail [VConstant (Str (x:xs))] = Just $ VConstant (Str xs)
268p_strTail _ = Nothing
269p_strIndex [VConstant (Str xs), VConstant (I i)]
270 | i < length xs = Just $ VConstant (Ch (xs!!i))
271p_strIndex _ = Nothing
272p_strCons [VConstant (Ch x), VConstant (Str xs)] = Just $ VConstant (Str (x:xs))
273p_strCons _ = Nothing
274p_strRev [VConstant (Str xs)] = Just $ VConstant (Str (reverse xs))
275p_strRev _ = Nothing
277p_cantreduce _ = Nothing
279elabPrim :: Prim -> Idris ()
280elabPrim (Prim n ty i def sc tot)
281 = do updateContext (addOperator n ty i def)
282 setTotality n tot
283 i <- getIState
284 putIState i { idris_scprims = (n, sc) : idris_scprims i }
286elabPrims :: Idris ()
287elabPrims = do mapM_ (elabDecl EAll toplevel)
288 (map (PData "" defaultSyntax (FC "builtin" 0) False)
289 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
290 mapM_ elabPrim primitives