@@ -11,14 +11,10 @@ import IRTS.Lang
1111import Core.TT
1212import Core.Evaluate
1313
14−import Epic.Epic hiding (Term, Type, Name, fn)
15−import qualified Epic.Epic as E
16−
1714data Prim = Prim { p_name :: Name,
1815 p_type :: Type,
1916 p_arity :: Int,
2017 p_def :: [Value] -> Maybe Value,
21− p_epic :: ([E.Name], E.Term),
2218 p_lexp :: (Int, PrimFn),
2319 p_total :: Totality
2420 }
@@ -30,208 +26,147 @@ believeTy = Bind (UN "a") (Pi (Set (UVar (-2))))
3026 (Bind (UN "b") (Pi (Set (UVar (-2))))
3127 (Bind (UN "x") (Pi (V 1)) (V 1)))
3228
33−type ETm = E.Term
34−type EOp = E.Op
35−
36−fun = E.fn
37−ref = E.ref
38−
39−eOp :: EOp -> ([E.Name], ETm)
40−eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))
41−
42−eOpFn :: E.Type -> E.Type -> String -> ([E.Name], ETm)
43−eOpFn ty rty op = ([E.name "x", E.name "y"],
44− foreign_ rty op [(E.fn "x", ty), (E.fn "y", ty)])
45−
46−strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]
47−intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]
48−charToInt x = x
49−intToChar x = x
50−intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]
51−bigIntToInt x = foreign_ tyInt "bigIntToInt" [(x, tyBigInt)]
52−strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]
53−bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]
54−strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]
55−floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]
56−intToFloat x = foreign_ tyFloat "intToFloat" [(x, tyInt)]
57−floatToInt x = foreign_ tyInt "floatToInt" [(x, tyFloat)]
58−
59−floatExp x = foreign_ tyFloat "exp" [(x, tyFloat)]
60−floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]
61−floatSin x = foreign_ tyFloat "sin" [(x, tyFloat)]
62−floatCos x = foreign_ tyFloat "cos" [(x, tyFloat)]
63−floatTan x = foreign_ tyFloat "tan" [(x, tyFloat)]
64−floatASin x = foreign_ tyFloat "asin" [(x, tyFloat)]
65−floatACos x = foreign_ tyFloat "acos" [(x, tyFloat)]
66−floatATan x = foreign_ tyFloat "atan" [(x, tyFloat)]
67−floatFloor x = foreign_ tyFloat "floor" [(x, tyFloat)]
68−floatCeil x = foreign_ tyFloat "ceil" [(x, tyFloat)]
69−floatSqrt x = foreign_ tyFloat "sqrt" [(x, tyFloat)]
70−
71−strIndex x i = foreign_ tyChar "strIndex" [(x, tyString), (i, tyInt)]
72−strHead x = foreign_ tyChar "strHead" [(x, tyString)]
73−strTail x = foreign_ tyString "strTail" [(x, tyString)]
74−strCons x xs = foreign_ tyString "strCons" [(x, tyChar), (xs, tyString)]
75−strRev x = foreign_ tyString "strrev" [(x, tyString)]
76−strEq x y = foreign_ tyInt "streq" [(x, tyString), (y, tyString)]
77−strLt x y = foreign_ tyInt "strlt" [(x, tyString), (y, tyString)]
78−
79−readStr x = foreign_ tyString "freadStr" [(x, tyPtr)]
80−
81−stream_stdin = let args :: [(ETm, E.Type)] = [] in
82− foreign_ tyPtr "get_stdin" args
83−
8429total = Total []
8530partial = Partial NotCovering
8631
8732primitives =
8833 -- operators
8934 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
90− (eOp E.plus_) (2, LPlus) total,
35+ (2, LPlus) total,
9136 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
92− (eOp E.minus_)
93− (2, LMinus) total,
37+ (2, LMinus) total,
9438 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
95− (eOp E.times_) (2, LTimes) total,
39+ (2, LTimes) total,
9640 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
97− (eOp E.divide_) (2, LDiv) partial,
41+ (2, LDiv) partial,
9842 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
99− (eOp E.eq_) (2, LEq) total,
43+ (2, LEq) total,
10044 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
101− (eOp E.lt_) (2, LLt) total,
45+ (2, LLt) total,
10246 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
103− (eOp E.lte_) (2, LLe) total,
47+ (2, LLe) total,
10448 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
105− (eOp E.gt_) (2, LGt) total,
49+ (2, LGt) total,
10650 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
107− (eOp E.gte_) (2, LGe) total,
51+ (2, LGe) total,
10852 Prim (UN "prim__eqChar") (ty [ChType, ChType] IType) 2 (bcBin (==))
109− (eOp E.eq_) (2, LEq) total,
53+ (2, LEq) total,
11054 Prim (UN "prim__ltChar") (ty [ChType, ChType] IType) 2 (bcBin (<))
111− (eOp E.lt_) (2, LLt) total,
55+ (2, LLt) total,
11256 Prim (UN "prim__lteChar") (ty [ChType, ChType] IType) 2 (bcBin (<=))
113− (eOp E.lte_) (2, LLe) total,
57+ (2, LLe) total,
11458 Prim (UN "prim__gtChar") (ty [ChType, ChType] IType) 2 (bcBin (>))
115− (eOp E.gt_) (2, LGt) total,
59+ (2, LGt) total,
11660 Prim (UN "prim__gteChar") (ty [ChType, ChType] IType) 2 (bcBin (>=))
117− (eOp E.gte_) (2, LGe) total,
61+ (2, LGe) total,
11862 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
119− (eOpFn tyBigInt tyBigInt "addBig")
63+
12064 (2, LBPlus) total,
12165 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
122− (eOpFn tyBigInt tyBigInt "subBig") (2, LBMinus) total,
66+ (2, LBMinus) total,
12367 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
124− (eOpFn tyBigInt tyBigInt "mulBig") (2, LBTimes) total,
68+ (2, LBTimes) total,
12569 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
126− (eOpFn tyBigInt tyBigInt "divBig") (2, LBDiv) partial,
70+ (2, LBDiv) partial,
12771 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
128− (eOpFn tyBigInt tyInt "eqBig") (2, LBEq) total,
72+ (2, LBEq) total,
12973 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
130− (eOpFn tyBigInt tyInt "ltBig") (2, LBLt) total,
74+ (2, LBLt) total,
13175 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
132− (eOpFn tyBigInt tyInt "leBig") (2, LBLe) total,
76+ (2, LBLe) total,
13377 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
134− (eOpFn tyBigInt tyInt "gtBig") (2, LBGt) total,
78+ (2, LBGt) total,
13579 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
136− (eOpFn tyBigInt tyInt "geBig") (2, LBGe) total,
80+ (2, LBGe) total,
13781 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
138− (eOp E.plusF_) (2, LFPlus) total,
82+ (2, LFPlus) total,
13983 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
140− (eOp E.minusF_) (2, LFMinus) total,
84+ (2, LFMinus) total,
14185 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
142− (eOp E.timesF_) (2, LFTimes) total,
86+ (2, LFTimes) total,
14387 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
144− (eOp E.divideF_) (2, LFDiv) total,
88+ (2, LFDiv) total,
14589 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
146− (eOp E.eqF_) (2, LFEq) total,
90+ (2, LFEq) total,
14791 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
148− (eOp E.ltF_) (2, LFLt) total,
92+ (2, LFLt) total,
14993 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
150− (eOp E.lteF_) (2, LFLe) total,
94+ (2, LFLe) total,
15195 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
152− (eOp E.gtF_) (2, LFGt) total,
96+ (2, LFGt) total,
15397 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
154− (eOp E.gteF_) (2, LFGe) total,
98+ (2, LFGe) total,
15599 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
156− ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y")
157100 (2, LStrConcat) total,
158101 Prim (UN "prim__eqString") (ty [StrType, StrType] IType) 2 (bsBin (==))
159− ([E.name "x", E.name "y"], strEq (fun "x") (fun "y"))
160102 (2, LStrEq) total,
161103 Prim (UN "prim__ltString") (ty [StrType, StrType] IType) 2 (bsBin (<))
162− ([E.name "x", E.name "y"], strLt (fun "x") (fun "y"))
163104 (2, LStrLt) total,
164105 -- Conversions
165106 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
166− ([E.name "x"], strToInt (fun "x")) (1, LStrInt) total,
107+ (1, LStrInt) total,
167108 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
168− ([E.name "x"], intToStr (fun "x")) (1, LIntStr) total,
109+ (1, LIntStr) total,
169110 Prim (UN "prim__charToInt") (ty [ChType] IType) 1 (c_charToInt)
170− ([E.name "x"], charToInt (fun "x")) (1, LNoOp) total,
111+ (1, LNoOp) total,
171112 Prim (UN "prim__intToChar") (ty [IType] ChType) 1 (c_intToChar)
172− ([E.name "x"], intToChar (fun "x")) (1, LNoOp) total,
113+ (1, LNoOp) total,
173114 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
174− ([E.name "x"], intToBigInt (fun "x")) (1, LIntBig) total,
115+ (1, LIntBig) total,
175116 Prim (UN "prim__bigIntToInt") (ty [BIType] IType) 1 (c_bigIntToInt)
176− ([E.name "x"], bigIntToInt (fun "x")) (1, LBigInt) total,
117+ (1, LBigInt) total,
177118 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
178− ([E.name "x"], strToBigInt (fun "x")) (1, LStrBig) total,
119+ (1, LStrBig) total,
179120 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
180− ([E.name "x"], bigIntToStr (fun "x")) (1, LBigStr) total,
121+ (1, LBigStr) total,
181122 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
182− ([E.name "x"], strToFloat (fun "x")) (1, LStrFloat) total,
123+ (1, LStrFloat) total,
183124 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
184− ([E.name "x"], floatToStr (fun "x")) (1, LFloatStr) total,
125+ (1, LFloatStr) total,
185126 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
186− ([E.name "x"], intToFloat (fun "x")) (1, LIntFloat) total,
127+ (1, LIntFloat) total,
187128 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
188− ([E.name "x"], floatToInt (fun "x")) (1, LFloatInt) total,
129+ (1, LFloatInt) total,
189130
190131 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
191− ([E.name "x"], floatExp (fun "x")) (1, LFExp) total,
132+ (1, LFExp) total,
192133 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
193− ([E.name "x"], floatLog (fun "x")) (1, LFLog) total,
134+ (1, LFLog) total,
194135 Prim (UN "prim__floatSin") (ty [FlType] FlType) 1 (p_floatSin)
195− ([E.name "x"], floatSin (fun "x")) (1, LFSin) total,
136+ (1, LFSin) total,
196137 Prim (UN "prim__floatCos") (ty [FlType] FlType) 1 (p_floatCos)
197− ([E.name "x"], floatCos (fun "x")) (1, LFCos) total,
138+ (1, LFCos) total,
198139 Prim (UN "prim__floatTan") (ty [FlType] FlType) 1 (p_floatTan)
199− ([E.name "x"], floatTan (fun "x")) (1, LFTan) total,
140+ (1, LFTan) total,
200141 Prim (UN "prim__floatASin") (ty [FlType] FlType) 1 (p_floatASin)
201− ([E.name "x"], floatASin (fun "x")) (1, LFASin) total,
142+ (1, LFASin) total,
202143 Prim (UN "prim__floatACos") (ty [FlType] FlType) 1 (p_floatACos)
203− ([E.name "x"], floatACos (fun "x")) (1, LFACos) total,
144+ (1, LFACos) total,
204145 Prim (UN "prim__floatATan") (ty [FlType] FlType) 1 (p_floatATan)
205− ([E.name "x"], floatATan (fun "x")) (1, LFATan) total,
146+ (1, LFATan) total,
206147 Prim (UN "prim__floatSqrt") (ty [FlType] FlType) 1 (p_floatSqrt)
207− ([E.name "x"], floatSqrt (fun "x")) (1, LFSqrt) total,
148+ (1, LFSqrt) total,
208149 Prim (UN "prim__floatFloor") (ty [FlType] FlType) 1 (p_floatFloor)
209− ([E.name "x"], floatFloor (fun "x")) (1, LFFloor) total,
150+ (1, LFFloor) total,
210151 Prim (UN "prim__floatCeil") (ty [FlType] FlType) 1 (p_floatCeil)
211− ([E.name "x"], floatCeil (fun "x")) (1, LFCeil) total,
152+ (1, LFCeil) total,
212153
213154 Prim (UN "prim__strHead") (ty [StrType] ChType) 1 (p_strHead)
214− ([E.name "x"], strHead (fun "x")) (1, LStrHead) partial,
155+ (1, LStrHead) partial,
215156 Prim (UN "prim__strTail") (ty [StrType] StrType) 1 (p_strTail)
216− ([E.name "x"], strTail (fun "x")) (1, LStrTail) partial,
157+ (1, LStrTail) partial,
217158 Prim (UN "prim__strCons") (ty [ChType, StrType] StrType) 2 (p_strCons)
218− ([E.name "x", E.name "xs"], strCons (fun "x") (fun "xs"))
219159 (2, LStrCons) total,
220160 Prim (UN "prim__strIndex") (ty [StrType, IType] ChType) 2 (p_strIndex)
221− ([E.name "x", E.name "i"], strIndex (fun "x") (fun "i"))
222161 (2, LStrIndex) partial,
223162 Prim (UN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)
224− ([E.name "x"], strRev (fun "x"))
225163 (1, LStrRev) total,
226164 Prim (UN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)
227− ([E.name "h"], readStr (fun "h")) (1, LReadStr) partial,
228−
165+ (1, LReadStr) partial,
229166 -- Streams
230167 Prim (UN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)
231− ([], stream_stdin) (0, LStdIn) partial,
232−
168+ (0, LStdIn) partial,
233169 Prim (UN "prim__believe_me") believeTy 3 (p_believeMe)
234− ([E.name "a", E.name "b", E.name "x"], fun "x")
235170 (1, LNoOp) total -- ahem
236171 ]
237172
@@ -336,12 +271,11 @@ p_strRev _ = Nothing
336271p_cantreduce _ = Nothing
337272
338273elabPrim :: Prim -> Idris ()
339−elabPrim (Prim n ty i def epic sc tot)
274+elabPrim (Prim n ty i def sc tot)
340275 = do updateContext (addOperator n ty i def)
341276 setTotality n tot
342277 i <- getIState
343− putIState i { idris_prims = (n, epic) : idris_prims i,
344− idris_scprims = (n, sc) : idris_scprims i }
278+ putIState i { idris_scprims = (n, sc) : idris_scprims i }
345279
346280elabPrims :: Idris ()
347281elabPrims = do mapM_ (elabDecl toplevel)