ca6a5e1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

import statement

ca6a5e1Edwin Brady15 years ago

interp.mi → interp.idrrenamed+1−5

compare with master

unifiedsplit

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

1−data Nat = O | S Nat;

1+import nat;

2−

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

4−plus O y = y;

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

7data Ty = TyNat | TyFun Ty Ty;

3data Ty = TyNat | TyFun Ty Ty;

miniidris.cabal+4−2

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

25 Idris.AbsSyntax, Idris.Parser, Idris.REPL,

26 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

27− Idris.Delaborate, Idris.Primitives

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

28+

29+ Paths_miniidris

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

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

30− containers, process, transformers

32+ containers, process, transformers, filepath, directory

32 Extensions: MultiParamTypeClasses, FunctionalDependencies,

34 Extensions: MultiParamTypeClasses, FunctionalDependencies,

33 FlexibleInstances

35 FlexibleInstances

nat.idrnew file+6

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

1+data Nat = O | S Nat;

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

4+plus O y = y;

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

src/Idris/AbsSyntax.hs+21−2

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

26 idris_implicits :: Ctxt [PArg],

27 idris_log :: String,

28 idris_options :: IOption,

29− idris_name :: Int

29+ idris_name :: Int,

30+ imported :: [FilePath]

30 }

31 }

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

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

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

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

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

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

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

41getIState :: Idris IState

42getIState :: Idris IState

42getIState = get

43getIState = get

45+putIState :: IState -> Idris ()

46+putIState = put

47+

44getName :: Idris Int

48getName :: Idris Int

45getName = do i <- get;

49getName = do i <- get;

46 let idx = idris_name i;

50 let idx = idris_name i;

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

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

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

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

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

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

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

116+ | PImport String

112 deriving Functor

117 deriving Functor

113

118

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

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

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

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

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

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

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

136declared (PParams _ ds) = concatMap declared ds

141declared (PParams _ ds) = concatMap declared ds

142+declared (PImport _) = []

137

143

138-- High level language terms

144-- High level language terms

139--

145--

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

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

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

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

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

379

385

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

5import Idris.AbsSyntax

6import Idris.Error

7import Idris.Delaborate

8+import Idris.Imports

9+import Paths_miniidris

9import Core.TT

11import Core.TT

10import Core.Elaborate

12import Core.Elaborate

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

13import Core.CaseTree

15import Core.CaseTree

15import Control.Monad

17import Control.Monad

18+import Control.Monad.State

16import Debug.Trace

19import Debug.Trace

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

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

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

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

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

48elabCon info (n, t)

51elabCon info (n, t)

49 = do ctxt <- getContext

52 = do ctxt <- getContext

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

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

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

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

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

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

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

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

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

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

55 return (n, cty)

58 return (n, cty)

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

79 (build info True (infTerm tm))

82 (build info True (infTerm tm))

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

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

81 let vtm = getInferTerm tm'

84 let vtm = getInferTerm tm'

82− iLOG (show vtm)

85+ logLvl 2 (show vtm)

83 tclift $ recheck ctxt [] vtm

86 tclift $ recheck ctxt [] vtm

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

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

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

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

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

100 mapM_ (elabDecl' winfo) whereblock

103 mapM_ (elabDecl' winfo) whereblock

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

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

102− iLOG (showImp True rhs)

105+ logLvl 2 (showImp True rhs)

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

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

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

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

105 (do pbinds lhs_tm

108 (do pbinds lhs_tm

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

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

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

134 }

137 }

135

138

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

140+

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

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

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

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

138

143

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

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

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

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

141 elabType info n ty

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

143 elabData info d

148 elabData info d

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

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

145 elabClauses info n ps

150 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

148 where

152 where

149 pinfo = let ds = concatMap declared ps

153 pinfo = let ds = concatMap declared ps

150 newps = params info ++ ns

154 newps = params info ++ ns

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

152 newb = addAlist dsParams (inblock info) in

156 newb = addAlist dsParams (inblock info) in

153 info { params = newps,

157 info { params = newps,

154 inblock = newb }

158 inblock = newb }

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

160+

155

161

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

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

157-- elaborated, typechecked term.

163-- elaborated, typechecked term.

src/Idris/Imports.hsnew file+38

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

1+module Idris.Imports where

3+import Idris.AbsSyntax

5+import Core.TT

6+import Paths_miniidris

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 @@

1module Idris.Parser where

3import Idris.AbsSyntax

4+import Idris.Imports

5+import Paths_miniidris

6+import Idris.ElabDecls

5import Core.CoreParser

8import Core.CoreParser

6import Core.TT

9import Core.TT

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

38chlit = PTok.charLiteral lexer

41chlit = PTok.charLiteral lexer

39lchar = lexeme.char

42lchar = lexeme.char

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+

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

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

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+

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

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

44−parseProg syn fname

91+parseProg syn fname input pos

45− = do file <- lift $ readFile fname

46− i <- get

92+ = do i <- get

93+ case (runParser (do setPosition pos

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

94+ ps <- many1 (pDecl syn)

48− eof

95+ eof

49− i' <- getState

96+ i' <- getState

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

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

51− Left err -> fail (show err)

98+ Left err -> fail (show err)

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

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

53− return (collect x)

100+ return (collect x)

101

55-- Collect PClauses with the same function name

102-- Collect PClauses with the same function name

56collect :: [PDecl] -> [PDecl]

103collect :: [PDecl] -> [PDecl]

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

75 return [fmap (addImpl i) d]

122 return [fmap (addImpl i) d]

76 <|> try (pUsing syn)

123 <|> try (pUsing syn)

77 <|> try (pParams syn)

124 <|> try (pParams syn)

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

126+ fp <- identifier

127+ lchar ';'

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

129

79pFunDecl :: SyntaxInfo -> IParser [PDecl]

130pFunDecl :: SyntaxInfo -> IParser [PDecl]

80pFunDecl syn

131pFunDecl syn

src/Main.hs+1−20

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

20import Idris.REPL

21import Idris.ElabDecls

22import Idris.Primitives

23+import Idris.Imports

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

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

25-- on with the REPL.

26-- on with the REPL.

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

44 makeOption (OLogging i) = setLogLevel i

45 makeOption (OLogging i) = setLogLevel i

45 makeOption _ = return ()

46 makeOption _ = return ()

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−

67getFile :: Opt -> Maybe String

48getFile :: Opt -> Maybe String

68getFile (Filename str) = Just str

49getFile (Filename str) = Just str

69getFile _ = Nothing

50getFile _ = Nothing