{-# LANGUAGE PatternSynonyms #-}

module Unison.Typechecker.TypeVar where

import Data.Set qualified as Set
import Unison.ABT qualified as ABT
import Unison.Term (Term, Term')
import Unison.Term qualified as Term
import Unison.Type (Type)
import Unison.Var (Var)
import Unison.Var qualified as Var

data TypeVar b v = Universal v | Existential b v deriving ((forall a b. (a -> b) -> TypeVar b a -> TypeVar b b)
-> (forall a b. a -> TypeVar b b -> TypeVar b a)
-> Functor (TypeVar b)
forall a b. a -> TypeVar b b -> TypeVar b a
forall a b. (a -> b) -> TypeVar b a -> TypeVar b b
forall b a b. a -> TypeVar b b -> TypeVar b a
forall b a b. (a -> b) -> TypeVar b a -> TypeVar b b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall b a b. (a -> b) -> TypeVar b a -> TypeVar b b
fmap :: forall a b. (a -> b) -> TypeVar b a -> TypeVar b b
$c<$ :: forall b a b. a -> TypeVar b b -> TypeVar b a
<$ :: forall a b. a -> TypeVar b b -> TypeVar b a
Functor)

instance (Eq v) => Eq (TypeVar b v) where
  Universal v
v == :: TypeVar b v -> TypeVar b v -> Bool
== Universal v
v2 = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2
  Existential b
_ v
v == Existential b
_ v
v2 = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2
  TypeVar b v
_ == TypeVar b v
_ = Bool
False

instance (Ord v) => Ord (TypeVar b v) where
  Universal v
v compare :: TypeVar b v -> TypeVar b v -> Ordering
`compare` Universal v
v2 = v -> v -> Ordering
forall a. Ord a => a -> a -> Ordering
compare v
v v
v2
  Existential b
_ v
v `compare` Existential b
_ v
v2 = v -> v -> Ordering
forall a. Ord a => a -> a -> Ordering
compare v
v v
v2
  Universal v
_ `compare` Existential b
_ v
_ = Ordering
LT
  TypeVar b v
_ `compare` TypeVar b v
_ = Ordering
GT

underlying :: TypeVar b v -> v
underlying :: forall b v. TypeVar b v -> v
underlying (Universal v
v) = v
v
underlying (Existential b
_ v
v) = v
v

instance (Show v) => Show (TypeVar b v) where
  show :: TypeVar b v -> String
show (Universal v
v) = v -> String
forall a. Show a => a -> String
show v
v
  show (Existential b
_ v
v) = String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
v

instance (ABT.Var v) => ABT.Var (TypeVar b v) where
  freshIn :: Set (TypeVar b v) -> TypeVar b v -> TypeVar b v
freshIn Set (TypeVar b v)
s TypeVar b v
v = Set v -> v -> v
forall v. Var v => Set v -> v -> v
ABT.freshIn ((TypeVar b v -> v) -> Set (TypeVar b v) -> Set v
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map TypeVar b v -> v
forall b v. TypeVar b v -> v
underlying Set (TypeVar b v)
s) (v -> v) -> TypeVar b v -> TypeVar b v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeVar b v
v

instance (Var v) => Var (TypeVar b v) where
  typed :: Type -> TypeVar b v
typed Type
t = v -> TypeVar b v
forall b v. v -> TypeVar b v
Universal (Type -> v
forall v. Var v => Type -> v
Var.typed Type
t)
  typeOf :: TypeVar b v -> Type
typeOf TypeVar b v
v = v -> Type
forall v. Var v => v -> Type
Var.typeOf (TypeVar b v -> v
forall b v. TypeVar b v -> v
underlying TypeVar b v
v)
  freshId :: TypeVar b v -> Word64
freshId TypeVar b v
v = v -> Word64
forall v. Var v => v -> Word64
Var.freshId (TypeVar b v -> v
forall b v. TypeVar b v -> v
underlying TypeVar b v
v)
  freshenId :: Word64 -> TypeVar b v -> TypeVar b v
freshenId Word64
id TypeVar b v
v = Word64 -> v -> v
forall v. Var v => Word64 -> v -> v
Var.freshenId Word64
id (v -> v) -> TypeVar b v -> TypeVar b v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypeVar b v
v

liftType :: (Ord v) => Type v a -> Type (TypeVar b v) a
liftType :: forall v a b. Ord v => Type v a -> Type (TypeVar b v) a
liftType = (v -> TypeVar b v) -> Term F v a -> Term F (TypeVar b 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 -> TypeVar b v
forall b v. v -> TypeVar b v
Universal

lowerType :: (Ord v) => Type (TypeVar b v) a -> Type v a
lowerType :: forall v b a. Ord v => Type (TypeVar b v) a -> Type v a
lowerType = (TypeVar b v -> v) -> Term F (TypeVar b v) a -> Term F 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 TypeVar b v -> v
forall b v. TypeVar b v -> v
underlying

liftTerm :: (Ord v) => Term v a -> Term' (TypeVar b v) v a
liftTerm :: forall v a b. Ord v => Term v a -> Term' (TypeVar b v) v a
liftTerm = (v -> TypeVar b v) -> Term' v v a -> Term' (TypeVar b v) v a
forall vt2 vt v a.
Ord vt2 =>
(vt -> vt2) -> Term' vt v a -> Term' vt2 v a
Term.vtmap v -> TypeVar b v
forall b v. v -> TypeVar b v
Universal

lowerTerm :: (Ord v) => Term' (TypeVar b v) v a -> Term v a
lowerTerm :: forall v b a. Ord v => Term' (TypeVar b v) v a -> Term v a
lowerTerm = (TypeVar b v -> v) -> Term' (TypeVar b v) v a -> Term' v v a
forall vt2 vt v a.
Ord vt2 =>
(vt -> vt2) -> Term' vt v a -> Term' vt2 v a
Term.vtmap TypeVar b v -> v
forall b v. TypeVar b v -> v
underlying