Added some serialisation

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

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,

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;

src/Core/Evaluate.hs

@@ -2,14 +2,16 @@
              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,
                 Value(..)) where
 
 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,29 +453,28 @@ 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
 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,17 +497,17 @@ 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
 
 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,13 +518,12 @@ 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
   li n i []           = Nothing
   li n i ((x, b): xs) 
              | n == x = Just (i, binderTy b)
              | otherwise = li n (i+1) xs
-

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

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

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
 

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) 

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