{-|
Module: Types
Description: Type inference and checking
Author: gatlin@niltag.net

This is still a work in progress.

= No really, what's this type system?

Eventually? I want

* Linear
* call-by-push-value with
* arbitrary rank type and kind polymorphism and
* graded (co)effects.

Papers and posts I am cribbing from:

* https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf
* https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly_constraints/src/Infer.hs
* https://cs-people.bu.edu/gaboardi/publication/GaboardiEtAlIicfp16.pdf
* others, stay tuned.

-}

{-# LANGUAGE DataKinds, PolyKinds, ExistentialQuantification, RankNTypes #-}
{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, StandaloneDeriving #-}

module Types
where

import Control.Monad
  ( foldM
  , forM
  , liftM2
  , mapAndUnzipM )
import Control.Monad.State
  (StateT(..)
  , evalStateT
  , get
  , gets
  , modify
  , put )
import Data.Functor.Identity (Identity(..))
import Control.Monad.Except (Except(..), ExceptT(..),runExcept,runExceptT,throwError)
import Control.Monad.Reader (ReaderT(..), runReaderT, ask, local)
import Control.Monad.Writer (WriterT, runWriterT, tell)
import Control.Comonad (Comonad(..), extract, extend)
import Data.Map (Map)
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Data.List (intersperse, intercalate, foldl', foldl1, nub)
import Data.Maybe (fromJust)
import qualified Data.Graph as G
import Text.Show.Unicode (ushow)
import Syntax (Symbol, Cbpv(..), CbpvExp, deps)
import Control.Comonad.Cofree (Cofree(..), unwrap)

-- * (basic) Type language

type TypeVar = Int

data Type
  = TVar TypeVar
  | TCon String
  | Type :-> Type
  | TForall [TypeVar] Type
  deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: Type -> Type -> Bool
Eq, Eq Type
Eq Type
-> (Type -> Type -> Ordering)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Bool)
-> (Type -> Type -> Type)
-> (Type -> Type -> Type)
-> Ord Type
Type -> Type -> Bool
Type -> Type -> Ordering
Type -> Type -> Type
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Type -> Type -> Type
$cmin :: Type -> Type -> Type
max :: Type -> Type -> Type
$cmax :: Type -> Type -> Type
>= :: Type -> Type -> Bool
$c>= :: Type -> Type -> Bool
> :: Type -> Type -> Bool
$c> :: Type -> Type -> Bool
<= :: Type -> Type -> Bool
$c<= :: Type -> Type -> Bool
< :: Type -> Type -> Bool
$c< :: Type -> Type -> Bool
compare :: Type -> Type -> Ordering
$ccompare :: Type -> Type -> Ordering
Ord)

instance Show Type where
  show :: Type -> Symbol
show (TVar TypeVar
n) = Symbol
"_" Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeVar -> Symbol
forall a. Show a => a -> Symbol
ushow TypeVar
n
  show (TCon Symbol
s) = Symbol
s
  show (TCon Symbol
"" :-> Type
t) = Symbol
"{ " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Symbol
forall a. Show a => a -> Symbol
ushow Type
t Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
" }"
  show (Type
t1 :-> Type
t2) = Type -> Symbol
forall a. Show a => a -> Symbol
ushow Type
t1 Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
" -> " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Symbol
forall a. Show a => a -> Symbol
ushow Type
t2
  show (TForall [] Type
t) = Type -> Symbol
forall a. Show a => a -> Symbol
ushow Type
t
  show (TForall [TypeVar]
tvs Type
t) = Symbol
"∀ " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
tvs' Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
". " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Symbol
forall a. Show a => a -> Symbol
ushow Type
t
    where tvs' :: Symbol
tvs' = [Symbol] -> Symbol
unwords ((TypeVar -> Symbol) -> [TypeVar] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\TypeVar
n -> Symbol
"_" Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeVar -> Symbol
forall a. Show a => a -> Symbol
ushow TypeVar
n) [TypeVar]
tvs)

-- these exist to remind us of constraints for now,
-- and in the future they may become type families of some sort
type Sigma = Type
type Rho = Type
type Tau = Type

tyInt, tyFloat, tyBool, tyBottom :: Rho
tyInt :: Type
tyInt = Symbol -> Type
TCon Symbol
"int"
tyFloat :: Type
tyFloat = Symbol -> Type
TCon Symbol
"float"
tyBool :: Type
tyBool = Symbol -> Type
TCon Symbol
"boolean"
tyBottom :: Type
tyBottom = Symbol -> Type
TCon Symbol
""

tyFunSig :: [Type] -> Type -> Type
tyFunSig :: [Type] -> Type -> Type
tyFunSig [Type]
args Type
ret = (Type -> Type -> Type) -> [Type] -> Type
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 ((Type -> Type -> Type) -> Type -> Type -> Type
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Type
(:->)) ([Type] -> Type) -> [Type] -> Type
forall a b. (a -> b) -> a -> b
$ Type
retType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
args

-- * Typing environment ("frame")

newtype Frame = Frame { Frame -> Map Symbol Type
types :: Map Symbol Type }
  deriving (Frame -> Frame -> Bool
(Frame -> Frame -> Bool) -> (Frame -> Frame -> Bool) -> Eq Frame
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Frame -> Frame -> Bool
$c/= :: Frame -> Frame -> Bool
== :: Frame -> Frame -> Bool
$c== :: Frame -> Frame -> Bool
Eq, TypeVar -> Frame -> ShowS
[Frame] -> ShowS
Frame -> Symbol
(TypeVar -> Frame -> ShowS)
-> (Frame -> Symbol) -> ([Frame] -> ShowS) -> Show Frame
forall a.
(TypeVar -> a -> ShowS)
-> (a -> Symbol) -> ([a] -> ShowS) -> Show a
showList :: [Frame] -> ShowS
$cshowList :: [Frame] -> ShowS
show :: Frame -> Symbol
$cshow :: Frame -> Symbol
showsPrec :: TypeVar -> Frame -> ShowS
$cshowsPrec :: TypeVar -> Frame -> ShowS
Show)

frameEmpty :: Frame
frameEmpty :: Frame
frameEmpty = Map Symbol Type -> Frame
Frame Map Symbol Type
forall k a. Map k a
M.empty

frameExtend :: Frame -> (Symbol, Type) -> Frame
frameExtend :: Frame -> (Symbol, Type) -> Frame
frameExtend Frame
frame (Symbol
x, Type
s) = Frame
frame { types :: Map Symbol Type
types = Symbol -> Type -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert Symbol
x Type
s (Frame -> Map Symbol Type
types Frame
frame) }

frameRemove :: Frame -> Symbol -> Frame
frameRemove :: Frame -> Symbol -> Frame
frameRemove (Frame Map Symbol Type
frame) Symbol
var = Map Symbol Type -> Frame
Frame (Symbol -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => k -> Map k a -> Map k a
M.delete Symbol
var Map Symbol Type
frame)

frameExtends :: Frame -> [(Symbol, Type)] -> Frame
frameExtends :: Frame -> [(Symbol, Type)] -> Frame
frameExtends Frame
frame [(Symbol, Type)]
xs = Frame
frame { types :: Map Symbol Type
types = Map Symbol Type -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union ([(Symbol, Type)] -> Map Symbol Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Symbol, Type)]
xs) (Frame -> Map Symbol Type
types Frame
frame) }

frameLookup :: Symbol -> Frame -> Maybe Type
frameLookup :: Symbol -> Frame -> Maybe Type
frameLookup Symbol
key (Frame Map Symbol Type
frame) = Symbol -> Map Symbol Type -> Maybe Type
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Symbol
key Map Symbol Type
frame

frameMerge :: Frame -> Frame -> Frame
frameMerge :: Frame -> Frame -> Frame
frameMerge (Frame Map Symbol Type
a) (Frame Map Symbol Type
b) = Map Symbol Type -> Frame
Frame (Map Symbol Type -> Map Symbol Type -> Map Symbol Type
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union Map Symbol Type
a Map Symbol Type
b)

framesMerge :: [Frame] -> Frame
framesMerge :: [Frame] -> Frame
framesMerge = (Frame -> Frame -> Frame) -> Frame -> [Frame] -> Frame
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Frame -> Frame -> Frame
frameMerge Frame
frameEmpty

frameSingleton :: Symbol -> Type -> Frame
frameSingleton :: Symbol -> Type -> Frame
frameSingleton Symbol
x Type
y = Map Symbol Type -> Frame
Frame (Symbol -> Type -> Map Symbol Type
forall k a. k -> a -> Map k a
M.singleton Symbol
x Type
y)

frameKeys :: Frame -> [Symbol]
frameKeys :: Frame -> [Symbol]
frameKeys (Frame Map Symbol Type
frame) = Map Symbol Type -> [Symbol]
forall k a. Map k a -> [k]
M.keys Map Symbol Type
frame

framesFromList :: [(Symbol, Type)] -> Frame
framesFromList :: [(Symbol, Type)] -> Frame
framesFromList [(Symbol, Type)]
xs = Map Symbol Type -> Frame
Frame ([(Symbol, Type)] -> Map Symbol Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Symbol, Type)]
xs)

framesToList :: Frame -> [(Symbol, Type)]
framesToList :: Frame -> [(Symbol, Type)]
framesToList (Frame Map Symbol Type
frame) = Map Symbol Type -> [(Symbol, Type)]
forall k a. Map k a -> [(k, a)]
M.toList Map Symbol Type
frame

instance Semigroup Frame where
  <> :: Frame -> Frame -> Frame
(<>) = Frame -> Frame -> Frame
frameMerge

instance Monoid Frame where
  mempty :: Frame
mempty = Frame
frameEmpty
  mappend :: Frame -> Frame -> Frame
mappend = Frame -> Frame -> Frame
forall a. Semigroup a => a -> a -> a
(<>)

-- * Inference monad

type Infer = ReaderT Frame (StateT InferState (Except String))
newtype InferState = InferState { InferState -> TypeVar
count :: Int }
defaultInferState :: InferState
defaultInferState = InferState :: TypeVar -> InferState
InferState { count :: TypeVar
count = TypeVar
0 }

runInfer :: Frame -> Infer a -> Either String a
runInfer :: forall a. Frame -> Infer a -> Either Symbol a
runInfer Frame
frame Infer a
m =
  Except Symbol a -> Either Symbol a
forall e a. Except e a -> Either e a
runExcept (Except Symbol a -> Either Symbol a)
-> Except Symbol a -> Either Symbol a
forall a b. (a -> b) -> a -> b
$ StateT InferState (ExceptT Symbol Identity) a
-> InferState -> Except Symbol a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Infer a -> Frame -> StateT InferState (ExceptT Symbol Identity) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Infer a
m Frame
frame) InferState
defaultInferState

-- * Constraint solving monad

newtype Subst = Subst (Map TypeVar Rho)
  deriving ( Subst -> Subst -> Bool
(Subst -> Subst -> Bool) -> (Subst -> Subst -> Bool) -> Eq Subst
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Subst -> Subst -> Bool
$c/= :: Subst -> Subst -> Bool
== :: Subst -> Subst -> Bool
$c== :: Subst -> Subst -> Bool
Eq
           , Eq Subst
Eq Subst
-> (Subst -> Subst -> Ordering)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Bool)
-> (Subst -> Subst -> Subst)
-> (Subst -> Subst -> Subst)
-> Ord Subst
Subst -> Subst -> Bool
Subst -> Subst -> Ordering
Subst -> Subst -> Subst
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Subst -> Subst -> Subst
$cmin :: Subst -> Subst -> Subst
max :: Subst -> Subst -> Subst
$cmax :: Subst -> Subst -> Subst
>= :: Subst -> Subst -> Bool
$c>= :: Subst -> Subst -> Bool
> :: Subst -> Subst -> Bool
$c> :: Subst -> Subst -> Bool
<= :: Subst -> Subst -> Bool
$c<= :: Subst -> Subst -> Bool
< :: Subst -> Subst -> Bool
$c< :: Subst -> Subst -> Bool
compare :: Subst -> Subst -> Ordering
$ccompare :: Subst -> Subst -> Ordering
Ord
           , TypeVar -> Subst -> ShowS
[Subst] -> ShowS
Subst -> Symbol
(TypeVar -> Subst -> ShowS)
-> (Subst -> Symbol) -> ([Subst] -> ShowS) -> Show Subst
forall a.
(TypeVar -> a -> ShowS)
-> (a -> Symbol) -> ([a] -> ShowS) -> Show a
showList :: [Subst] -> ShowS
$cshowList :: [Subst] -> ShowS
show :: Subst -> Symbol
$cshow :: Subst -> Symbol
showsPrec :: TypeVar -> Subst -> ShowS
$cshowsPrec :: TypeVar -> Subst -> ShowS
Show
           , NonEmpty Subst -> Subst
Subst -> Subst -> Subst
(Subst -> Subst -> Subst)
-> (NonEmpty Subst -> Subst)
-> (forall b. Integral b => b -> Subst -> Subst)
-> Semigroup Subst
forall b. Integral b => b -> Subst -> Subst
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> Subst -> Subst
$cstimes :: forall b. Integral b => b -> Subst -> Subst
sconcat :: NonEmpty Subst -> Subst
$csconcat :: NonEmpty Subst -> Subst
<> :: Subst -> Subst -> Subst
$c<> :: Subst -> Subst -> Subst
Semigroup
           , Semigroup Subst
Subst
Semigroup Subst
-> Subst
-> (Subst -> Subst -> Subst)
-> ([Subst] -> Subst)
-> Monoid Subst
[Subst] -> Subst
Subst -> Subst -> Subst
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Subst] -> Subst
$cmconcat :: [Subst] -> Subst
mappend :: Subst -> Subst -> Subst
$cmappend :: Subst -> Subst -> Subst
mempty :: Subst
$cmempty :: Subst
Monoid )

type Constraint = (Type, Type)
type Unifier = (Subst, [Constraint])

type Solve = Except String

class Substitutable t where
  substitute :: Subst -> t -> t
  ftv :: t -> Set TypeVar

instance Substitutable Type where
  substitute :: Subst -> Type -> Type
substitute Subst
_ (TCon Symbol
a) = Symbol -> Type
TCon Symbol
a
  substitute (Subst Map TypeVar Type
s) t :: Type
t@(TVar TypeVar
a) = Type -> TypeVar -> Map TypeVar Type -> Type
forall k a. Ord k => a -> k -> Map k a -> a
M.findWithDefault Type
t TypeVar
a Map TypeVar Type
s
  substitute Subst
s (Type
t1 :-> Type
t2) = Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
s Type
t1 Type -> Type -> Type
:-> Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
s Type
t2
  substitute (Subst Map TypeVar Type
s) (TForall [TypeVar]
tys Type
t) = [TypeVar] -> Type -> Type
TForall [TypeVar]
tys (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
s' Type
t
    where s' :: Subst
s' = Map TypeVar Type -> Subst
Subst (Map TypeVar Type -> Subst) -> Map TypeVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ (TypeVar -> Map TypeVar Type -> Map TypeVar Type)
-> Map TypeVar Type -> [TypeVar] -> Map TypeVar Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TypeVar -> Map TypeVar Type -> Map TypeVar Type
forall k a. Ord k => k -> Map k a -> Map k a
M.delete Map TypeVar Type
s [TypeVar]
tys

  ftv :: Type -> Set TypeVar
ftv TCon{} = Set TypeVar
forall a. Set a
S.empty
  ftv (TVar TypeVar
a) = TypeVar -> Set TypeVar
forall a. a -> Set a
S.singleton TypeVar
a
  ftv (Type
t1 :-> Type
t2) = Type -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv Type
t1 Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Type -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv Type
t2
  ftv (TForall [TypeVar]
tys Type
t) = Type -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv Type
t Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [TypeVar] -> Set TypeVar
forall a. Ord a => [a] -> Set a
S.fromList [TypeVar]
tys

instance Substitutable Constraint where
  substitute :: Subst -> Constraint -> Constraint
substitute Subst
s (Type
t1, Type
t2) = (Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
s Type
t1, Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
s Type
t2)
  ftv :: Constraint -> Set TypeVar
ftv (Type
t1, Type
t2) = Type -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv Type
t1 Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Type -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv Type
t2

instance Substitutable a => Substitutable [a] where
  substitute :: Subst -> [a] -> [a]
substitute = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> a) -> [a] -> [a])
-> (Subst -> a -> a) -> Subst -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> a -> a
forall t. Substitutable t => Subst -> t -> t
substitute
  ftv :: [a] -> Set TypeVar
ftv = (a -> Set TypeVar -> Set TypeVar)
-> Set TypeVar -> [a] -> Set TypeVar
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
S.union (Set TypeVar -> Set TypeVar -> Set TypeVar)
-> (a -> Set TypeVar) -> a -> Set TypeVar -> Set TypeVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv) Set TypeVar
forall a. Set a
S.empty

instance Substitutable Frame where
  substitute :: Subst -> Frame -> Frame
substitute Subst
s (Frame Map Symbol Type
frame) = Map Symbol Type -> Frame
Frame (Map Symbol Type -> Frame) -> Map Symbol Type -> Frame
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Map Symbol Type -> Map Symbol Type
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
s) Map Symbol Type
frame
  ftv :: Frame -> Set TypeVar
ftv (Frame Map Symbol Type
frame) = [Type] -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv ([Type] -> Set TypeVar) -> [Type] -> Set TypeVar
forall a b. (a -> b) -> a -> b
$ Map Symbol Type -> [Type]
forall k a. Map k a -> [a]
M.elems Map Symbol Type
frame

-- * Inference

typecheck :: Frame -> CbpvExp -> Either String Type
typecheck :: Frame -> CbpvExp -> Either Symbol Type
typecheck Frame
frame CbpvExp
ex = case Frame
-> Infer (Type, [Constraint]) -> Either Symbol (Type, [Constraint])
forall a. Frame -> Infer a -> Either Symbol a
runInfer Frame
frame (CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
ex) of
  Left Symbol
err -> Symbol -> Either Symbol Type
forall a b. a -> Either a b
Left Symbol
err
  Right (Type
ty, [Constraint]
cs) -> case [Constraint] -> Either Symbol Subst
runSolve [Constraint]
cs of
    Left Symbol
err -> Symbol -> Either Symbol Type
forall a b. a -> Either a b
Left Symbol
err
    Right Subst
subst -> Type -> Either Symbol Type
forall a b. b -> Either a b
Right (Type -> Type
closeOver (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
subst Type
ty)

closeOver :: Type -> Sigma
closeOver :: Type -> Type
closeOver = Type -> Type
normalize (Type -> Type) -> (Type -> Type) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Frame -> Type -> Type
generalize Frame
frameEmpty

normalize :: Sigma -> Sigma
normalize :: Type -> Type
normalize (TForall [TypeVar]
tys Type
body) = [TypeVar] -> Type -> Type
TForall (((TypeVar, TypeVar) -> TypeVar)
-> [(TypeVar, TypeVar)] -> [TypeVar]
forall a b. (a -> b) -> [a] -> [b]
map (TypeVar, TypeVar) -> TypeVar
forall a b. (a, b) -> b
snd [(TypeVar, TypeVar)]
ord) (Type -> Type
normtype Type
body) where
  ord :: [(TypeVar, TypeVar)]
ord = [TypeVar] -> [TypeVar] -> [(TypeVar, TypeVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([TypeVar] -> [TypeVar]
forall a. Eq a => [a] -> [a]
nub ([TypeVar] -> [TypeVar]) -> [TypeVar] -> [TypeVar]
forall a b. (a -> b) -> a -> b
$ Type -> [TypeVar]
fv Type
body) [TypeVar]
tys
  fv :: Type -> [TypeVar]
fv (TVar TypeVar
a) = [TypeVar
a]
  fv (Type
a :-> Type
b) = Type -> [TypeVar]
fv Type
a [TypeVar] -> [TypeVar] -> [TypeVar]
forall a. [a] -> [a] -> [a]
++ Type -> [TypeVar]
fv Type
b
  fv (TCon Symbol
_) = []
  normtype :: Type -> Type
normtype (Type
a :-> Type
b) = Type -> Type
normtype Type
a Type -> Type -> Type
:-> Type -> Type
normtype Type
b
  normtype (TCon Symbol
a) = Symbol -> Type
TCon Symbol
a
  normtype (TVar TypeVar
a) = case TypeVar -> [(TypeVar, TypeVar)] -> Maybe TypeVar
forall a b. Eq a => a -> [(a, b)] -> Maybe b
Prelude.lookup TypeVar
a [(TypeVar, TypeVar)]
ord of
    Just TypeVar
x -> TypeVar -> Type
TVar TypeVar
x
    Maybe TypeVar
Nothing -> Symbol -> Type
forall a. HasCallStack => Symbol -> a
error Symbol
"type variable not in signature"
normalize Type
t = Type
t

inFrame :: (Symbol, Type) -> Infer a -> Infer a
inFrame :: forall a. (Symbol, Type) -> Infer a -> Infer a
inFrame (Symbol
x, Type
sc) Infer a
m = do
  let scope :: Frame -> Frame
scope Frame
e = Frame -> Symbol -> Frame
frameRemove Frame
e Symbol
x Frame -> (Symbol, Type) -> Frame
`frameExtend` (Symbol
x, Type
sc)
  (Frame -> Frame) -> Infer a -> Infer a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local Frame -> Frame
scope Infer a
m

inFrames :: [(Symbol, Type)] -> Infer a -> Infer a
inFrames :: forall a. [(Symbol, Type)] -> Infer a -> Infer a
inFrames [(Symbol, Type)]
bindings Infer a
m = do
  let
    scope :: Frame -> Frame
scope Frame
e = Frame -> [(Symbol, Type)] -> Frame
forall {b}. Frame -> [(Symbol, b)] -> Frame
frameRemoves Frame
e [(Symbol, Type)]
bindings Frame -> [(Symbol, Type)] -> Frame
`frameExtends` [(Symbol, Type)]
bindings
    frameRemoves :: Frame -> [(Symbol, b)] -> Frame
frameRemoves (Frame Map Symbol Type
frame) [(Symbol, b)]
bindings =
      Map Symbol Type -> Frame
Frame (Map Symbol Type -> Frame) -> Map Symbol Type -> Frame
forall a b. (a -> b) -> a -> b
$ Map Symbol Type
frame Map Symbol Type -> Map Symbol b -> Map Symbol Type
forall k a b. Ord k => Map k a -> Map k b -> Map k a
`M.difference` [(Symbol, b)] -> Map Symbol b
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Symbol, b)]
bindings
  (Frame -> Frame) -> Infer a -> Infer a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local Frame -> Frame
scope Infer a
m

lookupInFrame :: Symbol -> Infer (Rho,[Constraint])
lookupInFrame :: Symbol -> Infer (Type, [Constraint])
lookupInFrame Symbol
s = do
  Type
σ <- case Symbol -> Maybe Type
primType Symbol
s of
    Just Type
sig -> Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
sig
    Maybe Type
Nothing -> do
      Frame
frame <- Infer Frame
getFrame
      case Symbol -> Frame -> Maybe Type
frameLookup Symbol
s Frame
frame of
        Maybe Type
Nothing -> Symbol
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Symbol
"Unbound symbol: " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
s)
        Just Type
sig -> Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
sig
  Type
ρ <- Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
instantiate Type
σ
  (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ρ, [])

fresh :: Infer Tau
fresh :: ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh = do
  InferState
s <- ReaderT
  Frame (StateT InferState (ExceptT Symbol Identity)) InferState
forall s (m :: * -> *). MonadState s m => m s
get
  InferState
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put InferState
s { count :: TypeVar
count = InferState -> TypeVar
count InferState
s TypeVar -> TypeVar -> TypeVar
forall a. Num a => a -> a -> a
+ TypeVar
1 }
  Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> ReaderT
      Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall a b. (a -> b) -> a -> b
$ TypeVar -> Type
TVar (InferState -> TypeVar
count InferState
s)

instantiate :: Sigma -> Infer Rho
instantiate :: Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
instantiate (TForall [TypeVar]
tys Type
t) = do
  [Type]
tys' <- (TypeVar
 -> ReaderT
      Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> [TypeVar]
-> ReaderT
     Frame (StateT InferState (ExceptT Symbol Identity)) [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
-> TypeVar
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall a b. a -> b -> a
const ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh) [TypeVar]
tys
  let s :: Subst
s = Map TypeVar Type -> Subst
Subst (Map TypeVar Type -> Subst) -> Map TypeVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ [(TypeVar, Type)] -> Map TypeVar Type
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(TypeVar, Type)] -> Map TypeVar Type)
-> [(TypeVar, Type)] -> Map TypeVar Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> [Type] -> [(TypeVar, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TypeVar]
tys [Type]
tys'
  Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
 -> ReaderT
      Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall a b. (a -> b) -> a -> b
$ Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
s Type
t
instantiate Type
ty = Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty

generalize :: Frame -> Rho -> Sigma
generalize :: Frame -> Type -> Type
generalize Frame
frame Type
t = [TypeVar] -> Type -> Type
TForall [TypeVar]
tys Type
t
  where tys :: [TypeVar]
tys = Set TypeVar -> [TypeVar]
forall a. Set a -> [a]
S.toList (Set TypeVar -> [TypeVar]) -> Set TypeVar -> [TypeVar]
forall a b. (a -> b) -> a -> b
$ Type -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv Type
t Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` Frame -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv Frame
frame

getFrame :: Infer Frame
getFrame :: Infer Frame
getFrame = Infer Frame
forall r (m :: * -> *). MonadReader r m => m r
ask

-- | Deep skolemization.
-- Returns the skolem variables and the skolemized ρ-type.
skolemize :: Sigma -> Infer ([TypeVar], Rho)
skolemize :: Type -> Infer ([TypeVar], Type)
skolemize (TForall [TypeVar]
tys Type
ρ1) = do -- rule PRPOLY
  [Type]
sks1 <- (TypeVar
 -> ReaderT
      Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> [TypeVar]
-> ReaderT
     Frame (StateT InferState (ExceptT Symbol Identity)) [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
-> TypeVar
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall a b. a -> b -> a
const ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh) [TypeVar]
tys
  ([TypeVar]
sks2, Type
ρ2) <- Type -> Infer ([TypeVar], Type)
skolemize Type
ρ1
  ([TypeVar], Type) -> Infer ([TypeVar], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Set TypeVar -> [TypeVar]
forall a. Set a -> [a]
S.toList ([Type] -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv [Type]
sks1) [TypeVar] -> [TypeVar] -> [TypeVar]
forall a. [a] -> [a] -> [a]
++ [TypeVar]
sks2, Type
ρ2)
skolemize (Type
σ1 :-> Type
σ2) = do -- rule PRFUN
  ([TypeVar]
sks, Type
σ2') <- Type -> Infer ([TypeVar], Type)
skolemize Type
σ2
  ([TypeVar], Type) -> Infer ([TypeVar], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypeVar]
sks, Type
σ1 Type -> Type -> Type
:-> Type
σ2')
skolemize Type
τ = ([TypeVar], Type) -> Infer ([TypeVar], Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Type
τ) -- rule PRMONO

{- | Type inference rules for 'CbpvExp'ressions.
All functions have at least one (terminal) argument of type ⊥.
-}
infer :: CbpvExp -> Infer (Rho, [Constraint])
infer :: CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
cbpvexpr  = case CbpvExp -> Cbpv CbpvExp
forall (f :: * -> *) (w :: * -> *) a.
ComonadCofree f w =>
w a -> f (w a)
unwrap CbpvExp
cbpvexpr of
  IntA Integer
_ -> (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tyInt, [])
  FloatA Double
_ -> (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tyFloat, [])
  BoolA Bool
_ -> (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tyBool, [])
  SymA Symbol
sym -> case Symbol
sym of
    Symbol
"_" -> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
-> (Type -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Type
ty -> (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, [])
    Symbol
_   -> Symbol -> Infer (Type, [Constraint])
lookupInFrame Symbol
sym
  OpA Symbol
op [CbpvExp]
erands -> CbpvExp -> Infer (Type, [Constraint])
infer (() () -> Cbpv CbpvExp -> CbpvExp
forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< CbpvExp -> [CbpvExp] -> Cbpv CbpvExp
forall a. a -> [a] -> Cbpv a
AppA (() () -> Cbpv CbpvExp -> CbpvExp
forall (f :: * -> *) a. a -> f (Cofree f a) -> Cofree f a
:< Symbol -> Cbpv CbpvExp
forall a. Symbol -> Cbpv a
SymA Symbol
op) [CbpvExp]
erands)
  SuspendA CbpvExp
exp -> CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
exp -- TODO try to improve this
  ResumeA CbpvExp
exp -> CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
exp  -- TODO try to improve this
  AppA CbpvExp
op [CbpvExp]
erands -> do
    Type
rho <- ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh
    Frame
frame <- Infer Frame
getFrame
    (Type
opt, [Constraint]
opc) <- CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
op
    ([Type]
erands_ts, [[Constraint]]
erands_cs) <- (CbpvExp -> Infer (Type, [Constraint]))
-> [CbpvExp]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     ([Type], [[Constraint]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM CbpvExp -> Infer (Type, [Constraint])
infer [CbpvExp]
erands
    [Constraint]
-> (Subst -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint])
forall a. [Constraint] -> (Subst -> Infer a) -> Infer a
solveInference ([[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Constraint]] -> [Constraint]) -> [[Constraint]] -> [Constraint]
forall a b. (a -> b) -> a -> b
$ [Constraint]
opc [Constraint] -> [[Constraint]] -> [[Constraint]]
forall a. a -> [a] -> [a]
: [[Constraint]]
erands_cs) ((Subst -> Infer (Type, [Constraint]))
 -> Infer (Type, [Constraint]))
-> (Subst -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint])
forall a b. (a -> b) -> a -> b
$ \Subst
sub -> do
      [Type]
erands_ts' <- [Type]
-> (Type
    -> ReaderT
         Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> ReaderT
     Frame (StateT InferState (ExceptT Symbol Identity)) [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Type]
erands_ts ((Type
  -> ReaderT
       Frame (StateT InferState (ExceptT Symbol Identity)) Type)
 -> ReaderT
      Frame (StateT InferState (ExceptT Symbol Identity)) [Type])
-> (Type
    -> ReaderT
         Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> ReaderT
     Frame (StateT InferState (ExceptT Symbol Identity)) [Type]
forall a b. (a -> b) -> a -> b
$ \Type
ty ->
        Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
instantiate (Type
 -> ReaderT
      Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> Type
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall a b. (a -> b) -> a -> b
$ Frame -> Type -> Type
generalize (Subst -> Frame -> Frame
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Frame
frame) (Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Type
ty)
      (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
rho, [ (Type
opt, [Type]
erands_ts' [Type] -> Type -> Type
`tyFunSig` Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Type
rho)])
  FunA [Symbol]
args CbpvExp
body -> do
    [Type]
tvs <- (Symbol
 -> ReaderT
      Frame (StateT InferState (ExceptT Symbol Identity)) Type)
-> [Symbol]
-> ReaderT
     Frame (StateT InferState (ExceptT Symbol Identity)) [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
-> Symbol
-> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
forall a b. a -> b -> a
const ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh) [Symbol]
args
    (Type
t, [Constraint]
c) <- [(Symbol, Type)]
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall a. [(Symbol, Type)] -> Infer a -> Infer a
inFrames ([Symbol] -> [Type] -> [(Symbol, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
args [Type]
tvs) (CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
body)
    (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
tvs [Type] -> Type -> Type
`tyFunSig` Type
t, [Constraint]
c)
  LetrecA [(Symbol, CbpvExp)]
bindings CbpvExp
body -> do
    let bindings' :: [(Symbol, CbpvExp)]
bindings' = [(Symbol, CbpvExp)] -> [(Symbol, CbpvExp)]
forall a. [a] -> [a]
reverse ([(Symbol, CbpvExp)] -> [(Symbol, CbpvExp)])
-> [(Symbol, CbpvExp)] -> [(Symbol, CbpvExp)]
forall a b. (a -> b) -> a -> b
$ Graph (Symbol, CbpvExp) Symbol -> [(Symbol, CbpvExp)]
forall node key. Graph node key -> [node]
topo (Graph (Symbol, CbpvExp) Symbol -> [(Symbol, CbpvExp)])
-> Graph (Symbol, CbpvExp) Symbol -> [(Symbol, CbpvExp)]
forall a b. (a -> b) -> a -> b
$ Map Symbol CbpvExp -> Graph (Symbol, CbpvExp) Symbol
makeDepGraph (Map Symbol CbpvExp -> Graph (Symbol, CbpvExp) Symbol)
-> Map Symbol CbpvExp -> Graph (Symbol, CbpvExp) Symbol
forall a b. (a -> b) -> a -> b
$ [(Symbol, CbpvExp)] -> Map Symbol CbpvExp
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Symbol, CbpvExp)]
bindings
    [(Symbol, Type)]
btvs <- [(Symbol, CbpvExp)]
-> ((Symbol, CbpvExp)
    -> ReaderT
         Frame (StateT InferState (ExceptT Symbol Identity)) (Symbol, Type))
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Symbol, CbpvExp)]
bindings' (((Symbol, CbpvExp)
  -> ReaderT
       Frame (StateT InferState (ExceptT Symbol Identity)) (Symbol, Type))
 -> ReaderT
      Frame
      (StateT InferState (ExceptT Symbol Identity))
      [(Symbol, Type)])
-> ((Symbol, CbpvExp)
    -> ReaderT
         Frame (StateT InferState (ExceptT Symbol Identity)) (Symbol, Type))
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall a b. (a -> b) -> a -> b
$ \(Symbol
name, CbpvExp
_) -> ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
-> (Type
    -> ReaderT
         Frame (StateT InferState (ExceptT Symbol Identity)) (Symbol, Type))
-> ReaderT
     Frame (StateT InferState (ExceptT Symbol Identity)) (Symbol, Type)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Type
tv -> (Symbol, Type)
-> ReaderT
     Frame (StateT InferState (ExceptT Symbol Identity)) (Symbol, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Symbol
name, Type
tv)
    let pass :: [(Symbol, Type)]
-> (Symbol, CbpvExp)
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
pass [(Symbol, Type)]
fr (Symbol
name, CbpvExp
defn) = [(Symbol, Type)]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall a. [(Symbol, Type)] -> Infer a -> Infer a
inFrames [(Symbol, Type)]
fr (ReaderT
   Frame
   (StateT InferState (ExceptT Symbol Identity))
   [(Symbol, Type)]
 -> ReaderT
      Frame
      (StateT InferState (ExceptT Symbol Identity))
      [(Symbol, Type)])
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall a b. (a -> b) -> a -> b
$ do
          (Type
ρ, [Constraint]
c) <- CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
defn
          [Constraint]
-> (Subst
    -> ReaderT
         Frame
         (StateT InferState (ExceptT Symbol Identity))
         [(Symbol, Type)])
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall a. [Constraint] -> (Subst -> Infer a) -> Infer a
solveInference [Constraint]
c ((Subst
  -> ReaderT
       Frame
       (StateT InferState (ExceptT Symbol Identity))
       [(Symbol, Type)])
 -> ReaderT
      Frame
      (StateT InferState (ExceptT Symbol Identity))
      [(Symbol, Type)])
-> (Subst
    -> ReaderT
         Frame
         (StateT InferState (ExceptT Symbol Identity))
         [(Symbol, Type)])
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall a b. (a -> b) -> a -> b
$ \Subst
sub -> do
            let σ :: Type
σ = Frame -> Type -> Type
generalize
                    (Subst -> Frame -> Frame
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub (Frame -> Frame) -> Frame -> Frame
forall a b. (a -> b) -> a -> b
$ [(Symbol, Type)] -> Frame
framesFromList [(Symbol, Type)]
fr)
                    (Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Type
ρ)
            [(Symbol, Type)]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Symbol, Type)]
 -> ReaderT
      Frame
      (StateT InferState (ExceptT Symbol Identity))
      [(Symbol, Type)])
-> [(Symbol, Type)]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall a b. (a -> b) -> a -> b
$ [(Symbol, Type)]
fr [(Symbol, Type)] -> [(Symbol, Type)] -> [(Symbol, Type)]
forall a. [a] -> [a] -> [a]
++ [(Symbol
name, Type
σ)]
    [(Symbol, Type)]
fr <- ([(Symbol, Type)]
 -> (Symbol, CbpvExp)
 -> ReaderT
      Frame
      (StateT InferState (ExceptT Symbol Identity))
      [(Symbol, Type)])
-> [(Symbol, Type)]
-> [(Symbol, CbpvExp)]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [(Symbol, Type)]
-> (Symbol, CbpvExp)
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     [(Symbol, Type)]
pass [(Symbol, Type)]
btvs [(Symbol, CbpvExp)]
bindings'
    [(Symbol, Type)]
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall a. [(Symbol, Type)] -> Infer a -> Infer a
inFrames [(Symbol, Type)]
fr (Infer (Type, [Constraint]) -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall a b. (a -> b) -> a -> b
$ CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
body
  LetA Symbol
var CbpvExp
exp CbpvExp
body -> do
    Frame
frame <- Infer Frame
getFrame
    (Type
ρ1, [Constraint]
c1) <- CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
exp
    [Constraint]
-> (Subst -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint])
forall a. [Constraint] -> (Subst -> Infer a) -> Infer a
solveInference [Constraint]
c1 ((Subst -> Infer (Type, [Constraint]))
 -> Infer (Type, [Constraint]))
-> (Subst -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint])
forall a b. (a -> b) -> a -> b
$ \Subst
sub -> do
      let σ :: Type
σ = Frame -> Type -> Type
generalize (Subst -> Frame -> Frame
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Frame
frame) (Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Type
ρ1)
      (Type
ρ2, [Constraint]
c2) <- (Symbol, Type)
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall a. (Symbol, Type) -> Infer a -> Infer a
inFrame (Symbol
var, Type
σ) (Infer (Type, [Constraint]) -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall a b. (a -> b) -> a -> b
$ (Frame -> Frame)
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Subst -> Frame -> Frame
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub) (CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
body)
      (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ρ2, [Constraint]
c1 [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [Constraint]
c2)
  IfA CbpvExp
c CbpvExp
t CbpvExp
e -> do
    ([Type]
ρs, [[Constraint]]
cs) <- (CbpvExp -> Infer (Type, [Constraint]))
-> [CbpvExp]
-> ReaderT
     Frame
     (StateT InferState (ExceptT Symbol Identity))
     ([Type], [[Constraint]])
forall (m :: * -> *) a b c.
Applicative m =>
(a -> m (b, c)) -> [a] -> m ([b], [c])
mapAndUnzipM CbpvExp -> Infer (Type, [Constraint])
infer [CbpvExp
c, CbpvExp
t, CbpvExp
e]
    (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type]
ρs [Type] -> TypeVar -> Type
forall a. [a] -> TypeVar -> a
!! TypeVar
1, [[Constraint]] -> [Constraint]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Constraint]]
cs [Constraint] -> [Constraint] -> [Constraint]
forall a. [a] -> [a] -> [a]
++ [ ([Type] -> Type
forall a. [a] -> a
head [Type]
ρs, Type
tyBool), ([Type]
ρs [Type] -> TypeVar -> Type
forall a. [a] -> TypeVar -> a
!! TypeVar
1, [Type]
ρs [Type] -> TypeVar -> Type
forall a. [a] -> TypeVar -> a
!! TypeVar
2) ])
  ResetA CbpvExp
exp -> do
    CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
exp
  ShiftA Symbol
karg CbpvExp
exp -> do
    Frame
frame <- Infer Frame
getFrame
    Type
tkarg <- ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh
    Type
tkret <- ReaderT Frame (StateT InferState (ExceptT Symbol Identity)) Type
fresh
    let tk :: Type
tk = Frame -> Type -> Type
generalize Frame
frame (Type
tkarg Type -> Type -> Type
:-> Type
tkret)
    (Type
rho, [Constraint]
c) <- (Symbol, Type)
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall a. (Symbol, Type) -> Infer a -> Infer a
inFrame (Symbol
karg, Type
tk) (Infer (Type, [Constraint]) -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint]) -> Infer (Type, [Constraint])
forall a b. (a -> b) -> a -> b
$ CbpvExp -> Infer (Type, [Constraint])
infer CbpvExp
exp
    [Constraint]
-> (Subst -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint])
forall a. [Constraint] -> (Subst -> Infer a) -> Infer a
solveInference [Constraint]
c ((Subst -> Infer (Type, [Constraint]))
 -> Infer (Type, [Constraint]))
-> (Subst -> Infer (Type, [Constraint]))
-> Infer (Type, [Constraint])
forall a b. (a -> b) -> a -> b
$ \Subst
sub -> do
      let TForall [TypeVar]
_ Type
tkarg' = Frame -> Type -> Type
generalize (Subst -> Frame -> Frame
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Frame
frame) (Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute Subst
sub Type
tkarg)
      (Type, [Constraint]) -> Infer (Type, [Constraint])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
tkarg', [])
  Cbpv CbpvExp
_ -> Symbol -> Infer (Type, [Constraint])
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Symbol
"Typechecking for that code Coming Soon™"

-- * Constraint solver

substEmpty :: Subst
substEmpty :: Subst
substEmpty = Subst
forall a. Monoid a => a
mempty

-- | Compose substitutions (with a left bias IIRC).
compose :: Subst -> Subst -> Subst
(Subst Map TypeVar Type
s1) compose :: Subst -> Subst -> Subst
`compose` (Subst Map TypeVar Type
s2) = Map TypeVar Type -> Subst
Subst (Map TypeVar Type -> Subst) -> Map TypeVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ (Type -> Type) -> Map TypeVar Type -> Map TypeVar Type
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Subst -> Type -> Type
forall t. Substitutable t => Subst -> t -> t
substitute (Map TypeVar Type -> Subst
Subst Map TypeVar Type
s1)) Map TypeVar Type
s2 Map TypeVar Type -> Map TypeVar Type -> Map TypeVar Type
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Map TypeVar Type
s1

runSolve :: [Constraint] -> Either String Subst
runSolve :: [Constraint] -> Either Symbol Subst
runSolve [Constraint]
cs = Identity (Either Symbol Subst) -> Either Symbol Subst
forall a. Identity a -> a
runIdentity (Identity (Either Symbol Subst) -> Either Symbol Subst)
-> Identity (Either Symbol Subst) -> Either Symbol Subst
forall a b. (a -> b) -> a -> b
$ ExceptT Symbol Identity Subst -> Identity (Either Symbol Subst)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT Symbol Identity Subst -> Identity (Either Symbol Subst))
-> ExceptT Symbol Identity Subst -> Identity (Either Symbol Subst)
forall a b. (a -> b) -> a -> b
$ Unifier -> ExceptT Symbol Identity Subst
solver Unifier
st
  where st :: Unifier
st = (Subst
substEmpty, [Constraint]
cs)

solver :: Unifier -> Solve Subst
solver :: Unifier -> ExceptT Symbol Identity Subst
solver (Subst
su, [Constraint]
cs) = case [Constraint]
cs of
  [] -> Subst -> ExceptT Symbol Identity Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
su
  ((Type
t1, Type
t2):[Constraint]
cs0) -> do
    Subst
su1 <- Type
t1 Type -> Type -> ExceptT Symbol Identity Subst
`unifies` Type
t2
    Unifier -> ExceptT Symbol Identity Subst
solver (Subst
su1 Subst -> Subst -> Subst
`compose` Subst
su, Subst -> [Constraint] -> [Constraint]
forall t. Substitutable t => Subst -> t -> t
substitute Subst
su1 [Constraint]
cs0)

unifies :: Type -> Type -> Solve Subst
unifies :: Type -> Type -> ExceptT Symbol Identity Subst
unifies Type
t1 Type
t2 | Type
t1 Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
t2 = Subst -> ExceptT Symbol Identity Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
substEmpty
unifies (TVar TypeVar
v) Type
t = TypeVar
v TypeVar -> Type -> ExceptT Symbol Identity Subst
`bind` Type
t
unifies Type
t (TVar TypeVar
v) = TypeVar
v TypeVar -> Type -> ExceptT Symbol Identity Subst
`bind` Type
t
unifies (Type
t1 :-> Type
t2) (Type
t3 :-> Type
t4) = [Type] -> [Type] -> ExceptT Symbol Identity Subst
unifyMany [Type
t1, Type
t2] [Type
t3, Type
t4]
unifies Type
t1 Type
t2 = Symbol -> ExceptT Symbol Identity Subst
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Symbol -> ExceptT Symbol Identity Subst)
-> Symbol -> ExceptT Symbol Identity Subst
forall a b. (a -> b) -> a -> b
$ Symbol
"Unification fail: " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Symbol
forall a. Show a => a -> Symbol
show Type
t1 Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
" vs " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Symbol
forall a. Show a => a -> Symbol
show Type
t2

unifyMany :: [Type] -> [Type] -> Solve Subst
unifyMany :: [Type] -> [Type] -> ExceptT Symbol Identity Subst
unifyMany [] [] = Subst -> ExceptT Symbol Identity Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
substEmpty
unifyMany (Type
t1 : [Type]
ts1) (Type
t2 : [Type]
ts2) = do
  Subst
su1 <- Type
t1 Type -> Type -> ExceptT Symbol Identity Subst
`unifies` Type
t2
  Subst
su2 <- [Type] -> [Type] -> ExceptT Symbol Identity Subst
unifyMany (Subst -> [Type] -> [Type]
forall t. Substitutable t => Subst -> t -> t
substitute Subst
su1 [Type]
ts1) (Subst -> [Type] -> [Type]
forall t. Substitutable t => Subst -> t -> t
substitute Subst
su1 [Type]
ts2)
  Subst -> ExceptT Symbol Identity Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Subst
su2 Subst -> Subst -> Subst
`compose` Subst
su1)
unifyMany [Type]
t1 [Type]
t2 = Symbol -> ExceptT Symbol Identity Subst
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Symbol -> ExceptT Symbol Identity Subst)
-> Symbol -> ExceptT Symbol Identity Subst
forall a b. (a -> b) -> a -> b
$ Symbol
"Unification mismatch: " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> Symbol
forall a. Show a => a -> Symbol
show [Type]
t1 Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
" vs " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ [Type] -> Symbol
forall a. Show a => a -> Symbol
show [Type]
t2

bind :: TypeVar -> Type -> Solve Subst
bind :: TypeVar -> Type -> ExceptT Symbol Identity Subst
bind TypeVar
v Type
t
  | Type
t Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== TypeVar -> Type
TVar TypeVar
v = Subst -> ExceptT Symbol Identity Subst
forall (m :: * -> *) a. Monad m => a -> m a
return Subst
substEmpty
  | TypeVar -> Type -> Bool
forall a. Substitutable a => TypeVar -> a -> Bool
occursCheck TypeVar
v Type
t =
      Symbol -> ExceptT Symbol Identity Subst
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Symbol -> ExceptT Symbol Identity Subst)
-> Symbol -> ExceptT Symbol Identity Subst
forall a b. (a -> b) -> a -> b
$ Symbol
"Infinite type: _" Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeVar -> Symbol
forall a. Show a => a -> Symbol
show TypeVar
v Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Symbol
" ~ " Symbol -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> Symbol
forall a. Show a => a -> Symbol
show Type
t
  | Bool
otherwise = Subst -> ExceptT Symbol Identity Subst
forall (m :: * -> *) a. Monad m => a -> m a
return (Map TypeVar Type -> Subst
Subst (Map TypeVar Type -> Subst) -> Map TypeVar Type -> Subst
forall a b. (a -> b) -> a -> b
$ TypeVar -> Type -> Map TypeVar Type
forall k a. k -> a -> Map k a
M.singleton TypeVar
v Type
t)

occursCheck :: Substitutable a => TypeVar -> a -> Bool
occursCheck :: forall a. Substitutable a => TypeVar -> a -> Bool
occursCheck TypeVar
v a
t = TypeVar
v TypeVar -> Set TypeVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` a -> Set TypeVar
forall t. Substitutable t => t -> Set TypeVar
ftv a
t

solveInference :: [Constraint] -> (Subst -> Infer a) -> Infer a
solveInference :: forall a. [Constraint] -> (Subst -> Infer a) -> Infer a
solveInference [Constraint]
c Subst -> Infer a
ks = case [Constraint] -> Either Symbol Subst
runSolve [Constraint]
c of
  Left Symbol
err -> Symbol -> Infer a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Symbol
err
  Right Subst
sub -> Subst -> Infer a
ks Subst
sub

-- | Lookup table for primitive operators.
primType :: Symbol -> Maybe Sigma
primType :: Symbol -> Maybe Type
primType Symbol
"add-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyInt)
primType Symbol
"mul-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyInt)
primType Symbol
"sub-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyInt)
primType Symbol
"div-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyInt)
primType Symbol
"add-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyFloat)
primType Symbol
"mul-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyFloat)
primType Symbol
"sub-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyFloat)
primType Symbol
"div-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyFloat)
primType Symbol
"eq-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"lte-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"gte-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"lt-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"gt-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyInt Type -> Type -> Type
:-> (Type
tyInt Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"eq-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"lte-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"gte-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"lt-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"gt-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyFloat Type -> Type -> Type
:-> (Type
tyFloat Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"=?" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TypeVar -> Type
TVar TypeVar
0 Type -> Type -> Type
:-> (TypeVar -> Type
TVar TypeVar
0 Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"not" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyBool Type -> Type -> Type
:-> Type
tyBool
primType Symbol
"mod-int" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TypeVar -> Type
TVar TypeVar
0 Type -> Type -> Type
:-> (TypeVar -> Type
TVar TypeVar
0 Type -> Type -> Type
:-> TypeVar -> Type
TVar TypeVar
0)
primType Symbol
"mod-float" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ TypeVar -> Type
TVar TypeVar
0 Type -> Type -> Type
:-> (TypeVar -> Type
TVar TypeVar
0 Type -> Type -> Type
:-> TypeVar -> Type
TVar TypeVar
0)
primType Symbol
"&&" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyBool Type -> Type -> Type
:-> (Type
tyBool Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
"||" = Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$ [TypeVar] -> Type -> Type
TForall [TypeVar
0] (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type
tyBool Type -> Type -> Type
:-> (Type
tyBool Type -> Type -> Type
:-> Type
tyBool)
primType Symbol
_ = Maybe Type
forall a. Maybe a
Nothing

-- * Graph implementation

data Graph node key = Graph
  { forall node key. Graph node key -> Graph
_graph :: G.Graph
  , forall node key. Graph node key -> TypeVar -> (node, key, [key])
_vertices :: G.Vertex -> (node, key, [key])
  }

graphFromList :: Ord key => [(node, key, [key])] -> Graph node key
graphFromList :: forall key node. Ord key => [(node, key, [key])] -> Graph node key
graphFromList = (Graph -> (TypeVar -> (node, key, [key])) -> Graph node key)
-> (Graph, TypeVar -> (node, key, [key])) -> Graph node key
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Graph -> (TypeVar -> (node, key, [key])) -> Graph node key
forall node key.
Graph -> (TypeVar -> (node, key, [key])) -> Graph node key
Graph ((Graph, TypeVar -> (node, key, [key])) -> Graph node key)
-> ([(node, key, [key])] -> (Graph, TypeVar -> (node, key, [key])))
-> [(node, key, [key])]
-> Graph node key
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(node, key, [key])] -> (Graph, TypeVar -> (node, key, [key]))
forall key node.
Ord key =>
[(node, key, [key])] -> (Graph, TypeVar -> (node, key, [key]))
G.graphFromEdges'

vertexLabels :: Functor f => Graph b t -> f G.Vertex -> f b
vertexLabels :: forall (f :: * -> *) b t.
Functor f =>
Graph b t -> f TypeVar -> f b
vertexLabels Graph b t
g = (TypeVar -> b) -> f TypeVar -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Graph b t -> TypeVar -> b
forall b t. Graph b t -> TypeVar -> b
vertexLabel Graph b t
g)

vertexLabel :: Graph b t -> G.Vertex -> b
vertexLabel :: forall b t. Graph b t -> TypeVar -> b
vertexLabel Graph b t
g = (\(b
vi, t
_, [t]
_) -> b
vi) ((b, t, [t]) -> b) -> (TypeVar -> (b, t, [t])) -> TypeVar -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Graph b t -> TypeVar -> (b, t, [t])
forall node key. Graph node key -> TypeVar -> (node, key, [key])
_vertices Graph b t
g

topo :: Graph node key -> [node]
topo :: forall node key. Graph node key -> [node]
topo Graph node key
g = Graph node key -> [TypeVar] -> [node]
forall (f :: * -> *) b t.
Functor f =>
Graph b t -> f TypeVar -> f b
vertexLabels Graph node key
g ([TypeVar] -> [node]) -> [TypeVar] -> [node]
forall a b. (a -> b) -> a -> b
$ Graph -> [TypeVar]
G.topSort (Graph node key -> Graph
forall node key. Graph node key -> Graph
_graph Graph node key
g)

makeDepGraph
  :: Map Symbol CbpvExp
  -> Graph (Symbol, CbpvExp) Symbol
makeDepGraph :: Map Symbol CbpvExp -> Graph (Symbol, CbpvExp) Symbol
makeDepGraph Map Symbol CbpvExp
defns = [((Symbol, CbpvExp), Symbol, [Symbol])]
-> Graph (Symbol, CbpvExp) Symbol
forall key node. Ord key => [(node, key, [key])] -> Graph node key
graphFromList ([((Symbol, CbpvExp), Symbol, [Symbol])]
 -> Graph (Symbol, CbpvExp) Symbol)
-> [((Symbol, CbpvExp), Symbol, [Symbol])]
-> Graph (Symbol, CbpvExp) Symbol
forall a b. (a -> b) -> a -> b
$ Map Symbol ((Symbol, CbpvExp), Symbol, [Symbol])
-> [((Symbol, CbpvExp), Symbol, [Symbol])]
forall k a. Map k a -> [a]
M.elems (Map Symbol ((Symbol, CbpvExp), Symbol, [Symbol])
 -> [((Symbol, CbpvExp), Symbol, [Symbol])])
-> Map Symbol ((Symbol, CbpvExp), Symbol, [Symbol])
-> [((Symbol, CbpvExp), Symbol, [Symbol])]
forall a b. (a -> b) -> a -> b
$ (Symbol -> CbpvExp -> ((Symbol, CbpvExp), Symbol, [Symbol]))
-> Map Symbol CbpvExp
-> Map Symbol ((Symbol, CbpvExp), Symbol, [Symbol])
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey Symbol -> CbpvExp -> ((Symbol, CbpvExp), Symbol, [Symbol])
forall {b}. b -> CbpvExp -> ((b, CbpvExp), b, [Symbol])
dep_list Map Symbol CbpvExp
defns where
  dep_list :: b -> CbpvExp -> ((b, CbpvExp), b, [Symbol])
dep_list b
sym CbpvExp
expr = ((b
sym, CbpvExp
expr), b
sym, Cofree Cbpv [Symbol] -> [Symbol]
forall (w :: * -> *) a. Comonad w => w a -> a
extract ((CbpvExp -> [Symbol]) -> CbpvExp -> Cofree Cbpv [Symbol]
forall (w :: * -> *) a b. Comonad w => (w a -> b) -> w a -> w b
extend (Map Symbol CbpvExp -> CbpvExp -> [Symbol]
deps Map Symbol CbpvExp
defns) CbpvExp
expr))