7c75851 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -70,6 +70,7 @@ Executable idris

70 Util.Pretty,

71

72 RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,

73+ IRTS.Lang, IRTS.LParser,

73

74

74 Paths_idris

75 Paths_idris

75

76

iif/testvm.iifnew file+14

@@ -0,0 +1,14 @@

1+data O 0

2+data S 1

3+

4+fun plus(x, y) = case x of {

5+ O => y

6+ | S(k) => S(plus(k, y))

7+ }

8+

9+fun natToInt(x) = case x of {

10+ O => 0

11+ | S(k) => natToInt(k) + 1

12+ }

13+

14+fun main() = printNum(natToInt(plus(S(S(O)), S(S(O)))))

src/Core/CaseTree.hs+4−4

@@ -11,10 +11,10 @@ import Debug.Trace

11data CaseDef = CaseDef [Name] SC [Term]

12 deriving Show

13

14−data SC = Case Name [CaseAlt]

14+data SC = Case Name [CaseAlt] -- invariant: lowest tags first

15 | STerm Term

16 | UnmatchedCase String -- error message

17− deriving Show

17+ deriving (Show, Eq, Ord)

18{-!

19deriving instance Binary SC

20!-}

@@ -22,7 +22,7 @@ deriving instance Binary SC

22data CaseAlt = ConCase Name Int [Name] SC

23 | ConstCase Const SC

24 | DefaultCase SC

25− deriving Show

25+ deriving (Show, Eq, Ord)

26{-!

27deriving instance Binary CaseAlt

28!-}

@@ -167,7 +167,7 @@ conRule (v:vs) cs err = do groups <- groupCons cs

167

168caseGroups :: [Name] -> [Group] -> SC -> State CS SC

169caseGroups (v:vs) gs err = do g <- altGroups gs

170− return $ Case v g

170+ return $ Case v (sort g)

171 where

172 altGroups [] = return [DefaultCase err]

173 altGroups (ConGroup (CName n i) args : cs)

src/Core/TT.hs+4−4

@@ -239,7 +239,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

239data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

241 | PtrType | VoidType | Forgot

242− deriving Eq

242+ deriving (Eq, Ord)

243{-!

244deriving instance Binary Const

245!-}

@@ -297,7 +297,7 @@ data Binder b = Lam { binderTy :: b }

297 binderVal :: b }

298 | PVar { binderTy :: b }

299 | PVTy { binderTy :: b }

300− deriving (Show, Eq, Functor)

300+ deriving (Show, Eq, Ord, Functor)

301{-!

302deriving instance Binary Binder

303!-}

@@ -382,7 +382,7 @@ instance Show UConstraint where

382type UCs = (Int, [UConstraint])

383

384data NameType = Bound | Ref | DCon Int Int | TCon Int Int

385− deriving (Show)

385+ deriving (Show, Ord)

386{-!

387deriving instance Binary NameType

388!-}

@@ -407,7 +407,7 @@ data TT n = P NameType n (TT n) -- embed type

407 | Constant Const

408 | Erased

409 | Set UExp

410− deriving Functor

410+ deriving (Ord, Functor)

411{-!

412deriving instance Binary TT

413!-}

src/IRTS/LParser.hs+1−1

@@ -60,7 +60,7 @@ pLDecl :: LParser (Name, LDecl)

60pLDecl = do reserved "data"

61 n <- iName []

62 ar <- natural

63− return (n, LConstructor n (fromInteger ar))

63+ return (n, LConstructor n (-1) (fromInteger ar))

64 <|> do reserved "fun"

65 n <- iName []

66 lchar '('

src/IRTS/Lang.hs+2−2

@@ -24,10 +24,10 @@ data LAlt = LConCase Int Name [Name] LExp

24 deriving Show

25

26data LDecl = LFun Name [Name] LExp -- name, arg names, definition

27− | LConstructor Name Int -- constructor name, arity

27+ | LConstructor Name Int Int -- constructor name, tag, arity

28 deriving Show

29

30type LDefs = Ctxt LDecl

31

32−

32+-- TODO: Add constructor tags, then scope and arity checker.

33

src/Idris/AbsSyntaxTree.hs+1

@@ -148,6 +148,7 @@ data Opt = Filename String

148 | IBCSubDir String

149 | ImportDir String

150 | BCAsm String

151+ | FOVM String

151 deriving Eq

152 deriving Eq

152

153

154

src/Idris/Transforms.hs+36−23

@@ -6,39 +6,52 @@ import Idris.AbsSyntax

6import Core.CaseTree

7import Core.TT

8

9+data TTOpt = TermTrans (TT Name -> TT Name) -- term transform

10+ | CaseTrans (SC -> SC) -- case expression transform

11+

9class Transform a where

12class Transform a where

10− transform :: (a -> a) -> a -> a

13+ transform :: TTOpt -> a -> a

11

14

12instance Transform (TT Name) where

15instance Transform (TT Name) where

13− transform t x = t (trans' x) where

16+ transform o@(TermTrans t) tm = trans t tm where

14− trans' (Bind n b sc) = Bind n (fmap (transform t) b) (transform t sc)

17+ trans t (Bind n b tm) = t $ Bind n (transform o b) (trans t tm)

15− trans' (App f a) = App (transform t f) (transform t a)

18+ trans t (App f a) = t $ App (trans t f) (trans t a)

16− trans' x = x

19+ trans t tm = t tm

17−

20+ transform _ tm = tm

18−type TTOpt = TT Name -> TT Name

19

21

20−optimisations :: [TTOpt]

22+instance Transform a => Transform (Binder a) where

21−optimisations = [zero, suc]

23+ transform t (Let ty v) = Let (transform t ty) (transform t v)

24+ transform t b = b { binderTy = transform t (binderTy b) }

22

25

23instance Transform SC where

26instance Transform SC where

24− transform t x = t (trans' x) where

27+ transform o@(CaseTrans t) sc = trans t sc where

28+ trans t (Case n alts) = t (Case n (map (transform o) alts))

29+ trans t x = t x

30+ transform o@(TermTrans t) sc = trans t sc where

25− trans' (Case n alts) = Case n (map transAlt alts)

31+ trans t (Case n alts) = Case n (map (transform o) alts)

26− trans' t = t

32+ trans t (STerm tm) = STerm (t tm)

27−

33+ trans t x = x

34+

35+instance Transform CaseAlt where

28− transAlt (ConCase n i as sc) = ConCase n i as (trans' sc)

36+ transform o (ConCase n i ns sc) = ConCase n i ns (transform o sc)

29− transAlt (ConstCase c sc) = ConstCase c (trans' sc)

37+ transform o (ConstCase c sc) = ConstCase c (transform o sc)

30− transAlt (DefaultCase sc) = DefaultCase (trans' sc)

38+ transform o (DefaultCase sc) = DefaultCase (transform o sc)

31−

39+

32−type CaseOpt = SC -> SC

40+natTrans = [TermTrans zero, TermTrans suc, CaseTrans natcase]

33−

41+

34−zero :: TTOpt

42+zname = NS (UN "O") ["nat","prelude"]

43+sname = NS (UN "S") ["nat","prelude"]

44+

45+zero :: TT Name -> TT Name

35−zero (P _ n _) | n == NS (UN "O") ["nat","prelude"]

46+zero (P _ n _) | n == zname

36 = Constant (BI 0)

47 = Constant (BI 0)

37zero x = x

48zero x = x

38

49

39−suc :: TTOpt

50+suc :: TT Name -> TT Name

40−suc (App (P _ s _) a) | s == NS (UN "S") ["nat","prelude"]

51+suc (App (P _ s _) a) | s == sname

41 = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a]

52 = mkApp (P Ref (UN "prim__addBigInt") Erased) [Constant (BI 1), a]

42suc x = x

53suc x = x

43

54

55+natcase :: SC -> SC

56+natcase = undefined

44

57

src/Main.hs+13

@@ -25,6 +25,9 @@ import Idris.Primitives

25import Idris.Imports

26import Idris.Error

27

28+import IRTS.Lang

29+import IRTS.LParser

30+

28import Paths_idris

31import Paths_idris

29

32

30-- Main program reads command line options, parses the main program, and gets

33-- Main program reads command line options, parses the main program, and gets

@@ -43,6 +46,7 @@ runIdris opts =

43 let ibcsubdir = opt getIBCSubDir opts

46 let ibcsubdir = opt getIBCSubDir opts

44 let importdirs = opt getImportDir opts

47 let importdirs = opt getImportDir opts

45 let bcs = opt getBC opts

48 let bcs = opt getBC opts

49+ let vm = opt getFOVM opts

46

50

47 when (Ver `elem` opts) $ liftIO showver

51 when (Ver `elem` opts) $ liftIO showver

48 when (Usage `elem` opts) $ liftIO usage

52 when (Usage `elem` opts) $ liftIO usage

@@ -52,6 +56,10 @@ runIdris opts =

52 setVerbose runrepl

56 setVerbose runrepl

53 when (Verbose `elem` opts) $ setVerbose True

57 when (Verbose `elem` opts) $ setVerbose True

54 mapM_ makeOption opts

58 mapM_ makeOption opts

59+ -- if we have the --fovm flag, drop into the first order VM testing

60+ case vm of

61+ [] -> return ()

62+ xs -> liftIO $ mapM_ fovm xs

55 -- if we have the --bytecode flag, drop into the bytecode assembler

63 -- if we have the --bytecode flag, drop into the bytecode assembler

56 case bcs of

64 case bcs of

57 [] -> return ()

65 [] -> return ()

@@ -92,6 +100,10 @@ getBC :: Opt -> Maybe String

92getBC (BCAsm str) = Just str

100getBC (BCAsm str) = Just str

93getBC _ = Nothing

101getBC _ = Nothing

94

102

103+getFOVM :: Opt -> Maybe String

104+getFOVM (FOVM str) = Just str

105+getFOVM _ = Nothing

106+

95getOutput :: Opt -> Maybe String

107getOutput :: Opt -> Maybe String

96getOutput (Output str) = Just str

108getOutput (Output str) = Just str

97getOutput _ = Nothing

109getOutput _ = Nothing

@@ -144,6 +156,7 @@ parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)

144parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)

156parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)

145parseArgs ("-i":n:ns) = liftM (ImportDir n : ) (parseArgs ns)

157parseArgs ("-i":n:ns) = liftM (ImportDir n : ) (parseArgs ns)

146parseArgs ("--bytecode":n:ns) = liftM (\x -> NoREPL : BCAsm n : x) (parseArgs ns)

158parseArgs ("--bytecode":n:ns) = liftM (\x -> NoREPL : BCAsm n : x) (parseArgs ns)

159+parseArgs ("--fovm":n:ns) = liftM (\x -> NoREPL : FOVM n : x) (parseArgs ns)

147parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

160parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

148

161

149ver = showVersion version

162ver = showVersion version