module Agda.TypeChecking.Serialise.Instances.Internal where
import Control.Applicative
import Control.Monad.State.Strict
import Agda.Syntax.Internal as I
import Agda.Syntax.Position as P
import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common ()
import Agda.TypeChecking.Serialise.Instances.Compilers ()
import Agda.TypeChecking.Monad
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Positivity.Occurrence
import Agda.Utils.Permutation
#include "undefined.h"
import Agda.Utils.Impossible
instance EmbPrj Signature where
icod_ (Sig a b c) = icode3' a b c
value = vcase valu where
valu [a, b, c] = valu3 Sig a b c
valu _ = malformed
instance EmbPrj Section where
icod_ (Section a) = icode1' a
value = vcase valu where
valu [a] = valu1 Section a
valu _ = malformed
instance EmbPrj a => EmbPrj (Tele a) where
icod_ EmptyTel = icode0'
icod_ (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
icod_ (Perm a b) = icode2' a b
value = vcase valu where
valu [a, b] = valu2 Perm a b
valu _ = malformed
instance EmbPrj a => EmbPrj (Drop a) where
icod_ (Drop a b) = icode2' a b
value = vcase valu where
valu [a, b] = valu2 Drop a b
valu _ = malformed
instance EmbPrj a => EmbPrj (Elim' a) where
icod_ (Apply a) = icode1' a
icod_ (Proj a) = icode1 0 a
value = vcase valu where
valu [a] = valu1 Apply a
valu [0, a] = valu1 Proj a
valu _ = malformed
instance EmbPrj I.ConHead where
icod_ (ConHead a b c) = icode3' a b c
value = vcase valu where
valu [a, b, c] = valu3 ConHead a b c
valu _ = malformed
instance (EmbPrj a) => EmbPrj (I.Type' a) where
icod_ (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
icod_ (NoAbs a b) = icode2 0 a b
icod_ (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
icod_ (Var a []) = icode1' a
icod_ (Var a b) = icode2 0 a b
icod_ (Lam a b) = icode2 1 a b
icod_ (Lit a ) = icode1 2 a
icod_ (Def a b) = icode2 3 a b
icod_ (Con a b) = icode2 4 a b
icod_ (Pi a b) = icode2 5 a b
icod_ (Sort a ) = icode1 7 a
icod_ (MetaV a b) = __IMPOSSIBLE__
icod_ (DontCare a ) = icode1 8 a
icod_ (Level a ) = icode1 9 a
icod_ (Shared p) = icodeMemo termD termC p $ icode (derefPtr p)
value r = vcase valu' r where
valu' xs = gets mkShared <*> valu xs
valu [a] = valu1 var a
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
icod_ (Max a) = icode1' a
value = vcase valu where
valu [a] = valu1 Max a
valu _ = malformed
instance EmbPrj PlusLevel where
icod_ (ClosedLevel a) = icode1' a
icod_ (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
icod_ (NeutralLevel _ a) = icode1' a
icod_ (UnreducedLevel a) = icode1 1 a
icod_ MetaLevel{} = __IMPOSSIBLE__
icod_ BlockedLevel{} = __IMPOSSIBLE__
value = vcase valu where
valu [a] = valu1 UnreducedLevel a
valu [1, a] = valu1 UnreducedLevel a
valu _ = malformed
instance EmbPrj I.Sort where
icod_ (Type a ) = icode1' a
icod_ Prop = icode1 1 ()
icod_ SizeUniv = icode1 3 ()
icod_ Inf = icode1 4 ()
icod_ (DLub a b) = __IMPOSSIBLE__
value = vcase valu where
valu [a] = valu1 Type a
valu [1, _] = valu0 Prop
valu [3, _] = valu0 SizeUniv
valu [4, _] = valu0 Inf
valu _ = malformed
instance EmbPrj DisplayForm where
icod_ (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
icod_ (OpenThing a b) = icode2' a b
value = vcase valu where
valu [a, b] = valu2 OpenThing a b
valu _ = malformed
instance EmbPrj CtxId where
icod_ (CtxId a) = icode a
value n = CtxId `fmap` value n
instance EmbPrj DisplayTerm where
icod_ (DTerm a ) = icode1' a
icod_ (DDot a ) = icode1 1 a
icod_ (DCon a b) = icode2 2 a b
icod_ (DDef a b) = icode2 3 a b
icod_ (DWithApp a b c) = icode3 4 a b c
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, c] = valu3 DWithApp a b c
valu _ = malformed
instance EmbPrj MutualId where
icod_ (MutId a) = icode a
value n = MutId `fmap` value n
instance EmbPrj Definition where
icod_ (Defn a b c d e f g h i j k) = icode11' a b (P.killRange c) d e f g h i j k
value = vcase valu where
valu [a, b, c, d, e, f, g, h, i, j, k] = valu11 Defn a b c d e f g h i j k
valu _ = malformed
instance EmbPrj NLPat where
icod_ (PVar a b) = icode2 0 a b
icod_ (PWild) = icode0 1
icod_ (PDef a b) = icode2 2 a b
icod_ (PLam a b) = icode2 3 a b
icod_ (PPi a b) = icode2 4 a b
icod_ (PBoundVar a b) = icode2 5 a b
icod_ (PTerm a) = icode1 6 a
value = vcase valu where
valu [0, a, b] = valu2 PVar a b
valu [1] = valu0 PWild
valu [2, a, b] = valu2 PDef a b
valu [3, a, b] = valu2 PLam a b
valu [4, a, b] = valu2 PPi a b
valu [5, a, b] = valu2 PBoundVar a b
valu [6, a] = valu1 PTerm a
valu _ = malformed
instance EmbPrj RewriteRule where
icod_ (RewriteRule a b c d e) = icode5' a b c d e
value = vcase valu where
valu [a, b, c, d, e] = valu5 RewriteRule a b c d e
valu _ = malformed
instance EmbPrj Projection where
icod_ (Projection a b c d e) = icode5' a b c d e
value = vcase valu where
valu [a, b, c, d, e] = valu5 Projection a b c d e
valu _ = malformed
instance EmbPrj ExtLamInfo where
icod_ (ExtLamInfo a b) = icode2' a b
value = vcase valu where
valu [a, b] = valu2 ExtLamInfo a b
valu _ = malformed
instance EmbPrj Polarity where
icod_ Covariant = return 0
icod_ Contravariant = return 1
icod_ Invariant = return 2
icod_ Nonvariant = return 3
value 0 = return Covariant
value 1 = return Contravariant
value 2 = return Invariant
value 3 = return Nonvariant
value _ = malformed
instance EmbPrj Occurrence where
icod_ StrictPos = return 0
icod_ Mixed = return 1
icod_ Unused = return 2
icod_ GuardPos = return 3
icod_ JustPos = return 4
icod_ JustNeg = return 5
value 0 = return StrictPos
value 1 = return Mixed
value 2 = return Unused
value 3 = return GuardPos
value 4 = return JustPos
value 5 = return JustNeg
value _ = malformed
instance EmbPrj EtaEquality where
icod_ (Specified a) = icode1 0 a
icod_ (Inferred a) = icode1 1 a
value = vcase valu where
valu [0,a] = valu1 Specified a
valu [1,a] = valu1 Inferred a
valu _ = malformed
instance EmbPrj Defn where
icod_ Axiom = icode0 0
icod_ (Function a b _ c d e f g h i j k l m n) = icode14 1 a b c d e f g h i j k l m n
icod_ (Datatype a b c d e f g h i j) = icode10 2 a b c d e f g h i j
icod_ (Record a b c d e f g h i j k l) = icode12 3 a b c d e f g h i j k l
icod_ (Constructor a b c d e) = icode5 4 a b c d e
icod_ (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, j, k, l, m, n] = valu14 (\ a b -> Function a b Nothing) a b c d e f g h i j k l m n
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, l] = valu12 Record a b c d e f g h i j k l
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 (WithArity a) where
icod_ (WithArity a b) = icode2' a b
value = vcase valu where
valu [a, b] = valu2 WithArity a b
valu _ = malformed
instance EmbPrj a => EmbPrj (Case a) where
icod_ (Branches a b c d) = icode4' a b c d
value = vcase valu where
valu [a, b, c, d] = valu4 Branches a b c d
valu _ = malformed
instance EmbPrj CompiledClauses where
icod_ Fail = icode0'
icod_ (Done a b) = icode2' a (P.killRange b)
icod_ (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 a => EmbPrj (FunctionInverse' a) where
icod_ NotInjective = icode0'
icod_ (Inverse a) = icode1' a
value = vcase valu where
valu [] = valu0 NotInjective
valu [a] = valu1 Inverse a
valu _ = malformed
instance EmbPrj TermHead where
icod_ SortHead = icode0'
icod_ PiHead = icode0 1
icod_ (ConsHead a) = icode1 2 a
value = vcase valu where
valu [] = valu0 SortHead
valu [1] = valu0 PiHead
valu [2, a] = valu1 ConsHead a
valu _ = malformed
instance EmbPrj I.Clause where
icod_ (Clause 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 Clause a b c d e f
valu _ = malformed
instance EmbPrj a => EmbPrj (I.ClauseBodyF a) where
icod_ (Body a) = icode1 0 a
icod_ (Bind a) = icode1' a
icod_ NoBody = icode0'
value = vcase valu where
valu [0, a] = valu1 Body a
valu [a] = valu1 Bind a
valu [] = valu0 NoBody
valu _ = malformed
instance EmbPrj I.ConPatternInfo where
icod_ (ConPatternInfo a b) = icode2' a b
value = vcase valu where
valu [a, b] = valu2 ConPatternInfo a b
valu _ = malformed
instance EmbPrj a => EmbPrj (I.Pattern' a) where
icod_ (VarP a ) = icode1' a
icod_ (ConP a b c) = icode3' a b c
icod_ (LitP a ) = icode1 2 a
icod_ (DotP a ) = icode1 3 a
icod_ (ProjP a ) = icode1 4 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 [4, a] = valu1 ProjP a
valu _ = malformed
instance EmbPrj a => EmbPrj (Builtin a) where
icod_ (Prim a) = icode1' a
icod_ (Builtin a) = icode1 1 a
value = vcase valu where
valu [a] = valu1 Prim a
valu [1, a] = valu1 Builtin a
valu _ = malformed