{-# 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
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
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
introducing
:: (Int -> 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))
introducingLambda
:: Maybe OccName
-> [(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
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
hasPositionalAncestry
:: Foldable t
=> t OccName
-> Judgement
-> OccName
-> Maybe Bool
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
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
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
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
(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
_ -> []
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
_ -> []
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
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
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
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
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
)
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
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
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
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
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
-> 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
}
isTopLevel :: Provenance -> Bool
isTopLevel :: Provenance -> Bool
isTopLevel TopLevelArgPrv{} = Bool
True
isTopLevel Provenance
_ = Bool
False
isLocalHypothesis :: Provenance -> Bool
isLocalHypothesis :: Provenance -> Bool
isLocalHypothesis UserPrv{} = Bool
True
isLocalHypothesis PatternMatchPrv{} = Bool
True
isLocalHypothesis TopLevelArgPrv{} = Bool
True
isLocalHypothesis Provenance
_ = Bool
False
isPatternMatch :: Provenance -> Bool
isPatternMatch :: Provenance -> Bool
isPatternMatch PatternMatchPrv{} = Bool
True
isPatternMatch Provenance
_ = Bool
False
isDisallowed :: Provenance -> Bool
isDisallowed :: Provenance -> Bool
isDisallowed DisallowedPrv{} = Bool
True
isDisallowed Provenance
_ = Bool
False
expandDisallowed :: Provenance -> Provenance
expandDisallowed :: Provenance -> Provenance
expandDisallowed (DisallowedPrv DisallowReason
_ Provenance
prv) = Provenance -> Provenance
expandDisallowed Provenance
prv
expandDisallowed Provenance
prv = Provenance
prv