{-# LANGUAGE DataKinds #-}

module Unison.Type where

import Control.Lens (Prism')
import Control.Monad.Writer.Strict qualified as Writer
import Data.Generics.Sum (_Ctor)
import Data.List.Extra (nubOrd)
import Data.Map qualified as Map
import Data.Monoid (Any (..))
import Data.Sequence qualified as Seq
import Data.Set qualified as Set
import Unison.ABT qualified as ABT
import Unison.HashQualified qualified as HQ
import Unison.Kind qualified as K
import Unison.LabeledDependency qualified as LD
import Unison.Name qualified as Name
import Unison.Names.ResolutionResult qualified as Names
import Unison.Prelude
  ( Const (Const, getConst),
    Generic,
    Generic1,
    Identity (runIdentity),
    Map,
    Set,
    Text,
    foldl',
    join,
    sortOn,
    ($>),
    (<&>),
  )
import Unison.Reference (TypeReference)
import Unison.Reference qualified as Reference
import Unison.Settings qualified as Settings
import Unison.Util.List qualified as List
import Unison.Var (Var)
import Unison.Var qualified as Var

-- | Base functor for types in the Unison language
data F a
  = Ref TypeReference
  | Arrow a a
  | Ann a K.Kind
  | App a a
  | Effect a a
  | Effects [a]
  | Forall a
  | IntroOuter a -- binder like ∀, used to introduce variables that are
  -- bound by outer type signatures, to support scoped type
  -- variables
  deriving ((forall m. Monoid m => F m -> m)
-> (forall m a. Monoid m => (a -> m) -> F a -> m)
-> (forall m a. Monoid m => (a -> m) -> F a -> m)
-> (forall a b. (a -> b -> b) -> b -> F a -> b)
-> (forall a b. (a -> b -> b) -> b -> F a -> b)
-> (forall b a. (b -> a -> b) -> b -> F a -> b)
-> (forall b a. (b -> a -> b) -> b -> F a -> b)
-> (forall a. (a -> a -> a) -> F a -> a)
-> (forall a. (a -> a -> a) -> F a -> a)
-> (forall a. F a -> [a])
-> (forall a. F a -> Bool)
-> (forall a. F a -> Int)
-> (forall a. Eq a => a -> F a -> Bool)
-> (forall a. Ord a => F a -> a)
-> (forall a. Ord a => F a -> a)
-> (forall a. Num a => F a -> a)
-> (forall a. Num a => F a -> a)
-> Foldable F
forall a. Eq a => a -> F a -> Bool
forall a. Num a => F a -> a
forall a. Ord a => F a -> a
forall m. Monoid m => F m -> m
forall a. F a -> Bool
forall a. F a -> Int
forall a. F a -> [a]
forall a. (a -> a -> a) -> F a -> a
forall m a. Monoid m => (a -> m) -> F a -> m
forall b a. (b -> a -> b) -> b -> F a -> b
forall a b. (a -> b -> b) -> b -> F a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => F m -> m
fold :: forall m. Monoid m => F m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> F a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> F a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> F a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> F a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> F a -> b
foldr :: forall a b. (a -> b -> b) -> b -> F a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> F a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> F a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> F a -> b
foldl :: forall b a. (b -> a -> b) -> b -> F a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> F a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> F a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> F a -> a
foldr1 :: forall a. (a -> a -> a) -> F a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> F a -> a
foldl1 :: forall a. (a -> a -> a) -> F a -> a
$ctoList :: forall a. F a -> [a]
toList :: forall a. F a -> [a]
$cnull :: forall a. F a -> Bool
null :: forall a. F a -> Bool
$clength :: forall a. F a -> Int
length :: forall a. F a -> Int
$celem :: forall a. Eq a => a -> F a -> Bool
elem :: forall a. Eq a => a -> F a -> Bool
$cmaximum :: forall a. Ord a => F a -> a
maximum :: forall a. Ord a => F a -> a
$cminimum :: forall a. Ord a => F a -> a
minimum :: forall a. Ord a => F a -> a
$csum :: forall a. Num a => F a -> a
sum :: forall a. Num a => F a -> a
$cproduct :: forall a. Num a => F a -> a
product :: forall a. Num a => F a -> a
Foldable, (forall a b. (a -> b) -> F a -> F b)
-> (forall a b. a -> F b -> F a) -> Functor F
forall a b. a -> F b -> F a
forall a b. (a -> b) -> F a -> F b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> F a -> F b
fmap :: forall a b. (a -> b) -> F a -> F b
$c<$ :: forall a b. a -> F b -> F a
<$ :: forall a b. a -> F b -> F a
Functor, (forall x. F a -> Rep (F a) x)
-> (forall x. Rep (F a) x -> F a) -> Generic (F a)
forall x. Rep (F a) x -> F a
forall x. F a -> Rep (F a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (F a) x -> F a
forall a x. F a -> Rep (F a) x
$cfrom :: forall a x. F a -> Rep (F a) x
from :: forall x. F a -> Rep (F a) x
$cto :: forall a x. Rep (F a) x -> F a
to :: forall x. Rep (F a) x -> F a
Generic, (forall a. F a -> Rep1 F a)
-> (forall a. Rep1 F a -> F a) -> Generic1 F
forall a. Rep1 F a -> F a
forall a. F a -> Rep1 F a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall a. F a -> Rep1 F a
from1 :: forall a. F a -> Rep1 F a
$cto1 :: forall a. Rep1 F a -> F a
to1 :: forall a. Rep1 F a -> F a
Generic1, F a -> F a -> Bool
(F a -> F a -> Bool) -> (F a -> F a -> Bool) -> Eq (F a)
forall a. Eq a => F a -> F a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => F a -> F a -> Bool
== :: F a -> F a -> Bool
$c/= :: forall a. Eq a => F a -> F a -> Bool
/= :: F a -> F a -> Bool
Eq, Eq (F a)
Eq (F a) =>
(F a -> F a -> Ordering)
-> (F a -> F a -> Bool)
-> (F a -> F a -> Bool)
-> (F a -> F a -> Bool)
-> (F a -> F a -> Bool)
-> (F a -> F a -> F a)
-> (F a -> F a -> F a)
-> Ord (F a)
F a -> F a -> Bool
F a -> F a -> Ordering
F a -> F a -> F a
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
forall a. Ord a => Eq (F a)
forall a. Ord a => F a -> F a -> Bool
forall a. Ord a => F a -> F a -> Ordering
forall a. Ord a => F a -> F a -> F a
$ccompare :: forall a. Ord a => F a -> F a -> Ordering
compare :: F a -> F a -> Ordering
$c< :: forall a. Ord a => F a -> F a -> Bool
< :: F a -> F a -> Bool
$c<= :: forall a. Ord a => F a -> F a -> Bool
<= :: F a -> F a -> Bool
$c> :: forall a. Ord a => F a -> F a -> Bool
> :: F a -> F a -> Bool
$c>= :: forall a. Ord a => F a -> F a -> Bool
>= :: F a -> F a -> Bool
$cmax :: forall a. Ord a => F a -> F a -> F a
max :: F a -> F a -> F a
$cmin :: forall a. Ord a => F a -> F a -> F a
min :: F a -> F a -> F a
Ord, Functor F
Foldable F
(Functor F, Foldable F) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> F a -> f (F b))
-> (forall (f :: * -> *) a. Applicative f => F (f a) -> f (F a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> F a -> m (F b))
-> (forall (m :: * -> *) a. Monad m => F (m a) -> m (F a))
-> Traversable F
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => F (m a) -> m (F a)
forall (f :: * -> *) a. Applicative f => F (f a) -> f (F a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> F a -> m (F b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> F a -> f (F b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> F a -> f (F b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> F a -> f (F b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => F (f a) -> f (F a)
sequenceA :: forall (f :: * -> *) a. Applicative f => F (f a) -> f (F a)
$cmapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> F a -> m (F b)
mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> F a -> m (F b)
$csequence :: forall (m :: * -> *) a. Monad m => F (m a) -> m (F a)
sequence :: forall (m :: * -> *) a. Monad m => F (m a) -> m (F a)
Traversable)

_Ref :: Prism' (F a) TypeReference
_Ref :: forall a (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p TypeReference (f TypeReference) -> p (F a) (f (F a))
_Ref = forall (ctor :: Symbol) s t a b.
AsConstructor ctor s t a b =>
Prism s t a b
_Ctor @"Ref"

-- | Types are represented as ABTs over the base functor F, with variables in `v`
type Type v a = ABT.Term F v a

-- | For use with recursion schemes.
type TypeF v a r = ABT.Term' F v a r

wrapV :: (Ord v) => Type v a -> Type (ABT.V v) a
wrapV :: forall v a. Ord v => Type v a -> Type (V v) a
wrapV = (v -> V v) -> Term F v a -> Term F (V v) a
forall (f :: * -> *) v' v a.
(Functor f, Foldable f, Ord v') =>
(v -> v') -> Term f v a -> Term f v' a
ABT.vmap v -> V v
forall v. v -> V v
ABT.Bound

freeVars :: Type v a -> Set v
freeVars :: forall v a. Type v a -> Set v
freeVars = Term F v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
ABT.freeVars

bindExternal ::
  (ABT.Var v) => [(v, TypeReference)] -> Type v a -> Type v a
bindExternal :: forall v a. Var v => [(v, TypeReference)] -> Type v a -> Type v a
bindExternal [(v, TypeReference)]
bs = [(v, Term F v ())] -> Term F v a -> Term F v a
forall (f :: * -> *) v b a.
(Foldable f, Functor f, Var v) =>
[(v, Term f v b)] -> Term f v a -> Term f v a
ABT.substsInheritAnnotation [(v
v, () -> TypeReference -> Term F v ()
forall v a. Ord v => a -> TypeReference -> Type v a
ref () TypeReference
r) | (v
v, TypeReference
r) <- [(v, TypeReference)]
bs]

bindReferences ::
  (Var v) =>
  (v -> Name.Name) ->
  Set v ->
  Map Name.Name TypeReference ->
  Type v a ->
  Names.ResolutionResult a (Type v a)
bindReferences :: forall v a.
Var v =>
(v -> Name)
-> Set v
-> Map Name TypeReference
-> Type v a
-> ResolutionResult a (Type v a)
bindReferences v -> Name
unsafeVarToName Set v
keepFree Map Name TypeReference
ns Type v a
t =
  let fvs :: [(v, a)]
fvs = Set v -> Type v a -> [(v, a)]
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
Set v -> Term f v a -> [(v, a)]
ABT.freeVarOccurrences Set v
keepFree Type v a
t
      rs :: [(v, a, Maybe TypeReference)]
rs = [(v
v, a
a, Name -> Map Name TypeReference -> Maybe TypeReference
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (v -> Name
unsafeVarToName v
v) Map Name TypeReference
ns) | (v
v, a
a) <- [(v, a)]
fvs]
      ok :: (v, a, Maybe TypeReference)
-> Either (Seq (ResolutionFailure a)) (v, TypeReference)
ok (v
v, a
_a, Just TypeReference
r) = (v, TypeReference)
-> Either (Seq (ResolutionFailure a)) (v, TypeReference)
forall a. a -> Either (Seq (ResolutionFailure a)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (v
v, TypeReference
r)
      ok (v
v, a
a, Maybe TypeReference
Nothing) =
        Seq (ResolutionFailure a)
-> Either (Seq (ResolutionFailure a)) (v, TypeReference)
forall a b. a -> Either a b
Left (Seq (ResolutionFailure a)
 -> Either (Seq (ResolutionFailure a)) (v, TypeReference))
-> Seq (ResolutionFailure a)
-> Either (Seq (ResolutionFailure a)) (v, TypeReference)
forall a b. (a -> b) -> a -> b
$
          ResolutionFailure a -> Seq (ResolutionFailure a)
forall a. a -> Seq a
Seq.singleton (HashQualified Name
-> a -> ResolutionError TypeReference -> ResolutionFailure a
forall annotation.
HashQualified Name
-> annotation
-> ResolutionError TypeReference
-> ResolutionFailure annotation
Names.TypeResolutionFailure (Name -> HashQualified Name
forall n. n -> HashQualified n
HQ.NameOnly (v -> Name
unsafeVarToName v
v)) a
a ResolutionError TypeReference
forall ref. ResolutionError ref
Names.NotFound)
   in ((v, a, Maybe TypeReference)
 -> Either (Seq (ResolutionFailure a)) (v, TypeReference))
-> [(v, a, Maybe TypeReference)]
-> Either (Seq (ResolutionFailure a)) [(v, TypeReference)]
forall e (f :: * -> *) a b.
(Semigroup e, Foldable f) =>
(a -> Either e b) -> f a -> Either e [b]
List.validate (v, a, Maybe TypeReference)
-> Either (Seq (ResolutionFailure a)) (v, TypeReference)
ok [(v, a, Maybe TypeReference)]
rs Either (Seq (ResolutionFailure a)) [(v, TypeReference)]
-> ([(v, TypeReference)] -> Type v a)
-> Either (Seq (ResolutionFailure a)) (Type v a)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \[(v, TypeReference)]
es -> [(v, TypeReference)] -> Type v a -> Type v a
forall v a. Var v => [(v, TypeReference)] -> Type v a -> Type v a
bindExternal [(v, TypeReference)]
es Type v a
t

newtype Monotype v a = Monotype {forall v a. Monotype v a -> Type v a
getPolytype :: Type v a} deriving (Monotype v a -> Monotype v a -> Bool
(Monotype v a -> Monotype v a -> Bool)
-> (Monotype v a -> Monotype v a -> Bool) -> Eq (Monotype v a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v a. Var v => Monotype v a -> Monotype v a -> Bool
$c== :: forall v a. Var v => Monotype v a -> Monotype v a -> Bool
== :: Monotype v a -> Monotype v a -> Bool
$c/= :: forall v a. Var v => Monotype v a -> Monotype v a -> Bool
/= :: Monotype v a -> Monotype v a -> Bool
Eq)

instance (Show v) => Show (Monotype v a) where
  show :: Monotype v a -> String
show = Type v a -> String
forall a. Show a => a -> String
show (Type v a -> String)
-> (Monotype v a -> Type v a) -> Monotype v a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Monotype v a -> Type v a
forall v a. Monotype v a -> Type v a
getPolytype

-- Smart constructor which checks if a `Type` has no `Forall` quantifiers.
monotype :: (ABT.Var v) => Type v a -> Maybe (Monotype v a)
monotype :: forall v a. Var v => Type v a -> Maybe (Monotype v a)
monotype Type v a
t = Type v a -> Monotype v a
forall v a. Type v a -> Monotype v a
Monotype (Type v a -> Monotype v a)
-> Maybe (Type v a) -> Maybe (Monotype v a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type v a -> Maybe (Maybe (Type v a)))
-> Type v a -> Maybe (Type v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
ABT.visit Type v a -> Maybe (Maybe (Type v a))
forall {v} {a} {a}. Var v => Term F v a -> Maybe (Maybe a)
isMono Type v a
t
  where
    isMono :: Term F v a -> Maybe (Maybe a)
isMono (Forall' Subst F v a
_) = Maybe a -> Maybe (Maybe a)
forall a. a -> Maybe a
Just Maybe a
forall a. Maybe a
Nothing
    isMono Term F v a
_ = Maybe (Maybe a)
forall a. Maybe a
Nothing

arity :: Type v a -> Int
arity :: forall v a. Type v a -> Int
arity (ForallNamed' v
_ Term F v a
body) = Term F v a -> Int
forall v a. Type v a -> Int
arity Term F v a
body
arity (Arrow' Term F v a
_ Term F v a
o) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Term F v a -> Int
forall v a. Type v a -> Int
arity Term F v a
o
arity (Ann' Term F v a
a Kind
_) = Term F v a -> Int
forall v a. Type v a -> Int
arity Term F v a
a
arity Term F v a
_ = Int
0

-- some smart patterns
pattern Ref' :: TypeReference -> ABT.Term F v a
pattern $mRef' :: forall {r} {v} {a}.
Term F v a -> (TypeReference -> r) -> ((# #) -> r) -> r
Ref' r <- ABT.Tm' (Ref r)

pattern Arrow' :: ABT.Term F v a -> ABT.Term F v a -> ABT.Term F v a
pattern $mArrow' :: forall {r} {v} {a}.
Term F v a -> (Term F v a -> Term F v a -> r) -> ((# #) -> r) -> r
Arrow' i o <- ABT.Tm' (Arrow i o)

pattern Arrow'' :: (Ord v) => ABT.Term F v a -> [Type v a] -> Type v a -> ABT.Term F v a
pattern $mArrow'' :: forall {r} {v} {a}.
Ord v =>
Term F v a
-> (Term F v a -> [Term F v a] -> Term F v a -> r)
-> ((# #) -> r)
-> r
Arrow'' i es o <- Arrow' i (Effect'' es o)

pattern Arrows' :: [Type v a] -> Type v a
pattern $mArrows' :: forall {r} {v} {a}.
Type v a -> ([Type v a] -> r) -> ((# #) -> r) -> r
Arrows' spine <- (unArrows -> Just spine)

pattern EffectfulArrows' :: Type v a -> [(Maybe [Type v a], Type v a)] -> Type v a
pattern $mEffectfulArrows' :: forall {r} {v} {a}.
Type v a
-> (Type v a -> [(Maybe [Type v a], Type v a)] -> r)
-> ((# #) -> r)
-> r
EffectfulArrows' fst rest <- (unEffectfulArrows -> Just (fst, rest))

pattern Ann' :: ABT.Term F v a -> K.Kind -> ABT.Term F v a
pattern $mAnn' :: forall {r} {v} {a}.
Term F v a -> (Term F v a -> Kind -> r) -> ((# #) -> r) -> r
Ann' t k <- ABT.Tm' (Ann t k)

pattern App' :: ABT.Term F v a -> ABT.Term F v a -> ABT.Term F v a
pattern $mApp' :: forall {r} {v} {a}.
Term F v a -> (Term F v a -> Term F v a -> r) -> ((# #) -> r) -> r
App' f x <- ABT.Tm' (App f x)

pattern Apps' :: Type v a -> [Type v a] -> Type v a
pattern $mApps' :: forall {r} {v} {a}.
Type v a -> (Type v a -> [Type v a] -> r) -> ((# #) -> r) -> r
Apps' f args <- (unApps -> Just (f, args))

pattern Pure' :: (Ord v) => Type v a -> Type v a
pattern $mPure' :: forall {r} {v} {a}.
Ord v =>
Type v a -> (Type v a -> r) -> ((# #) -> r) -> r
Pure' t <- (unPure -> Just t)

pattern Request' :: [Type v a] -> Type v a -> Type v a
pattern $mRequest' :: forall {r} {v} {a}.
Type v a -> ([Type v a] -> Type v a -> r) -> ((# #) -> r) -> r
Request' ets res <- Apps' (Ref' ((== effectRef) -> True)) [(flattenEffects -> ets), res]

pattern Effects' :: [ABT.Term F v a] -> ABT.Term F v a
pattern $mEffects' :: forall {r} {v} {a}.
Type v a -> ([Type v a] -> r) -> ((# #) -> r) -> r
Effects' es <- ABT.Tm' (Effects es)

-- Effect1' must match at least one effect
pattern Effect1' :: ABT.Term F v a -> ABT.Term F v a -> ABT.Term F v a
pattern $mEffect1' :: forall {r} {v} {a}.
Term F v a -> (Term F v a -> Term F v a -> r) -> ((# #) -> r) -> r
Effect1' e t <- ABT.Tm' (Effect e t)

pattern Effect' :: (Ord v) => [Type v a] -> Type v a -> Type v a
pattern $mEffect' :: forall {r} {v} {a}.
Ord v =>
Type v a -> ([Type v a] -> Type v a -> r) -> ((# #) -> r) -> r
Effect' es t <- (unEffects1 -> Just (es, t))

pattern Effect'' :: (Ord v) => [Type v a] -> Type v a -> Type v a
pattern $mEffect'' :: forall {r} {v} {a}.
Ord v =>
Type v a -> ([Type v a] -> Type v a -> r) -> ((# #) -> r) -> r
Effect'' es t <- (unEffect0 -> (es, t))

-- Effect0' may match zero effects
pattern Effect0' :: (Ord v) => [Type v a] -> Type v a -> Type v a
pattern $mEffect0' :: forall {r} {v} {a}.
Ord v =>
Type v a -> ([Type v a] -> Type v a -> r) -> ((# #) -> r) -> r
Effect0' es t <- (unEffect0 -> (es, t))

pattern Forall' :: (ABT.Var v) => ABT.Subst F v a -> ABT.Term F v a
pattern $mForall' :: forall {r} {v} {a}.
Var v =>
Term F v a -> (Subst F v a -> r) -> ((# #) -> r) -> r
Forall' subst <- ABT.Tm' (Forall (ABT.Abs' subst))

pattern IntroOuter' :: (ABT.Var v) => ABT.Subst F v a -> ABT.Term F v a
pattern $mIntroOuter' :: forall {r} {v} {a}.
Var v =>
Term F v a -> (Subst F v a -> r) -> ((# #) -> r) -> r
IntroOuter' subst <- ABT.Tm' (IntroOuter (ABT.Abs' subst))

pattern IntroOuterNamed' :: v -> ABT.Term F v a -> ABT.Term F v a
pattern $mIntroOuterNamed' :: forall {r} {v} {a}.
Term F v a -> (v -> Term F v a -> r) -> ((# #) -> r) -> r
IntroOuterNamed' v body <- ABT.Tm' (IntroOuter (ABT.out -> ABT.Abs v body))

pattern ForallsNamed' :: [v] -> Type v a -> Type v a
pattern $mForallsNamed' :: forall {r} {v} {a}.
Type v a -> ([v] -> Type v a -> r) -> ((# #) -> r) -> r
ForallsNamed' vs body <- (unForalls -> Just (vs, body))

pattern ForallsNamedOpt' :: [v] -> Type v a -> Type v a
pattern $mForallsNamedOpt' :: forall {r} {v} {a}.
Type v a -> ([v] -> Type v a -> r) -> ((# #) -> r) -> r
ForallsNamedOpt' vs body <- (unForallsOpt -> (vs, body))

unForallsOpt :: Type v a -> ([v], Type v a)
unForallsOpt :: forall v a. Type v a -> ([v], Type v a)
unForallsOpt (ForallsNamed' [v]
vs Type v a
t) = ([v]
vs, Type v a
t)
unForallsOpt Type v a
t = ([], Type v a
t)

pattern ForallNamed' :: v -> ABT.Term F v a -> ABT.Term F v a
pattern $mForallNamed' :: forall {r} {v} {a}.
Term F v a -> (v -> Term F v a -> r) -> ((# #) -> r) -> r
ForallNamed' v body <- ABT.Tm' (Forall (ABT.out -> ABT.Abs v body))

pattern Var' :: v -> ABT.Term f v a
pattern $mVar' :: forall {r} {v} {f :: * -> *} {a}.
Term f v a -> (v -> r) -> ((# #) -> r) -> r
Var' v <- ABT.Var' v

pattern Cycle' :: [v] -> f (ABT.Term f v a) -> ABT.Term f v a
pattern $mCycle' :: forall {r} {v} {f :: * -> *} {a}.
Term f v a -> ([v] -> f (Term f v a) -> r) -> ((# #) -> r) -> r
Cycle' xs t <- ABT.Cycle' xs t

pattern Abs' :: (Foldable f, Functor f, ABT.Var v) => ABT.Subst f v a -> ABT.Term f v a
pattern $mAbs' :: forall {r} {f :: * -> *} {v} {a}.
(Foldable f, Functor f, Var v) =>
Term f v a -> (Subst f v a -> r) -> ((# #) -> r) -> r
Abs' subst <- ABT.Abs' subst

unPure :: (Ord v) => Type v a -> Maybe (Type v a)
unPure :: forall v a. Ord v => Type v a -> Maybe (Type v a)
unPure (Effect'' [] Type v a
t) = Type v a -> Maybe (Type v a)
forall a. a -> Maybe a
Just Type v a
t
unPure (Effect'' [Type v a]
_ Type v a
_) = Maybe (Type v a)
forall a. Maybe a
Nothing
unPure Type v a
t = Type v a -> Maybe (Type v a)
forall a. a -> Maybe a
Just Type v a
t

unArrows :: Type v a -> Maybe [Type v a]
unArrows :: forall v a. Type v a -> Maybe [Type v a]
unArrows Type v a
t =
  case Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
go Type v a
t of [Type v a
_] -> Maybe [Type v a]
forall a. Maybe a
Nothing; [Type v a]
l -> [Type v a] -> Maybe [Type v a]
forall a. a -> Maybe a
Just [Type v a]
l
  where
    go :: Term F v a -> [Term F v a]
go (Arrow' Term F v a
i Term F v a
o) = Term F v a
i Term F v a -> [Term F v a] -> [Term F v a]
forall a. a -> [a] -> [a]
: Term F v a -> [Term F v a]
go Term F v a
o
    go Term F v a
o = [Term F v a
o]

unEffectfulArrows ::
  Type v a -> Maybe (Type v a, [(Maybe [Type v a], Type v a)])
unEffectfulArrows :: forall v a.
Type v a -> Maybe (Type v a, [(Maybe [Type v a], Type v a)])
unEffectfulArrows Type v a
t = case Type v a
t of
  Arrow' Type v a
i Type v a
o -> (Type v a, [(Maybe [Type v a], Type v a)])
-> Maybe (Type v a, [(Maybe [Type v a], Type v a)])
forall a. a -> Maybe a
Just (Type v a
i, Type v a -> [(Maybe [Type v a], Type v a)]
forall {v} {a}. Term F v a -> [(Maybe [Term F v a], Term F v a)]
go Type v a
o)
  Type v a
_ -> Maybe (Type v a, [(Maybe [Type v a], Type v a)])
forall a. Maybe a
Nothing
  where
    go :: Term F v a -> [(Maybe [Term F v a], Term F v a)]
go (Effect1' (Effects' [Term F v a]
es) (Arrow' Term F v a
i Term F v a
o)) =
      ([Term F v a] -> Maybe [Term F v a]
forall a. a -> Maybe a
Just ([Term F v a] -> Maybe [Term F v a])
-> [Term F v a] -> Maybe [Term F v a]
forall a b. (a -> b) -> a -> b
$ [Term F v a]
es [Term F v a] -> (Term F v a -> [Term F v a]) -> [Term F v a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term F v a -> [Term F v a]
forall v a. Type v a -> [Type v a]
flattenEffects, Term F v a
i) (Maybe [Term F v a], Term F v a)
-> [(Maybe [Term F v a], Term F v a)]
-> [(Maybe [Term F v a], Term F v a)]
forall a. a -> [a] -> [a]
: Term F v a -> [(Maybe [Term F v a], Term F v a)]
go Term F v a
o
    go (Effect1' (Effects' [Term F v a]
es) Term F v a
t) = [([Term F v a] -> Maybe [Term F v a]
forall a. a -> Maybe a
Just ([Term F v a] -> Maybe [Term F v a])
-> [Term F v a] -> Maybe [Term F v a]
forall a b. (a -> b) -> a -> b
$ [Term F v a]
es [Term F v a] -> (Term F v a -> [Term F v a]) -> [Term F v a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term F v a -> [Term F v a]
forall v a. Type v a -> [Type v a]
flattenEffects, Term F v a
t)]
    go (Arrow' Term F v a
i Term F v a
o) = (Maybe [Term F v a]
forall a. Maybe a
Nothing, Term F v a
i) (Maybe [Term F v a], Term F v a)
-> [(Maybe [Term F v a], Term F v a)]
-> [(Maybe [Term F v a], Term F v a)]
forall a. a -> [a] -> [a]
: Term F v a -> [(Maybe [Term F v a], Term F v a)]
go Term F v a
o
    go Term F v a
t = [(Maybe [Term F v a]
forall a. Maybe a
Nothing, Term F v a
t)]

unApps :: Type v a -> Maybe (Type v a, [Type v a])
unApps :: forall v a. Type v a -> Maybe (Type v a, [Type v a])
unApps Type v a
t = case Type v a -> [Type v a] -> [Type v a]
forall {v} {a}. Term F v a -> [Term F v a] -> [Term F v a]
go Type v a
t [] of
  [] -> Maybe (Type v a, [Type v a])
forall a. Maybe a
Nothing
  [Type v a
_] -> Maybe (Type v a, [Type v a])
forall a. Maybe a
Nothing
  Type v a
f : [Type v a]
args -> (Type v a, [Type v a]) -> Maybe (Type v a, [Type v a])
forall a. a -> Maybe a
Just (Type v a
f, [Type v a]
args)
  where
    go :: Term F v a -> [Term F v a] -> [Term F v a]
go (App' Term F v a
i Term F v a
o) [Term F v a]
acc = Term F v a -> [Term F v a] -> [Term F v a]
go Term F v a
i (Term F v a
o Term F v a -> [Term F v a] -> [Term F v a]
forall a. a -> [a] -> [a]
: [Term F v a]
acc)
    go Term F v a
fn [Term F v a]
args = Term F v a
fn Term F v a -> [Term F v a] -> [Term F v a]
forall a. a -> [a] -> [a]
: [Term F v a]
args

unIntroOuters :: Type v a -> Maybe ([v], Type v a)
unIntroOuters :: forall v a. Type v a -> Maybe ([v], Type v a)
unIntroOuters Type v a
t = Type v a -> [v] -> Maybe ([v], Type v a)
forall {a} {a}. Term F a a -> [a] -> Maybe ([a], Term F a a)
go Type v a
t []
  where
    go :: Term F a a -> [a] -> Maybe ([a], Term F a a)
go (IntroOuterNamed' a
v Term F a a
body) [a]
vs = Term F a a -> [a] -> Maybe ([a], Term F a a)
go Term F a a
body (a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
vs)
    go Term F a a
_body [] = Maybe ([a], Term F a a)
forall a. Maybe a
Nothing
    go Term F a a
body [a]
vs = ([a], Term F a a) -> Maybe ([a], Term F a a)
forall a. a -> Maybe a
Just ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
vs, Term F a a
body)

-- Most code doesn't care about `introOuter` binders and is fine dealing with the
-- these outer variable references as free variables. This function strips out
-- one or more `introOuter` binders, so `outer a b . (a, b)` becomes `(a, b)`.
stripIntroOuters :: Type v a -> Type v a
stripIntroOuters :: forall v a. Type v a -> Type v a
stripIntroOuters Type v a
t = case Type v a -> Maybe ([v], Type v a)
forall v a. Type v a -> Maybe ([v], Type v a)
unIntroOuters Type v a
t of
  Just ([v]
_, Type v a
t) -> Type v a
t
  Maybe ([v], Type v a)
Nothing -> Type v a
t

unForalls :: Type v a -> Maybe ([v], Type v a)
unForalls :: forall v a. Type v a -> Maybe ([v], Type v a)
unForalls Type v a
t = Type v a -> [v] -> Maybe ([v], Type v a)
forall {a} {a}. Term F a a -> [a] -> Maybe ([a], Term F a a)
go Type v a
t []
  where
    go :: Term F a a -> [a] -> Maybe ([a], Term F a a)
go (ForallNamed' a
v Term F a a
body) [a]
vs = Term F a a -> [a] -> Maybe ([a], Term F a a)
go Term F a a
body (a
v a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
vs)
    go Term F a a
_body [] = Maybe ([a], Term F a a)
forall a. Maybe a
Nothing
    go Term F a a
body [a]
vs = ([a], Term F a a) -> Maybe ([a], Term F a a)
forall a. a -> Maybe a
Just ([a] -> [a]
forall a. [a] -> [a]
reverse [a]
vs, Term F a a
body)

unEffect0 :: (Ord v) => Type v a -> ([Type v a], Type v a)
unEffect0 :: forall v a. Ord v => Type v a -> ([Type v a], Type v a)
unEffect0 (Effect1' Term F v a
e Term F v a
a) = (Term F v a -> [Term F v a]
forall v a. Type v a -> [Type v a]
flattenEffects Term F v a
e, Term F v a
a)
unEffect0 Term F v a
t = ([], Term F v a
t)

unEffects1 :: (Ord v) => Type v a -> Maybe ([Type v a], Type v a)
unEffects1 :: forall v a. Ord v => Type v a -> Maybe ([Type v a], Type v a)
unEffects1 (Effect1' (Effects' [Term F v a]
es) Term F v a
a) = ([Term F v a], Term F v a) -> Maybe ([Term F v a], Term F v a)
forall a. a -> Maybe a
Just ([Term F v a]
es, Term F v a
a)
unEffects1 Term F v a
_ = Maybe ([Term F v a], Term F v a)
forall a. Maybe a
Nothing

-- | True if the given type is a function, possibly quantified
isArrow :: (ABT.Var v) => Type v a -> Bool
isArrow :: forall v a. Var v => Type v a -> Bool
isArrow (ForallNamed' v
_ Term F v a
t) = Term F v a -> Bool
forall v a. Var v => Type v a -> Bool
isArrow Term F v a
t
isArrow (Arrow' Term F v a
_ Term F v a
_) = Bool
True
isArrow Term F v a
_ = Bool
False

-- some smart constructors

ref :: (Ord v) => a -> TypeReference -> Type v a
ref :: forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a = a -> F (Term F v a) -> Term F v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (F (Term F v a) -> Term F v a)
-> (TypeReference -> F (Term F v a)) -> TypeReference -> Term F v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeReference -> F (Term F v a)
forall a. TypeReference -> F a
Ref

refId :: (Ord v) => a -> Reference.Id -> Type v a
refId :: forall v a. Ord v => a -> Id -> Type v a
refId a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a (TypeReference -> Type v a)
-> (Id -> TypeReference) -> Id -> Type v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> TypeReference
forall h t. Id' h -> Reference' t h
Reference.DerivedId

termLink :: (Ord v) => a -> Type v a
termLink :: forall v a. Ord v => a -> Type v a
termLink a
a = a -> F (Term F v a) -> Term F v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (F (Term F v a) -> Term F v a)
-> (TypeReference -> F (Term F v a)) -> TypeReference -> Term F v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeReference -> F (Term F v a)
forall a. TypeReference -> F a
Ref (TypeReference -> Term F v a) -> TypeReference -> Term F v a
forall a b. (a -> b) -> a -> b
$ TypeReference
termLinkRef

typeLink :: (Ord v) => a -> Type v a
typeLink :: forall v a. Ord v => a -> Type v a
typeLink a
a = a -> F (Term F v a) -> Term F v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (F (Term F v a) -> Term F v a)
-> (TypeReference -> F (Term F v a)) -> TypeReference -> Term F v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeReference -> F (Term F v a)
forall a. TypeReference -> F a
Ref (TypeReference -> Term F v a) -> TypeReference -> Term F v a
forall a b. (a -> b) -> a -> b
$ TypeReference
typeLinkRef

derivedBase32Hex :: (Ord v) => TypeReference -> a -> Type v a
derivedBase32Hex :: forall v a. Ord v => TypeReference -> a -> Type v a
derivedBase32Hex TypeReference
r a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
r

intRef, natRef, floatRef, booleanRef, textRef, charRef, listRef, bytesRef, effectRef, termLinkRef, typeLinkRef :: TypeReference
intRef :: TypeReference
intRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Int"
natRef :: TypeReference
natRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Nat"
floatRef :: TypeReference
floatRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Float"
booleanRef :: TypeReference
booleanRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Boolean"
textRef :: TypeReference
textRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Text"
charRef :: TypeReference
charRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Char"
listRef :: TypeReference
listRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Sequence"
bytesRef :: TypeReference
bytesRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Bytes"
effectRef :: TypeReference
effectRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Effect"
termLinkRef :: TypeReference
termLinkRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Link.Term"
typeLinkRef :: TypeReference
typeLinkRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Link.Type"

builtinIORef, fileHandleRef, filePathRef, threadIdRef, socketRef :: TypeReference
builtinIORef :: TypeReference
builtinIORef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"IO"
fileHandleRef :: TypeReference
fileHandleRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Handle"
filePathRef :: TypeReference
filePathRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"FilePath"
threadIdRef :: TypeReference
threadIdRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"ThreadId"
socketRef :: TypeReference
socketRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Socket"

udpSocketRef, udpListenSocketRef, udpClientSockAddrRef :: TypeReference
udpSocketRef :: TypeReference
udpSocketRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"UDPSocket"
udpListenSocketRef :: TypeReference
udpListenSocketRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"ListenSocket"
udpClientSockAddrRef :: TypeReference
udpClientSockAddrRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"ClientSockAddr"

processHandleRef :: TypeReference
processHandleRef :: TypeReference
processHandleRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"ProcessHandle"

scopeRef, refRef :: TypeReference
scopeRef :: TypeReference
scopeRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Scope"
refRef :: TypeReference
refRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Ref"

iarrayRef, marrayRef :: TypeReference
iarrayRef :: TypeReference
iarrayRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"ImmutableArray"
marrayRef :: TypeReference
marrayRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"MutableArray"

ibytearrayRef, mbytearrayRef :: TypeReference
ibytearrayRef :: TypeReference
ibytearrayRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"ImmutableByteArray"
mbytearrayRef :: TypeReference
mbytearrayRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"MutableByteArray"

mvarRef, tvarRef :: TypeReference
mvarRef :: TypeReference
mvarRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"MVar"
tvarRef :: TypeReference
tvarRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"TVar"

ticketRef :: TypeReference
ticketRef :: TypeReference
ticketRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Ref.Ticket"

promiseRef :: TypeReference
promiseRef :: TypeReference
promiseRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Promise"

tlsRef :: TypeReference
tlsRef :: TypeReference
tlsRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Tls"

stmRef :: TypeReference
stmRef :: TypeReference
stmRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"STM"

patternRef :: TypeReference
patternRef :: TypeReference
patternRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Pattern"

charClassRef :: TypeReference
charClassRef :: TypeReference
charClassRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Char.Class"

tlsClientConfigRef :: TypeReference
tlsClientConfigRef :: TypeReference
tlsClientConfigRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Tls.ClientConfig"

tlsServerConfigRef :: TypeReference
tlsServerConfigRef :: TypeReference
tlsServerConfigRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Tls.ServerConfig"

tlsSignedCertRef :: TypeReference
tlsSignedCertRef :: TypeReference
tlsSignedCertRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Tls.SignedCert"

tlsPrivateKeyRef :: TypeReference
tlsPrivateKeyRef :: TypeReference
tlsPrivateKeyRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Tls.PrivateKey"

tlsCipherRef :: TypeReference
tlsCipherRef :: TypeReference
tlsCipherRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Tls.Cipher"

tlsVersionRef :: TypeReference
tlsVersionRef :: TypeReference
tlsVersionRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Tls.Version"

hashAlgorithmRef :: TypeReference
hashAlgorithmRef :: TypeReference
hashAlgorithmRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"crypto.HashAlgorithm"

codeRef, valueRef :: TypeReference
codeRef :: TypeReference
codeRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Code"
valueRef :: TypeReference
valueRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Value"

anyRef :: TypeReference
anyRef :: TypeReference
anyRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"Any"

timeSpecRef :: TypeReference
timeSpecRef :: TypeReference
timeSpecRef = Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin Text
"TimeSpec"

any :: (Ord v) => a -> Type v a
any :: forall v a. Ord v => a -> Type v a
any a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
anyRef

builtin :: (Ord v) => a -> Text -> Type v a
builtin :: forall v a. Ord v => a -> Text -> Type v a
builtin a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a (TypeReference -> Type v a)
-> (Text -> TypeReference) -> Text -> Type v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> TypeReference
forall t h. t -> Reference' t h
Reference.Builtin

int :: (Ord v) => a -> Type v a
int :: forall v a. Ord v => a -> Type v a
int a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
intRef

nat :: (Ord v) => a -> Type v a
nat :: forall v a. Ord v => a -> Type v a
nat a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
natRef

float :: (Ord v) => a -> Type v a
float :: forall v a. Ord v => a -> Type v a
float a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
floatRef

boolean :: (Ord v) => a -> Type v a
boolean :: forall v a. Ord v => a -> Type v a
boolean a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
booleanRef

text :: (Ord v) => a -> Type v a
text :: forall v a. Ord v => a -> Type v a
text a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
textRef

char :: (Ord v) => a -> Type v a
char :: forall v a. Ord v => a -> Type v a
char a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
charRef

fileHandle :: (Ord v) => a -> Type v a
fileHandle :: forall v a. Ord v => a -> Type v a
fileHandle a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
fileHandleRef

processHandle :: (Ord v) => a -> Type v a
processHandle :: forall v a. Ord v => a -> Type v a
processHandle a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
processHandleRef

threadId :: (Ord v) => a -> Type v a
threadId :: forall v a. Ord v => a -> Type v a
threadId a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
threadIdRef

builtinIO :: (Ord v) => a -> Type v a
builtinIO :: forall v a. Ord v => a -> Type v a
builtinIO a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
builtinIORef

scopeType :: (Ord v) => a -> Type v a
scopeType :: forall v a. Ord v => a -> Type v a
scopeType a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
scopeRef

refType :: (Ord v) => a -> Type v a
refType :: forall v a. Ord v => a -> Type v a
refType a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
refRef

iarrayType, marrayType, ibytearrayType, mbytearrayType :: (Ord v) => a -> Type v a
iarrayType :: forall v a. Ord v => a -> Type v a
iarrayType a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
iarrayRef
marrayType :: forall v a. Ord v => a -> Type v a
marrayType a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
marrayRef
ibytearrayType :: forall v a. Ord v => a -> Type v a
ibytearrayType a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
ibytearrayRef
mbytearrayType :: forall v a. Ord v => a -> Type v a
mbytearrayType a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
mbytearrayRef

socket :: (Ord v) => a -> Type v a
socket :: forall v a. Ord v => a -> Type v a
socket a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
socketRef

udpSocket :: (Ord v) => a -> Type v a
udpSocket :: forall v a. Ord v => a -> Type v a
udpSocket a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
udpSocketRef

udpListenSocket :: (Ord v) => a -> Type v a
udpListenSocket :: forall v a. Ord v => a -> Type v a
udpListenSocket a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
udpListenSocketRef

udpClientSockAddr :: (Ord v) => a -> Type v a
udpClientSockAddr :: forall v a. Ord v => a -> Type v a
udpClientSockAddr a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
udpClientSockAddrRef

list :: (Ord v) => a -> Type v a
list :: forall v a. Ord v => a -> Type v a
list a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
listRef

bytes :: (Ord v) => a -> Type v a
bytes :: forall v a. Ord v => a -> Type v a
bytes a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
bytesRef

effectType :: (Ord v) => a -> Type v a
effectType :: forall v a. Ord v => a -> Type v a
effectType a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a (TypeReference -> Type v a) -> TypeReference -> Type v a
forall a b. (a -> b) -> a -> b
$ TypeReference
effectRef

code, value :: (Ord v) => a -> Type v a
code :: forall v a. Ord v => a -> Type v a
code a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
codeRef
value :: forall v a. Ord v => a -> Type v a
value a
a = a -> TypeReference -> Type v a
forall v a. Ord v => a -> TypeReference -> Type v a
ref a
a TypeReference
valueRef

app :: (Ord v) => a -> Type v a -> Type v a -> Type v a
app :: forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
app a
a Type v a
f Type v a
arg = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> Type v a -> F (Type v a)
forall a. a -> a -> F a
App Type v a
f Type v a
arg)

-- `f x y z` means `((f x) y) z` and the annotation paired with `y` is the one
-- meant for `app (f x) y`
apps :: (Ord v) => Type v a -> [(a, Type v a)] -> Type v a
apps :: forall v a. Ord v => Type v a -> [(a, Type v a)] -> Type v a
apps = (Type v a -> (a, Type v a) -> Type v a)
-> Type v a -> [(a, Type v a)] -> Type v a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Type v a -> (a, Type v a) -> Type v a
forall {v} {a}. Ord v => Type v a -> (a, Type v a) -> Type v a
go where go :: Type v a -> (a, Type v a) -> Type v a
go Type v a
f (a
a, Type v a
t) = a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
app a
a Type v a
f Type v a
t

app' :: (Ord v, Semigroup a) => Type v a -> Type v a -> Type v a
app' :: forall v a.
(Ord v, Semigroup a) =>
Type v a -> Type v a -> Type v a
app' Type v a
f Type v a
arg = a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
app (Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
f a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
arg) Type v a
f Type v a
arg

apps' :: (Semigroup a, Ord v) => Type v a -> [Type v a] -> Type v a
apps' :: forall a v.
(Semigroup a, Ord v) =>
Type v a -> [Type v a] -> Type v a
apps' = (Type v a -> Type v a -> Type v a)
-> Type v a -> [Type v a] -> Type v a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type v a -> Type v a -> Type v a
forall v a.
(Ord v, Semigroup a) =>
Type v a -> Type v a -> Type v a
app'

arrow :: (Ord v) => a -> Type v a -> Type v a -> Type v a
arrow :: forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
a Type v a
i Type v a
o = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> Type v a -> F (Type v a)
forall a. a -> a -> F a
Arrow Type v a
i Type v a
o)

arrow' :: (Semigroup a, Ord v) => Type v a -> Type v a -> Type v a
arrow' :: forall a v.
(Semigroup a, Ord v) =>
Type v a -> Type v a -> Type v a
arrow' Type v a
i Type v a
o = a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow (Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
i a -> a -> a
forall a. Semigroup a => a -> a -> a
<> Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
o) Type v a
i Type v a
o

ann :: (Ord v) => a -> Type v a -> K.Kind -> Type v a
ann :: forall v a. Ord v => a -> Type v a -> Kind -> Type v a
ann a
a Type v a
e Kind
t = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> Kind -> F (Type v a)
forall a. a -> Kind -> F a
Ann Type v a
e Kind
t)

forAll :: (Ord v) => a -> v -> Type v a -> Type v a
forAll :: forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll a
a v
v Type v a
body = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> F (Type v a)
forall a. a -> F a
Forall (a -> v -> Type v a -> Type v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
ABT.abs' a
a v
v Type v a
body))

introOuter :: (Ord v) => a -> v -> Type v a -> Type v a
introOuter :: forall v a. Ord v => a -> v -> Type v a -> Type v a
introOuter a
a v
v Type v a
body = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> F (Type v a)
forall a. a -> F a
IntroOuter (a -> v -> Type v a -> Type v a
forall v a (f :: * -> *).
Ord v =>
a -> v -> Term f v a -> Term f v a
ABT.abs' a
a v
v Type v a
body))

iff :: (Var v) => Type v ()
iff :: forall v. Var v => Type v ()
iff = () -> v -> Type v () -> Type v ()
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll () v
aa (Type v () -> Type v ()) -> Type v () -> Type v ()
forall a b. (a -> b) -> a -> b
$ [((), Type v ())] -> Type v () -> Type v ()
forall v a. Ord v => [(a, Type v a)] -> Type v a -> Type v a
arrows (Type v () -> ((), Type v ())
forall {b}. b -> ((), b)
f (Type v () -> ((), Type v ())) -> [Type v ()] -> [((), Type v ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [() -> Type v ()
forall v a. Ord v => a -> Type v a
boolean (), Type v ()
a, Type v ()
a]) Type v ()
a
  where
    aa :: v
aa = Text -> v
forall v. Var v => Text -> v
Var.named Text
"a"
    a :: Type v ()
a = () -> v -> Type v ()
forall v a. Ord v => a -> v -> Type v a
var () v
aa
    f :: b -> ((), b)
f b
x = ((), b
x)

iff' :: (Var v) => a -> Type v a
iff' :: forall v a. Var v => a -> Type v a
iff' a
loc = a -> v -> Type v a -> Type v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll a
loc v
aa (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ [(a, Type v a)] -> Type v a -> Type v a
forall v a. Ord v => [(a, Type v a)] -> Type v a -> Type v a
arrows (Type v a -> (a, Type v a)
f (Type v a -> (a, Type v a)) -> [Type v a] -> [(a, Type v a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a -> Type v a
forall v a. Ord v => a -> Type v a
boolean a
loc, Type v a
a, Type v a
a]) Type v a
a
  where
    aa :: v
aa = Text -> v
forall v. Var v => Text -> v
Var.named Text
"a"
    a :: Type v a
a = a -> v -> Type v a
forall v a. Ord v => a -> v -> Type v a
var a
loc v
aa
    f :: Type v a -> (a, Type v a)
f Type v a
x = (a
loc, Type v a
x)

iff2 :: (Var v) => a -> Type v a
iff2 :: forall v a. Var v => a -> Type v a
iff2 a
loc = a -> v -> Type v a -> Type v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll a
loc v
aa (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ [(a, Type v a)] -> Type v a -> Type v a
forall v a. Ord v => [(a, Type v a)] -> Type v a -> Type v a
arrows (Type v a -> (a, Type v a)
f (Type v a -> (a, Type v a)) -> [Type v a] -> [(a, Type v a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type v a
a, Type v a
a]) Type v a
a
  where
    aa :: v
aa = Text -> v
forall v. Var v => Text -> v
Var.named Text
"a"
    a :: Type v a
a = a -> v -> Type v a
forall v a. Ord v => a -> v -> Type v a
var a
loc v
aa
    f :: Type v a -> (a, Type v a)
f Type v a
x = (a
loc, Type v a
x)

andor :: (Ord v) => Type v ()
andor :: forall v. Ord v => Type v ()
andor = [((), Type v ())] -> Type v () -> Type v ()
forall v a. Ord v => [(a, Type v a)] -> Type v a -> Type v a
arrows (Type v () -> ((), Type v ())
forall {b}. b -> ((), b)
f (Type v () -> ((), Type v ())) -> [Type v ()] -> [((), Type v ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [() -> Type v ()
forall v a. Ord v => a -> Type v a
boolean (), () -> Type v ()
forall v a. Ord v => a -> Type v a
boolean ()]) (Type v () -> Type v ()) -> Type v () -> Type v ()
forall a b. (a -> b) -> a -> b
$ () -> Type v ()
forall v a. Ord v => a -> Type v a
boolean ()
  where
    f :: b -> ((), b)
f b
x = ((), b
x)

andor' :: (Ord v) => a -> Type v a
andor' :: forall v a. Ord v => a -> Type v a
andor' a
a = [(a, Type v a)] -> Type v a -> Type v a
forall v a. Ord v => [(a, Type v a)] -> Type v a -> Type v a
arrows (Type v a -> (a, Type v a)
f (Type v a -> (a, Type v a)) -> [Type v a] -> [(a, Type v a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a -> Type v a
forall v a. Ord v => a -> Type v a
boolean a
a, a -> Type v a
forall v a. Ord v => a -> Type v a
boolean a
a]) (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ a -> Type v a
forall v a. Ord v => a -> Type v a
boolean a
a
  where
    f :: Type v a -> (a, Type v a)
f Type v a
x = (a
a, Type v a
x)

var :: (Ord v) => a -> v -> Type v a
var :: forall v a. Ord v => a -> v -> Type v a
var = a -> v -> Term F v a
forall a v (f :: * -> *). a -> v -> Term f v a
ABT.annotatedVar

v' :: (Var v) => Text -> Type v ()
v' :: forall v. Var v => Text -> Type v ()
v' Text
s = v -> Term F v ()
forall v (f :: * -> *). v -> Term f v ()
ABT.var (Text -> v
forall v. Var v => Text -> v
Var.named Text
s)

-- Like `v'`, but creates an annotated variable given an annotation
av' :: (Var v) => a -> Text -> Type v a
av' :: forall v a. Var v => a -> Text -> Type v a
av' a
a Text
s = a -> v -> Term F v a
forall a v (f :: * -> *). a -> v -> Term f v a
ABT.annotatedVar a
a (Text -> v
forall v. Var v => Text -> v
Var.named Text
s)

forAll' :: (Var v) => a -> [Text] -> Type v a -> Type v a
forAll' :: forall v a. Var v => a -> [Text] -> Type v a -> Type v a
forAll' a
a [Text]
vs Type v a
body = (v -> Type v a -> Type v a) -> Type v a -> [v] -> Type v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a -> v -> Type v a -> Type v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll a
a) Type v a
body (Text -> v
forall v. Var v => Text -> v
Var.named (Text -> v) -> [Text] -> [v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
vs)

foralls :: (Ord v) => a -> [v] -> Type v a -> Type v a
foralls :: forall v a. Ord v => a -> [v] -> Type v a -> Type v a
foralls a
a [v]
vs Type v a
body = (v -> Type v a -> Type v a) -> Type v a -> [v] -> Type v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a -> v -> Type v a -> Type v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll a
a) Type v a
body [v]
vs

-- Note: `a -> b -> c` parses as `a -> (b -> c)`
-- the annotation associated with `b` will be the annotation for the `b -> c`
-- node
arrows :: (Ord v) => [(a, Type v a)] -> Type v a -> Type v a
arrows :: forall v a. Ord v => [(a, Type v a)] -> Type v a -> Type v a
arrows [(a, Type v a)]
ts Type v a
result = ((a, Type v a) -> Type v a -> Type v a)
-> Type v a -> [(a, Type v a)] -> Type v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a, Type v a) -> Type v a -> Type v a
forall {a}. (a, Type v a) -> Type v a -> Type v a
go Type v a
result [(a, Type v a)]
ts
  where
    go :: (a, Type v a) -> Type v a -> Type v a
go = (a -> Type v a -> Type v a -> Type v a)
-> (a, Type v a) -> Type v a -> Type v a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow

-- The types of effectful computations
effect :: (Ord v) => a -> [Type v a] -> Type v a -> Type v a
effect :: forall v a. Ord v => a -> [Type v a] -> Type v a -> Type v a
effect a
a [Type v a]
es (Effect1' Type v a
fs Type v a
t) =
  let es' :: [Type v a]
es' = ([Type v a]
es [Type v a] -> (Type v a -> [Type v a]) -> [Type v a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
flattenEffects) [Type v a] -> [Type v a] -> [Type v a]
forall a. [a] -> [a] -> [a]
++ Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
flattenEffects Type v a
fs
   in a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> Type v a -> F (Type v a)
forall a. a -> a -> F a
Effect (a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a ([Type v a] -> F (Type v a)
forall a. [a] -> F a
Effects [Type v a]
es')) Type v a
t)
effect a
a [Type v a]
es Type v a
t = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> Type v a -> F (Type v a)
forall a. a -> a -> F a
Effect (a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a ([Type v a] -> F (Type v a)
forall a. [a] -> F a
Effects [Type v a]
es)) Type v a
t)

effects :: (Ord v) => a -> [Type v a] -> Type v a
effects :: forall v a. Ord v => a -> [Type v a] -> Type v a
effects a
a [Type v a]
es = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a ([Type v a] -> F (Type v a)
forall a. [a] -> F a
Effects ([Type v a] -> F (Type v a)) -> [Type v a] -> F (Type v a)
forall a b. (a -> b) -> a -> b
$ [Type v a]
es [Type v a] -> (Type v a -> [Type v a]) -> [Type v a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
flattenEffects)

effect1 :: (Ord v) => a -> Type v a -> Type v a -> Type v a
effect1 :: forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
effect1 a
a Type v a
es (Effect1' Type v a
fs Type v a
t) =
  let es' :: [Type v a]
es' = Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
flattenEffects Type v a
es [Type v a] -> [Type v a] -> [Type v a]
forall a. [a] -> [a] -> [a]
++ Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
flattenEffects Type v a
fs
   in a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> Type v a -> F (Type v a)
forall a. a -> a -> F a
Effect (a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a ([Type v a] -> F (Type v a)
forall a. [a] -> F a
Effects [Type v a]
es')) Type v a
t)
effect1 a
a Type v a
es Type v a
t = a -> F (Type v a) -> Type v a
forall (f :: * -> *) v a.
(Foldable f, Ord v) =>
a -> f (Term f v a) -> Term f v a
ABT.tm' a
a (Type v a -> Type v a -> F (Type v a)
forall a. a -> a -> F a
Effect Type v a
es Type v a
t)

flattenEffects :: Type v a -> [Type v a]
flattenEffects :: forall v a. Type v a -> [Type v a]
flattenEffects (Effects' [Term F v a]
es) = [Term F v a]
es [Term F v a] -> (Term F v a -> [Term F v a]) -> [Term F v a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term F v a -> [Term F v a]
forall v a. Type v a -> [Type v a]
flattenEffects
flattenEffects Term F v a
es = [Term F v a
es]

-- The types of first-class effect values
-- which get deconstructed in effect handlers.
effectV :: (Ord v) => a -> (a, Type v a) -> (a, Type v a) -> Type v a
effectV :: forall v a.
Ord v =>
a -> (a, Type v a) -> (a, Type v a) -> Type v a
effectV a
builtinA (a, Type v a)
e (a, Type v a)
t = Type v a -> [(a, Type v a)] -> Type v a
forall v a. Ord v => Type v a -> [(a, Type v a)] -> Type v a
apps (a -> Text -> Type v a
forall v a. Ord v => a -> Text -> Type v a
builtin a
builtinA Text
"Effect") [(a, Type v a)
e, (a, Type v a)
t]

-- Strips effects from a type. E.g. `{e} a` becomes `a`.
stripEffect :: (Ord v) => Type v a -> ([Type v a], Type v a)
stripEffect :: forall v a. Ord v => Type v a -> ([Type v a], Type v a)
stripEffect (Effect' [Type v a]
e Type v a
t) = case Type v a -> ([Type v a], Type v a)
forall v a. Ord v => Type v a -> ([Type v a], Type v a)
stripEffect Type v a
t of ([Type v a]
ei, Type v a
t) -> ([Type v a]
e [Type v a] -> [Type v a] -> [Type v a]
forall a. [a] -> [a] -> [a]
++ [Type v a]
ei, Type v a
t)
stripEffect Type v a
t = ([], Type v a
t)

-- The type of the flipped function application operator:
-- `(a -> (a -> b) -> b)`
flipApply :: (Var v) => Type v () -> Type v ()
flipApply :: forall v. Var v => Type v () -> Type v ()
flipApply Type v ()
t = () -> v -> Type v () -> Type v ()
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll () v
b (Type v () -> Type v ()) -> Type v () -> Type v ()
forall a b. (a -> b) -> a -> b
$ () -> Type v () -> Type v () -> Type v ()
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow () (() -> Type v () -> Type v () -> Type v ()
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow () Type v ()
t (() -> v -> Type v ()
forall v a. Ord v => a -> v -> Type v a
var () v
b)) (() -> v -> Type v ()
forall v a. Ord v => a -> v -> Type v a
var () v
b)
  where
    b :: v
b = Type v () -> v -> v
forall v (f :: * -> *) a. Var v => Term f v a -> v -> v
ABT.fresh Type v ()
t (Text -> v
forall v. Var v => Text -> v
Var.named Text
"b")

generalize' :: (Var v) => Var.Type -> Type v a -> Type v a
generalize' :: forall v a. Var v => Type -> Type v a -> Type v a
generalize' Type
k Type v a
t = [v] -> Type v a -> Type v a
forall v a. Ord v => [v] -> Type v a -> Type v a
generalize [v]
vsk Type v a
t
  where
    vsk :: [v]
vsk = [v
v | v
v <- Set v -> [v]
forall a. Set a -> [a]
Set.toList (Type v a -> Set v
forall v a. Type v a -> Set v
freeVars Type v a
t), v -> Type
forall v. Var v => v -> Type
Var.typeOf v
v Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
k]

-- | Bind the given variables with an outer `forAll`, if they are used in `t`.
generalize :: (Ord v) => [v] -> Type v a -> Type v a
generalize :: forall v a. Ord v => [v] -> Type v a -> Type v a
generalize [v]
vs Type v a
t = (v -> Type v a -> Type v a) -> Type v a -> [v] -> Type v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr v -> Type v a -> Type v a
forall {v} {a}. Ord v => v -> Term F v a -> Term F v a
f Type v a
t [v]
vs
  where
    f :: v -> Term F v a -> Term F v a
f v
v Term F v a
t =
      if v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v (Term F v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
ABT.freeVars Term F v a
t) then a -> v -> Term F v a -> Term F v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll (Term F v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term F v a
t) v
v Term F v a
t else Term F v a
t

unforall :: Type v a -> Type v a
unforall :: forall v a. Type v a -> Type v a
unforall (ForallsNamed' [v]
_ Type v a
t) = Type v a
t
unforall Type v a
t = Type v a
t

unforall' :: Type v a -> ([v], Type v a)
unforall' :: forall v a. Type v a -> ([v], Type v a)
unforall' (ForallsNamed' [v]
vs Type v a
t) = ([v]
vs, Type v a
t)
unforall' Type v a
t = ([], Type v a
t)

dependencies :: (Ord v) => Type v a -> Set TypeReference
dependencies :: forall v a. Ord v => Type v a -> Set TypeReference
dependencies Type v a
t = [TypeReference] -> Set TypeReference
forall a. Ord a => [a] -> Set a
Set.fromList ([TypeReference] -> Set TypeReference)
-> (Writer [TypeReference] (Type v a) -> [TypeReference])
-> Writer [TypeReference] (Type v a)
-> Set TypeReference
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Writer [TypeReference] (Type v a) -> [TypeReference]
forall w a. Writer w a -> w
Writer.execWriter (Writer [TypeReference] (Type v a) -> Set TypeReference)
-> Writer [TypeReference] (Type v a) -> Set TypeReference
forall a b. (a -> b) -> a -> b
$ (F (Type v a) -> WriterT [TypeReference] Identity (F (Type v a)))
-> Type v a -> Writer [TypeReference] (Type v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Monad g, Ord v) =>
(f (Term f v a) -> g (f (Term f v a)))
-> Term f v a -> g (Term f v a)
ABT.visit' F (Type v a) -> WriterT [TypeReference] Identity (F (Type v a))
forall {f :: * -> *} {a}.
MonadWriter [TypeReference] f =>
F a -> f (F a)
f Type v a
t
  where
    f :: F a -> f (F a)
f t :: F a
t@(Ref TypeReference
r) = [TypeReference] -> f ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
Writer.tell [TypeReference
r] f () -> F a -> f (F a)
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> F a
t
    f F a
t = F a -> f (F a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure F a
t

labeledDependencies :: (Ord v) => Type v a -> Set LD.LabeledDependency
labeledDependencies :: forall v a. Ord v => Type v a -> Set LabeledDependency
labeledDependencies = (TypeReference -> LabeledDependency)
-> Set TypeReference -> Set LabeledDependency
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map TypeReference -> LabeledDependency
LD.TypeReference (Set TypeReference -> Set LabeledDependency)
-> (Type v a -> Set TypeReference)
-> Type v a
-> Set LabeledDependency
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type v a -> Set TypeReference
forall v a. Ord v => Type v a -> Set TypeReference
dependencies

updateDependencies :: (Ord v) => Map TypeReference TypeReference -> Type v a -> Type v a
updateDependencies :: forall v a.
Ord v =>
Map TypeReference TypeReference -> Type v a -> Type v a
updateDependencies Map TypeReference TypeReference
typeUpdates = (F (Term F v a) -> F (Term F v a)) -> Term F v a -> Term F v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(f (Term f v a) -> f (Term f v a)) -> Term f v a -> Term f v a
ABT.rebuildUp F (Term F v a) -> F (Term F v a)
go
  where
    go :: F (Term F v a) -> F (Term F v a)
go (Ref TypeReference
r) = TypeReference -> F (Term F v a)
forall a. TypeReference -> F a
Ref (TypeReference
-> TypeReference
-> Map TypeReference TypeReference
-> TypeReference
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault TypeReference
r TypeReference
r Map TypeReference TypeReference
typeUpdates)
    go F (Term F v a)
f = F (Term F v a)
f

usesEffects :: (Ord v) => Type v a -> Bool
usesEffects :: forall v a. Ord v => Type v a -> Bool
usesEffects Type v a
t = Any -> Bool
getAny (Any -> Bool)
-> (Const Any (Type v a) -> Any) -> Const Any (Type v a) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const Any (Type v a) -> Any
forall {k} a (b :: k). Const a b -> a
getConst (Const Any (Type v a) -> Bool) -> Const Any (Type v a) -> Bool
forall a b. (a -> b) -> a -> b
$ (Type v a -> Maybe (Const Any (Type v a)))
-> Type v a -> Const Any (Type v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
ABT.visit Type v a -> Maybe (Const Any (Type v a))
forall {v} {a} {b}. Term F v a -> Maybe (Const Any b)
go Type v a
t
  where
    go :: Term F v a -> Maybe (Const Any b)
go (Effect1' Term F v a
_ Term F v a
_) = Const Any b -> Maybe (Const Any b)
forall a. a -> Maybe a
Just (Any -> Const Any b
forall {k} a (b :: k). a -> Const a b
Const (Bool -> Any
Any Bool
True))
    go Term F v a
_ = Maybe (Const Any b)
forall a. Maybe a
Nothing

-- Returns free effect variables in the given type, for instance, in:
--
--   ∀ e3 . a ->{e,e2} b ->{e3} c
--
-- This function would return the set {e, e2}, but not `e3` since `e3`
-- is bound by the enclosing forall.
freeEffectVars :: (Ord v) => Type v a -> Set v
freeEffectVars :: forall v a. Ord v => Type v a -> Set v
freeEffectVars Type v a
t =
  [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList ([v] -> Set v)
-> (Identity [[v]] -> [v]) -> Identity [[v]] -> Set v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[v]] -> [v]
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ([[v]] -> [v])
-> (Identity [[v]] -> [[v]]) -> Identity [[v]] -> [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity [[v]] -> [[v]]
forall a. Identity a -> a
runIdentity (Identity [[v]] -> Set v) -> Identity [[v]] -> Set v
forall a b. (a -> b) -> a -> b
$
    (Term F v (Set v) -> Identity [v])
-> Term F v (Set v) -> Identity [[v]]
forall (f :: * -> *) (g :: * -> *) v a b.
(Traversable f, Applicative g) =>
(Term f v a -> g b) -> Term f v a -> g [b]
ABT.foreachSubterm Term F v (Set v) -> Identity [v]
forall {v} {f :: * -> *}.
(Ord v, Applicative f) =>
Term F v (Set v) -> f [v]
go ((a, Set v) -> Set v
forall a b. (a, b) -> b
snd ((a, Set v) -> Set v) -> Term F v (a, Set v) -> Term F v (Set v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type v a -> Term F v (a, Set v)
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
Term f v a -> Term f v (a, Set v)
ABT.annotateBound Type v a
t)
  where
    go :: Term F v (Set v) -> f [v]
go t :: Term F v (Set v)
t@(Effects' [Term F v (Set v)]
es) =
      let frees :: Set v
frees = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList [v
v | Var' v
v <- [Term F v (Set v)]
es [Term F v (Set v)]
-> (Term F v (Set v) -> [Term F v (Set v)]) -> [Term F v (Set v)]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term F v (Set v) -> [Term F v (Set v)]
forall v a. Type v a -> [Type v a]
flattenEffects]
       in [v] -> f [v]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([v] -> f [v]) -> (Set v -> [v]) -> Set v -> f [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set v -> [v]
forall a. Set a -> [a]
Set.toList (Set v -> f [v]) -> Set v -> f [v]
forall a b. (a -> b) -> a -> b
$ Set v
frees Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Term F v (Set v) -> Set v
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term F v (Set v)
t
    go t :: Term F v (Set v)
t@(Effect1' Term F v (Set v)
e Term F v (Set v)
_) =
      let frees :: Set v
frees = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList [v
v | Var' v
v <- Term F v (Set v) -> [Term F v (Set v)]
forall v a. Type v a -> [Type v a]
flattenEffects Term F v (Set v)
e]
       in [v] -> f [v]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([v] -> f [v]) -> (Set v -> [v]) -> Set v -> f [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set v -> [v]
forall a. Set a -> [a]
Set.toList (Set v -> f [v]) -> Set v -> f [v]
forall a b. (a -> b) -> a -> b
$ Set v
frees Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Term F v (Set v) -> Set v
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term F v (Set v)
t
    go Term F v (Set v)
_ = [v] -> f [v]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

-- Converts all unadorned arrows in a type to have fresh
-- existential ability requirements. For example:
--
--   (a -> b) -> [a] -> [b]
--
-- Becomes
--
--   (a ->{e1} b) ->{e2} [a] ->{e3} [b]
existentializeArrows :: (Ord v, Monad m) => m v -> Type v a -> m (Type v a)
existentializeArrows :: forall v (m :: * -> *) a.
(Ord v, Monad m) =>
m v -> Type v a -> m (Type v a)
existentializeArrows m v
newVar Type v a
t = (Type v a -> Maybe (m (Type v a))) -> Type v a -> m (Type v a)
forall (f :: * -> *) (g :: * -> *) v a.
(Traversable f, Applicative g, Ord v) =>
(Term f v a -> Maybe (g (Term f v a)))
-> Term f v a -> g (Term f v a)
ABT.visit Type v a -> Maybe (m (Type v a))
go Type v a
t
  where
    go :: Type v a -> Maybe (m (Type v a))
go t :: Type v a
t@(Arrow' Type v a
a Type v a
b) = case Type v a
b of
      -- If an arrow already has attached abilities,
      -- leave it alone. Ex: `a ->{e} b` is kept as is.
      Effect1' Type v a
_ Type v a
_ -> m (Type v a) -> Maybe (m (Type v a))
forall a. a -> Maybe a
Just (m (Type v a) -> Maybe (m (Type v a)))
-> m (Type v a) -> Maybe (m (Type v a))
forall a b. (a -> b) -> a -> b
$ do
        Type v a
a <- m v -> Type v a -> m (Type v a)
forall v (m :: * -> *) a.
(Ord v, Monad m) =>
m v -> Type v a -> m (Type v a)
existentializeArrows m v
newVar Type v a
a
        Type v a
b <- m v -> Type v a -> m (Type v a)
forall v (m :: * -> *) a.
(Ord v, Monad m) =>
m v -> Type v a -> m (Type v a)
existentializeArrows m v
newVar Type v a
b
        Type v a -> m (Type v a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type v a -> m (Type v a)) -> Type v a -> m (Type v a)
forall a b. (a -> b) -> a -> b
$ a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow (Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
t) Type v a
a Type v a
b
      -- For unadorned arrows, make up a fresh variable.
      -- So `a -> b` becomes `a ->{e} b`, using the
      -- `newVar` variable generator.
      Type v a
_ -> m (Type v a) -> Maybe (m (Type v a))
forall a. a -> Maybe a
Just (m (Type v a) -> Maybe (m (Type v a)))
-> m (Type v a) -> Maybe (m (Type v a))
forall a b. (a -> b) -> a -> b
$ do
        v
e <- m v
newVar
        Type v a
a <- m v -> Type v a -> m (Type v a)
forall v (m :: * -> *) a.
(Ord v, Monad m) =>
m v -> Type v a -> m (Type v a)
existentializeArrows m v
newVar Type v a
a
        Type v a
b <- m v -> Type v a -> m (Type v a)
forall v (m :: * -> *) a.
(Ord v, Monad m) =>
m v -> Type v a -> m (Type v a)
existentializeArrows m v
newVar Type v a
b
        let ann :: a
ann = Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
t
        Type v a -> m (Type v a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type v a -> m (Type v a)) -> Type v a -> m (Type v a)
forall a b. (a -> b) -> a -> b
$ a -> Type v a -> Type v a -> Type v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann Type v a
a (a -> [Type v a] -> Type v a -> Type v a
forall v a. Ord v => a -> [Type v a] -> Type v a -> Type v a
effect a
ann [a -> v -> Type v a
forall v a. Ord v => a -> v -> Type v a
var a
ann v
e] Type v a
b)
    go Type v a
_ = Maybe (m (Type v a))
forall a. Maybe a
Nothing

purifyArrows :: (Ord v) => Type v a -> Type v a
purifyArrows :: forall v a. Ord v => Type v a -> Type v a
purifyArrows = (Term F v a -> Maybe (Term F v a)) -> Term F v a -> Term F v a
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Term F v a -> Maybe (Term F v a)
forall v a. Ord v => Type v a -> Maybe (Type v a)
go
  where
    go :: Term F v a -> Maybe (Term F v a)
go t :: Term F v a
t@(Arrow' Term F v a
a Term F v a
b) = case Term F v a
b of
      Effect1' Term F v a
_ Term F v a
_ -> Maybe (Term F v a)
forall a. Maybe a
Nothing
      Term F v a
_ -> Term F v a -> Maybe (Term F v a)
forall a. a -> Maybe a
Just (Term F v a -> Maybe (Term F v a))
-> Term F v a -> Maybe (Term F v a)
forall a b. (a -> b) -> a -> b
$ a -> Term F v a -> Term F v a -> Term F v a
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
arrow a
ann Term F v a
a (a -> [Term F v a] -> Term F v a -> Term F v a
forall v a. Ord v => a -> [Type v a] -> Type v a -> Type v a
effect a
ann [] Term F v a
b)
      where
        ann :: a
ann = Term F v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term F v a
t
    go Term F v a
_ = Maybe (Term F v a)
forall a. Maybe a
Nothing

-- Remove free effect variables from the type that are in the set
-- `keepEmptied` controls whether any ability lists that become `{}`
-- after this transformation are kept in the signature or elided entirely
removeEffectVars :: (ABT.Var v) => Bool -> Set v -> Type v a -> Type v a
removeEffectVars :: forall v a. Var v => Bool -> Set v -> Type v a -> Type v a
removeEffectVars Bool
keepEmptied Set v
removals Type v a
t =
  let z :: Type v ()
z = () -> [Type v ()] -> Type v ()
forall v a. Ord v => a -> [Type v a] -> Type v a
effects () []
      t' :: Type v a
t' = [(v, Type v ())] -> Type v a -> Type v a
forall (f :: * -> *) v b a.
(Foldable f, Functor f, Var v) =>
[(v, Term f v b)] -> Term f v a -> Term f v a
ABT.substsInheritAnnotation ((,Type v ()
z) (v -> (v, Type v ())) -> [v] -> [(v, Type v ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set v -> [v]
forall a. Set a -> [a]
Set.toList Set v
removals) Type v a
t
      -- leave explicitly empty `{}` alone
      removeEmpty :: Type v a -> Maybe (Type v a)
removeEmpty (Effect1' (Effects' []) Type v a
_) = Maybe (Type v a)
forall a. Maybe a
Nothing
      removeEmpty t :: Type v a
t@(Effect1' Type v a
e Type v a
v) =
        case Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
flattenEffects Type v a
e of
          [] | Bool -> Bool
not Bool
keepEmptied -> Type v a -> Maybe (Type v a)
forall a. a -> Maybe a
Just ((Type v a -> Maybe (Type v a)) -> Type v a -> Type v a
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Type v a -> Maybe (Type v a)
removeEmpty Type v a
v)
          [Type v a]
es -> Type v a -> Maybe (Type v a)
forall a. a -> Maybe a
Just (a -> [Type v a] -> Type v a -> Type v a
forall v a. Ord v => a -> [Type v a] -> Type v a -> Type v a
effect (Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
t) [Type v a]
es (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ (Type v a -> Maybe (Type v a)) -> Type v a -> Type v a
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Type v a -> Maybe (Type v a)
removeEmpty Type v a
v)
      removeEmpty t :: Type v a
t@(Effects' [Type v a]
es) =
        Type v a -> Maybe (Type v a)
forall a. a -> Maybe a
Just (Type v a -> Maybe (Type v a)) -> Type v a -> Maybe (Type v a)
forall a b. (a -> b) -> a -> b
$ a -> [Type v a] -> Type v a
forall v a. Ord v => a -> [Type v a] -> Type v a
effects (Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
t) ([Type v a]
es [Type v a] -> (Type v a -> [Type v a]) -> [Type v a]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type v a -> [Type v a]
forall v a. Type v a -> [Type v a]
flattenEffects)
      removeEmpty Type v a
_ = Maybe (Type v a)
forall a. Maybe a
Nothing
   in (Type v a -> Maybe (Type v a)) -> Type v a -> Type v a
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Type v a -> Maybe (Type v a)
removeEmpty Type v a
t'

-- Remove all effect variables from the type.
-- Used for type-based search, we apply this transformation to both the
-- indexed type and the query type, so the user can supply `a -> b` that will
-- match `a ->{e} b` (but not `a ->{IO} b`).
removeAllEffectVars :: (ABT.Var v) => Type v a -> Type v a
removeAllEffectVars :: forall v a. Var v => Type v a -> Type v a
removeAllEffectVars Type v a
t =
  let allEffectVars :: Set v
allEffectVars = (Type v a -> Set v) -> [Type v a] -> Set v
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type v a -> Set v
forall v a. Ord v => Type v a -> Set v
go (Type v a -> [Type v a]
forall v (f :: * -> *) a.
(Ord v, Traversable f) =>
Term f v a -> [Term f v a]
ABT.subterms Type v a
t)
      go :: Term F v a -> Set v
go (Effects' [Term F v a]
vs) = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList [v
v | Var' v
v <- [Term F v a]
vs]
      go (Effect1' (Var' v
v) Term F v a
_) = v -> Set v
forall a. a -> Set a
Set.singleton v
v
      go Term F v a
_ = Set v
forall a. Monoid a => a
mempty
      ([v]
vs, Type v a
tu) = Type v a -> ([v], Type v a)
forall v a. Type v a -> ([v], Type v a)
unforall' Type v a
t
   in [v] -> Type v a -> Type v a
forall v a. Ord v => [v] -> Type v a -> Type v a
generalize [v]
vs (Bool -> Set v -> Type v a -> Type v a
forall v a. Var v => Bool -> Set v -> Type v a -> Type v a
removeEffectVars Bool
False Set v
allEffectVars Type v a
tu)

-- Removes empty {} from type signatures, so
--  `a ->{} b` becomes `a -> b`
removeEmptyEffects :: (Ord v) => Type v a -> Type v a
removeEmptyEffects :: forall v a. Ord v => Type v a -> Type v a
removeEmptyEffects Type v a
t = (Type v a -> Type v a) -> Type v a -> Type v a
forall v (f :: * -> *) a.
(Ord v, Foldable f, Functor f) =>
(Term f v a -> Term f v a) -> Term f v a -> Term f v a
ABT.rebuildUp' Type v a -> Type v a
forall v a. Type v a -> Type v a
go Type v a
t
  where
    go :: Term F v a -> Term F v a
go (Effect1' (Effects' []) Term F v a
t) = Term F v a
t
    go Term F v a
t = Term F v a
t

-- pure effect variables are those used only in covariant position
-- for instance, in Nat ->{g} Nat ->{g2} Nat, `g` and `g2` only
-- appear to the right of an `->`, and as a result this type is
-- equivalent to `Nat ->{} Nat ->{} Nat`.
--
-- `keepEmptied` controls whether any ability lists that become `{}`
-- after this transformation are removed from the signature or
-- kept around.
removePureEffects :: (ABT.Var v) => Bool -> Type v a -> Type v a
removePureEffects :: forall v a. Var v => Bool -> Type v a -> Type v a
removePureEffects Bool
keepEmptied Type v a
t
  | Bool -> Bool
not Bool
Settings.removePureEffects = Type v a
t
  | Bool
otherwise =
      [v] -> Type v a -> Type v a
forall v a. Ord v => [v] -> Type v a -> Type v a
generalize [v]
vs (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ Bool -> Set v -> Type v a -> Type v a
forall v a. Var v => Bool -> Set v -> Type v a -> Type v a
removeEffectVars Bool
keepEmptied Set v
fvs Type v a
tu
  where
    ([v]
vs, Type v a
tu) = Type v a -> ([v], Type v a)
forall v a. Type v a -> ([v], Type v a)
unforall' Type v a
t
    vss :: Set v
vss = [v] -> Set v
forall a. Ord a => [a] -> Set a
Set.fromList [v]
vs
    fvs :: Set v
fvs = Type v a -> Set v
forall v a. Ord v => Type v a -> Set v
freeEffectVars Type v a
tu Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set v
keep

    keep :: Set v
keep = Bool -> Type v a -> Set v
keepVarsT Bool
True Type v a
tu

    keepVarsT :: Bool -> Type v a -> Set v
keepVarsT Bool
pos (Arrow' Type v a
i Type v a
o) =
      Bool -> Type v a -> Set v
keepVarsT (Bool -> Bool
not Bool
pos) Type v a
i Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Bool -> Type v a -> Set v
keepVarsT Bool
pos Type v a
o
    keepVarsT Bool
pos (Effect1' Type v a
e Type v a
o) =
      Bool -> Type v a -> Set v
keepVarsT Bool
pos Type v a
e Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Bool -> Type v a -> Set v
keepVarsT Bool
pos Type v a
o
    keepVarsT Bool
pos (Effects' [Type v a]
es) = (Type v a -> Set v) -> [Type v a] -> Set v
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Bool -> Type v a -> Set v
keepVarsE Bool
pos) [Type v a]
es
    keepVarsT Bool
pos (ForallNamed' v
_ Type v a
t) = Bool -> Type v a -> Set v
keepVarsT Bool
pos Type v a
t
    keepVarsT Bool
pos (IntroOuterNamed' v
_ Type v a
t) = Bool -> Type v a -> Set v
keepVarsT Bool
pos Type v a
t
    keepVarsT Bool
_ Type v a
t = Type v a -> Set v
forall v a. Type v a -> Set v
freeVars Type v a
t

    -- Note, this only allows removal if the variable was quantified,
    -- so variables that were free in `t` will not be removed.
    keepVarsE :: Bool -> Type v a -> Set v
keepVarsE Bool
pos (Var' v
v)
      | Bool
pos, v
v v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
vss = Set v
forall a. Monoid a => a
mempty
      | Bool
otherwise = v -> Set v
forall a. a -> Set a
Set.singleton v
v
    keepVarsE Bool
pos Type v a
e = Bool -> Type v a -> Set v
keepVarsT Bool
pos Type v a
e

editFunctionResult ::
  forall v a.
  (Ord v) =>
  (Type v a -> Type v a) ->
  Type v a ->
  Type v a
editFunctionResult :: forall v a. Ord v => (Type v a -> Type v a) -> Type v a -> Type v a
editFunctionResult Type v a -> Type v a
f = Type v a -> Type v a
go
  where
    go :: Type v a -> Type v a
    go :: Type v a -> Type v a
go (ABT.Term Set v
s a
a ABT F v (Type v a)
t) = case ABT F v (Type v a)
t of
      ABT.Tm (Forall Type v a
t) ->
        (\Type v a
x -> Set v -> a -> ABT F v (Type v a) -> Type v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
ABT.Term (Set v
s Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Type v a -> Set v
forall v a. Type v a -> Set v
freeVars Type v a
x) a
a (ABT F v (Type v a) -> Type v a)
-> (F (Type v a) -> ABT F v (Type v a)) -> F (Type v a) -> Type v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F (Type v a) -> ABT F v (Type v a)
forall (f :: * -> *) v r. f r -> ABT f v r
ABT.Tm (F (Type v a) -> Type v a) -> F (Type v a) -> Type v a
forall a b. (a -> b) -> a -> b
$ Type v a -> F (Type v a)
forall a. a -> F a
Forall Type v a
x) (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ Type v a -> Type v a
go Type v a
t
      ABT.Tm (Arrow Type v a
i Type v a
o) ->
        (\Type v a
x -> Set v -> a -> ABT F v (Type v a) -> Type v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
ABT.Term (Set v
s Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Type v a -> Set v
forall v a. Type v a -> Set v
freeVars Type v a
x) a
a (ABT F v (Type v a) -> Type v a)
-> (F (Type v a) -> ABT F v (Type v a)) -> F (Type v a) -> Type v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F (Type v a) -> ABT F v (Type v a)
forall (f :: * -> *) v r. f r -> ABT f v r
ABT.Tm (F (Type v a) -> Type v a) -> F (Type v a) -> Type v a
forall a b. (a -> b) -> a -> b
$ Type v a -> Type v a -> F (Type v a)
forall a. a -> a -> F a
Arrow Type v a
i Type v a
x) (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ Type v a -> Type v a
go Type v a
o
      ABT.Abs v
v Type v a
r ->
        (\Type v a
x -> Set v -> a -> ABT F v (Type v a) -> Type v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
ABT.Term (Set v
s Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Type v a -> Set v
forall v a. Type v a -> Set v
freeVars Type v a
x) a
a (ABT F v (Type v a) -> Type v a) -> ABT F v (Type v a) -> Type v a
forall a b. (a -> b) -> a -> b
$ v -> Type v a -> ABT F v (Type v a)
forall (f :: * -> *) v r. v -> r -> ABT f v r
ABT.Abs v
v Type v a
x) (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ Type v a -> Type v a
go Type v a
r
      ABT F v (Type v a)
_ -> Type v a -> Type v a
f (Set v -> a -> ABT F v (Type v a) -> Type v a
forall (f :: * -> *) v a.
Set v -> a -> ABT f v (Term f v a) -> Term f v a
ABT.Term Set v
s a
a ABT F v (Type v a)
t)

functionResult :: Type v a -> Maybe (Type v a)
functionResult :: forall v a. Type v a -> Maybe (Type v a)
functionResult = Bool -> Term F v a -> Maybe (Term F v a)
forall {v} {a}. Bool -> Term F v a -> Maybe (Term F v a)
go Bool
False
  where
    go :: Bool -> Term F v a -> Maybe (Term F v a)
go Bool
inArr (ForallNamed' v
_ Term F v a
body) = Bool -> Term F v a -> Maybe (Term F v a)
go Bool
inArr Term F v a
body
    go Bool
_inArr (Arrow' Term F v a
_i Term F v a
o) = Bool -> Term F v a -> Maybe (Term F v a)
go Bool
True Term F v a
o
    go Bool
inArr Term F v a
t = if Bool
inArr then Term F v a -> Maybe (Term F v a)
forall a. a -> Maybe a
Just Term F v a
t else Maybe (Term F v a)
forall a. Maybe a
Nothing

-- | Bind all free variables (not in `except`) that start with a lowercase
-- letter and are unqualified with an outer `forall`.
-- `a -> a` becomes `∀ a . a -> a`
-- `B -> B` becomes `B -> B` (not changed)
-- `.foo -> .foo` becomes `.foo -> .foo` (not changed)
-- `.foo.bar -> blarrg.woot` becomes `.foo.bar -> blarrg.woot` (unchanged)
generalizeLowercase :: (Var v) => Set v -> Type v a -> Type v a
generalizeLowercase :: forall v a. Var v => Set v -> Type v a -> Type v a
generalizeLowercase Set v
except Type v a
t = (v -> Type v a -> Type v a) -> Type v a -> [v] -> Type v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a -> v -> Type v a -> Type v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll (Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
t)) Type v a
t [v]
vars
  where
    vars :: [v]
vars =
      [v
v | v
v <- Set v -> [v]
forall a. Set a -> [a]
Set.toList (Type v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
ABT.freeVars Type v a
t Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set v
except), v -> Bool
forall v. Var v => v -> Bool
Var.universallyQuantifyIfFree v
v]

-- Convert all free variables in `allowed` to variables bound by an `introOuter`.
freeVarsToOuters :: (Ord v) => Set v -> Type v a -> Type v a
freeVarsToOuters :: forall v a. Ord v => Set v -> Type v a -> Type v a
freeVarsToOuters Set v
allowed Type v a
t = (v -> Type v a -> Type v a) -> Type v a -> [v] -> Type v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a -> v -> Type v a -> Type v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
introOuter (Type v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Type v a
t)) Type v a
t [v]
vars
  where
    vars :: [v]
vars = Set v -> [v]
forall a. Set a -> [a]
Set.toList (Set v -> [v]) -> Set v -> [v]
forall a b. (a -> b) -> a -> b
$ Type v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
ABT.freeVars Type v a
t Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set v
allowed

-- normalizes the order that variables are introduced by a forall
-- based on the location where the variables first appear in the type
normalizeForallOrder :: forall v a. (Var v) => Type v a -> Type v a
normalizeForallOrder :: forall v a. Var v => Type v a -> Type v a
normalizeForallOrder Type v a
tm0 =
  ((a, v) -> Type v a -> Type v a)
-> Type v a -> [(a, v)] -> Type v a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a, v) -> Type v a -> Type v a
step Type v a
body [(a, v)]
vs
  where
    step :: (a, v) -> Type v a -> Type v a
    step :: (a, v) -> Type v a -> Type v a
step (a
a, v
v) Type v a
body
      | v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member v
v (Type v a -> Set v
forall (f :: * -> *) v a. Term f v a -> Set v
ABT.freeVars Type v a
body) = a -> v -> Type v a -> Type v a
forall v a. Ord v => a -> v -> Type v a -> Type v a
forAll a
a v
v Type v a
body
      | Bool
otherwise = Type v a
body
    (Type v a
body, [(a, v)]
vs0) = Type v a -> (Type v a, [(a, v)])
forall {b} {a}. Term F b a -> (Term F b a, [(a, b)])
extract Type v a
tm0
    vs :: [(a, v)]
vs = ((a, v) -> Maybe Int) -> [(a, v)] -> [(a, v)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\(a
_, v
v) -> v -> Map v Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v Int
ind) [(a, v)]
vs0
    extract :: Term F b a -> (Term F b a, [(a, b)])
extract tm :: Term F b a
tm@(ABT.Tm' (Forall (ABT.Abs'' b
v Term F b a
body))) = ((Term F b a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term F b a
tm, b
v) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:) ([(a, b)] -> [(a, b)])
-> (Term F b a, [(a, b)]) -> (Term F b a, [(a, b)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term F b a -> (Term F b a, [(a, b)])
extract Term F b a
body
    extract Term F b a
body = (Term F b a
body, [])
    ind :: Map v Int
ind = Type v a -> Map v Int
forall v (f :: * -> *) a.
(Ord v, Foldable f) =>
Term f v a -> Map v Int
ABT.numberedFreeVars Type v a
body

-- | This function removes all variable shadowing from the types and reduces
-- fresh ids to the minimum possible to avoid ambiguity. Useful when showing
-- two different types.
cleanupVars :: (Var v) => [Type v a] -> [Type v a]
cleanupVars :: forall v a. Var v => [Type v a] -> [Type v a]
cleanupVars [Type v a]
ts | Bool -> Bool
not Bool
Settings.cleanupTypes = [Type v a]
ts
cleanupVars [Type v a]
ts =
  let changedVars :: Map v v
changedVars = [Type v a] -> Map v v
forall v a. Var v => [Type v a] -> Map v v
cleanupVarsMap [Type v a]
ts
   in Map v v -> Type v a -> Type v a
forall v a. Var v => Map v v -> Type v a -> Type v a
cleanupVars1' Map v v
changedVars (Type v a -> Type v a) -> [Type v a] -> [Type v a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type v a]
ts

-- Compute a variable replacement map from a collection of types, which
-- can be passed to `cleanupVars1'`. This is used to cleanup variable ids
-- for multiple related types, like when reporting a type error.
cleanupVarsMap :: (Var v) => [Type v a] -> Map.Map v v
cleanupVarsMap :: forall v a. Var v => [Type v a] -> Map v v
cleanupVarsMap [Type v a]
ts =
  let varsByName :: Map Text [v]
varsByName = (Map Text [v] -> v -> Map Text [v])
-> Map Text [v] -> [v] -> Map Text [v]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Map Text [v] -> v -> Map Text [v]
forall {a}. Var a => Map Text [a] -> a -> Map Text [a]
step Map Text [v]
forall k a. Map k a
Map.empty ([Type v a]
ts [Type v a] -> (Type v a -> [v]) -> [v]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Type v a -> [v]
forall (f :: * -> *) v a. Foldable f => Term f v a -> [v]
ABT.allVars)
      step :: Map Text [a] -> a -> Map Text [a]
step Map Text [a]
m a
v = ([a] -> [a] -> [a]) -> Text -> [a] -> Map Text [a] -> Map Text [a]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
(++) (a -> Text
forall v. Var v => v -> Text
Var.name (a -> Text) -> a -> Text
forall a b. (a -> b) -> a -> b
$ a -> a
forall v. Var v => v -> v
Var.reset a
v) [a
v] Map Text [a]
m
      changedVars :: Map v v
changedVars =
        [(v, v)] -> Map v v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
          [ (v
v, Word64 -> v -> v
forall v. Var v => Word64 -> v -> v
Var.freshenId Word64
i v
v)
            | (Text
_, [v]
vs) <- Map Text [v] -> [(Text, [v])]
forall k a. Map k a -> [(k, a)]
Map.toList Map Text [v]
varsByName,
              (v
v, Word64
i) <- [v] -> [v]
forall a. Ord a => [a] -> [a]
nubOrd [v]
vs [v] -> [Word64] -> [(v, Word64)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Word64
0 ..]
          ]
   in Map v v
changedVars

cleanupVars1' :: (Var v) => Map.Map v v -> Type v a -> Type v a
cleanupVars1' :: forall v a. Var v => Map v v -> Type v a -> Type v a
cleanupVars1' = Map v v -> Term F v a -> Term F v a
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
ABT.changeVars

-- | This function removes all variable shadowing from the type and reduces
-- fresh ids to the minimum possible to avoid ambiguity.
cleanupVars1 :: (Var v) => Type v a -> Type v a
cleanupVars1 :: forall v a. Var v => Type v a -> Type v a
cleanupVars1 Type v a
t | Bool -> Bool
not Bool
Settings.cleanupTypes = Type v a
t
cleanupVars1 Type v a
t =
  case [Type v a] -> [Type v a]
forall v a. Var v => [Type v a] -> [Type v a]
cleanupVars [Type v a
t] of
    [Type v a
t'] -> Type v a
t'
    [Type v a]
_ -> String -> Type v a
forall a. HasCallStack => String -> a
error String
"cleanupVars1: expected exactly one result"

-- This removes duplicates and normalizes the order of ability lists
cleanupAbilityLists :: (Var v) => Type v a -> Type v a
cleanupAbilityLists :: forall v a. Var v => Type v a -> Type v a
cleanupAbilityLists = (Term F v a -> Maybe (Term F v a)) -> Term F v a -> Term F v a
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Term F v a -> Maybe (Term F v a)
forall {v} {a}. Var v => Term F v a -> Maybe (Term F v a)
go
  where
    -- leave explicitly empty `{}` alone
    go :: Term F v a -> Maybe (Term F v a)
go (Effect1' (Effects' []) Term F v a
_v) = Maybe (Term F v a)
forall a. Maybe a
Nothing
    go t :: Term F v a
t@(Effect1' Term F v a
e Term F v a
v) =
      let es :: [Term F v a]
es = Set (Term F v a) -> [Term F v a]
forall a. Set a -> [a]
Set.toList (Set (Term F v a) -> [Term F v a])
-> ([Term F v a] -> Set (Term F v a))
-> [Term F v a]
-> [Term F v a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Term F v a] -> Set (Term F v a)
forall a. Ord a => [a] -> Set a
Set.fromList ([Term F v a] -> [Term F v a]) -> [Term F v a] -> [Term F v a]
forall a b. (a -> b) -> a -> b
$ Term F v a -> [Term F v a]
forall v a. Type v a -> [Type v a]
flattenEffects Term F v a
e
       in case [Term F v a]
es of
            [] -> Term F v a -> Maybe (Term F v a)
forall a. a -> Maybe a
Just ((Term F v a -> Maybe (Term F v a)) -> Term F v a -> Term F v a
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Term F v a -> Maybe (Term F v a)
go Term F v a
v)
            [Term F v a]
_ -> Term F v a -> Maybe (Term F v a)
forall a. a -> Maybe a
Just (a -> [Term F v a] -> Term F v a -> Term F v a
forall v a. Ord v => a -> [Type v a] -> Type v a -> Type v a
effect (Term F v a -> a
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term F v a
t) [Term F v a]
es (Term F v a -> Term F v a) -> Term F v a -> Term F v a
forall a b. (a -> b) -> a -> b
$ (Term F v a -> Maybe (Term F v a)) -> Term F v a -> Term F v a
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
ABT.visitPure Term F v a -> Maybe (Term F v a)
go Term F v a
v)
    go Term F v a
_ = Maybe (Term F v a)
forall a. Maybe a
Nothing

cleanups :: (Var v) => [Type v a] -> [Type v a]
cleanups :: forall v a. Var v => [Type v a] -> [Type v a]
cleanups [Type v a]
ts = [Type v a] -> [Type v a]
forall v a. Var v => [Type v a] -> [Type v a]
cleanupVars ([Type v a] -> [Type v a]) -> [Type v a] -> [Type v a]
forall a b. (a -> b) -> a -> b
$ (Type v a -> Type v a) -> [Type v a] -> [Type v a]
forall a b. (a -> b) -> [a] -> [b]
map Type v a -> Type v a
forall v a. Var v => Type v a -> Type v a
cleanupAbilityLists [Type v a]
ts

cleanup :: (Var v) => Type v a -> Type v a
cleanup :: forall v a. Var v => Type v a -> Type v a
cleanup Type v a
t | Bool -> Bool
not Bool
Settings.cleanupTypes = Type v a
t
cleanup Type v a
t = Type v a -> Type v a
forall v a. Var v => Type v a -> Type v a
normalizeForallOrder (Type v a -> Type v a)
-> (Type v a -> Type v a) -> Type v a -> Type v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Type v a -> Type v a
forall v a. Var v => Bool -> Type v a -> Type v a
removePureEffects Bool
True (Type v a -> Type v a)
-> (Type v a -> Type v a) -> Type v a -> Type v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type v a -> Type v a
forall v a. Var v => Type v a -> Type v a
cleanupVars1 (Type v a -> Type v a)
-> (Type v a -> Type v a) -> Type v a -> Type v a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type v a -> Type v a
forall v a. Var v => Type v a -> Type v a
cleanupAbilityLists (Type v a -> Type v a) -> Type v a -> Type v a
forall a b. (a -> b) -> a -> b
$ Type v a
t

builtinAbilities :: Set TypeReference
builtinAbilities :: Set TypeReference
builtinAbilities = [TypeReference] -> Set TypeReference
forall a. Ord a => [a] -> Set a
Set.fromList [TypeReference
builtinIORef, TypeReference
stmRef]

instance (Show a) => Show (F a) where
  showsPrec :: Int -> F a -> ShowS
showsPrec = Int -> F a -> ShowS
forall a. Show a => Int -> F a -> ShowS
go
    where
      go :: Int -> F a -> ShowS
go Int
_ (Ref TypeReference
r) = TypeReference -> ShowS
forall a. Show a => a -> ShowS
shows TypeReference
r
      go Int
p (Arrow a
i a
o) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec (Int
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) a
i ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> String -> ShowS
s String
" -> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
o
      go Int
p (Ann a
t Kind
k) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ a -> ShowS
forall a. Show a => a -> ShowS
shows a
t ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> String -> ShowS
s String
":" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> Kind -> ShowS
forall a. Show a => a -> ShowS
shows Kind
k
      go Int
p (App a
f a
x) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
9 a
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> String -> ShowS
s String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 a
x
      go Int
p (Effects [a]
es) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
          String -> ShowS
s String
"{" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> [a] -> ShowS
forall a. Show a => a -> ShowS
shows [a]
es ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> String -> ShowS
s String
"}"
      go Int
p (Effect a
e a
t) =
        Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
          Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
            a -> ShowS
forall a. Show a => a -> ShowS
shows a
e ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> String -> ShowS
s String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
t
      go Int
p (Forall a
body) = case Int
p of
        Int
0 -> Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
body
        Int
_ -> Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
s String
"∀ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> a -> ShowS
forall a. Show a => a -> ShowS
shows a
body
      go Int
p (IntroOuter a
body) = case Int
p of
        Int
0 -> Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p a
body
        Int
_ -> Bool -> ShowS -> ShowS
showParen Bool
True (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
s String
"outer " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
<> a -> ShowS
forall a. Show a => a -> ShowS
shows a
body
      <> :: (b -> c) -> (a -> b) -> a -> c
(<>) = (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
      s :: String -> ShowS
s = String -> ShowS
showString