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

git.iko.soy/Idris-dev

Test file for new VM, hook up parser

commit7c75851e8ce715ce25d2ffaa6a1fa50744c08f1b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 6 Aug 2012, 20:49 (14 years ago) parent3f76c32

9 files changed+76−34

compare with master

unifiedsplit

idris.cabal+1 iif/testvm.iif+14 src/Core/CaseTree.hs+4−4 src/Core/TT.hs+4−4 src/IRTS/LParser.hs+1−1 src/IRTS/Lang.hs+2−2 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Transforms.hs+36−23 src/Main.hs+13

idris.cabal+1

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

7070 Util.Pretty,

7171

7272 RTS.Bytecode, RTS.SC, RTS.PreC, RTS.CodegenC,

73+ IRTS.Lang, IRTS.LParser,

7374

7475 Paths_idris

7576

iif/testvm.iifnew file+14

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

1+data O 0

2+data S 1

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

5+ O => y

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

7+ }

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

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

1212 deriving Show

1313

14−data SC = Case Name [CaseAlt]

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

1515 | STerm Term

1616 | UnmatchedCase String -- error message

17− deriving Show

17+ deriving (Show, Eq, Ord)

1818{-!

1919deriving instance Binary SC

2020!-}

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

2222data CaseAlt = ConCase Name Int [Name] SC

2323 | ConstCase Const SC

2424 | DefaultCase SC

25− deriving Show

25+ deriving (Show, Eq, Ord)

2626{-!

2727deriving instance Binary CaseAlt

2828!-}

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

167167

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

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

170− return $ Case v g

170+ return $ Case v (sort g)

171171 where

172172 altGroups [] = return [DefaultCase err]

173173 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)

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

241241 | PtrType | VoidType | Forgot

242− deriving Eq

242+ deriving (Eq, Ord)

243243{-!

244244deriving instance Binary Const

245245!-}

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

297297 binderVal :: b }

298298 | PVar { binderTy :: b }

299299 | PVTy { binderTy :: b }

300− deriving (Show, Eq, Functor)

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

301301{-!

302302deriving instance Binary Binder

303303!-}

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

382382type UCs = (Int, [UConstraint])

383383

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

385− deriving (Show)

385+ deriving (Show, Ord)

386386{-!

387387deriving instance Binary NameType

388388!-}

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

407407 | Constant Const

408408 | Erased

409409 | Set UExp

410− deriving Functor

410+ deriving (Ord, Functor)

411411{-!

412412deriving instance Binary TT

413413!-}

src/IRTS/LParser.hs+1−1

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

6060pLDecl = do reserved "data"

6161 n <- iName []

6262 ar <- natural

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

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

6464 <|> do reserved "fun"

6565 n <- iName []

6666 lchar '('

src/IRTS/Lang.hs+2−2

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

2424 deriving Show

2525

2626data 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

2828 deriving Show

2929

3030type LDefs = Ctxt LDecl

3131

32−

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

3333

src/Idris/AbsSyntaxTree.hs+1

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

148148 | IBCSubDir String

149149 | ImportDir String

150150 | BCAsm String

151+ | FOVM String

151152 deriving Eq

152153

153154

src/Idris/Transforms.hs+36−23

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

66import Core.CaseTree

77import Core.TT

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

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

11+

912class Transform a where

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

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

1114

1215instance Transform (TT Name) where

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

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

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

16− trans' x = x

17−

18−type TTOpt = TT Name -> TT Name

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

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

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

19+ trans t tm = t tm

20+ transform _ tm = tm

1921

20−optimisations :: [TTOpt]

21−optimisations = [zero, suc]

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

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

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

2225

2326instance Transform SC where

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

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

26− trans' t = t

27−

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

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

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

31−

32−type CaseOpt = SC -> SC

33−

34−zero :: TTOpt

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

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

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

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

33+ trans t x = x

34+

35+instance Transform CaseAlt where

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

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

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

39+

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

41+

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

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

44+

45+zero :: TT Name -> TT Name

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

3647 = Constant (BI 0)

3748zero x = x

3849

39−suc :: TTOpt

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

50+suc :: TT Name -> TT Name

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

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

4253suc x = x

4354

55+natcase :: SC -> SC

56+natcase = undefined

4457

src/Main.hs+13

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

2525import Idris.Imports

2626import Idris.Error

2727

28+import IRTS.Lang

29+import IRTS.LParser

30+

2831import Paths_idris

2932

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

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

4346 let ibcsubdir = opt getIBCSubDir opts

4447 let importdirs = opt getImportDir opts

4548 let bcs = opt getBC opts

49+ let vm = opt getFOVM opts

4650

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

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

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

5256 setVerbose runrepl

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

5458 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

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

5664 case bcs of

5765 [] -> return ()

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

92100getBC (BCAsm str) = Just str

93101getBC _ = Nothing

94102

103+getFOVM :: Opt -> Maybe String

104+getFOVM (FOVM str) = Just str

105+getFOVM _ = Nothing

106+

95107getOutput :: Opt -> Maybe String

96108getOutput (Output str) = Just str

97109getOutput _ = Nothing

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

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

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

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

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

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

148161

149162ver = showVersion version