{-# LANGUAGE RecordWildCards #-}

module Unison.Typechecker.Context.Structure
  ( Element (..),
    variable,
    Info (..),
    unsolvedExistentials,
    Context (..),
    context0,
    CtxSegment,
    (|>),
    (<|),
    fmap',
    BadContext (..),
    validateSegment,
    SearchResult (..),
    focusProblem,
    culprit,
    info,
    filter,
    partition,
    apply,
    FT.fromList,
    mapMaybe,
    single,
    split,
    splitSeg,
    surround,
  )
where

import Data.FingerTree as FT hiding (split)
import Data.Foldable qualified as FO
import Data.Function (on)
import Data.List qualified as List
import Data.Map.Strict as Map hiding (filter, mapMaybe, partition, split)
import Data.Set as Set hiding (filter, partition, split)
import Data.Text qualified as Text
import Unison.ABT qualified as ABT
import Unison.Blank qualified as B
import Unison.PrettyPrintEnv qualified as PPE
import Unison.Syntax.TypePrinter qualified as TP
import Unison.Type qualified as Type
import Unison.Typechecker.TypeVar qualified as TypeVar
import Unison.Var (Var)
import Unison.Var qualified as Var
import Prelude hiding (filter)

type Monotype v loc = Type.Monotype (TypeVar v loc) loc

type TypeVar v loc = TypeVar.TypeVar (B.Blank loc) v

type Type v loc = Type.Type (TypeVar v loc) loc

-- | Elements of an ordered algorithmic context. A context is a sequence
-- of `Element`s (here represented as a finger tree), but not every
-- sequence represents a valid context. A context is only valid if every
-- type that occurs in the context is well scoped with regard to the
-- previous variable bindings in the context.
--
-- We will refer to invalid trees as 'context segments' since they can be
-- prefixed to become part of a valid context. Keeping track of the same
-- context information for _every_ segment is important to avoiding some
-- performance problems with a more naive implementation.
data Element v loc
  = -- | A variable declaration
    Var (TypeVar v loc)
  | -- | `v` is solved to some monotype
    Solved (B.Blank loc) v (Monotype v loc)
  | -- | `v` has type `a`, maybe quantified
    -- loc contains the span of the name of the bound 'v'
    Ann v loc (Type v loc)
  | -- | used for scoping
    Marker v

variable :: Element v loc -> v
variable :: forall v loc. Element v loc -> v
variable (Var TypeVar v loc
v) = TypeVar v loc -> v
forall b v. TypeVar b v -> v
TypeVar.underlying TypeVar v loc
v
variable (Solved Blank loc
_ v
v Monotype v loc
_) = v
v
variable (Ann v
v loc
_ Type v loc
_) = v
v
variable (Marker v
v) = v
v

instance (Var v) => Eq (Element v loc) where
  Var TypeVar v loc
v == :: Element v loc -> Element v loc -> Bool
== Var TypeVar v loc
v2 = TypeVar v loc
v TypeVar v loc -> TypeVar v loc -> Bool
forall a. Eq a => a -> a -> Bool
== TypeVar v loc
v2
  Solved Blank loc
_ v
v Monotype v loc
t == Solved Blank loc
_ v
v2 Monotype v loc
t2 = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2 Bool -> Bool -> Bool
&& Monotype v loc
t Monotype v loc -> Monotype v loc -> Bool
forall a. Eq a => a -> a -> Bool
== Monotype v loc
t2
  Ann v
v loc
_loc Type v loc
t == Ann v
v2 loc
_loc2 Type v loc
t2 = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2 Bool -> Bool -> Bool
&& Type v loc
t Type v loc -> Type v loc -> Bool
forall a. Eq a => a -> a -> Bool
== Type v loc
t2
  Marker v
v == Marker v
v2 = v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v2
  Element v loc
_ == Element v loc
_ = Bool
False

-- | Aggregate context (segment) information, built up from `Element`s.
--
-- `boundExistentialVars` is the set of existential variables that are
-- known to be 'in scope' due to the context segment.
--
-- `solvedExistentials` is a mapping of existential variables to their
-- solutions in the segment.
--
-- `boundUniversalVars` is the set of universal variables that are known
-- to be 'in scope' due to the context segment.
--
-- `termVarAnnotations` is a mapping of term variables to their type.
--
-- `allBoundVars` contains all the variables 'in scope' due to the
-- segment. Primarily used for freshening.
--
-- `freeUniversal/ExistentialVars` contains all the variables that occur
-- _free_ in types in the segment. This means that they are _not_ bound
-- in an `Element` previous to the one that the type occurs in.
--
-- `shadowedVars` contains variables that occur _multiple_ times in the
-- segment, and thus the latter shadows the former.
--
-- `recorded` tracks certain annotated elements.
--
-- A context segment is a well formed context if `free*Vars` and
-- `shadowedVars` are both empty.
--
-- Note: the fields here are intentionally lazy. In situations where
-- there is heavy context manipulation, this seems to actually be faster,
-- probably because the info is not actually used all of the time, and
-- any fields that are strict are actually demanded by use of every other
-- field in the info, regardless of whether the strict field ends up
-- needed.
data Info v loc = Info
  { forall v loc. Info v loc -> Set v
boundExistentialVars :: Set v,
    forall v loc. Info v loc -> Map v (Monotype v loc)
solvedExistentials :: Map v (Monotype v loc),
    forall v loc. Info v loc -> Set v
boundUniversalVars :: Set v,
    forall v loc. Info v loc -> Map v (loc, Type v loc)
termVarAnnotations :: Map v (loc, Type v loc),
    forall v loc. Info v loc -> Set v
allBoundVars :: Set v,
    forall v loc. Info v loc -> Set v
freeUniversalVars :: Set v,
    forall v loc. Info v loc -> Set v
freeExistentialVars :: Set v,
    forall v loc. Info v loc -> Set v
shadowedVars :: Set v,
    forall v loc. Info v loc -> Map v (Recorded loc, Type v loc)
recorded :: Map v (B.Recorded loc, Type v loc)
  }

type CtxSegment v loc = FingerTree (Info v loc) (Element v loc)

newtype Context v loc = Context (CtxSegment v loc)

-- | The empty context
context0 :: (Ord v) => Context v loc
context0 :: forall v loc. Ord v => Context v loc
context0 = CtxSegment v loc -> Context v loc
forall v loc. CtxSegment v loc -> Context v loc
Context CtxSegment v loc
forall v a. Measured v a => FingerTree v a
FT.empty

instance (Ord v) => Semigroup (Info v loc) where
  Info v loc
segl <> :: Info v loc -> Info v loc -> Info v loc
<> Info v loc
segr =
    Info
      { boundExistentialVars :: Set v
boundExistentialVars =
          (Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set v -> Set v -> Set v)
-> (Info v loc -> Set v) -> Info v loc -> Info v loc -> Set v
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Info v loc -> Set v
forall v loc. Info v loc -> Set v
boundExistentialVars) Info v loc
segl Info v loc
segr,
        boundUniversalVars :: Set v
boundUniversalVars =
          (Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set v -> Set v -> Set v)
-> (Info v loc -> Set v) -> Info v loc -> Info v loc -> Set v
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Info v loc -> Set v
forall v loc. Info v loc -> Set v
boundUniversalVars) Info v loc
segl Info v loc
segr,
        allBoundVars :: Set v
allBoundVars =
          (Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set v -> Set v -> Set v)
-> (Info v loc -> Set v) -> Info v loc -> Info v loc -> Set v
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Info v loc -> Set v
forall v loc. Info v loc -> Set v
allBoundVars) Info v loc
segl Info v loc
segr,
        -- Note: prefer solutions/annotations from the _right_
        solvedExistentials :: Map v (Monotype v loc)
solvedExistentials =
          (Map v (Monotype v loc)
-> Map v (Monotype v loc) -> Map v (Monotype v loc)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map v (Monotype v loc)
 -> Map v (Monotype v loc) -> Map v (Monotype v loc))
-> (Info v loc -> Map v (Monotype v loc))
-> Info v loc
-> Info v loc
-> Map v (Monotype v loc)
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Info v loc -> Map v (Monotype v loc)
forall v loc. Info v loc -> Map v (Monotype v loc)
solvedExistentials) Info v loc
segr Info v loc
segl,
        termVarAnnotations :: Map v (loc, Type v loc)
termVarAnnotations =
          (Map v (loc, Type v loc)
-> Map v (loc, Type v loc) -> Map v (loc, Type v loc)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map v (loc, Type v loc)
 -> Map v (loc, Type v loc) -> Map v (loc, Type v loc))
-> (Info v loc -> Map v (loc, Type v loc))
-> Info v loc
-> Info v loc
-> Map v (loc, Type v loc)
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Info v loc -> Map v (loc, Type v loc)
forall v loc. Info v loc -> Map v (loc, Type v loc)
termVarAnnotations) Info v loc
segr Info v loc
segl,
        $sel:freeExistentialVars:Info :: Set v
freeExistentialVars =
          Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union
            (Info v loc -> Set v
forall v loc. Info v loc -> Set v
freeExistentialVars Info v loc
segl)
            ( Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
                (Info v loc -> Set v
forall v loc. Info v loc -> Set v
freeExistentialVars Info v loc
segr)
                (Info v loc -> Set v
forall v loc. Info v loc -> Set v
boundExistentialVars Info v loc
segl)
            ),
        $sel:freeUniversalVars:Info :: Set v
freeUniversalVars =
          Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union
            (Info v loc -> Set v
forall v loc. Info v loc -> Set v
freeUniversalVars Info v loc
segl)
            ( Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
                (Info v loc -> Set v
forall v loc. Info v loc -> Set v
freeUniversalVars Info v loc
segr)
                (Info v loc -> Set v
forall v loc. Info v loc -> Set v
boundUniversalVars Info v loc
segl)
            ),
        shadowedVars :: Set v
shadowedVars =
          [Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions
            [ Info v loc -> Set v
forall v loc. Info v loc -> Set v
shadowedVars Info v loc
segl,
              Info v loc -> Set v
forall v loc. Info v loc -> Set v
shadowedVars Info v loc
segr,
              Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                (Info v loc -> Set v
forall v loc. Info v loc -> Set v
allBoundVars Info v loc
segl)
                (Info v loc -> Set v
forall v loc. Info v loc -> Set v
allBoundVars Info v loc
segr)
            ],
        recorded :: Map v (Recorded loc, Type v loc)
recorded = (Map v (Recorded loc, Type v loc)
-> Map v (Recorded loc, Type v loc)
-> Map v (Recorded loc, Type v loc)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (Map v (Recorded loc, Type v loc)
 -> Map v (Recorded loc, Type v loc)
 -> Map v (Recorded loc, Type v loc))
-> (Info v loc -> Map v (Recorded loc, Type v loc))
-> Info v loc
-> Info v loc
-> Map v (Recorded loc, Type v loc)
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Info v loc -> Map v (Recorded loc, Type v loc)
forall v loc. Info v loc -> Map v (Recorded loc, Type v loc)
recorded) Info v loc
segr Info v loc
segl
      }

emptyInfo :: Info v loc
emptyInfo :: forall v loc. Info v loc
emptyInfo =
  Info
    { boundExistentialVars :: Set v
boundExistentialVars = Set v
forall a. Set a
Set.empty,
      solvedExistentials :: Map v (Monotype v loc)
solvedExistentials = Map v (Monotype v loc)
forall k a. Map k a
Map.empty,
      boundUniversalVars :: Set v
boundUniversalVars = Set v
forall a. Set a
Set.empty,
      termVarAnnotations :: Map v (loc, Type v loc)
termVarAnnotations = Map v (loc, Type v loc)
forall k a. Map k a
Map.empty,
      allBoundVars :: Set v
allBoundVars = Set v
forall a. Set a
Set.empty,
      $sel:freeExistentialVars:Info :: Set v
freeExistentialVars = Set v
forall a. Set a
Set.empty,
      $sel:freeUniversalVars:Info :: Set v
freeUniversalVars = Set v
forall a. Set a
Set.empty,
      shadowedVars :: Set v
shadowedVars = Set v
forall a. Set a
Set.empty,
      recorded :: Map v (Recorded loc, Type v loc)
recorded = Map v (Recorded loc, Type v loc)
forall k a. Map k a
Map.empty
    }

-- | Gets the _unsolved_ existential variables of a context info.
unsolvedExistentials :: (Ord v) => Info v loc -> Set v
unsolvedExistentials :: forall v loc. Ord v => Info v loc -> Set v
unsolvedExistentials (Info {Map v (loc, Type v loc)
Map v (Recorded loc, Type v loc)
Map v (Monotype v loc)
Set v
boundExistentialVars :: forall v loc. Info v loc -> Set v
solvedExistentials :: forall v loc. Info v loc -> Map v (Monotype v loc)
boundUniversalVars :: forall v loc. Info v loc -> Set v
termVarAnnotations :: forall v loc. Info v loc -> Map v (loc, Type v loc)
allBoundVars :: forall v loc. Info v loc -> Set v
shadowedVars :: forall v loc. Info v loc -> Set v
recorded :: forall v loc. Info v loc -> Map v (Recorded loc, Type v loc)
$sel:freeUniversalVars:Info :: forall v loc. Info v loc -> Set v
$sel:freeExistentialVars:Info :: forall v loc. Info v loc -> Set v
boundExistentialVars :: Set v
solvedExistentials :: Map v (Monotype v loc)
boundUniversalVars :: Set v
termVarAnnotations :: Map v (loc, Type v loc)
allBoundVars :: Set v
freeUniversalVars :: Set v
freeExistentialVars :: Set v
shadowedVars :: Set v
recorded :: Map v (Recorded loc, Type v loc)
..}) =
  Set v
boundExistentialVars Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Map v (Monotype v loc) -> Set v
forall k a. Map k a -> Set k
Map.keysSet Map v (Monotype v loc)
solvedExistentials

instance (Ord v) => Monoid (Info v loc) where
  mempty :: Info v loc
mempty = Info v loc
forall v loc. Info v loc
emptyInfo

part :: Set (TypeVar v loc) -> ([v], [v])
part :: forall v loc. Set (TypeVar v loc) -> ([v], [v])
part = (([v], [v]) -> TypeVar (Blank loc) v -> ([v], [v]))
-> ([v], [v]) -> [TypeVar (Blank loc) v] -> ([v], [v])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' ([v], [v]) -> TypeVar (Blank loc) v -> ([v], [v])
forall {a} {b}. ([a], [a]) -> TypeVar b a -> ([a], [a])
classify ([], []) ([TypeVar (Blank loc) v] -> ([v], [v]))
-> (Set (TypeVar (Blank loc) v) -> [TypeVar (Blank loc) v])
-> Set (TypeVar (Blank loc) v)
-> ([v], [v])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (TypeVar (Blank loc) v) -> [TypeVar (Blank loc) v]
forall a. Set a -> [a]
Set.toDescList
  where
    classify :: ([a], [a]) -> TypeVar b a -> ([a], [a])
classify ([a]
es, [a]
us) (TypeVar.Existential b
_ a
e) = (a
e a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
es, [a]
us)
    classify ([a]
es, [a]
us) (TypeVar.Universal a
u) = ([a]
es, a
u a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
us)

instance (Ord v) => Measured (Info v loc) (Element v loc) where
  measure :: Element v loc -> Info v loc
measure (Var TypeVar v loc
tv)
    | TypeVar.Universal v
v <- TypeVar v loc
tv =
        Info v loc
forall v loc. Info v loc
emptyInfo
          { boundUniversalVars = Set.singleton v,
            allBoundVars = Set.singleton v
          }
    | TypeVar.Existential Blank loc
b v
v <- TypeVar v loc
tv =
        Info v loc
forall v loc. Info v loc
emptyInfo
          { boundExistentialVars = Set.singleton v,
            allBoundVars = Set.singleton v,
            recorded = case b of
              B.Recorded Recorded loc
b' ->
                v -> (Recorded loc, Type v loc) -> Map v (Recorded loc, Type v loc)
forall k a. k -> a -> Map k a
Map.singleton v
v (Recorded loc
b', Type v loc
ty)
                where
                  ty :: Type v loc
ty = loc -> TypeVar v loc -> Type v loc
forall a v (f :: * -> *). a -> v -> Term f v a
ABT.annotatedVar (Recorded loc -> loc
forall loc. Recorded loc -> loc
B.loc Recorded loc
b') TypeVar v loc
tv
              Blank loc
_ -> Map v (Recorded loc, Type v loc)
forall k a. Map k a
Map.empty
          }
  measure (Solved Blank loc
b v
v Monotype v loc
ty)
    | Type v loc
pty <- Monotype v loc -> Type v loc
forall v a. Monotype v a -> Type v a
Type.getPolytype Monotype v loc
ty,
      ([v]
evs, [v]
uvs) <- Set (TypeVar v loc) -> ([v], [v])
forall v loc. Set (TypeVar v loc) -> ([v], [v])
part (Set (TypeVar v loc) -> ([v], [v]))
-> Set (TypeVar v loc) -> ([v], [v])
forall a b. (a -> b) -> a -> b
$ Type v loc -> Set (TypeVar v loc)
forall v a. Type v a -> Set v
Type.freeVars Type v loc
pty =
        Info v loc
forall v loc. Info v loc
emptyInfo
          { boundExistentialVars = Set.singleton v,
            solvedExistentials = Map.singleton v ty,
            allBoundVars = Set.singleton v,
            freeExistentialVars = Set.fromList evs,
            freeUniversalVars = Set.fromList uvs,
            recorded = case b of
              B.Recorded Recorded loc
b' ->
                v -> (Recorded loc, Type v loc) -> Map v (Recorded loc, Type v loc)
forall k a. k -> a -> Map k a
Map.singleton v
v (Recorded loc
b', Type v loc
pty)
              Blank loc
_ -> Map v (Recorded loc, Type v loc)
forall k a. Map k a
Map.empty
          }
  measure (Ann v
v loc
loc Type v loc
ty)
    | ([v]
evs, [v]
uvs) <- Set (TypeVar v loc) -> ([v], [v])
forall v loc. Set (TypeVar v loc) -> ([v], [v])
part (Set (TypeVar v loc) -> ([v], [v]))
-> Set (TypeVar v loc) -> ([v], [v])
forall a b. (a -> b) -> a -> b
$ Type v loc -> Set (TypeVar v loc)
forall v a. Type v a -> Set v
Type.freeVars Type v loc
ty =
        Info v loc
forall v loc. Info v loc
emptyInfo
          { allBoundVars = Set.singleton v,
            termVarAnnotations = Map.singleton v (loc, ty),
            freeExistentialVars = Set.fromList evs,
            freeUniversalVars = Set.fromList uvs
          }
  measure (Marker v
v) = Info v loc
forall v loc. Info v loc
emptyInfo {allBoundVars = Set.singleton v}

instance (Ord v) => Measured (Info v loc) (Context v loc) where
  measure :: Context v loc -> Info v loc
measure (Context CtxSegment v loc
c) = CtxSegment v loc -> Info v loc
forall v a. Measured v a => a -> v
measure CtxSegment v loc
c

data BadContext
  = Shadowing
  | UnboundEx
  | UnboundUn

-- | Checks that a context segment forms a valid context. If so, then the
-- proper context is yielded. Otherwise an indication of what is wrong
-- with the segment is returned.
validateSegment ::
  (Ord v) => CtxSegment v loc -> Either BadContext (Context v loc)
validateSegment :: forall v loc.
Ord v =>
CtxSegment v loc -> Either BadContext (Context v loc)
validateSegment CtxSegment v loc
seg
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set v -> Bool
forall a. Set a -> Bool
Set.null Set v
shadowedVars = BadContext -> Either BadContext (Context v loc)
forall a b. a -> Either a b
Left BadContext
Shadowing
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set v -> Bool
forall a. Set a -> Bool
Set.null Set v
freeExistentialVars = BadContext -> Either BadContext (Context v loc)
forall a b. a -> Either a b
Left BadContext
UnboundEx
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set v -> Bool
forall a. Set a -> Bool
Set.null Set v
freeUniversalVars = BadContext -> Either BadContext (Context v loc)
forall a b. a -> Either a b
Left BadContext
UnboundUn
  | Bool
otherwise = Context v loc -> Either BadContext (Context v loc)
forall a b. b -> Either a b
Right (Context v loc -> Either BadContext (Context v loc))
-> Context v loc -> Either BadContext (Context v loc)
forall a b. (a -> b) -> a -> b
$ CtxSegment v loc -> Context v loc
forall v loc. CtxSegment v loc -> Context v loc
Context CtxSegment v loc
seg
  where
    Info {Map v (loc, Type v loc)
Map v (Recorded loc, Type v loc)
Map v (Monotype v loc)
Set v
boundExistentialVars :: forall v loc. Info v loc -> Set v
solvedExistentials :: forall v loc. Info v loc -> Map v (Monotype v loc)
boundUniversalVars :: forall v loc. Info v loc -> Set v
termVarAnnotations :: forall v loc. Info v loc -> Map v (loc, Type v loc)
allBoundVars :: forall v loc. Info v loc -> Set v
shadowedVars :: forall v loc. Info v loc -> Set v
recorded :: forall v loc. Info v loc -> Map v (Recorded loc, Type v loc)
$sel:freeUniversalVars:Info :: forall v loc. Info v loc -> Set v
$sel:freeExistentialVars:Info :: forall v loc. Info v loc -> Set v
shadowedVars :: Set v
freeExistentialVars :: Set v
freeUniversalVars :: Set v
boundExistentialVars :: Set v
solvedExistentials :: Map v (Monotype v loc)
boundUniversalVars :: Set v
termVarAnnotations :: Map v (loc, Type v loc)
allBoundVars :: Set v
recorded :: Map v (Recorded loc, Type v loc)
..} = CtxSegment v loc -> Info v loc
forall v a. Measured v a => a -> v
measure CtxSegment v loc
seg

-- Given a predicate on measures that is monotone, searches for a point
-- in the sequence at which the predicate first becomes true.
focusProblem ::
  (Measured v e) =>
  (v -> Bool) ->
  FingerTree v e ->
  SearchResult v e
focusProblem :: forall v e.
Measured v e =>
(v -> Bool) -> FingerTree v e -> SearchResult v e
focusProblem v -> Bool
p = (v -> v -> Bool) -> FingerTree v e -> SearchResult v e
forall v a.
Measured v a =>
(v -> v -> Bool) -> FingerTree v a -> SearchResult v a
search v -> v -> Bool
q
  where
    q :: v -> v -> Bool
q v
l v
_ = v -> Bool
p v
l

-- Searches for the first point at which an extracted set becomes
-- non-null.
findFirst ::
  (Measured v e) =>
  (v -> Set a) ->
  FingerTree v e ->
  SearchResult v e
findFirst :: forall v e a.
Measured v e =>
(v -> Set a) -> FingerTree v e -> SearchResult v e
findFirst v -> Set a
ex = (v -> Bool) -> FingerTree v e -> SearchResult v e
forall v e.
Measured v e =>
(v -> Bool) -> FingerTree v e -> SearchResult v e
focusProblem (Bool -> Bool
not (Bool -> Bool) -> (v -> Bool) -> v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> Bool
forall a. Set a -> Bool
Set.null (Set a -> Bool) -> (v -> Set a) -> v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Set a
ex)

-- Given a malformed context and a validation error, finds an element
-- that induces the error, and the preceding context.
culprit ::
  (Ord v) =>
  CtxSegment v loc ->
  BadContext ->
  (CtxSegment v loc, Element v loc)
culprit :: forall v loc.
Ord v =>
CtxSegment v loc -> BadContext -> (CtxSegment v loc, Element v loc)
culprit CtxSegment v loc
whole BadContext
err
  | Position CtxSegment v loc
pre Element v loc
e CtxSegment v loc
_ <- CtxSegment v loc -> SearchResult (Info v loc) (Element v loc)
srch CtxSegment v loc
whole = (CtxSegment v loc
pre, Element v loc
e)
  | Bool
otherwise = [Char] -> (CtxSegment v loc, Element v loc)
forall a. HasCallStack => [Char] -> a
error [Char]
"Context.Structure.culprit: impossible"
  where
    srch :: CtxSegment v loc -> SearchResult (Info v loc) (Element v loc)
srch = case BadContext
err of
      BadContext
Shadowing -> (Info v loc -> Set v)
-> CtxSegment v loc -> SearchResult (Info v loc) (Element v loc)
forall v e a.
Measured v e =>
(v -> Set a) -> FingerTree v e -> SearchResult v e
findFirst Info v loc -> Set v
forall v loc. Info v loc -> Set v
shadowedVars
      BadContext
UnboundEx -> (Info v loc -> Set v)
-> CtxSegment v loc -> SearchResult (Info v loc) (Element v loc)
forall v e a.
Measured v e =>
(v -> Set a) -> FingerTree v e -> SearchResult v e
findFirst Info v loc -> Set v
forall v loc. Info v loc -> Set v
freeExistentialVars
      BadContext
UnboundUn -> (Info v loc -> Set v)
-> CtxSegment v loc -> SearchResult (Info v loc) (Element v loc)
forall v e a.
Measured v e =>
(v -> Set a) -> FingerTree v e -> SearchResult v e
findFirst Info v loc -> Set v
forall v loc. Info v loc -> Set v
freeUniversalVars

-- | Return the aggregate `Info` associated to the context.
info :: (Ord v, Measured (Info v loc) c) => c -> Info v loc
info :: forall v loc c. (Ord v, Measured (Info v loc) c) => c -> Info v loc
info = c -> Info v loc
forall v a. Measured v a => a -> v
measure

-- | Replace any existentials with their solution in the context
apply ::
  (Var v, Measured (Info v loc) c) =>
  c ->
  Type v loc ->
  Type v loc
apply :: forall v loc c.
(Var v, Measured (Info v loc) c) =>
c -> Type v loc -> Type v loc
apply c
ctx = Map v (Monotype v loc) -> Type v loc -> Type v loc
forall v loc.
Var v =>
Map v (Monotype v loc) -> Type v loc -> Type v loc
apply' (Info v loc -> Map v (Monotype v loc)
forall v loc. Info v loc -> Map v (Monotype v loc)
solvedExistentials (Info v loc -> Map v (Monotype v loc))
-> (c -> Info v loc) -> c -> Map v (Monotype v loc)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> Info v loc
forall v a. Measured v a => a -> v
measure (c -> Map v (Monotype v loc)) -> c -> Map v (Monotype v loc)
forall a b. (a -> b) -> a -> b
$ c
ctx)

apply' ::
  (Var v) => Map v (Monotype v loc) -> Type v loc -> Type v loc
apply' :: forall v loc.
Var v =>
Map v (Monotype v loc) -> Type v loc -> Type v loc
apply' Map v (Monotype v loc)
_ Term F (TypeVar (Blank loc) v) loc
t | Set (TypeVar (Blank loc) v) -> Bool
forall a. Set a -> Bool
Set.null (Term F (TypeVar (Blank loc) v) loc -> Set (TypeVar (Blank loc) v)
forall v a. Type v a -> Set v
Type.freeVars Term F (TypeVar (Blank loc) v) loc
t) = Term F (TypeVar (Blank loc) v) loc
t
apply' Map v (Monotype v loc)
solved Term F (TypeVar (Blank loc) v) loc
t = Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
t
  where
    go :: Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
t = case Term F (TypeVar (Blank loc) v) loc
t of
      Type.Var' (TypeVar.Universal v
_) -> Term F (TypeVar (Blank loc) v) loc
t
      Type.Ref' TypeReference
_ -> Term F (TypeVar (Blank loc) v) loc
t
      Type.Var' (TypeVar.Existential Blank loc
_ v
v) ->
        Term F (TypeVar (Blank loc) v) loc
-> (Monotype v loc -> Term F (TypeVar (Blank loc) v) loc)
-> Maybe (Monotype v loc)
-> Term F (TypeVar (Blank loc) v) loc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Term F (TypeVar (Blank loc) v) loc
t (\(Type.Monotype Term F (TypeVar (Blank loc) v) loc
t') -> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
t') (v -> Map v (Monotype v loc) -> Maybe (Monotype v loc)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v (Monotype v loc)
solved)
      Type.Arrow' Term F (TypeVar (Blank loc) v) loc
i Term F (TypeVar (Blank loc) v) loc
o -> loc
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.arrow loc
a (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
i) (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
o)
      Type.App' Term F (TypeVar (Blank loc) v) loc
x Term F (TypeVar (Blank loc) v) loc
y -> loc
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.app loc
a (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
x) (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
y)
      Type.Ann' Term F (TypeVar (Blank loc) v) loc
v Kind
k -> loc
-> Term F (TypeVar (Blank loc) v) loc
-> Kind
-> Term F (TypeVar (Blank loc) v) loc
forall v a. Ord v => a -> Type v a -> Kind -> Type v a
Type.ann loc
a (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
v) Kind
k
      Type.Effect1' Term F (TypeVar (Blank loc) v) loc
e Term F (TypeVar (Blank loc) v) loc
t -> loc
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
forall v a. Ord v => a -> Type v a -> Type v a -> Type v a
Type.effect1 loc
a (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
e) (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
t)
      Type.Effects' [Term F (TypeVar (Blank loc) v) loc]
es -> loc
-> [Term F (TypeVar (Blank loc) v) loc]
-> Term F (TypeVar (Blank loc) v) loc
forall v a. Ord v => a -> [Type v a] -> Type v a
Type.effects loc
a ((Term F (TypeVar (Blank loc) v) loc
 -> Term F (TypeVar (Blank loc) v) loc)
-> [Term F (TypeVar (Blank loc) v) loc]
-> [Term F (TypeVar (Blank loc) v) loc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go [Term F (TypeVar (Blank loc) v) loc]
es)
      Type.ForallNamed' TypeVar (Blank loc) v
v Term F (TypeVar (Blank loc) v) loc
t' -> loc
-> TypeVar (Blank loc) v
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
forall v a. Ord v => a -> v -> Type v a -> Type v a
Type.forAll loc
a TypeVar (Blank loc) v
v (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
t')
      Type.IntroOuterNamed' TypeVar (Blank loc) v
v Term F (TypeVar (Blank loc) v) loc
t' -> loc
-> TypeVar (Blank loc) v
-> Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
forall v a. Ord v => a -> v -> Type v a -> Type v a
Type.introOuter loc
a TypeVar (Blank loc) v
v (Term F (TypeVar (Blank loc) v) loc
-> Term F (TypeVar (Blank loc) v) loc
go Term F (TypeVar (Blank loc) v) loc
t')
      Term F (TypeVar (Blank loc) v) loc
_ -> [Char] -> Term F (TypeVar (Blank loc) v) loc
forall a. HasCallStack => [Char] -> a
error ([Char] -> Term F (TypeVar (Blank loc) v) loc)
-> [Char] -> Term F (TypeVar (Blank loc) v) loc
forall a b. (a -> b) -> a -> b
$ [Char]
"Match error in Context.apply': " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term F (TypeVar (Blank loc) v) loc -> [Char]
forall a. Show a => a -> [Char]
show Term F (TypeVar (Blank loc) v) loc
t
      where
        a :: loc
a = Term F (TypeVar (Blank loc) v) loc -> loc
forall (f :: * -> *) v a. Term f v a -> a
ABT.annotation Term F (TypeVar (Blank loc) v) loc
t

-- Splits a context segment at an `Element` binding the given variable.
-- In a general context segment, variable bindings needn't be unique, so
-- this finds the right-most such occurrence, which would be the most
-- locally relevant occurrence.
--
-- Technically the context can contain both type and term variable
-- bindings, and these are not distinguished, so take care.
splitSeg ::
  (Ord v) =>
  v ->
  CtxSegment v loc ->
  Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
splitSeg :: forall v loc.
Ord v =>
v
-> CtxSegment v loc
-> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
splitSeg v
tgt CtxSegment v loc
seg = case (Info v loc -> Info v loc -> Bool)
-> CtxSegment v loc -> SearchResult (Info v loc) (Element v loc)
forall v a.
Measured v a =>
(v -> v -> Bool) -> FingerTree v a -> SearchResult v a
search Info v loc -> Info v loc -> Bool
p CtxSegment v loc
seg of
  Position CtxSegment v loc
l Element v loc
e CtxSegment v loc
r -> (CtxSegment v loc, Element v loc, CtxSegment v loc)
-> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
forall a. a -> Maybe a
Just (CtxSegment v loc
l, Element v loc
e, CtxSegment v loc
r)
  SearchResult (Info v loc) (Element v loc)
_ -> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
forall a. Maybe a
Nothing
  where
    -- Given info for a partition | i | j | of the context, tests whether
    -- `tgt` is bound in `i` and not in `j`. This means | i | ends with
    -- the last binding of `tgt`.
    p :: Info v loc -> Info v loc -> Bool
p Info v loc
i Info v loc
j =
      (v
tgt v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Info v loc -> Set v
forall v loc. Info v loc -> Set v
allBoundVars Info v loc
j)
        Bool -> Bool -> Bool
&& (v
tgt v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Info v loc -> Set v
forall v loc. Info v loc -> Set v
allBoundVars Info v loc
i)

-- Splits a context at an `Element` binding the given variable. Since in
-- a valid context, a variable only occurs once, this is completely
-- unambiguous.
split ::
  (Ord v) =>
  v ->
  Context v loc ->
  Maybe (Context v loc, Element v loc, CtxSegment v loc)
split :: forall v loc.
Ord v =>
v
-> Context v loc
-> Maybe (Context v loc, Element v loc, CtxSegment v loc)
split v
tgt (Context CtxSegment v loc
seg) = (CtxSegment v loc, Element v loc, CtxSegment v loc)
-> (Context v loc, Element v loc, CtxSegment v loc)
forall {v} {loc} {b} {c}.
(CtxSegment v loc, b, c) -> (Context v loc, b, c)
g ((CtxSegment v loc, Element v loc, CtxSegment v loc)
 -> (Context v loc, Element v loc, CtxSegment v loc))
-> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
-> Maybe (Context v loc, Element v loc, CtxSegment v loc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v
-> CtxSegment v loc
-> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
forall v loc.
Ord v =>
v
-> CtxSegment v loc
-> Maybe (CtxSegment v loc, Element v loc, CtxSegment v loc)
splitSeg v
tgt CtxSegment v loc
seg
  where
    -- Note: every prefix of a valid context is valid.
    g :: (CtxSegment v loc, b, c) -> (Context v loc, b, c)
g (CtxSegment v loc
l, b
e, c
r) = (CtxSegment v loc -> Context v loc
forall v loc. CtxSegment v loc -> Context v loc
Context CtxSegment v loc
l, b
e, c
r)

surround ::
  (Ord v) =>
  CtxSegment v loc ->
  Element v loc ->
  CtxSegment v loc ->
  CtxSegment v loc
surround :: forall v loc.
Ord v =>
CtxSegment v loc
-> Element v loc -> CtxSegment v loc -> CtxSegment v loc
surround CtxSegment v loc
l Element v loc
e CtxSegment v loc
r = CtxSegment v loc
l CtxSegment v loc -> CtxSegment v loc -> CtxSegment v loc
forall v a.
Measured v a =>
FingerTree v a -> FingerTree v a -> FingerTree v a
>< Element v loc
e Element v loc -> CtxSegment v loc -> CtxSegment v loc
forall v a. Measured v a => a -> FingerTree v a -> FingerTree v a
<| CtxSegment v loc
r

filter ::
  (Var v) =>
  (Element v loc -> Bool) ->
  CtxSegment v loc ->
  CtxSegment v loc
filter :: forall v loc.
Var v =>
(Element v loc -> Bool) -> CtxSegment v loc -> CtxSegment v loc
filter Element v loc -> Bool
p = (CtxSegment v loc -> Element v loc -> CtxSegment v loc)
-> CtxSegment v loc -> CtxSegment v loc -> CtxSegment v loc
forall b a. (b -> a -> b) -> b -> FingerTree (Info v loc) a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
FO.foldl' CtxSegment v loc -> Element v loc -> CtxSegment v loc
c CtxSegment v loc
forall a. Monoid a => a
mempty
  where
    c :: CtxSegment v loc -> Element v loc -> CtxSegment v loc
c CtxSegment v loc
seg Element v loc
e
      | Element v loc -> Bool
p Element v loc
e = CtxSegment v loc
seg CtxSegment v loc -> Element v loc -> CtxSegment v loc
forall v a. Measured v a => FingerTree v a -> a -> FingerTree v a
|> Element v loc
e
      | Bool
otherwise = CtxSegment v loc
seg

partition ::
  (Var v) =>
  (Element v loc -> Either (Element v loc) (Element v loc)) ->
  CtxSegment v loc ->
  (CtxSegment v loc, CtxSegment v loc)
partition :: forall v loc.
Var v =>
(Element v loc -> Either (Element v loc) (Element v loc))
-> CtxSegment v loc -> (CtxSegment v loc, CtxSegment v loc)
partition Element v loc -> Either (Element v loc) (Element v loc)
f = ((CtxSegment v loc, CtxSegment v loc)
 -> Element v loc -> (CtxSegment v loc, CtxSegment v loc))
-> (CtxSegment v loc, CtxSegment v loc)
-> CtxSegment v loc
-> (CtxSegment v loc, CtxSegment v loc)
forall b a. (b -> a -> b) -> b -> FingerTree (Info v loc) a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
FO.foldl' (CtxSegment v loc, CtxSegment v loc)
-> Element v loc -> (CtxSegment v loc, CtxSegment v loc)
g (CtxSegment v loc
forall a. Monoid a => a
mempty, CtxSegment v loc
forall a. Monoid a => a
mempty)
  where
    g :: (CtxSegment v loc, CtxSegment v loc)
-> Element v loc -> (CtxSegment v loc, CtxSegment v loc)
g (CtxSegment v loc
ls, CtxSegment v loc
rs) Element v loc
e = case Element v loc -> Either (Element v loc) (Element v loc)
f Element v loc
e of
      Left Element v loc
l -> (CtxSegment v loc
ls CtxSegment v loc -> Element v loc -> CtxSegment v loc
forall v a. Measured v a => FingerTree v a -> a -> FingerTree v a
|> Element v loc
l, CtxSegment v loc
rs)
      Right Element v loc
r -> (CtxSegment v loc
ls, CtxSegment v loc
rs CtxSegment v loc -> Element v loc -> CtxSegment v loc
forall v a. Measured v a => FingerTree v a -> a -> FingerTree v a
|> Element v loc
r)

-- | Applies a partial mapping to a context segment, resulting in a list.
mapMaybe :: (Element v loc -> Maybe b) -> CtxSegment v loc -> [b]
mapMaybe :: forall v loc b.
(Element v loc -> Maybe b) -> CtxSegment v loc -> [b]
mapMaybe Element v loc -> Maybe b
f = (Element v loc -> [b] -> [b])
-> [b] -> FingerTree (Info v loc) (Element v loc) -> [b]
forall a b. (a -> b -> b) -> b -> FingerTree (Info v loc) a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Prelude.foldr Element v loc -> [b] -> [b]
c []
  where
    c :: Element v loc -> [b] -> [b]
c Element v loc
e = ([b] -> [b]) -> (b -> [b] -> [b]) -> Maybe b -> [b] -> [b]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [b] -> [b]
forall a. a -> a
id (:) (Maybe b -> [b] -> [b]) -> Maybe b -> [b] -> [b]
forall a b. (a -> b) -> a -> b
$ Element v loc -> Maybe b
f Element v loc
e

single :: (Var v) => Element v loc -> CtxSegment v loc
single :: forall v loc. Var v => Element v loc -> CtxSegment v loc
single Element v loc
e = Element v loc -> FingerTree (Info v loc) (Element v loc)
forall v a. Measured v a => a -> FingerTree v a
FT.singleton Element v loc
e

instance (Var v) => Show (Element v loc) where
  show :: Element v loc -> [Char]
show (Var TypeVar v loc
v) = case TypeVar v loc
v of
    TypeVar.Universal v
x -> [Char]
"@" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> v -> [Char]
forall a. Show a => a -> [Char]
show v
x
    TypeVar v loc
e -> TypeVar v loc -> [Char]
forall a. Show a => a -> [Char]
show TypeVar v loc
e
  show (Solved Blank loc
_ v
v Monotype v loc
t) = [Char]
"'" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack (v -> Text
forall v. Var v => v -> Text
Var.name v
v) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack (Width -> PrettyPrintEnv -> Type (TypeVar v loc) loc -> Text
forall v a. Var v => Width -> PrettyPrintEnv -> Type v a -> Text
TP.prettyStr Width
0 PrettyPrintEnv
PPE.empty (Monotype v loc -> Type (TypeVar v loc) loc
forall v a. Monotype v a -> Type v a
Type.getPolytype Monotype v loc
t))
  show (Ann v
v loc
_loc Type (TypeVar v loc) loc
t) =
    Text -> [Char]
Text.unpack (v -> Text
forall v. Var v => v -> Text
Var.name v
v)
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : "
      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack (Width -> PrettyPrintEnv -> Type (TypeVar v loc) loc -> Text
forall v a. Var v => Width -> PrettyPrintEnv -> Type v a -> Text
TP.prettyStr Width
0 PrettyPrintEnv
PPE.empty Type (TypeVar v loc) loc
t)
  show (Marker v
v) = [Char]
"|" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Text -> [Char]
Text.unpack (v -> Text
forall v. Var v => v -> Text
Var.name v
v) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"|"

toReverseList :: CtxSegment v loc -> [Element v loc]
toReverseList :: forall v loc. CtxSegment v loc -> [Element v loc]
toReverseList = ([Element v loc] -> Element v loc -> [Element v loc])
-> [Element v loc]
-> FingerTree (Info v loc) (Element v loc)
-> [Element v loc]
forall b a. (b -> a -> b) -> b -> FingerTree (Info v loc) a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Prelude.foldl ((Element v loc -> [Element v loc] -> [Element v loc])
-> [Element v loc] -> Element v loc -> [Element v loc]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (:)) []

renderType :: (Ord loc, Var v) => Context v loc -> Type v loc -> String
renderType :: forall loc v.
(Ord loc, Var v) =>
Context v loc -> Type v loc -> [Char]
renderType Context v loc
ctx Type v loc
ty = Text -> [Char]
Text.unpack (Text -> [Char]) -> (Type v loc -> Text) -> Type v loc -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Width -> PrettyPrintEnv -> Type v loc -> Text
forall v a. Var v => Width -> PrettyPrintEnv -> Type v a -> Text
TP.prettyStr Width
0 PrettyPrintEnv
PPE.empty (Type v loc -> [Char]) -> Type v loc -> [Char]
forall a b. (a -> b) -> a -> b
$ Context v loc -> Type v loc -> Type v loc
forall v loc c.
(Var v, Measured (Info v loc) c) =>
c -> Type v loc -> Type v loc
apply Context v loc
ctx Type v loc
ty

renderElement ::
  (Ord loc, Var v) => Context v loc -> Element v loc -> String
renderElement :: forall loc v.
(Ord loc, Var v) =>
Context v loc -> Element v loc -> [Char]
renderElement Context v loc
ctx = \case
  Var TypeVar v loc
v
    | TypeVar.Universal v
x <- TypeVar v loc
v -> [Char]
"@" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> v -> [Char]
forall a. Show a => a -> [Char]
show v
x
    | Bool
otherwise -> TypeVar v loc -> [Char]
forall a. Show a => a -> [Char]
show TypeVar v loc
v
  Solved Blank loc
_ v
v (Type.Monotype Type (TypeVar v loc) loc
t) ->
    [[Char]] -> [Char]
forall a. Monoid a => [a] -> a
mconcat
      [ [Char]
"'",
        Text -> [Char]
Text.unpack (Text -> [Char]) -> Text -> [Char]
forall a b. (a -> b) -> a -> b
$ v -> Text
forall v. Var v => v -> Text
Var.name v
v,
        [Char]
" = ",
        Context v loc -> Type (TypeVar v loc) loc -> [Char]
forall loc v.
(Ord loc, Var v) =>
Context v loc -> Type v loc -> [Char]
renderType Context v loc
ctx Type (TypeVar v loc) loc
t
      ]
  Ann v
v loc
_loc Type (TypeVar v loc) loc
t ->
    [[Char]] -> [Char]
forall a. Monoid a => [a] -> a
mconcat
      [ Text -> [Char]
Text.unpack (Text -> [Char]) -> Text -> [Char]
forall a b. (a -> b) -> a -> b
$ v -> Text
forall v. Var v => v -> Text
Var.name v
v,
        [Char]
" : ",
        Context v loc -> Type (TypeVar v loc) loc -> [Char]
forall loc v.
(Ord loc, Var v) =>
Context v loc -> Type v loc -> [Char]
renderType Context v loc
ctx Type (TypeVar v loc) loc
t
      ]
  Marker v
v -> [Char]
"|" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Text -> [Char]
Text.unpack (v -> Text
forall v. Var v => v -> Text
Var.name v
v) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"|"

renderElements ::
  (Ord loc, Var v) => Context v loc -> [Element v loc] -> String
renderElements :: forall loc v.
(Ord loc, Var v) =>
Context v loc -> [Element v loc] -> [Char]
renderElements Context v loc
ctx = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n  " ([[Char]] -> [Char])
-> ([Element v loc] -> [[Char]]) -> [Element v loc] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Element v loc -> [Char]) -> [Element v loc] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Context v loc -> Element v loc -> [Char]
forall loc v.
(Ord loc, Var v) =>
Context v loc -> Element v loc -> [Char]
renderElement Context v loc
ctx)

instance (Ord loc, Var v) => Show (Context v loc) where
  show :: Context v loc -> [Char]
show ctx :: Context v loc
ctx@(Context CtxSegment v loc
es) =
    [Char]
"Γ\n  " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Context v loc -> [Element v loc] -> [Char]
forall loc v.
(Ord loc, Var v) =>
Context v loc -> [Element v loc] -> [Char]
renderElements Context v loc
ctx (CtxSegment v loc -> [Element v loc]
forall v loc. CtxSegment v loc -> [Element v loc]
toReverseList CtxSegment v loc
es)