module Agda.TypeChecking.Serialise
( encode
, encodeFile
, decode
, decodeFile
, EmbPrj
)
where
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.HashTable (HashTable)
import qualified Data.HashTable 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 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.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 = 20110217 * 10 + 0
type Node = [Int32]
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, Int32) U
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 = fmap (List.map fst . List.sortBy (compare `on` snd)) . H.toList
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 (==) hashInt2)
<*> 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 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 0
icode False = icode0 1
value = vcase valu where valu [0] = valu0 True
valu [1] = 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 1 r xs
value = vcase valu where valu [0, a, b] = valu2 C.NoName a b
valu [1, 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 e f) = icode6' a b c d e f
value = vcase valu where valu [a, b, c, d, e, f] = valu6 Scope a b c d e f
valu _ = malformed
instance EmbPrj Access where
icode PrivateAccess = icode0 0
icode PublicAccess = icode0 1
value = vcase valu where valu [0] = valu0 PrivateAccess
valu [1] = valu0 PublicAccess
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 0
icode ConName = icode0 1
value = vcase valu where valu [0] = 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 2 a b
value = vcase valu where valu [0, a, b] = valu2 LeftAssoc a b
valu [1, a, b] = valu2 RightAssoc a b
valu [2, 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 2 a
value = vcase valu where valu [0, a] = valu1 BindHole a
valu [1, a] = valu1 NormalHole a
valu [2, 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 0
icode CoInductive = icode0 1
value = vcase valu where valu [0] = valu0 Inductive
valu [1] = valu0 CoInductive
valu _ = malformed
instance EmbPrj Agda.Syntax.Common.Hiding where
icode Hidden = icode0 0
icode NotHidden = icode0 1
value = vcase valu where valu [0] = valu0 Hidden
valu [1] = valu0 NotHidden
valu _ = malformed
instance EmbPrj Agda.Syntax.Common.Relevance where
icode Relevant = icode0 0
icode Irrelevant = icode0 1
icode Forced = icode0 2
value = vcase valu where valu [0] = valu0 Relevant
valu [1] = valu0 Irrelevant
valu [2] = valu0 Forced
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 (Abs a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 Abs 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 (Fun a b) = icode2 6 a b
icode (Sort a ) = icode1 7 a
icode (MetaV a b) = __IMPOSSIBLE__
icode (DontCare ) = icode0 8
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 [6, a, b] = valu2 Fun a b
valu [7, a] = valu1 Sort a
valu [8] = valu0 DontCare
valu _ = malformed
instance EmbPrj I.Sort where
icode (Type a ) = icode1 0 a
icode Prop = icode0 1
icode (Lub a b) = icode2 2 a b
icode (Suc a ) = icode1 3 a
icode (MetaS a b) = __IMPOSSIBLE__
icode Inf = icode0 4
icode (DLub a b) = icode2 5 a b
value = vcase valu where valu [0, a] = valu1 Type a
valu [1] = valu0 Prop
valu [2, a, b] = valu2 Lub a b
valu [3, a] = valu1 Suc a
valu [4] = valu0 Inf
valu [5, a, b] = valu2 DLub a b
valu _ = malformed
instance EmbPrj Agda.Syntax.Literal.Literal where
icode (LitInt a b) = icode2 0 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 (LitLevel a b) = icode2 4 a b
icode (LitQName a b) = icode2 5 a b
value = vcase valu where valu [0, 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 [4, a, b] = valu2 LitLevel 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 (DWithApp a b) = icode2' a b
value = vcase valu where valu [a] = valu1 DTerm a
valu [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) = icode6' rel a b c d e
value = vcase valu where valu [rel, a, b, c, d, e] = valu6 Defn rel a b c d e
valu _ = malformed
instance EmbPrj HaskellRepresentation where
icode (HsType a) = icode1 0 a
icode (HsDefn a b) = icode2 1 a b
value = vcase valu where
valu [0, a] = valu1 HsType a
valu [1, a, b] = valu2 HsDefn a b
valu _ = malformed
instance EmbPrj Polarity where
icode Covariant = icode0 0
icode Contravariant = icode0 1
icode Invariant = icode0 2
value = vcase valu where
valu [0] = valu0 Covariant
valu [1] = valu0 Contravariant
valu [2] = valu0 Invariant
valu _ = malformed
instance EmbPrj Occurrence where
icode Positive = icode0 0
icode Negative = icode0 1
icode Unused = icode0 2
value = vcase valu where
valu [0] = valu0 Positive
valu [1] = valu0 Negative
valu [2] = valu0 Unused
valu _ = malformed
instance EmbPrj Defn where
icode (Axiom a b) = icode2 0 a b
icode (Function a b c d e f g h) = icode8 1 a b c d e f g h
icode (Datatype a b c d e f g h i j) = icode10 2 a b c d e f g h i j
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 f) = icode6 4 a b c d e f
icode (Primitive a b c d) = icode4 5 a b c d
value = vcase valu where
valu [0, a, b] = valu2 Axiom a b
valu [1, a, b, c, d, e, f, g, h] = valu8 Function a b c d e f g h
valu [2, a, b, c, d, e, f, g, h, i, j] = valu10 Datatype a b c d e f g h i j
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, f] = valu6 Constructor a b c d e f
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 0
icode (Done a b) = icode2 1 a b
icode (Case a b) = icode2 2 a b
value = vcase valu where
valu [0] = valu0 Fail
valu [1, 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 0
icode PiHead = icode0 1
icode (ConHead a) = icode1 2 a
value = vcase valu where valu [0] = return SortHead
valu [1] = return PiHead
valu [2, a] = valu1 ConHead a
valu _ = malformed
instance EmbPrj Agda.Syntax.Common.IsAbstract where
icode AbstractDef = icode0 0
icode ConcreteDef = icode0 1
value = vcase valu where valu [0] = valu0 AbstractDef
valu [1] = valu0 ConcreteDef
valu _ = malformed
instance EmbPrj I.Clauses where
icode (Clauses a b) = icode2' a b
value = vcase valu where valu [a, b] = valu2 Clauses a b
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 1 a
icode (NoBind a) = icode1 2 a
icode NoBody = icode0'
value = vcase valu where valu [0, a] = valu1 Body a
valu [1, a] = valu1 Bind a
valu [2, a] = valu1 NoBind a
valu [] = valu0 NoBody
valu _ = malformed
instance EmbPrj Delayed where
icode Delayed = icode0 0
icode NotDelayed = icode0 1
value = vcase valu where valu [0] = valu0 Delayed
valu [1] = valu0 NotDelayed
valu _ = malformed
instance EmbPrj I.Pattern where
icode (VarP a ) = icode1 0 a
icode (ConP a b c) = icode3 1 a b c
icode (LitP a ) = icode1 2 a
icode (DotP a ) = icode1 3 a
value = vcase valu where valu [0, a] = valu1 VarP a
valu [1, 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 0 a
icode (Builtin a) = icode1 1 a
value = vcase valu where valu [0, a] = valu1 Prim a
valu [1, a] = valu1 Builtin a
valu _ = malformed
instance EmbPrj HP.NameKind where
icode HP.Bound = icode0 0
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 [0] = 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 4
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 [4] = 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 1
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 [1] = 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 0
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 [0] = 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
icodeX :: (Dict -> HashTable k Int32) -> (Dict -> IORef Int32) ->
k -> S Int32
icodeX dict counter key = do
d <- asks dict
c <- asks counter
fresh <- lift $ readIORef c
mi <- lift $ H.lookup d key
case mi of
Just i -> return i
Nothing -> do lift $ H.insert d key fresh
lift $ writeIORef c (fresh + 1)
return fresh
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
aTyp <- typeRepKey $ typeOf (undefined :: a)
when ((convert aTyp :: Int64) > convert (maxBound :: Int32)) __IMPOSSIBLE__
when ((convert aTyp :: Int64) < convert (minBound :: Int32)) __IMPOSSIBLE__
let aTyp' = convert aTyp :: Int32
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
where
convert :: (Integral b, Integral c) => b -> c
convert = fromInteger . toInteger
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]
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]
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
emptyDict :: SourceToModule
-> IO Dict
emptyDict fileMod = Dict
<$> H.new (==) hashNode
<*> H.new (==) H.hashString
<*> H.new (==) (H.hashInt . fromIntegral)
<*> H.new (==) (H.hashInt . floor)
<*> newIORef 0
<*> newIORef 0
<*> newIORef 0
<*> newIORef 0
<*> return fileMod
hashNode :: Node -> Int32
hashNode is = List.foldl' f golden is
where f m c = fromIntegral c * magic + hashInt32 m
magic = 0xdeadbeef
golden :: Int32
golden = 1013904242
hashInt32 x = mulHi x golden + x
mulHi :: Int32 -> Int32 -> Int32
mulHi a b = fromIntegral (r `shiftR` 32)
where r :: Int64
r = fromIntegral a * fromIntegral b
hashInt2 :: (Int32, Int32) -> Int32
hashInt2 (ix, rep) = hashNode [ix , rep]