{-# LANGUAGE PatternSynonyms #-}

-- |
-- Module      :  Disco.Exhaustiveness
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Entry point into the exhaustiveness checker.
-- Converts information into a format the checker understands,
-- then pretty prints the results of running it.
module Disco.Exhaustiveness where

import Control.Monad (forM, unless, zipWithM)
import Control.Monad.Trans.Maybe (MaybeT, runMaybeT)
import Data.List (nub)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NonEmpty
import Data.Maybe (catMaybes)
import Disco.AST.Generic (Side (..))
import Disco.AST.Surface (
  Pattern,
  prettyPatternP,
  pattern PBool,
  pattern PChar,
  pattern PInj,
  pattern PList,
  pattern PNat,
  pattern PNeg,
  pattern PString,
  pattern PTup,
  pattern PUnit,
  pattern PWild,
 )
import Disco.AST.Typed (
  APattern,
  ATerm,
  pattern APBool,
  pattern APChar,
  pattern APCons,
  pattern APInj,
  pattern APList,
  pattern APNat,
  pattern APNeg,
  pattern APString,
  pattern APTup,
  pattern APUnit,
  pattern APVar,
  pattern APWild,
 )
import Disco.Effects.Fresh (Fresh)
import Disco.Effects.LFresh (LFresh, runLFresh)
import qualified Disco.Exhaustiveness.Constraint as C
import qualified Disco.Exhaustiveness.Possibilities as Poss
import qualified Disco.Exhaustiveness.TypeInfo as TI
import Disco.Messages
import Disco.Pretty (Doc, initPA, withPA)
import qualified Disco.Pretty.DSL as DSL
import Disco.Pretty.Prec (PA, funPA)
import qualified Disco.Types as Ty
import Polysemy
import Polysemy.Output
import Polysemy.Reader
import Unbound.Generics.LocallyNameless (Name)

-- | This exhaustiveness checking algorithm is based on the paper
--   "Lower Your Guards: A Compositional Pattern-Match Coverage Checker":
--   https://www.microsoft.com/en-us/research/uploads/prod/2020/03/lyg.pdf
--
--   Some simplifications were made to adapt the algorithm to suit Disco.
--   The most notable change is that here we always generate (at most) 3
--   concrete examples of uncovered patterns, instead of finding the most
--   general complete description of every uncovered input.
checkClauses :: (Members '[Fresh, Reader Ty.TyDefCtx, Output (Message ann), Embed IO] r) => Name ATerm -> [Ty.Type] -> NonEmpty [APattern] -> Sem r ()
checkClauses :: forall ann (r :: EffectRow).
Members
  '[Fresh, Reader TyDefCtx, Output (Message ann), Embed IO] r =>
Name ATerm -> [Type] -> NonEmpty [APattern] -> Sem r ()
checkClauses Name ATerm
name [Type]
types NonEmpty [APattern]
pats = do
  [TypedVar]
args <- [Type] -> Sem r [TypedVar]
forall (r :: EffectRow).
Member Fresh r =>
[Type] -> Sem r [TypedVar]
TI.newVars [Type]
types
  [Gdt]
cl <- (Int -> [APattern] -> Sem r Gdt)
-> [Int] -> [[APattern]] -> Sem r [Gdt]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ([TypedVar] -> Int -> [APattern] -> Sem r Gdt
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
[TypedVar] -> Int -> [APattern] -> Sem r Gdt
desugarClause [TypedVar]
args) [Int
1 ..] (NonEmpty [APattern] -> [[APattern]]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty [APattern]
pats)
  let gdt :: Gdt
gdt = (Gdt -> Gdt -> Gdt) -> [Gdt] -> Gdt
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Gdt -> Gdt -> Gdt
Branch [Gdt]
cl

  let argsNref :: [a]
argsNref = []
  ([NormRefType]
normalizedNrefs, Ant
_) <- [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
ua [NormRefType
forall a. [a]
argsNref] Gdt
gdt

  [[ExamplePat]]
examples <- [NormRefType] -> [TypedVar] -> Sem r [[ExamplePat]]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> [TypedVar] -> Sem r [[ExamplePat]]
findPosExamples [NormRefType]
normalizedNrefs [TypedVar]
args

  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([[ExamplePat]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[ExamplePat]]
examples) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ do
    let prettyExampleArgs :: [ExamplePat] -> Sem r (Doc ann)
prettyExampleArgs [ExamplePat]
exArgs =
          [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
DSL.hcat ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ (ExamplePat -> Sem r (Doc ann))
-> [ExamplePat] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map ExamplePat -> Sem r (Doc ann)
forall (r :: EffectRow) ann. ExamplePat -> Sem r (Doc ann)
prettyPrintExample [ExamplePat]
exArgs

    let prettyExampleLine :: Sem r (Doc ann) -> Sem r (Doc ann)
prettyExampleLine Sem r (Doc ann)
prettyArgs =
          String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
DSL.text (Name ATerm -> String
forall a. Show a => a -> String
show Name ATerm
name) Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
DSL.<> Sem r (Doc ann)
prettyArgs Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
DSL.<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
DSL.text String
"= ..."

    let prettyExamples :: Sem r (Doc ann)
prettyExamples =
          [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
DSL.vcat ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$ ([ExamplePat] -> Sem r (Doc ann))
-> [[ExamplePat]] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map (Sem r (Doc ann) -> Sem r (Doc ann)
prettyExampleLine (Sem r (Doc ann) -> Sem r (Doc ann))
-> ([ExamplePat] -> Sem r (Doc ann))
-> [ExamplePat]
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ExamplePat] -> Sem r (Doc ann)
forall {r :: EffectRow} {ann}. [ExamplePat] -> Sem r (Doc ann)
prettyExampleArgs) [[ExamplePat]]
examples

    Sem r (Doc ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
warn (Sem r (Doc ann) -> Sem r ()) -> Sem r (Doc ann) -> Sem r ()
forall a b. (a -> b) -> a -> b
$
      String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
DSL.text String
"Warning: the function"
        Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
DSL.<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
DSL.text (Name ATerm -> String
forall a. Show a => a -> String
show Name ATerm
name)
        Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
DSL.<+> String -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => String -> m (Doc ann)
DSL.text String
"is undefined for some inputs. For example:"
        Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
DSL.$+$ Sem r (Doc ann)
prettyExamples

prettyPrintExample :: ExamplePat -> Sem r (Doc ann)
prettyPrintExample :: forall (r :: EffectRow) ann. ExamplePat -> Sem r (Doc ann)
prettyPrintExample = Sem (LFresh : r) (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) a. Sem (LFresh : r) a -> Sem r a
runLFresh (Sem (LFresh : r) (Doc ann) -> Sem r (Doc ann))
-> (ExamplePat -> Sem (LFresh : r) (Doc ann))
-> ExamplePat
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PA
-> Sem (Reader PA : LFresh : r) (Doc ann)
-> Sem (LFresh : r) (Doc ann)
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA (Sem (Reader PA : LFresh : r) (Doc ann)
 -> Sem (LFresh : r) (Doc ann))
-> (ExamplePat -> Sem (Reader PA : LFresh : r) (Doc ann))
-> ExamplePat
-> Sem (LFresh : r) (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Sem (Reader PA : LFresh : r) (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern -> Sem r (Doc ann)
prettyPrintPattern (Pattern -> Sem (Reader PA : LFresh : r) (Doc ann))
-> (ExamplePat -> Pattern)
-> ExamplePat
-> Sem (Reader PA : LFresh : r) (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExamplePat -> Pattern
exampleToDiscoPattern

prettyPrintPattern :: (Members '[Reader PA, LFresh] r) => Pattern -> Sem r (Doc ann)
prettyPrintPattern :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Pattern -> Sem r (Doc ann)
prettyPrintPattern = PA -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Member (Reader PA) r =>
PA -> Sem r (Doc ann) -> Sem r (Doc ann)
withPA PA
funPA (Sem r (Doc ann) -> Sem r (Doc ann))
-> (Pattern -> Sem r (Doc ann)) -> Pattern -> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[LFresh, Reader PA] r =>
Pattern -> Sem r (Doc ann)
prettyPatternP

exampleToDiscoPattern :: ExamplePat -> Pattern
exampleToDiscoPattern :: ExamplePat -> Pattern
exampleToDiscoPattern e :: ExamplePat
e@(ExamplePat TI.DataCon {dcIdent :: DataCon -> Ident
TI.dcIdent = Ident
ident, dcTypes :: DataCon -> [Type]
TI.dcTypes = [Type]
types} [ExamplePat]
args) = case (Ident
ident, [ExamplePat]
args) of
  (Ident
TI.KUnknown, [ExamplePat]
_) -> Pattern
PWild
  (Ident
TI.KUnit, [ExamplePat]
_) -> Pattern
PUnit
  (TI.KBool Bool
b, [ExamplePat]
_) -> Bool -> Pattern
PBool Bool
b
  (TI.KNat Integer
n, [ExamplePat]
_) -> Integer -> Pattern
PNat Integer
n
  (TI.KInt Integer
z, [ExamplePat]
_) ->
    if Integer
z Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
      then Integer -> Pattern
PNat Integer
z
      else Pattern -> Pattern
PNeg (Integer -> Pattern
PNat (Integer -> Integer
forall a. Num a => a -> a
abs Integer
z))
  (Ident
TI.KPair, [ExamplePat]
_) -> [Pattern] -> Pattern
PTup ([Pattern] -> Pattern) -> [Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ (ExamplePat -> Pattern) -> [ExamplePat] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ExamplePat -> Pattern
exampleToDiscoPattern ([ExamplePat] -> [Pattern]) -> [ExamplePat] -> [Pattern]
forall a b. (a -> b) -> a -> b
$ ExamplePat -> [ExamplePat]
resugarPair ExamplePat
e
  (Ident
TI.KCons, [ExamplePat]
_) ->
    if Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
take Int
1 [Type]
types [Type] -> [Type] -> Bool
forall a. Eq a => a -> a -> Bool
== [Type
Ty.TyC]
      then String -> Pattern
PString (String -> Pattern) -> String -> Pattern
forall a b. (a -> b) -> a -> b
$ ExamplePat -> String
resugarString ExamplePat
e
      else [Pattern] -> Pattern
PList ([Pattern] -> Pattern) -> [Pattern] -> Pattern
forall a b. (a -> b) -> a -> b
$ (ExamplePat -> Pattern) -> [ExamplePat] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map ExamplePat -> Pattern
exampleToDiscoPattern ([ExamplePat] -> [Pattern]) -> [ExamplePat] -> [Pattern]
forall a b. (a -> b) -> a -> b
$ ExamplePat -> [ExamplePat]
resugarList ExamplePat
e
  (Ident
TI.KNil, [ExamplePat]
_) -> [Pattern] -> Pattern
PList []
  (TI.KChar Char
c, [ExamplePat]
_) -> Char -> Pattern
PChar Char
c
  (Ident
TI.KLeft, [ExamplePat
l]) -> Side -> Pattern -> Pattern
PInj Side
L (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ ExamplePat -> Pattern
exampleToDiscoPattern ExamplePat
l
  (Ident
TI.KRight, [ExamplePat
r]) -> Side -> Pattern -> Pattern
PInj Side
R (Pattern -> Pattern) -> Pattern -> Pattern
forall a b. (a -> b) -> a -> b
$ ExamplePat -> Pattern
exampleToDiscoPattern ExamplePat
r
  (Ident
TI.KLeft, [ExamplePat]
_) -> String -> Pattern
forall a. HasCallStack => String -> a
error String
"Found KLeft data constructor with 0 or multiple arguments"
  (Ident
TI.KRight, [ExamplePat]
_) -> String -> Pattern
forall a. HasCallStack => String -> a
error String
"Found KRight data constructor with 0 or multiple arguments"

resugarPair :: ExamplePat -> [ExamplePat]
resugarPair :: ExamplePat -> [ExamplePat]
resugarPair e :: ExamplePat
e@(ExamplePat TI.DataCon {dcIdent :: DataCon -> Ident
TI.dcIdent = Ident
ident} [ExamplePat]
args) = case (Ident
ident, [ExamplePat]
args) of
  (Ident
TI.KPair, [ExamplePat
efst, ExamplePat
esnd]) -> ExamplePat
efst ExamplePat -> [ExamplePat] -> [ExamplePat]
forall a. a -> [a] -> [a]
: ExamplePat -> [ExamplePat]
resugarPair ExamplePat
esnd
  (Ident
_, [ExamplePat]
_) -> [ExamplePat
e]

resugarList :: ExamplePat -> [ExamplePat]
resugarList :: ExamplePat -> [ExamplePat]
resugarList (ExamplePat TI.DataCon {dcIdent :: DataCon -> Ident
TI.dcIdent = Ident
ident} [ExamplePat]
args) = case (Ident
ident, [ExamplePat]
args) of
  (Ident
TI.KCons, [ExamplePat
ehead, ExamplePat
etail]) -> ExamplePat
ehead ExamplePat -> [ExamplePat] -> [ExamplePat]
forall a. a -> [a] -> [a]
: ExamplePat -> [ExamplePat]
resugarList ExamplePat
etail
  (Ident
_, [ExamplePat]
_) -> []

resugarString :: ExamplePat -> String
resugarString :: ExamplePat -> String
resugarString (ExamplePat TI.DataCon {dcIdent :: DataCon -> Ident
TI.dcIdent = Ident
ident} [ExamplePat]
args) = case (Ident
ident, [ExamplePat]
args) of
  (Ident
TI.KCons, [ExamplePat
ehead, ExamplePat
etail]) -> ExamplePat -> Char
assumeExampleChar ExamplePat
ehead Char -> String -> String
forall a. a -> [a] -> [a]
: ExamplePat -> String
resugarString ExamplePat
etail
  (Ident
_, [ExamplePat]
_) -> []

assumeExampleChar :: ExamplePat -> Char
assumeExampleChar :: ExamplePat -> Char
assumeExampleChar (ExamplePat TI.DataCon {dcIdent :: DataCon -> Ident
TI.dcIdent = TI.KChar Char
c} [ExamplePat]
_) = Char
c
assumeExampleChar ExamplePat
_ = String -> Char
forall a. HasCallStack => String -> a
error String
"Wrongly assumed that an ExamplePat was a Char"

desugarClause :: (Members '[Fresh, Embed IO] r) => [TI.TypedVar] -> Int -> [APattern] -> Sem r Gdt
desugarClause :: forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
[TypedVar] -> Int -> [APattern] -> Sem r Gdt
desugarClause [TypedVar]
args Int
clauseIdx [APattern]
argsPats = do
  [[Guard]]
guards <- (TypedVar -> APattern -> Sem r [Guard])
-> [TypedVar] -> [APattern] -> Sem r [[Guard]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch [TypedVar]
args [APattern]
argsPats
  Gdt -> Sem r Gdt
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Gdt -> Sem r Gdt) -> Gdt -> Sem r Gdt
forall a b. (a -> b) -> a -> b
$ (Guard -> Gdt -> Gdt) -> Gdt -> [Guard] -> Gdt
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Guard -> Gdt -> Gdt
Guarded (Int -> Gdt
Grhs Int
clauseIdx) ([Guard] -> Gdt) -> [Guard] -> Gdt
forall a b. (a -> b) -> a -> b
$ [[Guard]] -> [Guard]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Guard]]
guards

-- To work with the LYG algorithm, we need to desugar n-tuples to nested pairs
-- Just having a Tuple type with a variable number of arguments breaks.
-- Imagine we have
-- foo (1,2,3) = ...
-- foo (1,(2,n)) = ...
-- if we keep things in our nice "sugared" form, the solver will get confused,
-- and not realize that the last element of the tuple is fully covered by n,
-- because there will be two notions of last element: the last in the triple and
-- the last in the nested pair
desugarTuplePats :: [APattern] -> APattern
desugarTuplePats :: [APattern] -> APattern
desugarTuplePats [] = String -> APattern
forall a. HasCallStack => String -> a
error String
"Found empty tuple, what happened?"
desugarTuplePats [APattern
p] = APattern
p
desugarTuplePats (APattern
pfst : [APattern]
rest) = Type -> [APattern] -> APattern
APTup (APattern -> Type
forall t. HasType t => t -> Type
Ty.getType APattern
pfst Type -> Type -> Type
Ty.:*: APattern -> Type
forall t. HasType t => t -> Type
Ty.getType APattern
psnd) [APattern
pfst, APattern
psnd]
 where
  psnd :: APattern
psnd = [APattern] -> APattern
desugarTuplePats [APattern]
rest

-- | Convert a Disco APattern into a list of Guards which cover that pattern
--
--   These patterns are currently not handled:
--     , APNeg     --still need to handle rational case
--     , APFrac    --required for rationals?
--     algebraic (probably will be eventually replaced anyway):
--     , APAdd
--     , APMul
--     , APSub
--   These (or some updated version of them) may be handled eventually,
--   once updated arithmetic patterns are merged.
--
--   We treat unhandled patterns as if they are exhaustively matched against
--   (aka, they are seen as wildcards by the checker).
--   This necessarily results in some false negatives, but no false positives.
desugarMatch :: (Members '[Fresh, Embed IO] r) => TI.TypedVar -> APattern -> Sem r [Guard]
desugarMatch :: forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
var APattern
pat = case APattern
pat of
  (APTup (Type
ta Ty.:*: Type
tb) [APattern
pfst, APattern
psnd]) -> do
    TypedVar
varFst <- Type -> Sem r TypedVar
forall (r :: EffectRow). Member Fresh r => Type -> Sem r TypedVar
TI.newVar Type
ta
    TypedVar
varSnd <- Type -> Sem r TypedVar
forall (r :: EffectRow). Member Fresh r => Type -> Sem r TypedVar
TI.newVar Type
tb
    [Guard]
guardsFst <- TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
varFst APattern
pfst
    [Guard]
guardsSnd <- TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
varSnd APattern
psnd
    let guardPair :: Guard
guardPair = (TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch (Type -> Type -> DataCon
TI.pair Type
ta Type
tb) [TypedVar
varFst, TypedVar
varSnd])
    [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Guard] -> Sem r [Guard]) -> [Guard] -> Sem r [Guard]
forall a b. (a -> b) -> a -> b
$ [Guard
guardPair] [Guard] -> [Guard] -> [Guard]
forall a. [a] -> [a] -> [a]
++ [Guard]
guardsFst [Guard] -> [Guard] -> [Guard]
forall a. [a] -> [a] -> [a]
++ [Guard]
guardsSnd
  (APTup Type
_ [APattern]
sugary) -> TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
var ([APattern] -> APattern
desugarTuplePats [APattern]
sugary)
  (APCons Type
_ APattern
subHead APattern
subTail) -> do
    let typeHead :: Type
typeHead = APattern -> Type
forall t. HasType t => t -> Type
Ty.getType APattern
subHead
    let typeTail :: Type
typeTail = APattern -> Type
forall t. HasType t => t -> Type
Ty.getType APattern
subTail
    TypedVar
varHead <- Type -> Sem r TypedVar
forall (r :: EffectRow). Member Fresh r => Type -> Sem r TypedVar
TI.newVar Type
typeHead
    TypedVar
varTail <- Type -> Sem r TypedVar
forall (r :: EffectRow). Member Fresh r => Type -> Sem r TypedVar
TI.newVar Type
typeTail
    [Guard]
guardsHead <- TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
varHead APattern
subHead
    [Guard]
guardsTail <- TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
varTail APattern
subTail
    let guardCons :: Guard
guardCons = (TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch (Type -> Type -> DataCon
TI.cons Type
typeHead Type
typeTail) [TypedVar
varHead, TypedVar
varTail])
    [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Guard] -> Sem r [Guard]) -> [Guard] -> Sem r [Guard]
forall a b. (a -> b) -> a -> b
$ [Guard
guardCons] [Guard] -> [Guard] -> [Guard]
forall a. [a] -> [a] -> [a]
++ [Guard]
guardsHead [Guard] -> [Guard] -> [Guard]
forall a. [a] -> [a] -> [a]
++ [Guard]
guardsTail
  -- We have to desugar Lists into Cons and Nils
  (APList Type
_ []) -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch DataCon
TI.nil [])]
  (APList Type
ty (APattern
phead : [APattern]
ptail)) -> do
    -- APCons have the type of the list they are part of
    TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
var (Type -> APattern -> APattern -> APattern
APCons Type
ty APattern
phead (Type -> [APattern] -> APattern
APList Type
ty [APattern]
ptail))
  -- we have to desugar to a list, becuse we can match strings with cons
  (APString String
str) -> do
    let strType :: Type
strType = Type -> Type
Ty.TyList Type
Ty.TyC
    TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
var (Type -> [APattern] -> APattern
APList Type
strType ((Char -> APattern) -> String -> [APattern]
forall a b. (a -> b) -> [a] -> [b]
map Char -> APattern
APChar String
str))
  -- A bit of strangeness is required here because of how patterns work
  (APNat Type
Ty.TyN Integer
nat) -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch (Integer -> DataCon
TI.natural Integer
nat) [])]
  (APNat Type
Ty.TyZ Integer
z) -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch (Integer -> DataCon
TI.integer Integer
z) [])]
  (APNeg Type
Ty.TyZ (APNat Type
Ty.TyN Integer
z)) -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch (Integer -> DataCon
TI.integer (-Integer
z)) [])]
  -- These are more straightforward:
  (APWild Type
_) -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  (APVar Type
ty Name ATerm
name) -> do
    let newAlias :: TypedVar
newAlias = (Name ATerm, Type) -> TypedVar
TI.TypedVar (Name ATerm
name, Type
ty)
    [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
newAlias, TypedVar -> GuardConstraint
GWasOriginally TypedVar
var)]
  APattern
APUnit -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch DataCon
TI.unit [])]
  (APBool Bool
b) -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch (Bool -> DataCon
TI.bool Bool
b) [])]
  (APChar Char
c) -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [(TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch (Char -> DataCon
TI.char Char
c) [])]
  (APInj (Type
tl Ty.:+: Type
tr) Side
side APattern
subPat) -> do
    let dc :: DataCon
dc = case Side
side of
          Side
L -> Type -> DataCon
TI.left Type
tl
          Side
R -> Type -> DataCon
TI.right Type
tr
    TypedVar
newVar <- case Side
side of
      Side
L -> Type -> Sem r TypedVar
forall (r :: EffectRow). Member Fresh r => Type -> Sem r TypedVar
TI.newVar Type
tl
      Side
R -> Type -> Sem r TypedVar
forall (r :: EffectRow). Member Fresh r => Type -> Sem r TypedVar
TI.newVar Type
tr
    [Guard]
guards <- TypedVar -> APattern -> Sem r [Guard]
forall (r :: EffectRow).
Members '[Fresh, Embed IO] r =>
TypedVar -> APattern -> Sem r [Guard]
desugarMatch TypedVar
newVar APattern
subPat
    [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Guard] -> Sem r [Guard]) -> [Guard] -> Sem r [Guard]
forall a b. (a -> b) -> a -> b
$ (TypedVar
var, DataCon -> [TypedVar] -> GuardConstraint
GMatch DataCon
dc [TypedVar
newVar]) Guard -> [Guard] -> [Guard]
forall a. a -> [a] -> [a]
: [Guard]
guards
  APattern
_ -> [Guard] -> Sem r [Guard]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []

data Gdt where
  Grhs :: Int -> Gdt
  Branch :: Gdt -> Gdt -> Gdt
  Guarded :: Guard -> Gdt -> Gdt
  deriving (Int -> Gdt -> String -> String
[Gdt] -> String -> String
Gdt -> String
(Int -> Gdt -> String -> String)
-> (Gdt -> String) -> ([Gdt] -> String -> String) -> Show Gdt
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Gdt -> String -> String
showsPrec :: Int -> Gdt -> String -> String
$cshow :: Gdt -> String
show :: Gdt -> String
$cshowList :: [Gdt] -> String -> String
showList :: [Gdt] -> String -> String
Show, Gdt -> Gdt -> Bool
(Gdt -> Gdt -> Bool) -> (Gdt -> Gdt -> Bool) -> Eq Gdt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Gdt -> Gdt -> Bool
== :: Gdt -> Gdt -> Bool
$c/= :: Gdt -> Gdt -> Bool
/= :: Gdt -> Gdt -> Bool
Eq)

type Guard = (TI.TypedVar, GuardConstraint)

data GuardConstraint where
  GMatch :: TI.DataCon -> [TI.TypedVar] -> GuardConstraint
  GWasOriginally :: TI.TypedVar -> GuardConstraint
  deriving (Int -> GuardConstraint -> String -> String
[GuardConstraint] -> String -> String
GuardConstraint -> String
(Int -> GuardConstraint -> String -> String)
-> (GuardConstraint -> String)
-> ([GuardConstraint] -> String -> String)
-> Show GuardConstraint
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> GuardConstraint -> String -> String
showsPrec :: Int -> GuardConstraint -> String -> String
$cshow :: GuardConstraint -> String
show :: GuardConstraint -> String
$cshowList :: [GuardConstraint] -> String -> String
showList :: [GuardConstraint] -> String -> String
Show, GuardConstraint -> GuardConstraint -> Bool
(GuardConstraint -> GuardConstraint -> Bool)
-> (GuardConstraint -> GuardConstraint -> Bool)
-> Eq GuardConstraint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GuardConstraint -> GuardConstraint -> Bool
== :: GuardConstraint -> GuardConstraint -> Bool
$c/= :: GuardConstraint -> GuardConstraint -> Bool
/= :: GuardConstraint -> GuardConstraint -> Bool
Eq)

newtype Literal = Literal (TI.TypedVar, LitCond)

data LitCond where
  LitMatch :: TI.DataCon -> [TI.TypedVar] -> LitCond
  LitNot :: TI.DataCon -> LitCond
  LitWasOriginally :: TI.TypedVar -> LitCond
  deriving (Int -> LitCond -> String -> String
[LitCond] -> String -> String
LitCond -> String
(Int -> LitCond -> String -> String)
-> (LitCond -> String)
-> ([LitCond] -> String -> String)
-> Show LitCond
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> LitCond -> String -> String
showsPrec :: Int -> LitCond -> String -> String
$cshow :: LitCond -> String
show :: LitCond -> String
$cshowList :: [LitCond] -> String -> String
showList :: [LitCond] -> String -> String
Show, LitCond -> LitCond -> Bool
(LitCond -> LitCond -> Bool)
-> (LitCond -> LitCond -> Bool) -> Eq LitCond
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LitCond -> LitCond -> Bool
== :: LitCond -> LitCond -> Bool
$c/= :: LitCond -> LitCond -> Bool
/= :: LitCond -> LitCond -> Bool
Eq, Eq LitCond
Eq LitCond =>
(LitCond -> LitCond -> Ordering)
-> (LitCond -> LitCond -> Bool)
-> (LitCond -> LitCond -> Bool)
-> (LitCond -> LitCond -> Bool)
-> (LitCond -> LitCond -> Bool)
-> (LitCond -> LitCond -> LitCond)
-> (LitCond -> LitCond -> LitCond)
-> Ord LitCond
LitCond -> LitCond -> Bool
LitCond -> LitCond -> Ordering
LitCond -> LitCond -> LitCond
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LitCond -> LitCond -> Ordering
compare :: LitCond -> LitCond -> Ordering
$c< :: LitCond -> LitCond -> Bool
< :: LitCond -> LitCond -> Bool
$c<= :: LitCond -> LitCond -> Bool
<= :: LitCond -> LitCond -> Bool
$c> :: LitCond -> LitCond -> Bool
> :: LitCond -> LitCond -> Bool
$c>= :: LitCond -> LitCond -> Bool
>= :: LitCond -> LitCond -> Bool
$cmax :: LitCond -> LitCond -> LitCond
max :: LitCond -> LitCond -> LitCond
$cmin :: LitCond -> LitCond -> LitCond
min :: LitCond -> LitCond -> LitCond
Ord)

data Ant where
  AGrhs :: [C.NormRefType] -> Int -> Ant
  ABranch :: Ant -> Ant -> Ant
  deriving (Int -> Ant -> String -> String
[Ant] -> String -> String
Ant -> String
(Int -> Ant -> String -> String)
-> (Ant -> String) -> ([Ant] -> String -> String) -> Show Ant
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Ant -> String -> String
showsPrec :: Int -> Ant -> String -> String
$cshow :: Ant -> String
show :: Ant -> String
$cshowList :: [Ant] -> String -> String
showList :: [Ant] -> String -> String
Show)

ua :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> Gdt -> Sem r ([C.NormRefType], Ant)
ua :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
ua [NormRefType]
nrefs Gdt
gdt = case Gdt
gdt of
  Grhs Int
k -> ([NormRefType], Ant) -> Sem r ([NormRefType], Ant)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [NormRefType] -> Int -> Ant
AGrhs [NormRefType]
nrefs Int
k)
  Branch Gdt
t1 Gdt
t2 -> do
    ([NormRefType]
n1, Ant
u1) <- [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
ua [NormRefType]
nrefs Gdt
t1
    ([NormRefType]
n2, Ant
u2) <- [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
ua [NormRefType]
n1 Gdt
t2
    ([NormRefType], Ant) -> Sem r ([NormRefType], Ant)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NormRefType]
n2, Ant -> Ant -> Ant
ABranch Ant
u1 Ant
u2)
  Guarded (TypedVar
y, GWasOriginally TypedVar
x) Gdt
t -> do
    [NormRefType]
n <- [NormRefType] -> Literal -> Sem r [NormRefType]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Literal -> Sem r [NormRefType]
addLitMulti [NormRefType]
nrefs (Literal -> Sem r [NormRefType]) -> Literal -> Sem r [NormRefType]
forall a b. (a -> b) -> a -> b
$ (TypedVar, LitCond) -> Literal
Literal (TypedVar
y, TypedVar -> LitCond
LitWasOriginally TypedVar
x)
    [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
ua [NormRefType]
n Gdt
t
  Guarded (TypedVar
x, GMatch DataCon
dc [TypedVar]
args) Gdt
t -> do
    [NormRefType]
n <- [NormRefType] -> Literal -> Sem r [NormRefType]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Literal -> Sem r [NormRefType]
addLitMulti [NormRefType]
nrefs (Literal -> Sem r [NormRefType]) -> Literal -> Sem r [NormRefType]
forall a b. (a -> b) -> a -> b
$ (TypedVar, LitCond) -> Literal
Literal (TypedVar
x, DataCon -> [TypedVar] -> LitCond
LitMatch DataCon
dc [TypedVar]
args)
    ([NormRefType]
n', Ant
u) <- [NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Gdt -> Sem r ([NormRefType], Ant)
ua [NormRefType]
n Gdt
t
    [NormRefType]
n'' <- [NormRefType] -> Literal -> Sem r [NormRefType]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Literal -> Sem r [NormRefType]
addLitMulti [NormRefType]
nrefs (Literal -> Sem r [NormRefType]) -> Literal -> Sem r [NormRefType]
forall a b. (a -> b) -> a -> b
$ (TypedVar, LitCond) -> Literal
Literal (TypedVar
x, DataCon -> LitCond
LitNot DataCon
dc)
    ([NormRefType], Ant) -> Sem r ([NormRefType], Ant)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NormRefType]
n'' [NormRefType] -> [NormRefType] -> [NormRefType]
forall a. [a] -> [a] -> [a]
++ [NormRefType]
n', Ant
u)

addLitMulti :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> Literal -> Sem r [C.NormRefType]
addLitMulti :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Literal -> Sem r [NormRefType]
addLitMulti [] Literal
_ = [NormRefType] -> Sem r [NormRefType]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return []
addLitMulti (NormRefType
n : [NormRefType]
ns) Literal
lit = do
  Maybe NormRefType
r <- MaybeT (Sem r) NormRefType -> Sem r (Maybe NormRefType)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (Sem r) NormRefType -> Sem r (Maybe NormRefType))
-> MaybeT (Sem r) NormRefType -> Sem r (Maybe NormRefType)
forall a b. (a -> b) -> a -> b
$ NormRefType -> Literal -> MaybeT (Sem r) NormRefType
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> Literal -> MaybeT (Sem r) NormRefType
addLiteral NormRefType
n Literal
lit
  case Maybe NormRefType
r of
    Maybe NormRefType
Nothing -> [NormRefType] -> Literal -> Sem r [NormRefType]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Literal -> Sem r [NormRefType]
addLitMulti [NormRefType]
ns Literal
lit
    Just NormRefType
cfs -> do
      [NormRefType]
ns' <- [NormRefType] -> Literal -> Sem r [NormRefType]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> Literal -> Sem r [NormRefType]
addLitMulti [NormRefType]
ns Literal
lit
      [NormRefType] -> Sem r [NormRefType]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([NormRefType] -> Sem r [NormRefType])
-> [NormRefType] -> Sem r [NormRefType]
forall a b. (a -> b) -> a -> b
$ NormRefType
cfs NormRefType -> [NormRefType] -> [NormRefType]
forall a. a -> [a] -> [a]
: [NormRefType]
ns'

addLiteral :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> Literal -> MaybeT (Sem r) C.NormRefType
addLiteral :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> Literal -> MaybeT (Sem r) NormRefType
addLiteral NormRefType
constraints (Literal (TypedVar
x, LitCond
c)) = case LitCond
c of
  LitWasOriginally TypedVar
z ->
    NormRefType
constraints NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
`C.addConstraint` (TypedVar
x, TypedVar -> Constraint
C.CWasOriginally TypedVar
z)
  LitMatch DataCon
dc [TypedVar]
args ->
    NormRefType
constraints NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
`C.addConstraint` (TypedVar
x, DataCon -> [TypedVar] -> Constraint
C.CMatch DataCon
dc [TypedVar]
args)
  LitNot DataCon
dc ->
    NormRefType
constraints NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
`C.addConstraint` (TypedVar
x, DataCon -> Constraint
C.CNot DataCon
dc)

data InhabPat where
  IPIs :: TI.DataCon -> [InhabPat] -> InhabPat
  IPNot :: [TI.DataCon] -> InhabPat
  deriving (Int -> InhabPat -> String -> String
[InhabPat] -> String -> String
InhabPat -> String
(Int -> InhabPat -> String -> String)
-> (InhabPat -> String)
-> ([InhabPat] -> String -> String)
-> Show InhabPat
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> InhabPat -> String -> String
showsPrec :: Int -> InhabPat -> String -> String
$cshow :: InhabPat -> String
show :: InhabPat -> String
$cshowList :: [InhabPat] -> String -> String
showList :: [InhabPat] -> String -> String
Show, InhabPat -> InhabPat -> Bool
(InhabPat -> InhabPat -> Bool)
-> (InhabPat -> InhabPat -> Bool) -> Eq InhabPat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InhabPat -> InhabPat -> Bool
== :: InhabPat -> InhabPat -> Bool
$c/= :: InhabPat -> InhabPat -> Bool
/= :: InhabPat -> InhabPat -> Bool
Eq, Eq InhabPat
Eq InhabPat =>
(InhabPat -> InhabPat -> Ordering)
-> (InhabPat -> InhabPat -> Bool)
-> (InhabPat -> InhabPat -> Bool)
-> (InhabPat -> InhabPat -> Bool)
-> (InhabPat -> InhabPat -> Bool)
-> (InhabPat -> InhabPat -> InhabPat)
-> (InhabPat -> InhabPat -> InhabPat)
-> Ord InhabPat
InhabPat -> InhabPat -> Bool
InhabPat -> InhabPat -> Ordering
InhabPat -> InhabPat -> InhabPat
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: InhabPat -> InhabPat -> Ordering
compare :: InhabPat -> InhabPat -> Ordering
$c< :: InhabPat -> InhabPat -> Bool
< :: InhabPat -> InhabPat -> Bool
$c<= :: InhabPat -> InhabPat -> Bool
<= :: InhabPat -> InhabPat -> Bool
$c> :: InhabPat -> InhabPat -> Bool
> :: InhabPat -> InhabPat -> Bool
$c>= :: InhabPat -> InhabPat -> Bool
>= :: InhabPat -> InhabPat -> Bool
$cmax :: InhabPat -> InhabPat -> InhabPat
max :: InhabPat -> InhabPat -> InhabPat
$cmin :: InhabPat -> InhabPat -> InhabPat
min :: InhabPat -> InhabPat -> InhabPat
Ord)

-- Sanity check: are we giving the dataconstructor the
-- correct number of arguments?
mkIPMatch :: TI.DataCon -> [InhabPat] -> InhabPat
mkIPMatch :: DataCon -> [InhabPat] -> InhabPat
mkIPMatch DataCon
k [InhabPat]
pats =
  if [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataCon -> [Type]
TI.dcTypes DataCon
k) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [InhabPat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [InhabPat]
pats
    then String -> InhabPat
forall a. HasCallStack => String -> a
error (String -> InhabPat) -> String -> InhabPat
forall a b. (a -> b) -> a -> b
$ String
"Wrong number of DataCon args" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (DataCon, [InhabPat]) -> String
forall a. Show a => a -> String
show (DataCon
k, [InhabPat]
pats)
    else DataCon -> [InhabPat] -> InhabPat
IPIs DataCon
k [InhabPat]
pats

findInhabitants :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat])
findInhabitants :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> [TypedVar] -> Sem r (Possibilities [InhabPat])
findInhabitants [NormRefType]
nrefs [TypedVar]
args = do
  [Possibilities [InhabPat]]
a <- [NormRefType]
-> (NormRefType -> Sem r (Possibilities [InhabPat]))
-> Sem r [Possibilities [InhabPat]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NormRefType]
nrefs (NormRefType -> [TypedVar] -> Sem r (Possibilities [InhabPat])
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> [TypedVar] -> Sem r (Possibilities [InhabPat])
`findAllForNref` [TypedVar]
args)
  Possibilities [InhabPat] -> Sem r (Possibilities [InhabPat])
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Possibilities [InhabPat] -> Sem r (Possibilities [InhabPat]))
-> Possibilities [InhabPat] -> Sem r (Possibilities [InhabPat])
forall a b. (a -> b) -> a -> b
$ [Possibilities [InhabPat]] -> Possibilities [InhabPat]
forall a. [Possibilities a] -> Possibilities a
Poss.anyOf [Possibilities [InhabPat]]
a

findAllForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [InhabPat])
findAllForNref :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> [TypedVar] -> Sem r (Possibilities [InhabPat])
findAllForNref NormRefType
nref [TypedVar]
args = do
  [Possibilities InhabPat]
argPats <- [TypedVar]
-> (TypedVar -> Sem r (Possibilities InhabPat))
-> Sem r [Possibilities InhabPat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TypedVar]
args (TypedVar -> NormRefType -> Sem r (Possibilities InhabPat)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
TypedVar -> NormRefType -> Sem r (Possibilities InhabPat)
`findVarInhabitants` NormRefType
nref)
  Possibilities [InhabPat] -> Sem r (Possibilities [InhabPat])
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Possibilities [InhabPat] -> Sem r (Possibilities [InhabPat]))
-> Possibilities [InhabPat] -> Sem r (Possibilities [InhabPat])
forall a b. (a -> b) -> a -> b
$ [Possibilities InhabPat] -> Possibilities [InhabPat]
forall a. [Possibilities a] -> Possibilities [a]
Poss.allCombinations [Possibilities InhabPat]
argPats

findVarInhabitants :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities InhabPat)
findVarInhabitants :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
TypedVar -> NormRefType -> Sem r (Possibilities InhabPat)
findVarInhabitants TypedVar
var NormRefType
cns =
  case Maybe (DataCon, [TypedVar])
posMatch of
    Just (DataCon
k, [TypedVar]
args) -> do
      Possibilities [InhabPat]
argPossibilities <- NormRefType -> [TypedVar] -> Sem r (Possibilities [InhabPat])
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> [TypedVar] -> Sem r (Possibilities [InhabPat])
findAllForNref NormRefType
cns [TypedVar]
args
      Possibilities InhabPat -> Sem r (Possibilities InhabPat)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataCon -> [InhabPat] -> InhabPat
mkIPMatch DataCon
k ([InhabPat] -> InhabPat)
-> Possibilities [InhabPat] -> Possibilities InhabPat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Possibilities [InhabPat]
argPossibilities)
    Maybe (DataCon, [TypedVar])
Nothing -> case [DataCon] -> [DataCon]
forall a. Eq a => [a] -> [a]
nub [DataCon]
negMatches of
      [] -> InhabPat -> Sem r (Possibilities InhabPat)
forall (m :: * -> *) a. Monad m => a -> m (Possibilities a)
Poss.retSingle (InhabPat -> Sem r (Possibilities InhabPat))
-> InhabPat -> Sem r (Possibilities InhabPat)
forall a b. (a -> b) -> a -> b
$ [DataCon] -> InhabPat
IPNot []
      [DataCon]
neg -> do
        TyDefCtx
tyCtx <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @Ty.TyDefCtx
        case Type -> TyDefCtx -> Constructors
TI.tyDataCons (TypedVar -> Type
TI.getType TypedVar
var) TyDefCtx
tyCtx of
          TI.Infinite [DataCon]
_ -> InhabPat -> Sem r (Possibilities InhabPat)
forall (m :: * -> *) a. Monad m => a -> m (Possibilities a)
Poss.retSingle (InhabPat -> Sem r (Possibilities InhabPat))
-> InhabPat -> Sem r (Possibilities InhabPat)
forall a b. (a -> b) -> a -> b
$ [DataCon] -> InhabPat
IPNot [DataCon]
neg
          TI.Finite [DataCon]
dcs ->
            do
              let tryAddDc :: DataCon -> Sem r (Maybe NormRefType)
tryAddDc DataCon
dc = do
                    [TypedVar]
vars <- [Type] -> Sem r [TypedVar]
forall (r :: EffectRow).
Member Fresh r =>
[Type] -> Sem r [TypedVar]
TI.newVars (DataCon -> [Type]
TI.dcTypes DataCon
dc)
                    MaybeT (Sem r) NormRefType -> Sem r (Maybe NormRefType)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (NormRefType
cns NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
`C.addConstraint` (TypedVar
var, DataCon -> [TypedVar] -> Constraint
C.CMatch DataCon
dc [TypedVar]
vars))

              -- Try to add a positive constraint for each data constructor
              -- to the current nref
              -- If any of these additions succeed, save that nref,
              -- it now has positive information
              [NormRefType]
posNrefs <- [Maybe NormRefType] -> [NormRefType]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe NormRefType] -> [NormRefType])
-> Sem r [Maybe NormRefType] -> Sem r [NormRefType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
-> (DataCon -> Sem r (Maybe NormRefType))
-> Sem r [Maybe NormRefType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DataCon]
dcs DataCon -> Sem r (Maybe NormRefType)
tryAddDc

              if [NormRefType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NormRefType]
posNrefs
                then InhabPat -> Sem r (Possibilities InhabPat)
forall (m :: * -> *) a. Monad m => a -> m (Possibilities a)
Poss.retSingle (InhabPat -> Sem r (Possibilities InhabPat))
-> InhabPat -> Sem r (Possibilities InhabPat)
forall a b. (a -> b) -> a -> b
$ [DataCon] -> InhabPat
IPNot []
                else [Possibilities InhabPat] -> Possibilities InhabPat
forall a. [Possibilities a] -> Possibilities a
Poss.anyOf ([Possibilities InhabPat] -> Possibilities InhabPat)
-> Sem r [Possibilities InhabPat] -> Sem r (Possibilities InhabPat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NormRefType]
-> (NormRefType -> Sem r (Possibilities InhabPat))
-> Sem r [Possibilities InhabPat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NormRefType]
posNrefs (TypedVar -> NormRefType -> Sem r (Possibilities InhabPat)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
TypedVar -> NormRefType -> Sem r (Possibilities InhabPat)
findVarInhabitants TypedVar
var)
 where
  constraintsOnX :: [Constraint]
constraintsOnX = TypedVar -> NormRefType -> [Constraint]
C.onVar TypedVar
var NormRefType
cns
  posMatch :: Maybe (DataCon, [TypedVar])
posMatch = [Constraint] -> Maybe (DataCon, [TypedVar])
C.posMatch [Constraint]
constraintsOnX
  negMatches :: [DataCon]
negMatches = [Constraint] -> [DataCon]
C.negMatches [Constraint]
constraintsOnX

findRedundant :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Ant -> [TI.TypedVar] -> Sem r [Int]
findRedundant :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Ant -> [TypedVar] -> Sem r [Int]
findRedundant Ant
ant [TypedVar]
args = case Ant
ant of
  AGrhs [NormRefType]
ref Int
i -> do
    Bool
uninhabited <- Possibilities [InhabPat] -> Bool
forall a. Possibilities a -> Bool
Poss.none (Possibilities [InhabPat] -> Bool)
-> Sem r (Possibilities [InhabPat]) -> Sem r Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NormRefType] -> [TypedVar] -> Sem r (Possibilities [InhabPat])
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> [TypedVar] -> Sem r (Possibilities [InhabPat])
findInhabitants [NormRefType]
ref [TypedVar]
args
    [Int] -> Sem r [Int]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return [Int
i | Bool
uninhabited]
  ABranch Ant
a1 Ant
a2 -> [Int] -> [Int] -> [Int]
forall a. Monoid a => a -> a -> a
mappend ([Int] -> [Int] -> [Int]) -> Sem r [Int] -> Sem r ([Int] -> [Int])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ant -> [TypedVar] -> Sem r [Int]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Ant -> [TypedVar] -> Sem r [Int]
findRedundant Ant
a1 [TypedVar]
args Sem r ([Int] -> [Int]) -> Sem r [Int] -> Sem r [Int]
forall a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ant -> [TypedVar] -> Sem r [Int]
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Ant -> [TypedVar] -> Sem r [Int]
findRedundant Ant
a2 [TypedVar]
args

data ExamplePat where
  ExamplePat :: TI.DataCon -> [ExamplePat] -> ExamplePat
  deriving (Int -> ExamplePat -> String -> String
[ExamplePat] -> String -> String
ExamplePat -> String
(Int -> ExamplePat -> String -> String)
-> (ExamplePat -> String)
-> ([ExamplePat] -> String -> String)
-> Show ExamplePat
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ExamplePat -> String -> String
showsPrec :: Int -> ExamplePat -> String -> String
$cshow :: ExamplePat -> String
show :: ExamplePat -> String
$cshowList :: [ExamplePat] -> String -> String
showList :: [ExamplePat] -> String -> String
Show)

-- | Less general version of the above inhabitant finding function
--   returns a maximum of 3 possible args lists that haven't been matched against,
--   as to not overwhelm new users of the language.
--   This is essentially a DFS, and it has a bad habit of
--   trying to build infinite lists whenever it can, so we give it a max depth of 32
--   If we reach 32 levels of nested dataconstructors in this language,
--   it is pretty safe to assume we were chasing after an infinite structure
findPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => [C.NormRefType] -> [TI.TypedVar] -> Sem r [[ExamplePat]]
findPosExamples :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
[NormRefType] -> [TypedVar] -> Sem r [[ExamplePat]]
findPosExamples [NormRefType]
nrefs [TypedVar]
args = do
  [Possibilities [ExamplePat]]
a <- [NormRefType]
-> (NormRefType -> Sem r (Possibilities [ExamplePat]))
-> Sem r [Possibilities [ExamplePat]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NormRefType]
nrefs (\NormRefType
nref -> Int
-> NormRefType -> [TypedVar] -> Sem r (Possibilities [ExamplePat])
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Int
-> NormRefType -> [TypedVar] -> Sem r (Possibilities [ExamplePat])
findAllPosForNref Int
32 NormRefType
nref [TypedVar]
args)
  [[ExamplePat]] -> Sem r [[ExamplePat]]
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[ExamplePat]] -> Sem r [[ExamplePat]])
-> [[ExamplePat]] -> Sem r [[ExamplePat]]
forall a b. (a -> b) -> a -> b
$ Int -> [[ExamplePat]] -> [[ExamplePat]]
forall a. Int -> [a] -> [a]
take Int
3 ([[ExamplePat]] -> [[ExamplePat]])
-> [[ExamplePat]] -> [[ExamplePat]]
forall a b. (a -> b) -> a -> b
$ Possibilities [ExamplePat] -> [[ExamplePat]]
forall a. Possibilities a -> [a]
Poss.getPossibilities (Possibilities [ExamplePat] -> [[ExamplePat]])
-> Possibilities [ExamplePat] -> [[ExamplePat]]
forall a b. (a -> b) -> a -> b
$ [Possibilities [ExamplePat]] -> Possibilities [ExamplePat]
forall a. [Possibilities a] -> Possibilities a
Poss.anyOf [Possibilities [ExamplePat]]
a

findAllPosForNref :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> C.NormRefType -> [TI.TypedVar] -> Sem r (Poss.Possibilities [ExamplePat])
findAllPosForNref :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Int
-> NormRefType -> [TypedVar] -> Sem r (Possibilities [ExamplePat])
findAllPosForNref Int
fuel NormRefType
nref [TypedVar]
args = do
  [Possibilities ExamplePat]
argPats <- [TypedVar]
-> (TypedVar -> Sem r (Possibilities ExamplePat))
-> Sem r [Possibilities ExamplePat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [TypedVar]
args (\TypedVar
arg -> Int -> TypedVar -> NormRefType -> Sem r (Possibilities ExamplePat)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Int -> TypedVar -> NormRefType -> Sem r (Possibilities ExamplePat)
findVarPosExamples (Int
fuel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TypedVar
arg NormRefType
nref)
  Possibilities [ExamplePat] -> Sem r (Possibilities [ExamplePat])
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (Possibilities [ExamplePat] -> Sem r (Possibilities [ExamplePat]))
-> Possibilities [ExamplePat] -> Sem r (Possibilities [ExamplePat])
forall a b. (a -> b) -> a -> b
$ [Possibilities ExamplePat] -> Possibilities [ExamplePat]
forall a. [Possibilities a] -> Possibilities [a]
Poss.allCombinations [Possibilities ExamplePat]
argPats

findVarPosExamples :: (Members '[Fresh, Reader Ty.TyDefCtx] r) => Int -> TI.TypedVar -> C.NormRefType -> Sem r (Poss.Possibilities ExamplePat)
findVarPosExamples :: forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Int -> TypedVar -> NormRefType -> Sem r (Possibilities ExamplePat)
findVarPosExamples Int
fuel TypedVar
var NormRefType
cns =
  if Int
fuel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    then Possibilities ExamplePat -> Sem r (Possibilities ExamplePat)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Possibilities ExamplePat
forall a. Monoid a => a
mempty
    else case Maybe (DataCon, [TypedVar])
posMatch of
      Just (DataCon
k, [TypedVar]
args) -> do
        Possibilities [ExamplePat]
argPossibilities <- Int
-> NormRefType -> [TypedVar] -> Sem r (Possibilities [ExamplePat])
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Int
-> NormRefType -> [TypedVar] -> Sem r (Possibilities [ExamplePat])
findAllPosForNref (Int
fuel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) NormRefType
cns [TypedVar]
args
        Possibilities ExamplePat -> Sem r (Possibilities ExamplePat)
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (DataCon -> [ExamplePat] -> ExamplePat
mkExampleMatch DataCon
k ([ExamplePat] -> ExamplePat)
-> Possibilities [ExamplePat] -> Possibilities ExamplePat
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Possibilities [ExamplePat]
argPossibilities)
      Maybe (DataCon, [TypedVar])
Nothing -> do
        TyDefCtx
tyCtx <- forall i (r :: EffectRow). Member (Reader i) r => Sem r i
ask @Ty.TyDefCtx
        let dcs :: [DataCon]
dcs = Type -> TyDefCtx -> [DataCon] -> [DataCon]
getPosFrom (TypedVar -> Type
TI.getType TypedVar
var) TyDefCtx
tyCtx [DataCon]
negMatches
        let tryAddDc :: DataCon -> Sem r (Maybe NormRefType)
tryAddDc DataCon
dc = do
              [TypedVar]
vars <- [Type] -> Sem r [TypedVar]
forall (r :: EffectRow).
Member Fresh r =>
[Type] -> Sem r [TypedVar]
TI.newVars (DataCon -> [Type]
TI.dcTypes DataCon
dc)
              MaybeT (Sem r) NormRefType -> Sem r (Maybe NormRefType)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (NormRefType
cns NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
NormRefType -> (TypedVar, Constraint) -> MaybeT (Sem r) NormRefType
`C.addConstraint` (TypedVar
var, DataCon -> [TypedVar] -> Constraint
C.CMatch DataCon
dc [TypedVar]
vars))
        -- Try to add a positive constraint for each data constructor
        -- to the current nref
        -- If any of these additions succeed, save that nref,
        -- it now has positive information
        [NormRefType]
posNrefs <- [Maybe NormRefType] -> [NormRefType]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe NormRefType] -> [NormRefType])
-> Sem r [Maybe NormRefType] -> Sem r [NormRefType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCon]
-> (DataCon -> Sem r (Maybe NormRefType))
-> Sem r [Maybe NormRefType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DataCon]
dcs DataCon -> Sem r (Maybe NormRefType)
tryAddDc

        [Possibilities ExamplePat] -> Possibilities ExamplePat
forall a. [Possibilities a] -> Possibilities a
Poss.anyOf ([Possibilities ExamplePat] -> Possibilities ExamplePat)
-> Sem r [Possibilities ExamplePat]
-> Sem r (Possibilities ExamplePat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NormRefType]
-> (NormRefType -> Sem r (Possibilities ExamplePat))
-> Sem r [Possibilities ExamplePat]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [NormRefType]
posNrefs (Int -> TypedVar -> NormRefType -> Sem r (Possibilities ExamplePat)
forall (r :: EffectRow).
Members '[Fresh, Reader TyDefCtx] r =>
Int -> TypedVar -> NormRefType -> Sem r (Possibilities ExamplePat)
findVarPosExamples (Int
fuel Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TypedVar
var)
 where
  constraintsOnX :: [Constraint]
constraintsOnX = TypedVar -> NormRefType -> [Constraint]
C.onVar TypedVar
var NormRefType
cns
  posMatch :: Maybe (DataCon, [TypedVar])
posMatch = [Constraint] -> Maybe (DataCon, [TypedVar])
C.posMatch [Constraint]
constraintsOnX
  negMatches :: [DataCon]
negMatches = [Constraint] -> [DataCon]
C.negMatches [Constraint]
constraintsOnX

getPosFrom :: Ty.Type -> Ty.TyDefCtx -> [TI.DataCon] -> [TI.DataCon]
getPosFrom :: Type -> TyDefCtx -> [DataCon] -> [DataCon]
getPosFrom Type
ty TyDefCtx
ctx [DataCon]
neg = Int -> [DataCon] -> [DataCon]
forall a. Int -> [a] -> [a]
take Int
3 ([DataCon] -> [DataCon]) -> [DataCon] -> [DataCon]
forall a b. (a -> b) -> a -> b
$ (DataCon -> Bool) -> [DataCon] -> [DataCon]
forall a. (a -> Bool) -> [a] -> [a]
filter (DataCon -> [DataCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [DataCon]
neg) [DataCon]
dcs
 where
  dcs :: [DataCon]
dcs = case Type -> TyDefCtx -> Constructors
TI.tyDataCons Type
ty TyDefCtx
ctx of
    TI.Finite [DataCon]
dcs' -> [DataCon]
dcs'
    TI.Infinite [DataCon]
dcs' -> [DataCon]
dcs'

mkExampleMatch :: TI.DataCon -> [ExamplePat] -> ExamplePat
mkExampleMatch :: DataCon -> [ExamplePat] -> ExamplePat
mkExampleMatch DataCon
k [ExamplePat]
pats =
  if [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataCon -> [Type]
TI.dcTypes DataCon
k) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [ExamplePat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExamplePat]
pats
    then String -> ExamplePat
forall a. HasCallStack => String -> a
error (String -> ExamplePat) -> String -> ExamplePat
forall a b. (a -> b) -> a -> b
$ String
"Wrong number of DataCon args" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (DataCon, [ExamplePat]) -> String
forall a. Show a => a -> String
show (DataCon
k, [ExamplePat]
pats)
    else DataCon -> [ExamplePat] -> ExamplePat
ExamplePat DataCon
k [ExamplePat]
pats