-- | This module contains type annotations for terms of the language.
module Type.Check.HM.TyTerm(
    Ann(..)
  , TyTerm(..)
  , termType
  , tyVarE
  , tyPrimE
  , tyAppE
  , tyLamE
  , tyLetE
  , tyLetRecE
  , tyAssertTypeE
  , tyCaseE
  , tyConstrE
  , tyBottomE
  , mapType
) where

import Control.Arrow

import Data.Fix
import Data.Containers.ListUtils (nubOrdOn)
import Data.Foldable
import Data.Eq.Deriving
import Data.Ord.Deriving
import Text.Show.Deriving

import Type.Check.HM.Subst
import Type.Check.HM.Type
import Type.Check.HM.Term

import qualified Data.DList as D

-- | Type to annotate nodes of AST.
-- We use it for type annotations.
data Ann note f a = Ann
  { Ann note f a -> note
ann'note  :: note
  , Ann note f a -> f a
ann'value :: f a
  } deriving (Int -> Ann note f a -> ShowS
[Ann note f a] -> ShowS
Ann note f a -> String
(Int -> Ann note f a -> ShowS)
-> (Ann note f a -> String)
-> ([Ann note f a] -> ShowS)
-> Show (Ann note f a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall note (f :: * -> *) a.
(Show note, Show (f a)) =>
Int -> Ann note f a -> ShowS
forall note (f :: * -> *) a.
(Show note, Show (f a)) =>
[Ann note f a] -> ShowS
forall note (f :: * -> *) a.
(Show note, Show (f a)) =>
Ann note f a -> String
showList :: [Ann note f a] -> ShowS
$cshowList :: forall note (f :: * -> *) a.
(Show note, Show (f a)) =>
[Ann note f a] -> ShowS
show :: Ann note f a -> String
$cshow :: forall note (f :: * -> *) a.
(Show note, Show (f a)) =>
Ann note f a -> String
showsPrec :: Int -> Ann note f a -> ShowS
$cshowsPrec :: forall note (f :: * -> *) a.
(Show note, Show (f a)) =>
Int -> Ann note f a -> ShowS
Show, Ann note f a -> Ann note f a -> Bool
(Ann note f a -> Ann note f a -> Bool)
-> (Ann note f a -> Ann note f a -> Bool) -> Eq (Ann note f a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall note (f :: * -> *) a.
(Eq note, Eq (f a)) =>
Ann note f a -> Ann note f a -> Bool
/= :: Ann note f a -> Ann note f a -> Bool
$c/= :: forall note (f :: * -> *) a.
(Eq note, Eq (f a)) =>
Ann note f a -> Ann note f a -> Bool
== :: Ann note f a -> Ann note f a -> Bool
$c== :: forall note (f :: * -> *) a.
(Eq note, Eq (f a)) =>
Ann note f a -> Ann note f a -> Bool
Eq, a -> Ann note f b -> Ann note f a
(a -> b) -> Ann note f a -> Ann note f b
(forall a b. (a -> b) -> Ann note f a -> Ann note f b)
-> (forall a b. a -> Ann note f b -> Ann note f a)
-> Functor (Ann note f)
forall a b. a -> Ann note f b -> Ann note f a
forall a b. (a -> b) -> Ann note f a -> Ann note f b
forall note (f :: * -> *) a b.
Functor f =>
a -> Ann note f b -> Ann note f a
forall note (f :: * -> *) a b.
Functor f =>
(a -> b) -> Ann note f a -> Ann note f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Ann note f b -> Ann note f a
$c<$ :: forall note (f :: * -> *) a b.
Functor f =>
a -> Ann note f b -> Ann note f a
fmap :: (a -> b) -> Ann note f a -> Ann note f b
$cfmap :: forall note (f :: * -> *) a b.
Functor f =>
(a -> b) -> Ann note f a -> Ann note f b
Functor, Ann note f a -> Bool
(a -> m) -> Ann note f a -> m
(a -> b -> b) -> b -> Ann note f a -> b
(forall m. Monoid m => Ann note f m -> m)
-> (forall m a. Monoid m => (a -> m) -> Ann note f a -> m)
-> (forall m a. Monoid m => (a -> m) -> Ann note f a -> m)
-> (forall a b. (a -> b -> b) -> b -> Ann note f a -> b)
-> (forall a b. (a -> b -> b) -> b -> Ann note f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ann note f a -> b)
-> (forall b a. (b -> a -> b) -> b -> Ann note f a -> b)
-> (forall a. (a -> a -> a) -> Ann note f a -> a)
-> (forall a. (a -> a -> a) -> Ann note f a -> a)
-> (forall a. Ann note f a -> [a])
-> (forall a. Ann note f a -> Bool)
-> (forall a. Ann note f a -> Int)
-> (forall a. Eq a => a -> Ann note f a -> Bool)
-> (forall a. Ord a => Ann note f a -> a)
-> (forall a. Ord a => Ann note f a -> a)
-> (forall a. Num a => Ann note f a -> a)
-> (forall a. Num a => Ann note f a -> a)
-> Foldable (Ann note f)
forall a. Eq a => a -> Ann note f a -> Bool
forall a. Num a => Ann note f a -> a
forall a. Ord a => Ann note f a -> a
forall m. Monoid m => Ann note f m -> m
forall a. Ann note f a -> Bool
forall a. Ann note f a -> Int
forall a. Ann note f a -> [a]
forall a. (a -> a -> a) -> Ann note f a -> a
forall m a. Monoid m => (a -> m) -> Ann note f a -> m
forall b a. (b -> a -> b) -> b -> Ann note f a -> b
forall a b. (a -> b -> b) -> b -> Ann note f a -> b
forall note (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Ann note f a -> Bool
forall note (f :: * -> *) a.
(Foldable f, Num a) =>
Ann note f a -> a
forall note (f :: * -> *) a.
(Foldable f, Ord a) =>
Ann note f a -> a
forall note (f :: * -> *) m.
(Foldable f, Monoid m) =>
Ann note f m -> m
forall note (f :: * -> *) a. Foldable f => Ann note f a -> Bool
forall note (f :: * -> *) a. Foldable f => Ann note f a -> Int
forall note (f :: * -> *) a. Foldable f => Ann note f a -> [a]
forall note (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Ann note f a -> a
forall note (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Ann note f a -> m
forall note (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Ann note f a -> b
forall note (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Ann note 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
product :: Ann note f a -> a
$cproduct :: forall note (f :: * -> *) a.
(Foldable f, Num a) =>
Ann note f a -> a
sum :: Ann note f a -> a
$csum :: forall note (f :: * -> *) a.
(Foldable f, Num a) =>
Ann note f a -> a
minimum :: Ann note f a -> a
$cminimum :: forall note (f :: * -> *) a.
(Foldable f, Ord a) =>
Ann note f a -> a
maximum :: Ann note f a -> a
$cmaximum :: forall note (f :: * -> *) a.
(Foldable f, Ord a) =>
Ann note f a -> a
elem :: a -> Ann note f a -> Bool
$celem :: forall note (f :: * -> *) a.
(Foldable f, Eq a) =>
a -> Ann note f a -> Bool
length :: Ann note f a -> Int
$clength :: forall note (f :: * -> *) a. Foldable f => Ann note f a -> Int
null :: Ann note f a -> Bool
$cnull :: forall note (f :: * -> *) a. Foldable f => Ann note f a -> Bool
toList :: Ann note f a -> [a]
$ctoList :: forall note (f :: * -> *) a. Foldable f => Ann note f a -> [a]
foldl1 :: (a -> a -> a) -> Ann note f a -> a
$cfoldl1 :: forall note (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Ann note f a -> a
foldr1 :: (a -> a -> a) -> Ann note f a -> a
$cfoldr1 :: forall note (f :: * -> *) a.
Foldable f =>
(a -> a -> a) -> Ann note f a -> a
foldl' :: (b -> a -> b) -> b -> Ann note f a -> b
$cfoldl' :: forall note (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Ann note f a -> b
foldl :: (b -> a -> b) -> b -> Ann note f a -> b
$cfoldl :: forall note (f :: * -> *) b a.
Foldable f =>
(b -> a -> b) -> b -> Ann note f a -> b
foldr' :: (a -> b -> b) -> b -> Ann note f a -> b
$cfoldr' :: forall note (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Ann note f a -> b
foldr :: (a -> b -> b) -> b -> Ann note f a -> b
$cfoldr :: forall note (f :: * -> *) a b.
Foldable f =>
(a -> b -> b) -> b -> Ann note f a -> b
foldMap' :: (a -> m) -> Ann note f a -> m
$cfoldMap' :: forall note (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Ann note f a -> m
foldMap :: (a -> m) -> Ann note f a -> m
$cfoldMap :: forall note (f :: * -> *) m a.
(Foldable f, Monoid m) =>
(a -> m) -> Ann note f a -> m
fold :: Ann note f m -> m
$cfold :: forall note (f :: * -> *) m.
(Foldable f, Monoid m) =>
Ann note f m -> m
Foldable, Functor (Ann note f)
Foldable (Ann note f)
Functor (Ann note f)
-> Foldable (Ann note f)
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Ann note f a -> f (Ann note f b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Ann note f (f a) -> f (Ann note f a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Ann note f a -> m (Ann note f b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Ann note f (m a) -> m (Ann note f a))
-> Traversable (Ann note f)
(a -> f b) -> Ann note f a -> f (Ann note f b)
forall note (f :: * -> *). Traversable f => Functor (Ann note f)
forall note (f :: * -> *). Traversable f => Foldable (Ann note f)
forall note (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Ann note f (m a) -> m (Ann note f a)
forall note (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Ann note f (f a) -> f (Ann note f a)
forall note (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Ann note f a -> m (Ann note f b)
forall note (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Ann note f a -> f (Ann note f b)
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 =>
Ann note f (m a) -> m (Ann note f a)
forall (f :: * -> *) a.
Applicative f =>
Ann note f (f a) -> f (Ann note f a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ann note f a -> m (Ann note f b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ann note f a -> f (Ann note f b)
sequence :: Ann note f (m a) -> m (Ann note f a)
$csequence :: forall note (f :: * -> *) (m :: * -> *) a.
(Traversable f, Monad m) =>
Ann note f (m a) -> m (Ann note f a)
mapM :: (a -> m b) -> Ann note f a -> m (Ann note f b)
$cmapM :: forall note (f :: * -> *) (m :: * -> *) a b.
(Traversable f, Monad m) =>
(a -> m b) -> Ann note f a -> m (Ann note f b)
sequenceA :: Ann note f (f a) -> f (Ann note f a)
$csequenceA :: forall note (f :: * -> *) (f :: * -> *) a.
(Traversable f, Applicative f) =>
Ann note f (f a) -> f (Ann note f a)
traverse :: (a -> f b) -> Ann note f a -> f (Ann note f b)
$ctraverse :: forall note (f :: * -> *) (f :: * -> *) a b.
(Traversable f, Applicative f) =>
(a -> f b) -> Ann note f a -> f (Ann note f b)
$cp2Traversable :: forall note (f :: * -> *). Traversable f => Foldable (Ann note f)
$cp1Traversable :: forall note (f :: * -> *). Traversable f => Functor (Ann note f)
Traversable)

$(deriveShow1 ''Ann)
$(deriveEq1   ''Ann)
$(deriveOrd1  ''Ann)


-- | Terms with type annotations for all subexpressions.
newtype TyTerm prim loc v = TyTerm { TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v))
unTyTerm :: Fix (Ann (Type loc v) (TermF prim loc v)) }
  deriving (Int -> TyTerm prim loc v -> ShowS
[TyTerm prim loc v] -> ShowS
TyTerm prim loc v -> String
(Int -> TyTerm prim loc v -> ShowS)
-> (TyTerm prim loc v -> String)
-> ([TyTerm prim loc v] -> ShowS)
-> Show (TyTerm prim loc v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall prim loc v.
(Show loc, Show v, Show prim) =>
Int -> TyTerm prim loc v -> ShowS
forall prim loc v.
(Show loc, Show v, Show prim) =>
[TyTerm prim loc v] -> ShowS
forall prim loc v.
(Show loc, Show v, Show prim) =>
TyTerm prim loc v -> String
showList :: [TyTerm prim loc v] -> ShowS
$cshowList :: forall prim loc v.
(Show loc, Show v, Show prim) =>
[TyTerm prim loc v] -> ShowS
show :: TyTerm prim loc v -> String
$cshow :: forall prim loc v.
(Show loc, Show v, Show prim) =>
TyTerm prim loc v -> String
showsPrec :: Int -> TyTerm prim loc v -> ShowS
$cshowsPrec :: forall prim loc v.
(Show loc, Show v, Show prim) =>
Int -> TyTerm prim loc v -> ShowS
Show, TyTerm prim loc v -> TyTerm prim loc v -> Bool
(TyTerm prim loc v -> TyTerm prim loc v -> Bool)
-> (TyTerm prim loc v -> TyTerm prim loc v -> Bool)
-> Eq (TyTerm prim loc v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall prim loc v.
(Eq loc, Eq v, Eq prim) =>
TyTerm prim loc v -> TyTerm prim loc v -> Bool
/= :: TyTerm prim loc v -> TyTerm prim loc v -> Bool
$c/= :: forall prim loc v.
(Eq loc, Eq v, Eq prim) =>
TyTerm prim loc v -> TyTerm prim loc v -> Bool
== :: TyTerm prim loc v -> TyTerm prim loc v -> Bool
$c== :: forall prim loc v.
(Eq loc, Eq v, Eq prim) =>
TyTerm prim loc v -> TyTerm prim loc v -> Bool
Eq)

termType :: TyTerm prim loc v -> Type loc v
termType :: TyTerm prim loc v -> Type loc v
termType (TyTerm (Fix (Ann Type loc v
ty TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
_))) = Type loc v
ty

-- tyTerm :: Type loc v -> TermF loc var (Ann () ) -> TyTerm loc var
tyTerm :: Type loc v -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))) -> TyTerm prim loc v
tyTerm :: Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
x = Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
forall prim loc v.
Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
TyTerm (Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v)
-> Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ Ann
  (Type loc v)
  (TermF prim loc v)
  (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Fix (Ann (Type loc v) (TermF prim loc v))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Ann
   (Type loc v)
   (TermF prim loc v)
   (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> Fix (Ann (Type loc v) (TermF prim loc v)))
-> Ann
     (Type loc v)
     (TermF prim loc v)
     (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Fix (Ann (Type loc v) (TermF prim loc v))
forall a b. (a -> b) -> a -> b
$ Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Ann
     (Type loc v)
     (TermF prim loc v)
     (Fix (Ann (Type loc v) (TermF prim loc v)))
forall note (f :: * -> *) a. note -> f a -> Ann note f a
Ann Type loc v
ty TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
x

-- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.
tyVarE :: Type loc var -> loc -> var -> TyTerm prim loc var
tyVarE :: Type loc var -> loc -> var -> TyTerm prim loc var
tyVarE Type loc var
ty loc
loc var
var =  Type loc var
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> TyTerm prim loc var
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc var
ty (TermF prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> TyTerm prim loc var)
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> TyTerm prim loc var
forall a b. (a -> b) -> a -> b
$ loc
-> var
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
forall prim loc v r. loc -> v -> TermF prim loc v r
Var loc
loc var
var

-- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.
tyPrimE :: Type loc var -> loc -> prim -> TyTerm prim loc var
tyPrimE :: Type loc var -> loc -> prim -> TyTerm prim loc var
tyPrimE Type loc var
ty loc
loc prim
prim =  Type loc var
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> TyTerm prim loc var
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc var
ty (TermF prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> TyTerm prim loc var)
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> TyTerm prim loc var
forall a b. (a -> b) -> a -> b
$ loc
-> prim
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
forall prim loc v r. loc -> prim -> TermF prim loc v r
Prim loc
loc prim
prim

-- | 'appE' @loc a b@ constructs an application of @a@ to @b@ with source code at @loc@.
tyAppE :: Type loc v -> loc -> TyTerm prim loc v -> TyTerm prim loc v -> TyTerm prim loc v
tyAppE :: Type loc v
-> loc
-> TyTerm prim loc v
-> TyTerm prim loc v
-> TyTerm prim loc v
tyAppE Type loc v
ty loc
loc (TyTerm Fix (Ann (Type loc v) (TermF prim loc v))
l) (TyTerm Fix (Ann (Type loc v) (TermF prim loc v))
r) = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> r -> r -> TermF prim loc v r
App loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
l Fix (Ann (Type loc v) (TermF prim loc v))
r

-- | 'lamE' @loc x e@ constructs an abstraction of @x@ over @e@ with source code at @loc@.
tyLamE :: Type loc v -> loc -> v -> TyTerm prim loc v -> TyTerm prim loc v
tyLamE :: Type loc v -> loc -> v -> TyTerm prim loc v -> TyTerm prim loc v
tyLamE Type loc v
ty loc
loc v
x (TyTerm Fix (Ann (Type loc v) (TermF prim loc v))
e) = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc
-> v
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> v -> r -> TermF prim loc v r
Lam loc
loc v
x Fix (Ann (Type loc v) (TermF prim loc v))
e

-- | 'letE' @loc binds e@ constructs a binding of @binds@ in @e@ with source code at @loc@.
-- No recursive bindings.
tyLetE :: Type loc v -> loc -> Bind loc v (TyTerm prim loc v) -> TyTerm prim loc v -> TyTerm prim loc v
tyLetE :: Type loc v
-> loc
-> Bind loc v (TyTerm prim loc v)
-> TyTerm prim loc v
-> TyTerm prim loc v
tyLetE Type loc v
ty loc
loc Bind loc v (TyTerm prim loc v)
bind (TyTerm Fix (Ann (Type loc v) (TermF prim loc v))
e) = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc
-> Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> Bind loc v r -> r -> TermF prim loc v r
Let loc
loc ((TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind loc v (TyTerm prim loc v)
-> Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v))
forall prim loc v.
TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v))
unTyTerm Bind loc v (TyTerm prim loc v)
bind) Fix (Ann (Type loc v) (TermF prim loc v))
e

-- | 'letRecE' @loc binds e@ constructs a recursive binding of @binds@ in @e@ with source code at @loc@.
tyLetRecE :: Type loc v -> loc -> [Bind loc v (TyTerm prim loc v)] -> TyTerm prim loc v -> TyTerm prim loc v
tyLetRecE :: Type loc v
-> loc
-> [Bind loc v (TyTerm prim loc v)]
-> TyTerm prim loc v
-> TyTerm prim loc v
tyLetRecE Type loc v
ty loc
loc [Bind loc v (TyTerm prim loc v)]
binds (TyTerm Fix (Ann (Type loc v) (TermF prim loc v))
e) = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc
-> [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r.
loc -> [Bind loc v r] -> r -> TermF prim loc v r
LetRec loc
loc ((Bind loc v (TyTerm prim loc v)
 -> Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> [Bind loc v (TyTerm prim loc v)]
-> [Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v)))
-> Bind loc v (TyTerm prim loc v)
-> Bind loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v))
forall prim loc v.
TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v))
unTyTerm) [Bind loc v (TyTerm prim loc v)]
binds) Fix (Ann (Type loc v) (TermF prim loc v))
e

-- | 'assertTypeE' @loc term ty@ constructs assertion of the type @ty@ to @term@.
tyAssertTypeE :: loc -> TyTerm prim loc v -> Type loc v -> TyTerm prim loc v
tyAssertTypeE :: loc -> TyTerm prim loc v -> Type loc v -> TyTerm prim loc v
tyAssertTypeE loc
loc (TyTerm Fix (Ann (Type loc v) (TermF prim loc v))
a) Type loc v
ty = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> r -> Type loc v -> TermF prim loc v r
AssertType loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
a Type loc v
ty

-- | 'caseE' @loc expr alts@ constructs case alternatives expression.
tyCaseE :: Type loc v -> loc -> TyTerm prim loc v -> [CaseAlt loc v (TyTerm prim loc v)] -> TyTerm prim loc v
tyCaseE :: Type loc v
-> loc
-> TyTerm prim loc v
-> [CaseAlt loc v (TyTerm prim loc v)]
-> TyTerm prim loc v
tyCaseE Type loc v
ty loc
loc (TyTerm Fix (Ann (Type loc v) (TermF prim loc v))
e) [CaseAlt loc v (TyTerm prim loc v)]
alts = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc
-> Fix (Ann (Type loc v) (TermF prim loc v))
-> [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r.
loc -> r -> [CaseAlt loc v r] -> TermF prim loc v r
Case loc
loc Fix (Ann (Type loc v) (TermF prim loc v))
e ([CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
 -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall a b. (a -> b) -> a -> b
$ (CaseAlt loc v (TyTerm prim loc v)
 -> CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v))))
-> [CaseAlt loc v (TyTerm prim loc v)]
-> [CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v)))
-> CaseAlt loc v (TyTerm prim loc v)
-> CaseAlt loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v))
forall prim loc v.
TyTerm prim loc v -> Fix (Ann (Type loc v) (TermF prim loc v))
unTyTerm) [CaseAlt loc v (TyTerm prim loc v)]
alts

-- | 'constrE' @loc ty tag arity@ constructs constructor tag expression.
tyConstrE :: loc -> Type loc v -> v -> TyTerm prim loc v
tyConstrE :: loc -> Type loc v -> v -> TyTerm prim loc v
tyConstrE loc
loc Type loc v
ty v
tag = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc
-> Type loc v
-> v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> Type loc v -> v -> TermF prim loc v r
Constr loc
loc Type loc v
ty v
tag

-- | 'bottomE' @loc@ constructs bottom value.
tyBottomE :: Type loc v -> loc -> TyTerm prim loc v
tyBottomE :: Type loc v -> loc -> TyTerm prim loc v
tyBottomE Type loc v
ty loc
loc = Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall loc v prim.
Type loc v
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
tyTerm Type loc v
ty (TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
 -> TyTerm prim loc v)
-> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
-> TyTerm prim loc v
forall a b. (a -> b) -> a -> b
$ loc -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v)))
forall prim loc v r. loc -> TermF prim loc v r
Bottom loc
loc

instance LocFunctor (TyTerm prim) where
  mapLoc :: (locA -> locB) -> TyTerm prim locA var -> TyTerm prim locB var
mapLoc locA -> locB
f (TyTerm Fix (Ann (Type locA var) (TermF prim locA var))
x) = Fix (Ann (Type locB var) (TermF prim locB var))
-> TyTerm prim locB var
forall prim loc v.
Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
TyTerm (Fix (Ann (Type locB var) (TermF prim locB var))
 -> TyTerm prim locB var)
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> TyTerm prim locB var
forall a b. (a -> b) -> a -> b
$ (Ann
   (Type locA var)
   (TermF prim locA var)
   (Fix (Ann (Type locB var) (TermF prim locB var)))
 -> Fix (Ann (Type locB var) (TermF prim locB var)))
-> Fix (Ann (Type locA var) (TermF prim locA var))
-> Fix (Ann (Type locB var) (TermF prim locB var))
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix Ann
  (Type locA var)
  (TermF prim locA var)
  (Fix (Ann (Type locB var) (TermF prim locB var)))
-> Fix (Ann (Type locB var) (TermF prim locB var))
go Fix (Ann (Type locA var) (TermF prim locA var))
x
    where
      go :: Ann
  (Type locA var)
  (TermF prim locA var)
  (Fix (Ann (Type locB var) (TermF prim locB var)))
-> Fix (Ann (Type locB var) (TermF prim locB var))
go (Ann Type locA var
annTy TermF
  prim locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
term) = Ann
  (Type locB var)
  (TermF prim locB var)
  (Fix (Ann (Type locB var) (TermF prim locB var)))
-> Fix (Ann (Type locB var) (TermF prim locB var))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Ann
   (Type locB var)
   (TermF prim locB var)
   (Fix (Ann (Type locB var) (TermF prim locB var)))
 -> Fix (Ann (Type locB var) (TermF prim locB var)))
-> Ann
     (Type locB var)
     (TermF prim locB var)
     (Fix (Ann (Type locB var) (TermF prim locB var)))
-> Fix (Ann (Type locB var) (TermF prim locB var))
forall a b. (a -> b) -> a -> b
$ Type locB var
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
-> Ann
     (Type locB var)
     (TermF prim locB var)
     (Fix (Ann (Type locB var) (TermF prim locB var)))
forall note (f :: * -> *) a. note -> f a -> Ann note f a
Ann ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
annTy) (TermF
   prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
 -> Ann
      (Type locB var)
      (TermF prim locB var)
      (Fix (Ann (Type locB var) (TermF prim locB var))))
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
-> Ann
     (Type locB var)
     (TermF prim locB var)
     (Fix (Ann (Type locB var) (TermF prim locB var)))
forall a b. (a -> b) -> a -> b
$ case TermF
  prim locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
term of
        Var locA
loc var
v    -> locB
-> var
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> v -> TermF prim loc v r
Var (locA -> locB
f locA
loc) var
v
        Prim locA
loc prim
p   -> locB
-> prim
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> prim -> TermF prim loc v r
Prim (locA -> locB
f locA
loc) prim
p
        App locA
loc Fix (Ann (Type locB var) (TermF prim locB var))
a Fix (Ann (Type locB var) (TermF prim locB var))
b  -> locB
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> r -> r -> TermF prim loc v r
App (locA -> locB
f locA
loc) Fix (Ann (Type locB var) (TermF prim locB var))
a Fix (Ann (Type locB var) (TermF prim locB var))
b
        Lam locA
loc var
v Fix (Ann (Type locB var) (TermF prim locB var))
a  -> locB
-> var
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> v -> r -> TermF prim loc v r
Lam (locA -> locB
f locA
loc) var
v Fix (Ann (Type locB var) (TermF prim locB var))
a
        Let locA
loc Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
v Fix (Ann (Type locB var) (TermF prim locB var))
a  -> locB
-> Bind locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> Bind loc v r -> r -> TermF prim loc v r
Let (locA -> locB
f locA
loc) (Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
v { bind'loc :: locB
bind'loc = locA -> locB
f (locA -> locB) -> locA -> locB
forall a b. (a -> b) -> a -> b
$ Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
-> locA
forall loc var r. Bind loc var r -> loc
bind'loc Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
v }) Fix (Ann (Type locB var) (TermF prim locB var))
a
        LetRec locA
loc [Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))]
vs Fix (Ann (Type locB var) (TermF prim locB var))
a -> locB
-> [Bind
      locB var (Fix (Ann (Type locB var) (TermF prim locB var)))]
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r.
loc -> [Bind loc v r] -> r -> TermF prim loc v r
LetRec (locA -> locB
f locA
loc) ((Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
 -> Bind locB var (Fix (Ann (Type locB var) (TermF prim locB var))))
-> [Bind
      locA var (Fix (Ann (Type locB var) (TermF prim locB var)))]
-> [Bind
      locB var (Fix (Ann (Type locB var) (TermF prim locB var)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
b ->  Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
b { bind'loc :: locB
bind'loc = locA -> locB
f (locA -> locB) -> locA -> locB
forall a b. (a -> b) -> a -> b
$ Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
-> locA
forall loc var r. Bind loc var r -> loc
bind'loc Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
b }) [Bind locA var (Fix (Ann (Type locB var) (TermF prim locB var)))]
vs) Fix (Ann (Type locB var) (TermF prim locB var))
a
        AssertType locA
loc Fix (Ann (Type locB var) (TermF prim locB var))
r Type locA var
sig -> locB
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> Type locB var
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> r -> Type loc v -> TermF prim loc v r
AssertType (locA -> locB
f locA
loc) Fix (Ann (Type locB var) (TermF prim locB var))
r ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
sig)
        Constr locA
loc Type locA var
ty var
v -> locB
-> Type locB var
-> var
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> Type loc v -> v -> TermF prim loc v r
Constr (locA -> locB
f locA
loc) ((locA -> locB) -> Type locA var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc locA -> locB
f Type locA var
ty) var
v
        Case locA
loc Fix (Ann (Type locB var) (TermF prim locB var))
e [CaseAlt
   locA var (Fix (Ann (Type locB var) (TermF prim locB var)))]
alts -> locB
-> Fix (Ann (Type locB var) (TermF prim locB var))
-> [CaseAlt
      locB var (Fix (Ann (Type locB var) (TermF prim locB var)))]
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r.
loc -> r -> [CaseAlt loc v r] -> TermF prim loc v r
Case (locA -> locB
f locA
loc) Fix (Ann (Type locB var) (TermF prim locB var))
e ((CaseAlt locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
 -> CaseAlt
      locB var (Fix (Ann (Type locB var) (TermF prim locB var))))
-> [CaseAlt
      locA var (Fix (Ann (Type locB var) (TermF prim locB var)))]
-> [CaseAlt
      locB var (Fix (Ann (Type locB var) (TermF prim locB var)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((locA -> locB)
-> CaseAlt
     locA var (Fix (Ann (Type locB var) (TermF prim locB var)))
-> CaseAlt
     locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall t locB var a.
(t -> locB) -> CaseAlt t var a -> CaseAlt locB var a
mapAlt locA -> locB
f) [CaseAlt
   locA var (Fix (Ann (Type locB var) (TermF prim locB var)))]
alts)
        Bottom locA
loc -> locB
-> TermF
     prim locB var (Fix (Ann (Type locB var) (TermF prim locB var)))
forall prim loc v r. loc -> TermF prim loc v r
Bottom (locA -> locB
f locA
loc)

      mapAlt :: (t -> locB) -> CaseAlt t var a -> CaseAlt locB var a
mapAlt t -> locB
g alt :: CaseAlt t var a
alt@CaseAlt{a
t
var
[Typed t var (t, var)]
Type t var
caseAlt'rhs :: forall loc v a. CaseAlt loc v a -> a
caseAlt'constrType :: forall loc v a. CaseAlt loc v a -> Type loc v
caseAlt'args :: forall loc v a. CaseAlt loc v a -> [Typed loc v (loc, v)]
caseAlt'tag :: forall loc v a. CaseAlt loc v a -> v
caseAlt'loc :: forall loc v a. CaseAlt loc v a -> loc
caseAlt'rhs :: a
caseAlt'constrType :: Type t var
caseAlt'args :: [Typed t var (t, var)]
caseAlt'tag :: var
caseAlt'loc :: t
..} = CaseAlt t var a
alt
        { caseAlt'loc :: locB
caseAlt'loc  = t -> locB
g t
caseAlt'loc
        , caseAlt'args :: [Typed locB var (locB, var)]
caseAlt'args = (Typed t var (t, var) -> Typed locB var (locB, var))
-> [Typed t var (t, var)] -> [Typed locB var (locB, var)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t -> locB) -> Typed t var (t, var) -> Typed locB var (locB, var)
forall b c v d. (b -> c) -> Typed b v (b, d) -> Typed c v (c, d)
mapTyped t -> locB
g) [Typed t var (t, var)]
caseAlt'args
        , caseAlt'constrType :: Type locB var
caseAlt'constrType = (t -> locB) -> Type t var -> Type locB var
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc t -> locB
g Type t var
caseAlt'constrType
        }

      mapTyped :: (b -> c) -> Typed b v (b, d) -> Typed c v (c, d)
mapTyped b -> c
g (Typed Type b v
ty (b, d)
val) = Type c v -> (c, d) -> Typed c v (c, d)
forall loc v a. Type loc v -> a -> Typed loc v a
Typed ((b -> c) -> Type b v -> Type c v
forall (f :: * -> * -> *) locA locB var.
LocFunctor f =>
(locA -> locB) -> f locA var -> f locB var
mapLoc b -> c
g Type b v
ty) ((b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first b -> c
g (b, d)
val)

instance TypeFunctor (TyTerm prim) where
  mapType :: (Type loc var -> Type loc var)
-> TyTerm prim loc var -> TyTerm prim loc var
mapType Type loc var -> Type loc var
f (TyTerm Fix (Ann (Type loc var) (TermF prim loc var))
x) = Fix (Ann (Type loc var) (TermF prim loc var))
-> TyTerm prim loc var
forall prim loc v.
Fix (Ann (Type loc v) (TermF prim loc v)) -> TyTerm prim loc v
TyTerm (Fix (Ann (Type loc var) (TermF prim loc var))
 -> TyTerm prim loc var)
-> Fix (Ann (Type loc var) (TermF prim loc var))
-> TyTerm prim loc var
forall a b. (a -> b) -> a -> b
$ (Ann
   (Type loc var)
   (TermF prim loc var)
   (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> Fix (Ann (Type loc var) (TermF prim loc var)))
-> Fix (Ann (Type loc var) (TermF prim loc var))
-> Fix (Ann (Type loc var) (TermF prim loc var))
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix Ann
  (Type loc var)
  (TermF prim loc var)
  (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Fix (Ann (Type loc var) (TermF prim loc var))
go Fix (Ann (Type loc var) (TermF prim loc var))
x
    where
      go :: Ann
  (Type loc var)
  (TermF prim loc var)
  (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Fix (Ann (Type loc var) (TermF prim loc var))
go (Ann Type loc var
ty TermF prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
term) = Ann
  (Type loc var)
  (TermF prim loc var)
  (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Fix (Ann (Type loc var) (TermF prim loc var))
forall (f :: * -> *). f (Fix f) -> Fix f
Fix (Ann
   (Type loc var)
   (TermF prim loc var)
   (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> Fix (Ann (Type loc var) (TermF prim loc var)))
-> Ann
     (Type loc var)
     (TermF prim loc var)
     (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Fix (Ann (Type loc var) (TermF prim loc var))
forall a b. (a -> b) -> a -> b
$ Type loc var
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Ann
     (Type loc var)
     (TermF prim loc var)
     (Fix (Ann (Type loc var) (TermF prim loc var)))
forall note (f :: * -> *) a. note -> f a -> Ann note f a
Ann (Type loc var -> Type loc var
f Type loc var
ty) (TermF prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> Ann
      (Type loc var)
      (TermF prim loc var)
      (Fix (Ann (Type loc var) (TermF prim loc var))))
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> Ann
     (Type loc var)
     (TermF prim loc var)
     (Fix (Ann (Type loc var) (TermF prim loc var)))
forall a b. (a -> b) -> a -> b
$
        case TermF prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
term of
          Constr loc
loc Type loc var
cty var
cons -> loc
-> Type loc var
-> var
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
forall prim loc v r. loc -> Type loc v -> v -> TermF prim loc v r
Constr loc
loc (Type loc var -> Type loc var
f Type loc var
cty) var
cons
          Case loc
loc Fix (Ann (Type loc var) (TermF prim loc var))
e [CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))]
alts          -> loc
-> Fix (Ann (Type loc var) (TermF prim loc var))
-> [CaseAlt
      loc var (Fix (Ann (Type loc var) (TermF prim loc var)))]
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
forall prim loc v r.
loc -> r -> [CaseAlt loc v r] -> TermF prim loc v r
Case loc
loc Fix (Ann (Type loc var) (TermF prim loc var))
e ([CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))]
 -> TermF
      prim loc var (Fix (Ann (Type loc var) (TermF prim loc var))))
-> [CaseAlt
      loc var (Fix (Ann (Type loc var) (TermF prim loc var)))]
-> TermF
     prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
forall a b. (a -> b) -> a -> b
$ (CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
 -> CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var))))
-> [CaseAlt
      loc var (Fix (Ann (Type loc var) (TermF prim loc var)))]
-> [CaseAlt
      loc var (Fix (Ann (Type loc var) (TermF prim loc var)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
applyAlt [CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))]
alts
          TermF prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
other                    -> TermF prim loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
other

      applyAlt :: CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
-> CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
applyAlt alt :: CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
alt@CaseAlt{loc
var
[Typed loc var (loc, var)]
Fix (Ann (Type loc var) (TermF prim loc var))
Type loc var
caseAlt'rhs :: Fix (Ann (Type loc var) (TermF prim loc var))
caseAlt'constrType :: Type loc var
caseAlt'args :: [Typed loc var (loc, var)]
caseAlt'tag :: var
caseAlt'loc :: loc
caseAlt'rhs :: forall loc v a. CaseAlt loc v a -> a
caseAlt'constrType :: forall loc v a. CaseAlt loc v a -> Type loc v
caseAlt'args :: forall loc v a. CaseAlt loc v a -> [Typed loc v (loc, v)]
caseAlt'tag :: forall loc v a. CaseAlt loc v a -> v
caseAlt'loc :: forall loc v a. CaseAlt loc v a -> loc
..} = CaseAlt loc var (Fix (Ann (Type loc var) (TermF prim loc var)))
alt
        { caseAlt'args :: [Typed loc var (loc, var)]
caseAlt'args       = (Typed loc var (loc, var) -> Typed loc var (loc, var))
-> [Typed loc var (loc, var)] -> [Typed loc var (loc, var)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Typed loc var (loc, var) -> Typed loc var (loc, var)
applyTyped [Typed loc var (loc, var)]
caseAlt'args
        , caseAlt'constrType :: Type loc var
caseAlt'constrType = Type loc var -> Type loc var
f Type loc var
caseAlt'constrType
        }

      applyTyped :: Typed loc var (loc, var) -> Typed loc var (loc, var)
applyTyped ty :: Typed loc var (loc, var)
ty@Typed{(loc, var)
Type loc var
typed'value :: forall loc v a. Typed loc v a -> a
typed'type :: forall loc v a. Typed loc v a -> Type loc v
typed'value :: (loc, var)
typed'type :: Type loc var
..} = Typed loc var (loc, var)
ty { typed'type :: Type loc var
typed'type = Type loc var -> Type loc var
f Type loc var
typed'type }

instance CanApply (TyTerm prim) where
  apply :: Subst loc v -> TyTerm prim loc v -> TyTerm prim loc v
apply Subst loc v
subst TyTerm prim loc v
term = (Type loc v -> Type loc v)
-> TyTerm prim loc v -> TyTerm prim loc v
forall (f :: * -> * -> *) loc var.
TypeFunctor f =>
(Type loc var -> Type loc var) -> f loc var -> f loc var
mapType (Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
subst) TyTerm prim loc v
term

instance HasTypeVars (TyTerm prim) where
  tyVars :: TyTerm prim src var -> VarSet src var
tyVars (TyTerm Fix (Ann (Type src var) (TermF prim src var))
x) = (Ann (Type src var) (TermF prim src var) (VarSet src var)
 -> VarSet src var)
-> Fix (Ann (Type src var) (TermF prim src var)) -> VarSet src var
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix (\(Ann Type src var
ty TermF prim src var (VarSet src var)
term) -> Type src var -> VarSet src var
forall (f :: * -> * -> *) var src.
(HasTypeVars f, Ord var) =>
f src var -> VarSet src var
tyVars Type src var
ty VarSet src var -> VarSet src var -> VarSet src var
forall a. Semigroup a => a -> a -> a
<> TermF prim src var (VarSet src var) -> VarSet src var
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TermF prim src var (VarSet src var)
term) Fix (Ann (Type src var) (TermF prim src var))
x

  tyVarsInOrder :: TyTerm prim src var -> [(var, src)]
tyVarsInOrder (TyTerm Fix (Ann (Type src var) (TermF prim src var))
x) =
    ((var, src) -> var) -> [(var, src)] -> [(var, src)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn (var, src) -> var
forall a b. (a, b) -> a
fst ([(var, src)] -> [(var, src)]) -> [(var, src)] -> [(var, src)]
forall a b. (a -> b) -> a -> b
$ DList (var, src) -> [(var, src)]
forall a. DList a -> [a]
D.toList (DList (var, src) -> [(var, src)])
-> DList (var, src) -> [(var, src)]
forall a b. (a -> b) -> a -> b
$ (Ann (Type src var) (TermF prim src var) (DList (var, src))
 -> DList (var, src))
-> Fix (Ann (Type src var) (TermF prim src var))
-> DList (var, src)
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix (\(Ann Type src var
ty TermF prim src var (DList (var, src))
term) -> [(var, src)] -> DList (var, src)
forall a. [a] -> DList a
D.fromList (Type src var -> [(var, src)]
forall (f :: * -> * -> *) src var.
(HasTypeVars f, Eq src, Ord var) =>
f src var -> [(var, src)]
tyVarsInOrder Type src var
ty) DList (var, src) -> DList (var, src) -> DList (var, src)
forall a. Semigroup a => a -> a -> a
<> TermF prim src var (DList (var, src)) -> DList (var, src)
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold TermF prim src var (DList (var, src))
term) Fix (Ann (Type src var) (TermF prim src var))
x