{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.TypeChecking.Serialise.Instances.Internal where
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.TypeChecking.Coverage.SplitTree
import Agda.Utils.Permutation
#include "undefined.h"
import Agda.Utils.Impossible
instance EmbPrj Signature where
icod_ (Sig a b c) = icodeN' Sig a b c
value = valueN Sig
instance EmbPrj Section where
icod_ (Section a) = icodeN' Section a
value = valueN Section
instance EmbPrj a => EmbPrj (Tele a) where
icod_ EmptyTel = icodeN' EmptyTel
icod_ (ExtendTel a b) = icodeN' ExtendTel a b
value = vcase valu where
valu [] = valuN EmptyTel
valu [a, b] = valuN ExtendTel a b
valu _ = malformed
instance EmbPrj Permutation where
icod_ (Perm a b) = icodeN' Perm a b
value = valueN Perm
instance EmbPrj a => EmbPrj (Drop a) where
icod_ (Drop a b) = icodeN' Drop a b
value = valueN Drop
instance EmbPrj a => EmbPrj (Elim' a) where
icod_ (Apply a) = icodeN' Apply a
icod_ (IApply x y a) = icodeN 0 IApply x y a
icod_ (Proj a b) = icodeN 0 Proj a b
value = vcase valu where
valu [a] = valuN Apply a
valu [0,x,y,a] = valuN IApply x y a
valu [0, a, b] = valuN Proj a b
valu _ = malformed
instance EmbPrj I.ConHead where
icod_ (ConHead a b c) = icodeN' ConHead a b c
value = valueN ConHead
instance (EmbPrj a) => EmbPrj (I.Type' a) where
icod_ (El a b) = icodeN' El a b
value = valueN El
instance EmbPrj a => EmbPrj (I.Abs a) where
icod_ (NoAbs a b) = icodeN 0 NoAbs a b
icod_ (Abs a b) = icodeN' Abs a b
value = vcase valu where
valu [a, b] = valuN Abs a b
valu [0, a, b] = valuN NoAbs a b
valu _ = malformed
instance EmbPrj I.Term where
icod_ (Var a []) = icodeN' (\ a -> Var a []) a
icod_ (Var a b) = icodeN 0 Var a b
icod_ (Lam a b) = icodeN 1 Lam a b
icod_ (Lit a ) = icodeN 2 Lit a
icod_ (Def a b) = icodeN 3 Def a b
icod_ (Con a b c) = icodeN 4 Con a b c
icod_ (Pi a b) = icodeN 5 Pi a b
icod_ (Sort a ) = icodeN 7 Sort a
icod_ (MetaV a b) = __IMPOSSIBLE__
icod_ (DontCare a ) = icodeN 8 DontCare a
icod_ (Level a ) = icodeN 9 Level a
icod_ (Dummy s) = __IMPOSSIBLE__
value = vcase valu where
valu [a] = valuN var a
valu [0, a, b] = valuN Var a b
valu [1, a, b] = valuN Lam a b
valu [2, a] = valuN Lit a
valu [3, a, b] = valuN Def a b
valu [4, a, b, c] = valuN Con a b c
valu [5, a, b] = valuN Pi a b
valu [7, a] = valuN Sort a
valu [8, a] = valuN DontCare a
valu [9, a] = valuN Level a
valu _ = malformed
instance EmbPrj Level where
icod_ (Max a) = icodeN' Max a
value = valueN Max
instance EmbPrj PlusLevel where
icod_ (ClosedLevel a) = icodeN' ClosedLevel a
icod_ (Plus a b) = icodeN' Plus a b
value = vcase valu where
valu [a] = valuN ClosedLevel a
valu [a, b] = valuN Plus a b
valu _ = malformed
instance EmbPrj LevelAtom where
icod_ (NeutralLevel r a) = icodeN' (NeutralLevel r) a
icod_ (UnreducedLevel a) = icodeN 1 UnreducedLevel a
icod_ (MetaLevel a b) = __IMPOSSIBLE__
icod_ BlockedLevel{} = __IMPOSSIBLE__
value = vcase valu where
valu [a] = valuN UnreducedLevel a
valu [1, a] = valuN UnreducedLevel a
valu _ = malformed
instance EmbPrj I.Sort where
icod_ (Type a ) = icodeN 0 Type a
icod_ (Prop a ) = icodeN 1 Prop a
icod_ SizeUniv = icodeN 2 SizeUniv
icod_ Inf = icodeN 3 Inf
icod_ (PiSort a b) = icodeN 4 PiSort a b
icod_ (UnivSort a) = icodeN 5 UnivSort a
icod_ (MetaS a b) = __IMPOSSIBLE__
icod_ (DefS a b) = icodeN 6 DefS a b
icod_ (DummyS s) = __IMPOSSIBLE__
value = vcase valu where
valu [0, a] = valuN Type a
valu [1, a] = valuN Prop a
valu [2] = valuN SizeUniv
valu [3] = valuN Inf
valu [4, a, b] = valuN PiSort a b
valu [5, a] = valuN UnivSort a
valu [6, a, b] = valuN DefS a b
valu _ = malformed
instance EmbPrj DisplayForm where
icod_ (Display a b c) = icodeN' Display a b c
value = valueN Display
instance EmbPrj a => EmbPrj (Open a) where
icod_ (OpenThing a b) = icodeN' OpenThing a b
value = valueN OpenThing
instance EmbPrj CheckpointId where
icod_ (CheckpointId a) = icode a
value n = CheckpointId `fmap` value n
instance EmbPrj DisplayTerm where
icod_ (DTerm a ) = icodeN' DTerm a
icod_ (DDot a ) = icodeN 1 DDot a
icod_ (DCon a b c) = icodeN 2 DCon a b c
icod_ (DDef a b) = icodeN 3 DDef a b
icod_ (DWithApp a b c) = icodeN 4 DWithApp a b c
value = vcase valu where
valu [a] = valuN DTerm a
valu [1, a] = valuN DDot a
valu [2, a, b, c] = valuN DCon a b c
valu [3, a, b] = valuN DDef a b
valu [4, a, b, c] = valuN DWithApp a b c
valu _ = malformed
instance EmbPrj MutualId where
icod_ (MutId a) = icode a
value n = MutId `fmap` value n
instance EmbPrj CompKit where
icod_ (CompKit a b) = icodeN' CompKit a b
value = valueN CompKit
instance EmbPrj Definition where
icod_ (Defn a b c d e f g h i j k l m n o p) = icodeN' Defn a b (P.killRange c) d e f g h i j k l m n o p
value = valueN Defn
instance EmbPrj NLPat where
icod_ (PVar a b) = icodeN 0 PVar a b
icod_ (PWild) = icodeN 1 PWild
icod_ (PDef a b) = icodeN 2 PDef a b
icod_ (PLam a b) = icodeN 3 PLam a b
icod_ (PPi a b) = icodeN 4 PPi a b
icod_ (PBoundVar a b) = icodeN 5 PBoundVar a b
icod_ (PTerm a) = icodeN 6 PTerm a
value = vcase valu where
valu [0, a, b] = valuN PVar a b
valu [1] = valuN PWild
valu [2, a, b] = valuN PDef a b
valu [3, a, b] = valuN PLam a b
valu [4, a, b] = valuN PPi a b
valu [5, a, b] = valuN PBoundVar a b
valu [6, a] = valuN PTerm a
valu _ = malformed
instance EmbPrj NLPType where
icod_ (NLPType a b) = icodeN' NLPType a b
value = valueN NLPType
instance EmbPrj RewriteRule where
icod_ (RewriteRule a b c d e f) = icodeN' RewriteRule a b c d e f
value = valueN RewriteRule
instance EmbPrj Projection where
icod_ (Projection a b c d e) = icodeN' Projection a b c d e
value = valueN Projection
instance EmbPrj ProjLams where
icod_ (ProjLams a) = icodeN' ProjLams a
value = valueN ProjLams
instance EmbPrj System where
icod_ (System a b) = icodeN' System a b
value = valueN System
instance EmbPrj ExtLamInfo where
icod_ (ExtLamInfo a b) = icodeN' ExtLamInfo a b
value = valueN ExtLamInfo
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 IsForced where
icod_ Forced = return 0
icod_ NotForced = return 1
value 0 = return Forced
value 1 = return NotForced
value _ = malformed
instance EmbPrj NumGeneralizableArgs where
icod_ NoGeneralizableArgs = icodeN' NoGeneralizableArgs
icod_ (SomeGeneralizableArgs a) = icodeN' SomeGeneralizableArgs a
value = vcase valu where
valu [] = valuN NoGeneralizableArgs
valu [a] = valuN SomeGeneralizableArgs a
valu _ = malformed
instance EmbPrj DoGeneralize where
icod_ YesGeneralize = return 0
icod_ NoGeneralize = return 1
value 0 = return YesGeneralize
value 1 = return NoGeneralize
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) = icodeN 0 Specified a
icod_ (Inferred a) = icodeN 1 Inferred a
value = vcase valu where
valu [0,a] = valuN Specified a
valu [1,a] = valuN Inferred a
valu _ = malformed
instance EmbPrj Defn where
icod_ Axiom = icodeN 0 Axiom
icod_ (Function a b s t (_:_) c d e f g h i j k m) = __IMPOSSIBLE__
icod_ (Function a b s t [] c d e f g h i j k m) =
icodeN 1 (\ a b s -> Function a b s t []) a b s c d e f g h i j k m
icod_ (Datatype a b c d e f g h i) = icodeN 2 Datatype a b c d e f g h i
icod_ (Record a b c d e f g h i j k) = icodeN 3 Record a b c d e f g h i j k
icod_ (Constructor a b c d e f g h i) = icodeN 4 Constructor a b c d e f g h i
icod_ (Primitive a b c d e) = icodeN 5 Primitive a b c d e
icod_ AbstractDefn{} = __IMPOSSIBLE__
icod_ GeneralizableVar = icodeN 6 GeneralizableVar
icod_ DataOrRecSig{} = __IMPOSSIBLE__
value = vcase valu where
valu [0] = valuN Axiom
valu [1, a, b, s, c, d, e, f, g, h, i, j, k, m] = valuN (\ a b s -> Function a b s Nothing []) a b s c d e f g h i j k m
valu [2, a, b, c, d, e, f, g, h, i] = valuN Datatype a b c d e f g h i
valu [3, a, b, c, d, e, f, g, h, i, j, k] = valuN Record a b c d e f g h i j k
valu [4, a, b, c, d, e, f, g, h, i] = valuN Constructor a b c d e f g h i
valu [5, a, b, c, d, e] = valuN Primitive a b c d e
valu [6] = valuN GeneralizableVar
valu _ = malformed
instance EmbPrj SplitTag where
icod_ (SplitCon c) = icodeN 0 SplitCon c
icod_ (SplitLit l) = icodeN 1 SplitLit l
icod_ SplitCatchall = icodeN' SplitCatchall
value = vcase valu where
valu [] = valuN SplitCatchall
valu [0, c] = valuN SplitCon c
valu [1, l] = valuN SplitLit l
valu _ = malformed
instance EmbPrj a => EmbPrj (SplitTree' a) where
icod_ (SplittingDone a) = icodeN' SplittingDone a
icod_ (SplitAt a b) = icodeN 0 SplitAt a b
value = vcase valu where
valu [a] = valuN SplittingDone a
valu [0, a, b] = valuN SplitAt a b
valu _ = malformed
instance EmbPrj FunctionFlag where
icod_ FunStatic = icodeN 0 FunStatic
icod_ FunInline = icodeN 1 FunInline
icod_ FunMacro = icodeN 2 FunMacro
value = vcase valu where
valu [0] = valuN FunStatic
valu [1] = valuN FunInline
valu [2] = valuN FunMacro
valu _ = malformed
instance EmbPrj a => EmbPrj (WithArity a) where
icod_ (WithArity a b) = icodeN' WithArity a b
value = valueN WithArity
instance EmbPrj a => EmbPrj (Case a) where
icod_ (Branches a b c d e f g) = icodeN' Branches a b c d e f g
value = valueN Branches
instance EmbPrj CompiledClauses where
icod_ Fail = icodeN' Fail
icod_ (Done a b) = icodeN' Done a (P.killRange b)
icod_ (Case a b) = icodeN 2 Case a b
value = vcase valu where
valu [] = valuN Fail
valu [a, b] = valuN Done a b
valu [2, a, b] = valuN Case a b
valu _ = malformed
instance EmbPrj a => EmbPrj (FunctionInverse' a) where
icod_ NotInjective = icodeN' NotInjective
icod_ (Inverse a) = icodeN' Inverse a
value = vcase valu where
valu [] = valuN NotInjective
valu [a] = valuN Inverse a
valu _ = malformed
instance EmbPrj TermHead where
icod_ SortHead = icodeN' SortHead
icod_ PiHead = icodeN 1 PiHead
icod_ (ConsHead a) = icodeN 2 ConsHead a
icod_ (VarHead a) = icodeN 3 VarHead a
icod_ UnknownHead = icodeN 4 UnknownHead
value = vcase valu where
valu [] = valuN SortHead
valu [1] = valuN PiHead
valu [2, a] = valuN ConsHead a
valu [3, a] = valuN VarHead a
valu [4] = valuN UnknownHead
valu _ = malformed
instance EmbPrj I.Clause where
icod_ (Clause a b c d e f g h) = icodeN' Clause a b c d e f g h
value = valueN Clause
instance EmbPrj I.ConPatternInfo where
icod_ (ConPatternInfo a b c d) = icodeN' ConPatternInfo a b c d
value = valueN ConPatternInfo
instance EmbPrj I.DBPatVar where
icod_ (DBPatVar a b) = icodeN' DBPatVar a b
value = valueN DBPatVar
instance EmbPrj I.PatOrigin where
icod_ PatOSystem = icodeN' PatOSystem
icod_ PatOSplit = icodeN 1 PatOSplit
icod_ (PatOVar a) = icodeN 2 PatOVar a
icod_ PatODot = icodeN 3 PatODot
icod_ PatOWild = icodeN 4 PatOWild
icod_ PatOCon = icodeN 5 PatOCon
icod_ PatORec = icodeN 6 PatORec
icod_ PatOLit = icodeN 7 PatOLit
icod_ PatOAbsurd = icodeN 8 PatOAbsurd
value = vcase valu where
valu [] = valuN PatOSystem
valu [1] = valuN PatOSplit
valu [2, a] = valuN PatOVar a
valu [3] = valuN PatODot
valu [4] = valuN PatOWild
valu [5] = valuN PatOCon
valu [6] = valuN PatORec
valu [7] = valuN PatOLit
valu [8] = valuN PatOAbsurd
valu _ = malformed
instance EmbPrj a => EmbPrj (I.Pattern' a) where
icod_ (VarP a b ) = icodeN 0 VarP a b
icod_ (ConP a b c) = icodeN 1 ConP a b c
icod_ (LitP a ) = icodeN 2 LitP a
icod_ (DotP a b ) = icodeN 3 DotP a b
icod_ (ProjP a b ) = icodeN 4 ProjP a b
icod_ (IApplyP a b c d) = icodeN 5 IApplyP a b c d
icod_ (DefP a b c) = icodeN 6 DefP a b c
value = vcase valu where
valu [0, a, b] = valuN VarP a b
valu [1, a, b, c] = valuN ConP a b c
valu [2, a] = valuN LitP a
valu [3, a, b] = valuN DotP a b
valu [4, a, b] = valuN ProjP a b
valu [5, a, b, c, d] = valuN IApplyP a b c d
valu [6, a, b, c] = valuN DefP a b c
valu _ = malformed
instance EmbPrj a => EmbPrj (Builtin a) where
icod_ (Prim a) = icodeN' Prim a
icod_ (Builtin a) = icodeN 1 Builtin a
value = vcase valu where
valu [a] = valuN Prim a
valu [1, a] = valuN Builtin a
valu _ = malformed
instance EmbPrj a => EmbPrj (Substitution' a) where
icod_ IdS = icodeN' IdS
icod_ (EmptyS a) = icodeN 1 EmptyS a
icod_ (a :# b) = icodeN 2 (:#) a b
icod_ (Strengthen a b) = icodeN 3 Strengthen a b
icod_ (Wk a b) = icodeN 4 Wk a b
icod_ (Lift a b) = icodeN 5 Lift a b
value = vcase valu where
valu [] = valuN IdS
valu [1, a] = valuN EmptyS a
valu [2, a, b] = valuN (:#) a b
valu [3, a, b] = valuN Strengthen a b
valu [4, a, b] = valuN Wk a b
valu [5, a, b] = valuN Lift a b
valu _ = malformed