ca6a5e1 · Idris-dev · git.iko.soy

interp.mi → interp.idrrenamed+1−5

@@ -1,8 +1,4 @@

1−data Nat = O | S Nat;

2−

3−plus : Nat -> Nat -> Nat;

4−plus O y = y;

5−plus (S k) y = S (plus k y);

1+import nat;

62

73data Ty = TyNat | TyFun Ty Ty;

84

miniidris.cabal+4−2

@@ -24,10 +24,12 @@ Executable miniidris

2424

2525 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

2626 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

27− Idris.Delaborate, Idris.Primitives

27+ Idris.Delaborate, Idris.Primitives, Idris.Imports,

28+

29+ Paths_miniidris

2830

2931 Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline,

30− containers, process, transformers

32+ containers, process, transformers, filepath, directory

3133

3234 Extensions: MultiParamTypeClasses, FunctionalDependencies,

3335 FlexibleInstances

nat.idrnew file+6

@@ -0,0 +1,6 @@

1+data Nat = O | S Nat;

2+

3+plus : Nat -> Nat -> Nat;

4+plus O y = y;

5+plus (S k) y = S (plus k y);

6+

src/Idris/AbsSyntax.hs+21−2

@@ -26,10 +26,11 @@ data IState = IState { tt_ctxt :: Context,

2626 idris_implicits :: Ctxt [PArg],

2727 idris_log :: String,

2828 idris_options :: IOption,

29− idris_name :: Int

29+ idris_name :: Int,

30+ imported :: [FilePath]

3031 }

3132

32−idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0

33+idrisInit = IState emptyContext [] emptyContext "" defaultOpts 0 []

3334

3435-- The monad for the main REPL - reading and processing files and updating

3536-- global state (hence the IO inner monad).

@@ -41,6 +42,9 @@ getContext = do i <- get; return (tt_ctxt i)

4142getIState :: Idris IState

4243getIState = get

4344

45+putIState :: IState -> Idris ()

46+putIState = put

47+

4448getName :: Idris Int

4549getName = do i <- get;

4650 let idx = idris_name i;

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

109113 | PClauses Name [PClause' t] -- pattern clause

110114 | PData (PData' t) -- data declaration

111115 | PParams [(Name, PTerm)] [PDecl' t] -- params block

116+ | PImport String

112117 deriving Functor

113118

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

@@ -134,6 +139,7 @@ declared (PTy n t) = [n]

134139declared (PClauses n _) = [] -- not a declaration

135140declared (PData (PDatadecl n _ ts)) = n : map fst ts

136141declared (PParams _ ds) = concatMap declared ds

142+declared (PImport _) = []

137143

138144-- High level language terms

139145--

@@ -377,3 +383,16 @@ addImpl ist ptm = ai [] ptm

377383 | n == n' = Just (t, reverse acc ++ gs)

378384 find n (g : gs) acc = find n gs (g : acc)

379385

386+-- Debugging/logging stuff

387+

388+dumpDecls :: [PDecl] -> String

389+dumpDecls [] = ""

390+dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

391+

392+dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops

393+dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

394+dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)

395+dumpDecl (PData d) = showDImp True d

396+dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

397+dumpDecl (PImport i) = "import " ++ i

398+

src/Idris/ElabDecls.hs+13−7

@@ -5,6 +5,8 @@ module Idris.ElabDecls where

55import Idris.AbsSyntax

66import Idris.Error

77import Idris.Delaborate

8+import Idris.Imports

9+import Paths_miniidris

810

911import Core.TT

1012import Core.Elaborate

@@ -13,6 +15,7 @@ import Core.Typecheck

1315import Core.CaseTree

1416

1517import Control.Monad

18+import Control.Monad.State

1619import Debug.Trace

1720

1821-- Data to pass to recursively called elaborators; e.g. for where blocks,

@@ -47,9 +50,9 @@ elabData info (PDatadecl n t dcons)

4750elabCon :: ElabInfo -> (Name, PTerm) -> Idris (Name, Type)

4851elabCon info (n, t)

4952 = do ctxt <- getContext

50− iLOG $ "Constructor " ++ show n ++ " : " ++ showImp True t

53+ logLvl 2 $ "Constructor " ++ show n ++ " : " ++ showImp True t

5154 (t', log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

52−-- iLOG $ "Rechecking " ++ show t'

55+-- logLvl 2 $ "Rechecking " ++ show t'

5356 (cty, _) <- tclift $ recheck ctxt [] t'

5457 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

5558 return (n, cty)

@@ -79,7 +82,7 @@ elabVal info tm

7982 (build info True (infTerm tm))

8083 logLvl 3 ("Value: " ++ show tm')

8184 let vtm = getInferTerm tm'

82− iLOG (show vtm)

85+ logLvl 2 (show vtm)

8386 tclift $ recheck ctxt [] vtm

8487

8588elabClause :: ElabInfo -> PClause -> Idris (Term, Term)

@@ -99,7 +102,7 @@ elabClause info (PClause fname lhs rhs whereblock)

99102 let winfo = pinfo (pvars ist lhs_tm) whereblock windex

100103 mapM_ (elabDecl' winfo) whereblock

101104 -- Now build the RHS, using the type of the LHS as the goal.

102− iLOG (showImp True rhs)

105+ logLvl 2 (showImp True rhs)

103106 ctxt <- getContext -- new context with where block added

104107 (rhs', _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

105108 (do pbinds lhs_tm

@@ -133,18 +136,19 @@ elabClause info (PClause fname lhs rhs whereblock)

133136 _ -> MN i (show n)) . l

134137 }

135138

139+-- TODO: Also build a 'binary' version of each declaration for fast reloading

140+

136141elabDecl :: ElabInfo -> PDecl -> Idris ()

137142elabDecl info d = idrisCatch (elabDecl' info d) (\e -> iputStrLn (report e))

138143

139144elabDecl' info (PFix _ _) = return () -- nothing to elaborate

140145elabDecl' info (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

141146 elabType info n ty

142−elabDecl' info (PData d) = do iLOG $ "Elaborating " ++ show d

147+elabDecl' info (PData d) = do iLOG $ "Elaborating " ++ show (d_name d)

143148 elabData info d

144149elabDecl' info d@(PClauses n ps) = do iLOG $ "Elaborating clause " ++ show n

145150 elabClauses info n ps

146−elabDecl' info (PParams ns ps) = do iLOG $ "Params block " ++ show ns

147− mapM_ (elabDecl' pinfo) ps

151+elabDecl' info (PParams ns ps) = mapM_ (elabDecl' pinfo) ps

148152 where

149153 pinfo = let ds = concatMap declared ps

150154 newps = params info ++ ns

@@ -152,6 +156,8 @@ elabDecl' info (PParams ns ps) = do iLOG $ "Params block " ++ show ns

152156 newb = addAlist dsParams (inblock info) in

153157 info { params = newps,

154158 inblock = newb }

159+-- elabDecl' info (PImport i) = loadModule i

160+

155161

156162-- Using the elaborator, convert a term in raw syntax to a fully

157163-- elaborated, typechecked term.

src/Idris/Imports.hsnew file+38

@@ -0,0 +1,38 @@

1+module Idris.Imports where

2+

3+import Idris.AbsSyntax

4+

5+import Core.TT

6+import Paths_miniidris

7+

8+import System.FilePath

9+import System.Directory

10+import Control.Monad.State

11+

12+data IFileType = IDR FilePath | IBC FilePath

13+ deriving Eq

14+

15+srcPath :: FilePath -> FilePath

16+srcPath fp = let (n, ext) = splitExtension fp in

17+ case ext of

18+ "" -> fp ++ ".idr"

19+ _ -> fp

20+

21+-- Get name of byte compiled version of an import

22+ibcPath :: FilePath -> FilePath

23+ibcPath fp = let (n, ext) = splitExtension fp in

24+ n ++ ".ibc"

25+

26+findImport :: [FilePath] -> FilePath -> IO IFileType

27+findImport [] fp = fail $ "Can't find import " ++ fp

28+findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)

29+ let idrp = srcPath (d ++ "/" ++ fp)

30+ ibc <- doesFileExist (ibcPath ibcp)

31+ idr <- doesFileExist (srcPath idrp)

32+ if ibc

33+ then return (IBC ibcp)

34+ else if idr

35+ then return (IDR idrp)

36+ else findImport ds fp

37+

38+

src/Idris/Parser.hs+62−11

@@ -1,6 +1,9 @@

11module Idris.Parser where

22

33import Idris.AbsSyntax

4+import Idris.Imports

5+import Paths_miniidris

6+import Idris.ElabDecls

47

58import Core.CoreParser

69import Core.TT

@@ -38,19 +41,63 @@ strlit = PTok.stringLiteral lexer

3841chlit = PTok.charLiteral lexer

3942lchar = lexeme.char

4043

44+-- Loading modules

45+

46+loadModule :: FilePath -> Idris ()

47+loadModule f = do datadir <- lift $ getDataDir

48+ fp <- lift $ findImport [datadir, "."] f

49+ i <- getIState

50+ if (f `elem` imported i)

51+ then iLOG $ "Already read " ++ f

52+ else do putIState (i { imported = f : imported i })

53+ case fp of

54+ IDR fn -> loadSource fn

55+ IBC fn -> error "Not implemented"

56+

57+loadSource :: FilePath -> Idris ()

58+loadSource f = do iLOG ("Reading " ++ f)

59+ file <- lift $ readFile f

60+ (modules, rest, pos) <- parseImports f file

61+ mapM_ loadModule modules

62+ ds <- parseProg defaultSyntax f rest pos

63+ logLvl 3 (dumpDecls ds)

64+ i <- getIState

65+ logLvl 3 (show (idris_infixes i))

66+ -- Now add all the declarations to the context

67+ mapM_ (elabDecl toplevel) ds

68+ iLOG ("Finished " ++ f)

69+ return ()

70+

4171parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

4272

43−parseProg :: SyntaxInfo -> String -> Idris [PDecl]

44−parseProg syn fname

45− = do file <- lift $ readFile fname

46− i <- get

47− case (runParser (do ps <- many1 (pDecl syn)

48− eof

49− i' <- getState

50− return (concat ps, i')) i fname file) of

51− Left err -> fail (show err)

52− Right (x, i) -> do put i

53− return (collect x)

73+parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)

74+parseImports fname input

75+ = do i <- get

76+ case (runParser (do ps <- many pImport

77+ rest <- getInput

78+ pos <- getPosition

79+ return ((ps, rest, pos), i)) i fname input) of

80+ Left err -> fail (show err)

81+ Right (x, i) -> do put i

82+ return x

83+

84+pImport :: IParser String

85+pImport = do reserved "import"

86+ f <- identifier

87+ lchar ';'

88+ return f

89+

90+parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]

91+parseProg syn fname input pos

92+ = do i <- get

93+ case (runParser (do setPosition pos

94+ ps <- many1 (pDecl syn)

95+ eof

96+ i' <- getState

97+ return (concat ps, i')) i fname input) of

98+ Left err -> fail (show err)

99+ Right (x, i) -> do put i

100+ return (collect x)

54101

55102-- Collect PClauses with the same function name

56103collect :: [PDecl] -> [PDecl]

@@ -75,6 +122,10 @@ pDecl syn

75122 return [fmap (addImpl i) d]

76123 <|> try (pUsing syn)

77124 <|> try (pParams syn)

125+ <|> try (do reserved "import"

126+ fp <- identifier

127+ lchar ';'

128+ fail "imports must be at the top of file")

78129

79130pFunDecl :: SyntaxInfo -> IParser [PDecl]

80131pFunDecl syn

src/Main.hs+1−20

@@ -20,6 +20,7 @@ import Idris.Parser

2020import Idris.REPL

2121import Idris.ElabDecls

2222import Idris.Primitives

23+import Idris.Imports

2324

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

2526-- on with the REPL.

@@ -44,26 +45,6 @@ runIdris opts =

4445 makeOption (OLogging i) = setLogLevel i

4546 makeOption _ = return ()

4647

47−loadModule :: FilePath -> Idris ()

48−loadModule f = do iLOG ("Reading " ++ show f)

49− ds <- parseProg defaultSyntax f

50− logLvl 3 (dumpDecls ds)

51− i <- get

52− logLvl 3 (show (idris_infixes i))

53− -- Now add all the declarations to the context

54− mapM_ (elabDecl toplevel) ds

55− return ()

56−

57−dumpDecls :: [PDecl] -> String

58−dumpDecls [] = ""

59−dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

60−

61−dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops

62−dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

63−dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)

64−dumpDecl (PData d) = showDImp True d

65−dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

66−

6748getFile :: Opt -> Maybe String

6849getFile (Filename str) = Just str

6950getFile _ = Nothing