path: root/src/LambdaCube/Compiler/DesugaredSource.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module LambdaCube.Compiler.DesugaredSource
    ( module LambdaCube.Compiler.DesugaredSource
    , Fixity(..)
    )where

import System.IO.Unsafe
import Text.Printf
import qualified Data.ByteString.Char8 as BS

import Data.Binary
import GHC.Generics (Generic)
import qualified System.FilePath.Posix as FilePath

--import Data.Text (Text)
import Data.Monoid
import Data.Maybe
import Data.List
import Data.Function
import Data.Bits
import qualified Data.Map as Map
import qualified Data.Set as Set
import Control.Arrow hiding ((<+>))

import LambdaCube.Compiler.Utils
import LambdaCube.Compiler.DeBruijn
import LambdaCube.Compiler.Pretty --hiding (braces, parens)

import Paths_lambdacube_compiler (getDataDir)

-------------------------------------------------------------------------------- simple name

-- TODO: move to Text
type SName = String

pattern Ticked :: SName -> SName
pattern Ticked s = '\'': s

untick :: SName -> SName
untick (Ticked s) = s
untick s = s

switchTick :: SName -> SName
switchTick (Ticked n) = n
switchTick n = Ticked n

pattern CaseName :: SName -> SName
pattern CaseName cs <- 'c':'a':'s':'e':cs where CaseName cs = "case" ++ cs

pattern MatchName :: SName -> SName
pattern MatchName cs <- 'm':'a':'t':'c':'h':cs where MatchName cs = "match" ++ cs

-------------------------------------------------------------------------------- file position

-- source position without file name
newtype SPos = SPos_ Int
  deriving (Eq, Ord, Generic)

instance Binary SPos

row :: SPos -> Int
row (SPos_ i) = i `shiftR` 16

column :: SPos -> Int
column (SPos_ i) = i .&. 0xffff

pattern SPos :: Int -> Int -> SPos
pattern SPos a b <- ((row &&& column) -> (a, b))
  where SPos a b =  SPos_ $ (a `shiftL` 16) .|. b

instance PShow SPos where
    pShow (SPos r c) = pShow r <> ":" <> pShow c

-------------------------------------------------------------------------------- file info

data FileInfo = FileInfo
    { fileId      :: !Int
    , filePath    :: FilePath
    , fileModule  :: String   -- module name
    }
    deriving Generic

instance Binary FileInfo

fileContent :: FileInfo -> String
fileContent fi = unsafePerformIO $ do
  let fname = filePath fi
  BS.putStrLn $ BS.pack $ printf "load source %s" fname
  readFile fname

instance Eq FileInfo where (==) = (==) `on` fileId
instance Ord FileInfo where compare = compare `on` fileId

instance PShow FileInfo where
  pShow fi = let path = filePath fi
             in text $ if isPrefixOf lcPreludePath path
                        then "<<installed-prelude-path>>" ++ drop (length lcPreludePath) path
                        else path

lcPreludePath :: String
lcPreludePath = unsafePerformIO $ (FilePath.</> "lc") <$> getDataDir

showPos :: FileInfo -> SPos -> Doc
showPos n p = pShow n <> ":" <> pShow p

-------------------------------------------------------------------------------- range

data Range = Range
    { rangeFile  :: !FileInfo
    , rangeStart :: !SPos
    , rangeStop  :: !SPos
    }
    deriving (Eq, Ord, Generic)

instance Binary Range

instance Show Range where show = ppShow
instance PShow Range
  where
    pShow (Range n b@(SPos r c) e@(SPos r' c')) = expand (pShow n <+> pShow b <> "-" <> pShow e)
      $ vcat $ (showPos n b <> ":")
             : map text (drop (r - 1) $ take r' $ lines $ fileContent n)
            ++ [text $ replicate (c - 1) ' ' ++ replicate (c' - c) '^' | r' == r]

showRangeWithoutFileName :: Range -> Doc
showRangeWithoutFileName (Range _ b e) = pShow b <> "-" <> pShow e

joinRange :: Range -> Range -> Range
joinRange (Range n b e) (Range n' b' e') = Range n (min b b') (max e e')
-- TODO: check (n == n') ?

-------------------------------------------------------------------------------- source info

data SI
    = NoSI (Set.Set String) -- no source info, attached debug info
    | RangeSI Range
    deriving Generic

instance Binary SI

getRange :: SI -> Maybe Range
getRange (RangeSI r) = Just r
getRange _ = Nothing

--instance Show SI where show _ = "SI"
instance Eq SI where _ == _ = True
instance Ord SI where _ `compare` _ = EQ

instance Monoid SI where
    mempty = NoSI Set.empty
#if !MIN_VERSION_base(4,11,0)
    mappend (RangeSI r1) (RangeSI r2) = RangeSI (joinRange r1 r2)
    mappend (NoSI ds1) (NoSI ds2) = NoSI  (ds1 `Set.union` ds2)
    mappend r@RangeSI{} _ = r
    mappend _ r@RangeSI{} = r
#else
instance Semigroup SI where
    (<>) (RangeSI r1) (RangeSI r2) = RangeSI (joinRange r1 r2)
    (<>) (NoSI ds1) (NoSI ds2) = NoSI  (ds1 `Set.union` ds2)
    (<>) r@RangeSI{} _ = r
    (<>) _ r@RangeSI{} = r
#endif

instance PShow SI where
    pShow (NoSI ds) = hsep $ map text $ Set.toList ds
    pShow (RangeSI r) = pShow r

hashPos :: FileInfo -> SPos -> Int
hashPos fn (SPos_ p) = (1 + fileId fn) `shiftL` 32 .|. p

debugSI :: String -> SI
debugSI a = NoSI (Set.singleton a)

validate :: SI -> [SI] -> SI
si@(RangeSI r) `validate` xs | r `notElem` [r | RangeSI r <- xs]  = si
_ `validate` _ = mempty

-------------------------------------------------------------------------------- type classes for source info

class SourceInfo a where
    sourceInfo :: a -> SI

instance SourceInfo SI where
    sourceInfo = id

instance SourceInfo si => SourceInfo [si] where
    sourceInfo = foldMap sourceInfo

class SetSourceInfo a where
    setSI :: SI -> a -> a

-------------------------------------------------------------------------------- name with source info

data SIName = SIName__ { nameHash :: Int, nameSI :: SI, nameFixity :: Maybe Fixity, sName :: SName }
    deriving Generic

instance Binary SIName

pattern SIName_ :: SI -> Maybe Fixity -> SName -> SIName
pattern SIName_ si f n <- SIName__ _ si f n
  where SIName_ si f n =  SIName__ (fnameHash si n) si f n

pattern SIName :: SI -> SName -> SIName
pattern SIName si n <- SIName_ si _ n
  where SIName si n =  SIName_ si Nothing n

instance Eq SIName where (==) = (==) `on` sName
instance Ord SIName where compare = compare `on` sName
instance Show SIName where show = sName
instance PShow SIName
  where
    pShow (SIName_ si f n) = expand (if isOpName n then DOp0 n (defaultFixity f) else maybe (text n) (DOp0 n) f) $ case si of
        NoSI{} -> text n --maybe (text n) (DOp0 n) f
        _ -> pShow si

instance SourceInfo SIName where
    sourceInfo (SIName si _) = si

instance SetSourceInfo SIName where
    setSI si (SIName_ _ f s) = SIName_ si f s

-------------------------------------------------------------------------------- hashed names

newtype FName = FName { fName :: SIName }
    deriving Generic

instance Binary FName

instance Eq    FName where (==) = (==) `on` nameHash . fName
instance Ord   FName where compare = compare `on` nameHash . fName
instance Show  FName where show = show . fName
instance PShow FName where pShow = pShow . fName

data FNameTag
    -- type constructors & constructors
    = F'Type
    | F'Empty
    | F'Unit        | FTT
    | F'Constraint  | FCUnit | FCEmpty
    | F'Nat         | FZero | FSucc
    | F'Bool        | FFalse | FTrue
    | F'Ordering    | FLT | FGT | FEQ
    | F'List        | FNil | FCons
    | F'HList       | FHCons | FHNil
    | F'VecS        | FV2 | FV3 | FV4
                    | FRecordCons
                    | FRecItem
                    | FSx | FSy | FSz | FSw
    | F'Int
    | F'Word
    | F'Float
    | F'String
    | F'Char
    | F'Output
    -- type functions
    | F'T2 | F'EqCT | F'CW | F'Split | F'VecScalar
    -- functions
    | Fcoe | FparEval | Ft2C | FprimFix
    | Fparens | FtypeAnn | Fundefined | Fotherwise | FprimIfThenElse | FfromTo | FconcatMap | FfromInt | Fproject | Fswizzscalar | Fswizzvector

    | FunsafeCoerce | FreflCstr | FhlistNilCase | FhlistConsCase
    | FprimAddInt | FprimSubInt | FprimModInt | FprimSqrtFloat | FprimRound | FprimIntToFloat | FprimIntToNat
    | FprimCompareInt | FprimCompareFloat | FprimCompareChar | FprimCompareString
    | FPrimGreaterThan | FPrimGreaterThanEqual | FPrimLessThan | FPrimLessThanEqual | FPrimEqualV | FPrimNotEqualV | FPrimEqual | FPrimNotEqual
    | FPrimSubS | FPrimSub | FPrimAddS | FPrimAdd | FPrimMulS | FPrimMul | FPrimDivS | FPrimDiv | FPrimModS | FPrimMod
    | FPrimNeg | FPrimAnd | FPrimOr | FPrimXor | FPrimNot

    -- other
    | F_rhs | F_section
    deriving (Eq, Ord, Show, Enum, Bounded, Generic)

instance Binary FNameTag

tagName :: FNameTag -> String
tagName FCons = ":"
tagName t = case show t of 'F': s -> s

pattern Tag :: FNameTag -> SIName
pattern Tag t <- (toTag . nameHash -> Just t)
  where Tag t =  SIName__ (fromEnum t) (tagSI t) (tagFixity t) (tagName t)

pattern FTag :: FNameTag -> FName
pattern FTag t = FName (Tag t)

toTag :: Int -> Maybe FNameTag
toTag i
    | i <= fromEnum (maxBound :: FNameTag) = Just (toEnum i)
    | otherwise = Nothing

tagFixity :: FNameTag -> Maybe Fixity
tagFixity FCons = Just $ InfixR 5
tagFixity _ = Nothing

tagSI :: FNameTag -> SI
tagSI t = NoSI $ Set.singleton $ tagName t

fnameHash :: SI -> SName -> Int
fnameHash (RangeSI (Range fn p _)) s = maybe (hashPos fn p) fromEnum $ Map.lookup s fntable
fnameHash _ s = 0xffff -- TODO error $ "mkFName: " ++ show s

fntable :: Map.Map String FNameTag
fntable = Map.fromList $ (tagName &&& id) <$> [minBound ..]

-------------------------------------------------------------------------------- literal

data Lit
    = LInt    Integer
    | LChar   Char
    | LFloat  Double
    | LString String
  deriving (Eq, Generic)

instance Binary Lit

instance PShow Lit where
    pShow = \case
        LFloat x  -> pShow x
        LString x -> text $ show x
        LInt x    -> pShow x
        LChar x   -> pShow x

-------------------------------------------------------------------------------- expression

data SExp' a
    = SLit    SI Lit
    | SGlobal SIName
    | SApp_   SI Visibility (SExp' a) (SExp' a)
    | SBind_  SI Binder (SData SIName){-parameter name-} (SExp' a) (SExp' a)
    | SVar_   (SData SIName) !Int
    | SLet_   SI (SData SIName) (SExp' a) (SExp' a)    -- let x = e in f   -->  SLet e f{-x is Var 0-}
    | SLHS    SIName (SExp' a)
    | STyped  a
  deriving (Eq, Generic)

instance Binary SExp

sLHS :: SIName -> SExp' a -> SExp' a
sLHS _ (SRHS x) = x
sLHS n x = SLHS n x

type SExp = SExp' Void

data Binder
    = BPi  Visibility
    | BLam Visibility
    | BMeta      -- a metavariable is like a floating hidden lambda
  deriving (Eq, Generic)

instance Binary Binder

instance PShow Binder where
    pShow = \case
        BPi v -> "BPi" `DApp` pShow v
        BLam v -> "BLam" `DApp` pShow v
        BMeta -> "BMeta"

data Visibility = Hidden | Visible
  deriving (Eq, Generic)

instance Binary Visibility

instance PShow Visibility where
    pShow = \case
        Hidden -> "Hidden"
        Visible -> "Visible"

dummyName :: String -> SIName
dummyName s = SIName (debugSI s) "" --("v_" ++ s)

dummyName' :: String -> SData SIName
dummyName' = SData . dummyName

sVar :: String -> Int -> SExp' a
sVar = SVar . dummyName

pattern SBind :: Binder -> SData SIName -> SExp' a -> SExp' a -> SExp' a
pattern SBind v x a b <- SBind_ _ v x a b
  where SBind v x a b =  SBind_ (sourceInfo a <> sourceInfo b) v x a b

pattern SPi :: Visibility -> SExp' a -> SExp' a -> SExp' a
pattern SPi  h a b <- SBind (BPi  h) _ a b
  where SPi  h a b =  SBind (BPi  h) (dummyName' "SPi") a b

pattern SLam :: Visibility -> SExp' a -> SExp' a -> SExp' a
pattern SLam h a b <- SBind (BLam h) _ a b
  where SLam h a b =  SBind (BLam h) (dummyName' "SLam") a b

pattern Wildcard :: SExp' a -> SExp' a
pattern Wildcard t <- SBind BMeta _ t (SVar _ 0)
  where Wildcard t =  SBind BMeta (dummyName' "Wildcard") t (sVar "Wildcard2" 0)

pattern SLet :: SIName -> SExp' a -> SExp' a -> SExp' a
pattern SLet n a b <- SLet_ _ (SData n) a b
  where SLet n a b =  SLet_ (sourceInfo a <> sourceInfo b) (SData n) a b

pattern SLamV :: SExp' a -> SExp' a
pattern SLamV a  = SLam Visible (Wildcard SType) a

pattern SVar :: SIName -> Int -> SExp' a
pattern SVar a b = SVar_ (SData a) b

pattern SApp :: Visibility -> SExp' a -> SExp' a -> SExp' a
pattern SApp h a b <- SApp_ _ h a b
  where SApp h a b =  SApp_ (sourceInfo a <> sourceInfo b) h a b

pattern SAppH :: SExp' a -> SExp' a -> SExp' a
pattern SAppH a b    = SApp Hidden a b

pattern SAppV :: SExp' a -> SExp' a -> SExp' a
pattern SAppV a b    = SApp Visible a b

pattern SAppV2 :: SExp' a -> SExp' a -> SExp' a -> SExp' a
pattern SAppV2 f a b = f `SAppV` a `SAppV` b

infixl 2 `SAppV`, `SAppH`
------------------------------------------------------------------------------------------------- ****************************************
pattern SBuiltin :: FNameTag -> SExp' a
pattern SBuiltin s = SGlobal (Tag s)

pattern SRHS a      = SBuiltin F_rhs     `SAppV` a
pattern Section e   = SBuiltin F_section `SAppV` e
pattern SType       = SBuiltin F'Type
pattern SConstraint = SBuiltin F'Constraint
pattern Parens e    = SBuiltin Fparens   `SAppV` e
pattern SAnn a t    = SBuiltin FtypeAnn  `SAppH` t `SAppV` a
pattern SCW a       = SBuiltin F'CW      `SAppV` a

pattern TyType :: SExp' a -> SExp' a
pattern TyType a    = SAnn a SType

-- builtin heterogenous list
pattern HList a   = SBuiltin F'HList `SAppV` a
pattern HCons a b = SBuiltin FHCons  `SAppV` a `SAppV` b
pattern HNil      = SBuiltin FHNil

-- builtin list
pattern BList a   = SBuiltin F'List `SAppV` a
pattern BCons a b = SBuiltin FCons `SAppV` a `SAppV` b
pattern BNil      = SBuiltin FNil

getTTuple :: SExp' a -> [SExp' a]
getTTuple (HList (getList -> Just xs)) = xs
getTTuple x = [x]

getList :: SExp' a -> Maybe [SExp' a]
getList BNil = Just []
getList (BCons x (getList -> Just y)) = Just (x:y)
getList _ = Nothing

sLit :: Lit -> SExp' a
sLit = SLit mempty

isPi :: Binder -> Bool
isPi (BPi _) = True
isPi _ = False

pattern UncurryS :: [(Visibility, SExp' a)] -> SExp' a -> SExp' a
pattern UncurryS ps t <- (getParamsS -> (ps, t))
  where UncurryS ps t = foldr (uncurry SPi) t ps

getParamsS :: SExp' a -> ([(Visibility, SExp' a)], SExp' a)
getParamsS (SPi h t x) = first ((h, t):) $ getParamsS x
getParamsS x = ([], x)

pattern AppsS :: SExp' a -> [(Visibility, SExp' a)] -> SExp' a
pattern AppsS f args  <- (getApps -> (f, args))
  where AppsS = foldl $ \a (v, b) -> SApp v a b

getApps :: SExp' a -> (SExp' a, [(Visibility, SExp' a)])
getApps = second reverse . run where
  run (SApp h a b) = second ((h, b):) $ run a
  run x = (x, [])

-- todo: remove
downToS :: String -> Int -> Int -> [SExp' a]
downToS err n m = [sVar (err ++ "_" ++ show i) (n + i) | i <- [m-1, m-2..0]]

instance SourceInfo (SExp' a) where
    sourceInfo = \case
        SGlobal sn        -> sourceInfo sn
        SBind_ si _ _ _ _ -> si
        SApp_ si _ _ _    -> si
        SLet_ si _ _ _    -> si
        SVar sn _         -> sourceInfo sn
        SLit si _         -> si
        SLHS n x          -> sourceInfo x
        STyped _          -> mempty

instance SetSourceInfo SExp where
    setSI si = \case
        SBind_ _ a b c d -> SBind_ si a b c d
        SApp_ _ a b c    -> SApp_ si a b c
        SLet_ _ le a b   -> SLet_ si le a b
        SVar sn i        -> SVar (setSI si sn) i
        SGlobal sn       -> SGlobal (setSI si sn)
        SLit _ l         -> SLit si l
        SLHS n x         -> SLHS n $ setSI si x
        STyped v         -> elimVoid v

foldS
    :: Monoid m
    => (Int -> t -> m)
    -> (SIName -> Int -> m)
    -> (SIName -> Int -> Int -> m)
    -> Int
    -> SExp' t
    -> m
foldS h g f = fs
  where
    fs i = \case
        SApp _ a b -> fs i a <> fs i b
        SLet _ a b -> fs i a <> fs (i+1) b
        SBind_ _ _ _ a b -> fs i a <> fs (i+1) b
        SVar sn j -> f sn j i
        SGlobal sn -> g sn i
        x@SLit{} -> mempty
        SLHS _ x -> fs i x
        STyped x -> h i x

foldName :: Monoid m => (SIName -> m) -> SExp' Void -> m
foldName f = foldS (\_ -> elimVoid) (\sn _ -> f sn) mempty 0

usedS :: SIName -> SExp -> Bool
usedS n = getAny . foldName (Any . (== n))

mapS
    :: (Int -> a -> SExp' a)
    -> (SIName -> Int -> SExp' a)
    -> (SIName -> Int -> Int{-level-} -> SExp' a)
    -> Int
    -> SExp' a
    -> SExp' a
mapS hh gg f2 = g where
    g i = \case
        SApp_ si v a b -> SApp_ si v (g i a) (g i b)
        SLet_ si x a b -> SLet_ si x (g i a) (g (i+1) b)
        SBind_ si k si' a b -> SBind_ si k si' (g i a) (g (i+1) b)
        SVar sn j -> f2 sn j i
        SGlobal sn -> gg sn i
        SLHS n x -> SLHS n $ g i x
        STyped x -> hh i x
        x@SLit{} -> x

instance HasFreeVars a => HasFreeVars (SExp' a) where
    getFreeVars = foldS (\l x -> shiftFreeVars (-l) $ getFreeVars x) mempty (\sn i l -> if i >= l then freeVar $ i - l else mempty) 0

instance Rearrange a => Rearrange (SExp' a) where
    rearrange i f = mapS (\i x -> STyped $ rearrange i f x) (const . SGlobal) (\sn j i -> SVar sn $ if j < i then j else i + rearrangeFun f (j - i)) i

instance DeBruijnify SIName SExp where
    deBruijnify_ j xs
        = mapS (\_ -> elimVoid) (\sn x -> maybe (SGlobal sn) (\i -> SVar sn $ i + x) $ elemIndex sn xs)
                                (\sn j k -> SVar sn $ if j >= k then j + l else j) j
      where
        l = length xs

trSExp :: (a -> b) -> SExp' a -> SExp' b
trSExp f = g where
    g = \case
        SApp_ si v a b -> SApp_ si v (g a) (g b)
        SLet_ si x a b -> SLet_ si x (g a) (g b)
        SBind_ si k si' a b -> SBind_ si k si' (g a) (g b)
        SVar sn j -> SVar sn j
        SGlobal sn -> SGlobal sn
        SLit si l -> SLit si l
        SLHS n x -> SLHS n (g x)
        STyped a -> STyped $ f a

trSExp' :: SExp -> SExp' a
trSExp' = trSExp elimVoid

instance (HasFreeVars a, PShow a) => PShow (SExp' a) where
    pShow = \case
        SGlobal ns      -> pShow ns
        Parens x        -> pShow x     -- TODO: remove
        SAnn a b        -> shAnn (pShow a) (pShow b)
        TyType a        -> text "tyType" `DApp` pShow a
        SApp h a b      -> shApp h (pShow a) (pShow b)
        Wildcard SType  -> text "_"
        Wildcard t      -> shAnn (text "_") (pShow t)
        SBind_ _ h (SData n) SType b -> shLam_ (usedVar' 0 b $ sName n) h Nothing (pShow b)
        SBind_ _ h (SData n) a b -> shLam (usedVar' 0 b $ sName n) h (pShow a) (pShow b)
        SLet _ a b      -> shLet_ (pShow a) (pShow b)
        SLHS n x        -> "_lhs" `DApp` pShow n `DApp` pShow x
        STyped a        -> pShow a
        SVar _ i        -> shVar i
        SLit _ l        -> pShow l

shApp :: Visibility -> Doc -> Doc -> Doc
shApp Visible a b = DApp a b
shApp Hidden a b = DApp a (DAt b)

usedVar' :: HasFreeVars a => Int -> a -> x -> Maybe x
usedVar' a b s | usedVar a b = Just s
               | otherwise = Nothing

shLam :: Maybe String -> Binder -> Doc -> Doc -> Doc
shLam usedVar h a b = shLam_ usedVar h (Just a) b

simpleFo :: Doc -> Doc
simpleFo (DExpand x _) = x
simpleFo x = x

shLam_ :: Maybe String -> Binder -> Maybe Doc -> Doc -> Doc
shLam_ Nothing (BPi Hidden) (Just ((simpleFo -> DText "'CW") `DApp` a)) b = DFreshName Nothing $ showContext (DUp 0 a) b
  where
    showContext :: Doc -> Doc -> Doc
    showContext x (DFreshName u d) = DFreshName u $ showContext (DUp 0 x) d
    showContext x (DParContext xs y) = DParContext (DComma x xs) y
    showContext x (DContext xs y) = DParContext (DComma x xs) y
    showContext x y = DContext x y

shLam_ usedVar h a b = DFreshName usedVar $ lam (p $ DUp 0 <$> a) b
  where
    lam :: Doc -> Doc -> Doc
    lam = case h of
        BPi Visible
            | isJust usedVar   -> showForall "->"
            | otherwise -> shArr
        BPi Hidden
            | isJust usedVar   -> showForall "."
            | otherwise -> showContext
        _ -> showLam

    shAnn' :: Doc -> Maybe Doc -> Doc
    shAnn' a = maybe a (shAnn a)

    p :: Maybe Doc -> Doc
    p = case h of
        BMeta -> shAnn' (blue $ DVar 0)
        BLam Hidden -> DAt . shAnn' (DVar 0)
        BLam Visible -> shAnn' (DVar 0)
        _ -> ann

    ann :: Maybe Doc -> Doc
    ann | isJust usedVar = shAnn' (DVar 0)
        | otherwise = fromMaybe (text "Type")

    showForall :: String -> Doc -> Doc -> Doc
    showForall s x (DFreshName u d) = DFreshName u $ showForall s (DUp 0 x) d
    showForall s x (DForall s' xs y) | s == s' = DForall s (DSep (InfixR 11) x xs) y
    showForall s x y = DForall s x y

    showContext :: Doc -> Doc -> Doc
    showContext x y = DContext' x y

showLam :: Doc -> Doc -> Doc
showLam x (DFreshName u d) = DFreshName u $ showLam (DUp 0 x) d
showLam x (DLam xs y) = DLam (DSep (InfixR 11) x xs) y
showLam x y = DLam x y

shLet :: Int -> Doc -> Doc -> Doc
shLet i a b = DLet' (DLet "=" (blue $ shVar i) $ DUp i a) (DUp i b)

showLet :: Doc -> Doc -> Doc
showLet x (DFreshName u d) = DFreshName u $ showLet (DUp 0 x) d
showLet x (DLet' xs y) = DLet' (DSemi x xs) y
showLet x y = DLet' x y

shLet_ :: Doc -> Doc -> Doc
shLet_ a b = DFreshName (Just "") $ showLet (DLet "=" (shVar 0) $ DUp 0 a) b

-------------------------------------------------------------------------------- statement

data Stmt
    = StmtLet SIName SExp
    | Data SIName [(Visibility, SExp)]{-parameters-} SExp{-type-} [(SIName, SExp)]{-constructor names and types-}
    | PrecDef SIName Fixity
    deriving Generic

instance Binary Stmt

pattern StLet :: SIName -> Maybe (SExp' Void) -> SExp' Void -> Stmt
pattern StLet n mt x <- StmtLet n (getSAnn -> (x, mt))
  where StLet n mt x =  StmtLet n $ maybe x (SAnn x) mt

getSAnn :: SExp' a -> (SExp' a, Maybe (SExp' a))
getSAnn (SAnn x t) = (x, Just t)
getSAnn x = (x, Nothing)

pattern Primitive :: SIName -> SExp' Void -> Stmt
pattern Primitive n t = StLet n (Just t) (SBuiltin Fundefined)

instance PShow Stmt where
    pShow stmt = vcat . map DResetFreshNames $ case stmt of
        Primitive n t -> pure $ shAnn (pShow n) (pShow t)
        StLet n ty e -> [shAnn (pShow n) (pShow t) | Just t <- [ty]] ++ [DLet "=" (pShow n) (pShow e)]
        Data n ps ty cs -> pure $ nest 2 $ "data" <+> nest 2 (shAnn (foldl DApp (DTypeNamespace True $ pShow n) [shAnn (text "_") (pShow t) | (v, t) <- ps]) (pShow ty)) </> "where" <> nest 2 (hardline <> vcat [shAnn (pShow n) $ pShow $ UncurryS (first (const Hidden) <$> ps) t | (n, t) <- cs])
        PrecDef n i -> pure $ pShow i <+> text (sName n) --DOp0 (sName n) i

instance DeBruijnify SIName Stmt where
    deBruijnify_ k v = \case
        StmtLet sn e -> StmtLet sn (deBruijnify_ k v e)
        x@PrecDef{} -> x
        x -> error $ "deBruijnify @ " ++ ppShow x

-------------------------------------------------------------------------------- module

data Module_ a = Module
    { extensions    :: Extensions
    , moduleImports :: [(SIName, ImportItems)]
    , moduleExports :: Maybe [Export]
    , definitions   :: a
    }

data Export = ExportModule SIName | ExportId SIName

data ImportItems
    = ImportAllBut [SIName]
    | ImportJust [SIName]

type Extensions = [Extension]

data Extension
    = NoImplicitPrelude
    | TraceTypeCheck
    deriving (Enum, Eq, Ord, Show)

extensionMap :: Map.Map String Extension
extensionMap = Map.fromList $ map (show &&& id) [toEnum 0 .. ]