-- | Unification terms.
--
-- These represent the known state of a unification variable.

{-# LANGUAGE TemplateHaskell, UndecidableInstances #-}

module Hyper.Unify.Term
    ( UTerm(..)
        , _UUnbound, _USkolem, _UToVar, _UTerm, _UInstantiated
        , _UResolving, _UResolved, _UConverted
    , UTermBody(..), uBody, uConstraints
    ) where

import Hyper
import Hyper.Unify.Constraints (TypeConstraintsOf)

import Hyper.Internal.Prelude

-- | A unification term with a known body
data UTermBody v ast = UTermBody
    { UTermBody v ast -> TypeConstraintsOf (GetHyperType ast)
_uConstraints :: TypeConstraintsOf (GetHyperType ast)
    , UTermBody v ast -> ast :# v
_uBody :: ast :# v
    } deriving (forall x. UTermBody v ast -> Rep (UTermBody v ast) x)
-> (forall x. Rep (UTermBody v ast) x -> UTermBody v ast)
-> Generic (UTermBody v ast)
forall x. Rep (UTermBody v ast) x -> UTermBody v ast
forall x. UTermBody v ast -> Rep (UTermBody v ast) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (v :: HyperType) (ast :: AHyperType) x.
Rep (UTermBody v ast) x -> UTermBody v ast
forall (v :: HyperType) (ast :: AHyperType) x.
UTermBody v ast -> Rep (UTermBody v ast) x
$cto :: forall (v :: HyperType) (ast :: AHyperType) x.
Rep (UTermBody v ast) x -> UTermBody v ast
$cfrom :: forall (v :: HyperType) (ast :: AHyperType) x.
UTermBody v ast -> Rep (UTermBody v ast) x
Generic

-- | A unification term pointed by a unification variable
data UTerm v ast
    = UUnbound (TypeConstraintsOf (GetHyperType ast))
      -- ^ Unbound variable with at least the given constraints
    | USkolem (TypeConstraintsOf (GetHyperType ast))
      -- ^ A variable bound by a rigid quantified variable with
      -- *exactly* the given constraints
    | UToVar (v ast)
      -- ^ Unified with another variable (union-find)
    | UTerm (UTermBody v ast)
      -- ^ Known type term with unification variables as children
    | UInstantiated (v ast)
      -- ^ Temporary state during instantiation indicating which fresh
      -- unification variable a skolem is mapped to
    | UResolving (UTermBody v ast)
      -- ^ Temporary state while unification term is being traversed,
      -- if it occurs inside itself (detected via state still being
      -- UResolving), then the type is an infinite type
    | UResolved (Pure ast)
      -- ^ Final resolved state. `Hyper.Unify.applyBindings` resolved to
      -- this expression (allowing caching/sharing)
    | UConverted Int
      -- ^ Temporary state used in "Hyper.Unify.Binding.ST.Save" while
      -- converting to a pure binding
    deriving (forall x. UTerm v ast -> Rep (UTerm v ast) x)
-> (forall x. Rep (UTerm v ast) x -> UTerm v ast)
-> Generic (UTerm v ast)
forall x. Rep (UTerm v ast) x -> UTerm v ast
forall x. UTerm v ast -> Rep (UTerm v ast) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (v :: HyperType) (ast :: AHyperType) x.
Rep (UTerm v ast) x -> UTerm v ast
forall (v :: HyperType) (ast :: AHyperType) x.
UTerm v ast -> Rep (UTerm v ast) x
$cto :: forall (v :: HyperType) (ast :: AHyperType) x.
Rep (UTerm v ast) x -> UTerm v ast
$cfrom :: forall (v :: HyperType) (ast :: AHyperType) x.
UTerm v ast -> Rep (UTerm v ast) x
Generic

makePrisms ''UTerm
makeLenses ''UTermBody
makeCommonInstances [''UTerm, ''UTermBody]