{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
-- | The primitive datatype basis for Eidos programs: the built-in type
--   constructors (with their data constructors, where they have any) that
--   bridged programs may reference without declaring — the unit and tuple
--   families, Bool, Maybe/Either (base names, as the bridge emits them),
--   the abstract width-bearing types (Vec, Finite, Proxy), and the reactive
--   stack types (which exist in Eidos only; Synolon's type grammar bans
--   them). The bridge prepends these to every program so the linter can
--   resolve constructor occurrences.
--
--   The basis' type-variable uniques are NEGATIVE: the bridge mints
--   non-negative uniques, so basis binders can never collide with program
--   binders (the uniqueness lint checks both together).
module ReWire.Eidos.PrimBasis (primDatas, addPrims) where

import ReWire.Annotation (Annote (MsgAnnote))
import ReWire.Eidos.Syntax

import Data.Text (Text)

import qualified Data.Text as T

-- | Prepend the primitive basis (dropping any duplicate declarations, which
--   the bridge does not produce but hand-written .eir might).
addPrims :: Program -> Program
addPrims :: Program -> Program
addPrims Program
p = Program
p { progDatas = primDatas <> filter ((`notElem` map dataName primDatas) . dataName) (progDatas p) }

primDatas :: [DataDefn]
primDatas :: [DataDefn]
primDatas =
      [ Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"()"       Kind
KStar                                                [Text -> Text -> DataCon
nullCtor Text
"()" Text
"()"]
      -- (The type-level arithmetic constructors +, -, * are recognized by
      -- name in evalNat/natNorm and need no declaration; their kinds
      -- construct Nat, not *, so they are not datatypes.)
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"Bool"     Kind
KStar                                                [Text -> Text -> DataCon
nullCtor Text
"False" Text
"Bool", Text -> Text -> DataCon
nullCtor Text
"True" Text
"Bool"]
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"ExtDev"   (Kind
KStar Kind -> Kind -> Kind
`KFun` (Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar))                  []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"Finite"   (Kind
KNat Kind -> Kind -> Kind
`KFun` Kind
KStar)                                  []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"Identity" Kind
kmonad                                               []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"Integer"  Kind
KStar                                                []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"Proxy"    (Kind
KNat Kind -> Kind -> Kind
`KFun` Kind
KStar)                                  [DataCon
proxyCtor]
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"ReacT"    (Kind
KStar Kind -> Kind -> Kind
`KFun` (Kind
KStar Kind -> Kind -> Kind
`KFun` (Kind
kmonad Kind -> Kind -> Kind
`KFun` Kind
kmonad))) []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"StateT"   (Kind
KStar Kind -> Kind -> Kind
`KFun` (Kind
kmonad Kind -> Kind -> Kind
`KFun` Kind
kmonad))                []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"String"   Kind
KStar                                                []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"Vec"      (Kind
KNat Kind -> Kind -> Kind
`KFun` (Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar))                   []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"[_]"      (Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar)                                 []
      , Text -> Kind -> [DataCon] -> DataDefn
mkData Text
"[]"       (Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar)                                 []
      , DataDefn
maybeData
      , DataDefn
eitherData
      ]
      [DataDefn] -> [DataDefn] -> [DataDefn]
forall a. Semigroup a => a -> a -> a
<> (Uniq -> DataDefn) -> [Uniq] -> [DataDefn]
forall a b. (a -> b) -> [a] -> [b]
map Uniq -> DataDefn
mkTuple [Uniq
2 .. Uniq
62]
      where kmonad :: Kind
            kmonad :: Kind
kmonad = Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar

an :: Text -> Annote
an :: Text -> Annote
an Text
n = Text -> Annote
MsgAnnote (Text -> Annote) -> Text -> Annote
forall a b. (a -> b) -> a -> b
$ Text
"Prim: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n

mkData :: TyConId -> Kind -> [DataCon] -> DataDefn
mkData :: Text -> Kind -> [DataCon] -> DataDefn
mkData Text
n = Annote -> Text -> Kind -> [DataCon] -> DataDefn
DataDefn (Text -> Annote
an Text
n) Text
n

nullCtor :: DataConId -> TyConId -> DataCon
nullCtor :: Text -> Text -> DataCon
nullCtor Text
c Text
t = Annote -> Text -> Sig -> DataCon
DataCon (Text -> Annote
an Text
c) Text
c (Sig -> DataCon) -> Sig -> DataCon
forall a b. (a -> b) -> a -> b
$ Ty -> Sig
monoSig (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon (Text -> Annote
an Text
t) Text
t

-- | Basis type variables: negative uniques, disjoint per declaration (each
--   declaration gets a distinct hundred).
basisTv :: Int -> Int -> Text -> Kind -> TyVar
basisTv :: Uniq -> Uniq -> Text -> Kind -> TyVar
basisTv Uniq
decl Uniq
i Text
x = Text -> Uniq -> Kind -> TyVar
TyVar Text
x (Uniq -> Uniq
forall a. Num a => a -> a
negate (Uniq -> Uniq) -> Uniq -> Uniq
forall a b. (a -> b) -> a -> b
$ Uniq
decl Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
* Uniq
100 Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
+ Uniq
i Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
+ Uniq
1)

proxyCtor :: DataCon
proxyCtor :: DataCon
proxyCtor = Annote -> Text -> Sig -> DataCon
DataCon (Text -> Annote
an Text
"Proxy") Text
"Proxy" (Sig -> DataCon) -> Sig -> DataCon
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
n] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> Ty -> Ty
TyApp Annote
a (Annote -> Text -> Ty
TyCon Annote
a Text
"Proxy") (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> TyVar -> Ty
TyVarT Annote
a TyVar
n
      where a :: Annote
a = Text -> Annote
an Text
"Proxy"
            n :: TyVar
n = Uniq -> Uniq -> Text -> Kind -> TyVar
basisTv Uniq
1 Uniq
0 Text
"n" Kind
KNat

maybeData :: DataDefn
maybeData :: DataDefn
maybeData = Annote -> Text -> Kind -> [DataCon] -> DataDefn
DataDefn Annote
a Text
"GHC.Internal.Maybe.Maybe" (Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar)
      [ Annote -> Text -> Sig -> DataCon
DataCon Annote
a Text
"GHC.Internal.Maybe.Nothing" (Sig -> DataCon) -> Sig -> DataCon
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
tv] Ty
mt
      , Annote -> Text -> Sig -> DataCon
DataCon Annote
a Text
"GHC.Internal.Maybe.Just"    (Sig -> DataCon) -> Sig -> DataCon
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
tv] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> Ty -> Ty
Arrow Annote
a (Annote -> TyVar -> Ty
TyVarT Annote
a TyVar
tv) Ty
mt
      ]
      where a :: Annote
a  = Text -> Annote
an Text
"Maybe"
            tv :: TyVar
tv = Uniq -> Uniq -> Text -> Kind -> TyVar
basisTv Uniq
2 Uniq
0 Text
"a" Kind
KStar
            mt :: Ty
mt = Annote -> Ty -> Ty -> Ty
TyApp Annote
a (Annote -> Text -> Ty
TyCon Annote
a Text
"GHC.Internal.Maybe.Maybe") (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> TyVar -> Ty
TyVarT Annote
a TyVar
tv

eitherData :: DataDefn
eitherData :: DataDefn
eitherData = Annote -> Text -> Kind -> [DataCon] -> DataDefn
DataDefn Annote
a Text
"GHC.Internal.Data.Either.Either" (Kind
KStar Kind -> Kind -> Kind
`KFun` (Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar))
      [ Annote -> Text -> Sig -> DataCon
DataCon Annote
a Text
"GHC.Internal.Data.Either.Left"  (Sig -> DataCon) -> Sig -> DataCon
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
tva, TyVar
tvb] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> Ty -> Ty
Arrow Annote
a (Annote -> TyVar -> Ty
TyVarT Annote
a TyVar
tva) Ty
et
      , Annote -> Text -> Sig -> DataCon
DataCon Annote
a Text
"GHC.Internal.Data.Either.Right" (Sig -> DataCon) -> Sig -> DataCon
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
tva, TyVar
tvb] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> Ty -> Ty
Arrow Annote
a (Annote -> TyVar -> Ty
TyVarT Annote
a TyVar
tvb) Ty
et
      ]
      where a :: Annote
a   = Text -> Annote
an Text
"Either"
            tva :: TyVar
tva = Uniq -> Uniq -> Text -> Kind -> TyVar
basisTv Uniq
3 Uniq
0 Text
"a" Kind
KStar
            tvb :: TyVar
tvb = Uniq -> Uniq -> Text -> Kind -> TyVar
basisTv Uniq
3 Uniq
1 Text
"b" Kind
KStar
            et :: Ty
et  = Annote -> Ty -> Ty -> Ty
TyApp Annote
a (Annote -> Ty -> Ty -> Ty
TyApp Annote
a (Annote -> Text -> Ty
TyCon Annote
a Text
"GHC.Internal.Data.Either.Either") (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> TyVar -> Ty
TyVarT Annote
a TyVar
tva) (Ty -> Ty) -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> TyVar -> Ty
TyVarT Annote
a TyVar
tvb

mkTuple :: Int -> DataDefn
mkTuple :: Uniq -> DataDefn
mkTuple Uniq
n = Annote -> Text -> Kind -> [DataCon] -> DataDefn
DataDefn Annote
a Text
name Kind
k [Annote -> Text -> Sig -> DataCon
DataCon Annote
a Text
name (Sig -> DataCon) -> Sig -> DataCon
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar]
tvs (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ (TyVar -> Ty -> Ty) -> Ty -> [TyVar] -> Ty
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Annote -> Ty -> Ty -> Ty
Arrow Annote
a (Ty -> Ty -> Ty) -> (TyVar -> Ty) -> TyVar -> Ty -> Ty
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annote -> TyVar -> Ty
TyVarT Annote
a) Ty
rt [TyVar]
tvs]
      where name :: Text
name = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Uniq -> Text -> Text
T.replicate (Uniq
n Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
- Uniq
1) Text
"," Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
            a :: Annote
a    = Text -> Annote
an Text
"tuple"
            tvs :: [TyVar]
tvs  = [ Uniq -> Uniq -> Text -> Kind -> TyVar
basisTv (Uniq
10 Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
+ Uniq
n) Uniq
i (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Uniq -> String
tvName Uniq
i) Kind
KStar | Uniq
i <- [Uniq
0 .. Uniq
n Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
- Uniq
1] ]
            k :: Kind
k    = (Kind -> Kind -> Kind) -> Kind -> [Kind] -> Kind
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Kind -> Kind -> Kind
KFun Kind
KStar ([Kind] -> Kind) -> [Kind] -> Kind
forall a b. (a -> b) -> a -> b
$ Uniq -> Kind -> [Kind]
forall a. Uniq -> a -> [a]
replicate Uniq
n Kind
KStar
            rt :: Ty
rt   = (Ty -> Ty -> Ty) -> Ty -> [Ty] -> Ty
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Annote -> Ty -> Ty -> Ty
TyApp Annote
a) (Annote -> Text -> Ty
TyCon Annote
a Text
name) ([Ty] -> Ty) -> [Ty] -> Ty
forall a b. (a -> b) -> a -> b
$ (TyVar -> Ty) -> [TyVar] -> [Ty]
forall a b. (a -> b) -> [a] -> [b]
map (Annote -> TyVar -> Ty
TyVarT Annote
a) [TyVar]
tvs

            tvName :: Int -> String
            tvName :: Uniq -> String
tvName Uniq
i | Uniq
i Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
< Uniq
26    = [Uniq -> Char
forall a. Enum a => Uniq -> a
toEnum (Uniq -> Char) -> Uniq -> Char
forall a b. (a -> b) -> a -> b
$ Char -> Uniq
forall a. Enum a => a -> Uniq
fromEnum Char
'a' Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
+ Uniq
i]
                     | Bool
otherwise = Char
't' Char -> String -> String
forall a. a -> [a] -> [a]
: Uniq -> String
forall a. Show a => a -> String
show Uniq
i