Permalink
Browse files

Added some Data.Binary serialisation

Ignore-this: adc172dedf31a663dba8b1c112461f5f

darcs-hash:20091205182916-228f4-2ee4d78ecb870c21a4408cf09dddd796cc23cf71.gz
  • Loading branch information...
1 parent e7bc05f commit 975e1a8d100bf686c8a3a8aa6f7ac8e21c6b5140 eb committed Dec 5, 2009
Showing with 29 additions and 4 deletions.
  1. +2 −2 Ivor/TT.lhs
  2. +1 −0 Ivor/TTCore.lhs
  3. +25 −1 Ivor/ViewTerm.lhs
  4. +1 −1 ivor.cabal
View
@@ -792,8 +792,8 @@ Give a parseable but ugly representation of a term.
> -- |Reduce a term and its type to Normal Form (using new evaluator, reducing
> -- given names a maximum number of times)
> evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term
-> evalnewLimit (Ctxt st) (Term (tm,ty)) ns = Term (tidyNames (eval_nf_limit (defs st) tm ns),
-> tidyNames (eval_nf_limit (defs st) ty ns))
+> evalnewLimit (Ctxt st) (Term (tm,ty)) ns = Term (eval_nf_limit (defs st) tm ns,
+> eval_nf_limit (defs st) ty ns)
> -- |Check a term in the context of the given goal
> checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
View
@@ -9,6 +9,7 @@
> import Data.Char
> import Control.Monad.State
> import Data.Typeable
+> import Data.Binary hiding (get,put)
> import Debug.Trace
Raw terms are those read in directly from the user, and may be badly typed.
View
@@ -32,6 +32,8 @@
> import Data.Typeable
> import Data.List
+> import Data.Binary
+> import Control.Monad
> import Debug.Trace
> name :: String -> Name
@@ -52,7 +54,7 @@
> -- is for.
> data NameType = Bound | Free | DataCon | TypeCon | ElimOp
> | Unknown -- ^ Use for sending to typechecker.
-> deriving Show
+> deriving (Show, Enum)
> -- | Construct a term representing a variable
> mkVar :: String -- ^ Variable name
@@ -82,6 +84,8 @@
> data Annot = FileLoc FilePath Int -- ^ source file, line number
+
+
> instance Eq ViewTerm where
> (==) (Name _ x) (Name _ y) = x == y
> (==) (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') = f == f' && a == a'
@@ -380,3 +384,23 @@
> doTr x = case matchMeta lhs x of
> Just vars -> replaceMeta vars rhs
> Nothing -> x
+
+> instance Binary Name where
+> put (UN s) = do put (0 :: Word8); put s
+> put (MN s) = do put (1 :: Word8); put s
+
+> get = do tag <- getWord8
+> case tag of
+> 0 -> liftM UN get
+> 1 -> liftM MN get
+
+> instance Binary NameType where
+> put x = put (fromEnum x)
+> get = do t <- get
+> return (toEnum t)
+
+> instance Binary Annot where
+> put (FileLoc p i) = do put p; put i
+> get = do p <- get
+> i <- get
+> return (FileLoc p i)
View
@@ -58,7 +58,7 @@ Extra-source-files: emacs/ivor-mode.el, examplett/staged.tt, examplett/test.c, e
-Build-depends: base >=3 && <5, parsec, mtl, directory
+Build-depends: base >=3 && <5, parsec, mtl, directory, binary
Build-type: Simple
Extensions: MultiParamTypeClasses, FunctionalDependencies,

0 comments on commit 975e1a8

Please sign in to comment.