module Agda.TypeChecking.Serialise
( encode
, encodeFile
, decode
, decodeFile
, EmbPrj
)
where
import Control.Applicative
import qualified Control.Exception as E
import Control.Monad
import Control.Monad.Reader
import Control.Monad.State.Strict
import Control.Monad.Error
import Data.Array.IArray
import Data.Bits (shiftR)
import Data.Word
import Data.ByteString.Lazy as L
import Data.Hashable
import qualified Data.HashTable.IO as H
import Data.Int (Int32, Int64)
import Data.IORef
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import qualified Data.Binary as B
import qualified Data.Binary.Get as B
import qualified Data.List as List
import Data.Function
import Data.Typeable
import qualified Codec.Compression.GZip as G
import qualified Agda.Compiler.Epic.Interface as Epic
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name as C
import Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Scope.Base
import Agda.Syntax.Position (Position(..), Range)
import qualified Agda.Syntax.Position as P
import Agda.Syntax.Common
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Literal
import qualified Agda.Compiler.JS.Syntax as JS
import qualified Agda.Interaction.Highlighting.Range as HR
import qualified Agda.Interaction.Highlighting.Precise as HP
import Agda.Interaction.FindFile
import Agda.TypeChecking.Monad
import Agda.TypeChecking.CompiledClause
import Agda.Utils.FileName
import Agda.Utils.Monad
import Agda.Utils.Tuple
import Agda.Utils.Permutation
#include "../undefined.h"
import Agda.Utils.Impossible
currentInterfaceVersion :: Word64
currentInterfaceVersion = 20111026 * 10 + 0
type Node = [Int32]
type HashTable k v = H.BasicHashTable k v
data Dict = Dict{ nodeD :: !(HashTable Node Int32)
, stringD :: !(HashTable String Int32)
, integerD :: !(HashTable Integer Int32)
, doubleD :: !(HashTable Double Int32)
, nodeC :: !(IORef Int32)
, stringC :: !(IORef Int32)
, integerC :: !(IORef Int32)
, doubleC :: !(IORef Int32)
, fileMod :: !SourceToModule
}
data U = forall a . Typeable a => U !a
type Memo = HashTable (Int32, TypeRep') U
newtype TypeRep' = TypeRep' { unTypeRep' :: TypeRep }
deriving Eq
instance Hashable TypeRep' where
hash = hash . show . unTypeRep'
data St = St
{ nodeE :: !(Array Int32 Node)
, stringE :: !(Array Int32 String)
, integerE :: !(Array Int32 Integer)
, doubleE :: !(Array Int32 Double)
, nodeMemo :: !Memo
, modFile :: !ModuleToSource
, includes :: [AbsolutePath]
}
type S a = ReaderT Dict IO a
type R a = ErrorT TypeError (StateT St IO) a
malformed :: R a
malformed = throwError $ GenericError "Malformed input."
class Typeable a => EmbPrj a where
icode :: a -> S Int32
value :: Int32 -> R a
encode :: EmbPrj a => a -> TCM ByteString
encode a = do
fileMod <- sourceToModule
liftIO $ do
newD@(Dict nD sD iD dD _ _ _ _ _) <- emptyDict fileMod
root <- runReaderT (icode a) newD
nL <- l nD; sL <- l sD; iL <- l iD; dL <- l dD
return $ B.encode currentInterfaceVersion `L.append`
G.compress (B.encode (root, nL, sL, iL, dL))
where
l h = List.map fst . List.sortBy (compare `on` snd) <$> H.toList h
decode :: EmbPrj a => ByteString -> TCM (Maybe a)
decode s = do
mf <- stModuleToSource <$> get
incs <- getIncludeDirs
(mf, x) <- liftIO $ E.handle (\(E.ErrorCall {}) -> noResult) $ do
(ver, s, _) <- return $ B.runGetState B.get s 0
if ver /= currentInterfaceVersion
then noResult
else do
((r, nL, sL, iL, dL), s, _) <-
return $ B.runGetState B.get (G.decompress s) 0
if s /= L.empty
then noResult
else do
st <- St (ar nL) (ar sL) (ar iL) (ar dL)
<$> liftIO H.new
<*> return mf <*> return incs
(r, st) <- runStateT (runErrorT (value r)) st
return (Just (modFile st), case r of
Left _ -> Nothing
Right x -> Just x)
case mf of
Nothing -> return ()
Just mf -> modify $ \s -> s { stModuleToSource = mf }
return x
where
ar l = listArray (0, List.genericLength l 1) l
noResult = return (Nothing, Nothing)
encodeFile :: EmbPrj a
=> FilePath
-> a
-> TCM ()
encodeFile f x = liftIO . L.writeFile f =<< encode x
decodeFile :: EmbPrj a => FilePath -> TCM (Maybe a)
decodeFile f = decode =<< liftIO (L.readFile f)
instance EmbPrj String where
icode = icodeX stringD stringC
value i = (! i) `fmap` gets stringE
instance EmbPrj Integer where
icode = icodeX integerD integerC
value i = (! i) `fmap` gets integerE
instance EmbPrj Int32 where
icode i = return i
value i = return i
instance EmbPrj Int where
icode i = return (fromIntegral i)
value i = return (fromIntegral i)
instance EmbPrj Char where
icode c = return (fromIntegral $ fromEnum c)
value i = return (toEnum $ fromInteger $ toInteger i)
instance EmbPrj Double where
icode = icodeX doubleD doubleC
value i = (! i) `fmap` gets doubleE
instance EmbPrj () where
icode () = icode0'
value = vcase valu where valu [] = valu0 ()
valu _ = malformed
instance (EmbPrj a, EmbPrj b) => EmbPrj (a, b) where
icode (a, b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 (,) a b
valu _ = malformed
instance (EmbPrj a, EmbPrj b, EmbPrj c) => EmbPrj (a, b, c) where
icode (a, b, c) = icode3' a b c
value = vcase valu where valu [a, b, c] = valu3 (,,) a b c
valu _ = malformed
instance EmbPrj a => EmbPrj (Maybe a) where
icode Nothing = icode0'
icode (Just x) = icode1' x
value = vcase valu where valu [] = valu0 Nothing
valu [x] = valu1 Just x
valu _ = malformed
instance EmbPrj Bool where
icode True = icode0'
icode False = icode0 0
value = vcase valu where valu [] = valu0 True
valu [0] = valu0 False
valu _ = malformed
instance EmbPrj AbsolutePath where
icode file = do
mm <- M.lookup file . fileMod <$> ask
case mm of
Just m -> icode m
Nothing -> __IMPOSSIBLE__
value m = do
m <- value m
mf <- modFile <$> get
incs <- includes <$> get
(r, mf) <- liftIO $ findFile'' incs m mf
modify $ \s -> s { modFile = mf }
case r of
Left err -> throwError $ findErrorToTypeError m err
Right f -> return f
instance EmbPrj Position where
icode (P.Pn file pos line col) = icode4' file pos line col
value = vcase valu
where
valu [f, p, l, c] = valu4 P.Pn f p l c
valu _ = malformed
instance EmbPrj TopLevelModuleName where
icode (TopLevelModuleName a) = icode1' a
value = vcase valu where valu [a] = valu1 TopLevelModuleName a
valu _ = malformed
instance EmbPrj a => EmbPrj [a] where
icode xs = icodeN =<< mapM icode xs
value = vcase (mapM value)
instance (Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Map a b) where
icode m = icode (M.toList m)
value m = M.fromList `fmap` value m
instance (Ord a, EmbPrj a) => EmbPrj (Set a) where
icode s = icode (S.toList s)
value s = S.fromList `fmap` value s
instance EmbPrj P.Interval where
icode (P.Interval p q) = icode2' p q
value = vcase valu where valu [p, q] = valu2 P.Interval p q
valu _ = malformed
instance EmbPrj Range where
icode (P.Range is) = icode1' is
value = vcase valu where valu [is] = valu1 P.Range is
valu _ = malformed
instance EmbPrj HR.Range where
icode (HR.Range a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 HR.Range a b
valu _ = malformed
instance EmbPrj C.Name where
icode (C.NoName a b) = icode2 0 a b
icode (C.Name r xs) = icode2' r xs
value = vcase valu where valu [0, a, b] = valu2 C.NoName a b
valu [r, xs] = valu2 C.Name r xs
valu _ = malformed
instance EmbPrj NamePart where
icode Hole = icode0'
icode (Id a) = icode1' a
value = vcase valu where valu [] = valu0 Hole
valu [a] = valu1 Id a
valu _ = malformed
instance EmbPrj C.QName where
icode (Qual a b) = icode2' a b
icode (C.QName a ) = icode1' a
value = vcase valu where valu [a, b] = valu2 Qual a b
valu [a] = valu1 C.QName a
valu _ = malformed
instance EmbPrj Scope where
icode (Scope a b c d) = icode4' a b c d
value = vcase valu where valu [a, b, c, d] = valu4 Scope a b c d
valu _ = malformed
instance EmbPrj NameSpaceId where
icode PublicNS = icode0'
icode PrivateNS = icode0 1
icode ImportedNS = icode0 2
icode OnlyQualifiedNS = icode0 3
value = vcase valu where valu [] = valu0 PublicNS
valu [1] = valu0 PrivateNS
valu [2] = valu0 ImportedNS
valu [3] = valu0 OnlyQualifiedNS
valu _ = malformed
instance EmbPrj Access where
icode PrivateAccess = icode0 0
icode PublicAccess = icode0'
icode OnlyQualified = icode0 2
value = vcase valu where valu [0] = valu0 PrivateAccess
valu [] = valu0 PublicAccess
valu [2] = valu0 OnlyQualified
valu _ = malformed
instance EmbPrj NameSpace where
icode (NameSpace a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 NameSpace a b
valu _ = malformed
instance EmbPrj AbstractName where
icode (AbsName a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 AbsName a b
valu _ = malformed
instance EmbPrj AbstractModule where
icode (AbsModule a) = icode a
value n = AbsModule `fmap` value n
instance EmbPrj KindOfName where
icode DefName = icode0'
icode ConName = icode0 1
value = vcase valu where valu [] = valu0 DefName
valu [1] = valu0 ConName
valu _ = malformed
instance EmbPrj Agda.Syntax.Fixity.Fixity where
icode (LeftAssoc a b) = icode2 0 a b
icode (RightAssoc a b) = icode2 1 a b
icode (NonAssoc a b) = icode2' a b
value = vcase valu where valu [0, a, b] = valu2 LeftAssoc a b
valu [1, a, b] = valu2 RightAssoc a b
valu [a, b] = valu2 NonAssoc a b
valu _ = malformed
instance EmbPrj Agda.Syntax.Fixity.Fixity' where
icode (Fixity' a b) = icode2' a b
value = vcase valu where valu [a,b] = valu2 Fixity' a b
valu _ = malformed
instance EmbPrj GenPart where
icode (BindHole a) = icode1 0 a
icode (NormalHole a) = icode1 1 a
icode (IdPart a) = icode1' a
value = vcase valu where valu [0, a] = valu1 BindHole a
valu [1, a] = valu1 NormalHole a
valu [a] = valu1 IdPart a
valu _ = malformed
instance EmbPrj A.QName where
icode (A.QName a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 A.QName a b
valu _ = malformed
instance EmbPrj A.ModuleName where
icode (A.MName a) = icode a
value n = A.MName `fmap` value n
instance EmbPrj A.Name where
icode (A.Name a b c d) = icode4' a b c d
value = vcase valu where valu [a, b, c, d] = valu4 A.Name a b c d
valu _ = malformed
instance EmbPrj NameId where
icode (NameId a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 NameId a b
valu _ = malformed
instance EmbPrj Signature where
icode (Sig a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 Sig a b
valu _ = malformed
instance EmbPrj Section where
icode (Section a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 Section a b
valu _ = malformed
instance EmbPrj Telescope where
icode EmptyTel = icode0'
icode (ExtendTel a b) = icode2' a b
value = vcase valu where valu [] = valu0 EmptyTel
valu [a, b] = valu2 ExtendTel a b
valu _ = malformed
instance EmbPrj Permutation where
icode (Perm a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 Perm a b
valu _ = malformed
instance (EmbPrj a) => EmbPrj (Agda.Syntax.Common.Arg a) where
icode (Arg a b c) = icode3' a b c
value = vcase valu where valu [a, b, c] = valu3 Arg a b c
valu _ = malformed
instance EmbPrj Agda.Syntax.Common.Induction where
icode Inductive = icode0'
icode CoInductive = icode0 1
value = vcase valu where valu [] = valu0 Inductive
valu [1] = valu0 CoInductive
valu _ = malformed
instance EmbPrj Agda.Syntax.Common.Hiding where
icode Hidden = icode0 0
icode NotHidden = icode0'
icode Instance = icode0 2
value = vcase valu where valu [0] = valu0 Hidden
valu [] = valu0 NotHidden
valu [2] = valu0 Instance
valu _ = malformed
instance EmbPrj Agda.Syntax.Common.Relevance where
icode Relevant = icode0'
icode Irrelevant = icode0 1
icode Forced = icode0 2
icode NonStrict = icode0 3
value = vcase valu where valu [] = valu0 Relevant
valu [1] = valu0 Irrelevant
valu [2] = valu0 Forced
valu [3] = valu0 NonStrict
valu _ = malformed
instance EmbPrj I.Type where
icode (El a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 El a b
valu _ = malformed
instance (EmbPrj a) => EmbPrj (I.Abs a) where
icode (NoAbs a b) = icode2 0 a b
icode (Abs a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 Abs a b
valu [0, a, b] = valu2 NoAbs a b
valu _ = malformed
instance EmbPrj I.Term where
icode (Var a b) = icode2 0 a b
icode (Lam a b) = icode2 1 a b
icode (Lit a ) = icode1 2 a
icode (Def a b) = icode2 3 a b
icode (Con a b) = icode2 4 a b
icode (Pi a b) = icode2 5 a b
icode (Sort a ) = icode1 7 a
icode (MetaV a b) = __IMPOSSIBLE__
icode (DontCare a ) = icode1 8 a
icode (Level a ) = icode1 9 a
value = vcase valu where valu [0, a, b] = valu2 Var a b
valu [1, a, b] = valu2 Lam a b
valu [2, a] = valu1 Lit a
valu [3, a, b] = valu2 Def a b
valu [4, a, b] = valu2 Con a b
valu [5, a, b] = valu2 Pi a b
valu [7, a] = valu1 Sort a
valu [8, a] = valu1 DontCare a
valu [9, a] = valu1 Level a
valu _ = malformed
instance EmbPrj Level where
icode (Max a) = icode1' a
value = vcase valu where valu [a] = valu1 Max a
valu _ = malformed
instance EmbPrj PlusLevel where
icode (ClosedLevel a) = icode1' a
icode (Plus a b) = icode2' a b
value = vcase valu where valu [a] = valu1 ClosedLevel a
valu [a, b] = valu2 Plus a b
valu _ = malformed
instance EmbPrj LevelAtom where
icode (NeutralLevel a) = icode1' a
icode (UnreducedLevel a) = icode1 1 a
icode MetaLevel{} = __IMPOSSIBLE__
icode BlockedLevel{} = __IMPOSSIBLE__
value = vcase valu where valu [a] = valu1 NeutralLevel a
valu [1, a] = valu1 UnreducedLevel a
valu _ = malformed
instance EmbPrj I.Sort where
icode (Type a ) = icode1' a
icode Prop = icode1 1 ()
icode Inf = icode1 4 ()
icode (DLub a b) = __IMPOSSIBLE__
value = vcase valu where valu [a] = valu1 Type a
valu [1, _] = valu0 Prop
valu [4, _] = valu0 Inf
valu _ = malformed
instance EmbPrj Agda.Syntax.Literal.Literal where
icode (LitInt a b) = icode2' a b
icode (LitFloat a b) = icode2 1 a b
icode (LitString a b) = icode2 2 a b
icode (LitChar a b) = icode2 3 a b
icode (LitQName a b) = icode2 5 a b
value = vcase valu where valu [a, b] = valu2 LitInt a b
valu [1, a, b] = valu2 LitFloat a b
valu [2, a, b] = valu2 LitString a b
valu [3, a, b] = valu2 LitChar a b
valu [5, a, b] = valu2 LitQName a b
valu _ = malformed
instance EmbPrj DisplayForm where
icode (Display a b c) = icode3' a b c
value = vcase valu where valu [a, b, c] = valu3 Display a b c
valu _ = malformed
instance EmbPrj a => EmbPrj (Open a) where
icode (OpenThing a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 OpenThing a b
valu _ = malformed
instance EmbPrj CtxId where
icode (CtxId a) = icode a
value n = CtxId `fmap` value n
instance EmbPrj DisplayTerm where
icode (DTerm a ) = icode1' a
icode (DDot a ) = icode1 1 a
icode (DCon a b) = icode2 2 a b
icode (DDef a b) = icode2 3 a b
icode (DWithApp a b) = icode2 4 a b
value = vcase valu where valu [a] = valu1 DTerm a
valu [1, a] = valu1 DDot a
valu [2, a, b] = valu2 DCon a b
valu [3, a, b] = valu2 DDef a b
valu [4, a, b] = valu2 DWithApp a b
valu _ = malformed
instance EmbPrj MutualId where
icode (MutId a) = icode a
value n = MutId `fmap` value n
instance EmbPrj Definition where
icode (Defn rel a b c d e f) = icode7' rel a b c d e f
value = vcase valu where valu [rel, a, b, c, d, e, f] = valu7 Defn rel a b c d e f
valu _ = malformed
instance EmbPrj HaskellRepresentation where
icode (HsType a) = icode1' a
icode (HsDefn a b) = icode2' a b
value = vcase valu where
valu [a] = valu1 HsType a
valu [a, b] = valu2 HsDefn a b
valu _ = malformed
instance EmbPrj JS.Exp where
icode (JS.Self) = icode0 0
icode (JS.Local i) = icode1 1 i
icode (JS.Global i) = icode1 2 i
icode (JS.Undefined) = icode0 3
icode (JS.String s) = icode1 4 s
icode (JS.Char c) = icode1 5 c
icode (JS.Integer n) = icode1 6 n
icode (JS.Double d) = icode1 7 d
icode (JS.Lambda n e) = icode2 8 n e
icode (JS.Object o) = icode1 9 o
icode (JS.Apply e es) = icode2 10 e es
icode (JS.Lookup e l) = icode2 11 e l
icode (JS.If e f g) = icode3 12 e f g
icode (JS.BinOp e op f) = icode3 13 e op f
icode (JS.PreOp op e) = icode2 14 op e
icode (JS.Const i) = icode1 15 i
value = vcase valu where valu [0] = valu0 JS.Self
valu [1, a] = valu1 JS.Local a
valu [2, a] = valu1 JS.Global a
valu [3] = valu0 JS.Undefined
valu [4, a] = valu1 JS.String a
valu [5, a] = valu1 JS.Char a
valu [6, a] = valu1 JS.Integer a
valu [7, a] = valu1 JS.Double a
valu [8, a, b] = valu2 JS.Lambda a b
valu [9, a] = valu1 JS.Object a
valu [10, a, b] = valu2 JS.Apply a b
valu [11, a, b] = valu2 JS.Lookup a b
valu [12, a, b, c] = valu3 JS.If a b c
valu [13, a, b, c] = valu3 JS.BinOp a b c
valu [14, a, b] = valu2 JS.PreOp a b
valu [15, a] = valu1 JS.Const a
valu _ = malformed
instance EmbPrj JS.LocalId where
icode (JS.LocalId l) = icode l
value n = JS.LocalId `fmap` value n
instance EmbPrj JS.GlobalId where
icode (JS.GlobalId l) = icode l
value n = JS.GlobalId `fmap` value n
instance EmbPrj JS.MemberId where
icode (JS.MemberId l) = icode l
value n = JS.MemberId `fmap` value n
instance EmbPrj Polarity where
icode Covariant = icode0'
icode Contravariant = icode0 1
icode Invariant = icode0 2
value = vcase valu where
valu [] = valu0 Covariant
valu [1] = valu0 Contravariant
valu [2] = valu0 Invariant
valu _ = malformed
instance EmbPrj Occurrence where
icode Positive = icode0'
icode Negative = icode0 1
icode Unused = icode0 2
value = vcase valu where
valu [] = valu0 Positive
valu [1] = valu0 Negative
valu [2] = valu0 Unused
valu _ = malformed
instance EmbPrj CompiledRepresentation where
icode (CompiledRep a b c) = icode3' a b c
value = vcase valu where valu [a, b, c] = valu3 CompiledRep a b c
valu _ = malformed
instance EmbPrj Defn where
icode Axiom = icode0 0
icode (Function a b c d e f g h i) = icode9 1 a b c d e f g h i
icode (Datatype a b c d e f g h i) = icode9 2 a b c d e f g h i
icode (Record a b c d e f g h i j k) = icode11 3 a b c d e f g h i j k
icode (Constructor a b c d e) = icode5 4 a b c d e
icode (Primitive a b c d) = icode4 5 a b c d
value = vcase valu where
valu [0] = valu0 Axiom
valu [1, a, b, c, d, e, f, g, h, i] = valu9 Function a b c d e f g h i
valu [2, a, b, c, d, e, f, g, h, i] = valu9 Datatype a b c d e f g h i
valu [3, a, b, c, d, e, f, g, h, i, j, k] = valu11 Record a b c d e f g h i j k
valu [4, a, b, c, d, e] = valu5 Constructor a b c d e
valu [5, a, b, c, d] = valu4 Primitive a b c d
valu _ = malformed
instance EmbPrj a => EmbPrj (Case a) where
icode (Branches a b c) = icode3' a b c
value = vcase valu where
valu [a, b, c] = valu3 Branches a b c
valu _ = malformed
instance EmbPrj CompiledClauses where
icode Fail = icode0'
icode (Done a b) = icode2' a b
icode (Case a b) = icode2 2 a b
value = vcase valu where
valu [] = valu0 Fail
valu [a, b] = valu2 Done a b
valu [2, a, b] = valu2 Case a b
valu _ = malformed
instance EmbPrj FunctionInverse where
icode NotInjective = icode0'
icode (Inverse a) = icode1' a
value = vcase valu where valu [] = valu0 NotInjective
valu [a] = valu1 Inverse a
valu _ = malformed
instance EmbPrj TermHead where
icode SortHead = icode0'
icode PiHead = icode0 1
icode (ConHead a) = icode1 2 a
value = vcase valu where valu [] = valu0 SortHead
valu [1] = valu0 PiHead
valu [2, a] = valu1 ConHead a
valu _ = malformed
instance EmbPrj Agda.Syntax.Common.IsAbstract where
icode AbstractDef = icode0 0
icode ConcreteDef = icode0'
value = vcase valu where valu [0] = valu0 AbstractDef
valu [] = valu0 ConcreteDef
valu _ = malformed
instance EmbPrj I.Clause where
icode (Clause a b c d e) = icode5' a b c d e
value = vcase valu where valu [a, b, c, d, e] = valu5 Clause a b c d e
valu _ = malformed
instance EmbPrj I.ClauseBody where
icode (Body a) = icode1 0 a
icode (Bind a) = icode1' a
icode NoBody = icode0'
value = vcase valu where valu [0, a] = valu1 Body a
valu [a] = valu1 Bind a
valu [] = valu0 NoBody
valu _ = malformed
instance EmbPrj Delayed where
icode Delayed = icode0 0
icode NotDelayed = icode0'
value = vcase valu where valu [0] = valu0 Delayed
valu [] = valu0 NotDelayed
valu _ = malformed
instance EmbPrj I.Pattern where
icode (VarP a ) = icode1' a
icode (ConP a b c) = icode3' a b c
icode (LitP a ) = icode1 2 a
icode (DotP a ) = icode1 3 a
value = vcase valu where valu [a] = valu1 VarP a
valu [a, b, c] = valu3 ConP a b c
valu [2, a] = valu1 LitP a
valu [3, a] = valu1 DotP a
valu _ = malformed
instance EmbPrj a => EmbPrj (Builtin a) where
icode (Prim a) = icode1' a
icode (Builtin a) = icode1 1 a
value = vcase valu where valu [a] = valu1 Prim a
valu [1, a] = valu1 Builtin a
valu _ = malformed
instance EmbPrj HP.NameKind where
icode HP.Bound = icode0'
icode (HP.Constructor a) = icode1 1 a
icode HP.Datatype = icode0 2
icode HP.Field = icode0 3
icode HP.Function = icode0 4
icode HP.Module = icode0 5
icode HP.Postulate = icode0 6
icode HP.Primitive = icode0 7
icode HP.Record = icode0 8
value = vcase valu where
valu [] = valu0 HP.Bound
valu [1 , a] = valu1 HP.Constructor a
valu [2] = valu0 HP.Datatype
valu [3] = valu0 HP.Field
valu [4] = valu0 HP.Function
valu [5] = valu0 HP.Module
valu [6] = valu0 HP.Postulate
valu [7] = valu0 HP.Primitive
valu [8] = valu0 HP.Record
valu _ = malformed
instance EmbPrj HP.Aspect where
icode HP.Comment = icode0 0
icode HP.Keyword = icode0 1
icode HP.String = icode0 2
icode HP.Number = icode0 3
icode HP.Symbol = icode0'
icode HP.PrimitiveType = icode0 5
icode (HP.Name mk b) = icode2 6 mk b
value = vcase valu where
valu [0] = valu0 HP.Comment
valu [1] = valu0 HP.Keyword
valu [2] = valu0 HP.String
valu [3] = valu0 HP.Number
valu [] = valu0 HP.Symbol
valu [5] = valu0 HP.PrimitiveType
valu [6, mk, b] = valu2 HP.Name mk b
valu _ = malformed
instance EmbPrj HP.OtherAspect where
icode HP.Error = icode0 0
icode HP.DottedPattern = icode0'
icode HP.UnsolvedMeta = icode0 2
icode HP.TerminationProblem = icode0 3
icode HP.IncompletePattern = icode0 4
value = vcase valu where
valu [0] = valu0 HP.Error
valu [] = valu0 HP.DottedPattern
valu [2] = valu0 HP.UnsolvedMeta
valu [3] = valu0 HP.TerminationProblem
valu [4] = valu0 HP.IncompletePattern
valu _ = malformed
instance EmbPrj HP.MetaInfo where
icode (HP.MetaInfo a b c d) = icode4' a b c d
value = vcase valu where
valu [a, b, c, d] = valu4 HP.MetaInfo a b c d
valu _ = malformed
instance EmbPrj Precedence where
icode TopCtx = icode0'
icode FunctionSpaceDomainCtx = icode0 1
icode (LeftOperandCtx a) = icode1 2 a
icode (RightOperandCtx a) = icode1 3 a
icode FunctionCtx = icode0 4
icode ArgumentCtx = icode0 5
icode InsideOperandCtx = icode0 6
icode WithFunCtx = icode0 7
icode WithArgCtx = icode0 8
icode DotPatternCtx = icode0 9
value = vcase valu
where
valu [] = valu0 TopCtx
valu [1] = valu0 FunctionSpaceDomainCtx
valu [2, a] = valu1 LeftOperandCtx a
valu [3, a] = valu1 RightOperandCtx a
valu [4] = valu0 FunctionCtx
valu [5] = valu0 ArgumentCtx
valu [6] = valu0 InsideOperandCtx
valu [7] = valu0 WithFunCtx
valu [8] = valu0 WithArgCtx
valu [9] = valu0 DotPatternCtx
valu _ = malformed
instance EmbPrj ScopeInfo where
icode (ScopeInfo a b c d) = icode4' a b c d
value = vcase valu where valu [a, b, c, d] = valu4 ScopeInfo a b c d
valu _ = malformed
instance EmbPrj Interface where
icode (Interface a b c d e f g h i) = icode9' a b c d e f g h i
value = vcase valu where valu [a, b, c, d, e, f, g, h, i] = valu9 Interface a b c d e f g h i
valu _ = malformed
instance EmbPrj Epic.EInterface where
icode (Epic.EInterface a b c d e f g h) = icode8' a b c d e f g h
value = vcase valu where
valu [a, b, c, d, e, f, g, h] = valu8 Epic.EInterface a b c d e f g h
valu _ = malformed
instance EmbPrj Epic.InjectiveFun where
icode (Epic.InjectiveFun a b) = icode2' a b
value = vcase valu where
valu [a,b] = valu2 Epic.InjectiveFun a b
valu _ = malformed
instance EmbPrj Epic.Relevance where
icode Epic.Irr = icode0 0
icode Epic.Rel = icode0 1
value = vcase valu where valu [0] = valu0 Epic.Irr
valu [1] = valu0 Epic.Rel
valu _ = malformed
instance EmbPrj Epic.Forced where
icode Epic.Forced = icode0 0
icode Epic.NotForced = icode0 1
value = vcase valu where valu [0] = valu0 Epic.Forced
valu [1] = valu0 Epic.NotForced
valu _ = malformed
instance EmbPrj Epic.Tag where
icode (Epic.Tag a) = icode1 0 a
icode (Epic.PrimTag a) = icode1 1 a
value = vcase valu
where
valu [0, a] = valu1 Epic.Tag a
valu [1, a] = valu1 Epic.PrimTag a
valu _ = malformed
icodeX :: (Eq k, Hashable k) =>
(Dict -> HashTable k Int32) -> (Dict -> IORef Int32) ->
k -> S Int32
icodeX dict counter key = do
d <- asks dict
c <- asks counter
liftIO $ do
mi <- H.lookup d key
case mi of
Just i -> return i
Nothing -> do
fresh <- readIORef c
H.insert d key fresh
writeIORef c $! fresh + 1
return fresh
icodeN :: [Int32] -> S Int32
icodeN = icodeX nodeD nodeC
vcase :: forall a . EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase valu = \ix -> do
memo <- gets nodeMemo
(aTyp, maybeU) <- liftIO $ do
let aTyp = TypeRep' $ typeOf (undefined :: a)
maybeU <- H.lookup memo (ix, aTyp)
return (aTyp, maybeU)
case maybeU of
Just (U u) -> maybe malformed return (cast u)
Nothing -> do
v <- valu . (! ix) =<< gets nodeE
liftIO $ H.insert memo (ix, aTyp) (U v)
return v
icode0 tag = icodeN [tag]
icode1 tag a = icodeN . (tag :) =<< sequence [icode a]
icode2 tag a b = icodeN . (tag :) =<< sequence [icode a, icode b]
icode3 tag a b c = icodeN . (tag :) =<< sequence [icode a, icode b, icode c]
icode4 tag a b c d = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d]
icode5 tag a b c d e = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e]
icode6 tag a b c d e f = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f]
icode7 tag a b c d e f g = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g]
icode8 tag a b c d e f g h = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h]
icode9 tag a b c d e f g h i = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i]
icode10 tag a b c d e f g h i j = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j]
icode11 tag a b c d e f g h i j k = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j, icode k]
icode12 tag a b c d e f g h i j k l = icodeN . (tag :) =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j, icode k, icode l]
icode0' = icodeN []
icode1' a = icodeN =<< sequence [icode a]
icode2' a b = icodeN =<< sequence [icode a, icode b]
icode3' a b c = icodeN =<< sequence [icode a, icode b, icode c]
icode4' a b c d = icodeN =<< sequence [icode a, icode b, icode c, icode d]
icode5' a b c d e = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e]
icode6' a b c d e f = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f]
icode7' a b c d e f g = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g]
icode8' a b c d e f g h = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h]
icode9' a b c d e f g h i = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i]
icode10' a b c d e f g h i j = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j]
icode11' a b c d e f g h i j k = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j, icode k]
icode12' a b c d e f g h i j k l = icodeN =<< sequence [icode a, icode b, icode c, icode d, icode e, icode f, icode g, icode h, icode i, icode j, icode k, icode l]
valu0 z = return z
valu1 z a = valu0 z `ap` value a
valu2 z a b = valu1 z a `ap` value b
valu3 z a b c = valu2 z a b `ap` value c
valu4 z a b c d = valu3 z a b c `ap` value d
valu5 z a b c d e = valu4 z a b c d `ap` value e
valu6 z a b c d e f = valu5 z a b c d e `ap` value f
valu7 z a b c d e f g = valu6 z a b c d e f `ap` value g
valu8 z a b c d e f g h = valu7 z a b c d e f g `ap` value h
valu9 z a b c d e f g h i = valu8 z a b c d e f g h `ap` value i
valu10 z a b c d e f g h i j = valu9 z a b c d e f g h i `ap` value j
valu11 z a b c d e f g h i j k = valu10 z a b c d e f g h i j `ap` value k
valu12 z a b c d e f g h i j k l = valu11 z a b c d e f g h i j k `ap` value l
emptyDict :: SourceToModule
-> IO Dict
emptyDict fileMod = Dict
<$> H.new
<*> H.new
<*> H.new
<*> H.new
<*> newIORef 0
<*> newIORef 0
<*> newIORef 0
<*> newIORef 0
<*> return fileMod