{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.TypeChecking.Serialise.Instances.Abstract where

import qualified Data.Map as Map
import qualified Data.Set as Set

import Agda.Syntax.Common
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Info
import Agda.Syntax.Scope.Base
import Agda.Syntax.Position as P
import Agda.Syntax.Fixity

import Agda.TypeChecking.Serialise.Base
import Agda.TypeChecking.Serialise.Instances.Common ()

import Agda.TypeChecking.Monad

import Agda.Utils.Except

#include "undefined.h"
import Agda.Utils.Impossible

instance EmbPrj A.BindName where
  icod_ (A.BindName n) = icodeN' A.BindName n
  value = valueN A.BindName

instance EmbPrj Scope where
  icod_ (Scope a b c d e) = icodeN' Scope a b c d e

  value = valueN Scope

instance EmbPrj NameSpaceId where
  icod_ PublicNS        = icodeN' PublicNS
  icod_ PrivateNS       = icodeN 1 PrivateNS
  icod_ ImportedNS      = icodeN 2 ImportedNS
  icod_ OnlyQualifiedNS = icodeN 3 OnlyQualifiedNS

  value = vcase valu where
    valu []  = valuN PublicNS
    valu [1] = valuN PrivateNS
    valu [2] = valuN ImportedNS
    valu [3] = valuN OnlyQualifiedNS
    valu _   = malformed

instance EmbPrj Access where
  icod_ (PrivateAccess UserWritten) = icodeN 0 ()
  icod_ PrivateAccess{}             = icodeN 1 ()
  icod_ PublicAccess                = icodeN' PublicAccess
  icod_ OnlyQualified               = icodeN 2 ()

  value = vcase valu where
    valu [0] = valuN $ PrivateAccess UserWritten
    valu [1] = valuN $ PrivateAccess Inserted
    valu []  = valuN PublicAccess
    valu [2] = valuN OnlyQualified
    valu _   = malformed

instance EmbPrj NameSpace where
  icod_ (NameSpace a b c) = icodeN' NameSpace a b c

  value = valueN NameSpace

instance EmbPrj WhyInScope where
  icod_ Defined       = icodeN' Defined
  icod_ (Opened a b)  = icodeN 0 Opened a b
  icod_ (Applied a b) = icodeN 1 Applied a b

  value = vcase valu where
    valu []        = valuN Defined
    valu [0, a, b] = valuN Opened a b
    valu [1, a, b] = valuN Applied a b
    valu _         = malformed

instance EmbPrj AbstractName where
  icod_ (AbsName a b c d) = icodeN' AbsName a b c d

  value = valueN AbsName

instance EmbPrj NameMetadata where
  icod_ NoMetadata                  = icodeN' NoMetadata
  icod_ (GeneralizedVarsMetadata a) = icodeN' GeneralizedVarsMetadata a

  value = vcase valu where
    valu []  = valuN NoMetadata
    valu [a] = valuN GeneralizedVarsMetadata a
    valu _   = malformed

instance EmbPrj AbstractModule where
  icod_ (AbsModule a b) = icodeN' AbsModule a b

  value = valueN AbsModule

instance EmbPrj KindOfName where
  icod_ DefName        = icodeN' DefName
  icod_ ConName        = icodeN 1 ConName
  icod_ FldName        = icodeN 2 FldName
  icod_ PatternSynName = icodeN 3 PatternSynName
  icod_ QuotableName   = icodeN 4 QuotableName
  icod_ MacroName      = icodeN 5 MacroName
  icod_ GeneralizeName = icodeN 6 GeneralizeName
  icod_ DisallowedGeneralizeName = icodeN 7 DisallowedGeneralizeName

  value = vcase valu where
    valu []  = valuN DefName
    valu [1] = valuN ConName
    valu [2] = valuN FldName
    valu [3] = valuN PatternSynName
    valu [4] = valuN QuotableName
    valu [5] = valuN MacroName
    valu [6] = valuN GeneralizeName
    valu [7] = valuN DisallowedGeneralizeName
    valu _   = malformed

instance EmbPrj Binder where
  icod_ LambdaBound   = icodeN' LambdaBound
  icod_ PatternBound  = icodeN 1 PatternBound
  icod_ LetBound      = icodeN 2 LetBound

  value = vcase valu where
    valu []  = valuN LambdaBound
    valu [1] = valuN PatternBound
    valu [2] = valuN LetBound
    valu _   = malformed

instance EmbPrj LocalVar where
  icod_ (LocalVar a b c)  = icodeN' LocalVar a b c

  value = valueN LocalVar

instance EmbPrj ConPatInfo where
  icod_ (ConPatInfo a _ b) = icodeN' (\a b -> ConPatInfo a patNoRange b) a b

  value = valueN $ \a b -> ConPatInfo a patNoRange b

instance EmbPrj ConPatLazy

-- Only for pattern synonyms (where a is Void)
instance EmbPrj a => EmbPrj (A.Pattern' a) where
  icod_ (A.VarP a)            = icodeN 0 A.VarP a
  icod_ (A.ConP a b c)        = icodeN 1 A.ConP a b c
  icod_ (A.DefP p a b)        = icodeN 2 (A.DefP p) a b
  icod_ t@(A.WildP p)         = icodeN 3 t
  icod_ (A.AsP p a b)         = icodeN 4 (A.AsP p) a b
  icod_ (A.DotP p a)          = icodeN 5 (A.DotP p) a
  icod_ t@(A.AbsurdP _)       = icodeN 6 t
  icod_ (A.LitP a)            = icodeN 7 A.LitP a
  icod_ (A.ProjP p a b)       = icodeN 8 (A.ProjP p) a b
  icod_ (A.PatternSynP p a b) = icodeN 9 (A.PatternSynP p) a b
  icod_ (A.RecP p a)          = icodeN 10 (A.RecP p) a
  icod_ (A.EqualP _ a)        = __IMPOSSIBLE__
  icod_ (A.WithP i a)         = icodeN 11 (A.WithP i) a

  value = vcase valu where
    valu [0, a]       = valuN A.VarP a
    valu [1, a, b, c] = valuN A.ConP a b c
    valu [2, a, b]    = valuN (A.DefP i) a b
    valu [3]          = valuN (A.WildP i)
    valu [4, a, b]    = valuN (A.AsP i) a b
    valu [5, a]       = valuN (A.DotP i) a
    valu [6]          = valuN (A.AbsurdP i)
    valu [7, a]       = valuN (A.LitP) a
    valu [8, a, b]    = valuN (A.ProjP i) a b
    valu [9, a, b]    = valuN (A.PatternSynP i) a b
    valu [10, a]      = valuN (A.RecP i) a
    valu [11, a]      = valuN (A.WithP i) a
    valu _            = malformed

    i = patNoRange

instance EmbPrj ParenPreference where
  icod_ PreferParen     = icodeN' PreferParen
  icod_ PreferParenless = icodeN 1 PreferParenless
  value = vcase valu where
    valu []  = valuN PreferParen
    valu [1] = valuN PreferParenless
    valu _   = malformed

instance EmbPrj Precedence where
  icod_ TopCtx                 = icodeN' TopCtx
  icod_ FunctionSpaceDomainCtx = icodeN 1 FunctionSpaceDomainCtx
  icod_ (LeftOperandCtx a)     = icodeN 2 LeftOperandCtx a
  icod_ (RightOperandCtx a b)  = icodeN 3 RightOperandCtx a b
  icod_ FunctionCtx            = icodeN 4 FunctionCtx
  icod_ (ArgumentCtx a)        = icodeN 5 ArgumentCtx a
  icod_ InsideOperandCtx       = icodeN 6 InsideOperandCtx
  icod_ WithFunCtx             = icodeN 7 WithFunCtx
  icod_ WithArgCtx             = icodeN 8 WithArgCtx
  icod_ DotPatternCtx          = icodeN 9 DotPatternCtx

  value = vcase valu where
    valu []        = valuN TopCtx
    valu [1]       = valuN FunctionSpaceDomainCtx
    valu [2, a]    = valuN LeftOperandCtx a
    valu [3, a, b] = valuN RightOperandCtx a b
    valu [4]       = valuN FunctionCtx
    valu [5, a]    = valuN ArgumentCtx a
    valu [6]       = valuN InsideOperandCtx
    valu [7]       = valuN WithFunCtx
    valu [8]       = valuN WithArgCtx
    valu [9]       = valuN DotPatternCtx
    valu _         = malformed

instance EmbPrj ScopeInfo where
  icod_ (ScopeInfo a b c d e f g h i j) = icodeN' (\ a b c d e -> ScopeInfo a b c d e f g h i j) a b c d e

  value = valueN (\ a b c d e -> ScopeInfo a b c d e Map.empty Map.empty Set.empty Map.empty Map.empty)