a4a77bf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make do notation use Monad class

commita4a77bf892d346f21c0fea704eb8d2827be2e992 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 9 Nov 2011, 17:42 (15 years ago) parent285112b

4 files changed+17−5

compare with master

unifiedsplit

lib/io.idr+7 lib/nat.idr+5−2 src/Idris/AbsSyntax.hs+1−1 src/Idris/Compiler.hs+4−2

lib/io.idr+7

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

88io_return : a -> IO a;

99io_return = prim__IO;

1010

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+

1218

1319interpFTy : FTy -> Set;

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

3743mkForeign : Foreign x -> x;

3844-- mkForeign compiled as primitive

3945

46+

lib/nat.idr+5−2

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

1818mult O y = O;

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

2020

21−instance numNat : Num Nat;

22−instance numNat = instanceNum plus sub mult;

21+instance Num Nat where {

22+ (+) = plus;

23+ (-) = sub;

24+ (*) = mult;

25+}

2326

2427instance Eq Nat where {

2528 O == O = True;

src/Idris/AbsSyntax.hs+1−1

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

344344 | Expr Name

345345 deriving Show

346346

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

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

348348

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

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

src/Idris/Compiler.hs+4−2

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

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

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

2929

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

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

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

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

3133

3234class ToEpic a where

3335 epic :: a -> Idris E.Term

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

3739 case lookup n (idris_prims i) of

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

3941 _ -> do def <- epic d

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

4043 return $ EpicFn (ename n) def

4144

4245impossible = int 42424242

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

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

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

7073 a' <- epic' env a

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

7274 return (f' @@ a')

7375 epic' env (Constant c) = epic c

7476 epic' env (Set _) = return impossible