{-# LANGUAGE DataKinds        #-}
{-# LANGUAGE LambdaCase       #-}
{-# LANGUAGE RecordWildCards  #-}
{-# LANGUAGE TupleSections    #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns     #-}

module Ide.Plugin.Tactic.Judgements
  ( blacklistingDestruct
  , unwhitelistingSplit
  , introducingLambda
  , introducingRecursively
  , introducingPat
  , jGoal
  , jHypothesis
  , jEntireHypothesis
  , jPatHypothesis
  , substJdg
  , unsetIsTopHole
  , filterSameTypeFromOtherPositions
  , isDestructBlacklisted
  , withNewGoal
  , jLocalHypothesis
  , isSplitWhitelisted
  , isPatternMatch
  , filterPosition
  , isTopHole
  , disallowing
  , mkFirstJudgement
  , hypothesisFromBindings
  , isTopLevel
  ) where

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           DataCon (DataCon)
import           Development.IDE.Spans.LocalBindings
import           Ide.Plugin.Tactic.Types
import           OccName
import           SrcLoc
import           Type


------------------------------------------------------------------------------
-- | Given a 'SrcSpan' and a 'Bindings', create a hypothesis.
hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType)
hypothesisFromBindings :: RealSrcSpan -> Bindings -> Map OccName (HyInfo CType)
hypothesisFromBindings RealSrcSpan
span Bindings
bs = [(Name, Maybe Type)] -> Map OccName (HyInfo CType)
buildHypothesis ([(Name, Maybe Type)] -> Map OccName (HyInfo CType))
-> [(Name, Maybe Type)] -> Map OccName (HyInfo 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)] -> Map OccName (HyInfo CType)
buildHypothesis :: [(Name, Maybe Type)] -> Map OccName (HyInfo CType)
buildHypothesis
  = [(OccName, HyInfo CType)] -> Map OccName (HyInfo CType)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
  ([(OccName, HyInfo CType)] -> Map OccName (HyInfo CType))
-> ([(Name, Maybe Type)] -> [(OccName, HyInfo CType)])
-> [(Name, Maybe Type)]
-> Map OccName (HyInfo CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Name, Maybe Type) -> Maybe (OccName, HyInfo CType))
-> [(Name, Maybe Type)] -> [(OccName, HyInfo CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Name, Maybe Type) -> Maybe (OccName, HyInfo CType)
forall name.
HasOccName name =>
(name, Maybe Type) -> Maybe (OccName, HyInfo CType)
go
  where
    go :: (name, Maybe Type) -> Maybe (OccName, HyInfo CType)
go (name -> OccName
forall name. HasOccName name => name -> OccName
occName -> OccName
occ, Maybe Type
t)
      | Just Type
ty <- Maybe Type
t
      , Char -> Bool
isAlpha (Char -> Bool) -> (OccName -> Char) -> OccName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Char
forall a. [a] -> a
head ([Char] -> Char) -> (OccName -> [Char]) -> OccName -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OccName -> [Char]
occNameString (OccName -> Bool) -> OccName -> Bool
forall a b. (a -> b) -> a -> b
$ OccName
occ = (OccName, HyInfo CType) -> Maybe (OccName, HyInfo CType)
forall a. a -> Maybe a
Just (OccName
occ, Provenance -> CType -> HyInfo CType
forall a. Provenance -> a -> HyInfo a
HyInfo Provenance
UserPrv (CType -> HyInfo CType) -> CType -> HyInfo CType
forall a b. (a -> b) -> a -> b
$ Type -> CType
CType Type
ty)
      | Bool
otherwise = Maybe (OccName, HyInfo CType)
forall a. Maybe a
Nothing


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


------------------------------------------------------------------------------
-- | Helper function for implementing functions which introduce new hypotheses.
introducing
    :: (Int -> Provenance)  -- ^ A function from the position of the arg to its
                            -- provenance.
    -> [(OccName, a)]
    -> Judgement' a
    -> Judgement' a
introducing :: (Int -> Provenance)
-> [(OccName, a)] -> Judgement' a -> Judgement' a
introducing Int -> Provenance
f [(OccName, a)]
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" ((Map OccName (HyInfo a) -> Identity (Map OccName (HyInfo a)))
 -> Judgement' a -> Identity (Judgement' a))
-> Map OccName (HyInfo a) -> Judgement' a -> Judgement' a
forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ [(OccName, HyInfo a)] -> Map OccName (HyInfo a)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([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)) -> (OccName, HyInfo a))
-> [(OccName, HyInfo a)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
    \(Int
pos, (OccName
name, a
ty)) -> (OccName
name, Provenance -> a -> HyInfo a
forall a. Provenance -> a -> HyInfo a
HyInfo (Int -> Provenance
f Int
pos) a
ty))


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


------------------------------------------------------------------------------
-- | Introduce a binding in a recursive context.
introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a
introducingRecursively :: [(OccName, a)] -> Judgement' a -> Judgement' a
introducingRecursively = (Int -> Provenance)
-> [(OccName, a)] -> Judgement' a -> Judgement' a
forall a.
(Int -> Provenance)
-> [(OccName, a)] -> Judgement' a -> Judgement' a
introducing ((Int -> Provenance)
 -> [(OccName, a)] -> Judgement' a -> Judgement' a)
-> (Int -> Provenance)
-> [(OccName, a)]
-> Judgement' a
-> Judgement' a
forall a b. (a -> b) -> a -> b
$ Provenance -> Int -> Provenance
forall a b. a -> b -> a
const Provenance
RecursivePrv


------------------------------------------------------------------------------
-- | 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 -> Bool) -> t OccName -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
name) 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 -> [OccName] -> Judgement -> Judgement
forall a.
DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
disallowing DisallowReason
reason (Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys (Map OccName (HyInfo CType) -> [OccName])
-> Map OccName (HyInfo CType) -> [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
forall p. OccName -> p -> 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
$ Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis Judgement
jdg) Judgement
jdg
  where
    go :: OccName -> p -> Bool
go OccName
name p
_
      = Bool -> Bool
not
      (Bool -> Bool) -> (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Bool -> Bool
forall a. Maybe a -> Bool
isJust
      (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
$ Judgement' a -> Map OccName (HyInfo a)
forall a. Judgement' a -> Map OccName (HyInfo 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'
      | 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 -> DataCon -> Int -> [OccName]
findDconPositionVals :: Judgement' a -> DataCon -> Int -> [OccName]
findDconPositionVals Judgement' a
jdg DataCon
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
$ Judgement' a -> Map OccName (HyInfo a)
forall a. Judgement' a -> Map OccName (HyInfo 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 DataCon
pv_datacon  PatVal
pv Uniquely DataCon -> Uniquely DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon -> Uniquely DataCon
forall a. a -> Uniquely a
Uniquely DataCon
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 :: DataCon -> Int -> Judgement -> Judgement
filterSameTypeFromOtherPositions :: DataCon -> Int -> Judgement -> Judgement
filterSameTypeFromOtherPositions DataCon
dcon Int
pos Judgement
jdg =
  let hy :: Map OccName (HyInfo CType)
hy = Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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 -> DataCon -> Int -> [OccName]
forall a. Judgement' a -> DataCon -> Int -> [OccName]
findDconPositionVals Judgement
jdg DataCon
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) (Judgement -> Map OccName (HyInfo CType)
forall a. Judgement' a -> Map OccName (HyInfo 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 -> [OccName] -> Judgement -> Judgement
forall a.
DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
disallowing DisallowReason
Shadowed (Map OccName (HyInfo CType) -> [OccName]
forall k a. Map k a -> [k]
M.keys 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 =
  case OccName -> Map OccName PatVal -> Maybe PatVal
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup OccName
name (Map OccName PatVal -> Maybe PatVal)
-> Map OccName PatVal -> Maybe PatVal
forall a b. (a -> b) -> a -> b
$ Judgement' a -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement' a
jdg of
    Just PatVal
pv -> PatVal -> Set OccName
pv_ancestry PatVal
pv
    Maybe PatVal
Nothing -> Set OccName
forall a. Monoid a => a
mempty


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))
-> Map OccName PatVal
-> (PatVal -> Set OccName)
-> Map OccName (Set OccName)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (PatVal -> Set OccName)
-> Map OccName PatVal -> Map OccName (Set OccName)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (Judgement' a -> Map OccName PatVal
forall a. Judgement' a -> Map OccName PatVal
jPatHypothesis Judgement' a
jdg) PatVal -> Set OccName
pv_ancestry


------------------------------------------------------------------------------
-- 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


------------------------------------------------------------------------------
-- | Pattern vals are currently tracked in jHypothesis, with an extra piece of
-- data sitting around in jPatternVals.
introducingPat
    :: Maybe OccName
    -> DataCon
    -> [(OccName, a)]
    -> Judgement' a
    -> Judgement' a
introducingPat :: Maybe OccName
-> DataCon -> [(OccName, a)] -> Judgement' a -> Judgement' a
introducingPat Maybe OccName
scrutinee DataCon
dc [(OccName, a)]
ns Judgement' a
jdg
  = (Int -> Provenance)
-> [(OccName, a)] -> Judgement' a -> Judgement' a
forall a.
(Int -> Provenance)
-> [(OccName, a)] -> Judgement' a -> Judgement' a
introducing (\Int
pos ->
      PatVal -> Provenance
PatternMatchPrv (PatVal -> Provenance) -> PatVal -> Provenance
forall a b. (a -> b) -> a -> b
$
        Maybe OccName -> Set OccName -> Uniquely DataCon -> 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)
          (DataCon -> Uniquely DataCon
forall a. a -> Uniquely a
Uniquely DataCon
dc)
          Int
pos
    ) [(OccName, a)]
ns Judgement' a
jdg


------------------------------------------------------------------------------
-- | Prevent some occnames from being used in the hypothesis. This will hide
-- them from 'jHypothesis', but not from 'jEntireHypothesis'.
disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
disallowing :: DisallowReason -> [OccName] -> Judgement' a -> Judgement' a
disallowing DisallowReason
reason ([OccName] -> Set OccName
forall a. Ord a => [a] -> Set a
S.fromList -> 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" ((Map OccName (HyInfo a) -> Identity (Map OccName (HyInfo a)))
 -> Judgement' a -> Identity (Judgement' a))
-> (Map OccName (HyInfo a) -> Map OccName (HyInfo a))
-> Judgement' a
-> Judgement' a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((OccName -> HyInfo a -> HyInfo a)
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey ((OccName -> HyInfo a -> HyInfo a)
 -> Map OccName (HyInfo a) -> Map OccName (HyInfo a))
-> (OccName -> HyInfo a -> HyInfo a)
-> Map OccName (HyInfo a)
-> Map OccName (HyInfo a)
forall a b. (a -> b) -> a -> b
$ \OccName
name HyInfo a
hi ->
    case OccName -> Set OccName -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member OccName
name 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 -> Map OccName (HyInfo a)
jHypothesis :: Judgement' a -> Map OccName (HyInfo a)
jHypothesis = (HyInfo a -> Bool)
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.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) (Map OccName (HyInfo a) -> Map OccName (HyInfo a))
-> (Judgement' a -> Map OccName (HyInfo a))
-> Judgement' a
-> Map OccName (HyInfo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement' a -> Map OccName (HyInfo a)
forall a. Judgement' a -> Map OccName (HyInfo a)
jEntireHypothesis


------------------------------------------------------------------------------
-- | The whole hypothesis, including things disallowed.
jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a)
jEntireHypothesis :: Judgement' a -> Map OccName (HyInfo a)
jEntireHypothesis = Judgement' a -> Map OccName (HyInfo a)
forall a. Judgement' a -> Map OccName (HyInfo a)
_jHypothesis


------------------------------------------------------------------------------
-- | Just the local hypothesis.
jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a)
jLocalHypothesis :: Judgement' a -> Map OccName (HyInfo a)
jLocalHypothesis = (HyInfo a -> Bool)
-> Map OccName (HyInfo a) -> Map OccName (HyInfo a)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.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) (Map OccName (HyInfo a) -> Map OccName (HyInfo a))
-> (Judgement' a -> Map OccName (HyInfo a))
-> Judgement' a
-> Map OccName (HyInfo a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgement' a -> Map OccName (HyInfo a)
forall a. Judgement' a -> Map OccName (HyInfo a)
jHypothesis


------------------------------------------------------------------------------
-- | 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


------------------------------------------------------------------------------
-- | 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
. Judgement' a -> Map OccName (HyInfo a)
forall a. Judgement' a -> Map OccName (HyInfo 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
    :: M.Map OccName (HyInfo CType)
    -> Bool  -- ^ are we in the top level rhs hole?
    -> Type
    -> Judgement' CType
mkFirstJudgement :: Map OccName (HyInfo CType) -> Bool -> Type -> Judgement
mkFirstJudgement Map OccName (HyInfo CType)
hy Bool
top Type
goal = Judgement :: forall a.
Map OccName (HyInfo a) -> Bool -> Bool -> Bool -> a -> Judgement' a
Judgement
  { _jHypothesis :: Map OccName (HyInfo CType)
_jHypothesis        = Map OccName (HyInfo 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
  }


------------------------------------------------------------------------------
-- | 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


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