Syntax.hs

-- The raw abstract syntax and (refined) abstract syntax for Frank
{-# LANGUAGE DataKinds,GADTs,StandaloneDeriving, FlexibleInstances,
             UndecidableInstances, LambdaCase, KindSignatures,
             PatternSynonyms #-}
module Syntax where

import qualified Data.Map.Strict as M
import qualified Data.Set as S
import Data.List
import Data.Functor.Identity

import BwdFwd

import Shonky.Renaming

{-- Elementary definitions --}
type Id = String

-- Top level definitions instantiate this class
class HasId a where
  getId :: a -> Id

{-- For the definition of the AST as fixed-points --}

-- Fixed-point operator, takes a functor f
data Fix f = Fx (f (Fix f))
deriving instance Show (f (Fix f)) => Show (Fix f)
deriving instance Eq (f (Fix f)) => Eq (Fix f)

-- Gives the fixed-point of a functor "f" (see AST definitions),
--       parameterised by transformer "t" (e.g. AnnotT Raw)
type TFix (t :: (* -> *) -> (* -> *))
          (f :: ((* -> *) -> (* -> *)) -> * -> *) = Fix (t (f t))

-- Annotation Transformer
-- Takes an annotation object "a",
--                  a functor "f",
--              recursor type "r"
data AnnotT a f r = AnnF (f r, a)
deriving instance (Show (f r), Show a) => Show (AnnotT a f r)
deriving instance (Eq (f r), Eq a) => Eq (AnnotT a f r)

-- Like TFix, but with special transformer, namely "AnnotT a"
-- Takes an annotation object "a",
--                  a functor "f"
type AnnotTFix a f = TFix (AnnotT a) f

-- Add annotation
ann :: a -> f (AnnotT a) (AnnotTFix a f) -> AnnotTFix a f
ann a v = Fx (AnnF (v, a))

-- Retrieve object + annotation
unAnn :: AnnotTFix a f -> (f (AnnotT a) (AnnotTFix a f), a)
unAnn (Fx (AnnF (v, a))) = (v, a)

-- Remove annotation
strip :: AnnotTFix a f -> f (AnnotT a) (AnnotTFix a f)
strip = fst . unAnn

-- Get annotation
attr :: AnnotTFix a f -> a
attr = snd . unAnn

-- Modify annotation
modifyAnn :: a -> AnnotTFix a f -> AnnotTFix a f
modifyAnn a = ann a . strip

-- To annotate the origin of a node
data Source = InCode (Int, Int)
            | BuiltIn
            | Implicit
            | ImplicitNear (Int, Int)
            | Generated
  deriving (Show, Eq)

class HasSource a where
  getSource :: a -> Source
instance HasSource a => HasSource (AnnotTFix a f) where
  getSource x = getSource (attr x)

implicitNear :: HasSource a => a -> Source
implicitNear v = case getSource v of
                   InCode (line, col) -> ImplicitNear (line, col)
                   _                  -> Implicit

{-- Syntax annotations: Raw syntax comes from the parser and is preprocessed
    into Refined syntax. --}

class NotRaw a where
  idNotRaw :: a -> a
instance NotRaw () where idNotRaw = Prelude.id
instance NotRaw (AnnotT a Identity ()) where idNotRaw = Prelude.id

class NotRefined a where
  idNotRefined :: a -> a

class NotDesugared a where
  idNotDesugared :: a -> a
instance NotDesugared (AnnotT a Identity ()) where idNotDesugared = id

-- output from the parser
newtype Raw = Raw Source
  deriving (Show, Eq)
instance NotDesugared Raw where idNotDesugared = id
instance HasSource Raw where getSource (Raw s) = s

-- well-formed AST (after tidying up the output from the parser)
newtype Refined = Refined Source
  deriving (Show, Eq)
instance NotRaw Refined where idNotRaw = id
instance NotDesugared Refined where idNotDesugared = id
instance HasSource Refined where getSource (Refined s) = s

-- desugaring of types:
--   * type variables are given unique names
--   * strings are lists of characters
newtype Desugared = Desugared Source
  deriving (Show, Eq)
instance NotRaw Desugared where idNotRaw = id
instance HasSource Desugared where getSource (Desugared s) = s

-- Typed kind for distinguishing monomorphic and polymorphic variables.
newtype Typed = Typed Source
              deriving (Show, Eq)
instance NotRaw Typed where idNotRaw = id
instance NotDesugared Typed where idNotDesugared = id
instance HasSource Typed where getSource (Typed s) = s

{- AST nodes -}

-- Parts of the grammar are specific to raw/refined/desugared syntax.
-- The following markings are used:
-- - require Raw/Refined/Desugared:   t = AnnotT Raw
-- - require NotRaw / NotDesugared:   NotRaw (t Identity ()) =>   annotation

data Prog t = MkProg [TopTm t]
deriving instance Show t => Show (Prog t)
deriving instance Eq t => Eq (Prog t)

-- A top-level multihandler signature and clause.
data MHSigF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkSig :: Id -> CType Raw -> MHSigF (AnnotT Raw) r
deriving instance (Show r, Show (TFix t MHSigF)) => Show (MHSigF t r)
deriving instance (Eq r, Eq (TFix t MHSigF)) => Eq (MHSigF t r)
type MHSig a = AnnotTFix a MHSigF
pattern Sig x cty a = Fx (AnnF (MkSig x cty, a))
instance HasId (MHSig t) where getId (Sig x _ _) = x

data MHClsF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkMHCls :: Id -> Clause Raw -> MHClsF (AnnotT Raw) r
deriving instance (Show r, Show (TFix t MHClsF)) => Show (MHClsF t r)
deriving instance (Eq r, Eq (TFix t MHClsF)) => Eq (MHClsF t r)
type MHCls a = AnnotTFix a MHClsF
pattern MHCls x cls a = Fx (AnnF (MkMHCls x cls, a))
instance HasId (MHCls t) where getId (MHCls x _ _) = x

{---------------}
{- Parts of the grammar specific to the refined syntax. -}

-- FIXME: currently all top-level bindings are mutually
-- recursive. This setup will break if we add non-recursive value
-- bindings.
--
-- An obvious design is to group mutually recursive bindings using
-- letrec, as specified in the paper.
--
-- Data and interface definitions can continue to be globally mutually
-- recursive as they do not depend on values.

-- a recursive multihandler definition
data MHDefF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkDef :: Id -> TFix t CTypeF -> [TFix t ClauseF] -> MHDefF t r
deriving instance (Show r,
                   Show (TFix t CTypeF),
                   Show (TFix t ClauseF),
                   Show (TFix t MHDefF)) => Show (MHDefF t r)
deriving instance (Eq r,
                   Eq (TFix t CTypeF),
                   Eq (TFix t ClauseF),
                   Eq (TFix t MHDefF)) => Eq (MHDefF t r)
type MHDef a = AnnotTFix a MHDefF
pattern Def x cty clss a = Fx (AnnF (MkDef x cty clss, a))
instance HasId (MHDef t) where getId (Def x _ _ _) = x

{- MH here = 'operator' in the paper. Operator here doesn't have a name
   in the paper. -}

data OperatorF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkMono :: Id -> OperatorF (AnnotT Typed) r         -- monotypic (just variable)
  MkPoly :: Id -> OperatorF (AnnotT Typed) r         -- polytypic (handler expecting arguments, could also be 0 args (!))
  MkVarId :: Id -> OperatorF t r
  MkCmdId :: Id -> OperatorF t r
deriving instance (Show r, Show (TFix t OperatorF)) => Show (OperatorF t r)
deriving instance (Eq r, Eq (TFix t OperatorF)) => Eq (OperatorF t r)
type Operator a = AnnotTFix a OperatorF
pattern Mono x a = Fx (AnnF (MkMono x, a))
pattern Poly x a = Fx (AnnF (MkPoly x, a))
pattern VarId x a = Fx (AnnF (MkVarId x, a))
pattern CmdId x a = Fx (AnnF (MkCmdId x, a))

data DataConF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkDataCon :: Id -> [TFix t TmF] -> DataConF t r
deriving instance (Show r,
                   Show (TFix t TmF),
                   Show (TFix t DataConF)) => Show (DataConF t r)
deriving instance (Eq r,
                   Eq (TFix t TmF),
                   Eq (TFix t DataConF)) => Eq (DataConF t r)
type DataCon a = AnnotTFix a DataConF
pattern DataCon x tms a = Fx (AnnF (MkDataCon x tms, a))

{---------------}
{- Parts of the grammar independent of the syntax. -}

-- A raw term collects multihandler signatures and clauses separately. A
-- refined top-level term collects multihandler signatures and clauses in
-- one definition.
data TopTmF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkDataTm :: TFix t DataTF -> TopTmF t r
  MkItfTm :: TFix t ItfF -> TopTmF t r
  MkItfAliasTm :: TFix (AnnotT Raw) ItfAliasF -> TopTmF (AnnotT Raw) r
  MkSigTm :: TFix (AnnotT Raw) MHSigF -> TopTmF (AnnotT Raw) r
  MkClsTm :: TFix (AnnotT Raw) MHClsF -> TopTmF (AnnotT Raw) r
  MkDefTm :: NotRaw (t Identity ()) => TFix t MHDefF -> TopTmF t r
  -- MkDefTm :: NotRaw t => MHDef t -> TopTmF t r
deriving instance (Show (TFix t DataTF),
                   Show (TFix t ItfF),
                   Show (TFix t ItfAliasF),
                   Show (TFix (AnnotT Raw) MHSigF),
                   Show (TFix (AnnotT Raw) MHClsF),
                   Show (TFix t MHDefF),
                   Show r, Show (TFix t TopTmF)) => Show (TopTmF t r)
deriving instance (Eq (TFix t DataTF),
                   Eq (TFix t ItfF),
                   Eq (TFix t ItfAliasF),
                   Eq (TFix (AnnotT Raw) MHSigF),
                   Eq (TFix (AnnotT Raw) MHClsF),
                   Eq (TFix t MHDefF),
                   Eq r, Eq (TFix t TopTmF)) => Eq (TopTmF t r)
type TopTm a = AnnotTFix a TopTmF
pattern DataTm dt a = Fx (AnnF (MkDataTm dt, a))
pattern ItfTm itf a = Fx (AnnF (MkItfTm itf, a))
pattern ItfAliasTm itfAl a = Fx (AnnF (MkItfAliasTm itfAl, a))
pattern SigTm sig a = Fx (AnnF (MkSigTm sig, a))
pattern ClsTm cls a = Fx (AnnF (MkClsTm cls, a))
pattern DefTm def a = Fx (AnnF (MkDefTm def, a))
-- TODO: LC: Automatic generation of the following? Should be possible
--           somehow
instance HasId (TopTm t) where getId (DataTm dt _) = getId dt
                               getId (ItfTm itf _) = getId itf
                               getId (ItfAliasTm itfAl _) = getId itfAl
                               getId (SigTm sig _) = getId sig
                               getId (ClsTm cls _) = getId cls
                               getId (DefTm def _) = getId def

data UseF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkRawId :: Id -> UseF (AnnotT Raw) r
  MkRawComb :: r -> [TFix (AnnotT Raw) TmF] -> UseF (AnnotT Raw) r
  MkOp :: NotRaw (t Identity ()) => TFix t OperatorF -> UseF t r
  MkApp :: NotRaw (t Identity ()) => r -> [TFix t TmF] -> UseF t r
  MkAdapted :: [TFix t AdaptorF] -> r -> UseF t r
deriving instance (Show (TFix t OperatorF),
                   Show (TFix t TmF),
                   Show (TFix t ItfMapF),
                   Show (TFix t AdaptorF),
                   Show r, Show (TFix t UseF)) => Show (UseF t r)
deriving instance (Eq (TFix t OperatorF),
                   Eq (TFix t TmF),
                   Eq (TFix t ItfMapF),
                   Eq (TFix t AdaptorF),
                   Eq r, Eq (TFix t UseF)) => Eq (UseF t r)
type Use a = AnnotTFix a UseF
pattern RawId x a = Fx (AnnF (MkRawId x, a))
pattern RawComb f xs a = Fx (AnnF (MkRawComb f xs, a))
pattern Op op a = Fx (AnnF (MkOp op, a))
pattern App f xs a = Fx (AnnF (MkApp f xs, a))
pattern Adapted rs tm a = Fx (AnnF (MkAdapted rs tm, a))

-- Tm here = 'construction' in the paper

data TmF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkSC :: TFix t SCompF -> TmF t r
  MkLet :: Id -> r -> r -> TmF (AnnotT Raw) r
  MkStr :: String -> TmF t r
  MkInt :: Int -> TmF t r
  MkChar :: Char -> TmF t r
  MkList :: [r] -> TmF (AnnotT Raw) r
  MkTmSeq :: r -> r -> TmF t r
  MkUse :: TFix t UseF -> TmF t r
  MkDCon :: NotRaw (t Identity ()) => TFix t DataConF -> TmF t r
deriving instance (Show (TFix t SCompF),
                   Show (TFix t UseF),
                   Show (TFix t DataConF),
                   Show r, Show (TFix t TmF)) => Show (TmF t r)
deriving instance (Eq (TFix t SCompF),
                   Eq (TFix t UseF),
                   Eq (TFix t DataConF),
                   Eq r, Eq (TFix t TmF)) => Eq (TmF t r)
type Tm a = AnnotTFix a TmF
pattern SC sc a = Fx (AnnF (MkSC sc, a))
pattern Let x tm1 tm2 a = Fx (AnnF (MkLet x tm1 tm2, a))
pattern StrTm str a = Fx (AnnF (MkStr str, a))
pattern IntTm n a = Fx (AnnF (MkInt n, a))
pattern CharTm c a = Fx (AnnF (MkChar c, a))
pattern ListTm xs a = Fx (AnnF (MkList xs, a))
pattern TmSeq tm1 tm2 a = Fx (AnnF (MkTmSeq tm1 tm2, a))
pattern Use u a = Fx (AnnF (MkUse u, a))
pattern DCon dc a = Fx (AnnF (MkDCon dc, a))

-- A clause for a multihandler definition
data ClauseF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkCls :: [TFix t PatternF] -> TFix t TmF -> ClauseF t r
deriving instance (Show (TFix t PatternF),
                   Show (TFix t TmF),
                   Show r, Show (TFix t ClauseF)) => Show (ClauseF t r)
deriving instance (Eq (TFix t PatternF),
                   Eq (TFix t TmF),
                   Eq r, Eq (TFix t ClauseF)) => Eq (ClauseF t r)
type Clause a = AnnotTFix a ClauseF
pattern Cls ps t a = Fx (AnnF (MkCls ps t, a))

data SCompF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkSComp :: [TFix t ClauseF] -> SCompF t r
deriving instance (Show (TFix t ClauseF),
                   Show r, Show (TFix t SCompF)) => Show (SCompF t r)
deriving instance (Eq (TFix t ClauseF),
                   Eq r, Eq (TFix t SCompF)) => Eq (SCompF t r)
type SComp a = AnnotTFix a SCompF
pattern SComp cls a = Fx (AnnF (MkSComp cls, a))

data Kind = VT   -- value type
          | ET   -- effect type
  deriving (Show, Eq)

data DataTF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkDT :: Id -> [(Id, Kind)] -> [TFix t CtrF] -> DataTF t r
deriving instance (Show (TFix t CtrF),
                   Show r, Show (TFix t DataTF)) => Show (DataTF t r)
deriving instance (Eq (TFix t CtrF),
                   Eq r, Eq (TFix t DataTF)) => Eq (DataTF t r)
type DataT a = AnnotTFix a DataTF
pattern DT x ps ctrs a = Fx (AnnF (MkDT x ps ctrs, a))
instance HasId (DataT t) where getId (DT x _ _ _) = x

data ItfF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkItf :: Id -> [(Id, Kind)] -> [TFix t CmdF] -> ItfF t r
deriving instance (Show (TFix t CmdF),
                   Show r, Show (TFix t ItfF)) => Show (ItfF t r)
deriving instance (Eq (TFix t CmdF),
                   Eq r, Eq (TFix t ItfF)) => Eq (ItfF t r)
type Itf a = AnnotTFix a ItfF
pattern Itf x ps cmds a = Fx (AnnF (MkItf x ps cmds, a))
instance HasId (Itf t) where getId (Itf x _ _ _) = x

data ItfAliasF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkItfAlias :: Id -> [(Id, Kind)] -> TFix t ItfMapF -> ItfAliasF t r
deriving instance (Show (TFix t ItfMapF),
                   Show r, Show (TFix t ItfAliasF)) => Show (ItfAliasF t r)
deriving instance (Eq (TFix t ItfMapF),
                   Eq r, Eq (TFix t ItfAliasF)) => Eq (ItfAliasF t r)
type ItfAlias a = AnnotTFix a ItfAliasF
pattern ItfAlias x ps itfMap a = Fx (AnnF (MkItfAlias x ps itfMap, a))
instance HasId (ItfAlias t) where getId (ItfAlias x _ _ _) = x

data CtrF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkCtr :: Id -> [TFix t VTypeF] -> CtrF t r
deriving instance (Show (TFix t VTypeF),
                   Show r, Show (TFix t CtrF)) => Show (CtrF t r)
deriving instance (Eq (TFix t VTypeF),
                   Eq r, Eq (TFix t CtrF)) => Eq (CtrF t r)
type Ctr a = AnnotTFix a CtrF
pattern Ctr x tys a = Fx (AnnF (MkCtr x tys, a))

data CmdF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkCmd :: Id -> [(Id, Kind)] -> [TFix t VTypeF] -> TFix t VTypeF ->
           CmdF t r
deriving instance (Show (TFix t VTypeF),
                   Show r, Show (TFix t CmdF)) => Show (CmdF t r)
deriving instance (Eq (TFix t VTypeF),
                   Eq r, Eq (TFix t CmdF)) => Eq (CmdF t r)
--                    id  ty vars      arg tys   result ty
type Cmd a = AnnotTFix a CmdF
pattern Cmd x ps tys ty a = Fx (AnnF (MkCmd x ps tys ty, a))

data PatternF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkVPat :: TFix t ValuePatF -> PatternF t r
  MkCmdPat :: Id -> Int -> [TFix t ValuePatF] -> Id -> PatternF t r
  MkThkPat :: Id -> PatternF t r
deriving instance (Show (TFix t ValuePatF),
                   Show r, Show (TFix t PatternF)) => Show (PatternF t r)
deriving instance (Eq (TFix t ValuePatF),
                   Eq r, Eq (TFix t PatternF)) => Eq (PatternF t r)
type Pattern a = AnnotTFix a PatternF
pattern VPat vp a = Fx (AnnF (MkVPat vp, a))
pattern CmdPat x n vps k a = Fx (AnnF (MkCmdPat x n vps k, a))
pattern ThkPat x a = Fx (AnnF (MkThkPat x, a))

-- TODO: should we compile away string patterns into list of char patterns?
-- Takes      tag "t" (e.g. Refined),
--       recursor "r"
data ValuePatF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkVarPat :: Id -> ValuePatF t r
  MkDataPat :: Id -> [r] -> ValuePatF t r
  MkIntPat :: Int -> ValuePatF t r
  MkCharPat :: Char -> ValuePatF t r
  MkStrPat :: String -> ValuePatF t r
  MkConsPat :: r -> r -> ValuePatF (AnnotT Raw) r
  MkListPat :: [r] -> ValuePatF (AnnotT Raw) r
deriving instance (Show r, Show (TFix t ValuePatF)) => Show (ValuePatF t r)
deriving instance (Eq r, Eq (TFix t ValuePatF)) => Eq (ValuePatF t r)
type ValuePat a = AnnotTFix a ValuePatF
pattern VarPat x a = Fx (AnnF (MkVarPat x, a))
pattern DataPat x vps a = Fx (AnnF (MkDataPat x vps, a))
pattern IntPat n a = Fx (AnnF (MkIntPat n, a))
pattern CharPat c a = Fx (AnnF (MkCharPat c, a))
pattern StrPat str a = Fx (AnnF (MkStrPat str, a))
pattern ConsPat p1 p2 a = Fx (AnnF (MkConsPat p1 p2, a))
pattern ListPat ps a = Fx (AnnF (MkListPat ps, a))

-- Type hierarchy
data CTypeF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkCType :: [TFix t PortF] -> TFix t PegF -> CTypeF t r                    -- computation types
deriving instance (Show (TFix t PortF),
                   Show (TFix t PegF),
                   Show r, Show (TFix t CTypeF)) => Show (CTypeF t r)
deriving instance (Eq (TFix t PortF),
                   Eq (TFix t PegF),
                   Eq r, Eq (TFix t CTypeF)) => Eq (CTypeF t r)
type CType a = AnnotTFix a CTypeF
pattern CType ports peg a = Fx (AnnF (MkCType ports peg, a))

data PortF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkPort :: [TFix t AdjustmentF] -> TFix t VTypeF -> PortF t r              -- ports
deriving instance (Show (TFix t AdjustmentF),
                   Show (TFix t VTypeF),
                   Show r, Show (TFix t PortF)) => Show (PortF t r)
deriving instance (Eq (TFix t AdjustmentF),
                   Eq (TFix t VTypeF),
                   Eq r, Eq (TFix t PortF)) => Eq (PortF t r)
type Port a = AnnotTFix a PortF
pattern Port adjs ty a = Fx (AnnF (MkPort adjs ty, a))

data PegF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkPeg :: TFix t AbF -> TFix t VTypeF -> PegF t r                          -- pegs
deriving instance (Show (TFix t AbF),
                   Show (TFix t VTypeF),
                   Show r, Show (TFix t PegF)) => Show (PegF t r)
deriving instance (Eq (TFix t AbF),
                   Eq (TFix t VTypeF),
                   Eq r, Eq (TFix t PegF)) => Eq (PegF t r)
type Peg a = AnnotTFix a PegF
pattern Peg ab ty a = Fx (AnnF (MkPeg ab ty, a))

data VTypeF :: ((* -> *) -> (* -> *)) -> * -> * where                       -- value types
  MkDTTy :: Id -> [TFix t TyArgF] -> VTypeF t r                             --   data types (instant. type constr.)  may be refined to MkTVar
  MkSCTy :: TFix t CTypeF -> VTypeF t  r                                    --   suspended computation types
  MkTVar :: NotDesugared (t Identity ()) => Id -> VTypeF t  r               --                                       may be refined to MkDTTy
  MkRTVar :: Id -> VTypeF (AnnotT Desugared)  r                             --   rigid type variable (bound)
  MkFTVar :: Id -> VTypeF (AnnotT Desugared)  r                             --   flexible type variable (free)
  MkStringTy :: NotDesugared (t Identity ()) => VTypeF t r                  --   string type
  MkIntTy :: VTypeF t r                                                     --   int type
  MkCharTy :: VTypeF t r                                                    --   char type
deriving instance (Show (TFix t TyArgF),
                   Show (TFix t CTypeF),
                   Show r, Show (TFix t VTypeF)) => Show (VTypeF t r)
deriving instance (Eq (TFix t TyArgF),
                   Eq (TFix t CTypeF),
                   Eq r, Eq (TFix t VTypeF)) => Eq (VTypeF t r)
type VType a = AnnotTFix a VTypeF
pattern DTTy x tyArgs a = Fx (AnnF (MkDTTy x tyArgs, a))
pattern SCTy cty a = Fx (AnnF (MkSCTy cty, a))
pattern TVar x a = Fx (AnnF (MkTVar x, a))
pattern RTVar x a = Fx (AnnF (MkRTVar x, a))
pattern FTVar x a = Fx (AnnF (MkFTVar x, a))
pattern StringTy a = Fx (AnnF (MkStringTy, a))
pattern IntTy a = Fx (AnnF (MkIntTy, a))
pattern CharTy a = Fx (AnnF (MkCharTy, a))

-- Interface-id -> list of bwd-list of ty arg's (each entry an instantiation)
data ItfMapF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkItfMap :: M.Map Id (Bwd [TFix t TyArgF]) -> ItfMapF t r
deriving instance (Show (TFix t TyArgF),
                   Show r, Show (TFix t ItfMapF)) => Show (ItfMapF t r)
deriving instance (Eq (TFix t TyArgF),
                   Eq r, Eq (TFix t ItfMapF)) => Eq (ItfMapF t r)
type ItfMap a = AnnotTFix a ItfMapF
pattern ItfMap m a = Fx (AnnF (MkItfMap m, a))

-- Adjustments
data AdjustmentF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkConsAdj :: Id -> [TFix t TyArgF] -> AdjustmentF t r                     -- interface-id, list of ty arg's
  MkAdaptorAdj :: TFix t AdaptorF -> AdjustmentF t r
deriving instance (Show (TFix t TyArgF),
                   Show (TFix t AdaptorF),
                   Show r, Show (TFix t AdjustmentF)) => Show (AdjustmentF t r)
deriving instance (Eq (TFix t TyArgF),
                   Eq (TFix t AdaptorF),
                   Eq r, Eq (TFix t AdjustmentF)) => Eq (AdjustmentF t r)
type Adjustment a = AnnotTFix a AdjustmentF
pattern ConsAdj x ts a = Fx (AnnF (MkConsAdj x ts, a))
pattern AdaptorAdj adp a = Fx (AnnF (MkAdaptorAdj adp, a))

-- Abilities
data AbF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkAb :: TFix t AbModF -> TFix t ItfMapF -> AbF t r                        -- interface-id  ->  list of ty arg's
deriving instance (Show (TFix t AbModF),
                   Show (TFix t ItfMapF),
                   Show r, Show (TFix t AbF)) => Show (AbF t r)
deriving instance (Eq (TFix t AbModF),
                   Eq (TFix t ItfMapF),
                   Eq r, Eq (TFix t AbF)) => Eq (AbF t r)
type Ab a = AnnotTFix a AbF
pattern Ab abMod itfMap a = Fx (AnnF (MkAb abMod itfMap, a))

-- Ability modes
data AbModF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkEmpAb :: AbModF t r                                                     -- empty            (closed ability)
  MkAbVar :: NotDesugared (t Identity ()) => Id -> AbModF t r               -- non-desugared effect variable
  MkAbRVar :: Id -> AbModF (AnnotT Desugared)  r                            -- rigid eff var    (open ability)
  MkAbFVar :: Id -> AbModF (AnnotT Desugared)  r                            -- flexible eff var (open ability)
deriving instance (Show r, Show (TFix t AbModF)) => Show (AbModF t r)
deriving instance (Eq r, Eq (TFix t AbModF)) => Eq (AbModF t r)
type AbMod a = AnnotTFix a AbModF
pattern EmpAb a = Fx (AnnF (MkEmpAb, a))
pattern AbVar x a = Fx (AnnF (MkAbVar x, a))
pattern AbRVar x a = Fx (AnnF (MkAbRVar x, a))
pattern AbFVar x a = Fx (AnnF (MkAbFVar x, a))

data TyArgF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkVArg :: TFix t VTypeF -> TyArgF t r
  MkEArg :: TFix t AbF   -> TyArgF t r
deriving instance (Show (TFix t VTypeF),
                   Show (TFix t AbF),
                   Show r, Show (TFix t TyArgF)) => Show (TyArgF t r)
deriving instance (Eq (TFix t VTypeF),
                   Eq (TFix t AbF),
                   Eq r, Eq (TFix t TyArgF)) => Eq (TyArgF t r)
type TyArg a = AnnotTFix a TyArgF
pattern VArg ty a = Fx (AnnF (MkVArg ty, a))
pattern EArg ab a = Fx (AnnF (MkEArg ab, a))

-- TODO: LC: Make distinction between MkAdp and MkCompilableAdp on
-- type-level (GADT)
data AdaptorF :: ((* -> *) -> (* -> *)) -> * -> * where
  MkRawAdp :: Id -> Id -> [Id] -> [Id] -> AdaptorF (AnnotT Raw) r           -- e.g. I(s y x -> y x) (s is first arg, [y x] is second arg, [y x] is third arg)
  MkAdp :: Id -> Maybe Int -> [Int] -> AdaptorF t r                         -- adapt an interface `x` in an ability from right to left according to `ns` and (possibly - according to Maybe) attach all instances from `m` on
  MkCompilableAdp :: Id -> Int -> [Int] -> AdaptorF t r                     -- adapt an interface `x` in an ability that has exactly `n` instances of it from right to left according to `ns`
deriving instance (Show r, Show (TFix t AdaptorF)) => Show (AdaptorF t r)
deriving instance (Eq r, Eq (TFix t AdaptorF)) => Eq (AdaptorF t r)
type Adaptor a = AnnotTFix a AdaptorF
pattern RawAdp x liat left right a = Fx (AnnF (MkRawAdp x liat left right, a))
pattern Adp x mm ns a = Fx (AnnF (MkAdp x mm ns, a))
pattern CompilableAdp x m ns a = Fx (AnnF (MkCompilableAdp x m ns, a))

desugaredStrTy :: Desugared -> VType Desugared
desugaredStrTy a = DTTy "List" [VArg (CharTy a) a] a

getCmds :: Itf t -> [Cmd t]
getCmds (Itf _ _ xs _) = xs

collectINames :: [Itf t] -> [Id]
collectINames = map (\case (Itf itf _ _ _) -> itf)

getCtrs :: DataT t -> [Ctr t]
getCtrs (DT _ _ xs _) = xs

collectDTNames :: [DataT t] -> [Id]
collectDTNames = map (\case (DT dt _ _ _) -> dt)

-- Convert ability to a list of interface names and effect variables
{-
abToList :: Ab a -> [Id]
abToList MkEmpAb = []
abToList (MkAbVar id) = [id]
abToList MkOpenAb = []
abToList (MkAbPlus ab id _) = id : abToList ab

-- Substitute the ability for the distinguished effect variable in the type.
substOpenAb :: Ab a -> VType a -> VType a
substOpenAb ab (MkDTTy id abs xs) =
  MkDTTy id (map (substOpenAbAb ab) abs) (map (substOpenAb ab) xs)
substOpenAb ab (MkSCTy cty) = MkSCTy $ substOpenAbCType ab cty
substOpenAb _ ty = ty

substOpenAbAb :: Ab a -> Ab a -> Ab a
substOpenAbAb ab MkEmpAb = MkEmpAb
substOpenAbAb ab MkOpenAb = ab
substOpenAbAb ab (MkAbVar x) = MkAbVar x
substOpenAbAb ab (MkAbPlus ab' x ts) =
  MkAbPlus (substOpenAbAb ab' ab) x (map (substOpenAb ab) ts)

substOpenAbAdj :: Ab a -> Adj a -> Adj a
substOpenAbAdj ab MkIdAdj = MkIdAdj
substOpenAbAdj ab (MkAdjPlus adj itf xs) =
  MkAdjPlus (substOpenAbAdj ab adj) itf (map (substOpenAb ab) xs)

substOpenAbCType :: Ab a -> CType a -> CType a
substOpenAbCType ab (MkCType ps q) =
  MkCType (map (substOpenAbPort ab) ps) (substOpenAbPeg ab q)

substOpenAbPeg :: Ab a -> Peg a -> Peg a
substOpenAbPeg ab (MkPeg ab' ty) =
  MkPeg (substOpenAbAb ab ab') (substOpenAb ab ty)

substOpenAbPort :: Ab a -> Port a -> Port a
substOpenAbPort ab (MkPort adj ty) =
  MkPort (substOpenAbAdj ab adj) (substOpenAb ab ty)
-}

getOpName :: Operator t -> Id
getOpName (Mono x _) = x
getOpName (Poly x _) = x
getOpName (VarId x _) = x
getOpName (CmdId x _) = x

-- transform type variable (+ its kind) to a raw tye variable argument
-- (use during refinement of itf maps)
tyVar2rawTyVarArg :: (Id, Kind) -> TyArg Raw
tyVar2rawTyVarArg (id, VT) = VArg (TVar id (Raw Generated)) (Raw Generated)
tyVar2rawTyVarArg (id, ET) = EArg (liftAbMod (AbVar id (Raw Generated)))
                                  (Raw Generated)

-- transform type variable (+ its kind) to a rigid tye variable argument
-- (prepare for later unification)
tyVar2rigTyVarArg :: (Id, Kind) -> TyArg Desugared
tyVar2rigTyVarArg (id, VT) = VArg (RTVar id (Desugared Generated))
                                  (Desugared Generated)
tyVar2rigTyVarArg (id, ET) = EArg (liftAbMod (AbRVar id
                                                     (Desugared Generated)))
                                  (Desugared Generated)

liftAbMod :: AbMod t -> Ab t
liftAbMod abMod = Ab abMod (ItfMap M.empty (attr abMod)) (attr abMod)

-- Only to be applied to identifiers representing rigid or flexible
-- metavariables (type or effect).
trimVar :: Id -> Id
trimVar = takeWhile (/= '$')

{- Operations on interface maps -}

-- For each interface, the instances are concatenated
-- e.g. [State Bool, State Int] + [State String, State Char] =
-- [State Bool, State Int, State String, State Char]
plusItfMap :: ItfMap t -> ItfMap t -> ItfMap t
plusItfMap (ItfMap m a) (ItfMap m' _) = foldl plusItfMap' (ItfMap m a) (M.toList m')
  where plusItfMap' :: ItfMap t -> (Id, Bwd [TyArg t]) -> ItfMap t
        plusItfMap' (ItfMap m'' a'') (x, instants) =
          if M.member x m'' then ItfMap (M.adjust (\instants' -> instants' <>< bwd2fwd instants) x m'') a''
                                                                       else ItfMap (M.insert x instants m'') a''

-- eg. [State Bool,State Int] + State Char = [State Bool,State Int,State Char]
addInstanceToItfMap :: ItfMap Raw -> (Id, [TyArg Raw]) -> ItfMap Raw
addInstanceToItfMap (ItfMap m a) (x, args) =
  if M.member x m then ItfMap (M.adjust (:< args) x m) a
  else ItfMap (M.insert x (BEmp :< args) m) a

-- Given m1 and m2, return
-- 1) All interfaces that occur in m1 *and* m2
-- 2) Of those interface, take only the longest suffix of common length,
--    with instances from m1
intersectItfMap :: ItfMap t -> ItfMap t -> ItfMap t
intersectItfMap (ItfMap m1 a) (ItfMap m2 _) = ItfMap m'' a
  where m'  = M.intersectionWith (\args args' -> takeBwd (min (length args) (length args')) args) m1 m2
        m'' = M.filter (not . null) m'

-- Given m1 and m2, cut off entry suffixes of m1 of length determined by m2's
-- entries' lengths
cutItfMapSuffix :: ItfMap t -> ItfMap t -> ItfMap t
cutItfMapSuffix (ItfMap m1 a) (ItfMap m2 _) = ItfMap m'' a
  where m' = M.differenceWith (\args args' -> Just $ dropBwd (length args') args) m1 m2
        m'' = M.filter (not . null) m'

stripInactiveOffItfMap :: ItfMap t -> ItfMap t
stripInactiveOffItfMap (ItfMap m a) = ItfMap m' a
  where m' = M.map (\case BEmp -> error "invariant broken"
                          (_ :< x) -> BEmp :< x) m

isItfMapSuffixOf :: Eq t => ItfMap t -> ItfMap t -> Bool
isItfMapSuffixOf m1 m2 = (m2 `cutItfMapSuffix` m1) `plusItfMap` m1 == m2

emptyItfMap :: t -> ItfMap t
emptyItfMap = ItfMap M.empty

isItfMapEmpty :: ItfMap t -> Bool
isItfMapEmpty (ItfMap m _) = M.null m

-- Normal form of lists of adjustments
-- M.Map Id (Bwd [TyArg Desugared]:  I -> Enrichments for I (instances which are
--                                   handled here)
-- M.Map Id (Renaming, Int):         I -> Total renaming for I, number of enrichments for I
adjsNormalForm :: [Adjustment Desugared] ->
                  (M.Map Id (Bwd [TyArg Desugared]), M.Map Id Renaming)
adjsNormalForm = foldl (flip addAdjNormalForm) (M.empty, M.empty)

addAdjNormalForm :: Adjustment Desugared ->
  (M.Map Id (Bwd [TyArg Desugared]), M.Map Id Renaming) ->
  (M.Map Id (Bwd [TyArg Desugared]), M.Map Id Renaming)
addAdjNormalForm (ConsAdj x ts a) (insts, adps) = (
  adjustWithDefault (:< ts) x BEmp insts,
  adjustWithDefault (\(rs, r) ->
    (renToNormalForm (0:(map (+1) rs), r+1))) x renId adps)
addAdjNormalForm (AdaptorAdj adp@(CompilableAdp x m ns _) a) (insts, adps) = (
  insts,
  adjustWithDefault (\r ->
    (renToNormalForm $ renCompose (adpToRen adp) r)) x renId adps)
-- TODO: LC: double-check that the last line is correct

-- helpers

adjustWithDefault :: Ord k => (a -> a) -> k -> a -> M.Map k a -> M.Map k a
adjustWithDefault f k def m =
  let g = \x -> case x of Nothing -> Just def
                          _ -> x
  in
  M.adjust f k (M.alter g k m)

adpToRen :: Adaptor Desugared -> Renaming
adpToRen (CompilableAdp x m ns _) = (reverse ns, m)