8f77986 · Idris-dev · git.iko.soy

idris.cabal+3−3

@@ -33,15 +33,15 @@ Executable idris

3333 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

3434 Idris.Delaborate, Idris.Primitives, Idris.Imports,

3535 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

36− Idris.Coverage,

36+ Idris.Coverage, Idris.IBC,

3737

3838 Paths_idris

3939

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

4141 containers, process, transformers, filepath, directory,

42− epic>=0.9.1

42+ binary, derive, epic>=0.9.1

4343

4444 Extensions: MultiParamTypeClasses, FunctionalDependencies,

45− FlexibleInstances

45+ FlexibleInstances, TemplateHaskell

4646 ghc-prof-options: -auto-all

4747 ghc-options: -rtsopts

impl-paper/overview.tex+1−1

@@ -25,8 +25,8 @@ High level view of steps we've taken to implement this new version:

2525\end{itemize}

2626\item An Elaborator, as an EDSL, which is a language for applying primitive tactics and

2727 constructing derived tactics, from a high level syntax withe implicit arguments.

28−\item Advanced elaborations: using declarations, where clauses.

2928\item Adding primitive operators and a link to Epic~\cite{epic-tfp}.

29+\item Advanced elaborations: using declarations, where clauses, type classes.

3030\end{itemize}

3131

3232For the high level language: we need nothing more than the core type theory,

lib/prelude/vect.idr+1−1

@@ -22,7 +22,7 @@ lookup : Fin n -> Vect a n -> a;

2222lookup fO (x :: xs) = x;

2323lookup (fS k) (x :: xs) = lookup k xs;

2424lookup fO [] impossible;

25−lookup (fS k) [] impossible;

25+lookup (fS _) [] impossible;

2626

2727app : Vect a n -> Vect a m -> Vect a (n + m);

2828app [] ys = ys;

src/Core/Evaluate.hs+22−24

@@ -2,7 +2,7 @@

22 PatternGuards #-}

33

44module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

5− Fun(..), Def(..),

5+ Def(..),

66 Context, initContext, ctxtAlist, uconstraints, next_tvar,

77 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

88 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

@@ -10,6 +10,8 @@ module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

1010

1111import Debug.Trace

1212import Control.Monad.State

13+import qualified Data.Binary as B

14+import Data.Binary hiding (get, put)

1315

1416import Core.TT

1517import Core.CaseTree

@@ -106,8 +108,9 @@ eval ctxt statics genv tm opts = ev True [] tm where

106108 ev top env (P _ n ty)

107109 | Just (Let t v) <- lookup n genv = ev top env v

108110 ev top env (P Ref n ty) = case lookupDef Nothing n ctxt of

109− [Function (Fun _ _ _ v)] -> return v

110− [TyDecl nt ty hty] -> return $ VP nt n hty

111+ [Function _ tm] -> ev True env tm

112+ [TyDecl nt ty] -> do vty <- ev True env ty

113+ return $ VP nt n vty

111114 [CaseOp inl _ _ [] tree] ->

112115 if simpl && (not inl)

113116 then liftM (VP Ref n) (ev top env ty)

@@ -293,8 +296,8 @@ eval_hnf ctxt statics genv tm = ev [] tm where

293296 ev env (P _ n ty)

294297 | Just (Let t v) <- lookup n genv = ev env v

295298 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of

296− [Function (Fun _ _ t _)] -> ev env t

297− [TyDecl nt ty hty] -> return $ HP nt n ty

299+ [Function _ t] -> ev env t

300+ [TyDecl nt ty] -> return $ HP nt n ty

298301 [CaseOp inl _ _ [] tree] ->

299302 do c <- evCase env [] [] tree

300303 case c of

@@ -416,23 +419,20 @@ spec ctxt statics genv tm = undefined

416419

417420-- CONTEXTS -----------------------------------------------------------------

418421

419−data Fun = Fun Type Value Term Value

420− deriving Show

421−

422422{- A definition is either a simple function (just an expression with a type),

423423 a constant, which could be a data or type constructor, an axiom or as an

424424 yet undefined function, or an Operator.

425425 An Operator is a function which explains how to reduce.

426426 A CaseOp is a function defined by a simple case tree -}

427427

428−data Def = Function Fun

429− | TyDecl NameType Type Value

428+data Def = Function Type Term

429+ | TyDecl NameType Type

430430 | Operator Type Int ([Value] -> Maybe Value)

431431 | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable

432432

433433instance Show Def where

434− show (Function f) = "Function: " ++ show f

435− show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty

434+ show (Function ty tm) = "Function: " ++ show (ty, tm)

435+ show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty

436436 show (Operator ty _ _) = "Operator: " ++ show ty

437437 show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++

438438 show ns ++ " " ++ show sc

@@ -453,14 +453,13 @@ veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

453453addToCtxt :: Name -> Term -> Type -> Context -> Context

454454addToCtxt n tm ty uctxt

455455 = let ctxt = definitions uctxt

456− ctxt' = addDef n (Function (Fun ty (veval uctxt [] ty)

457− tm (veval uctxt [] tm))) ctxt in

456+ ctxt' = addDef n (Function ty tm) ctxt in

458457 uctxt { definitions = ctxt' }

459458

460459addTyDecl :: Name -> Type -> Context -> Context

461460addTyDecl n ty uctxt

462461 = let ctxt = definitions uctxt

463− ctxt' = addDef n (TyDecl Ref ty (veval uctxt [] ty)) ctxt in

462+ ctxt' = addDef n (TyDecl Ref ty) ctxt in

464463 uctxt { definitions = ctxt' }

465464

466465addDatatype :: Datatype Name -> Context -> Context

@@ -468,14 +467,14 @@ addDatatype (Data n tag ty cons) uctxt

468467 = let ctxt = definitions uctxt

469468 ty' = normalise uctxt [] ty

470469 ctxt' = addCons 0 cons (addDef n

471− (TyDecl (TCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt) in

470+ (TyDecl (TCon tag (arity ty')) ty) ctxt) in

472471 uctxt { definitions = ctxt' }

473472 where

474473 addCons tag [] ctxt = ctxt

475474 addCons tag ((n, ty) : cons) ctxt

476475 = let ty' = normalise uctxt [] ty in

477476 addCons (tag+1) cons (addDef n

478− (TyDecl (DCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt)

477+ (TyDecl (DCon tag (arity ty')) ty) ctxt)

479478

480479addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

481480addCasedef n alwaysInline tcase ps ty uctxt

@@ -498,8 +497,8 @@ lookupTy :: Maybe [String] -> Name -> Context -> [Type]

498497lookupTy root n ctxt

499498 = do def <- lookupCtxt root n (definitions ctxt)

500499 case def of

501− (Function (Fun ty _ _ _)) -> return ty

502− (TyDecl _ ty _) -> return ty

500+ (Function ty _) -> return ty

501+ (TyDecl _ ty) -> return ty

503502 (Operator ty _ _) -> return ty

504503 (CaseOp _ ty _ _ _) -> return ty

505504

@@ -507,8 +506,8 @@ lookupP :: Maybe [String] -> Name -> Context -> [Term]

507506lookupP root n ctxt

508507 = do def <- lookupCtxt root n (definitions ctxt)

509508 case def of

510− (Function (Fun ty _ tm _)) -> return (P Ref n ty)

511− (TyDecl nt ty hty) -> return (P nt n ty)

509+ (Function ty tm) -> return (P Ref n ty)

510+ (TyDecl nt ty) -> return (P nt n ty)

512511 (CaseOp _ ty _ _ _) -> return (P Ref n ty)

513512 (Operator ty _ _) -> return (P Ref n ty)

514513

@@ -519,8 +518,8 @@ lookupVal :: Maybe [String] -> Name -> Context -> [Value]

519518lookupVal root n ctxt

520519 = do def <- lookupCtxt root n (definitions ctxt)

521520 case def of

522− (Function (Fun _ _ _ htm)) -> return htm

523− (TyDecl nt ty hty) -> return (VP nt n hty)

521+ (Function _ htm) -> return (veval ctxt [] htm)

522+ (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

524523

525524lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

526525lookupTyEnv n env = li n 0 env where

@@ -528,4 +527,3 @@ lookupTyEnv n env = li n 0 env where

528527 li n i ((x, b): xs)

529528 | n == x = Just (i, binderTy b)

530529 | otherwise = li n (i+1) xs

531−

src/Core/TT.hs+2

@@ -7,6 +7,8 @@ import Debug.Trace

77import qualified Data.Map as Map

88import Data.Char

99import Data.List

10+import qualified Data.Binary as B

11+import Data.Binary hiding (get, put)

1012

1113{- The language has:

1214 * Full dependent types

src/Idris/AbsSyntax.hs+27−3

@@ -47,11 +47,27 @@ data IState = IState { tt_ctxt :: Context,

4747 idris_libs :: [String],

4848 idris_hdrs :: [String],

4949 last_proof :: Maybe (Name, [String]),

50− errLine :: Maybe Int

50+ errLine :: Maybe Int,

51+ ibc_write :: [IBCWrite]

5152 }

52−

53+

54+-- information that needs writing for the current module's .ibc file

55+data IBCWrite = IBCFix FixDecl

56+ | IBCImp Name

57+ | IBCStatic Name

58+ | IBCClass Name

59+ | IBCMeta Name

60+ | IBCSyntax Syntax

61+ | IBCKeyword String

62+ | IBCImport FilePath

63+ | IBCObj FilePath

64+ | IBCLib String

65+ | IBCHeader String

66+ | IBCDef Name -- i.e. main context

67+ deriving Show

68+

5369idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

54− "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing

70+ "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing []

5571

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

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

@@ -75,6 +91,12 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

7591addHdr :: String -> Idris ()

7692addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

7793

94+addIBC :: IBCWrite -> Idris ()

95+addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })

96+

97+clearIBC :: Idris ()

98+clearIBC = do i <- get; put (i { ibc_write = [] })

99+

78100getHdrs :: Idris [String]

79101getHdrs = do i <- get; return (idris_hdrs i)

80102

@@ -768,9 +790,11 @@ implicit syn n ptm

768790 let (tm', impdata) = implicitise syn i ptm

769791 let (tm'', spos) = findStatics i tm'

770792 put (i { idris_implicits = addDef n impdata (idris_implicits i) })

793+ addIBC (IBCImp n)

771794 logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata)

772795 i <- get

773796 put (i { idris_statics = addDef n spos (idris_statics i) })

797+ addIBC (IBCStatic n)

774798 return tm''

775799

776800implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg])

src/Idris/Compiler.hs+1−1

@@ -49,7 +49,7 @@ build (n, d) = do i <- getIState

4949impossible = int 42424242

5050

5151instance ToEpic Def where

52− epic (Function (Fun _ _ tm _)) = epic tm

52+ epic (Function tm _) = epic tm

5353 epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising

5454 epic _ = return impossible

5555

src/Idris/ElabDecls.hs+7−2

@@ -47,6 +47,7 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in

4747 logLvl 2 $ "---> " ++ show cty

4848 let nty = normalise ctxt [] cty

4949 ds <- checkDef fc ((n, nty):defer)

50+ addIBC (IBCDef n)

5051 addDeferred ds

5152

5253elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()

@@ -66,6 +67,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

6667 updateContext (addTyDecl n cty) -- temporary, to check cons

6768 cons <- mapM (elabCon info syn) dcons

6869 ttag <- getName

70+ addIBC (IBCDef n)

6971 updateContext (addDatatype (Data n ttag cty cons))

7072

7173elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

@@ -84,6 +86,7 @@ elabCon info syn (n, t_in, fc)

8486 ctxt <- getContext

8587 (cty, _) <- recheckC ctxt fc [] t'

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

89+ addIBC (IBCDef n)

8790 return (n, cty)

8891

8992elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

@@ -103,8 +106,9 @@ elabClauses info fc opts n_in cs_in = let n = liftname info n_in in

103106 logLvl 3 (show tree)

104107 ctxt <- getContext

105108 case lookupTy (namespace info) n ctxt of

106− [ty] -> updateContext (addCasedef n (inlinable opts)

107− tcase pdef ty)

109+ [ty] -> do updateContext (addCasedef n (inlinable opts)

110+ tcase pdef ty)

111+ addIBC (IBCDef n)

108112 [] -> return ()

109113 where

110114 debind (x, y) = (depat x, depat y)

@@ -335,6 +339,7 @@ elabClass info syn fc constraints tn ps ds

335339 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

336340 put (i { idris_classes = addDef tn (CI cn imethods defaults (map fst ps))

337341 (idris_classes i) })

342+ addIBC (IBCClass cn)

338343 where

339344 pibind [] x = x

340345 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

src/Idris/IBC.hsnew file+85

@@ -0,0 +1,85 @@

1+{-# LANGUAGE TypeSynonymInstances, TemplateHaskell #-}

2+

3+module Idris.IBC where

4+

5+import Core.Evaluate

6+import Core.TT

7+import Core.CaseTree

8+import Idris.Compiler

9+import Idris.AbsSyntax

10+

11+import Data.Binary

12+import Data.List

13+import Data.DeriveTH

14+import Control.Monad

15+

16+ibcVersion :: Word8

17+ibcVersion = 1

18+

19+data IBCFile = IBCFile { ver :: Word8,

20+ ibc_imports :: [FilePath],

21+ ibc_fixes :: [FixDecl],

22+ ibc_statics :: [(Name, [Bool])],

23+ ibc_classes :: [(Name, ClassInfo)],

24+ ibc_syntax :: [Syntax],

25+ ibc_keywords :: [String],

26+ ibc_objs :: [FilePath],

27+ ibc_libs :: [String],

28+ ibc_hdrs :: [String],

29+ ibc_defs :: [(Name, Def)] }

30+

31+initIBC :: IBCFile

32+initIBC = IBCFile ibcVersion [] [] [] [] [] [] [] [] [] []

33+

34+loadIBC :: FilePath -> Idris ()

35+loadIBC fp = fail "Not implemented"

36+

37+writeIBC :: FilePath -> Idris ()

38+writeIBC f

39+ = do iLOG $ "Writing ibc " ++ show f

40+ i <- getIState

41+ case idris_metavars i \\ primDefs of

42+ (_:_) -> fail "Can't write ibc when there are unsolve metavariables"

43+ [] -> return ()

44+ return ()

45+

46+$( derive makeBinary ''IBCFile )

47+$( derive makeBinary ''PTerm )

48+$( derive makeBinary ''Raw )

49+$( derive makeBinary ''PTactic' )

50+$( derive makeBinary ''PDo' )

51+$( derive makeBinary ''PArg' )

52+$( derive makeBinary ''ClassInfo )

53+$( derive makeBinary ''Plicity )

54+$( derive makeBinary ''FC )

55+$( derive makeBinary ''Syntax )

56+$( derive makeBinary ''SynContext )

57+$( derive makeBinary ''SSymbol )

58+$( derive makeBinary ''Static )

59+$( derive makeBinary ''Fixity )

60+$( derive makeBinary ''FixDecl )

61+

62+$( derive makeBinary ''Def )

63+$( derive makeBinary ''SC )

64+$( derive makeBinary ''CaseAlt )

65+$( derive makeBinary ''NameType )

66+$( derive makeBinary ''Name )

67+$( derive makeBinary ''Binder )

68+$( derive makeBinary ''TT )

69+$( derive makeBinary ''Const )

70+

71+-- We need this for serialising Def. Fortunately, it never gets used because

72+-- we'll never serialise a primitive operator

73+

74+instance Binary (a -> b) where

75+ put x = return ()

76+ get = undefined

77+

78+-- We assume that universe levels have been checked, so anything external

79+-- can just have the same universe variable and we won't get any new

80+-- cycles.

81+

82+instance Binary UExp where

83+ put x = return ()

84+ get = return (UVar (-1))

85+

src/Idris/Imports.hs+2−2

@@ -9,7 +9,7 @@ import System.FilePath

99import System.Directory

1010import Control.Monad.State

1111

12−data IFileType = IDR FilePath | IBC FilePath

12+data IFileType = IDR FilePath | IBC FilePath FilePath

1313 deriving Eq

1414

1515srcPath :: FilePath -> FilePath

@@ -30,7 +30,7 @@ findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)

3030 ibc <- doesFileExist (ibcPath ibcp)

3131 idr <- doesFileExist (srcPath idrp)

3232 if ibc

33− then return (IBC ibcp)

33+ then return (IBC ibcp idrp)

3434 else if idr

3535 then return (IDR idrp)

3636 else findImport ds fp

src/Idris/Parser.hs+19−5

@@ -5,6 +5,7 @@ import Idris.Imports

55import Idris.Error

66import Idris.ElabDecls

77import Idris.ElabTerm

8+import Idris.IBC

89import Paths_idris

910

1011import Core.CoreParser

@@ -59,7 +60,8 @@ loadModule f

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

6061 case fp of

6162 IDR fn -> loadSource fn

62− IBC fn -> error "Not implemented"

63+ IBC fn src -> idrisCatch (loadIBC fn)

64+ (\c -> loadSource src)

6365 let (dir, fh) = splitFileName f

6466 return (dropExtension fh))

6567 (\e -> do let msg = report e

@@ -72,6 +74,8 @@ loadSource f = do iLOG ("Reading " ++ f)

7274 file <- lift $ readFile f

7375 (mname, modules, rest, pos) <- parseImports f file

7476 mapM_ loadModule modules

77+ clearIBC -- start a new .ibc file

78+ mapM_ (\m -> addIBC (IBCImport m)) modules

7579 ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })

7680 f rest pos

7781 let ds = namespaces mname ds'

@@ -82,6 +86,9 @@ loadSource f = do iLOG ("Reading " ++ f)

8286 -- Now add all the declarations to the context

8387 mapM_ (elabDecl toplevel) ds

8488 iLOG ("Finished " ++ f)

89+ let ibc = dropExtension f ++ ".ibc"

90+ idrisCatch (do writeIBC ibc; clearIBC)

91+ (\c -> return ()) -- failure is harmless

8592 return ()

8693 where

8794 namespaces [] ds = ds

@@ -216,9 +223,12 @@ pSyntaxDecl syn

216223 i <- getState

217224 let rs = syntax_rules i

218225 let ns = syntax_keywords i

226+ let ibc = ibc_write i

219227 let ks = map show (names s)

220228 setState (i { syntax_rules = s : rs,

221− syntax_keywords = ks ++ ns })

229+ syntax_keywords = ks ++ ns,

230+ ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc

231+ })

222232 fc <- pfc

223233 return (PSyntax fc s)

224234 where

@@ -312,7 +322,8 @@ pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

312322 istate <- getState

313323 let fs = map (Fix (f prec)) ops

314324 setState (istate {

315− idris_infixes = sort (fs ++ idris_infixes istate) })

325+ idris_infixes = sort (fs ++ idris_infixes istate),

326+ ibc_write = map IBCFix fs ++ ibc_write istate })

316327 fc <- pfc

317328 return (PFix fc (f prec) ops)

318329

@@ -785,13 +796,16 @@ pWhereblock n syn

785796

786797pDirective :: IParser [PDecl]

787798pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

788− return [PDirective (addLib lib)])

799+ return [PDirective (do addLib lib

800+ addIBC (IBCLib lib))])

789801 <|> try (do lchar '%'; reserved "link"; obj <- strlit;

790802 return [PDirective (do datadir <- lift $ getDataDir

791803 o <- lift $ findInPath [".", datadir] obj

804+ addIBC (IBCObj o)

792805 addObjectFile o)])

793806 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

794− return [PDirective (addHdr hdr)])

807+ return [PDirective (do addHdr hdr

808+ addIBC (IBCHeader hdr))])

795809 <|> do lchar '%'; reserved "logging"; i <- natural;

796810 return [PDirective (setLogLevel (fromInteger i))]

797811