-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.SCase
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Add support for symbolic case expressions. Constructed with the help of ChatGPT,
-- which was remarkably good at giving me the basic structure.
--
-- Provides a quasiquoter  `[sCase|Expr expr of ... |]` for symbolic cases
-- where @Expr@ is the underlying type.
--
-- Also provides `[pCase|Expr expr of ... |]` for proof case-splits.
-----------------------------------------------------------------------------

{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE TemplateHaskellQuotes #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SCase (sCase, pCase) where

import Language.Haskell.TH
import Language.Haskell.TH.Quote
import qualified Language.Haskell.Meta.Parse            as Meta
import qualified Language.Haskell.Meta.Syntax.Translate as Meta

import qualified Language.Haskell.Exts as E

import Control.Monad (unless, when, zipWithM)

import Data.SBV.Client (getConstructors)
import Data.SBV.Core.Model (ite, sym)
import Data.SBV.Core.Data  (sTrue, sNot, (.&&), (.||), (.==), literal)

import Data.Char  (isSpace, isDigit)
import Data.List  (intercalate)
import Data.Maybe (isJust, fromMaybe)

import Prelude hiding (fail)
import qualified Prelude as P(fail)

import Data.Generics
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.Set (Set)

import System.FilePath

-- | TH parse trees don't have location. Let's have a simple mechanism to keep track of them for our use case
data Offset = Unknown | OffBy Int Int Int
 deriving Int -> Offset -> ShowS
[Offset] -> ShowS
Offset -> String
(Int -> Offset -> ShowS)
-> (Offset -> String) -> ([Offset] -> ShowS) -> Show Offset
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Offset -> ShowS
showsPrec :: Int -> Offset -> ShowS
$cshow :: Offset -> String
show :: Offset -> String
$cshowList :: [Offset] -> ShowS
showList :: [Offset] -> ShowS
Show

-- | Better fail method, keeping track of offsets
fail :: Offset -> String -> Q a
fail :: forall a. Offset -> String -> Q a
fail Offset
Unknown     String
s = String -> Q a
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
P.fail String
s
fail off :: Offset
off@OffBy{} String
s = do Loc
loc <- Q Loc
location
                        String -> Q a
forall a. String -> Q a
forall (m :: * -> *) a. MonadFail m => String -> m a
P.fail (Loc -> Offset -> String
fmtLoc Loc
loc Offset
off String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++  String
s)

-- | Format a given location by the offset
fmtLoc :: Loc -> Offset -> String
fmtLoc :: Loc -> Offset -> String
fmtLoc loc :: Loc
loc@Loc{loc_start :: Loc -> CharPos
loc_start = (Int
sl, Int
_)} Offset
off = ShowS
takeFileName (Loc -> String
loc_filename Loc
newLoc) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ CharPos -> CharPos -> String
forall {a} {a}.
(Show a, Show a, Eq a, Eq a) =>
(a, a) -> (a, a) -> String
sh (Loc -> CharPos
loc_start Loc
newLoc) (Loc -> CharPos
loc_end Loc
newLoc)
  where sh :: (a, a) -> (a, a) -> String
sh ab :: (a, a)
ab@(a
a, a
b) cd :: (a, a)
cd@(a
c, a
d) | a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c = a -> String
forall a. Show a => a -> String
show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ if a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
d then String
"" else Char
'-' Char -> ShowS
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show a
d
                               | Bool
True   = (a, a) -> String
forall a. Show a => a -> String
show (a, a)
ab String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"-" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (a, a) -> String
forall a. Show a => a -> String
show (a, a)
cd

        newLoc :: Loc
newLoc = case Offset
off of
                   Offset
Unknown       -> Loc
loc
                   OffBy Int
lo Int
co Int
w -> Loc
loc {loc_start = (sl + lo, co + 1), loc_end = (sl + lo, co + w)}

-- | What kind of case-match are we given. In each case, the last maybe exp is the possible guard.
data Case = CMatch Offset          -- regular match
                   Name            -- name of the constructor
                   (Maybe [Pat])   -- [a, b, c] in C a b c. Or Nothing if C{}
                   (Maybe Exp)     -- guard
                   Exp             -- rhs
                   (Set Name)      -- All variables used all RHSs and All guards
          | CWild  Offset          -- wild card
                   (Maybe Exp)     -- guard
                   Exp             -- rhs

-- | What's the offset?
caseOffset :: Case -> Offset
caseOffset :: Case -> Offset
caseOffset (CMatch Offset
o Name
_ Maybe [Pat]
_ Maybe Exp
_ Exp
_ Set Name
_) = Offset
o
caseOffset (CWild  Offset
o       Maybe Exp
_ Exp
_) = Offset
o

-- | Show a case nicely
showCase :: Case -> String
showCase :: Case -> String
showCase = Maybe Loc -> Case -> String
showCaseGen Maybe Loc
forall a. Maybe a
Nothing

-- | Show a case nicely, with location
showCaseGen :: Maybe Loc -> Case -> String
showCaseGen :: Maybe Loc -> Case -> String
showCaseGen Maybe Loc
mbLoc Case
sc = case Case
sc of
                         CMatch Offset
_ Name
c (Just [Pat]
ps) Maybe Exp
mbG Exp
_ Set Name
_ -> String
loc String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (Name -> String
nameBase Name
c String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Pat -> String) -> [Pat] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Pat -> String
forall a. Ppr a => a -> String
pprint [Pat]
ps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Maybe Exp -> [String]
forall {a}. Ppr a => Maybe a -> [String]
shGuard Maybe Exp
mbG)
                         CMatch Offset
_ Name
c Maybe [Pat]
Nothing   Maybe Exp
mbG Exp
_ Set Name
_ -> String
loc String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (Name -> String
nameBase Name
c String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String
"{}"           String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Maybe Exp -> [String]
forall {a}. Ppr a => Maybe a -> [String]
shGuard Maybe Exp
mbG)
                         CWild  Offset
_             Maybe Exp
mbG Exp
_   -> String
loc String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (String
"_"                         String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Maybe Exp -> [String]
forall {a}. Ppr a => Maybe a -> [String]
shGuard Maybe Exp
mbG)
 where shGuard :: Maybe a -> [String]
shGuard Maybe a
Nothing  = []
       shGuard (Just a
e) = [String
"|", a -> String
forall a. Ppr a => a -> String
pprint a
e]

       loc :: String
loc = case Maybe Loc
mbLoc of
               Maybe Loc
Nothing -> String
""
               Just Loc
l  -> Loc -> Offset -> String
fmtLoc Loc
l (Case -> Offset
caseOffset Case
sc) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": "

-- | Get the name of the constructor, if any
getCaseConstructor :: Case -> Maybe Name
getCaseConstructor :: Case -> Maybe Name
getCaseConstructor (CMatch Offset
_ Name
nm Maybe [Pat]
_ Maybe Exp
_ Exp
_ Set Name
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm
getCaseConstructor CWild{}               = Maybe Name
forall a. Maybe a
Nothing

-- | Get the guard, if any
getCaseGuard :: Case -> Maybe Exp
getCaseGuard :: Case -> Maybe Exp
getCaseGuard (CMatch Offset
_ Name
_ Maybe [Pat]
_ Maybe Exp
mbg Exp
_ Set Name
_) = Maybe Exp
mbg
getCaseGuard (CWild  Offset
_     Maybe Exp
mbg Exp
_  ) = Maybe Exp
mbg

-- | Is there a guard?
isGuarded :: Case -> Bool
isGuarded :: Case -> Bool
isGuarded = Maybe Exp -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Exp -> Bool) -> (Case -> Maybe Exp) -> Case -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Case -> Maybe Exp
getCaseGuard

-- | Find offset of each successive match. This isn't perfect, but it does the job
findOffsets :: String -> [Offset]
findOffsets :: String -> [Offset]
findOffsets String
s = ParseResult (Exp SrcSpanInfo) -> [Offset]
analyze (ParseResult (Exp SrcSpanInfo) -> [Offset])
-> ParseResult (Exp SrcSpanInfo) -> [Offset]
forall a b. (a -> b) -> a -> b
$ ParseMode -> String -> ParseResult (Exp SrcSpanInfo)
E.parseExpWithMode ParseMode
E.defaultParseMode (String -> ParseResult (Exp SrcSpanInfo))
-> String -> ParseResult (Exp SrcSpanInfo)
forall a b. (a -> b) -> a -> b
$ String
"case ()" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
tab String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
rest
  where rest :: String
rest = ShowS
relevant String
s
        -- there's a chance the replication below might yield a negative value, which can make our
        -- offset calculation slightly off. But this should be exceedingly rare because it'd have to be that
        -- matches are on the same line and the "Type expr" part of the original must be shorter than 7 chars.
        -- Let's ignore that possibility.
        tab :: String
tab  = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
rest Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
7) Char
' '
        relevant :: ShowS
relevant r :: String
r@(Char
' ':Char
'o':Char
'f':String
_) = String
r
        relevant String
""                = String
""
        relevant (Char
_:String
cs)            = ShowS
relevant String
cs

        analyze :: ParseResult (Exp SrcSpanInfo) -> [Offset]
analyze E.ParseFailed{} = [] -- Just ignore
        analyze (E.ParseOk Exp SrcSpanInfo
e)   = case Exp SrcSpanInfo
e of
                                   E.Case SrcSpanInfo
_ Exp SrcSpanInfo
_ [Alt SrcSpanInfo]
alts -> (Alt SrcSpanInfo -> Offset) -> [Alt SrcSpanInfo] -> [Offset]
forall a b. (a -> b) -> [a] -> [b]
map Alt SrcSpanInfo -> Offset
getOff [Alt SrcSpanInfo]
alts
                                   Exp SrcSpanInfo
_               -> []
          where getOff :: Alt SrcSpanInfo -> Offset
getOff (E.Alt SrcSpanInfo
l Pat SrcSpanInfo
p Rhs SrcSpanInfo
_ Maybe (Binds SrcSpanInfo)
_) = Int -> Int -> Int -> Offset
OffBy (SrcSpan -> Int
E.srcSpanStartLine SrcSpan
as Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (SrcSpan -> Int
E.srcSpanStartColumn SrcSpan
as Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
w
                   where as :: SrcSpan
as = SrcSpanInfo -> SrcSpan
E.srcInfoSpan SrcSpanInfo
l
                         cs :: SrcSpan
cs = SrcSpanInfo -> SrcSpan
E.srcInfoSpan (Pat SrcSpanInfo -> SrcSpanInfo
forall l. Pat l -> l
forall (ast :: * -> *) l. Annotated ast => ast l -> l
E.ann Pat SrcSpanInfo
p)
                         w :: Int
w  = SrcSpan -> Int
E.srcSpanEndColumn SrcSpan
cs Int -> Int -> Int
forall a. Num a => a -> a -> a
- SrcSpan -> Int
E.srcSpanStartColumn SrcSpan
cs

-- * Shared parsing infrastructure

-- | Parse a Haskell expression using haskell-src-exts
metaParse :: String -> Either String Exp
metaParse :: String -> Either String Exp
metaParse = (Exp SrcSpanInfo -> Exp)
-> Either String (Exp SrcSpanInfo) -> Either String Exp
forall a b. (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Exp SrcSpanInfo -> Exp
forall a. ToExp a => a -> Exp
Meta.toExp (Either String (Exp SrcSpanInfo) -> Either String Exp)
-> (String -> Either String (Exp SrcSpanInfo))
-> String
-> Either String Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseResult (Exp SrcSpanInfo) -> Either String (Exp SrcSpanInfo)
forall a. ParseResult a -> Either String a
Meta.parseResultToEither (ParseResult (Exp SrcSpanInfo) -> Either String (Exp SrcSpanInfo))
-> (String -> ParseResult (Exp SrcSpanInfo))
-> String
-> Either String (Exp SrcSpanInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseMode -> String -> ParseResult (Exp SrcSpanInfo)
E.parseExpWithMode ParseMode
pm
  where pm :: ParseMode
pm = ParseMode
E.defaultParseMode { E.parseFilename = []
                                , E.baseLanguage  = E.Haskell2010
                                , E.extensions = map E.EnableExtension (exts ++ extras)
                                }
        exts :: [KnownExtension]
exts = [ KnownExtension
E.PostfixOperators
               , KnownExtension
E.QuasiQuotes
               , KnownExtension
E.UnicodeSyntax
               , KnownExtension
E.PatternSignatures
               , KnownExtension
E.MagicHash
               , KnownExtension
E.ForeignFunctionInterface
               , KnownExtension
E.TemplateHaskell
               , KnownExtension
E.RankNTypes
               , KnownExtension
E.MultiParamTypeClasses
               , KnownExtension
E.RecursiveDo
               , KnownExtension
E.TypeApplications
               ]

        -- The above just mimics the defaults. These our extras.
        extras :: [KnownExtension]
extras = [KnownExtension
E.DataKinds]

-- | Split the quasiquote input into (type, scrutinee) and alternatives
parts :: String -> Maybe ((String, String), String)
parts :: String -> Maybe ((String, String), String)
parts = String -> String -> Maybe ((String, String), String)
go String
""
  where go :: String -> String -> Maybe ((String, String), String)
go String
_     String
""             = Maybe ((String, String), String)
forall a. Maybe a
Nothing
        go String
sofar (Char
'o':Char
'f':String
rest) = ((String, String), String) -> Maybe ((String, String), String)
forall a. a -> Maybe a
Just ((Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Char -> Bool
isSpace ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace (ShowS
forall a. [a] -> [a]
reverse String
sofar)), String
rest)
        go String
sofar (Char
c:String
cs)         = String -> String -> Maybe ((String, String), String)
go (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
sofar) String
cs

-- | Extract guards from a match body
getGuards :: Body -> [Dec] -> Q [(Maybe Exp, Exp)]
getGuards :: Body -> [Dec] -> Q [(Maybe Exp, Exp)]
getGuards (NormalB  Exp
rhs)  [Dec]
locals = [(Maybe Exp, Exp)] -> Q [(Maybe Exp, Exp)]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Maybe Exp
forall a. Maybe a
Nothing, [Dec] -> Exp -> Exp
addLocals [Dec]
locals Exp
rhs)]
getGuards (GuardedB [(Guard, Exp)]
exps) [Dec]
locals = ((Guard, Exp) -> Q (Maybe Exp, Exp))
-> [(Guard, Exp)] -> Q [(Maybe Exp, Exp)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Guard, Exp) -> Q (Maybe Exp, Exp)
get [(Guard, Exp)]
exps
  where get :: (Guard, Exp) -> Q (Maybe Exp, Exp)
get (NormalG Exp
e,  Exp
rhs)
          | Exp -> Bool
isSTrue Exp
e
          = (Maybe Exp, Exp) -> Q (Maybe Exp, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Exp
forall a. Maybe a
Nothing, [Dec] -> Exp -> Exp
addLocals [Dec]
locals Exp
rhs)
          | Bool
True
          = (Maybe Exp, Exp) -> Q (Maybe Exp, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
e, [Dec] -> Exp -> Exp
addLocals [Dec]
locals Exp
rhs)
        get (PatG [Stmt]
stmts, Exp
rhs)
          | (Stmt -> Bool) -> [Stmt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Stmt -> Bool
isNoBindS [Stmt]
stmts
          = let guards :: [Exp]
guards = [Exp
e | NoBindS Exp
e <- [Stmt]
stmts]
                conj :: Exp
conj   = (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\Exp
a Exp
b -> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.&&), Exp
a, Exp
b]) [Exp]
guards
            in (Maybe Exp, Exp) -> Q (Maybe Exp, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if Exp -> Bool
isSTrue Exp
conj then Maybe Exp
forall a. Maybe a
Nothing else Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
conj, [Dec] -> Exp -> Exp
addLocals [Dec]
locals Exp
rhs)
          | Bool
True
          = Offset -> String -> Q (Maybe Exp, Exp)
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q (Maybe Exp, Exp)) -> String -> Q (Maybe Exp, Exp)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$  String
"sCase/pCase: Pattern guards are not supported: "
                                   String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
"        " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Stmt -> String
forall a. Ppr a => a -> String
pprint Stmt
s | Stmt
s <- [Stmt]
stmts]
          where isNoBindS :: Stmt -> Bool
isNoBindS (NoBindS Exp
_) = Bool
True
                isNoBindS Stmt
_           = Bool
False

        -- Is this literally sTrue (or True)? This is a bit dangerous since
        -- we just look at the base-name, but good enough
        isSTrue :: Exp -> Bool
isSTrue (VarE  Name
nm) = Name -> String
nameBase Name
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
nameBase 'sTrue
        isSTrue (ConE  Name
nm) = Name -> String
nameBase Name
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"True"
        isSTrue Exp
_          = Bool
False

-- | Turn where clause into simple let
addLocals :: [Dec] -> Exp -> Exp
addLocals :: [Dec] -> Exp -> Exp
addLocals [] Exp
e = Exp
e
addLocals [Dec]
ds Exp
e = [Dec] -> Exp -> Exp
LetE [Dec]
ds Exp
e

-- | Given an occurrence of a name, find what it refers to
getReference :: Offset -> Name -> Q Name
getReference :: Offset -> Name -> Q Name
getReference Offset
off Name
refName = do Maybe Name
mbN <- String -> Q (Maybe Name)
lookupValueName (Name -> String
nameBase Name
refName)
                              case Maybe Name
mbN of
                                Maybe Name
Nothing -> Offset -> String -> Q Name
forall a. Offset -> String -> Q a
fail Offset
off (String -> Q Name) -> String -> Q Name
forall a b. (a -> b) -> a -> b
$ String
"sCase/pCase: Not in scope: data constructor: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Ppr a => a -> String
pprint Name
refName
                                Just Name
n  -> Name -> Q Name
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
n

-- | Convert a match into a list of cases
matchToPair :: Exp -> Offset -> Match -> Q [Case]
matchToPair :: Exp -> Offset -> Match -> Q [Case]
matchToPair Exp
scrut Offset
off (Match Pat
pat Body
grhs [Dec]
locals) = do
  [(Maybe Exp, Exp)]
rhss <- Body -> [Dec] -> Q [(Maybe Exp, Exp)]
getGuards Body
grhs [Dec]
locals
  let allUsed :: Set Name
allUsed = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (((Maybe Exp, Exp) -> Set Name) -> [(Maybe Exp, Exp)] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe Exp
mbG, Exp
e) -> Set Name -> (Exp -> Set Name) -> Maybe Exp -> Set Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Name
forall a. Set a
Set.empty Exp -> Set Name
freeVars Maybe Exp
mbG Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Exp -> Set Name
freeVars Exp
e) [(Maybe Exp, Exp)]
rhss)

  case Pat
pat of
    ConP Name
conName [Type]
_ [Pat]
subpats -> do
      Name
con <- Offset -> Name -> Q Name
getReference Offset
off Name
conName
      -- For each sub-pattern at position i, flatten it against the accessor expression
      let accessor :: a -> Exp
accessor a
i = Exp -> Exp -> Exp
AppE (Name -> Exp
VarE (String -> Name
mkName (String
"get" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
con String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i))) Exp
scrut
      [(Pat, [Exp], [Dec])]
flatResults <- (Int -> Pat -> Q (Pat, [Exp], [Dec]))
-> [Int] -> [Pat] -> Q [(Pat, [Exp], [Dec])]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Offset -> Exp -> Pat -> Q (Pat, [Exp], [Dec])
flattenPat Offset
off (Exp -> Pat -> Q (Pat, [Exp], [Dec]))
-> (Int -> Exp) -> Int -> Pat -> Q (Pat, [Exp], [Dec])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Exp
forall {a}. Show a => a -> Exp
accessor) [(Int
1::Int)..] [Pat]
subpats
      let ps :: [Pat]
ps      = ((Pat, [Exp], [Dec]) -> Pat) -> [(Pat, [Exp], [Dec])] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Pat, [Exp], [Dec]) -> Pat
forall a b c. (a, b, c) -> a
fstOf3 [(Pat, [Exp], [Dec])]
flatResults
          subGrds :: [Exp]
subGrds = ((Pat, [Exp], [Dec]) -> [Exp]) -> [(Pat, [Exp], [Dec])] -> [Exp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Pat, [Exp], [Dec]) -> [Exp]
forall a b c. (a, b, c) -> b
sndOf3 [(Pat, [Exp], [Dec])]
flatResults
          subDecs :: [Dec]
subDecs = ((Pat, [Exp], [Dec]) -> [Dec]) -> [(Pat, [Exp], [Dec])] -> [Dec]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Pat, [Exp], [Dec]) -> [Dec]
forall a b c. (a, b, c) -> c
thdOf3 [(Pat, [Exp], [Dec])]
flatResults

          andAll :: [Exp] -> Exp
andAll [Exp
g]    = Exp
g
          andAll (Exp
g:[Exp]
gs) = (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.&&), Exp
g, [Exp] -> Exp
andAll [Exp]
gs]
          andAll []     = Name -> Exp
VarE 'sTrue

          -- Merge synthetic nested-pattern guards and bindings into each (guard, rhs) pair
          merge :: (Maybe Exp, Exp) -> (Maybe Exp, Exp)
merge (Maybe Exp
mbG, Exp
rhs) =
            let usedInRhs :: Set Name
usedInRhs  = Exp -> Set Name
freeVars Exp
rhs
                usedInGrd :: Set Name
usedInGrd  = Set Name -> (Exp -> Set Name) -> Maybe Exp -> Set Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Name
forall a. Set a
Set.empty Exp -> Set Name
freeVars Maybe Exp
mbG
                decsFor :: Set Name -> [Dec]
decsFor Set Name
s  = [ Dec
d | d :: Dec
d@(ValD (VarP Name
v) Body
_ [Dec]
_) <- [Dec]
subDecs, Name
v Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
s ]
                rhs' :: Exp
rhs' = [Dec] -> Exp -> Exp
addLocals (Set Name -> [Dec]
decsFor Set Name
usedInRhs) Exp
rhs
                mbG' :: Maybe Exp
mbG' = case ([Exp]
subGrds, Maybe Exp
mbG) of
                          ([], Maybe Exp
Nothing) -> Maybe Exp
forall a. Maybe a
Nothing
                          ([], Just Exp
g ) -> Exp -> Maybe Exp
forall a. a -> Maybe a
Just ([Dec] -> Exp -> Exp
addLocals (Set Name -> [Dec]
decsFor Set Name
usedInGrd) Exp
g)
                          ([Exp]
gs, Maybe Exp
Nothing) -> Exp -> Maybe Exp
forall a. a -> Maybe a
Just ([Exp] -> Exp
andAll [Exp]
gs)
                          ([Exp]
gs, Just Exp
g ) -> Exp -> Maybe Exp
forall a. a -> Maybe a
Just ((Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.&&), [Exp] -> Exp
andAll [Exp]
gs, [Dec] -> Exp -> Exp
addLocals (Set Name -> [Dec]
decsFor Set Name
usedInGrd) Exp
g])
            in (Maybe Exp
mbG', Exp
rhs')

      [Case] -> Q [Case]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Offset
-> Name -> Maybe [Pat] -> Maybe Exp -> Exp -> Set Name -> Case
CMatch Offset
off Name
con ([Pat] -> Maybe [Pat]
forall a. a -> Maybe a
Just [Pat]
ps) Maybe Exp
mbG Exp
rhs Set Name
allUsed | (Maybe Exp
mbG, Exp
rhs) <- ((Maybe Exp, Exp) -> (Maybe Exp, Exp))
-> [(Maybe Exp, Exp)] -> [(Maybe Exp, Exp)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Exp, Exp) -> (Maybe Exp, Exp)
merge [(Maybe Exp, Exp)]
rhss]

    RecP Name
conName []        -> do Name
con <- Offset -> Name -> Q Name
getReference Offset
off Name
conName
                                 [Case] -> Q [Case]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Offset
-> Name -> Maybe [Pat] -> Maybe Exp -> Exp -> Set Name -> Case
CMatch Offset
off Name
con Maybe [Pat]
forall a. Maybe a
Nothing   Maybe Exp
mbG Exp
rhs Set Name
allUsed | (Maybe Exp
mbG, Exp
rhs) <- [(Maybe Exp, Exp)]
rhss]

    Pat
WildP                  ->    [Case] -> Q [Case]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Offset -> Maybe Exp -> Exp -> Case
CWild  Offset
off               Maybe Exp
mbG Exp
rhs         | (Maybe Exp
mbG, Exp
rhs) <- [(Maybe Exp, Exp)]
rhss]

    Pat
_ -> Offset -> String -> Q [Case]
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q [Case]) -> String -> Q [Case]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase/pCase: Unsupported pattern:"
                                , String
"            Saw: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pat -> String
forall a. Ppr a => a -> String
pprint Pat
pat
                                , String
""
                                , String
"        Only constructors with variables (i.e., Cstr a b _ d)"
                                , String
"        Empty record matches (i.e., Cstr{})"
                                , String
"        And wildcards (i.e., _) for default"
                                , String
"        are supported at the top level."
                                , String
"        (Integer and string literals are supported in nested positions.)"
                                ]

-- | Flatten a sub-pattern against a given accessor expression.
-- Returns: a simple VarP/WildP for the flat pattern list, a list of
-- synthetic isCstr guard expressions, and let-bindings that bring
-- nested-pattern variables into scope.
flattenPat :: Offset -> Exp -> Pat -> Q (Pat, [Exp], [Dec])
flattenPat :: Offset -> Exp -> Pat -> Q (Pat, [Exp], [Dec])
flattenPat Offset
_   Exp
_   Pat
WildP                    = (Pat, [Exp], [Dec]) -> Q (Pat, [Exp], [Dec])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat
WildP, [], [])
flattenPat Offset
_   Exp
_   p :: Pat
p@(VarP Name
_)               = (Pat, [Exp], [Dec]) -> Q (Pat, [Exp], [Dec])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat
p,     [], [])
flattenPat Offset
off Exp
arg (ParensP Pat
p)              = Offset -> Exp -> Pat -> Q (Pat, [Exp], [Dec])
flattenPat Offset
off Exp
arg Pat
p
flattenPat Offset
off Exp
arg (ConP Name
conName [Type]
_ [Pat]
subpats) = do
  Name
con   <- Offset -> Name -> Q Name
getReference Offset
off Name
conName
  -- Arity check: reify the constructor to find its actual field count
  DataConI Name
_ Type
conType Name
_ <- Name -> Q Info
reify Name
con
  let arity :: Int
arity = Type -> Int
countArgs Type
conType
  Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Pat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pat]
subpats) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
    Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
off (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase/pCase: Arity mismatch in nested pattern."
                       , String
"        Constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
con
                       , String
"        Expected   : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
arity
                       , String
"        Given      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Pat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pat]
subpats)
                       ]
  let tester :: Exp
tester      = Exp -> Exp -> Exp
AppE (Name -> Exp
VarE (String -> Name
mkName (String
"is" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
con))) Exp
arg
      accessor :: a -> Exp
accessor a
i  = Exp -> Exp -> Exp
AppE (Name -> Exp
VarE (String -> Name
mkName (String
"get" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
con String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i))) Exp
arg
  [(Pat, [Exp], [Dec])]
subResults <- (Int -> Pat -> Q (Pat, [Exp], [Dec]))
-> [Int] -> [Pat] -> Q [(Pat, [Exp], [Dec])]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Offset -> Exp -> Pat -> Q (Pat, [Exp], [Dec])
flattenPat Offset
off (Exp -> Pat -> Q (Pat, [Exp], [Dec]))
-> (Int -> Exp) -> Int -> Pat -> Q (Pat, [Exp], [Dec])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Exp
forall {a}. Show a => a -> Exp
accessor) [(Int
1::Int)..] [Pat]
subpats
  let subGrds :: [Exp]
subGrds = ((Pat, [Exp], [Dec]) -> [Exp]) -> [(Pat, [Exp], [Dec])] -> [Exp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Pat, [Exp], [Dec]) -> [Exp]
forall a b c. (a, b, c) -> b
sndOf3 [(Pat, [Exp], [Dec])]
subResults
      subDecs :: [Dec]
subDecs = ((Pat, [Exp], [Dec]) -> [Dec]) -> [(Pat, [Exp], [Dec])] -> [Dec]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Pat, [Exp], [Dec]) -> [Dec]
forall a b c. (a, b, c) -> c
thdOf3 [(Pat, [Exp], [Dec])]
subResults
      subPats :: [Pat]
subPats = ((Pat, [Exp], [Dec]) -> Pat) -> [(Pat, [Exp], [Dec])] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Pat, [Exp], [Dec]) -> Pat
forall a b c. (a, b, c) -> a
fstOf3 [(Pat, [Exp], [Dec])]
subResults
      patDecs :: [Dec]
patDecs = [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
v) (Exp -> Body
NormalB (Int -> Exp
forall {a}. Show a => a -> Exp
accessor Int
i)) []
                | (Int
i, VarP Name
v) <- [Int] -> [Pat] -> [(Int, Pat)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1::Int)..] [Pat]
subPats ]
  (Pat, [Exp], [Dec]) -> Q (Pat, [Exp], [Dec])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat
WildP, Exp
tester Exp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
: [Exp]
subGrds, [Dec]
patDecs [Dec] -> [Dec] -> [Dec]
forall a. [a] -> [a] -> [a]
++ [Dec]
subDecs)
flattenPat Offset
off Exp
arg (LitP Lit
lit) = do
  Exp
eq <- Offset -> Exp -> Lit -> Q Exp
litToEq Offset
off Exp
arg Lit
lit
  (Pat, [Exp], [Dec]) -> Q (Pat, [Exp], [Dec])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pat
WildP, [Exp
eq], [])
flattenPat Offset
o Exp
_ Pat
p = Offset -> String -> Q (Pat, [Exp], [Dec])
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q (Pat, [Exp], [Dec]))
-> String -> Q (Pat, [Exp], [Dec])
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase/pCase: Unsupported complex pattern match."
                                    , String
"        Saw: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Pat -> String
forall a. Ppr a => a -> String
pprint Pat
p
                                    , String
""
                                    , String
"      Only variables, wildcards, nested constructors, and integer/string literals are supported."
                                    ]

fstOf3 :: (a, b, c) -> a
fstOf3 :: forall a b c. (a, b, c) -> a
fstOf3 (a
a, b
_, c
_) = a
a

sndOf3 :: (a, b, c) -> b
sndOf3 :: forall a b c. (a, b, c) -> b
sndOf3 (a
_, b
b, c
_) = b
b

thdOf3 :: (a, b, c) -> c
thdOf3 :: forall a b c. (a, b, c) -> c
thdOf3 (a
_, b
_, c
c) = c
c

-- * sCase

-- | Quasi-quoter for symbolic case expressions.
sCase :: QuasiQuoter
sCase :: QuasiQuoter
sCase = QuasiQuoter
  { quoteExp :: String -> Q Exp
quoteExp  = String -> Q Exp
extract
  , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall {p} {a}. String -> p -> Q a
bad String
"pattern"
  , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall {p} {a}. String -> p -> Q a
bad String
"type"
  , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall {p} {a}. String -> p -> Q a
bad String
"declaration"
  }
  where
    bad :: String -> p -> Q a
bad String
ctx p
_ = Offset -> String -> Q a
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q a) -> String -> Q a
forall a b. (a -> b) -> a -> b
$ String
"sCase: not usable in " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
ctx String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" context"

    extract :: String -> ExpQ
    extract :: String -> Q Exp
extract String
src =
      case String -> Maybe ((String, String), String)
parts String
src of
        Maybe ((String, String), String)
Nothing -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase: Failed to parse a symbolic case-expression."
                                          , String
""
                                          , String
"           Instead of:   case      expr of alts"
                                          , String
"           Write     : [sCase|Type expr of alts|]"
                                          , String
""
                                          , String
"        where Type is the underlying concrete type of the expression."
                                          ]
        Just ((String
typ, String
scrutStr), String
altsStr) -> do
          let fnTok :: String
fnTok    = String
"sCase" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
typ
              fullCase :: String
fullCase = String
"case " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
scrutStr String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" of " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
altsStr
              offsets :: [Offset]
offsets  = String -> [Offset]
findOffsets String
src
          case String -> Either String Exp
metaParse String
fullCase of
            Right (CaseE Exp
scrut [Match]
matches) -> do
              Exp
fnName <- String -> Q (Maybe Name)
lookupValueName String
fnTok Q (Maybe Name) -> (Maybe Name -> Q Exp) -> Q Exp
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Just Name
n  -> Exp -> Q Exp
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Name -> Exp
VarE Name
n)
                Maybe Name
Nothing -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase: Unknown symbolic ADT: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
typ
                                                  , String
""
                                                  , String
"        To use a symbolic case expression, declare your ADT, and then:"
                                                  , String
"             mkSymbolic [''" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
typ String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"]"
                                                  , String
"        In a template-haskell context."
                                                  ]
              Either [Exp] [(Exp, Exp)]
cases <- (Offset -> Match -> Q [Case]) -> [Offset] -> [Match] -> Q [[Case]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Exp -> Offset -> Match -> Q [Case]
matchToPair Exp
scrut) ([Offset]
offsets [Offset] -> [Offset] -> [Offset]
forall a. [a] -> [a] -> [a]
++ Offset -> [Offset]
forall a. a -> [a]
repeat Offset
Unknown) [Match]
matches Q [[Case]]
-> ([[Case]] -> Q (Either [Exp] [(Exp, Exp)]))
-> Q (Either [Exp] [(Exp, Exp)])
forall a b. Q a -> (a -> Q b) -> Q b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Exp -> String -> [Case] -> Q (Either [Exp] [(Exp, Exp)])
checkCase Exp
scrut String
typ ([Case] -> Q (Either [Exp] [(Exp, Exp)]))
-> ([[Case]] -> [Case])
-> [[Case]]
-> Q (Either [Exp] [(Exp, Exp)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Case]] -> [Case]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
              String -> Exp -> Exp -> Either [Exp] [(Exp, Exp)] -> Q Exp
forall {f :: * -> *} {t :: * -> *}.
(Foldable t, Quote f) =>
String -> Exp -> Exp -> Either (t Exp) [(Exp, Exp)] -> f Exp
buildCase String
typ Exp
fnName Exp
scrut Either [Exp] [(Exp, Exp)]
cases
            Right Exp
_  -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
Unknown String
"sCase: Parse error, cannot extract a case-expression."
            Left String
err -> case String -> [String]
lines String
err of
                          (String
_:String
loc:[String]
res) | [String
"SrcLoc", String
_, String
l, String
c] <- String -> [String]
words String
loc, (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
l, (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
c
                             -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail (Int -> Int -> Int -> Offset
OffBy (String -> Int
forall a. Read a => String -> a
read String
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (String -> Int
forall a. Read a => String -> a
read String
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
1) ([String] -> String
unlines [String]
res)
                          [String]
_  -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ String
"sCase parse error: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
err

    buildCase :: String -> Exp -> Exp -> Either (t Exp) [(Exp, Exp)] -> f Exp
buildCase String
_    Exp
caseFunc  Exp
scrut (Left  t Exp
cases) = Exp -> f Exp
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> f Exp) -> Exp -> f Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> Exp -> t Exp -> Exp
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Exp
caseFunc Exp -> Exp -> Exp
`AppE` Exp
scrut) t Exp
cases
    buildCase String
typ Exp
_caseFunc Exp
_scrut (Right [(Exp, Exp)]
cases) = do
        Name
uniq <- String -> f Name
forall (m :: * -> *). Quote m => String -> m Name
newName String
"u"
        let suffix :: String
suffix = Int -> ShowS
forall a. Int -> [a] -> [a]
drop Int
2 (Name -> String
forall a. Show a => a -> String
show Name
uniq)
            iteChain :: [(Exp, Exp)] -> f Exp
iteChain []              = Exp -> f Exp
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> f Exp) -> Exp -> f Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'sym) (Lit -> Exp
LitE (String -> Lit
StringL (String
"unmatched_sCase_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
suffix)))
            iteChain ((Exp
t, Exp
e) : [(Exp, Exp)]
rest) = do Exp
r <- [(Exp, Exp)] -> f Exp
iteChain [(Exp, Exp)]
rest
                                          Exp -> f Exp
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> f Exp) -> Exp -> f Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'ite) [Exp
t, Exp
e, Exp
r]
        [(Exp, Exp)] -> f Exp
forall {f :: * -> *}. Monad f => [(Exp, Exp)] -> f Exp
iteChain [(Exp, Exp)]
cases

    -- Make sure things are in good-shape and decide if we have guards
    checkCase :: Exp -> String -> [Case] -> Q (Either [Exp] [(Exp, Exp)])
    checkCase :: Exp -> String -> [Case] -> Q (Either [Exp] [(Exp, Exp)])
checkCase Exp
scrut String
typ [Case]
cases = do
        Loc
loc   <- Q Loc
location

        [(Name, [Type])]
cstrs <- -- We don't need the field names if user supplied them; so drop them here
                 let dropFieldNames :: (a, [(a, b)]) -> (a, [b])
dropFieldNames (a
c, [(a, b)]
nts) = (a
c, ((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
nts)
                 in ((Name, [(Maybe Name, Type)]) -> (Name, [Type]))
-> [(Name, [(Maybe Name, Type)])] -> [(Name, [Type])]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [(Maybe Name, Type)]) -> (Name, [Type])
forall {a} {a} {b}. (a, [(a, b)]) -> (a, [b])
dropFieldNames ([(Name, [(Maybe Name, Type)])] -> [(Name, [Type])])
-> (([Name], [(Name, [(Maybe Name, Type)])])
    -> [(Name, [(Maybe Name, Type)])])
-> ([Name], [(Name, [(Maybe Name, Type)])])
-> [(Name, [Type])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], [(Name, [(Maybe Name, Type)])])
-> [(Name, [(Maybe Name, Type)])]
forall a b. (a, b) -> b
snd (([Name], [(Name, [(Maybe Name, Type)])]) -> [(Name, [Type])])
-> Q ([Name], [(Name, [(Maybe Name, Type)])]) -> Q [(Name, [Type])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructors (String -> Name
mkName String
typ)

        -- Is there a catch all clause?
        let hasCatchAll :: Bool
hasCatchAll = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool
True | CWild Offset
_ Maybe Exp
Nothing Exp
_ <- [Case]
cases]

        -- Step 0: If there's an unguarded wild-card, make sure nothing else follows it.
        -- Note that this also handles wild-card being present twice.
        let checkWild :: [Case] -> Q ()
checkWild []                         = () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            checkWild (CMatch{}          : [Case]
rest) = [Case] -> Q ()
checkWild [Case]
rest
            checkWild (CWild Offset
_ Just{}  Exp
_ : [Case]
rest) = [Case] -> Q ()
checkWild [Case]
rest
            checkWild (CWild Offset
o Maybe Exp
Nothing Exp
_ : [Case]
rest) =
                  case [Case]
rest of
                    []  -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                    [Case]
red  -> Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"sCase: Wildcard makes the remaining matches redundant:"
                                             String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
"        " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Loc -> Case -> String
showCaseGen (Loc -> Maybe Loc
forall a. a -> Maybe a
Just Loc
loc) Case
r | Case
r <- [Case]
red]
        [Case] -> Q ()
checkWild [Case]
cases

        -- Step 2: Make sure every constructor listed actually exists and matches in arity.
        let chk1 :: Case -> Q ()
            chk1 :: Case -> Q ()
chk1 Case
c = case Case
c of
                       CMatch Offset
o Name
nm Maybe [Pat]
ps Maybe Exp
_ Exp
_ Set Name
_ -> Offset -> Name -> Maybe Int -> Q ()
isSafe Offset
o Name
nm ([Pat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Pat] -> Int) -> Maybe [Pat] -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Pat]
ps)
                       CWild  {}            -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              where isSafe :: Offset -> Name -> Maybe Int -> Q ()
                    isSafe :: Offset -> Name -> Maybe Int -> Q ()
isSafe Offset
o Name
nm Maybe Int
mbLen
                      | Just [Type]
ts <- Name
nm Name -> [(Name, [Type])] -> Maybe [Type]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Name, [Type])]
cstrs
                      = case Maybe Int
mbLen of
                           Maybe Int
Nothing  -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                           Just Int
cnt -> Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
cnt)
                                            (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase: Arity mismatch."
                                                               , String
"        Type       : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ
                                                               , String
"        Constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
nm
                                                               , String
"        Expected   : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts)
                                                               , String
"        Given      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
cnt
                                                               ]
                      | Bool
True
                      = Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase: Unknown constructor:"
                                         , String
"        Type          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ
                                         , String
"        Saw           : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Ppr a => a -> String
pprint Name
nm
                                         , String
"        Must be one of: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((Name, [Type]) -> String) -> [(Name, [Type])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> String
forall a. Ppr a => a -> String
pprint (Name -> String)
-> ((Name, [Type]) -> Name) -> (Name, [Type]) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, [Type]) -> Name
forall a b. (a, b) -> a
fst) [(Name, [Type])]
cstrs)
                                         ]

        (Case -> Q ()) -> [Case] -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Case -> Q ()
chk1 [Case]
cases

        -- Step 2: Make sure constructor matches are not overlapping
        let problem :: String -> [String] -> Case -> Q a
problem String
w [String]
extras Case
x = Offset -> String -> Q a
forall a. Offset -> String -> Q a
fail (Case -> Offset
caseOffset Case
x) (String -> Q a) -> String -> Q a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
"sCase: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":"
                                                                 , String
"        Type       : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ
                                                                 , String
"        Constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Case -> String
showCase Case
x
                                                                 ]
                                                              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"      " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e | String
e <- [String]
extras]

            overlap :: Case -> [Case] -> Q a
overlap Case
x [Case]
xs = String -> [String] -> Case -> Q a
forall {a}. String -> [String] -> Case -> Q a
problem String
"Overlapping case constructors" [String]
extras Case
x
              where extras :: [String]
extras = String
"Overlaps with:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
p | String
p <- (Case -> String) -> [Case] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Loc -> Case -> String
showCaseGen (Loc -> Maybe Loc
forall a. a -> Maybe a
Just Loc
loc)) [Case]
xs]

            unmatched :: Case -> Q a
unmatched Case
x
             | Case -> Bool
isGuarded Case
x = String -> [String] -> Case -> Q a
forall {a}. String -> [String] -> Case -> Q a
problem String
"Non-exhaustive match" [String
"NB. Guarded match might fail."] Case
x
             | Bool
True        = String -> [String] -> Case -> Q a
forall {a}. String -> [String] -> Case -> Q a
problem String
"Non-exhaustive match" []                                Case
x

            nonExhaustive :: Offset -> Name -> Q a
nonExhaustive Offset
o Name
cstr = Offset -> String -> Q a
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q a) -> String -> Q a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase: Pattern match(es) are non-exhaustive."
                                                    , String
"        Not matched     : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
cstr
                                                    , String
"        Patterns of type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ
                                                    , String
"        Must match each : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((Name, [Type]) -> String) -> [(Name, [Type])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> String
nameBase (Name -> String)
-> ((Name, [Type]) -> Name) -> (Name, [Type]) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, [Type]) -> Name
forall a b. (a, b) -> a
fst) [(Name, [Type])]
cstrs)
                                                    , String
""
                                                    , String
"      You can use a '_' to match multiple cases."
                                                    ]
            -- We're done
            chk2 :: [Case] -> Q ()
chk2 [] = () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

            -- If we have a non-guarded match, then there must be no matches for this constructor later on. If so, they're redundant.
            chk2 (c :: Case
c@(CMatch Offset
_ Name
nm Maybe [Pat]
_ Maybe Exp
Nothing Exp
_ Set Name
_) : [Case]
rest)
              = case (Case -> Bool) -> [Case] -> [Case]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Case
oc -> Case -> Maybe Name
getCaseConstructor Case
oc Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm) [Case]
rest of
                  [] -> [Case] -> Q ()
chk2 [Case]
rest
                  [Case]
os -> Case -> [Case] -> Q ()
forall {a}. Case -> [Case] -> Q a
overlap ([Case] -> Case
forall a. HasCallStack => [a] -> a
last [Case]
os) (Case
c Case -> [Case] -> [Case]
forall a. a -> [a] -> [a]
: [Case] -> [Case]
forall a. HasCallStack => [a] -> [a]
init [Case]
os)

            -- If we have a guarded match, then this guard can fail. So either there must be a match
            -- for it later on, or there must be a catch-all. Note that if it exists later, we don't
            -- care if that occurrence is guarded or not; because if it is guarded, we'll fail on the last one.
            chk2 (c :: Case
c@(CMatch Offset
_ Name
nm Maybe [Pat]
_ Just{} Exp
_ Set Name
_) : [Case]
rest)
              | Bool
hasCatchAll Bool -> Bool -> Bool
|| Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm Maybe Name -> [Maybe Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Case -> Maybe Name) -> [Case] -> [Maybe Name]
forall a b. (a -> b) -> [a] -> [b]
map Case -> Maybe Name
getCaseConstructor [Case]
rest
              = [Case] -> Q ()
chk2 [Case]
rest
              | Bool
True
              = Case -> Q ()
forall {a}. Case -> Q a
unmatched Case
c

            -- If there's a guarded wildcard, must make sure there's a catch all afterwards
            chk2 (c :: Case
c@(CWild Offset
_ Just{} Exp
_) : [Case]
rest)
              | Bool
hasCatchAll
              = [Case] -> Q ()
chk2 [Case]
rest
              | Bool
True
              = Case -> Q ()
forall {a}. Case -> Q a
unmatched Case
c

            -- No need to worry about anything following catch-all, since we already covered that before
            chk2 (CWild Offset
_ Maybe Exp
Nothing Exp
_ : [Case]
rest) = [Case] -> Q ()
chk2 [Case]
rest

        [Case] -> Q ()
chk2 [Case]
cases

        -- At this point, we either have a simple case with no guards, in which case
        -- we translate this to an sCase for that type. So find all alternatives.
        -- Otherwise, this will become an ite-chain
        let hasGuards :: Bool
hasGuards = (Case -> Bool) -> [Case] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Case -> Bool
isGuarded [Case]
cases

        if Bool -> Bool
not Bool
hasGuards
           then do Maybe (Offset, Exp)
defaultCase <- case [((Exp
e, Maybe Exp
mbg), Case
c) | c :: Case
c@(CWild Offset
_ Maybe Exp
mbg Exp
e) <- [Case]
cases] of
                                    []                  -> Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp))
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Offset, Exp)
forall a. Maybe a
Nothing
                                    [((Exp
e, Maybe Exp
Nothing), Case
c)] -> Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp))
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp)))
-> Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp))
forall a b. (a -> b) -> a -> b
$ (Offset, Exp) -> Maybe (Offset, Exp)
forall a. a -> Maybe a
Just (Case -> Offset
caseOffset Case
c, Exp
e)
                                    cs :: [((Exp, Maybe Exp), Case)]
cs@(((Exp, Maybe Exp)
_, Case
c):[((Exp, Maybe Exp), Case)]
_)       -> Offset -> String -> Q (Maybe (Offset, Exp))
forall a. Offset -> String -> Q a
fail (Case -> Offset
caseOffset Case
c)
                                                         (String -> Q (Maybe (Offset, Exp)))
-> String -> Q (Maybe (Offset, Exp))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$   String
"sCase: Impossible happened; found unexpected cases:"
                                                                   String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  [ String
"        " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Case -> String
showCase Case
curc | Case
curc <- (((Exp, Maybe Exp), Case) -> Case)
-> [((Exp, Maybe Exp), Case)] -> [Case]
forall a b. (a -> b) -> [a] -> [b]
map ((Exp, Maybe Exp), Case) -> Case
forall a b. (a, b) -> b
snd [((Exp, Maybe Exp), Case)]
cs]
                                                                   [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
""
                                                                      , String
"      Please report this as a bug."
                                                                      ]
                   let find :: Name -> [Case] -> Maybe Case
find Name
_ []     = Maybe Case
forall a. Maybe a
Nothing
                       find Name
w (Case
c:[Case]
cs)
                         | Bool
matches = Case -> Maybe Case
forall a. a -> Maybe a
Just Case
c
                         | Bool
True    = Name -> [Case] -> Maybe Case
find Name
w [Case]
cs
                         where matches :: Bool
matches = case Case
c of
                                           CMatch Offset
_ Name
nm Maybe [Pat]
_ Maybe Exp
_ Exp
_ Set Name
_ -> Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
w
                                           CWild  {}           -> Bool
False

                       case2rhs :: Case -> [Type] -> (Maybe Exp, Exp)
                       case2rhs :: Case -> [Type] -> (Maybe Exp, Exp)
case2rhs Case
cs [Type]
ts = ([Pat] -> Exp -> Exp
LamE [Pat]
pats (Exp -> Exp) -> Maybe Exp -> Maybe Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Exp
mbGuard, [Pat] -> Exp -> Exp
LamE [Pat]
pats Exp
e)
                         where (Maybe Exp
mbGuard, Exp
e, [Pat]
pats) = case Case
cs of
                                                      CMatch Offset
_ Name
_ (Just [Pat]
ps) Maybe Exp
mbG Exp
rhs Set Name
_ -> (Maybe Exp
mbG, Exp
rhs, [Pat]
ps)
                                                      CMatch Offset
_ Name
_ Maybe [Pat]
Nothing   Maybe Exp
mbG Exp
rhs Set Name
_ -> (Maybe Exp
mbG, Exp
rhs, (Type -> Pat) -> [Type] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Pat -> Type -> Pat
forall a b. a -> b -> a
const Pat
WildP) [Type]
ts)
                                                      CWild  Offset
_             Maybe Exp
mbG Exp
rhs   -> (Maybe Exp
mbG, Exp
rhs, (Type -> Pat) -> [Type] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Pat -> Type -> Pat
forall a b. a -> b -> a
const Pat
WildP) [Type]
ts)

                       collect :: (Name, [Type]) -> Q (Maybe Exp, Exp)
collect (Name
cstr, [Type]
ts)
                         | Just Case
e <- Name -> [Case] -> Maybe Case
find Name
cstr [Case]
cases
                         = (Maybe Exp, Exp) -> Q (Maybe Exp, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Maybe Exp, Exp) -> Q (Maybe Exp, Exp))
-> (Maybe Exp, Exp) -> Q (Maybe Exp, Exp)
forall a b. (a -> b) -> a -> b
$ Case -> [Type] -> (Maybe Exp, Exp)
case2rhs Case
e [Type]
ts
                         | Bool
True
                         = case Maybe (Offset, Exp)
defaultCase of
                             Maybe (Offset, Exp)
Nothing -> Offset -> Name -> Q (Maybe Exp, Exp)
forall {a}. Offset -> Name -> Q a
nonExhaustive Offset
Unknown Name
cstr
                             Just (Offset
_, Exp
de) -> do let ps :: [Pat]
ps = (Type -> Pat) -> [Type] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Pat -> Type -> Pat
forall a b. a -> b -> a
const Pat
WildP) [Type]
ts
                                                (Maybe Exp, Exp) -> Q (Maybe Exp, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Exp
forall a. Maybe a
Nothing, [Pat] -> Exp -> Exp
LamE [Pat]
ps Exp
de)

                   [(Maybe Exp, Exp)]
res <- ((Name, [Type]) -> Q (Maybe Exp, Exp))
-> [(Name, [Type])] -> Q [(Maybe Exp, Exp)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name, [Type]) -> Q (Maybe Exp, Exp)
collect [(Name, [Type])]
cstrs

                   -- If we reached here, all is well; except we might have an extra wildcard that we did not use
                   Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Case] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Case]
cases Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [(Name, [Type])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, [Type])]
cstrs) (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$
                     case Maybe (Offset, Exp)
defaultCase of
                       Maybe (Offset, Exp)
Nothing     -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                       Just (Offset
o, Exp
_) -> Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o String
"sCase: Wildcard match is redundant"

                   -- Double check that we had no guards and return the cases
                   case [Exp
r | (Just{}, Exp
r) <- [(Maybe Exp, Exp)]
res] of
                     [] -> Either [Exp] [(Exp, Exp)] -> Q (Either [Exp] [(Exp, Exp)])
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either [Exp] [(Exp, Exp)] -> Q (Either [Exp] [(Exp, Exp)]))
-> Either [Exp] [(Exp, Exp)] -> Q (Either [Exp] [(Exp, Exp)])
forall a b. (a -> b) -> a -> b
$ [Exp] -> Either [Exp] [(Exp, Exp)]
forall a b. a -> Either a b
Left ([Exp] -> Either [Exp] [(Exp, Exp)])
-> [Exp] -> Either [Exp] [(Exp, Exp)]
forall a b. (a -> b) -> a -> b
$ ((Maybe Exp, Exp) -> Exp) -> [(Maybe Exp, Exp)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Exp, Exp) -> Exp
forall a b. (a, b) -> b
snd [(Maybe Exp, Exp)]
res
                     [Exp]
rs -> Offset -> String -> Q (Either [Exp] [(Exp, Exp)])
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q (Either [Exp] [(Exp, Exp)]))
-> String -> Q (Either [Exp] [(Exp, Exp)])
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$    String
"sCase: Impossible happened; found a guard in no-guard case."
                                                  String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  [ String
"        " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Exp -> String
forall a. Ppr a => a -> String
pprint Exp
r | Exp
r <- [Exp]
rs]
                                                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
""
                                                    , String
"      Please report this as a bug."
                                                    ]

           else do -- We have guards.
                   Maybe (Offset, Exp)
defaultCase <- case [(Case
c, Exp
e) | c :: Case
c@(CWild Offset
_ Maybe Exp
Nothing Exp
e) <- [Case]
cases] of
                                    []         -> Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp))
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Offset, Exp)
forall a. Maybe a
Nothing
                                    ((Case
c, Exp
e):[(Case, Exp)]
_) -> Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp))
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp)))
-> Maybe (Offset, Exp) -> Q (Maybe (Offset, Exp))
forall a b. (a -> b) -> a -> b
$ (Offset, Exp) -> Maybe (Offset, Exp)
forall a. a -> Maybe a
Just (Case -> Offset
caseOffset Case
c, Exp
e)

                   -- Collect, for each constructor, the corresponding cases:
                   let cstrMatches :: [(Name, ([Type], [Case]))]
                       cstrMatches :: [(Name, ([Type], [Case]))]
cstrMatches = ((Name, [Type]) -> (Name, ([Type], [Case])))
-> [(Name, [Type])] -> [(Name, ([Type], [Case]))]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
cstr, [Type]
ts) -> (Name
cstr, ([Type]
ts, (Case -> [Case]) -> [Case] -> [Case]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Name -> Case -> [Case]
matches Name
cstr) [Case]
cases))) [(Name, [Type])]
cstrs
                         where matches :: Name -> Case -> [Case]
matches Name
cstr Case
c | Just Name
n <- Case -> Maybe Name
getCaseConstructor Case
c, Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
cstr = [Case
c]
                                              | Bool
True                                      = []

                   -- Make sure we have a match for every constructor or a catch-all
                   Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
hasCatchAll (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ case [Name
nm | (Name
nm, ([Type]
_, [])) <- [(Name, ([Type], [Case]))]
cstrMatches] of
                                          []    -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                                          (Name
x:[Name]
_) -> Offset -> Name -> Q ()
forall {a}. Offset -> Name -> Q a
nonExhaustive Offset
Unknown Name
x

                   -- If every constructor have a full match, then catch-all, if exists, is redundant:
                   case Maybe (Offset, Exp)
defaultCase of
                     Maybe (Offset, Exp)
Nothing     -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                     Just (Offset
o, Exp
_)
                       | ((Name, [Type]) -> Name) -> [(Name, [Type])] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [Type]) -> Name
forall a b. (a, b) -> a
fst [(Name, [Type])]
cstrs [Name] -> [Name] -> Bool
forall a. Eq a => a -> a -> Bool
== [Name
nm | (Name
nm, ([Type]
_, [Case]
cs)) <- [(Name, ([Type], [Case]))]
cstrMatches, Bool -> Bool
not ((Case -> Bool) -> [Case] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Case -> Bool
isGuarded [Case]
cs)]
                       -> Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o String
"sCase: Wildcard match is redundant"
                       | Bool
True
                       -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

                   let collect :: Case -> Q (Exp, Exp)
                       collect :: Case -> Q (Exp, Exp)
collect (CWild  Offset
_        Maybe Exp
mbG Exp
rhs        ) = (Exp, Exp) -> Q (Exp, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Maybe Exp -> Exp
forall a. a -> Maybe a -> a
fromMaybe (Name -> Exp
VarE 'sTrue) Maybe Exp
mbG, Exp
rhs)
                       collect (CMatch Offset
o Name
nm Maybe [Pat]
mbp Maybe Exp
mbG Exp
rhs Set Name
allUsed) = do
                           case Name
nm Name -> [(Name, [Type])] -> Maybe [Type]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Name, [Type])]
cstrs of
                             Maybe [Type]
Nothing -> Offset -> String -> Q (Exp, Exp)
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q (Exp, Exp)) -> String -> Q (Exp, Exp)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"sCase: Impossible happened."
                                                         , String
"        Unable to determine params for: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Name -> String
forall a. Ppr a => a -> String
pprint Name
nm
                                                         ]
                             Just [Type]
ts -> do let pats :: [Pat]
pats = [Pat] -> Maybe [Pat] -> [Pat]
forall a. a -> Maybe a -> a
fromMaybe ((Type -> Pat) -> [Type] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Pat -> Type -> Pat
forall a b. a -> b -> a
const Pat
WildP) [Type]
ts) Maybe [Pat]
mbp
                                               args :: [Exp]
args = [ Exp -> Exp -> Exp
AppE (Name -> Exp
VarE (String -> Name
mkName (String
"get" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i))) Exp
scrut
                                                      | (Int
i, Type
_) <- [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1 :: Int) ..] [Type]
ts]
                                               rec :: Exp
rec  = Name -> Exp
VarE (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Name
mkName (String -> Name) -> String -> Name
forall a b. (a -> b) -> a -> b
$ String
"is" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
nm

                                               -- What are the free variables in the guard and the rhs that we bind?
                                               used :: Set Name
used    = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList [Name
n | VarP Name
n <- [Pat]
pats] Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set Name
allUsed
                                               close :: Exp -> Exp
close Exp
e = (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (Exp -> Exp -> Exp
AppE (Exp -> Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'const)) (Exp
eExp -> [Exp] -> [Exp]
forall a. a -> [a] -> [a]
:[Exp]
extras)
                                                 where extras :: [Exp]
extras = (Name -> Exp) -> [Name] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Exp
VarE ([Name] -> [Exp]) -> [Name] -> [Exp]
forall a b. (a -> b) -> a -> b
$ Set Name -> [Name]
forall a. Set a -> [a]
Set.toList (Set Name
used Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Exp -> Set Name
freeVars Exp
e)

                                               mkApp :: Exp -> Exp
mkApp Exp
f | [Pat] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pat]
pats = Exp
f
                                                       | Bool
True      = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
AppE ([Pat] -> Exp -> Exp
LamE [Pat]
pats Exp
f) [Exp]
args

                                               grd :: Exp
                                               grd :: Exp
grd = case Maybe Exp
mbG of
                                                       Maybe Exp
Nothing -> Exp -> Exp -> Exp
AppE Exp
rec Exp
scrut
                                                       Just Exp
g  -> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.&&), Exp -> Exp -> Exp
AppE Exp
rec Exp
scrut, Exp -> Exp
mkApp (Exp -> Exp
close Exp
g)]

                                           (Exp, Exp) -> Q (Exp, Exp)
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp
grd, Exp -> Exp
mkApp (Exp -> Exp
close Exp
rhs))

                   [(Exp, Exp)] -> Either [Exp] [(Exp, Exp)]
forall a b. b -> Either a b
Right ([(Exp, Exp)] -> Either [Exp] [(Exp, Exp)])
-> Q [(Exp, Exp)] -> Q (Either [Exp] [(Exp, Exp)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Case -> Q (Exp, Exp)) -> [Case] -> Q [(Exp, Exp)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Case -> Q (Exp, Exp)
collect [Case]
cases

-- * pCase

-- | Quasi-quoter for proof case-splits.
--
-- Like 'sCase', but generates @cases [cond ==> proof, ...]@ instead of
-- @ite@ chains. Wildcards are allowed as the last scrutinee (with or
-- without guards), and exhaustiveness is checked at proof time by the
-- @cases@ combinator rather than at compile time.
--
-- Guards within the same constructor accumulate negations: a second guard
-- implicitly assumes the first guard failed. A wildcard guard is the
-- negation of the disjunction of all prior guards (De Morgan).
pCase :: QuasiQuoter
pCase :: QuasiQuoter
pCase = QuasiQuoter
  { quoteExp :: String -> Q Exp
quoteExp  = String -> Q Exp
extractProof
  , quotePat :: String -> Q Pat
quotePat  = String -> String -> Q Pat
forall {p} {a}. String -> p -> Q a
bad String
"pattern"
  , quoteType :: String -> Q Type
quoteType = String -> String -> Q Type
forall {p} {a}. String -> p -> Q a
bad String
"type"
  , quoteDec :: String -> Q [Dec]
quoteDec  = String -> String -> Q [Dec]
forall {p} {a}. String -> p -> Q a
bad String
"declaration"
  }
  where
    bad :: String -> p -> Q a
bad String
ctx p
_ = Offset -> String -> Q a
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q a) -> String -> Q a
forall a b. (a -> b) -> a -> b
$ String
"pCase: not usable in " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
ctx String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" context"

    extractProof :: String -> ExpQ
    extractProof :: String -> Q Exp
extractProof String
src =
      case String -> Maybe ((String, String), String)
parts String
src of
        Maybe ((String, String), String)
Nothing -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"pCase: Failed to parse a proof case-expression."
                                          , String
""
                                          , String
"           Instead of:   case      expr of alts"
                                          , String
"           Write     : [pCase|Type expr of alts|]"
                                          , String
""
                                          , String
"        where Type is the underlying concrete type of the expression."
                                          ]
        Just ((String
typ, String
scrutStr), String
altsStr) -> do
          let fullCase :: String
fullCase = String
"case " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
scrutStr String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" of " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
altsStr
              offsets :: [Offset]
offsets  = String -> [Offset]
findOffsets String
src
          case String -> Either String Exp
metaParse String
fullCase of
            Right (CaseE Exp
scrut [Match]
matches) -> do
              [[Case]]
cs <- (Offset -> Match -> Q [Case]) -> [Offset] -> [Match] -> Q [[Case]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Exp -> Offset -> Match -> Q [Case]
matchToPair Exp
scrut) ([Offset]
offsets [Offset] -> [Offset] -> [Offset]
forall a. [a] -> [a] -> [a]
++ Offset -> [Offset]
forall a. a -> [a]
repeat Offset
Unknown) [Match]
matches
              [Case]
validated <- String -> [Case] -> Q [Case]
checkProofCase String
typ ([[Case]] -> [Case]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Case]]
cs)
              Exp -> String -> [Case] -> Q Exp
buildProofCase Exp
scrut String
typ [Case]
validated
            Right Exp
_  -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
Unknown String
"pCase: Parse error, cannot extract a case-expression."
            Left String
err -> case String -> [String]
lines String
err of
                          (String
_:String
loc:[String]
res) | [String
"SrcLoc", String
_, String
l, String
c] <- String -> [String]
words String
loc, (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
l, (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
c
                             -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail (Int -> Int -> Int -> Offset
OffBy (String -> Int
forall a. Read a => String -> a
read String
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (String -> Int
forall a. Read a => String -> a
read String
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
1) ([String] -> String
unlines [String]
res)
                          [String]
_  -> Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
Unknown (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ String
"pCase parse error: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
err

    -- | Validate cases for proof context
    checkProofCase :: String -> [Case] -> Q [Case]
    checkProofCase :: String -> [Case] -> Q [Case]
checkProofCase String
typ [Case]
cases = do
        Loc
loc <- Q Loc
location

        [(Name, [Type])]
cstrs <- let dropFieldNames :: (a, [(a, b)]) -> (a, [b])
dropFieldNames (a
c, [(a, b)]
nts) = (a
c, ((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
nts)
                 in ((Name, [(Maybe Name, Type)]) -> (Name, [Type]))
-> [(Name, [(Maybe Name, Type)])] -> [(Name, [Type])]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [(Maybe Name, Type)]) -> (Name, [Type])
forall {a} {a} {b}. (a, [(a, b)]) -> (a, [b])
dropFieldNames ([(Name, [(Maybe Name, Type)])] -> [(Name, [Type])])
-> (([Name], [(Name, [(Maybe Name, Type)])])
    -> [(Name, [(Maybe Name, Type)])])
-> ([Name], [(Name, [(Maybe Name, Type)])])
-> [(Name, [Type])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], [(Name, [(Maybe Name, Type)])])
-> [(Name, [(Maybe Name, Type)])]
forall a b. (a, b) -> b
snd (([Name], [(Name, [(Maybe Name, Type)])]) -> [(Name, [Type])])
-> Q ([Name], [(Name, [(Maybe Name, Type)])]) -> Q [(Name, [Type])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructors (String -> Name
mkName String
typ)

        -- Validate wildcard placement: unguarded wildcard must be last, nothing after it
        let checkWild :: [Case] -> Q ()
checkWild []                         = () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            checkWild (CMatch{}          : [Case]
rest) = [Case] -> Q ()
checkWild [Case]
rest
            checkWild (CWild Offset
_ Just{}  Exp
_ : [Case]
rest) = [Case] -> Q ()
checkWild [Case]
rest
            checkWild (CWild Offset
o Maybe Exp
Nothing Exp
_ : [Case]
rest) =
                  case [Case]
rest of
                    []  -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                    [Case]
red -> Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"pCase: Wildcard makes the remaining matches redundant:"
                                            String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
"        " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Loc -> Case -> String
showCaseGen (Loc -> Maybe Loc
forall a. a -> Maybe a
Just Loc
loc) Case
r | Case
r <- [Case]
red]
        [Case] -> Q ()
checkWild [Case]
cases

        -- Wildcards must come after all explicit constructor matches
        let checkWildBeforeCstr :: [Case] -> Q ()
checkWildBeforeCstr [] = () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            checkWildBeforeCstr (CWild Offset
o Maybe Exp
_ Exp
_ : [Case]
rest)
              | (Case -> Bool) -> [Case] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\case CMatch{} -> Bool
True; Case
_ -> Bool
False) [Case]
rest
              = Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"pCase: Wildcard must come after all constructor matches:"
                                 String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
"        " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Loc -> Case -> String
showCaseGen (Loc -> Maybe Loc
forall a. a -> Maybe a
Just Loc
loc) Case
r | Case
r <- (Case -> Bool) -> [Case] -> [Case]
forall a. (a -> Bool) -> [a] -> [a]
filter (\case CMatch{} -> Bool
True; Case
_ -> Bool
False) [Case]
rest]
            checkWildBeforeCstr (Case
_ : [Case]
rest) = [Case] -> Q ()
checkWildBeforeCstr [Case]
rest
        [Case] -> Q ()
checkWildBeforeCstr [Case]
cases

        -- Check arity and constructor validity
        let chk1 :: Case -> Q ()
            chk1 :: Case -> Q ()
chk1 Case
c = case Case
c of
                       CMatch Offset
o Name
nm Maybe [Pat]
ps Maybe Exp
_ Exp
_ Set Name
_ -> Offset -> Name -> Maybe Int -> Q ()
isSafe Offset
o Name
nm ([Pat] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Pat] -> Int) -> Maybe [Pat] -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Pat]
ps)
                       CWild  {}            -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
              where isSafe :: Offset -> Name -> Maybe Int -> Q ()
isSafe Offset
o Name
nm Maybe Int
mbLen
                      | Just [Type]
ts <- Name
nm Name -> [(Name, [Type])] -> Maybe [Type]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Name, [Type])]
cstrs
                      = case Maybe Int
mbLen of
                           Maybe Int
Nothing  -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                           Just Int
cnt -> Bool -> Q () -> Q ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
cnt)
                                            (Q () -> Q ()) -> Q () -> Q ()
forall a b. (a -> b) -> a -> b
$ Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"pCase: Arity mismatch."
                                                               , String
"        Type       : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ
                                                               , String
"        Constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
nm
                                                               , String
"        Expected   : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts)
                                                               , String
"        Given      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
cnt
                                                               ]
                      | Bool
True
                      = Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail Offset
o (String -> Q ()) -> String -> Q ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"pCase: Unknown constructor:"
                                         , String
"        Type          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
typ
                                         , String
"        Saw           : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Ppr a => a -> String
pprint Name
nm
                                         , String
"        Must be one of: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (((Name, [Type]) -> String) -> [(Name, [Type])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> String
forall a. Ppr a => a -> String
pprint (Name -> String)
-> ((Name, [Type]) -> Name) -> (Name, [Type]) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, [Type]) -> Name
forall a b. (a, b) -> a
fst) [(Name, [Type])]
cstrs)
                                         ]

        (Case -> Q ()) -> [Case] -> Q ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Case -> Q ()
chk1 [Case]
cases

        -- Check overlap: unguarded constructor match followed by same constructor
        let chk2 :: [Case] -> Q ()
chk2 [] = () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            chk2 (c :: Case
c@(CMatch Offset
_ Name
nm Maybe [Pat]
_ Maybe Exp
Nothing Exp
_ Set Name
_) : [Case]
rest)
              = case (Case -> Bool) -> [Case] -> [Case]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Case
oc -> Case -> Maybe Name
getCaseConstructor Case
oc Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm) [Case]
rest of
                  [] -> [Case] -> Q ()
chk2 [Case]
rest
                  [Case]
os -> Loc -> Case -> [Case] -> Q ()
forall {a}. Loc -> Case -> [Case] -> Q a
overlap Loc
loc ([Case] -> Case
forall a. HasCallStack => [a] -> a
last [Case]
os) (Case
c Case -> [Case] -> [Case]
forall a. a -> [a] -> [a]
: [Case] -> [Case]
forall a. HasCallStack => [a] -> [a]
init [Case]
os)
            chk2 (Case
_ : [Case]
rest) = [Case] -> Q ()
chk2 [Case]
rest

        [Case] -> Q ()
chk2 [Case]
cases

        -- If every constructor has an unguarded match, any wildcard is redundant
        let fullyCovered :: [Name]
fullyCovered = [ Name
cstr | (Name
cstr, [Type]
_) <- [(Name, [Type])]
cstrs
                                  , (Case -> Bool) -> [Case] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Case
c -> Case -> Maybe Name
getCaseConstructor Case
c Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Maybe Name
forall a. a -> Maybe a
Just Name
cstr Bool -> Bool -> Bool
&& Bool -> Bool
not (Case -> Bool
isGuarded Case
c)) [Case]
cases
                                  ]
        case [Case
c | c :: Case
c@CWild{} <- [Case]
cases] of
          []    -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          (Case
c:[Case]
_) | [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
fullyCovered Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(Name, [Type])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, [Type])]
cstrs
                -> Offset -> String -> Q ()
forall a. Offset -> String -> Q a
fail (Case -> Offset
caseOffset Case
c) String
"pCase: Wildcard match is redundant"
                | Bool
True
                -> () -> Q ()
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

        -- No exhaustiveness check: the `cases` combinator checks completeness at proof time.
        [Case] -> Q [Case]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Case]
cases

    overlap :: Loc -> Case -> [Case] -> Q a
overlap Loc
loc Case
x [Case]
xs = Offset -> String -> Q a
forall a. Offset -> String -> Q a
fail (Case -> Offset
caseOffset Case
x) (String -> Q a) -> String -> Q a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
"pCase: Overlapping case constructors:"
                                                        , String
"        Constructor: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Case -> String
showCase Case
x
                                                        ]
                                                     [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"      Overlaps with:" ]
                                                     [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"        " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Loc -> Case -> String
showCaseGen (Loc -> Maybe Loc
forall a. a -> Maybe a
Just Loc
loc) Case
p | Case
p <- [Case]
xs]

    -- | Build the proof case expression
    buildProofCase :: Exp -> String -> [Case] -> ExpQ
    buildProofCase :: Exp -> String -> [Case] -> Q Exp
buildProofCase Exp
scrut String
typ [Case]
cases = do
        [(Name, [Type])]
cstrs <- let dropFieldNames :: (a, [(a, b)]) -> (a, [b])
dropFieldNames (a
c, [(a, b)]
nts) = (a
c, ((a, b) -> b) -> [(a, b)] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> b
forall a b. (a, b) -> b
snd [(a, b)]
nts)
                 in ((Name, [(Maybe Name, Type)]) -> (Name, [Type]))
-> [(Name, [(Maybe Name, Type)])] -> [(Name, [Type])]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [(Maybe Name, Type)]) -> (Name, [Type])
forall {a} {a} {b}. (a, [(a, b)]) -> (a, [b])
dropFieldNames ([(Name, [(Maybe Name, Type)])] -> [(Name, [Type])])
-> (([Name], [(Name, [(Maybe Name, Type)])])
    -> [(Name, [(Maybe Name, Type)])])
-> ([Name], [(Name, [(Maybe Name, Type)])])
-> [(Name, [Type])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Name], [(Name, [(Maybe Name, Type)])])
-> [(Name, [(Maybe Name, Type)])]
forall a b. (a, b) -> b
snd (([Name], [(Name, [(Maybe Name, Type)])]) -> [(Name, [Type])])
-> Q ([Name], [(Name, [(Maybe Name, Type)])]) -> Q [(Name, [Type])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Q ([Name], [(Name, [(Maybe Name, Type)])])
getConstructors (String -> Name
mkName String
typ)
        -- Collect guard variables for each constructor across all arms
        -- (needed to suppress false "unused binding" warnings for guard-only variables)
        let allGrdVars :: Map Name (Set Name)
            allGrdVars :: Map Name (Set Name)
allGrdVars = (Set Name -> Set Name -> Set Name)
-> [(Name, Set Name)] -> Map Name (Set Name)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.union
                           [ (Name
nm, Set Name -> (Exp -> Set Name) -> Maybe Exp -> Set Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Name
forall a. Set a
Set.empty Exp -> Set Name
freeVars Maybe Exp
mbG)
                           | CMatch Offset
_ Name
nm Maybe [Pat]
_ Maybe Exp
mbG Exp
_ Set Name
_ <- [Case]
cases ]
        [(Exp, Exp)]
allPairs <- Exp
-> [(Name, [Type])]
-> Map Name (Set Name)
-> [(Maybe Name, Exp, Maybe Exp)]
-> [Case]
-> Q [(Exp, Exp)]
processCases Exp
scrut [(Name, [Type])]
cstrs Map Name (Set Name)
allGrdVars [] [Case]
cases
        let casesName :: Name
casesName   = String -> Name
mkName String
"cases"
            impliesName :: Name
impliesName = String -> Name
mkName String
"==>"
            mkPair :: (Exp, Exp) -> Exp
mkPair (Exp
g, Exp
r) = Maybe Exp -> Exp -> Maybe Exp -> Exp
InfixE (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
g) (Name -> Exp
VarE Name
impliesName) (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
r)
        Exp -> Q Exp
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp
AppE (Name -> Exp
VarE Name
casesName) ([Exp] -> Exp
ListE (((Exp, Exp) -> Exp) -> [(Exp, Exp)] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Exp, Exp) -> Exp
mkPair [(Exp, Exp)]
allPairs))

    -- | Process all cases linearly, accumulating prior guards.
    -- Prior guards are tagged with their constructor name (Nothing for wildcards).
    -- Each entry stores (constructor, fullGuard, userGuardOnly):
    --   fullGuard    = the complete guard expression (used for wildcard De Morgan negation)
    --   userGuardOnly = Just the user guard part (used for same-constructor negation)
    --                   Nothing if unguarded (same-constructor arms don't negate unguarded matches)
    processCases :: Exp -> [(Name, [Type])] -> Map Name (Set Name) -> [(Maybe Name, Exp, Maybe Exp)] -> [Case] -> Q [(Exp, Exp)]
    processCases :: Exp
-> [(Name, [Type])]
-> Map Name (Set Name)
-> [(Maybe Name, Exp, Maybe Exp)]
-> [Case]
-> Q [(Exp, Exp)]
processCases Exp
_     [(Name, [Type])]
_     Map Name (Set Name)
_          [(Maybe Name, Exp, Maybe Exp)]
_           []         = [(Exp, Exp)] -> Q [(Exp, Exp)]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    processCases Exp
scrut [(Name, [Type])]
cstrs Map Name (Set Name)
allGrdVars [(Maybe Name, Exp, Maybe Exp)]
priorGuards (Case
c:[Case]
rest) = case Case
c of
      CWild Offset
_ Maybe Exp
mbG Exp
rhs -> do
        -- Wildcard: negate the disjunction of ALL prior full guards (De Morgan)
        let allGuards :: [Exp]
allGuards  = [Exp
g | (Maybe Name
_, Exp
g, Maybe Exp
_) <- [(Maybe Name, Exp, Maybe Exp)]
priorGuards]
            baseGuard :: Exp
baseGuard  = [Exp] -> Exp
negateAll [Exp]
allGuards
            finalGuard :: Exp
finalGuard = case Maybe Exp
mbG of
                           Maybe Exp
Nothing -> Exp
baseGuard
                           Just Exp
g  -> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.&&), Exp
baseGuard, Exp
g]
        [(Exp, Exp)]
rest' <- Exp
-> [(Name, [Type])]
-> Map Name (Set Name)
-> [(Maybe Name, Exp, Maybe Exp)]
-> [Case]
-> Q [(Exp, Exp)]
processCases Exp
scrut [(Name, [Type])]
cstrs Map Name (Set Name)
allGrdVars ([(Maybe Name, Exp, Maybe Exp)]
priorGuards [(Maybe Name, Exp, Maybe Exp)]
-> [(Maybe Name, Exp, Maybe Exp)] -> [(Maybe Name, Exp, Maybe Exp)]
forall a. [a] -> [a] -> [a]
++ [(Maybe Name
forall a. Maybe a
Nothing, Exp
finalGuard, Maybe Exp
forall a. Maybe a
Nothing)]) [Case]
rest
        [(Exp, Exp)] -> Q [(Exp, Exp)]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Exp, Exp)] -> Q [(Exp, Exp)]) -> [(Exp, Exp)] -> Q [(Exp, Exp)]
forall a b. (a -> b) -> a -> b
$ (Exp
finalGuard, Exp
rhs) (Exp, Exp) -> [(Exp, Exp)] -> [(Exp, Exp)]
forall a. a -> [a] -> [a]
: [(Exp, Exp)]
rest'

      CMatch Offset
_o Name
nm Maybe [Pat]
mbp Maybe Exp
mbG Exp
rhs Set Name
_allUsed -> do
        let ts :: [Type]
ts   = case Name -> [(Name, [Type])] -> Maybe [Type]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
nm [(Name, [Type])]
cstrs of
                     Just [Type]
t  -> [Type]
t
                     Maybe [Type]
Nothing -> String -> [Type]
forall a. HasCallStack => String -> a
error (String -> [Type]) -> String -> [Type]
forall a b. (a -> b) -> a -> b
$ String
"pCase: impossible: unknown constructor " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
nm
            pats :: [Pat]
pats = [Pat] -> Maybe [Pat] -> [Pat]
forall a. a -> Maybe a -> a
fromMaybe ((Type -> Pat) -> [Type] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Pat -> Type -> Pat
forall a b. a -> b -> a
const Pat
WildP) [Type]
ts) Maybe [Pat]
mbp

            -- Build let-bindings for pattern variables
            args :: [(Int, Exp)]
args    = [ (Int
i, Exp -> Exp -> Exp
AppE (Name -> Exp
VarE (String -> Name
mkName (String
"get" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i))) Exp
scrut)
                      | (Int
i, Type
_) <- [Int] -> [Type] -> [(Int, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1 :: Int) ..] [Type]
ts ]
            bindings :: [Dec]
bindings = [ Pat -> Body -> [Dec] -> Dec
ValD (Name -> Pat
VarP Name
v) (Exp -> Body
NormalB Exp
acc) []
                       | (Int
i, Exp
acc) <- [(Int, Exp)]
args, VarP Name
v <- [[Pat]
pats [Pat] -> Int -> Pat
forall a. HasCallStack => [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)] ]

            testerGuard :: Exp
testerGuard = Exp -> Exp -> Exp
AppE (Name -> Exp
VarE (String -> Name
mkName (String
"is" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
nameBase Name
nm))) Exp
scrut

            -- Only negate prior USER guards for the SAME constructor (others are mutually exclusive)
            sameUserGuards :: [Exp]
sameUserGuards = [ Exp
ug | (Just Name
cn, Exp
_, Just Exp
ug) <- [(Maybe Name, Exp, Maybe Exp)]
priorGuards, Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nm ]
            negPriors :: [Exp]
negPriors      = (Exp -> Exp) -> [Exp] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'sNot)) [Exp]
sameUserGuards

            -- Build the final guard (wrap user guard in bindings so pattern vars are in scope)
            grdVars :: Set Name
grdVars     = Set Name -> (Exp -> Set Name) -> Maybe Exp -> Set Name
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set Name
forall a. Set a
Set.empty Exp -> Set Name
freeVars Maybe Exp
mbG
            grdBindings :: [Dec]
grdBindings = (Dec -> Bool) -> [Dec] -> [Dec]
forall a. (a -> Bool) -> [a] -> [a]
filter (\case
                                     ValD (VarP Name
v) Body
_ [Dec]
_ -> Name
v Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
grdVars
                                     Dec
_                 -> Bool
True) [Dec]
bindings
            guardParts :: [Exp]
guardParts  = [Exp
testerGuard] [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ [Exp]
negPriors [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ [Exp] -> (Exp -> [Exp]) -> Maybe Exp -> [Exp]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Exp -> [Exp]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> [Exp]) -> (Exp -> Exp) -> Exp -> [Exp]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Dec] -> Exp -> Exp
addLocals [Dec]
grdBindings) Maybe Exp
mbG
            finalGuard :: Exp
finalGuard  = case [Exp]
guardParts of
                            []  -> Name -> Exp
VarE 'sTrue
                            [Exp
g] -> Exp
g
                            [Exp]
gs  -> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (\Exp
a Exp
b -> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.&&), Exp
a, Exp
b]) [Exp]
gs

            -- Wrap RHS with let-bindings; include all bindings except those
            -- used in any guard of the same constructor but not in this RHS
            -- (to avoid false "unused" warnings from GHC for guard-only variables)
            cstrGrdVars :: Set Name
cstrGrdVars = Set Name -> Name -> Map Name (Set Name) -> Set Name
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set Name
forall a. Set a
Set.empty Name
nm Map Name (Set Name)
allGrdVars
            rhsVars :: Set Name
rhsVars = Exp -> Set Name
freeVars Exp
rhs
            rhs' :: Exp
rhs'    = [Dec] -> Exp -> Exp
addLocals ((Dec -> Bool) -> [Dec] -> [Dec]
forall a. (a -> Bool) -> [a] -> [a]
filter (\case
                                            ValD (VarP Name
v) Body
_ [Dec]
_ -> Bool -> Bool
not (Name
v Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
cstrGrdVars) Bool -> Bool -> Bool
|| Name
v Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
rhsVars
                                            Dec
_                 -> Bool
True) [Dec]
bindings) Exp
rhs

            -- Track: full guard for wildcard negation, user guard for same-constructor negation
            userGuardOnly :: Maybe Exp
userGuardOnly = case Maybe Exp
mbG of
                              Just Exp
g  -> Exp -> Maybe Exp
forall a. a -> Maybe a
Just ([Dec] -> Exp -> Exp
addLocals [Dec]
grdBindings Exp
g)
                              Maybe Exp
Nothing -> Maybe Exp
forall a. Maybe a
Nothing
            priorGuards' :: [(Maybe Name, Exp, Maybe Exp)]
priorGuards' = [(Maybe Name, Exp, Maybe Exp)]
priorGuards [(Maybe Name, Exp, Maybe Exp)]
-> [(Maybe Name, Exp, Maybe Exp)] -> [(Maybe Name, Exp, Maybe Exp)]
forall a. [a] -> [a] -> [a]
++ [(Name -> Maybe Name
forall a. a -> Maybe a
Just Name
nm, Exp
finalGuard, Maybe Exp
userGuardOnly)]

        [(Exp, Exp)]
rest' <- Exp
-> [(Name, [Type])]
-> Map Name (Set Name)
-> [(Maybe Name, Exp, Maybe Exp)]
-> [Case]
-> Q [(Exp, Exp)]
processCases Exp
scrut [(Name, [Type])]
cstrs Map Name (Set Name)
allGrdVars [(Maybe Name, Exp, Maybe Exp)]
priorGuards' [Case]
rest
        [(Exp, Exp)] -> Q [(Exp, Exp)]
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Exp, Exp)] -> Q [(Exp, Exp)]) -> [(Exp, Exp)] -> Q [(Exp, Exp)]
forall a b. (a -> b) -> a -> b
$ (Exp
finalGuard, Exp
rhs') (Exp, Exp) -> [(Exp, Exp)] -> [(Exp, Exp)]
forall a. a -> [a] -> [a]
: [(Exp, Exp)]
rest'

    -- | Negate the disjunction of all given guards using De Morgan: sNot (g1 .|| g2 .|| ...)
    negateAll :: [Exp] -> Exp
    negateAll :: [Exp] -> Exp
negateAll [] = Name -> Exp
VarE 'sTrue
    negateAll [Exp]
gs = Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'sNot) ((Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (\Exp
a Exp
b -> (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.||), Exp
a, Exp
b]) [Exp]
gs)

-- * Standalone helpers

-- | Free variables = used – bound
freeVars :: Exp -> Set Name
freeVars :: Exp -> Set Name
freeVars Exp
e = Exp -> Set Name
usedVars Exp
e Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Exp -> Set Name
boundVars Exp
e
 where boundVars :: Exp -> Set Name
       boundVars :: Exp -> Set Name
boundVars = (Set Name -> Set Name -> Set Name)
-> GenericQ (Set Name) -> GenericQ (Set Name)
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set Name -> (Pat -> Set Name) -> a -> Set Name
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ Set Name
forall a. Set a
Set.empty Pat -> Set Name
f)
         where f :: Pat -> Set Name
               f :: Pat -> Set Name
f (VarP Name
n)  = Name -> Set Name
forall a. a -> Set a
Set.singleton Name
n
               f (AsP Name
n Pat
_) = Name -> Set Name
forall a. a -> Set a
Set.singleton Name
n
               f Pat
_         = Set Name
forall a. Set a
Set.empty

       usedVars :: Exp -> Set Name
       usedVars :: Exp -> Set Name
usedVars = (Set Name -> Set Name -> Set Name)
-> GenericQ (Set Name) -> GenericQ (Set Name)
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything Set Name -> Set Name -> Set Name
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set Name -> (Exp -> Set Name) -> a -> Set Name
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ Set Name
forall a. Set a
Set.empty Exp -> Set Name
f)
         where f :: Exp -> Set Name
               f :: Exp -> Set Name
f (VarE Name
n) = Name -> Set Name
forall a. a -> Set a
Set.singleton Name
n
               f Exp
_        = Set Name
forall a. Set a
Set.empty

-- | Count the number of arguments in a constructor type by counting arrows.
-- e.g., @Integer -> String -> Bool@ has 2 arguments.
-- Handles both plain ArrowT and multiplicity-annotated arrows (MulArrowT).
countArgs :: Type -> Int
countArgs :: Type -> Int
countArgs (AppT (AppT Type
ArrowT Type
_) Type
rest)            = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
countArgs Type
rest
countArgs (AppT (AppT (AppT Type
MulArrowT Type
_) Type
_) Type
rest) = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Type -> Int
countArgs Type
rest
countArgs (ForallT [TyVarBndr Specificity]
_ [Type]
_ Type
t)                         = Type -> Int
countArgs Type
t
countArgs Type
_                                       = Int
0

-- | Generate a symbolic equality guard for a literal pattern.
-- @litToEq off arg lit@ produces the expression @arg .== litVal@.
-- For integers, the literal is used directly (relying on @fromInteger@).
-- For strings, the literal is wrapped with @literal@ to convert @String@ to @SString@.
-- Only integer and string literals are supported; others produce a compile error.
litToEq :: Offset -> Exp -> Lit -> Q Exp
litToEq :: Offset -> Exp -> Lit -> Q Exp
litToEq Offset
_   Exp
arg (IntegerL Integer
n) = Exp -> Q Exp
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.==), Exp
arg, Lit -> Exp
LitE (Integer -> Lit
IntegerL Integer
n)]
litToEq Offset
_   Exp
arg (StringL  String
s) = Exp -> Q Exp
forall a. a -> Q a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> Q Exp) -> Exp -> Q Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [Exp] -> Exp
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Exp -> Exp -> Exp
AppE [Name -> Exp
VarE '(.==), Exp
arg, Exp -> Exp -> Exp
AppE (Name -> Exp
VarE 'literal) (Lit -> Exp
LitE (String -> Lit
StringL String
s))]
litToEq Offset
off Exp
_   Lit
lit          = Offset -> String -> Q Exp
forall a. Offset -> String -> Q a
fail Offset
off (String -> Q Exp) -> String -> Q Exp
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
  [ String
"sCase/pCase: Unsupported literal in pattern: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Lit -> String
forall a. Show a => a -> String
show Lit
lit
  , String
"       Only integer and string literals are supported."
  ]