git.iko.soy/Idris-dev
on 083fc70 help sign in
Idris-dev/src/Idris/Primitives.hs
57 lines 2.4 kB history raw
1module Idris.Primitives(elabPrims) where
3import Idris.ElabDecls
4import Idris.AbsSyntax
6import Core.TT
7import Core.Evaluate
9data Prim = Prim { p_name :: Name,
10 p_type :: Type,
11 p_arity :: Int,
12 p_def :: [Value] -> Maybe Value
13 }
15ty [] x = Constant x
16ty (t:ts) x = Bind (MN 0 "T") (Pi (Constant t)) (ty ts x)
18primitives =
19 [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+)),
20 Prim (UN ["prim__subInt"]) (ty [IType, IType] IType) 2 (iBin (-)),
21 Prim (UN ["prim__mulInt"]) (ty [IType, IType] IType) 2 (iBin (*)),
22 Prim (UN ["prim__divInt"]) (ty [IType, IType] IType) 2 (iBin (div)),
23 Prim (UN ["prim__eqInt"]) (ty [IType, IType] IType) 2 (biBin (==)),
24 Prim (UN ["prim__ltInt"]) (ty [IType, IType] IType) 2 (biBin (<)),
25 Prim (UN ["prim__lteInt"]) (ty [IType, IType] IType) 2 (biBin (<=)),
26 Prim (UN ["prim__gtInt"]) (ty [IType, IType] IType) 2 (biBin (>)),
27 Prim (UN ["prim__gteInt"]) (ty [IType, IType] IType) 2 (biBin (>=)),
28 Prim (UN ["prim__addFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (+)),
29 Prim (UN ["prim__subFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (-)),
30 Prim (UN ["prim__mulFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (*)),
31 Prim (UN ["prim__divFloat"]) (ty [FlType, FlType] FlType) 2 (fBin (/)),
32 Prim (UN ["prim__eqFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (==)),
33 Prim (UN ["prim__ltFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<)),
34 Prim (UN ["prim__lteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (<=)),
35 Prim (UN ["prim__gtFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>)),
36 Prim (UN ["prim__gteFloat"]) (ty [FlType, FlType] IType) 2 (bfBin (>=))
37 ]
39iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))
40iBin _ _ = Nothing
42biBin op = iBin (\x y -> if (op x y) then 1 else 0)
44fBin op [VConstant (Fl x), VConstant (Fl y)] = Just $ VConstant (Fl (op x y))
45fBin _ _ = Nothing
47bfBin op [VConstant (Fl x), VConstant (Fl y)] = let i = (if op x y then 1 else 0) in
48 Just $ VConstant (I i)
49bfBin _ _ = Nothing
51elabPrim :: Prim -> Idris ()
52elabPrim (Prim n ty i def) = updateContext (addOperator n ty i def)
54elabPrims :: Idris ()
55elabPrims = do elabDecl toplevel (PData inferDecl)
56 mapM_ elabPrim primitives