{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
-- | The Eidos-level builtin signature table (doc\/eidos.md §7, doc\/synolon.md §6): the
--   signature scheme every 'Prim' occurrence must instantiate, and the
--   one-way matcher the linter checks occurrences with.
--
--   Matching is first-order and unification-free: scheme variables bind
--   to the occurrence type's subterms, bindings must agree (up to
--   'natNorm'), and everything else compares structurally. Type-level
--   arithmetic on the scheme side (@Vec ((i + n) + m) a@ and the like)
--   cannot be inverted by matching, so arithmetic subterms become
--   deferred equations, checked only when substitution makes both sides
--   nat-closed and skipped otherwise — the check is deliberately partial
--   there (sound: it never rejects a correct instance).
--
--   A builtin with no recorded signature ('Nothing') has its occurrence
--   types trusted, as all builtins were before this table existed:
--   currently only 'Extern' (its parameter-list type is legacy-shaped).
module ReWire.Eidos.BuiltinSigs (builtinSig, matchesSig) where

import ReWire.Annotation (Annote (MsgAnnote))
import ReWire.Builtins (Builtin (..))
import ReWire.Eidos.Syntax
import ReWire.Eidos.Types (natNorm, tyEq, evalNat, substTv, flattenTyApp)

import Data.HashMap.Strict (HashMap)

import qualified Data.HashMap.Strict as Map
import qualified Data.HashSet        as Set

-- | Does the occurrence type instantiate the signature scheme?
matchesSig :: Sig -> Ty -> Bool
matchesSig :: Sig -> Ty -> Bool
matchesSig (Sig [TyVar]
tvs Ty
sigT) Ty
t = case Ty
-> Ty
-> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
go Ty
sigT (Ty -> Ty
natNorm Ty
t) (HashMap TyVar Ty
forall k v. HashMap k v
Map.empty, []) of
      Maybe (HashMap TyVar Ty, [(Ty, Ty)])
Nothing           -> Bool
False
      Just (HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs) -> ((Ty, Ty) -> Bool) -> [(Ty, Ty)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (HashMap TyVar Ty -> (Ty, Ty) -> Bool
checkDeferred HashMap TyVar Ty
bnds) [(Ty, Ty)]
defs
      where vs :: HashSet TyVar
vs = [TyVar] -> HashSet TyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
Set.fromList [TyVar]
tvs

            go :: Ty -> Ty -> (HashMap TyVar Ty, [(Ty, Ty)]) -> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
            go :: Ty
-> Ty
-> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
go Ty
s Ty
tgt (HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs) = case Ty
s of
                  TyVarT Annote
_ TyVar
v | TyVar
v TyVar -> HashSet TyVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`Set.member` HashSet TyVar
vs -> case TyVar -> HashMap TyVar Ty -> Maybe Ty
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup TyVar
v HashMap TyVar Ty
bnds of
                        Maybe Ty
Nothing -> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a. a -> Maybe a
Just (TyVar -> Ty -> HashMap TyVar Ty -> HashMap TyVar Ty
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert TyVar
v Ty
tgt HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs)
                        Just Ty
t0 -> if Ty -> Ty -> Bool
tyEq Ty
t0 Ty
tgt then (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a. a -> Maybe a
Just (HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs) else Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a. Maybe a
Nothing
                  Ty
_ | Ty -> Bool
isNatArith Ty
s -> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a. a -> Maybe a
Just (HashMap TyVar Ty
bnds, (Ty
s, Ty
tgt) (Ty, Ty) -> [(Ty, Ty)] -> [(Ty, Ty)]
forall a. a -> [a] -> [a]
: [(Ty, Ty)]
defs)
                  Arrow Annote
_ Ty
s1 Ty
s2 | Arrow Annote
_ Ty
t1 Ty
t2 <- Ty
tgt -> Ty
-> Ty
-> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
go Ty
s1 Ty
t1 (HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs) Maybe (HashMap TyVar Ty, [(Ty, Ty)])
-> ((HashMap TyVar Ty, [(Ty, Ty)])
    -> Maybe (HashMap TyVar Ty, [(Ty, Ty)]))
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ty
-> Ty
-> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
go Ty
s2 Ty
t2
                  TyApp Annote
_ Ty
s1 Ty
s2 | TyApp Annote
_ Ty
t1 Ty
t2 <- Ty
tgt -> Ty
-> Ty
-> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
go Ty
s1 Ty
t1 (HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs) Maybe (HashMap TyVar Ty, [(Ty, Ty)])
-> ((HashMap TyVar Ty, [(Ty, Ty)])
    -> Maybe (HashMap TyVar Ty, [(Ty, Ty)]))
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Ty
-> Ty
-> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
go Ty
s2 Ty
t2
                  TyCon Annote
_ Text
c     | TyCon Annote
_ Text
c'    <- Ty
tgt, Text
c Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
c' -> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a. a -> Maybe a
Just (HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs)
                  TyNat Annote
_ Natural
n     | TyNat Annote
_ Natural
n'    <- Ty
tgt, Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n' -> (HashMap TyVar Ty, [(Ty, Ty)])
-> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a. a -> Maybe a
Just (HashMap TyVar Ty
bnds, [(Ty, Ty)]
defs)
                  Ty
_ -> Maybe (HashMap TyVar Ty, [(Ty, Ty)])
forall a. Maybe a
Nothing

            -- An application of the built-in nat arithmetic constructors
            -- (doc/eidos.md §3.1) — deferred rather than decomposed.
            isNatArith :: Ty -> Bool
            isNatArith :: Ty -> Bool
isNatArith Ty
ty = case Ty -> (Ty, [Ty])
flattenTyApp Ty
ty of
                  (TyCon Annote
_ Text
c, Ty
_ : [Ty]
_) -> Text
c Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ([Text
"+", Text
"-", Text
"*"] :: [TyConId])
                  (Ty, [Ty])
_                  -> Bool
False

            checkDeferred :: HashMap TyVar Ty -> (Ty, Ty) -> Bool
            checkDeferred :: HashMap TyVar Ty -> (Ty, Ty) -> Bool
checkDeferred HashMap TyVar Ty
bnds (Ty
s, Ty
tgt) = case (Ty -> Maybe Natural
evalNat (Ty -> Maybe Natural) -> Ty -> Maybe Natural
forall a b. (a -> b) -> a -> b
$ HashMap TyVar Ty -> Ty -> Ty
substTv HashMap TyVar Ty
bnds Ty
s, Ty -> Maybe Natural
evalNat Ty
tgt) of
                  (Just Natural
n, Just Natural
n') -> Natural
n Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
n'
                  (Maybe Natural, Maybe Natural)
_                 -> Bool
True -- open on either side: unchecked.

-- | The signature scheme of each builtin (doc\/eidos.md §7, doc\/synolon.md §6).
builtinSig :: Builtin -> Maybe Sig
builtinSig :: Builtin -> Maybe Sig
builtinSig = \ case
      Builtin
Error           -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
string Ty -> Ty -> Ty
--> Ty
va
      Builtin
Extern          -> Maybe Sig
forall a. Maybe a
Nothing
      Builtin
Cryptol         -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
string Ty -> Ty -> Ty
--> Ty
string Ty -> Ty -> Ty
--> Ty
va Ty -> Ty -> Ty
--> Ty
va
      Builtin
Bind            -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
mM, TyVar
aS, TyVar
bS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> Ty -> Ty
TyApp Annote
an Ty
vm Ty
va Ty -> Ty -> Ty
--> (Ty
va Ty -> Ty -> Ty
--> Annote -> Ty -> Ty -> Ty
TyApp Annote
an Ty
vm Ty
vb) Ty -> Ty -> Ty
--> Annote -> Ty -> Ty -> Ty
TyApp Annote
an Ty
vm Ty
vb
      Builtin
Return          -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
mM, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
va Ty -> Ty -> Ty
--> Annote -> Ty -> Ty -> Ty
TyApp Annote
an Ty
vm Ty
va
      Builtin
Put             -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
sS, TyVar
mM] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
vs Ty -> Ty -> Ty
--> Ty -> Ty -> Ty -> Ty
stateT Ty
vs Ty
vm Ty
unit
      Builtin
Get             -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
sS, TyVar
mM] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty -> Ty -> Ty
stateT Ty
vs Ty
vm Ty
vs
      Builtin
Signal          -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
oS, TyVar
iS, TyVar
mM] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
vo Ty -> Ty -> Ty
--> Ty -> Ty -> Ty -> Ty -> Ty
reacT Ty
vi Ty
vo Ty
vm Ty
vi
      Builtin
Lift            -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
tT, TyVar
mM, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Ty -> Ty -> Ty
TyApp Annote
an Ty
vm Ty
va Ty -> Ty -> Ty
--> Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an Ty
vt Ty
vm) Ty
va
      Builtin
Extrude         -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
iS, TyVar
oS, TyVar
sS, TyVar
mM, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty -> Ty -> Ty -> Ty
reacT Ty
vi Ty
vo (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
"StateT") Ty
vs) Ty
vm) Ty
va Ty -> Ty -> Ty
--> Ty
vs Ty -> Ty -> Ty
--> Ty -> Ty -> Ty -> Ty -> Ty
reacT Ty
vi Ty
vo Ty
vm Ty
va
      Builtin
VecFromList     -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
list Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
va
      Builtin
VecReplicate    -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
va
      Builtin
VecReverse      -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty -> Ty
vec Ty
vn Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
va
      Builtin
VecSlice        -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
iN, TyVar
nN, TyVar
mN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
proxy Ty
vi' Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec (Ty -> Ty -> Ty
plus (Ty -> Ty -> Ty
plus Ty
vi' Ty
vn) Ty
vm') Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
va
      Builtin
VecRSlice       -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
iN, TyVar
nN, TyVar
mN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
proxy Ty
vi' Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec (Ty -> Ty -> Ty
plus (Ty -> Ty -> Ty
plus Ty
vi' Ty
vn) Ty
vm') Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
va
      Builtin
VecIndex        -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty -> Ty
vec Ty
vn Ty
va Ty -> Ty -> Ty
--> Ty -> Ty
finite Ty
vn Ty -> Ty -> Ty
--> Ty
va
      Builtin
VecIndexProxy   -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
mN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty -> Ty
vec (Ty -> Ty -> Ty
plus (Ty -> Ty -> Ty
plus Ty
vn Ty
vm') (Annote -> Natural -> Ty
TyNat Annote
an Natural
1)) Ty
va Ty -> Ty -> Ty
--> Ty -> Ty
proxy Ty
vn Ty -> Ty -> Ty
--> Ty
va
      Builtin
VecConcat       -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
mN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty -> Ty
vec Ty
vn Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vm' Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec (Ty -> Ty -> Ty
plus Ty
vn Ty
vm') Ty
va
      Builtin
VecMap          -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
aS, TyVar
bS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ (Ty
va Ty -> Ty -> Ty
--> Ty
vb) Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
va Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
vb
      Builtin
VecGenerate     -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
aS] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ (Ty -> Ty
finite Ty
vn Ty -> Ty -> Ty
--> Ty
va) Ty -> Ty -> Ty
--> Ty -> Ty -> Ty
vec Ty
vn Ty
va
      Builtin
Finite          -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
integer Ty -> Ty -> Ty
--> Ty -> Ty
finite Ty
vn
      Builtin
FiniteMinBound  -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
finite Ty
vn
      Builtin
FiniteMaxBound  -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
finite Ty
vn
      Builtin
ToFinite        -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
mN, TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vm' Ty -> Ty -> Ty
--> Ty -> Ty
finite Ty
vn
      Builtin
ToFiniteMod     -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
mN, TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vm' Ty -> Ty -> Ty
--> Ty -> Ty
finite Ty
vn
      Builtin
FromFinite      -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN, TyVar
mN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
finite Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
bVec Ty
vm'
      Builtin
NatVal          -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
proxy Ty
vn Ty -> Ty -> Ty
--> Ty
integer
      Builtin
Bits            -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty
integer Ty -> Ty -> Ty
--> Ty -> Ty
bVec (Annote -> Natural -> Ty
TyNat Annote
an Natural
128)
      Builtin
Resize          -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
mN, TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
bVec Ty
vm'
      Builtin
BitSlice        -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
mN, TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
finite Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
finite Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
bVec Ty
vm'
      Builtin
BitIndex        -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
finite Ty
vn Ty -> Ty -> Ty
--> Ty
bool
      Builtin
Add             -> Maybe Sig
binOp
      Builtin
Sub             -> Maybe Sig
binOp
      Builtin
Mul             -> Maybe Sig
binOp
      Builtin
Div             -> Maybe Sig
binOp
      Builtin
Mod             -> Maybe Sig
binOp
      Builtin
Pow             -> Maybe Sig
binOp
      Builtin
LAnd            -> Maybe Sig
cmpOp
      Builtin
LOr             -> Maybe Sig
cmpOp
      Builtin
And             -> Maybe Sig
binOp
      Builtin
Or              -> Maybe Sig
binOp
      Builtin
XOr             -> Maybe Sig
binOp
      Builtin
XNor            -> Maybe Sig
binOp
      Builtin
LShift          -> Maybe Sig
binOp
      Builtin
RShift          -> Maybe Sig
binOp
      Builtin
RShiftArith     -> Maybe Sig
binOp
      Builtin
Eq              -> Maybe Sig
cmpOp
      Builtin
Gt              -> Maybe Sig
cmpOp
      Builtin
GtEq            -> Maybe Sig
cmpOp
      Builtin
Lt              -> Maybe Sig
cmpOp
      Builtin
LtEq            -> Maybe Sig
cmpOp
      Builtin
LNot            -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty
bool
      Builtin
Not             -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
bVec Ty
vn
      Builtin
RAnd            -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty
bool
      Builtin
ROr             -> Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty
bool
      Builtin
RNAnd           -> Maybe Sig
redOp
      Builtin
RNor            -> Maybe Sig
redOp
      Builtin
RXOr            -> Maybe Sig
redOp
      Builtin
RXNor           -> Maybe Sig
redOp
      Builtin
MSBit           -> Maybe Sig
redOp
      where an :: Annote
            an :: Annote
an = Text -> Annote
MsgAnnote Text
"builtin signature"

            -- Table type variables: negative uniques, per the primitive
            -- basis convention (these signatures are only matched
            -- against, never inserted into programs).
            kmonad :: Kind
kmonad = Kind
KStar Kind -> Kind -> Kind
`KFun` Kind
KStar

            nN :: TyVar
nN  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"n" (-Uniq
9001) Kind
KNat
            mN :: TyVar
mN  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"m" (-Uniq
9002) Kind
KNat
            iN :: TyVar
iN  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"i" (-Uniq
9003) Kind
KNat
            aS :: TyVar
aS  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"a" (-Uniq
9004) Kind
KStar
            bS :: TyVar
bS  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"b" (-Uniq
9005) Kind
KStar
            sS :: TyVar
sS  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"s" (-Uniq
9006) Kind
KStar
            oS :: TyVar
oS  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"o" (-Uniq
9007) Kind
KStar
            iS :: TyVar
iS  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"i" (-Uniq
9008) Kind
KStar
            mM :: TyVar
mM  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"m" (-Uniq
9009) Kind
kmonad
            tT :: TyVar
tT  = Text -> Uniq -> Kind -> TyVar
TyVar Text
"t" (-Uniq
9010) (Kind -> TyVar) -> Kind -> TyVar
forall a b. (a -> b) -> a -> b
$ Kind
kmonad Kind -> Kind -> Kind
`KFun` Kind
kmonad

            vn :: Ty
vn  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
nN
            vm' :: Ty
vm' = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
mN
            vi' :: Ty
vi' = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
iN
            va :: Ty
va  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
aS
            vb :: Ty
vb  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
bS
            vs :: Ty
vs  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
sS
            vo :: Ty
vo  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
oS
            vi :: Ty
vi  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
iS
            vm :: Ty
vm  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
mM
            vt :: Ty
vt  = Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
tT

            infixr 1 -->
            --> :: Ty -> Ty -> Ty
(-->) = Annote -> Ty -> Ty -> Ty
Arrow Annote
an

            bool :: Ty
bool    = Annote -> Text -> Ty
TyCon Annote
an Text
"Bool"
            unit :: Ty
unit    = Annote -> Text -> Ty
TyCon Annote
an Text
"()"
            string :: Ty
string  = Annote -> Text -> Ty
TyCon Annote
an Text
"String"
            integer :: Ty
integer = Annote -> Text -> Ty
TyCon Annote
an Text
"Integer"

            vec :: Ty -> Ty -> Ty
vec Ty
n Ty
t    = Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
"Vec") Ty
n) Ty
t
            bVec :: Ty -> Ty
bVec Ty
n     = Ty -> Ty -> Ty
vec Ty
n Ty
bool
            list :: Ty -> Ty
list       = Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Ty -> Ty -> Ty) -> Ty -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon Annote
an Text
"[_]"
            proxy :: Ty -> Ty
proxy      = Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Ty -> Ty -> Ty) -> Ty -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon Annote
an Text
"Proxy"
            finite :: Ty -> Ty
finite     = Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Ty -> Ty -> Ty) -> Ty -> Ty -> Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon Annote
an Text
"Finite"
            plus :: Ty -> Ty -> Ty
plus Ty
t1 Ty
t2 = Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
"+") Ty
t1) Ty
t2

            stateT :: Ty -> Ty -> Ty -> Ty
stateT Ty
s Ty
m Ty
t    = Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
"StateT") Ty
s) Ty
m) Ty
t
            reacT :: Ty -> Ty -> Ty -> Ty -> Ty
reacT Ty
i Ty
o Ty
m Ty
t   = Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
"ReacT") Ty
i) Ty
o) Ty
m) Ty
t

            -- Vec n Bool -> Vec n Bool -> Vec n Bool
            binOp :: Maybe Sig
binOp = Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
bVec Ty
vn
            -- Vec n Bool -> Vec n Bool -> Bool
            cmpOp :: Maybe Sig
cmpOp = Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty -> Ty
bVec Ty
vn Ty -> Ty -> Ty
--> Ty
bool
            -- Vec (1 + n) Bool -> Bool
            redOp :: Maybe Sig
redOp = Sig -> Maybe Sig
forall a. a -> Maybe a
Just (Sig -> Maybe Sig) -> Sig -> Maybe Sig
forall a b. (a -> b) -> a -> b
$ [TyVar] -> Ty -> Sig
Sig [TyVar
nN] (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Ty -> Ty
bVec (Ty -> Ty -> Ty
plus (Annote -> Natural -> Ty
TyNat Annote
an Natural
1) Ty
vn) Ty -> Ty -> Ty
--> Ty
bool