content: {-# LANGUAGE OverloadedStrings, ConstraintKinds, FlexibleContexts #-}
  module Core.Lower.Basic
    ( TypeRepr(..)
    , LowerState(..)
    , LowerTrack
    , MonadLower
    , mkTyvar, mkVal, mkType, mkCo, mkCon, mkVar
    , lowerType
    , lowerLiteral
    ) where
  
  import Control.Monad.Reader
  import Control.Monad.Namey
  import Control.Monad.State
  
  import qualified Data.VarMap as VarMap
  import qualified Data.VarSet as VarSet
  
  import qualified Core.Core as C
  import Core.Core hiding (Atom, Term, Stmt, Type, Pattern, Arm)
  import Core.Var
  
  import qualified Syntax.Builtin as Bi
  import qualified Syntax as S
  import Syntax.Var (VarResolved(..), Var, Resolved, Typed)
  import Syntax (Lit(..), Skolem(..))
  
  data TypeRepr
    = OpaqueTy -- ^ An opaque type, for interfacing with foreign values.
    | SumTy VarSet.Set -- ^ A sum type, with the set of constructors.
  
    -- | A type which just wraps another.
    --
    -- This holds the name of the constructor, and the inner and outer
    -- type, both sharing their free variables.
    | WrapperTy CoVar C.Type C.Type
    deriving (Show, Eq)
  
  data LowerState
    = LS
      { vars  :: VarMap.Map C.Type
      , ctors :: VarMap.Map C.Type
      -- | The map of types to their constructors /if they have any/.
      , types :: VarMap.Map TypeRepr
      } deriving (Eq, Show)
  
  instance Semigroup LowerState where
    (LS v c t) <> (LS v' c' t') = LS (VarMap.union v v') (VarMap.union c c') (VarMap.union t t')
  
  instance Monoid LowerState where
    mempty = LS mempty mempty mempty
  
  type LowerTrack = VarMap.Map CoVar
  
  type MonadLower m
    = ( MonadNamey m
      , MonadState LowerTrack m
      , MonadReader LowerState m )
  
  mkTyvar, mkVal, mkType, mkCo, mkCon :: Var Resolved -> CoVar
  mkTyvar = mkVar TypeVar
  mkVal = mkVar ValueVar
  mkType = mkVar TypeConVar
  mkCo = mkVar CastVar
  mkCon = mkVar DataConVar
  
  -- | Make a core variable from a "Syntax" variable and a given kind.
  mkVar :: VarInfo -> Var Resolved -> CoVar
  mkVar k (TgName n i) = CoVar i (Just n) k
  mkVar _ n@TgInternal{} = error ("Cannot convert " ++ show n ++ " to CoVar")
  
  -- | Lower a type from "Syntax" to one in "Core.Core".
  lowerType :: S.Type Typed -> C.Type
  lowerType t@S.TyTuple{} = go t where
    go (S.TyTuple a b) = ExactRowsTy [("_1", lowerType a), ("_2", lowerType b)]
    go x = lowerType x
  lowerType (S.TyPi bind b)
    | S.Invisible v Nothing _ <- bind =
      ForallTy (Relevant (mkTyvar v)) StarTy (lowerType b)
    | S.Invisible v (Just c) _ <- bind =
      ForallTy (Relevant (mkTyvar v)) (lowerType c) (lowerType b)
    | S.Anon a <- bind =
      ForallTy Irrelevant (lowerType a) (lowerType b)
    | S.Implicit a <- bind =
      ForallTy Irrelevant (lowerType a) (lowerType b)
  lowerType (S.TyApp (S.TyApp (S.TyCon v ()) l) r)
    | v == Bi.tyArrowName = ForallTy Irrelevant (lowerType l) (lowerType r)
    | v == Bi.tyTupleName = lowerType (S.TyTuple l r)
  lowerType (S.TyApp a b) = AppTy (lowerType a) (lowerType b)
  lowerType (S.TyRows rho vs) = RowsTy (lowerType rho) (map (fmap lowerType) vs)
  lowerType (S.TyExactRows []) = NilTy
  lowerType (S.TyExactRows vs) = ExactRowsTy (map (fmap lowerType) vs)
  lowerType (S.TyVar v _) = VarTy (mkTyvar v)
  lowerType (S.TyCon v _)
    | v == Bi.tyConstraintName = StarTy
    | otherwise = ConTy (mkType v)
  lowerType (S.TyPromotedCon v _) = ConTy (mkCon v) -- TODO this is in the wrong scope
  lowerType (S.TySkol (Skolem (TgName _ v) (TgName n _) _ _)) = VarTy (CoVar v (Just n) TypeVar)
  lowerType (S.TySkol _) = error "impossible lowerType TySkol"
  lowerType (S.TyOperator l o r)
    | S.TyCon o' _ <- o, o' == Bi.tyTupleName = lowerType (S.TyTuple l r)
    | otherwise = (lowerType o `AppTy` lowerType l) `AppTy` lowerType r
  lowerType (S.TyWildcard (Just t)) = lowerType t
  lowerType (S.TyWildcard _) = error "impossible lowerType TyWildcard"
  lowerType (S.TyParens t) = lowerType t
  lowerType (S.TyWithConstraints _ t) = lowerType t
  lowerType S.TyType = StarTy
  
  -- All "lifted" types can just be *, screw Lint
  lowerType S.TyLit{} = StarTy
  lowerType S.TyTupleL{} = StarTy
  
  -- | Lower a literal from "Syntax" to one from "Core.Core".
  lowerLiteral :: Lit -> Literal
  lowerLiteral (LiFloat d) = Float d
  lowerLiteral (LiInt i) = Int i
  lowerLiteral (LiStr t) = Str t
  lowerLiteral (LiBool True) = LitTrue
  lowerLiteral (LiBool False) = LitFalse
  lowerLiteral LiUnit = Unit
  