module Wingman.Judgements where

import           Control.Arrow
import           Control.Lens hiding (Context)
import           Data.Bool
import           Data.Char
import           Data.Coerce
import           Data.Generics.Product (field)
import           Data.Map (Map)
import qualified Data.Map as M
import           Data.Maybe
import           Data.Set (Set)
import qualified Data.Set as S
import           Development.IDE.Core.UseStale (Tracked, unTrack)
import           Development.IDE.GHC.Compat hiding (isTopLevel)
import           Development.IDE.Spans.LocalBindings
import           Wingman.GHC (algebraicTyCon, normalizeType)
import           Wingman.Judgements.Theta
import           Wingman.Types


------------------------------------------------------------------------------
-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType
hypothesisFromBindings :: Tracked age RealSrcSpan -> Tracked age Bindings -> Hypothesis CType
hypothesisFromBindings (Tracked age RealSrcSpan -> RealSrcSpan
forall (age :: Age) a. Tracked age a -> a
unTrack -> RealSrcSpan
span) (Tracked age Bindings -> Bindings
forall (age :: Age) a. Tracked age a -> a
unTrack -> Bindings
bs) = [(Name, Maybe Type)] -> Hypothesis CType
buildHypothesis ([(Name, Maybe Type)] -> Hypothesis CType)
-> [(Name, Maybe Type)] -> Hypothesis CType
forall a b. (a -> b) -> a -> b
$ Bindings -> RealSrcSpan -> [(Name, Maybe Type)]
getLocalScope Bindings
bs RealSrcSpan
span


------------------------------------------------------------------------------
-- | Convert a @Set Id@ into a hypothesis.
buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType
buildHypothesis :: [(Name, Maybe Type)] -> Hypothesis CType
buildHypothesis
  = [HyInfo CType] -> Hypothesis CType
forall a. [HyInfo a] -> Hypothesis a
Hypothesis
  ([HyInfo CType] -> Hypothesis CType)
-> ([(Name, Maybe Type)] -> [HyInfo CType])
-> [(Name, Maybe Type)]
-> Hypothesis CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Maybe Type) -> Maybe (HyInfo CType))
-> [(Name, Maybe Type)] -> [HyInfo CType]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name, Maybe Type) -> Maybe (HyInfo CType)
forall name.
HasOccName name =>
(name, Maybe Type) -> Maybe (HyInfo CType)
go
  where
    go :: (name, Maybe Type) -> Maybe (HyInfo CType)
go (name -> OccName
forall name. HasOccName name => name -> OccName
occName -> OccName
occ, Maybe Type
t)
      | Just Type
ty <- Maybe Type
t
      , (Char
h:[Char]
_) <- OccName -> [Char]
occNameString OccName
occ
      , Char -> Bool
isAlpha Char
h = HyInfo CType -> Maybe (HyInfo CType)
forall a. a -> Maybe a
Just (HyInfo CType -> Maybe (HyInfo CType))
-> HyInfo CType -> Maybe (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> CType -> HyInfo CType
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
occ Provenance
UserPrv (CType -> HyInfo CType) -> CType -> HyInfo CType
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType Type
ty
      | Bool
otherwise = Maybe (HyInfo CType)
forall a. Maybe a
Nothing


------------------------------------------------------------------------------
-- | Build a trivial hypothesis containing only a single name. The corresponding
-- HyInfo has no provenance or type.
hySingleton :: OccName -> Hypothesis ()
hySingleton :: OccName -> Hypothesis ()
hySingleton OccName
n = [HyInfo ()] -> Hypothesis ()
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo ()] -> Hypothesis ())
-> (HyInfo () -> [HyInfo ()]) -> HyInfo () -> Hypothesis ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo () -> [HyInfo ()]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HyInfo () -> Hypothesis ()) -> HyInfo () -> Hypothesis ()
forall a b. (a -> b) -> a -> b
$ OccName -> Provenance -> () -> HyInfo ()
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
n Provenance
UserPrv ()


blacklistingDestruct :: Judgement -> Judgement
blacklistingDestruct :: Judgement -> Judgement
blacklistingDestruct =
  forall s t a b.
HasField "_jBlacklistDestruct" s t a b =>
Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"_jBlacklistDestruct" ((Bool -> Identity Bool) -> Judgement -> Identity Judgement)
-> Bool -> Judgement -> Judgement
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Bool
True


unwhitelistingSplit :: Judgement -> Judgement
unwhitelistingSplit :: Judgement -> Judgement
unwhitelistingSplit =
  forall s t a b. HasField "_jWhitelistSplit" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"_jWhitelistSplit" ((Bool -> Identity Bool) -> Judgement -> Identity Judgement)
-> Bool -> Judgement -> Judgement
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Bool
False


isDestructBlacklisted :: Judgement -> Bool
isDestructBlacklisted :: Judgement -> Bool
isDestructBlacklisted = Judgement -> Bool
forall a. Judgement' a -> Bool
_jBlacklistDestruct


isSplitWhitelisted :: Judgement -> Bool
isSplitWhitelisted :: Judgement -> Bool
isSplitWhitelisted = Judgement -> Bool
forall a. Judgement' a -> Bool
_jWhitelistSplit


withNewGoal :: a -> Judgement' a -> Judgement' a
withNewGoal :: a -> Judgement' a -> Judgement' a
withNewGoal a
t = forall s t a b. HasField "_jGoal" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"_jGoal" ((a -> Identity a) -> Judgement' a -> Identity (Judgement' a))
-> a -> Judgement' a -> Judgement' a
forall s t a b. ASetter s t a b -> b -> s -> t
.~ a
t

------------------------------------------------------------------------------
-- | Like 'withNewGoal' but allows you to modify the goal rather than replacing
-- it.
withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a
withModifiedGoal :: (a -> a) -> Judgement' a -> Judgement' a
withModifiedGoal a -> a
f = forall s t a b. HasField "_jGoal" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"_jGoal" ((a -> Identity a) -> Judgement' a -> Identity (Judgement' a))
-> (a -> a) -> Judgement' a -> Judgement' a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ a -> a
f


------------------------------------------------------------------------------
-- | Add some new type equalities to the local judgement.
withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement
withNewCoercions :: [(CType, CType)] -> Judgement -> Judgement
withNewCoercions [(CType, CType)]
ev Judgement
j =
  let subst :: TCvSubst
subst = Set TyVar -> [(Type, Type)] -> TCvSubst
allEvidenceToSubst Set TyVar
forall a. Monoid a => a
mempty ([(Type, Type)] -> TCvSubst) -> [(Type, Type)] -> TCvSubst
forall a b. (a -> b) -> a -> b
$ [(CType, CType)] -> [(Type, Type)]
coerce [(CType, CType)]
ev
   in (CType -> CType) -> Judgement -> Judgement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> CType
CType (Type -> CType) -> (CType -> Type) -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCvSubst -> Type -> Type
substTyAddInScope TCvSubst
subst (Type -> Type) -> (CType -> Type) -> CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType) Judgement
j
      Judgement -> (Judgement -> Judgement) -> Judgement
forall a b. a -> (a -> b) -> b
& forall s t a b. HasField "j_coercion" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"j_coercion" ((TCvSubst -> Identity TCvSubst)
 -> Judgement -> Identity Judgement)
-> (TCvSubst -> TCvSubst) -> Judgement -> Judgement
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ TCvSubst -> TCvSubst -> TCvSubst
unionTCvSubst TCvSubst
subst


normalizeHypothesis :: Functor f => Context -> f CType -> f CType
normalizeHypothesis :: Context -> f CType -> f CType
normalizeHypothesis = (CType -> CType) -> f CType -> f CType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((CType -> CType) -> f CType -> f CType)
-> (Context -> CType -> CType) -> Context -> f CType -> f CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Type) -> CType -> CType
coerce ((Type -> Type) -> CType -> CType)
-> (Context -> Type -> Type) -> Context -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> Type -> Type
normalizeType

normalizeJudgement :: Functor f => Context -> f CType -> f CType
normalizeJudgement :: Context -> f CType -> f CType
normalizeJudgement = Context -> f CType -> f CType
forall (f :: * -> *). Functor f => Context -> f CType -> f CType
normalizeHypothesis


introduce :: Context -> Hypothesis CType -> Judgement' CType -> Judgement' CType
-- NOTE(sandy): It's important that we put the new hypothesis terms first,
-- since 'jAcceptableDestructTargets' will never destruct a pattern that occurs
-- after a previously-destructed term.
introduce :: Context -> Hypothesis CType -> Judgement -> Judgement
introduce Context
ctx Hypothesis CType
hy =
  forall s t a b. HasField "_jHypothesis" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"_jHypothesis" ((Hypothesis CType -> Identity (Hypothesis CType))
 -> Judgement -> Identity Judgement)
-> (Hypothesis CType -> Hypothesis CType) -> Judgement -> Judgement
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Hypothesis CType -> Hypothesis CType -> Hypothesis CType
forall a. Monoid a => a -> a -> a
mappend (Context -> Hypothesis CType -> Hypothesis CType
forall (f :: * -> *). Functor f => Context -> f CType -> f CType
normalizeHypothesis Context
ctx Hypothesis CType
hy)


------------------------------------------------------------------------------
-- | Helper function for implementing functions which introduce new hypotheses.
introduceHypothesis
    :: (Int -> Int -> Provenance)
        -- ^ A function from the total number of args and position of this arg
        -- to its provenance.
    -> [(OccName, a)]
    -> Hypothesis a
introduceHypothesis :: (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
introduceHypothesis Int -> Int -> Provenance
f [(OccName, a)]
ns =
  [HyInfo a] -> Hypothesis a
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo a] -> Hypothesis a) -> [HyInfo a] -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ [Int] -> [(OccName, a)] -> [(Int, (OccName, a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(OccName, a)]
ns [(Int, (OccName, a))]
-> ((Int, (OccName, a)) -> HyInfo a) -> [HyInfo a]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Int
pos, (OccName
name, a
ty)) ->
    OccName -> Provenance -> a -> HyInfo a
forall a. OccName -> Provenance -> a -> HyInfo a
HyInfo OccName
name (Int -> Int -> Provenance
f ([(OccName, a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(OccName, a)]
ns) Int
pos) a
ty


------------------------------------------------------------------------------
-- | Introduce bindings in the context of a lamba.
lambdaHypothesis
    :: Maybe OccName   -- ^ The name of the top level function. For any other
                       -- function, this should be 'Nothing'.
    -> [(OccName, a)]
    -> Hypothesis a
lambdaHypothesis :: Maybe OccName -> [(OccName, a)] -> Hypothesis a
lambdaHypothesis Maybe OccName
func =
  (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a.
(Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
introduceHypothesis ((Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a)
-> (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ \Int
count Int
pos ->
    Provenance
-> (OccName -> Provenance) -> Maybe OccName -> Provenance
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Provenance
UserPrv (\OccName
x -> OccName -> Int -> Int -> Provenance
TopLevelArgPrv OccName
x Int
pos Int
count) Maybe OccName
func


------------------------------------------------------------------------------
-- | Introduce a binding in a recursive context.
recursiveHypothesis :: [(OccName, a)] -> Hypothesis a
recursiveHypothesis :: [(OccName, a)] -> Hypothesis a
recursiveHypothesis = (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a.
(Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
introduceHypothesis ((Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a)
-> (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ (Int -> Provenance) -> Int -> Int -> Provenance
forall a b. a -> b -> a
const ((Int -> Provenance) -> Int -> Int -> Provenance)
-> (Int -> Provenance) -> Int -> Int -> Provenance
forall a b. (a -> b) -> a -> b
$ Provenance -> Int -> Provenance
forall a b. a -> b -> a
const Provenance
RecursivePrv


------------------------------------------------------------------------------
-- | Introduce a binding in a recursive context.
userHypothesis :: [(OccName, a)] -> Hypothesis a
userHypothesis :: [(OccName, a)] -> Hypothesis a
userHypothesis = (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a.
(Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
introduceHypothesis ((Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a)
-> (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ (Int -> Provenance) -> Int -> Int -> Provenance
forall a b. a -> b -> a
const ((Int -> Provenance) -> Int -> Int -> Provenance)
-> (Int -> Provenance) -> Int -> Int -> Provenance
forall a b. (a -> b) -> a -> b
$ Provenance -> Int -> Provenance
forall a b. a -> b -> a
const Provenance
UserPrv


------------------------------------------------------------------------------
-- | Check whether any of the given occnames are an ancestor of the term.
hasPositionalAncestry
    :: Foldable t
    => t OccName   -- ^ Desired ancestors.
    -> Judgement
    -> OccName     -- ^ Potential child
    -> Maybe Bool  -- ^ Just True if the result is the oldest positional ancestor
                   -- just false if it's a descendent
                   -- otherwise nothing
hasPositionalAncestry :: t OccName -> Judgement -> OccName -> Maybe Bool
hasPositionalAncestry t OccName
ancestors Judgement
jdg OccName
name
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ t OccName -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t OccName
ancestors
  = case OccName
name OccName -> t OccName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t OccName
ancestors of
      Bool
True  -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
      Bool
False ->
        case OccName -> Map OccName (Set OccName) -> Maybe (Set OccName)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName (Set OccName) -> Maybe (Set OccName))
-> Map OccName (Set OccName) -> Maybe (Set OccName)
forall a b. (a -> b) -> a -> b
$ Judgement -> Map OccName (Set OccName)
forall a. Judgement' a -> Map OccName (Set OccName)
jAncestryMap Judgement
jdg of
          Just Set OccName
ancestry ->
            Maybe Bool -> Maybe Bool -> Bool -> Maybe Bool
forall a. a -> a -> Bool -> a
bool Maybe Bool
forall a. Maybe a
Nothing (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False) (Bool -> Maybe Bool) -> Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ (OccName -> Bool) -> t OccName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((OccName -> Set OccName -> Bool) -> Set OccName -> OccName -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip OccName -> Set OccName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set OccName
ancestry) t OccName
ancestors
          Maybe (Set OccName)
Nothing -> Maybe Bool
forall a. Maybe a
Nothing
  | Bool
otherwise = Maybe Bool
forall a. Maybe a
Nothing


------------------------------------------------------------------------------
-- | Helper function for disallowing hypotheses that have the wrong ancestry.
filterAncestry
    :: Foldable t
    => t OccName
    -> DisallowReason
    -> Judgement
    -> Judgement
filterAncestry :: t OccName -> DisallowReason -> Judgement -> Judgement
filterAncestry t OccName
ancestry DisallowReason
reason Judgement
jdg =
    DisallowReason -> Set OccName -> Judgement -> Judgement
forall a.
DisallowReason -> Set OccName -> Judgement' a -> Judgement' a
disallowing DisallowReason
reason (Map OccName (HyInfo CType) -> Set OccName
forall k a. Map k a -> Set k
M.keysSet (Map OccName (HyInfo CType) -> Set OccName)
-> Map OccName (HyInfo CType) -> Set OccName
forall a b. (a -> b) -> a -> b
$ (OccName -> HyInfo CType -> Bool)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey OccName -> HyInfo CType -> Bool
go (Map OccName (HyInfo CType) -> Map OccName (HyInfo CType))
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName (Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg) Judgement
jdg
  where
    go :: OccName -> HyInfo CType -> Bool
go OccName
name HyInfo CType
_
      = Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing
      (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ t OccName -> Judgement -> OccName -> Maybe Bool
forall (t :: * -> *).
Foldable t =>
t OccName -> Judgement -> OccName -> Maybe Bool
hasPositionalAncestry t OccName
ancestry Judgement
jdg OccName
name


------------------------------------------------------------------------------
-- | @filter defn pos@ removes any hypotheses which are bound in @defn@ to
-- a position other than @pos@. Any terms whose ancestry doesn't include @defn@
-- remain.
filterPosition :: OccName -> Int -> Judgement -> Judgement
filterPosition :: OccName -> Int -> Judgement -> Judgement
filterPosition OccName
defn Int
pos Judgement
jdg =
  Maybe OccName -> DisallowReason -> Judgement -> Judgement
forall (t :: * -> *).
Foldable t =>
t OccName -> DisallowReason -> Judgement -> Judgement
filterAncestry (Judgement -> OccName -> Int -> Maybe OccName
forall a. Judgement' a -> OccName -> Int -> Maybe OccName
findPositionVal Judgement
jdg OccName
defn Int
pos) (Int -> DisallowReason
WrongBranch Int
pos) Judgement
jdg


------------------------------------------------------------------------------
-- | Helper function for determining the ancestry list for 'filterPosition'.
findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
findPositionVal :: Judgement' a -> OccName -> Int -> Maybe OccName
findPositionVal Judgement' a
jdg OccName
defn Int
pos = [OccName] -> Maybe OccName
forall a. [a] -> Maybe a
listToMaybe ([OccName] -> Maybe OccName) -> [OccName] -> Maybe OccName
forall a b. (a -> b) -> a -> b
$ do
  -- It's important to inspect the entire hypothesis here, as we need to trace
  -- ancstry through potentially disallowed terms in the hypothesis.
  (OccName
name, HyInfo a
hi) <- Map OccName (HyInfo a) -> [(OccName, HyInfo a)]
forall k a. Map k a -> [(k, a)]
M.toList
              (Map OccName (HyInfo a) -> [(OccName, HyInfo a)])
-> Map OccName (HyInfo a) -> [(OccName, HyInfo a)]
forall a b. (a -> b) -> a -> b
$ (HyInfo a -> HyInfo a)
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Provenance -> Provenance) -> HyInfo a -> HyInfo a
forall a. (Provenance -> Provenance) -> HyInfo a -> HyInfo a
overProvenance Provenance -> Provenance
expandDisallowed)
              (Map OccName (HyInfo a) -> Map OccName (HyInfo a))
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
forall a b. (a -> b) -> a -> b
$ Hypothesis a -> Map OccName (HyInfo a)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName
              (Hypothesis a -> Map OccName (HyInfo a))
-> Hypothesis a -> Map OccName (HyInfo a)
forall a b. (a -> b) -> a -> b
$ Judgement' a -> Hypothesis a
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis Judgement' a
jdg
  case HyInfo a -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance HyInfo a
hi of
    TopLevelArgPrv OccName
defn' Int
pos' Int
_
      | OccName
defn OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
defn'
      , Int
pos  Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
pos' -> OccName -> [OccName]
forall (f :: * -> *) a. Applicative f => a -> f a
pure OccName
name
    PatternMatchPrv PatVal
pv
      | PatVal -> Maybe OccName
pv_scrutinee PatVal
pv Maybe OccName -> Maybe OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName -> Maybe OccName
forall a. a -> Maybe a
Just OccName
defn
      , PatVal -> Int
pv_position PatVal
pv  Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
pos -> OccName -> [OccName]
forall (f :: * -> *) a. Applicative f => a -> f a
pure OccName
name
    Provenance
_ -> []


------------------------------------------------------------------------------
-- | Helper function for determining the ancestry list for
-- 'filterSameTypeFromOtherPositions'.
findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName]
findDconPositionVals :: Judgement' a -> ConLike -> Int -> [OccName]
findDconPositionVals Judgement' a
jdg ConLike
dcon Int
pos = do
  (OccName
name, HyInfo a
hi) <- Map OccName (HyInfo a) -> [(OccName, HyInfo a)]
forall k a. Map k a -> [(k, a)]
M.toList (Map OccName (HyInfo a) -> [(OccName, HyInfo a)])
-> Map OccName (HyInfo a) -> [(OccName, HyInfo a)]
forall a b. (a -> b) -> a -> b
$ Hypothesis a -> Map OccName (HyInfo a)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName (Hypothesis a -> Map OccName (HyInfo a))
-> Hypothesis a -> Map OccName (HyInfo a)
forall a b. (a -> b) -> a -> b
$ Judgement' a -> Hypothesis a
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement' a
jdg
  case HyInfo a -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance HyInfo a
hi of
    PatternMatchPrv PatVal
pv
      | PatVal -> Uniquely ConLike
pv_datacon  PatVal
pv Uniquely ConLike -> Uniquely ConLike -> Bool
forall a. Eq a => a -> a -> Bool
== ConLike -> Uniquely ConLike
forall a. a -> Uniquely a
Uniquely ConLike
dcon
      , PatVal -> Int
pv_position PatVal
pv Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
pos -> OccName -> [OccName]
forall (f :: * -> *) a. Applicative f => a -> f a
pure OccName
name
    Provenance
_ -> []


------------------------------------------------------------------------------
-- | Disallow any hypotheses who have the same type as anything bound by the
-- given position for the datacon. Used to ensure recursive functions like
-- 'fmap' preserve the relative ordering of their arguments by eliminating any
-- other term which might match.
filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement
filterSameTypeFromOtherPositions :: ConLike -> Int -> Judgement -> Judgement
filterSameTypeFromOtherPositions ConLike
dcon Int
pos Judgement
jdg =
  let hy :: Map OccName (HyInfo CType)
hy = Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName
         (Hypothesis CType -> Map OccName (HyInfo CType))
-> (Judgement -> Hypothesis CType)
-> Judgement
-> Map OccName (HyInfo CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis
         (Judgement -> Map OccName (HyInfo CType))
-> Judgement -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ [OccName] -> DisallowReason -> Judgement -> Judgement
forall (t :: * -> *).
Foldable t =>
t OccName -> DisallowReason -> Judgement -> Judgement
filterAncestry
             (Judgement -> ConLike -> Int -> [OccName]
forall a. Judgement' a -> ConLike -> Int -> [OccName]
findDconPositionVals Judgement
jdg ConLike
dcon Int
pos)
             (Int -> DisallowReason
WrongBranch Int
pos)
             Judgement
jdg
      tys :: Set CType
tys = [CType] -> Set CType
forall a. Ord a => [a] -> Set a
S.fromList ([CType] -> Set CType) -> [CType] -> Set CType
forall a b. (a -> b) -> a -> b
$ HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type (HyInfo CType -> CType) -> [HyInfo CType] -> [CType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map OccName (HyInfo CType) -> [HyInfo CType]
forall k a. Map k a -> [a]
M.elems Map OccName (HyInfo CType)
hy
      to_remove :: Map OccName (HyInfo CType)
to_remove =
        (HyInfo CType -> Bool)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter ((CType -> Set CType -> Bool) -> Set CType -> CType -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip CType -> Set CType -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member Set CType
tys (CType -> Bool) -> (HyInfo CType -> CType) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type) (Hypothesis CType -> Map OccName (HyInfo CType)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName (Hypothesis CType -> Map OccName (HyInfo CType))
-> Hypothesis CType -> Map OccName (HyInfo CType)
forall a b. (a -> b) -> a -> b
$ Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jHypothesis Judgement
jdg)
          Map OccName (HyInfo CType)
-> Map OccName (HyInfo CType) -> Map OccName (HyInfo CType)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.\\ Map OccName (HyInfo CType)
hy
   in DisallowReason -> Set OccName -> Judgement -> Judgement
forall a.
DisallowReason -> Set OccName -> Judgement' a -> Judgement' a
disallowing DisallowReason
Shadowed (Map OccName (HyInfo CType) -> Set OccName
forall k a. Map k a -> Set k
M.keysSet Map OccName (HyInfo CType)
to_remove) Judgement
jdg


------------------------------------------------------------------------------
-- | Return the ancestry of a 'PatVal', or 'mempty' otherwise.
getAncestry :: Judgement' a -> OccName -> Set OccName
getAncestry :: Judgement' a -> OccName -> Set OccName
getAncestry Judgement' a
jdg OccName
name =
  Set OccName
-> (PatVal -> Set OccName) -> Maybe PatVal -> Set OccName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set OccName
forall a. Monoid a => a
mempty PatVal -> Set OccName
pv_ancestry (Maybe PatVal -> Set OccName)
-> (Map OccName PatVal -> Maybe PatVal)
-> Map OccName PatVal
-> Set OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> Map OccName PatVal -> Maybe PatVal
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName PatVal -> Set OccName)
-> Map OccName PatVal -> Set OccName
forall a b. (a -> b) -> a -> b
$ Judgement' a -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement' a
jdg


jAncestryMap :: Judgement' a -> Map OccName (Set OccName)
jAncestryMap :: Judgement' a -> Map OccName (Set OccName)
jAncestryMap Judgement' a
jdg =
  (PatVal -> Set OccName)
-> Map OccName PatVal -> Map OccName (Set OccName)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map PatVal -> Set OccName
pv_ancestry (Judgement' a -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement' a
jdg)


provAncestryOf :: Provenance -> Set OccName
provAncestryOf :: Provenance -> Set OccName
provAncestryOf (TopLevelArgPrv OccName
o Int
_ Int
_) = OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
o
provAncestryOf (PatternMatchPrv (PatVal Maybe OccName
mo Set OccName
so Uniquely ConLike
_ Int
_)) =
  Set OccName
-> (OccName -> Set OccName) -> Maybe OccName -> Set OccName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set OccName
forall a. Monoid a => a
mempty OccName -> Set OccName
forall a. a -> Set a
S.singleton Maybe OccName
mo Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Set OccName
so
provAncestryOf (ClassMethodPrv Uniquely Class
_) = Set OccName
forall a. Monoid a => a
mempty
provAncestryOf Provenance
UserPrv = Set OccName
forall a. Monoid a => a
mempty
provAncestryOf Provenance
RecursivePrv = Set OccName
forall a. Monoid a => a
mempty
provAncestryOf Provenance
ImportPrv = Set OccName
forall a. Monoid a => a
mempty
provAncestryOf (DisallowedPrv DisallowReason
_ Provenance
p2) = Provenance -> Set OccName
provAncestryOf Provenance
p2


------------------------------------------------------------------------------
-- TODO(sandy): THIS THING IS A BIG BIG HACK
--
-- Why? 'ctxDefiningFuncs' is _all_ of the functions currently beind defined
-- (eg, we might be in a where block). The head of this list is not guaranteed
-- to be the one we're interested in.
extremelyStupid__definingFunction :: Context -> OccName
extremelyStupid__definingFunction :: Context -> OccName
extremelyStupid__definingFunction =
  (OccName, CType) -> OccName
forall a b. (a, b) -> a
fst ((OccName, CType) -> OccName)
-> (Context -> (OccName, CType)) -> Context -> OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(OccName, CType)] -> (OccName, CType)
forall a. [a] -> a
head ([(OccName, CType)] -> (OccName, CType))
-> (Context -> [(OccName, CType)]) -> Context -> (OccName, CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Context -> [(OccName, CType)]
ctxDefiningFuncs


patternHypothesis
    :: Maybe OccName
    -> ConLike
    -> Judgement' a
    -> [(OccName, a)]
    -> Hypothesis a
patternHypothesis :: Maybe OccName
-> ConLike -> Judgement' a -> [(OccName, a)] -> Hypothesis a
patternHypothesis Maybe OccName
scrutinee ConLike
dc Judgement' a
jdg
  = (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a.
(Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
introduceHypothesis ((Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a)
-> (Int -> Int -> Provenance) -> [(OccName, a)] -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ \Int
_ Int
pos ->
      PatVal -> Provenance
PatternMatchPrv (PatVal -> Provenance) -> PatVal -> Provenance
forall a b. (a -> b) -> a -> b
$
        Maybe OccName -> Set OccName -> Uniquely ConLike -> Int -> PatVal
PatVal
          Maybe OccName
scrutinee
          (Set OccName
-> (OccName -> Set OccName) -> Maybe OccName -> Set OccName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
              Set OccName
forall a. Monoid a => a
mempty
              (\OccName
scrut -> OccName -> Set OccName
forall a. a -> Set a
S.singleton OccName
scrut Set OccName -> Set OccName -> Set OccName
forall a. Semigroup a => a -> a -> a
<> Judgement' a -> OccName -> Set OccName
forall a. Judgement' a -> OccName -> Set OccName
getAncestry Judgement' a
jdg OccName
scrut)
              Maybe OccName
scrutinee)
          (ConLike -> Uniquely ConLike
forall a. a -> Uniquely a
Uniquely ConLike
dc)
          Int
pos


------------------------------------------------------------------------------
-- | Prevent some occnames from being used in the hypothesis. This will hide
-- them from 'jHypothesis', but not from 'jEntireHypothesis'.
disallowing :: DisallowReason -> S.Set OccName -> Judgement' a -> Judgement' a
disallowing :: DisallowReason -> Set OccName -> Judgement' a -> Judgement' a
disallowing DisallowReason
reason Set OccName
ns =
  forall s t a b. HasField "_jHypothesis" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"_jHypothesis" ((Hypothesis a -> Identity (Hypothesis a))
 -> Judgement' a -> Identity (Judgement' a))
-> (Hypothesis a -> Hypothesis a) -> Judgement' a -> Judgement' a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (\Hypothesis a
z -> [HyInfo a] -> Hypothesis a
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo a] -> Hypothesis a)
-> ((HyInfo a -> HyInfo a) -> [HyInfo a])
-> (HyInfo a -> HyInfo a)
-> Hypothesis a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HyInfo a -> HyInfo a) -> [HyInfo a] -> [HyInfo a])
-> [HyInfo a] -> (HyInfo a -> HyInfo a) -> [HyInfo a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (HyInfo a -> HyInfo a) -> [HyInfo a] -> [HyInfo a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis Hypothesis a
z) ((HyInfo a -> HyInfo a) -> Hypothesis a)
-> (HyInfo a -> HyInfo a) -> Hypothesis a
forall a b. (a -> b) -> a -> b
$ \HyInfo a
hi ->
    case OccName -> Set OccName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (HyInfo a -> OccName
forall a. HyInfo a -> OccName
hi_name HyInfo a
hi) Set OccName
ns of
      Bool
True  -> (Provenance -> Provenance) -> HyInfo a -> HyInfo a
forall a. (Provenance -> Provenance) -> HyInfo a -> HyInfo a
overProvenance (DisallowReason -> Provenance -> Provenance
DisallowedPrv DisallowReason
reason) HyInfo a
hi
      Bool
False -> HyInfo a
hi
                           )


------------------------------------------------------------------------------
-- | The hypothesis, consisting of local terms and the ambient environment
-- (impors and class methods.) Hides disallowed values.
jHypothesis :: Judgement' a -> Hypothesis a
jHypothesis :: Judgement' a -> Hypothesis a
jHypothesis
  = [HyInfo a] -> Hypothesis a
forall a. [HyInfo a] -> Hypothesis a
Hypothesis
  ([HyInfo a] -> Hypothesis a)
-> (Judgement' a -> [HyInfo a]) -> Judgement' a -> Hypothesis a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo a -> Bool) -> [HyInfo a] -> [HyInfo a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (HyInfo a -> Bool) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provenance -> Bool
isDisallowed (Provenance -> Bool)
-> (HyInfo a -> Provenance) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo a -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance)
  ([HyInfo a] -> [HyInfo a])
-> (Judgement' a -> [HyInfo a]) -> Judgement' a -> [HyInfo a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
  (Hypothesis a -> [HyInfo a])
-> (Judgement' a -> Hypothesis a) -> Judgement' a -> [HyInfo a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement' a -> Hypothesis a
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis


------------------------------------------------------------------------------
-- | The whole hypothesis, including things disallowed.
jEntireHypothesis :: Judgement' a -> Hypothesis a
jEntireHypothesis :: Judgement' a -> Hypothesis a
jEntireHypothesis = Judgement' a -> Hypothesis a
forall a. Judgement' a -> Hypothesis a
_jHypothesis


------------------------------------------------------------------------------
-- | Just the local hypothesis.
jLocalHypothesis :: Judgement' a -> Hypothesis a
jLocalHypothesis :: Judgement' a -> Hypothesis a
jLocalHypothesis
  = [HyInfo a] -> Hypothesis a
forall a. [HyInfo a] -> Hypothesis a
Hypothesis
  ([HyInfo a] -> Hypothesis a)
-> (Judgement' a -> [HyInfo a]) -> Judgement' a -> Hypothesis a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo a -> Bool) -> [HyInfo a] -> [HyInfo a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Provenance -> Bool
isLocalHypothesis (Provenance -> Bool)
-> (HyInfo a -> Provenance) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo a -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance)
  ([HyInfo a] -> [HyInfo a])
-> (Judgement' a -> [HyInfo a]) -> Judgement' a -> [HyInfo a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
  (Hypothesis a -> [HyInfo a])
-> (Judgement' a -> Hypothesis a) -> Judgement' a -> [HyInfo a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement' a -> Hypothesis a
forall a. Judgement' a -> Hypothesis a
jHypothesis


------------------------------------------------------------------------------
-- | Filter elements from the hypothesis
hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a
hyFilter :: (HyInfo a -> Bool) -> Hypothesis a -> Hypothesis a
hyFilter HyInfo a -> Bool
f  = [HyInfo a] -> Hypothesis a
forall a. [HyInfo a] -> Hypothesis a
Hypothesis ([HyInfo a] -> Hypothesis a)
-> (Hypothesis a -> [HyInfo a]) -> Hypothesis a -> Hypothesis a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo a -> Bool) -> [HyInfo a] -> [HyInfo a]
forall a. (a -> Bool) -> [a] -> [a]
filter HyInfo a -> Bool
f ([HyInfo a] -> [HyInfo a])
-> (Hypothesis a -> [HyInfo a]) -> Hypothesis a -> [HyInfo a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis


------------------------------------------------------------------------------
-- | Given a judgment, return the hypotheses that are acceptable to destruct.
--
-- We use the ordering of the hypothesis for this purpose. Since new bindings
-- are always inserted at the beginning, we can impose a canonical ordering on
-- which order to try destructs by what order they are introduced --- stopping
-- at the first one we've already destructed.
jAcceptableDestructTargets :: Judgement' CType -> [HyInfo CType]
jAcceptableDestructTargets :: Judgement -> [HyInfo CType]
jAcceptableDestructTargets
  = (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe TyCon -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TyCon -> Bool)
-> (HyInfo CType -> Maybe TyCon) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TyCon
algebraicTyCon (Type -> Maybe TyCon)
-> (HyInfo CType -> Type) -> HyInfo CType -> Maybe TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (HyInfo CType -> CType) -> HyInfo CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> CType
forall a. HyInfo a -> a
hi_type)
  ([HyInfo CType] -> [HyInfo CType])
-> (Judgement -> [HyInfo CType]) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo CType -> Bool) -> [HyInfo CType] -> [HyInfo CType]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Bool -> Bool
not (Bool -> Bool) -> (HyInfo CType -> Bool) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Provenance -> Bool
isAlreadyDestructed (Provenance -> Bool)
-> (HyInfo CType -> Provenance) -> HyInfo CType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo CType -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance)
  ([HyInfo CType] -> [HyInfo CType])
-> (Judgement -> [HyInfo CType]) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis CType -> [HyInfo CType]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
  (Hypothesis CType -> [HyInfo CType])
-> (Judgement -> Hypothesis CType) -> Judgement -> [HyInfo CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> Hypothesis CType
forall a. Judgement' a -> Hypothesis a
jEntireHypothesis


------------------------------------------------------------------------------
-- | If we're in a top hole, the name of the defining function.
isTopHole :: Context -> Judgement' a -> Maybe OccName
isTopHole :: Context -> Judgement' a -> Maybe OccName
isTopHole Context
ctx =
  Maybe OccName -> Maybe OccName -> Bool -> Maybe OccName
forall a. a -> a -> Bool -> a
bool Maybe OccName
forall a. Maybe a
Nothing (OccName -> Maybe OccName
forall a. a -> Maybe a
Just (OccName -> Maybe OccName) -> OccName -> Maybe OccName
forall a b. (a -> b) -> a -> b
$ Context -> OccName
extremelyStupid__definingFunction Context
ctx) (Bool -> Maybe OccName)
-> (Judgement' a -> Bool) -> Judgement' a -> Maybe OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement' a -> Bool
forall a. Judgement' a -> Bool
_jIsTopHole


unsetIsTopHole :: Judgement' a -> Judgement' a
unsetIsTopHole :: Judgement' a -> Judgement' a
unsetIsTopHole = forall s t a b. HasField "_jIsTopHole" s t a b => Lens s t a b
forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"_jIsTopHole" ((Bool -> Identity Bool)
 -> Judgement' a -> Identity (Judgement' a))
-> Bool -> Judgement' a -> Judgement' a
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Bool
False


------------------------------------------------------------------------------
-- | What names are currently in scope in the hypothesis?
hyNamesInScope :: Hypothesis a -> Set OccName
hyNamesInScope :: Hypothesis a -> Set OccName
hyNamesInScope = Map OccName (HyInfo a) -> Set OccName
forall k a. Map k a -> Set k
M.keysSet (Map OccName (HyInfo a) -> Set OccName)
-> (Hypothesis a -> Map OccName (HyInfo a))
-> Hypothesis a
-> Set OccName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis a -> Map OccName (HyInfo a)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName


------------------------------------------------------------------------------
-- | Are there any top-level function argument bindings in this judgement?
jHasBoundArgs :: Judgement' a -> Bool
jHasBoundArgs :: Judgement' a -> Bool
jHasBoundArgs
  = (HyInfo a -> Bool) -> [HyInfo a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Provenance -> Bool
isTopLevel (Provenance -> Bool)
-> (HyInfo a -> Provenance) -> HyInfo a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo a -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance)
  ([HyInfo a] -> Bool)
-> (Judgement' a -> [HyInfo a]) -> Judgement' a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis
  (Hypothesis a -> [HyInfo a])
-> (Judgement' a -> Hypothesis a) -> Judgement' a -> [HyInfo a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement' a -> Hypothesis a
forall a. Judgement' a -> Hypothesis a
jLocalHypothesis


jNeedsToBindArgs :: Judgement' CType -> Bool
jNeedsToBindArgs :: Judgement -> Bool
jNeedsToBindArgs = Type -> Bool
isFunTy (Type -> Bool) -> (Judgement -> Type) -> Judgement -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
unCType (CType -> Type) -> (Judgement -> CType) -> Judgement -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement -> CType
forall a. Judgement' a -> a
jGoal


------------------------------------------------------------------------------
-- | Fold a hypothesis into a single mapping from name to info. This
-- unavoidably will cause duplicate names (things like methods) to shadow one
-- another.
hyByName :: Hypothesis a -> Map OccName (HyInfo a)
hyByName :: Hypothesis a -> Map OccName (HyInfo a)
hyByName
  = [(OccName, HyInfo a)] -> Map OccName (HyInfo a)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
  ([(OccName, HyInfo a)] -> Map OccName (HyInfo a))
-> (Hypothesis a -> [(OccName, HyInfo a)])
-> Hypothesis a
-> Map OccName (HyInfo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HyInfo a -> (OccName, HyInfo a))
-> [HyInfo a] -> [(OccName, HyInfo a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HyInfo a -> OccName
forall a. HyInfo a -> OccName
hi_name (HyInfo a -> OccName)
-> (HyInfo a -> HyInfo a) -> HyInfo a -> (OccName, HyInfo a)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& HyInfo a -> HyInfo a
forall a. a -> a
id)
  ([HyInfo a] -> [(OccName, HyInfo a)])
-> (Hypothesis a -> [HyInfo a])
-> Hypothesis a
-> [(OccName, HyInfo a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis a -> [HyInfo a]
forall a. Hypothesis a -> [HyInfo a]
unHypothesis


------------------------------------------------------------------------------
-- | Only the hypothesis members which are pattern vals
jPatHypothesis :: Judgement' a -> Map OccName PatVal
jPatHypothesis :: Judgement' a -> Map OccName PatVal
jPatHypothesis
  = (HyInfo a -> Maybe PatVal)
-> Map OccName (HyInfo a) -> Map OccName PatVal
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
M.mapMaybe (Provenance -> Maybe PatVal
getPatVal (Provenance -> Maybe PatVal)
-> (HyInfo a -> Provenance) -> HyInfo a -> Maybe PatVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HyInfo a -> Provenance
forall a. HyInfo a -> Provenance
hi_provenance)
  (Map OccName (HyInfo a) -> Map OccName PatVal)
-> (Judgement' a -> Map OccName (HyInfo a))
-> Judgement' a
-> Map OccName PatVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Hypothesis a -> Map OccName (HyInfo a)
forall a. Hypothesis a -> Map OccName (HyInfo a)
hyByName
  (Hypothesis a -> Map OccName (HyInfo a))
-> (Judgement' a -> Hypothesis a)
-> Judgement' a
-> Map OccName (HyInfo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement' a -> Hypothesis a
forall a. Judgement' a -> Hypothesis a
jHypothesis


getPatVal :: Provenance-> Maybe PatVal
getPatVal :: Provenance -> Maybe PatVal
getPatVal Provenance
prov =
  case Provenance
prov of
    PatternMatchPrv PatVal
pv -> PatVal -> Maybe PatVal
forall a. a -> Maybe a
Just PatVal
pv
    Provenance
_                  -> Maybe PatVal
forall a. Maybe a
Nothing


jGoal :: Judgement' a -> a
jGoal :: Judgement' a -> a
jGoal = Judgement' a -> a
forall a. Judgement' a -> a
_jGoal


substJdg :: TCvSubst -> Judgement -> Judgement
substJdg :: TCvSubst -> Judgement -> Judgement
substJdg TCvSubst
subst = (CType -> CType) -> Judgement -> Judgement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((CType -> CType) -> Judgement -> Judgement)
-> (CType -> CType) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$ Type -> CType
coerce (Type -> CType) -> (CType -> Type) -> CType -> CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (Type -> Type) -> (CType -> Type) -> CType -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CType -> Type
coerce


mkFirstJudgement
    :: Context
    -> Hypothesis CType
    -> Bool  -- ^ are we in the top level rhs hole?
    -> Type
    -> Judgement' CType
mkFirstJudgement :: Context -> Hypothesis CType -> Bool -> Type -> Judgement
mkFirstJudgement Context
ctx Hypothesis CType
hy Bool
top Type
goal =
  Context -> Judgement -> Judgement
forall (f :: * -> *). Functor f => Context -> f CType -> f CType
normalizeJudgement Context
ctx (Judgement -> Judgement) -> Judgement -> Judgement
forall a b. (a -> b) -> a -> b
$
    Judgement :: forall a.
Hypothesis a
-> Bool -> Bool -> Bool -> a -> TCvSubst -> Judgement' a
Judgement
      { _jHypothesis :: Hypothesis CType
_jHypothesis        = Hypothesis CType
hy
      , _jBlacklistDestruct :: Bool
_jBlacklistDestruct = Bool
False
      , _jWhitelistSplit :: Bool
_jWhitelistSplit    = Bool
True
      , _jIsTopHole :: Bool
_jIsTopHole         = Bool
top
      , _jGoal :: CType
_jGoal              = Type -> CType
CType Type
goal
      , j_coercion :: TCvSubst
j_coercion          = TCvSubst
emptyTCvSubst
      }


------------------------------------------------------------------------------
-- | Is this a top level function binding?
isTopLevel :: Provenance -> Bool
isTopLevel :: Provenance -> Bool
isTopLevel TopLevelArgPrv{} = Bool
True
isTopLevel Provenance
_                = Bool
False


------------------------------------------------------------------------------
-- | Is this a local function argument, pattern match or user val?
isLocalHypothesis :: Provenance -> Bool
isLocalHypothesis :: Provenance -> Bool
isLocalHypothesis UserPrv{}         = Bool
True
isLocalHypothesis PatternMatchPrv{} = Bool
True
isLocalHypothesis TopLevelArgPrv{}  = Bool
True
isLocalHypothesis Provenance
_                 = Bool
False


------------------------------------------------------------------------------
-- | Is this a pattern match?
isPatternMatch :: Provenance -> Bool
isPatternMatch :: Provenance -> Bool
isPatternMatch PatternMatchPrv{} = Bool
True
isPatternMatch Provenance
_                 = Bool
False


------------------------------------------------------------------------------
-- | Was this term ever disallowed?
isDisallowed :: Provenance -> Bool
isDisallowed :: Provenance -> Bool
isDisallowed DisallowedPrv{} = Bool
True
isDisallowed Provenance
_               = Bool
False

------------------------------------------------------------------------------
-- | Has this term already been disallowed?
isAlreadyDestructed :: Provenance -> Bool
isAlreadyDestructed :: Provenance -> Bool
isAlreadyDestructed (DisallowedPrv DisallowReason
AlreadyDestructed Provenance
_) = Bool
True
isAlreadyDestructed Provenance
_ = Bool
False


------------------------------------------------------------------------------
-- | Eliminates 'DisallowedPrv' provenances.
expandDisallowed :: Provenance -> Provenance
expandDisallowed :: Provenance -> Provenance
expandDisallowed (DisallowedPrv DisallowReason
_ Provenance
prv) = Provenance -> Provenance
expandDisallowed Provenance
prv
expandDisallowed Provenance
prv                   = Provenance
prv