git.iko.soy/Idris-dev
on bbaa193 help sign in
Idris-dev/src/Idris/Primitives.hs
195 lines 7.8 kB history raw
1{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
3module Idris.Primitives(elabPrims) where
5import Idris.ElabDecls
6import Idris.AbsSyntax
8import Core.TT
9import Core.Evaluate
11import Epic.Epic hiding (Term, Type, Name, fn)
12import qualified Epic.Epic as E
14data Prim = Prim { p_name :: Name,
15 p_type :: Type,
16 p_arity :: Int,
17 p_def :: [Value] -> Maybe Value,
18 p_epic :: ([E.Name], E.Term)
19 }
21ty [] x = Constant x
22ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
24type ETm = E.Term
25type EOp = E.Op
27fun = E.fn
28ref = E.ref
30eOp :: EOp -> ([E.Name], ETm)
31eOp op = ([E.name "x", E.name "y"], E.op_ op (E.fn "x") (E.fn "y"))
33eOpFn :: E.Type -> E.Type -> String -> ([E.Name], ETm)
34eOpFn ty rty op = ([E.name "x", E.name "y"],
35 foreign_ rty op [(E.fn "x", ty), (E.fn "y", ty)])
37strToInt x = foreign_ tyInt "strToInt" [(x, tyString)]
38intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]
39intToBigInt x = foreign_ tyBigInt "intToBigInt" [(x, tyInt)]
40strToBigInt x = foreign_ tyBigInt "strToBig" [(x, tyString)]
41bigIntToStr x = foreign_ tyString "bigToStr" [(x, tyBigInt)]
42strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]
43floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]
44intToFloat x = foreign_ tyFloat "intToFloat" [(x, tyInt)]
45floatToInt x = foreign_ tyInt "floatToInt" [(x, tyFloat)]
47floatExp x = foreign_ tyFloat "exp" [(x, tyFloat)]
48floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]
50primitives =
51 -- operators
52 [Prim (UN "prim__addInt") (ty [IType, IType] IType) 2 (iBin (+))
53 (eOp E.plus_),
54 Prim (UN "prim__subInt") (ty [IType, IType] IType) 2 (iBin (-))
55 (eOp E.minus_),
56 Prim (UN "prim__mulInt") (ty [IType, IType] IType) 2 (iBin (*))
57 (eOp E.times_),
58 Prim (UN "prim__divInt") (ty [IType, IType] IType) 2 (iBin (div))
59 (eOp E.divide_),
60 Prim (UN "prim__eqInt") (ty [IType, IType] IType) 2 (biBin (==))
61 (eOp E.eq_),
62 Prim (UN "prim__ltInt") (ty [IType, IType] IType) 2 (biBin (<))
63 (eOp E.lt_),
64 Prim (UN "prim__lteInt") (ty [IType, IType] IType) 2 (biBin (<=))
65 (eOp E.lte_),
66 Prim (UN "prim__gtInt") (ty [IType, IType] IType) 2 (biBin (>))
67 (eOp E.gt_),
68 Prim (UN "prim__gteInt") (ty [IType, IType] IType) 2 (biBin (>=))
69 (eOp E.gte_),
70 Prim (UN "prim__addBigInt") (ty [BIType, BIType] BIType) 2 (bBin (+))
71 (eOpFn tyBigInt tyBigInt "addBig"),
72 Prim (UN "prim__subBigInt") (ty [BIType, BIType] BIType) 2 (bBin (-))
73 (eOpFn tyBigInt tyBigInt "subBig"),
74 Prim (UN "prim__mulBigInt") (ty [BIType, BIType] BIType) 2 (bBin (*))
75 (eOpFn tyBigInt tyBigInt "mulBig"),
76 Prim (UN "prim__divBigInt") (ty [BIType, BIType] BIType) 2 (bBin (div))
77 (eOpFn tyBigInt tyBigInt "divBig"),
78 Prim (UN "prim__eqBigInt") (ty [BIType, BIType] IType) 2 (bbBin (==))
79 (eOpFn tyBigInt tyInt "eqBig"),
80 Prim (UN "prim__ltBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<))
81 (eOpFn tyBigInt tyInt "ltBig"),
82 Prim (UN "prim__lteBigInt") (ty [BIType, BIType] IType) 2 (bbBin (<=))
83 (eOpFn tyBigInt tyInt "leBig"),
84 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>))
85 (eOpFn tyBigInt tyInt "gtBig"),
86 Prim (UN "prim__gtBigInt") (ty [BIType, BIType] IType) 2 (bbBin (>=))
87 (eOpFn tyBigInt tyInt "geBig"),
88 Prim (UN "prim__addFloat") (ty [FlType, FlType] FlType) 2 (fBin (+))
89 (eOp E.plusF_),
90 Prim (UN "prim__subFloat") (ty [FlType, FlType] FlType) 2 (fBin (-))
91 (eOp E.minusF_),
92 Prim (UN "prim__mulFloat") (ty [FlType, FlType] FlType) 2 (fBin (*))
93 (eOp E.timesF_),
94 Prim (UN "prim__divFloat") (ty [FlType, FlType] FlType) 2 (fBin (/))
95 (eOp E.divideF_),
96 Prim (UN "prim__eqFloat") (ty [FlType, FlType] IType) 2 (bfBin (==))
97 (eOp E.eqF_),
98 Prim (UN "prim__ltFloat") (ty [FlType, FlType] IType) 2 (bfBin (<))
99 (eOp E.ltF_),
100 Prim (UN "prim__lteFloat") (ty [FlType, FlType] IType) 2 (bfBin (<=))
101 (eOp E.lteF_),
102 Prim (UN "prim__gtFloat") (ty [FlType, FlType] IType) 2 (bfBin (>))
103 (eOp E.gtF_),
104 Prim (UN "prim__gteFloat") (ty [FlType, FlType] IType) 2 (bfBin (>=))
105 (eOp E.gteF_),
106 Prim (UN "prim__concat") (ty [StrType, StrType] StrType) 2 (sBin (++))
107 ([E.name "x", E.name "y"], (fun "append") @@ fun "x" @@ fun "y"),
108 -- Conversions
109 Prim (UN "prim__strToInt") (ty [StrType] IType) 1 (c_strToInt)
110 ([E.name "x"], strToInt (fun "x")),
111 Prim (UN "prim__intToStr") (ty [IType] StrType) 1 (c_intToStr)
112 ([E.name "x"], intToStr (fun "x")),
113 Prim (UN "prim__intToBigInt") (ty [IType] BIType) 1 (c_intToBigInt)
114 ([E.name "x"], intToBigInt (fun "x")),
115 Prim (UN "prim__strToBigInt") (ty [StrType] BIType) 1 (c_strToBigInt)
116 ([E.name "x"], strToBigInt (fun "x")),
117 Prim (UN "prim__bigIntToStr") (ty [BIType] StrType) 1 (c_bigIntToStr)
118 ([E.name "x"], bigIntToStr (fun "x")),
119 Prim (UN "prim__strToFloat") (ty [StrType] FlType) 1 (c_strToFloat)
120 ([E.name "x"], strToFloat (fun "x")),
121 Prim (UN "prim__floatToStr") (ty [FlType] StrType) 1 (c_floatToStr)
122 ([E.name "x"], floatToStr (fun "x")),
123 Prim (UN "prim__intToFloat") (ty [IType] FlType) 1 (c_intToFloat)
124 ([E.name "x"], intToFloat (fun "x")),
125 Prim (UN "prim__floatToInt") (ty [FlType] IType) 1 (c_floatToInt)
126 ([E.name "x"], floatToInt (fun "x")),
127 Prim (UN "prim__floatExp") (ty [FlType] FlType) 1 (p_floatExp)
128 ([E.name "x"], floatExp (fun "x")),
129 Prim (UN "prim__floatLog") (ty [FlType] FlType) 1 (p_floatLog)
130 ([E.name "x"], floatLog (fun "x"))
131 ]
133iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
134iBin _ _ = Nothing
136bBin op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (BI (op x y))
137bBin _ _ = Nothing
139bBini op [VConstant (BI x), VConstant (BI y)] = Just $ VConstant (I (op x y))
140bBini _ _ = Nothing
142biBin op = iBin (\x y -> if (op x y) then 1 else 0)
143bbBin op = bBini (\x y -> if (op x y) then 1 else 0)
145fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
146fBin _ _ = Nothing
148bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
149 Just $ VConstant (I i)
150bfBin _ _ = Nothing
152sBin op [VConstant (Str x), VConstant (Str y)] = Just $ VConstant (Str (op x y))
153sBin _ _ = Nothing
155c_intToStr [VConstant (I x)] = Just $ VConstant (Str (show x))
156c_intToStr _ = Nothing
157c_strToInt [VConstant (Str x)] = Just $ VConstant (I (read x))
158c_strToInt _ = Nothing
160c_intToBigInt [VConstant (I x)] = Just $ VConstant (BI (fromIntegral x))
161c_intToBigInt _ = Nothing
163c_bigIntToStr [VConstant (BI x)] = Just $ VConstant (Str (show x))
164c_bigIntToStr _ = Nothing
165c_strToBigInt [VConstant (Str x)] = Just $ VConstant (BI (read x))
166c_strToBigInt _ = Nothing
168c_floatToStr [VConstant (Fl x)] = Just $ VConstant (Str (show x))
169c_floatToStr _ = Nothing
170c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))
171c_strToFloat _ = Nothing
173c_floatToInt [VConstant (Fl x)] = Just $ VConstant (I (truncate x))
174c_floatToInt _ = Nothing
176c_intToFloat [VConstant (I x)] = Just $ VConstant (Fl (fromIntegral x))
177c_intToFloat _ = Nothing
179p_floatExp [VConstant (Fl x)] = Just $ VConstant (Fl (exp x))
180p_floatExp _ = Nothing
181p_floatLog [VConstant (Fl x)] = Just $ VConstant (Fl (log x))
182p_floatLog _ = Nothing
184elabPrim :: Prim -> Idris ()
185elabPrim (Prim n ty i def epic)
186 = do updateContext (addOperator n ty i def)
187 i <- getIState
188 putIState i { idris_prims = (n, epic) : idris_prims i }
190elabPrims :: Idris ()
191elabPrims = do mapM_ (elabDecl toplevel)
192 (map (PData defaultSyntax (FC "builtin" 0))
193 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
194 mapM_ elabPrim primitives