From 8f779863c46f2ff8abdd046a9a01947cbf4be2b5 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Wed, 7 Dec 2011 22:53:47 +0000 Subject: [PATCH] Added some serialisation --- idris.cabal | 6 +-- impl-paper/overview.tex | 2 +- lib/prelude/vect.idr | 2 +- src/Core/Evaluate.hs | 46 +++++++++++----------- src/Core/TT.hs | 2 + src/Idris/AbsSyntax.hs | 30 +++++++++++++-- src/Idris/Compiler.hs | 2 +- src/Idris/ElabDecls.hs | 9 ++++- src/Idris/IBC.hs | 85 +++++++++++++++++++++++++++++++++++++++++ src/Idris/Imports.hs | 4 +- src/Idris/Parser.hs | 24 +++++++++--- 11 files changed, 170 insertions(+), 42 deletions(-) create mode 100644 src/Idris/IBC.hs diff --git a/idris.cabal b/idris.cabal index 639e3be0da..34d350ac3c 100644 --- a/idris.cabal +++ b/idris.cabal @@ -33,15 +33,15 @@ Executable idris Idris.REPLParser, Idris.ElabDecls, Idris.Error, Idris.Delaborate, Idris.Primitives, Idris.Imports, Idris.Compiler, Idris.Prover, Idris.ElabTerm, - Idris.Coverage, + Idris.Coverage, Idris.IBC, Paths_idris Build-depends: base>=4 && <5, parsec, mtl, Cabal, readline, containers, process, transformers, filepath, directory, - epic>=0.9.1 + binary, derive, epic>=0.9.1 Extensions: MultiParamTypeClasses, FunctionalDependencies, - FlexibleInstances + FlexibleInstances, TemplateHaskell ghc-prof-options: -auto-all ghc-options: -rtsopts diff --git a/impl-paper/overview.tex b/impl-paper/overview.tex index fd9a1fb44d..5b1b437d4d 100644 --- a/impl-paper/overview.tex +++ b/impl-paper/overview.tex @@ -25,8 +25,8 @@ \section{overview} \end{itemize} \item An Elaborator, as an EDSL, which is a language for applying primitive tactics and constructing derived tactics, from a high level syntax withe implicit arguments. -\item Advanced elaborations: using declarations, where clauses. \item Adding primitive operators and a link to Epic~\cite{epic-tfp}. +\item Advanced elaborations: using declarations, where clauses, type classes. \end{itemize} For the high level language: we need nothing more than the core type theory, diff --git a/lib/prelude/vect.idr b/lib/prelude/vect.idr index e7917d9dc2..83bcdb7eab 100644 --- a/lib/prelude/vect.idr +++ b/lib/prelude/vect.idr @@ -22,7 +22,7 @@ lookup : Fin n -> Vect a n -> a; lookup fO (x :: xs) = x; lookup (fS k) (x :: xs) = lookup k xs; lookup fO [] impossible; -lookup (fS k) [] impossible; +lookup (fS _) [] impossible; app : Vect a n -> Vect a m -> Vect a (n + m); app [] ys = ys; diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs index f4fc1188d5..309404f586 100644 --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -2,7 +2,7 @@ PatternGuards #-} module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf, - Fun(..), Def(..), + Def(..), Context, initContext, ctxtAlist, uconstraints, next_tvar, addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator, lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv, @@ -10,6 +10,8 @@ module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf, import Debug.Trace import Control.Monad.State +import qualified Data.Binary as B +import Data.Binary hiding (get, put) import Core.TT import Core.CaseTree @@ -106,8 +108,9 @@ eval ctxt statics genv tm opts = ev True [] tm where ev top env (P _ n ty) | Just (Let t v) <- lookup n genv = ev top env v ev top env (P Ref n ty) = case lookupDef Nothing n ctxt of - [Function (Fun _ _ _ v)] -> return v - [TyDecl nt ty hty] -> return $ VP nt n hty + [Function _ tm] -> ev True env tm + [TyDecl nt ty] -> do vty <- ev True env ty + return $ VP nt n vty [CaseOp inl _ _ [] tree] -> if simpl && (not inl) then liftM (VP Ref n) (ev top env ty) @@ -293,8 +296,8 @@ eval_hnf ctxt statics genv tm = ev [] tm where ev env (P _ n ty) | Just (Let t v) <- lookup n genv = ev env v ev env (P Ref n ty) = case lookupDef Nothing n ctxt of - [Function (Fun _ _ t _)] -> ev env t - [TyDecl nt ty hty] -> return $ HP nt n ty + [Function _ t] -> ev env t + [TyDecl nt ty] -> return $ HP nt n ty [CaseOp inl _ _ [] tree] -> do c <- evCase env [] [] tree case c of @@ -416,23 +419,20 @@ spec ctxt statics genv tm = undefined -- CONTEXTS ----------------------------------------------------------------- -data Fun = Fun Type Value Term Value - deriving Show - {- A definition is either a simple function (just an expression with a type), a constant, which could be a data or type constructor, an axiom or as an yet undefined function, or an Operator. An Operator is a function which explains how to reduce. A CaseOp is a function defined by a simple case tree -} -data Def = Function Fun - | TyDecl NameType Type Value +data Def = Function Type Term + | TyDecl NameType Type | Operator Type Int ([Value] -> Maybe Value) | CaseOp Bool Type [(Term, Term)] [Name] SC -- Bool for inlineable instance Show Def where - show (Function f) = "Function: " ++ show f - show (TyDecl nt ty val) = "TyDecl: " ++ show nt ++ " " ++ show ty + show (Function ty tm) = "Function: " ++ show (ty, tm) + show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty show (Operator ty _ _) = "Operator: " ++ show ty show (CaseOp _ ty ps ns sc) = "Case: " ++ show ps ++ "\n" ++ show ns ++ " " ++ show sc @@ -453,14 +453,13 @@ veval ctxt env t = evalState (eval ctxt emptyContext env t []) () addToCtxt :: Name -> Term -> Type -> Context -> Context addToCtxt n tm ty uctxt = let ctxt = definitions uctxt - ctxt' = addDef n (Function (Fun ty (veval uctxt [] ty) - tm (veval uctxt [] tm))) ctxt in + ctxt' = addDef n (Function ty tm) ctxt in uctxt { definitions = ctxt' } addTyDecl :: Name -> Type -> Context -> Context addTyDecl n ty uctxt = let ctxt = definitions uctxt - ctxt' = addDef n (TyDecl Ref ty (veval uctxt [] ty)) ctxt in + ctxt' = addDef n (TyDecl Ref ty) ctxt in uctxt { definitions = ctxt' } addDatatype :: Datatype Name -> Context -> Context @@ -468,14 +467,14 @@ addDatatype (Data n tag ty cons) uctxt = let ctxt = definitions uctxt ty' = normalise uctxt [] ty ctxt' = addCons 0 cons (addDef n - (TyDecl (TCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt) in + (TyDecl (TCon tag (arity ty')) ty) ctxt) in uctxt { definitions = ctxt' } where addCons tag [] ctxt = ctxt addCons tag ((n, ty) : cons) ctxt = let ty' = normalise uctxt [] ty in addCons (tag+1) cons (addDef n - (TyDecl (DCon tag (arity ty')) ty (veval uctxt [] ty)) ctxt) + (TyDecl (DCon tag (arity ty')) ty) ctxt) addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context addCasedef n alwaysInline tcase ps ty uctxt @@ -498,8 +497,8 @@ lookupTy :: Maybe [String] -> Name -> Context -> [Type] lookupTy root n ctxt = do def <- lookupCtxt root n (definitions ctxt) case def of - (Function (Fun ty _ _ _)) -> return ty - (TyDecl _ ty _) -> return ty + (Function ty _) -> return ty + (TyDecl _ ty) -> return ty (Operator ty _ _) -> return ty (CaseOp _ ty _ _ _) -> return ty @@ -507,8 +506,8 @@ lookupP :: Maybe [String] -> Name -> Context -> [Term] lookupP root n ctxt = do def <- lookupCtxt root n (definitions ctxt) case def of - (Function (Fun ty _ tm _)) -> return (P Ref n ty) - (TyDecl nt ty hty) -> return (P nt n ty) + (Function ty tm) -> return (P Ref n ty) + (TyDecl nt ty) -> return (P nt n ty) (CaseOp _ ty _ _ _) -> return (P Ref n ty) (Operator ty _ _) -> return (P Ref n ty) @@ -519,8 +518,8 @@ lookupVal :: Maybe [String] -> Name -> Context -> [Value] lookupVal root n ctxt = do def <- lookupCtxt root n (definitions ctxt) case def of - (Function (Fun _ _ _ htm)) -> return htm - (TyDecl nt ty hty) -> return (VP nt n hty) + (Function _ htm) -> return (veval ctxt [] htm) + (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty)) lookupTyEnv :: Name -> Env -> Maybe (Int, Type) lookupTyEnv n env = li n 0 env where @@ -528,4 +527,3 @@ lookupTyEnv n env = li n 0 env where li n i ((x, b): xs) | n == x = Just (i, binderTy b) | otherwise = li n (i+1) xs - diff --git a/src/Core/TT.hs b/src/Core/TT.hs index 7b21e88b17..77118536c7 100644 --- a/src/Core/TT.hs +++ b/src/Core/TT.hs @@ -7,6 +7,8 @@ import Debug.Trace import qualified Data.Map as Map import Data.Char import Data.List +import qualified Data.Binary as B +import Data.Binary hiding (get, put) {- The language has: * Full dependent types diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index c9b725992d..a7e5dcf422 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -47,11 +47,27 @@ data IState = IState { tt_ctxt :: Context, idris_libs :: [String], idris_hdrs :: [String], last_proof :: Maybe (Name, [String]), - errLine :: Maybe Int + errLine :: Maybe Int, + ibc_write :: [IBCWrite] } - + +-- information that needs writing for the current module's .ibc file +data IBCWrite = IBCFix FixDecl + | IBCImp Name + | IBCStatic Name + | IBCClass Name + | IBCMeta Name + | IBCSyntax Syntax + | IBCKeyword String + | IBCImport FilePath + | IBCObj FilePath + | IBCLib String + | IBCHeader String + | IBCDef Name -- i.e. main context + deriving Show + idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext - "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing + "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing [] -- The monad for the main REPL - reading and processing files and updating -- global state (hence the IO inner monad). @@ -75,6 +91,12 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i }) addHdr :: String -> Idris () addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i }) +addIBC :: IBCWrite -> Idris () +addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i }) + +clearIBC :: Idris () +clearIBC = do i <- get; put (i { ibc_write = [] }) + getHdrs :: Idris [String] getHdrs = do i <- get; return (idris_hdrs i) @@ -768,9 +790,11 @@ implicit syn n ptm let (tm', impdata) = implicitise syn i ptm let (tm'', spos) = findStatics i tm' put (i { idris_implicits = addDef n impdata (idris_implicits i) }) + addIBC (IBCImp n) logLvl 5 ("Implicit " ++ show n ++ " " ++ show impdata) i <- get put (i { idris_statics = addDef n spos (idris_statics i) }) + addIBC (IBCStatic n) return tm'' implicitise :: SyntaxInfo -> IState -> PTerm -> (PTerm, [PArg]) diff --git a/src/Idris/Compiler.hs b/src/Idris/Compiler.hs index 66c9fcf2f9..33a8102b76 100644 --- a/src/Idris/Compiler.hs +++ b/src/Idris/Compiler.hs @@ -49,7 +49,7 @@ build (n, d) = do i <- getIState impossible = int 42424242 instance ToEpic Def where - epic (Function (Fun _ _ tm _)) = epic tm + epic (Function tm _) = epic tm epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising epic _ = return impossible diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs index 3b8eedb6ab..41b159f850 100644 --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -47,6 +47,7 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in logLvl 2 $ "---> " ++ show cty let nty = normalise ctxt [] cty ds <- checkDef fc ((n, nty):defer) + addIBC (IBCDef n) addDeferred ds elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris () @@ -66,6 +67,7 @@ elabData info syn fc (PDatadecl n t_in dcons) updateContext (addTyDecl n cty) -- temporary, to check cons cons <- mapM (elabCon info syn) dcons ttag <- getName + addIBC (IBCDef n) updateContext (addDatatype (Data n ttag cty cons)) elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type) @@ -84,6 +86,7 @@ elabCon info syn (n, t_in, fc) ctxt <- getContext (cty, _) <- recheckC ctxt fc [] t' logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty + addIBC (IBCDef n) return (n, cty) elabClauses :: 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 logLvl 3 (show tree) ctxt <- getContext case lookupTy (namespace info) n ctxt of - [ty] -> updateContext (addCasedef n (inlinable opts) - tcase pdef ty) + [ty] -> do updateContext (addCasedef n (inlinable opts) + tcase pdef ty) + addIBC (IBCDef n) [] -> return () where debind (x, y) = (depat x, depat y) @@ -335,6 +339,7 @@ elabClass info syn fc constraints tn ps ds let defaults = map (\ (x, (y, z)) -> (x,y)) defs put (i { idris_classes = addDef tn (CI cn imethods defaults (map fst ps)) (idris_classes i) }) + addIBC (IBCClass cn) where pibind [] x = x pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x) diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs new file mode 100644 index 0000000000..798474299c --- /dev/null +++ b/src/Idris/IBC.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE TypeSynonymInstances, TemplateHaskell #-} + +module Idris.IBC where + +import Core.Evaluate +import Core.TT +import Core.CaseTree +import Idris.Compiler +import Idris.AbsSyntax + +import Data.Binary +import Data.List +import Data.DeriveTH +import Control.Monad + +ibcVersion :: Word8 +ibcVersion = 1 + +data IBCFile = IBCFile { ver :: Word8, + ibc_imports :: [FilePath], + ibc_fixes :: [FixDecl], + ibc_statics :: [(Name, [Bool])], + ibc_classes :: [(Name, ClassInfo)], + ibc_syntax :: [Syntax], + ibc_keywords :: [String], + ibc_objs :: [FilePath], + ibc_libs :: [String], + ibc_hdrs :: [String], + ibc_defs :: [(Name, Def)] } + +initIBC :: IBCFile +initIBC = IBCFile ibcVersion [] [] [] [] [] [] [] [] [] [] + +loadIBC :: FilePath -> Idris () +loadIBC fp = fail "Not implemented" + +writeIBC :: FilePath -> Idris () +writeIBC f + = do iLOG $ "Writing ibc " ++ show f + i <- getIState + case idris_metavars i \\ primDefs of + (_:_) -> fail "Can't write ibc when there are unsolve metavariables" + [] -> return () + return () + +$( derive makeBinary ''IBCFile ) +$( derive makeBinary ''PTerm ) +$( derive makeBinary ''Raw ) +$( derive makeBinary ''PTactic' ) +$( derive makeBinary ''PDo' ) +$( derive makeBinary ''PArg' ) +$( derive makeBinary ''ClassInfo ) +$( derive makeBinary ''Plicity ) +$( derive makeBinary ''FC ) +$( derive makeBinary ''Syntax ) +$( derive makeBinary ''SynContext ) +$( derive makeBinary ''SSymbol ) +$( derive makeBinary ''Static ) +$( derive makeBinary ''Fixity ) +$( derive makeBinary ''FixDecl ) + +$( derive makeBinary ''Def ) +$( derive makeBinary ''SC ) +$( derive makeBinary ''CaseAlt ) +$( derive makeBinary ''NameType ) +$( derive makeBinary ''Name ) +$( derive makeBinary ''Binder ) +$( derive makeBinary ''TT ) +$( derive makeBinary ''Const ) + +-- We need this for serialising Def. Fortunately, it never gets used because +-- we'll never serialise a primitive operator + +instance Binary (a -> b) where + put x = return () + get = undefined + +-- We assume that universe levels have been checked, so anything external +-- can just have the same universe variable and we won't get any new +-- cycles. + +instance Binary UExp where + put x = return () + get = return (UVar (-1)) + diff --git a/src/Idris/Imports.hs b/src/Idris/Imports.hs index e266d043c8..d067fbf32b 100644 --- a/src/Idris/Imports.hs +++ b/src/Idris/Imports.hs @@ -9,7 +9,7 @@ import System.FilePath import System.Directory import Control.Monad.State -data IFileType = IDR FilePath | IBC FilePath +data IFileType = IDR FilePath | IBC FilePath FilePath deriving Eq srcPath :: FilePath -> FilePath @@ -30,7 +30,7 @@ findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp) ibc <- doesFileExist (ibcPath ibcp) idr <- doesFileExist (srcPath idrp) if ibc - then return (IBC ibcp) + then return (IBC ibcp idrp) else if idr then return (IDR idrp) else findImport ds fp diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs index 10c6a53ee0..e8a41f8b63 100644 --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -5,6 +5,7 @@ import Idris.Imports import Idris.Error import Idris.ElabDecls import Idris.ElabTerm +import Idris.IBC import Paths_idris import Core.CoreParser @@ -59,7 +60,8 @@ loadModule f else do putIState (i { imported = f : imported i }) case fp of IDR fn -> loadSource fn - IBC fn -> error "Not implemented" + IBC fn src -> idrisCatch (loadIBC fn) + (\c -> loadSource src) let (dir, fh) = splitFileName f return (dropExtension fh)) (\e -> do let msg = report e @@ -72,6 +74,8 @@ loadSource f = do iLOG ("Reading " ++ f) file <- lift $ readFile f (mname, modules, rest, pos) <- parseImports f file mapM_ loadModule modules + clearIBC -- start a new .ibc file + mapM_ (\m -> addIBC (IBCImport m)) modules ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname }) f rest pos let ds = namespaces mname ds' @@ -82,6 +86,9 @@ loadSource f = do iLOG ("Reading " ++ f) -- Now add all the declarations to the context mapM_ (elabDecl toplevel) ds iLOG ("Finished " ++ f) + let ibc = dropExtension f ++ ".ibc" + idrisCatch (do writeIBC ibc; clearIBC) + (\c -> return ()) -- failure is harmless return () where namespaces [] ds = ds @@ -216,9 +223,12 @@ pSyntaxDecl syn i <- getState let rs = syntax_rules i let ns = syntax_keywords i + let ibc = ibc_write i let ks = map show (names s) setState (i { syntax_rules = s : rs, - syntax_keywords = ks ++ ns }) + syntax_keywords = ks ++ ns, + ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc + }) fc <- pfc return (PSyntax fc s) where @@ -312,7 +322,8 @@ pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',') istate <- getState let fs = map (Fix (f prec)) ops setState (istate { - idris_infixes = sort (fs ++ idris_infixes istate) }) + idris_infixes = sort (fs ++ idris_infixes istate), + ibc_write = map IBCFix fs ++ ibc_write istate }) fc <- pfc return (PFix fc (f prec) ops) @@ -785,13 +796,16 @@ pWhereblock n syn pDirective :: IParser [PDecl] pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit; - return [PDirective (addLib lib)]) + return [PDirective (do addLib lib + addIBC (IBCLib lib))]) <|> try (do lchar '%'; reserved "link"; obj <- strlit; return [PDirective (do datadir <- lift $ getDataDir o <- lift $ findInPath [".", datadir] obj + addIBC (IBCObj o) addObjectFile o)]) <|> try (do lchar '%'; reserved "include"; hdr <- strlit; - return [PDirective (addHdr hdr)]) + return [PDirective (do addHdr hdr + addIBC (IBCHeader hdr))]) <|> do lchar '%'; reserved "logging"; i <- natural; return [PDirective (setLogLevel (fromInteger i))]