5afe678 · Idris-dev · git.iko.soy

lib/prelude.idr+9

compare with master

unifiedsplit

@@ -85,6 +85,15 @@ instance MonadPlus Maybe where {

85 mplus Nothing Nothing = Nothing;

86}

87

88+---- some mathematical operations

89+

90+%lib "m"

91+

92+exp : Float -> Float;

93+exp x = prim__floatExp x;

94+

95+log : Float -> Float;

96+log x = prim__floatLog x;

88

97

89---- some basic io

98---- some basic io

90

99

src/Idris/AbsSyntax.hs+1

@@ -221,6 +221,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

221 t -- full instance type

222 [PDecl' t]

223 | PSyntax FC Syntax

224+ | PDirective (Idris ())

224 deriving Functor

225 deriving Functor

225

226

226data PClause' t = PClause Name t [t] t [PDecl' t]

227data PClause' t = PClause Name t [t] t [PDecl' t]

src/Idris/Compiler.hs+1−1

@@ -20,7 +20,7 @@ compile f = do ds <- mkDecls

20 objs <- getObjectFiles

21 libs <- getLibs

22 lift $ compileObjWith [Debug] (mkProgram ds) (f ++ ".o")

23− lift $ link ((f ++ ".o") : objs) f

23+ lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

24

25mkDecls :: Idris [EpicDecl]

26mkDecls = do i <- getIState

src/Idris/ElabDecls.hs+1−1

@@ -458,7 +458,7 @@ elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show

458elabDecl' info (PInstance s f cs n ps t ds)

459 = do iLOG $ "Elaborating instance " ++ show n

460 elabInstance info s f cs n ps t ds

461−

461+elabDecl' info (PDirective i) = i

462

463-- elabDecl' info (PImport i) = loadModule i

464

src/Idris/Imports.hs+8

@@ -35,4 +35,12 @@ findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)

35 then return (IDR idrp)

36 else findImport ds fp

37

38+-- find a specific filename somewhere in a path

39+

40+findInPath :: [FilePath] -> FilePath -> IO FilePath

41+findInPath [] fp = fail $ "Can't find file " ++ fp

42+findInPath (d:ds) fp = do let p = d ++ "/" ++ fp

43+ e <- doesFileExist p

44+ if e then return p else findInPath ds p

45+

38

46

src/Idris/Parser.hs+9

@@ -167,6 +167,7 @@ pDecl syn

167 <|> pParams syn

168 <|> pClass syn

169 <|> pInstance syn

170+ <|> pDirective

170 <|> try (do reserved "import"

171 <|> try (do reserved "import"

171 fp <- identifier

172 fp <- identifier

172 lchar ';'

173 lchar ';'

@@ -673,6 +674,14 @@ pWhereblock n syn

673 lchar '}';

674 lchar '}';

674 return (concat ds, map (\x -> (x, decoration syn x)) dns)

675 return (concat ds, map (\x -> (x, decoration syn x)) dns)

675

676

677+pDirective :: IParser [PDecl]

678+pDirective = do lchar '%'; reserved "lib"; lib <- strlit;

679+ return [PDirective (addLib lib)]

680+ <|> do lchar '%'; reserved "link"; obj <- strlit;

681+ return [PDirective (do datadir <- lift $ getDataDir

682+ o <- lift $ findInPath [".", datadir] obj

683+ addObjectFile o)]

684+

676pTactic :: SyntaxInfo -> IParser PTactic

685pTactic :: SyntaxInfo -> IParser PTactic

677pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

686pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

678 return $ Intro ns

687 return $ Intro ns

src/Idris/Primitives.hs+13−1

@@ -35,6 +35,9 @@ intToStr x = foreign_ tyString "intToStr" [(x, tyInt)]

35strToFloat x = foreign_ tyFloat "strToFloat" [(x, tyString)]

36floatToStr x = foreign_ tyString "floatToStr" [(x, tyFloat)]

37

38+floatExp x = foreign_ tyFloat "exp" [(x, tyFloat)]

39+floatLog x = foreign_ tyFloat "log" [(x, tyFloat)]

40+

38primitives =

41primitives =

39 -- operators

42 -- operators

40 [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))

43 [Prim (UN ["prim__addInt"]) (ty [IType, IType] IType) 2 (iBin (+))

@@ -83,7 +86,11 @@ primitives =

83 Prim (UN ["prim__strToFloat"]) (ty [StrType] FlType) 1 (c_strToFloat)

86 Prim (UN ["prim__strToFloat"]) (ty [StrType] FlType) 1 (c_strToFloat)

84 ([E.name "x"], strToFloat (fun "x")),

87 ([E.name "x"], strToFloat (fun "x")),

85 Prim (UN ["prim__floatToStr"]) (ty [FlType] StrType) 1 (c_floatToStr)

88 Prim (UN ["prim__floatToStr"]) (ty [FlType] StrType) 1 (c_floatToStr)

86− ([E.name "x"], floatToStr (fun "x"))

89+ ([E.name "x"], floatToStr (fun "x")),

90+ Prim (UN ["prim__floatExp"]) (ty [FlType] FlType) 1 (p_floatExp)

91+ ([E.name "x"], floatExp (fun "x")),

92+ Prim (UN ["prim__floatLog"]) (ty [FlType] FlType) 1 (p_floatLog)

93+ ([E.name "x"], floatLog (fun "x"))

87 ]

94 ]

88

95

89iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

96iBin op [VConstant (I x), VConstant (I y)] = Just $ VConstant (I (op x y))

@@ -111,6 +118,11 @@ c_floatToStr _ = Nothing

111c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))

118c_strToFloat [VConstant (Str x)] = Just $ VConstant (Fl (read x))

112c_strToFloat _ = Nothing

119c_strToFloat _ = Nothing

113

120

121+p_floatExp [VConstant (Fl x)] = Just $ VConstant (Fl (exp x))

122+p_floatExp _ = Nothing

123+p_floatLog [VConstant (Fl x)] = Just $ VConstant (Fl (log x))

124+p_floatLog _ = Nothing

125+

114elabPrim :: Prim -> Idris ()

126elabPrim :: Prim -> Idris ()

115elabPrim (Prim n ty i def epic)

127elabPrim (Prim n ty i def epic)

116 = do updateContext (addOperator n ty i def)

128 = do updateContext (addOperator n ty i def)