a4a77bf · Idris-dev · git.iko.soy

lib/io.idr+7

compare with master

unifiedsplit

@@ -8,6 +8,12 @@ io_bind (prim__IO v) k = k v;

8io_return : a -> IO a;

9io_return = prim__IO;

10

11+-- This may seem pointless, but we can use it to force an

12+-- evaluation of main that Epic wouldn't otherwise do...

13+

14+run__IO : IO () -> IO ();

15+run__IO (prim__IO v) = prim__IO v;

16+

12

18

13interpFTy : FTy -> Set;

19interpFTy : FTy -> Set;

@@ -37,3 +43,4 @@ data Foreign : Set -> Set where

37mkForeign : Foreign x -> x;

43mkForeign : Foreign x -> x;

38-- mkForeign compiled as primitive

44-- mkForeign compiled as primitive

39

45

46+

lib/nat.idr+5−2

@@ -18,8 +18,11 @@ mult : Nat -> Nat -> Nat;

18mult O y = O;

19mult (S k) y = plus y (mult k y);

20

21−instance numNat : Num Nat;

21+instance Num Nat where {

22−instance numNat = instanceNum plus sub mult;

22+ (+) = plus;

23+ (-) = sub;

24+ (*) = mult;

25+}

23

26

24instance Eq Nat where {

27instance Eq Nat where {

25 O == O = True;

28 O == O = True;

src/Idris/AbsSyntax.hs+1−1

@@ -344,7 +344,7 @@ data SSymbol = Keyword Name

344 | Expr Name

345 deriving Show

346

347−initDSL = DSL (UN ["io_bind"]) (UN ["io_return"])

347+initDSL = DSL (UN [">>="]) (UN ["return"])

348

349data SyntaxInfo = Syn { using :: [(Name, PTerm)],

350 syn_params :: [(Name, PTerm)],

src/Idris/Compiler.hs+4−2

@@ -27,7 +27,9 @@ mkDecls = do i <- getIState

27ename x = name ("idris_" ++ show x)

28aname x = name ("a_" ++ show x)

29

30+-- The 'unsafePerformIO' makes sure it gets evaluated fully

31+epicMain = effect_ $ ref (ename (UN ["run__IO"])) @@

30−epicMain = ref (ename (UN ["main"]))

32+ ref (ename (UN ["main"]))

31

33

32class ToEpic a where

34class ToEpic a where

33 epic :: a -> Idris E.Term

35 epic :: a -> Idris E.Term

@@ -37,6 +39,7 @@ build (n, d) = do i <- getIState

37 case lookup n (idris_prims i) of

39 case lookup n (idris_prims i) of

38 Just opDef -> return $ EpicFn (ename n) opDef

40 Just opDef -> return $ EpicFn (ename n) opDef

39 _ -> do def <- epic d

41 _ -> do def <- epic d

42+ logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def

40 return $ EpicFn (ename n) def

43 return $ EpicFn (ename n) def

41

44

42impossible = int 42424242

45impossible = int 42424242

@@ -68,7 +71,6 @@ instance ToEpic (TT Name) where

68 epic' env (Bind _ _ _) = return impossible

71 epic' env (Bind _ _ _) = return impossible

69 epic' env (App f a) = do f' <- epic' env f

72 epic' env (App f a) = do f' <- epic' env f

70 a' <- epic' env a

73 a' <- epic' env a

71− logLvl 3 $ "Compiled " ++ show f ++ " @@ " ++ show a

72 return (f' @@ a')

74 return (f' @@ a')

73 epic' env (Constant c) = epic c

75 epic' env (Constant c) = epic c

74 epic' env (Set _) = return impossible

76 epic' env (Set _) = return impossible