{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns #-}

module Unison.Runtime.Pattern
  ( DataSpec,
    splitPatterns,
    builtinDataSpec,
  )
where

import Control.Monad.State (State, evalState, modify, runState, state)
import Data.List (transpose)
import Data.Map.Strict
  ( fromListWith,
    insertWith,
  )
import Data.Map.Strict qualified as Map
import Data.Set (member)
import Data.Set qualified as Set
import Unison.ABT
  ( absChain',
    renames,
    visitPure,
    pattern AbsN',
  )
import Unison.Builtin.Decls (builtinDataDecls, builtinEffectDecls)
import Unison.ConstructorReference (ConstructorReference, GConstructorReference (..))
import Unison.ConstructorReference qualified as ConstructorReference
import Unison.DataDeclaration (declFields)
import Unison.Pattern
import Unison.Pattern qualified as P
import Unison.Prelude hiding (guard)
import Unison.Reference (Reference, Reference' (Builtin, DerivedId))
import Unison.Runtime.ANF (internalBug)
import Unison.Term hiding (Term, matchPattern)
import Unison.Term qualified as Tm
import Unison.Type qualified as Rf
import Unison.Var (Type (Pattern), Var, freshIn, freshenId, typed)

type Term v = Tm.Term v ()

-- Represents the number of fields of constructors of a data type/
-- ability in order of constructors
type Cons = [Int]

type NCons = [(Int, Int)]

-- Maps references to the constructor information for abilities (left)
-- and data types (right)
type DataSpec = Map Reference (Either Cons Cons)

data PType = PData Reference | PReq (Set Reference) | Unknown

instance Semigroup PType where
  PType
Unknown <> :: PType -> PType -> PType
<> PType
r = PType
r
  PType
l <> PType
Unknown = PType
l
  t :: PType
t@(PData Reference
l) <> PData Reference
r
    | Reference
l Reference -> Reference -> Bool
forall a. Eq a => a -> a -> Bool
== Reference
r = PType
t
  PReq Set Reference
l <> PReq Set Reference
r = Set Reference -> PType
PReq (Set Reference
l Set Reference -> Set Reference -> Set Reference
forall a. Semigroup a => a -> a -> a
<> Set Reference
r)
  PType
_ <> PType
_ = [Char] -> PType
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"inconsistent pattern matching types"

instance Monoid PType where
  mempty :: PType
mempty = PType
Unknown

type Ctx v = Map v PType

-- Representation of a row in a pattern compilation matrix.
-- There is a list of patterns annotated with the variables they
-- are matching against, an optional guard, and the body of the
-- 'match' clause associated with this row.
data PatternRow v = PR
  { forall v. PatternRow v -> [Pattern v]
matches :: [Pattern v],
    forall v. PatternRow v -> Maybe (Term v)
guard :: Maybe (Term v),
    forall v. PatternRow v -> Term v
body :: Term v
  }
  deriving (Int -> PatternRow v -> ShowS
[PatternRow v] -> ShowS
PatternRow v -> [Char]
(Int -> PatternRow v -> ShowS)
-> (PatternRow v -> [Char])
-> ([PatternRow v] -> ShowS)
-> Show (PatternRow v)
forall v. Show v => Int -> PatternRow v -> ShowS
forall v. Show v => [PatternRow v] -> ShowS
forall v. Show v => PatternRow v -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> PatternRow v -> ShowS
showsPrec :: Int -> PatternRow v -> ShowS
$cshow :: forall v. Show v => PatternRow v -> [Char]
show :: PatternRow v -> [Char]
$cshowList :: forall v. Show v => [PatternRow v] -> ShowS
showList :: [PatternRow v] -> ShowS
Show)

-- This is the data and ability 'constructor' information for all
-- the things defined in Haskell source code.
builtinDataSpec :: DataSpec
builtinDataSpec :: DataSpec
builtinDataSpec = [(Reference, Either Cons Cons)] -> DataSpec
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Reference, Either Cons Cons)]
forall {t}. [(Reference' t Hash, Either Cons Cons)]
decls
  where
    decls :: [(Reference' t Hash, Either Cons Cons)]
decls =
      [ (Id' Hash -> Reference' t Hash
forall h t. Id' h -> Reference' t h
DerivedId Id' Hash
x, Decl Symbol () -> Either Cons Cons
forall v a. Var v => Decl v a -> Either Cons Cons
declFields (Decl Symbol () -> Either Cons Cons)
-> Decl Symbol () -> Either Cons Cons
forall a b. (a -> b) -> a -> b
$ DataDeclaration Symbol () -> Decl Symbol ()
forall a b. b -> Either a b
Right DataDeclaration Symbol ()
y)
        | (Symbol
_, Id' Hash
x, DataDeclaration Symbol ()
y) <- [(Symbol, Id' Hash, DataDeclaration Symbol ())]
builtinDataDecls
      ]
        [(Reference' t Hash, Either Cons Cons)]
-> [(Reference' t Hash, Either Cons Cons)]
-> [(Reference' t Hash, Either Cons Cons)]
forall a. [a] -> [a] -> [a]
++ [ (Id' Hash -> Reference' t Hash
forall h t. Id' h -> Reference' t h
DerivedId Id' Hash
x, Decl Symbol () -> Either Cons Cons
forall v a. Var v => Decl v a -> Either Cons Cons
declFields (Decl Symbol () -> Either Cons Cons)
-> Decl Symbol () -> Either Cons Cons
forall a b. (a -> b) -> a -> b
$ EffectDeclaration Symbol () -> Decl Symbol ()
forall a b. a -> Either a b
Left EffectDeclaration Symbol ()
y)
             | (Symbol
_, Id' Hash
x, EffectDeclaration Symbol ()
y) <- [(Symbol, Id' Hash, EffectDeclaration Symbol ())]
builtinEffectDecls
           ]

-- A pattern compilation matrix is just a list of rows. There is
-- no need for the rows to have uniform length; the variable
-- annotations on the patterns in the rows keep track of what
-- should be matched against when decomposing a matrix.
data PatternMatrix v = PM {forall v. PatternMatrix v -> [PatternRow v]
_rows :: [PatternRow v]}
  deriving (Int -> PatternMatrix v -> ShowS
[PatternMatrix v] -> ShowS
PatternMatrix v -> [Char]
(Int -> PatternMatrix v -> ShowS)
-> (PatternMatrix v -> [Char])
-> ([PatternMatrix v] -> ShowS)
-> Show (PatternMatrix v)
forall v. Show v => Int -> PatternMatrix v -> ShowS
forall v. Show v => [PatternMatrix v] -> ShowS
forall v. Show v => PatternMatrix v -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> PatternMatrix v -> ShowS
showsPrec :: Int -> PatternMatrix v -> ShowS
$cshow :: forall v. Show v => PatternMatrix v -> [Char]
show :: PatternMatrix v -> [Char]
$cshowList :: forall v. Show v => [PatternMatrix v] -> ShowS
showList :: [PatternMatrix v] -> ShowS
Show)

usedVars :: (Ord v) => PatternMatrix v -> Set v
usedVars :: forall v. Ord v => PatternMatrix v -> Set v
usedVars (PM [PatternRow v]
rs) = (PatternRow v -> Set v) -> [PatternRow v] -> Set v
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap PatternRow v -> Set v
usedR [PatternRow v]
rs
  where
    usedR :: PatternRow v -> Set v
usedR (PR [Pattern v]
ps Maybe (Term v)
g Term v
b) =
      (Pattern v -> Set v) -> [Pattern v] -> Set v
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pattern v -> Set v
usedP [Pattern v]
ps Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> (Term v -> Set v) -> Maybe (Term v) -> Set v
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Term v -> Set v
forall vt v a. Term' vt v a -> Set v
freeVars Maybe (Term v)
g Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Term v -> Set v
forall vt v a. Term' vt v a -> Set v
freeVars Term v
b
    usedP :: Pattern v -> Set v
usedP = (v -> Set v) -> Pattern v -> Set v
forall m a. Monoid m => (a -> m) -> Pattern a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap v -> Set v
forall a. a -> Set a
Set.singleton

-- Heuristics guide the pattern compilation. They inspect the
-- pattern matrix and (may) choose a variable to split on next.
-- The full strategy will consist of multiple heuristics composed
-- in series.
type Heuristic v = PatternMatrix v -> Maybe v

choose :: [Heuristic v] -> PatternMatrix v -> v
choose :: forall v. [Heuristic v] -> PatternMatrix v -> v
choose [] (PM (PR (Pattern v
p : [Pattern v]
_) Maybe (Term v)
_ Term v
_ : [PatternRow v]
_)) = Pattern v -> v
forall loc. Pattern loc -> loc
loc Pattern v
p
choose [] PatternMatrix v
_ =
  [Char] -> v
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"pattern matching: failed to choose a splitting"
choose (Heuristic v
h : [Heuristic v]
hs) PatternMatrix v
m
  | Just v
i <- Heuristic v
h PatternMatrix v
m = v
i
  | Bool
otherwise = [Heuristic v] -> PatternMatrix v -> v
forall v. [Heuristic v] -> PatternMatrix v -> v
choose [Heuristic v]
hs PatternMatrix v
m

refutable :: P.Pattern a -> Bool
refutable :: forall a. Pattern a -> Bool
refutable (P.Unbound a
_) = Bool
False
refutable (P.Var a
_) = Bool
False
refutable Pattern a
_ = Bool
True

rowIrrefutable :: PatternRow v -> Bool
rowIrrefutable :: forall v. PatternRow v -> Bool
rowIrrefutable (PR [Pattern v]
ps Maybe (Term v)
_ Term v
_) = [Pattern v] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Pattern v]
ps

firstRow :: ([P.Pattern v] -> Maybe v) -> Heuristic v
firstRow :: forall v. ([Pattern v] -> Maybe v) -> Heuristic v
firstRow [Pattern v] -> Maybe v
f (PM (PatternRow v
r : [PatternRow v]
_)) = [Pattern v] -> Maybe v
f ([Pattern v] -> Maybe v) -> [Pattern v] -> Maybe v
forall a b. (a -> b) -> a -> b
$ PatternRow v -> [Pattern v]
forall v. PatternRow v -> [Pattern v]
matches PatternRow v
r
firstRow [Pattern v] -> Maybe v
_ PatternMatrix v
_ = Maybe v
forall a. Maybe a
Nothing

heuristics :: [Heuristic v]
heuristics :: forall v. [Heuristic v]
heuristics = [([Pattern v] -> Maybe v) -> Heuristic v
forall v. ([Pattern v] -> Maybe v) -> Heuristic v
firstRow (([Pattern v] -> Maybe v) -> Heuristic v)
-> ([Pattern v] -> Maybe v) -> Heuristic v
forall a b. (a -> b) -> a -> b
$ (Pattern v -> v) -> Maybe (Pattern v) -> Maybe v
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern v -> v
forall loc. Pattern loc -> loc
loc (Maybe (Pattern v) -> Maybe v)
-> ([Pattern v] -> Maybe (Pattern v)) -> [Pattern v] -> Maybe v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Pattern v] -> Maybe (Pattern v)
forall a. [a] -> Maybe a
listToMaybe]

extractVar :: (Var v) => P.Pattern v -> Maybe v
extractVar :: forall v. Var v => Pattern v -> Maybe v
extractVar Pattern v
p
  | P.Unbound {} <- Pattern v
p = Maybe v
forall a. Maybe a
Nothing
  | Bool
otherwise = v -> Maybe v
forall a. a -> Maybe a
Just (Pattern v -> v
forall loc. Pattern loc -> loc
loc Pattern v
p)

extractVars :: (Var v) => [P.Pattern v] -> [v]
extractVars :: forall v. Var v => [Pattern v] -> [v]
extractVars = [Maybe v] -> [v]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe v] -> [v])
-> ([Pattern v] -> [Maybe v]) -> [Pattern v] -> [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern v -> Maybe v) -> [Pattern v] -> [Maybe v]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern v -> Maybe v
forall v. Var v => Pattern v -> Maybe v
extractVar

-- Splits a data type pattern, yielding its subpatterns. The provided
-- integers are the tag and number of fields for the constructor being
-- matched against. A constructor pattern thus only yields results if
-- it matches the tag (and number of subpatterns as a consistency
-- check), while variables can also match and know how many subpatterns
-- to yield.
--
-- The outer list indicates success of the match. It could be Maybe,
-- but elsewhere these results are added to a list, so it is more
-- convenient to yield a list here.
decomposePattern ::
  (Var v) =>
  Maybe Reference ->
  Int ->
  Int ->
  P.Pattern v ->
  [[P.Pattern v]]
decomposePattern :: forall v.
Var v =>
Maybe Reference -> Int -> Int -> Pattern v -> [[Pattern v]]
decomposePattern (Just Reference
rf0) Int
t Int
_ (P.Boolean v
_ Bool
b)
  | Reference
rf0 Reference -> Reference -> Bool
forall a. Eq a => a -> a -> Bool
== Reference
Rf.booleanRef,
    Int
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== if Bool
b then Int
1 else Int
0 =
      [[]]
decomposePattern (Just Reference
rf0) Int
t Int
nfields p :: Pattern v
p@(P.Constructor v
_ (ConstructorReference Reference
rf ConstructorId
u) [Pattern v]
ps)
  | Int
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== ConstructorId -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ConstructorId
u,
    Reference
rf0 Reference -> Reference -> Bool
forall a. Eq a => a -> a -> Bool
== Reference
rf =
      if [Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nfields
        then [[Pattern v]
ps]
        else [Char] -> [[Pattern v]]
forall a. HasCallStack => [Char] -> a
internalBug [Char]
err
  where
    err :: [Char]
err =
      [Char]
"decomposePattern: wrong number of constructor fields: "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Pattern v) -> [Char]
forall a. Show a => a -> [Char]
show (Int
nfields, Pattern v
p)
decomposePattern (Just Reference
rf0) Int
t Int
nfields p :: Pattern v
p@(P.EffectBind v
_ (ConstructorReference Reference
rf ConstructorId
u) [Pattern v]
ps Pattern v
pk)
  | Int
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== ConstructorId -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ConstructorId
u,
    Reference
rf0 Reference -> Reference -> Bool
forall a. Eq a => a -> a -> Bool
== Reference
rf =
      if [Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nfields
        then [[Pattern v]
ps [Pattern v] -> [Pattern v] -> [Pattern v]
forall a. [a] -> [a] -> [a]
++ [Pattern v
pk]]
        else [Char] -> [[Pattern v]]
forall a. HasCallStack => [Char] -> a
internalBug [Char]
err
  where
    err :: [Char]
err =
      [Char]
"decomposePattern: wrong number of ability fields: "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Pattern v) -> [Char]
forall a. Show a => a -> [Char]
show (Int
nfields, Pattern v
p)
decomposePattern Maybe Reference
_ Int
t Int
_ (P.EffectPure v
_ Pattern v
p)
  | Int
t Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== -Int
1 = [[Pattern v
p]]
decomposePattern Maybe Reference
_ Int
_ Int
nfields (P.Var v
_) =
  [Int -> Pattern v -> [Pattern v]
forall a. Int -> a -> [a]
replicate Int
nfields (v -> Pattern v
forall loc. loc -> Pattern loc
P.Unbound (Type -> v
forall v. Var v => Type -> v
typed Type
Pattern))]
decomposePattern Maybe Reference
_ Int
_ Int
nfields (P.Unbound v
_) =
  [Int -> Pattern v -> [Pattern v]
forall a. Int -> a -> [a]
replicate Int
nfields (v -> Pattern v
forall loc. loc -> Pattern loc
P.Unbound (Type -> v
forall v. Var v => Type -> v
typed Type
Pattern))]
decomposePattern Maybe Reference
_ Int
_ Int
_ (P.SequenceLiteral v
_ [Pattern v]
_) =
  [Char] -> [[Pattern v]]
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"decomposePattern: sequence literal"
decomposePattern Maybe Reference
_ Int
_ Int
_ Pattern v
_ = []

matchBuiltin :: P.Pattern a -> Maybe (P.Pattern ())
matchBuiltin :: forall a. Pattern a -> Maybe (Pattern ())
matchBuiltin (P.Var a
_) = Pattern () -> Maybe (Pattern ())
forall a. a -> Maybe a
Just (Pattern () -> Maybe (Pattern ()))
-> Pattern () -> Maybe (Pattern ())
forall a b. (a -> b) -> a -> b
$ () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound ()
matchBuiltin (P.Unbound a
_) = Pattern () -> Maybe (Pattern ())
forall a. a -> Maybe a
Just (Pattern () -> Maybe (Pattern ()))
-> Pattern () -> Maybe (Pattern ())
forall a b. (a -> b) -> a -> b
$ () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound ()
matchBuiltin (P.Nat a
_ ConstructorId
n) = Pattern () -> Maybe (Pattern ())
forall a. a -> Maybe a
Just (Pattern () -> Maybe (Pattern ()))
-> Pattern () -> Maybe (Pattern ())
forall a b. (a -> b) -> a -> b
$ () -> ConstructorId -> Pattern ()
forall loc. loc -> ConstructorId -> Pattern loc
P.Nat () ConstructorId
n
matchBuiltin (P.Int a
_ Int64
n) = Pattern () -> Maybe (Pattern ())
forall a. a -> Maybe a
Just (Pattern () -> Maybe (Pattern ()))
-> Pattern () -> Maybe (Pattern ())
forall a b. (a -> b) -> a -> b
$ () -> Int64 -> Pattern ()
forall loc. loc -> Int64 -> Pattern loc
P.Int () Int64
n
matchBuiltin (P.Text a
_ Text
t) = Pattern () -> Maybe (Pattern ())
forall a. a -> Maybe a
Just (Pattern () -> Maybe (Pattern ()))
-> Pattern () -> Maybe (Pattern ())
forall a b. (a -> b) -> a -> b
$ () -> Text -> Pattern ()
forall loc. loc -> Text -> Pattern loc
P.Text () Text
t
matchBuiltin (P.Char a
_ Char
c) = Pattern () -> Maybe (Pattern ())
forall a. a -> Maybe a
Just (Pattern () -> Maybe (Pattern ()))
-> Pattern () -> Maybe (Pattern ())
forall a b. (a -> b) -> a -> b
$ () -> Char -> Pattern ()
forall loc. loc -> Char -> Pattern loc
P.Char () Char
c
matchBuiltin (P.Float a
_ Double
d) = Pattern () -> Maybe (Pattern ())
forall a. a -> Maybe a
Just (Pattern () -> Maybe (Pattern ()))
-> Pattern () -> Maybe (Pattern ())
forall a b. (a -> b) -> a -> b
$ () -> Double -> Pattern ()
forall loc. loc -> Double -> Pattern loc
P.Float () Double
d
matchBuiltin Pattern a
_ = Maybe (Pattern ())
forall a. Maybe a
Nothing

-- Represents the various cases that that may occur when performing
-- a sequence match. These fall into two groups:
--
--   E, C, S: empty, cons, snoc
--   L, R, DL, DR: split left/right, insufficient elements
--
-- These groups correspond to different sorts of matches we can compile
-- to. We can view the left/right end of a sequence, or attempt to
-- split a sequence at a specified offset from the left/right side.
data SeqMatch = E | C | S | L Int | R Int | DL Int | DR Int
  deriving (SeqMatch -> SeqMatch -> Bool
(SeqMatch -> SeqMatch -> Bool)
-> (SeqMatch -> SeqMatch -> Bool) -> Eq SeqMatch
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SeqMatch -> SeqMatch -> Bool
== :: SeqMatch -> SeqMatch -> Bool
$c/= :: SeqMatch -> SeqMatch -> Bool
/= :: SeqMatch -> SeqMatch -> Bool
Eq, Eq SeqMatch
Eq SeqMatch =>
(SeqMatch -> SeqMatch -> Ordering)
-> (SeqMatch -> SeqMatch -> Bool)
-> (SeqMatch -> SeqMatch -> Bool)
-> (SeqMatch -> SeqMatch -> Bool)
-> (SeqMatch -> SeqMatch -> Bool)
-> (SeqMatch -> SeqMatch -> SeqMatch)
-> (SeqMatch -> SeqMatch -> SeqMatch)
-> Ord SeqMatch
SeqMatch -> SeqMatch -> Bool
SeqMatch -> SeqMatch -> Ordering
SeqMatch -> SeqMatch -> SeqMatch
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SeqMatch -> SeqMatch -> Ordering
compare :: SeqMatch -> SeqMatch -> Ordering
$c< :: SeqMatch -> SeqMatch -> Bool
< :: SeqMatch -> SeqMatch -> Bool
$c<= :: SeqMatch -> SeqMatch -> Bool
<= :: SeqMatch -> SeqMatch -> Bool
$c> :: SeqMatch -> SeqMatch -> Bool
> :: SeqMatch -> SeqMatch -> Bool
$c>= :: SeqMatch -> SeqMatch -> Bool
>= :: SeqMatch -> SeqMatch -> Bool
$cmax :: SeqMatch -> SeqMatch -> SeqMatch
max :: SeqMatch -> SeqMatch -> SeqMatch
$cmin :: SeqMatch -> SeqMatch -> SeqMatch
min :: SeqMatch -> SeqMatch -> SeqMatch
Ord, Int -> SeqMatch -> ShowS
[SeqMatch] -> ShowS
SeqMatch -> [Char]
(Int -> SeqMatch -> ShowS)
-> (SeqMatch -> [Char]) -> ([SeqMatch] -> ShowS) -> Show SeqMatch
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SeqMatch -> ShowS
showsPrec :: Int -> SeqMatch -> ShowS
$cshow :: SeqMatch -> [Char]
show :: SeqMatch -> [Char]
$cshowList :: [SeqMatch] -> ShowS
showList :: [SeqMatch] -> ShowS
Show)

seqPSize :: P.Pattern v -> Maybe Int
seqPSize :: forall v. Pattern v -> Maybe Int
seqPSize (P.SequenceLiteral v
_ [Pattern v]
l) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ [Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
l
seqPSize (P.SequenceOp v
_ Pattern v
_ SeqOp
Cons Pattern v
r) = (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
r
seqPSize (P.SequenceOp v
_ Pattern v
l SeqOp
Snoc Pattern v
_) = (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
l
seqPSize (P.SequenceOp v
_ Pattern v
l SeqOp
Concat Pattern v
r) = Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) (Int -> Int -> Int) -> Maybe Int -> Maybe (Int -> Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
l Maybe (Int -> Int) -> Maybe Int -> Maybe Int
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
r
seqPSize Pattern v
_ = Maybe Int
forall a. Maybe a
Nothing

-- Decides a sequence matching operation to perform based on a column
-- of patterns that match against it. Literals do not really force a
-- bias, so the decision of which side to view is postponed to
-- subsequent patterns if we encounter a literal first. A literal with
-- priority does block a splitting pattern, though.
decideSeqPat :: [P.Pattern v] -> [SeqMatch]
decideSeqPat :: forall v. [Pattern v] -> [SeqMatch]
decideSeqPat = Bool -> [Pattern v] -> [SeqMatch]
forall {v}. Bool -> [Pattern v] -> [SeqMatch]
go Bool
False
  where
    go :: Bool -> [Pattern v] -> [SeqMatch]
go Bool
_ [] = [SeqMatch
E, SeqMatch
C]
    go Bool
_ (P.SequenceLiteral {} : [Pattern v]
ps) = Bool -> [Pattern v] -> [SeqMatch]
go Bool
True [Pattern v]
ps
    go Bool
_ (P.SequenceOp v
_ Pattern v
_ SeqOp
Snoc Pattern v
_ : [Pattern v]
_) = [SeqMatch
E, SeqMatch
S]
    go Bool
_ (P.SequenceOp v
_ Pattern v
_ SeqOp
Cons Pattern v
_ : [Pattern v]
_) = [SeqMatch
E, SeqMatch
C]
    go Bool
guard (P.SequenceOp v
_ Pattern v
l SeqOp
Concat Pattern v
r : [Pattern v]
_)
      | Bool
guard = [SeqMatch
E, SeqMatch
C] -- prefer prior literals
      | Just Int
n <- Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
l = [Int -> SeqMatch
L Int
n, Int -> SeqMatch
DL Int
n]
      | Just Int
n <- Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
r = [Int -> SeqMatch
R Int
n, Int -> SeqMatch
DR Int
n]
    go Bool
b (P.Unbound v
_ : [Pattern v]
ps) = Bool -> [Pattern v] -> [SeqMatch]
go Bool
b [Pattern v]
ps
    go Bool
b (P.Var v
_ : [Pattern v]
ps) = Bool -> [Pattern v] -> [SeqMatch]
go Bool
b [Pattern v]
ps
    go Bool
_ (Pattern v
p : [Pattern v]
_) =
      [Char] -> [SeqMatch]
forall a. HasCallStack => [Char] -> a
internalBug ([Char] -> [SeqMatch]) -> [Char] -> [SeqMatch]
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot process sequence pattern: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Pattern v -> [Char]
forall a. Show a => a -> [Char]
show Pattern v
p

-- Represents the possible correspondences between a sequence pattern
-- and a sequence matching compilation target. Unlike data matching,
-- where a pattern either matches or is disjoint from a tag, sequence
-- patterns can overlap in non-trivial ways where it would be difficult
-- to avoid re-testing the original list.
data SeqCover v
  = Cover [P.Pattern v]
  | Disjoint
  | Overlap

-- Determines how a pattern corresponds to a sequence matching
-- compilation target.
decomposeSeqP :: (Var v) => Set v -> SeqMatch -> P.Pattern v -> SeqCover v
decomposeSeqP :: forall v. Var v => Set v -> SeqMatch -> Pattern v -> SeqCover v
decomposeSeqP Set v
_ SeqMatch
E (P.SequenceLiteral v
_ []) = [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover []
decomposeSeqP Set v
_ SeqMatch
E Pattern v
_ = SeqCover v
forall v. SeqCover v
Disjoint
decomposeSeqP Set v
_ SeqMatch
C (P.SequenceOp v
_ Pattern v
l SeqOp
Cons Pattern v
r) = [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover [Pattern v
l, Pattern v
r]
decomposeSeqP Set v
_ SeqMatch
C (P.SequenceOp v
_ Pattern v
_ SeqOp
Concat Pattern v
_) = SeqCover v
forall v. SeqCover v
Overlap
decomposeSeqP Set v
_ SeqMatch
C (P.SequenceLiteral v
_ []) = SeqCover v
forall v. SeqCover v
Disjoint
decomposeSeqP Set v
avoid SeqMatch
C (P.SequenceLiteral v
_ (Pattern v
p : [Pattern v]
ps)) =
  [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover [Pattern v
p, v -> [Pattern v] -> Pattern v
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral v
u [Pattern v]
ps]
  where
    u :: v
u = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
avoid (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ Type -> v
forall v. Var v => Type -> v
typed Type
Pattern
decomposeSeqP Set v
_ SeqMatch
S (P.SequenceOp v
_ Pattern v
l SeqOp
Snoc Pattern v
r) = [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover [Pattern v
l, Pattern v
r]
decomposeSeqP Set v
_ SeqMatch
S (P.SequenceOp v
_ Pattern v
_ SeqOp
Concat Pattern v
_) = SeqCover v
forall v. SeqCover v
Overlap
decomposeSeqP Set v
_ SeqMatch
S (P.SequenceLiteral v
_ []) = SeqCover v
forall v. SeqCover v
Disjoint
decomposeSeqP Set v
avoid SeqMatch
S (P.SequenceLiteral v
_ [Pattern v]
ps) =
  [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover [v -> [Pattern v] -> Pattern v
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral v
u ([Pattern v] -> [Pattern v]
forall a. HasCallStack => [a] -> [a]
init [Pattern v]
ps), [Pattern v] -> Pattern v
forall a. HasCallStack => [a] -> a
last [Pattern v]
ps]
  where
    u :: v
u = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
avoid (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ Type -> v
forall v. Var v => Type -> v
typed Type
Pattern
decomposeSeqP Set v
_ (L Int
n) (P.SequenceOp v
_ Pattern v
l SeqOp
Concat Pattern v
r)
  | Just Int
m <- Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
l,
    Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m =
      [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover [Pattern v
l, Pattern v
r]
  | Bool
otherwise = SeqCover v
forall v. SeqCover v
Overlap
decomposeSeqP Set v
avoid (L Int
n) (P.SequenceLiteral v
_ [Pattern v]
ps)
  | [Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n,
    ([Pattern v]
pl, [Pattern v]
pr) <- Int -> [Pattern v] -> ([Pattern v], [Pattern v])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [Pattern v]
ps =
      [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover ([Pattern v] -> SeqCover v) -> [Pattern v] -> SeqCover v
forall a b. (a -> b) -> a -> b
$ v -> [Pattern v] -> Pattern v
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral v
u ([Pattern v] -> Pattern v) -> [[Pattern v]] -> [Pattern v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Pattern v]
pl, [Pattern v]
pr]
  | Bool
otherwise = SeqCover v
forall v. SeqCover v
Disjoint
  where
    u :: v
u = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
avoid (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ Type -> v
forall v. Var v => Type -> v
typed Type
Pattern
decomposeSeqP Set v
_ (R Int
n) (P.SequenceOp v
_ Pattern v
l SeqOp
Concat Pattern v
r)
  | Just Int
m <- Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
r,
    Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m =
      [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover [Pattern v
l, Pattern v
r]
decomposeSeqP Set v
avoid (R Int
n) (P.SequenceLiteral v
_ [Pattern v]
ps)
  | [Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n,
    ([Pattern v]
pl, [Pattern v]
pr) <- Int -> [Pattern v] -> ([Pattern v], [Pattern v])
forall a. Int -> [a] -> ([a], [a])
splitAt ([Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [Pattern v]
ps =
      [Pattern v] -> SeqCover v
forall v. [Pattern v] -> SeqCover v
Cover ([Pattern v] -> SeqCover v) -> [Pattern v] -> SeqCover v
forall a b. (a -> b) -> a -> b
$ v -> [Pattern v] -> Pattern v
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral v
u ([Pattern v] -> Pattern v) -> [[Pattern v]] -> [Pattern v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Pattern v]
pl, [Pattern v]
pr]
  | Bool
otherwise = SeqCover v
forall v. SeqCover v
Disjoint
  where
    u :: v
u = Set v -> v -> v
forall v. Var v => Set v -> v -> v
freshIn Set v
avoid (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ Type -> v
forall v. Var v => Type -> v
typed Type
Pattern
decomposeSeqP Set v
_ (DL Int
n) (P.SequenceOp v
_ Pattern v
l SeqOp
Concat Pattern v
_)
  | Just Int
m <- Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
l, Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = SeqCover v
forall v. SeqCover v
Disjoint
decomposeSeqP Set v
_ (DL Int
n) (P.SequenceLiteral v
_ [Pattern v]
ps)
  | [Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = SeqCover v
forall v. SeqCover v
Disjoint
decomposeSeqP Set v
_ (DR Int
n) (P.SequenceOp v
_ Pattern v
_ SeqOp
Concat Pattern v
r)
  | Just Int
m <- Pattern v -> Maybe Int
forall v. Pattern v -> Maybe Int
seqPSize Pattern v
r, Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = SeqCover v
forall v. SeqCover v
Disjoint
decomposeSeqP Set v
_ (DR Int
n) (P.SequenceLiteral v
_ [Pattern v]
ps)
  | [Pattern v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Pattern v]
ps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = SeqCover v
forall v. SeqCover v
Disjoint
decomposeSeqP Set v
_ SeqMatch
_ Pattern v
_ = SeqCover v
forall v. SeqCover v
Overlap

-- Splits a pattern row with respect to matching a variable against a
-- data type constructor. If the row would match the specified
-- constructor, the subpatterns and resulting row are yielded. A list
-- is used as the result value to indicate success or failure to match,
-- because these results are accumulated into a larger list elsewhere.
splitRow ::
  (Var v) =>
  v ->
  Maybe Reference ->
  Int ->
  Int ->
  PatternRow v ->
  [([P.Pattern v], PatternRow v)]
splitRow :: forall v.
Var v =>
v
-> Maybe Reference
-> Int
-> Int
-> PatternRow v
-> [([Pattern v], PatternRow v)]
splitRow v
v Maybe Reference
rf Int
t Int
nfields (PR ((Pattern v -> Bool) -> [Pattern v] -> ([Pattern v], [Pattern v])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ((v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v) (v -> Bool) -> (Pattern v -> v) -> Pattern v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern v -> v
forall loc. Pattern loc -> loc
loc) -> ([Pattern v]
pl, Pattern v
sp : [Pattern v]
pr)) Maybe (Term v)
g Term v
b) =
  Maybe Reference -> Int -> Int -> Pattern v -> [[Pattern v]]
forall v.
Var v =>
Maybe Reference -> Int -> Int -> Pattern v -> [[Pattern v]]
decomposePattern Maybe Reference
rf Int
t Int
nfields Pattern v
sp
    [[Pattern v]]
-> ([Pattern v] -> ([Pattern v], PatternRow v))
-> [([Pattern v], PatternRow v)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \[Pattern v]
subs -> ([Pattern v]
subs, [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
forall v. [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
PR ([Pattern v]
pl [Pattern v] -> [Pattern v] -> [Pattern v]
forall a. [a] -> [a] -> [a]
++ (Pattern v -> Bool) -> [Pattern v] -> [Pattern v]
forall a. (a -> Bool) -> [a] -> [a]
filter Pattern v -> Bool
forall a. Pattern a -> Bool
refutable [Pattern v]
subs [Pattern v] -> [Pattern v] -> [Pattern v]
forall a. [a] -> [a] -> [a]
++ [Pattern v]
pr) Maybe (Term v)
g Term v
b)
splitRow v
_ Maybe Reference
_ Int
_ Int
_ PatternRow v
row = [([], PatternRow v
row)]

-- Splits a row with respect to a variable, expecting that the
-- variable will be matched against a builtin pattern (non-data type,
-- non-request, non-sequence). In addition to returning the
-- subpatterns and new row, returns a version of the pattern that was
-- matched against the variable that may be collected to determine the
-- cases the built-in value is matched against.
splitRowBuiltin ::
  (Var v) =>
  v ->
  PatternRow v ->
  [(P.Pattern (), [([P.Pattern v], PatternRow v)])]
splitRowBuiltin :: forall v.
Var v =>
v -> PatternRow v -> [(Pattern (), [([Pattern v], PatternRow v)])]
splitRowBuiltin v
v (PR ((Pattern v -> Bool) -> [Pattern v] -> ([Pattern v], [Pattern v])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ((v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v) (v -> Bool) -> (Pattern v -> v) -> Pattern v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern v -> v
forall loc. Pattern loc -> loc
loc) -> ([Pattern v]
pl, Pattern v
sp : [Pattern v]
pr)) Maybe (Term v)
g Term v
b)
  | Just Pattern ()
p <- Pattern v -> Maybe (Pattern ())
forall a. Pattern a -> Maybe (Pattern ())
matchBuiltin Pattern v
sp = [(Pattern ()
p, [([], [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
forall v. [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
PR ([Pattern v]
pl [Pattern v] -> [Pattern v] -> [Pattern v]
forall a. [a] -> [a] -> [a]
++ [Pattern v]
pr) Maybe (Term v)
g Term v
b)])]
  | Bool
otherwise = []
splitRowBuiltin v
_ PatternRow v
r = [(() -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound (), [([], PatternRow v
r)])]

-- Splits a row with respect to a variable, expecting that the
-- variable will be matched against a sequence matching operation.
-- Yields the subpatterns and a new row to be used in subsequent
-- compilation. The outer list result is used to indicate success or
-- failure.
splitRowSeq ::
  (Var v) =>
  Set v ->
  v ->
  SeqMatch ->
  PatternRow v ->
  [([P.Pattern v], PatternRow v)]
splitRowSeq :: forall v.
Var v =>
Set v
-> v -> SeqMatch -> PatternRow v -> [([Pattern v], PatternRow v)]
splitRowSeq Set v
avoid0 v
v SeqMatch
m r :: PatternRow v
r@(PR ((Pattern v -> Bool) -> [Pattern v] -> ([Pattern v], [Pattern v])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break ((v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v) (v -> Bool) -> (Pattern v -> v) -> Pattern v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern v -> v
forall loc. Pattern loc -> loc
loc) -> ([Pattern v]
pl, Pattern v
sp : [Pattern v]
pr)) Maybe (Term v)
g Term v
b) =
  case Set v -> SeqMatch -> Pattern v -> SeqCover v
forall v. Var v => Set v -> SeqMatch -> Pattern v -> SeqCover v
decomposeSeqP Set v
avoid SeqMatch
m Pattern v
sp of
    Cover [Pattern v]
sps ->
      [([Pattern v]
sps, [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
forall v. [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
PR ([Pattern v]
pl [Pattern v] -> [Pattern v] -> [Pattern v]
forall a. [a] -> [a] -> [a]
++ (Pattern v -> Bool) -> [Pattern v] -> [Pattern v]
forall a. (a -> Bool) -> [a] -> [a]
filter Pattern v -> Bool
forall a. Pattern a -> Bool
refutable [Pattern v]
sps [Pattern v] -> [Pattern v] -> [Pattern v]
forall a. [a] -> [a] -> [a]
++ [Pattern v]
pr) Maybe (Term v)
g Term v
b)]
    SeqCover v
Disjoint -> []
    SeqCover v
Overlap -> [([], PatternRow v
r)]
  where
    avoid :: Set v
avoid = Set v
avoid0 Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Set v -> (Term v -> Set v) -> Maybe (Term v) -> Set v
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set v
forall a. Monoid a => a
mempty Term v -> Set v
forall vt v a. Term' vt v a -> Set v
freeVars Maybe (Term v)
g Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> Term v -> Set v
forall vt v a. Term' vt v a -> Set v
freeVars Term v
b
splitRowSeq Set v
_ v
_ SeqMatch
_ PatternRow v
r = [([], PatternRow v
r)]

-- Renames the variables annotating the patterns in a row, for once a
-- canonical choice has been made.
renameRow :: (Var v) => Map v v -> PatternRow v -> PatternRow v
renameRow :: forall v. Var v => Map v v -> PatternRow v -> PatternRow v
renameRow Map v v
m (PR [Pattern v]
p0 Maybe (Term v)
g0 Term v
b0) = [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
forall v. [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
PR [Pattern v]
p Maybe (Term v)
g Term v
b
  where
    access :: v -> v
access v
k
      | Just v
v <- v -> Map v v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
k Map v v
m = v
v
      | Bool
otherwise = v
k
    p :: [Pattern v]
p = ((Pattern v -> Pattern v) -> [Pattern v] -> [Pattern v]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern v -> Pattern v) -> [Pattern v] -> [Pattern v])
-> ((v -> v) -> Pattern v -> Pattern v)
-> (v -> v)
-> [Pattern v]
-> [Pattern v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v -> v) -> Pattern v -> Pattern v
forall a b. (a -> b) -> Pattern a -> Pattern b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) v -> v
access [Pattern v]
p0
    g :: Maybe (Term v)
g = Map v v -> Term v -> Term v
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
m (Term v -> Term v) -> Maybe (Term v) -> Maybe (Term v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Term v)
g0
    b :: Term v
b = Map v v -> Term v -> Term v
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
m Term v
b0

-- Chooses a common set of variables for use when decomposing
-- patterns into multiple sub-patterns. It is too naive to simply use
-- the variables in the first row, because it may have been generated
-- by decomposing a variable or unbound pattern, which will make up
-- variables for subpatterns.
chooseVars :: (Var v) => [[P.Pattern v]] -> [v]
chooseVars :: forall v. Var v => [[Pattern v]] -> [v]
chooseVars [] = []
chooseVars ([] : [[Pattern v]]
rs) = [[Pattern v]] -> [v]
forall v. Var v => [[Pattern v]] -> [v]
chooseVars [[Pattern v]]
rs
chooseVars ((P.Unbound {} : [Pattern v]
_) : [[Pattern v]]
rs) = [[Pattern v]] -> [v]
forall v. Var v => [[Pattern v]] -> [v]
chooseVars [[Pattern v]]
rs
chooseVars ([Pattern v]
r : [[Pattern v]]
_) = [Pattern v] -> [v]
forall v. Var v => [Pattern v] -> [v]
extractVars [Pattern v]
r

-- Creates a pattern matrix from many rows with the subpatterns
-- introduced during the splitting that generated those rows. Also
-- yields an indication of the type of the variables that the
-- subpatterns match against, if possible.
buildMatrix ::
  (Var v) =>
  [([P.Pattern v], PatternRow v)] ->
  ([(v, PType)], PatternMatrix v)
buildMatrix :: forall v.
Var v =>
[([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v)
buildMatrix [] = ([], [PatternRow v] -> PatternMatrix v
forall v. [PatternRow v] -> PatternMatrix v
PM [])
buildMatrix [([Pattern v], PatternRow v)]
vrs = ([v] -> [PType] -> [(v, PType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
cvs [PType]
rs, [PatternRow v] -> PatternMatrix v
forall v. [PatternRow v] -> PatternMatrix v
PM ([PatternRow v] -> PatternMatrix v)
-> [PatternRow v] -> PatternMatrix v
forall a b. (a -> b) -> a -> b
$ ([Pattern v], PatternRow v) -> PatternRow v
fixRow (([Pattern v], PatternRow v) -> PatternRow v)
-> [([Pattern v], PatternRow v)] -> [PatternRow v]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Pattern v], PatternRow v)]
vrs)
  where
    rs :: [PType]
rs = ([Pattern v] -> PType) -> [[Pattern v]] -> [PType]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Pattern v] -> PType
forall a. Show a => [Pattern a] -> PType
determineType ([[Pattern v]] -> [PType])
-> ([([Pattern v], PatternRow v)] -> [[Pattern v]])
-> [([Pattern v], PatternRow v)]
-> [PType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Pattern v]] -> [[Pattern v]]
forall a. [[a]] -> [[a]]
transpose ([[Pattern v]] -> [[Pattern v]])
-> ([([Pattern v], PatternRow v)] -> [[Pattern v]])
-> [([Pattern v], PatternRow v)]
-> [[Pattern v]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Pattern v], PatternRow v) -> [Pattern v])
-> [([Pattern v], PatternRow v)] -> [[Pattern v]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Pattern v], PatternRow v) -> [Pattern v]
forall a b. (a, b) -> a
fst ([([Pattern v], PatternRow v)] -> [PType])
-> [([Pattern v], PatternRow v)] -> [PType]
forall a b. (a -> b) -> a -> b
$ [([Pattern v], PatternRow v)]
vrs
    cvs :: [v]
cvs = [[Pattern v]] -> [v]
forall v. Var v => [[Pattern v]] -> [v]
chooseVars ([[Pattern v]] -> [v]) -> [[Pattern v]] -> [v]
forall a b. (a -> b) -> a -> b
$ ([Pattern v], PatternRow v) -> [Pattern v]
forall a b. (a, b) -> a
fst (([Pattern v], PatternRow v) -> [Pattern v])
-> [([Pattern v], PatternRow v)] -> [[Pattern v]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [([Pattern v], PatternRow v)]
vrs
    fixRow :: ([Pattern v], PatternRow v) -> PatternRow v
fixRow ([Pattern v] -> [v]
forall v. Var v => [Pattern v] -> [v]
extractVars -> [v]
rvs, PatternRow v
pr) =
      Map v v -> PatternRow v -> PatternRow v
forall v. Var v => Map v v -> PatternRow v -> PatternRow v
renameRow ((v -> v -> v) -> [(v, v)] -> Map v v
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
fromListWith v -> v -> v
forall a b. a -> b -> a
const ([(v, v)] -> Map v v) -> ([v] -> [(v, v)]) -> [v] -> Map v v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [v] -> [v] -> [(v, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
rvs ([v] -> Map v v) -> [v] -> Map v v
forall a b. (a -> b) -> a -> b
$ [v]
cvs) PatternRow v
pr

-- Splits a pattern matrix on a given variable, expected to be matched
-- against builtin type patterns. Yields the cases covered and
-- corresponding matrices for those cases, with types for any new
-- variables (although currently builtin patterns do not introduce
-- variables).
splitMatrixBuiltin ::
  (Var v) =>
  v ->
  PatternMatrix v ->
  [(P.Pattern (), [(v, PType)], PatternMatrix v)]
splitMatrixBuiltin :: forall v.
Var v =>
v
-> PatternMatrix v -> [(Pattern (), [(v, PType)], PatternMatrix v)]
splitMatrixBuiltin v
v (PM [PatternRow v]
rs) =
  ((Pattern (), ([(v, PType)], PatternMatrix v))
 -> (Pattern (), [(v, PType)], PatternMatrix v))
-> [(Pattern (), ([(v, PType)], PatternMatrix v))]
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Pattern ()
a, ([(v, PType)]
b, PatternMatrix v
c)) -> (Pattern ()
a, [(v, PType)]
b, PatternMatrix v
c))
    ([(Pattern (), ([(v, PType)], PatternMatrix v))]
 -> [(Pattern (), [(v, PType)], PatternMatrix v)])
-> ([(Pattern (), [([Pattern v], PatternRow v)])]
    -> [(Pattern (), ([(v, PType)], PatternMatrix v))])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Pattern ()) ([(v, PType)], PatternMatrix v)
-> [(Pattern (), ([(v, PType)], PatternMatrix v))]
forall k a. Map k a -> [(k, a)]
Map.toList
    (Map (Pattern ()) ([(v, PType)], PatternMatrix v)
 -> [(Pattern (), ([(v, PType)], PatternMatrix v))])
-> ([(Pattern (), [([Pattern v], PatternRow v)])]
    -> Map (Pattern ()) ([(v, PType)], PatternMatrix v))
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), ([(v, PType)], PatternMatrix v))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v))
-> Map (Pattern ()) [([Pattern v], PatternRow v)]
-> Map (Pattern ()) ([(v, PType)], PatternMatrix v)
forall a b. (a -> b) -> Map (Pattern ()) a -> Map (Pattern ()) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v)
forall v.
Var v =>
[([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v)
buildMatrix
    (Map (Pattern ()) [([Pattern v], PatternRow v)]
 -> Map (Pattern ()) ([(v, PType)], PatternMatrix v))
-> ([(Pattern (), [([Pattern v], PatternRow v)])]
    -> Map (Pattern ()) [([Pattern v], PatternRow v)])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> Map (Pattern ()) ([(v, PType)], PatternMatrix v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([([Pattern v], PatternRow v)]
 -> [([Pattern v], PatternRow v)] -> [([Pattern v], PatternRow v)])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> Map (Pattern ()) [([Pattern v], PatternRow v)]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
fromListWith (([([Pattern v], PatternRow v)]
 -> [([Pattern v], PatternRow v)] -> [([Pattern v], PatternRow v)])
-> [([Pattern v], PatternRow v)]
-> [([Pattern v], PatternRow v)]
-> [([Pattern v], PatternRow v)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [([Pattern v], PatternRow v)]
-> [([Pattern v], PatternRow v)] -> [([Pattern v], PatternRow v)]
forall a. [a] -> [a] -> [a]
(++))
    ([(Pattern (), [([Pattern v], PatternRow v)])]
 -> Map (Pattern ()) [([Pattern v], PatternRow v)])
-> ([(Pattern (), [([Pattern v], PatternRow v)])]
    -> [(Pattern (), [([Pattern v], PatternRow v)])])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> Map (Pattern ()) [([Pattern v], PatternRow v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [([Pattern v], PatternRow v)])]
forall v.
Var v =>
[(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [([Pattern v], PatternRow v)])]
expandIrrefutable
    ([(Pattern (), [([Pattern v], PatternRow v)])]
 -> [(Pattern (), [(v, PType)], PatternMatrix v)])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
forall a b. (a -> b) -> a -> b
$ v -> PatternRow v -> [(Pattern (), [([Pattern v], PatternRow v)])]
forall v.
Var v =>
v -> PatternRow v -> [(Pattern (), [([Pattern v], PatternRow v)])]
splitRowBuiltin v
v (PatternRow v -> [(Pattern (), [([Pattern v], PatternRow v)])])
-> [PatternRow v] -> [(Pattern (), [([Pattern v], PatternRow v)])]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [PatternRow v]
rs

expandIrrefutable ::
  (Var v) =>
  [(P.Pattern (), [([P.Pattern v], PatternRow v)])] ->
  [(P.Pattern (), [([P.Pattern v], PatternRow v)])]
expandIrrefutable :: forall v.
Var v =>
[(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [([Pattern v], PatternRow v)])]
expandIrrefutable [(Pattern (), [([Pattern v], PatternRow v)])]
rss = ((Pattern (), [([Pattern v], PatternRow v)])
 -> [(Pattern (), [([Pattern v], PatternRow v)])])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [([Pattern v], PatternRow v)])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Pattern (), [([Pattern v], PatternRow v)])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
expand [(Pattern (), [([Pattern v], PatternRow v)])]
rss
  where
    specific :: [Pattern ()]
specific = (Pattern () -> Bool) -> [Pattern ()] -> [Pattern ()]
forall a. (a -> Bool) -> [a] -> [a]
filter Pattern () -> Bool
forall a. Pattern a -> Bool
refutable ([Pattern ()] -> [Pattern ()]) -> [Pattern ()] -> [Pattern ()]
forall a b. (a -> b) -> a -> b
$ (Pattern (), [([Pattern v], PatternRow v)]) -> Pattern ()
forall a b. (a, b) -> a
fst ((Pattern (), [([Pattern v], PatternRow v)]) -> Pattern ())
-> [(Pattern (), [([Pattern v], PatternRow v)])] -> [Pattern ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Pattern (), [([Pattern v], PatternRow v)])]
rss
    expand :: (Pattern (), [([Pattern v], PatternRow v)])
-> [(Pattern (), [([Pattern v], PatternRow v)])]
expand tup :: (Pattern (), [([Pattern v], PatternRow v)])
tup@(Pattern ()
p, [([Pattern v], PatternRow v)]
rs)
      | Bool -> Bool
not (Pattern () -> Bool
forall a. Pattern a -> Bool
refutable Pattern ()
p) = (Pattern () -> (Pattern (), [([Pattern v], PatternRow v)]))
-> [Pattern ()] -> [(Pattern (), [([Pattern v], PatternRow v)])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,[([Pattern v], PatternRow v)]
rs) [Pattern ()]
specific [(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [([Pattern v], PatternRow v)])]
-> [(Pattern (), [([Pattern v], PatternRow v)])]
forall a. [a] -> [a] -> [a]
++ [(Pattern (), [([Pattern v], PatternRow v)])
tup]
    expand (Pattern (), [([Pattern v], PatternRow v)])
tup = [(Pattern (), [([Pattern v], PatternRow v)])
tup]

matchPattern :: [(v, PType)] -> SeqMatch -> P.Pattern ()
matchPattern :: forall v. [(v, PType)] -> SeqMatch -> Pattern ()
matchPattern [(v, PType)]
vrs = \case
  SeqMatch
E -> Int -> Pattern ()
sz Int
0
  SeqMatch
C -> () -> Pattern () -> SeqOp -> Pattern () -> Pattern ()
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp () Pattern ()
vr SeqOp
Cons Pattern ()
vr
  SeqMatch
S -> () -> Pattern () -> SeqOp -> Pattern () -> Pattern ()
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp () Pattern ()
vr SeqOp
Snoc Pattern ()
vr
  L Int
n -> () -> Pattern () -> SeqOp -> Pattern () -> Pattern ()
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp () (Int -> Pattern ()
sz Int
n) SeqOp
Concat (() -> Pattern ()
forall loc. loc -> Pattern loc
P.Var ())
  R Int
n -> () -> Pattern () -> SeqOp -> Pattern () -> Pattern ()
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp () (() -> Pattern ()
forall loc. loc -> Pattern loc
P.Var ()) SeqOp
Concat (Int -> Pattern ()
sz Int
n)
  DL Int
_ -> () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound ()
  DR Int
_ -> () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound ()
  where
    vr :: Pattern ()
vr | [] <- [(v, PType)]
vrs = () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound () | Bool
otherwise = () -> Pattern ()
forall loc. loc -> Pattern loc
P.Var ()
    sz :: Int -> Pattern ()
sz Int
n = () -> [Pattern ()] -> Pattern ()
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral () ([Pattern ()] -> Pattern ())
-> (Pattern () -> [Pattern ()]) -> Pattern () -> Pattern ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Pattern () -> [Pattern ()]
forall a. Int -> a -> [a]
replicate Int
n (Pattern () -> Pattern ()) -> Pattern () -> Pattern ()
forall a b. (a -> b) -> a -> b
$ () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound ()

-- Splits a matrix at a given variable with respect to sequence
-- patterns. Yields the appropriate patterns for the covered cases,
-- variables introduced for each case with their types, and new
-- matricies for subsequent compilation.
splitMatrixSeq ::
  (Var v) =>
  Set v ->
  v ->
  PatternMatrix v ->
  [(P.Pattern (), [(v, PType)], PatternMatrix v)]
splitMatrixSeq :: forall v.
Var v =>
Set v
-> v
-> PatternMatrix v
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
splitMatrixSeq Set v
avoid v
v (PM [PatternRow v]
rs) =
  [(Pattern (), [(v, PType)], PatternMatrix v)]
cases
  where
    ms :: [SeqMatch]
ms = [Pattern v] -> [SeqMatch]
forall v. [Pattern v] -> [SeqMatch]
decideSeqPat ([Pattern v] -> [SeqMatch]) -> [Pattern v] -> [SeqMatch]
forall a b. (a -> b) -> a -> b
$ Int -> [Pattern v] -> [Pattern v]
forall a. Int -> [a] -> [a]
take Int
1 ([Pattern v] -> [Pattern v])
-> (PatternRow v -> [Pattern v]) -> PatternRow v -> [Pattern v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pattern v -> Bool) -> [Pattern v] -> [Pattern v]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((v -> v -> Bool
forall a. Eq a => a -> a -> Bool
/= v
v) (v -> Bool) -> (Pattern v -> v) -> Pattern v -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern v -> v
forall loc. Pattern loc -> loc
loc) ([Pattern v] -> [Pattern v])
-> (PatternRow v -> [Pattern v]) -> PatternRow v -> [Pattern v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatternRow v -> [Pattern v]
forall v. PatternRow v -> [Pattern v]
matches (PatternRow v -> [Pattern v]) -> [PatternRow v] -> [Pattern v]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [PatternRow v]
rs
    hint :: SeqMatch -> f (f PType) -> f (f PType)
hint SeqMatch
m f (f PType)
vrs
      | SeqMatch
m SeqMatch -> [SeqMatch] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SeqMatch
E, SeqMatch
C, SeqMatch
S] = f (f PType)
vrs
      | Bool
otherwise = ((f PType -> f PType) -> f (f PType) -> f (f PType)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((f PType -> f PType) -> f (f PType) -> f (f PType))
-> ((PType -> PType) -> f PType -> f PType)
-> (PType -> PType)
-> f (f PType)
-> f (f PType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PType -> PType) -> f PType -> f PType
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (PType -> PType -> PType
forall a b. a -> b -> a
const (PType -> PType -> PType) -> PType -> PType -> PType
forall a b. (a -> b) -> a -> b
$ Reference -> PType
PData Reference
Rf.listRef) f (f PType)
vrs
    cases :: [(Pattern (), [(v, PType)], PatternMatrix v)]
cases =
      [SeqMatch]
ms [SeqMatch]
-> (SeqMatch -> (Pattern (), [(v, PType)], PatternMatrix v))
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \SeqMatch
m ->
        let frs :: [([Pattern v], PatternRow v)]
frs = [PatternRow v]
rs [PatternRow v]
-> (PatternRow v -> [([Pattern v], PatternRow v)])
-> [([Pattern v], PatternRow v)]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set v
-> v -> SeqMatch -> PatternRow v -> [([Pattern v], PatternRow v)]
forall v.
Var v =>
Set v
-> v -> SeqMatch -> PatternRow v -> [([Pattern v], PatternRow v)]
splitRowSeq Set v
avoid v
v SeqMatch
m
            ([(v, PType)]
vrs, PatternMatrix v
pm) = [([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v)
forall v.
Var v =>
[([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v)
buildMatrix [([Pattern v], PatternRow v)]
frs
         in ([(v, PType)] -> SeqMatch -> Pattern ()
forall v. [(v, PType)] -> SeqMatch -> Pattern ()
matchPattern [(v, PType)]
vrs SeqMatch
m, SeqMatch -> [(v, PType)] -> [(v, PType)]
forall {f :: * -> *} {f :: * -> *}.
(Functor f, Functor f) =>
SeqMatch -> f (f PType) -> f (f PType)
hint SeqMatch
m [(v, PType)]
vrs, PatternMatrix v
pm)

-- Splits a matrix at a given variable with respect to a data type or
-- ability match. Yields a new matrix for each constructor, with
-- variables introduced and their types for each case.
splitMatrix ::
  (Var v) =>
  v ->
  Maybe Reference ->
  NCons ->
  PatternMatrix v ->
  [(Int, [(v, PType)], PatternMatrix v)]
splitMatrix :: forall v.
Var v =>
v
-> Maybe Reference
-> NCons
-> PatternMatrix v
-> [(Int, [(v, PType)], PatternMatrix v)]
splitMatrix v
v Maybe Reference
rf NCons
cons (PM [PatternRow v]
rs) =
  ((Int, ([(v, PType)], PatternMatrix v))
 -> (Int, [(v, PType)], PatternMatrix v))
-> [(Int, ([(v, PType)], PatternMatrix v))]
-> [(Int, [(v, PType)], PatternMatrix v)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
a, ([(v, PType)]
b, PatternMatrix v
c)) -> (Int
a, [(v, PType)]
b, PatternMatrix v
c)) ([(Int, ([(v, PType)], PatternMatrix v))]
 -> [(Int, [(v, PType)], PatternMatrix v)])
-> ([(Int, [([Pattern v], PatternRow v)])]
    -> [(Int, ([(v, PType)], PatternMatrix v))])
-> [(Int, [([Pattern v], PatternRow v)])]
-> [(Int, [(v, PType)], PatternMatrix v)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Int, [([Pattern v], PatternRow v)])
 -> (Int, ([(v, PType)], PatternMatrix v)))
-> [(Int, [([Pattern v], PatternRow v)])]
-> [(Int, ([(v, PType)], PatternMatrix v))]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((Int, [([Pattern v], PatternRow v)])
  -> (Int, ([(v, PType)], PatternMatrix v)))
 -> [(Int, [([Pattern v], PatternRow v)])]
 -> [(Int, ([(v, PType)], PatternMatrix v))])
-> (([([Pattern v], PatternRow v)]
     -> ([(v, PType)], PatternMatrix v))
    -> (Int, [([Pattern v], PatternRow v)])
    -> (Int, ([(v, PType)], PatternMatrix v)))
-> ([([Pattern v], PatternRow v)]
    -> ([(v, PType)], PatternMatrix v))
-> [(Int, [([Pattern v], PatternRow v)])]
-> [(Int, ([(v, PType)], PatternMatrix v))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v))
-> (Int, [([Pattern v], PatternRow v)])
-> (Int, ([(v, PType)], PatternMatrix v))
forall a b. (a -> b) -> (Int, a) -> (Int, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) [([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v)
forall v.
Var v =>
[([Pattern v], PatternRow v)] -> ([(v, PType)], PatternMatrix v)
buildMatrix ([(Int, [([Pattern v], PatternRow v)])]
 -> [(Int, [(v, PType)], PatternMatrix v)])
-> [(Int, [([Pattern v], PatternRow v)])]
-> [(Int, [(v, PType)], PatternMatrix v)]
forall a b. (a -> b) -> a -> b
$ [(Int, [([Pattern v], PatternRow v)])]
mmap
  where
    mmap :: [(Int, [([Pattern v], PatternRow v)])]
mmap = ((Int, Int) -> (Int, [([Pattern v], PatternRow v)]))
-> NCons -> [(Int, [([Pattern v], PatternRow v)])]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Int
t, Int
fs) -> (Int
t, v
-> Maybe Reference
-> Int
-> Int
-> PatternRow v
-> [([Pattern v], PatternRow v)]
forall v.
Var v =>
v
-> Maybe Reference
-> Int
-> Int
-> PatternRow v
-> [([Pattern v], PatternRow v)]
splitRow v
v Maybe Reference
rf Int
t Int
fs (PatternRow v -> [([Pattern v], PatternRow v)])
-> [PatternRow v] -> [([Pattern v], PatternRow v)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [PatternRow v]
rs)) NCons
cons

-- Monad for pattern preparation. It is a state monad carrying a fresh
-- variable source, the list of variables bound the pattern being
-- prepared, and a variable renaming mapping.
type PPM v a = State (Word64, [v], Map v v) a

freshVar :: (Var v) => PPM v v
freshVar :: forall v. Var v => PPM v v
freshVar = ((ConstructorId, [v], Map v v)
 -> (v, (ConstructorId, [v], Map v v)))
-> StateT (ConstructorId, [v], Map v v) Identity v
forall a.
((ConstructorId, [v], Map v v)
 -> (a, (ConstructorId, [v], Map v v)))
-> StateT (ConstructorId, [v], Map v v) Identity a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state (((ConstructorId, [v], Map v v)
  -> (v, (ConstructorId, [v], Map v v)))
 -> StateT (ConstructorId, [v], Map v v) Identity v)
-> ((ConstructorId, [v], Map v v)
    -> (v, (ConstructorId, [v], Map v v)))
-> StateT (ConstructorId, [v], Map v v) Identity v
forall a b. (a -> b) -> a -> b
$ \(ConstructorId
fw, [v]
vs, Map v v
rn) ->
  let v :: v
v = ConstructorId -> v -> v
forall v. Var v => ConstructorId -> v -> v
freshenId ConstructorId
fw (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ Type -> v
forall v. Var v => Type -> v
typed Type
Pattern
   in (v
v, (ConstructorId
fw ConstructorId -> ConstructorId -> ConstructorId
forall a. Num a => a -> a -> a
+ ConstructorId
1, [v]
vs, Map v v
rn))

useVar :: PPM v v
useVar :: forall v. PPM v v
useVar = ((ConstructorId, [v], Map v v)
 -> (v, (ConstructorId, [v], Map v v)))
-> StateT (ConstructorId, [v], Map v v) Identity v
forall a.
((ConstructorId, [v], Map v v)
 -> (a, (ConstructorId, [v], Map v v)))
-> StateT (ConstructorId, [v], Map v v) Identity a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state (((ConstructorId, [v], Map v v)
  -> (v, (ConstructorId, [v], Map v v)))
 -> StateT (ConstructorId, [v], Map v v) Identity v)
-> ((ConstructorId, [v], Map v v)
    -> (v, (ConstructorId, [v], Map v v)))
-> StateT (ConstructorId, [v], Map v v) Identity v
forall a b. (a -> b) -> a -> b
$ \case
  (ConstructorId
avoid, v
v : [v]
vs, Map v v
rn) -> (v
v, (ConstructorId
avoid, [v]
vs, Map v v
rn))
  (ConstructorId, [v], Map v v)
_ -> [Char] -> (v, (ConstructorId, [v], Map v v))
forall a. HasCallStack => [Char] -> a
error [Char]
"useVar: Expected multiple vars"

renameTo :: (Var v) => v -> v -> PPM v ()
renameTo :: forall v. Var v => v -> v -> PPM v ()
renameTo v
to v
from =
  ((ConstructorId, [v], Map v v) -> (ConstructorId, [v], Map v v))
-> StateT (ConstructorId, [v], Map v v) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (((ConstructorId, [v], Map v v) -> (ConstructorId, [v], Map v v))
 -> StateT (ConstructorId, [v], Map v v) Identity ())
-> ((ConstructorId, [v], Map v v) -> (ConstructorId, [v], Map v v))
-> StateT (ConstructorId, [v], Map v v) Identity ()
forall a b. (a -> b) -> a -> b
$ \(ConstructorId
avoid, [v]
vs, Map v v
rn) ->
    ( ConstructorId
avoid,
      [v]
vs,
      (v -> v -> v) -> v -> v -> Map v v -> Map v v
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
insertWith ([Char] -> v -> v -> v
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"renameTo: duplicate rename") v
from v
to Map v v
rn
    )

-- Tries to rewrite sequence patterns into a format that can be
-- matched most flexibly.
normalizeSeqP :: P.Pattern a -> P.Pattern a
normalizeSeqP :: forall a. Pattern a -> Pattern a
normalizeSeqP (P.As a
a Pattern a
p) = a -> Pattern a -> Pattern a
forall loc. loc -> Pattern loc -> Pattern loc
P.As a
a (Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP Pattern a
p)
normalizeSeqP (P.EffectPure a
a Pattern a
p) = a -> Pattern a -> Pattern a
forall loc. loc -> Pattern loc -> Pattern loc
P.EffectPure a
a (Pattern a -> Pattern a) -> Pattern a -> Pattern a
forall a b. (a -> b) -> a -> b
$ Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP Pattern a
p
normalizeSeqP (P.EffectBind a
a GConstructorReference Reference
r [Pattern a]
ps Pattern a
k) =
  a
-> GConstructorReference Reference
-> [Pattern a]
-> Pattern a
-> Pattern a
forall loc.
loc
-> GConstructorReference Reference
-> [Pattern loc]
-> Pattern loc
-> Pattern loc
P.EffectBind a
a GConstructorReference Reference
r (Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP (Pattern a -> Pattern a) -> [Pattern a] -> [Pattern a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern a]
ps) (Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP Pattern a
k)
normalizeSeqP (P.Constructor a
a GConstructorReference Reference
r [Pattern a]
ps) =
  a -> GConstructorReference Reference -> [Pattern a] -> Pattern a
forall loc.
loc
-> GConstructorReference Reference -> [Pattern loc] -> Pattern loc
P.Constructor a
a GConstructorReference Reference
r ([Pattern a] -> Pattern a) -> [Pattern a] -> Pattern a
forall a b. (a -> b) -> a -> b
$ Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP (Pattern a -> Pattern a) -> [Pattern a] -> [Pattern a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern a]
ps
normalizeSeqP (P.SequenceLiteral a
a [Pattern a]
ps) =
  a -> [Pattern a] -> Pattern a
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral a
a ([Pattern a] -> Pattern a) -> [Pattern a] -> Pattern a
forall a b. (a -> b) -> a -> b
$ Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP (Pattern a -> Pattern a) -> [Pattern a] -> [Pattern a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Pattern a]
ps
normalizeSeqP (P.SequenceOp a
a Pattern a
p0 SeqOp
op Pattern a
q0) =
  case (SeqOp
op, Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP Pattern a
p0, Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP Pattern a
q0) of
    (SeqOp
Cons, Pattern a
p, P.SequenceLiteral a
_ [Pattern a]
ps) ->
      a -> [Pattern a] -> Pattern a
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral a
a (Pattern a
p Pattern a -> [Pattern a] -> [Pattern a]
forall a. a -> [a] -> [a]
: [Pattern a]
ps)
    (SeqOp
Snoc, P.SequenceLiteral a
_ [Pattern a]
ps, Pattern a
p) ->
      a -> [Pattern a] -> Pattern a
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral a
a ([Pattern a]
ps [Pattern a] -> [Pattern a] -> [Pattern a]
forall a. [a] -> [a] -> [a]
++ [Pattern a
p])
    (SeqOp
Concat, P.SequenceLiteral a
_ [Pattern a]
ps, P.SequenceLiteral a
_ [Pattern a]
qs) ->
      a -> [Pattern a] -> Pattern a
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral a
a ([Pattern a]
ps [Pattern a] -> [Pattern a] -> [Pattern a]
forall a. [a] -> [a] -> [a]
++ [Pattern a]
qs)
    (SeqOp
Concat, P.SequenceLiteral a
_ [Pattern a]
ps, Pattern a
q) ->
      (Pattern a -> Pattern a -> Pattern a)
-> Pattern a -> [Pattern a] -> Pattern a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Pattern a
p Pattern a
r -> a -> Pattern a -> SeqOp -> Pattern a -> Pattern a
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp a
a Pattern a
p SeqOp
Cons Pattern a
r) Pattern a
q [Pattern a]
ps
    (SeqOp
Concat, Pattern a
p, P.SequenceLiteral a
_ [Pattern a]
qs) ->
      (Pattern a -> Pattern a -> Pattern a)
-> Pattern a -> [Pattern a] -> Pattern a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\Pattern a
r Pattern a
q -> a -> Pattern a -> SeqOp -> Pattern a -> Pattern a
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp a
a Pattern a
r SeqOp
Snoc Pattern a
q) Pattern a
p [Pattern a]
qs
    (SeqOp
op, Pattern a
p, Pattern a
q) -> a -> Pattern a -> SeqOp -> Pattern a -> Pattern a
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp a
a Pattern a
p SeqOp
op Pattern a
q
normalizeSeqP Pattern a
p = Pattern a
p

-- Prepares a pattern for compilation, like `preparePattern`. This
-- function, however, is used when a candidate variable for a pattern
-- has already been chosen, as with an As pattern. This allows turning
-- redundant names (like with the pattern u@v) into renamings.
prepareAs :: (Var v) => P.Pattern a -> v -> PPM v (P.Pattern v)
prepareAs :: forall v a. Var v => Pattern a -> v -> PPM v (Pattern v)
prepareAs (P.Unbound a
_) v
u = Pattern v
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a. a -> StateT (ConstructorId, [v], Map v v) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern v
 -> StateT (ConstructorId, [v], Map v v) Identity (Pattern v))
-> Pattern v
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a b. (a -> b) -> a -> b
$ v -> Pattern v
forall loc. loc -> Pattern loc
P.Var v
u
prepareAs (P.As a
_ Pattern a
p) v
u = (PPM v v
forall v. PPM v v
useVar PPM v v
-> (v -> StateT (ConstructorId, [v], Map v v) Identity ())
-> StateT (ConstructorId, [v], Map v v) Identity ()
forall a b.
StateT (ConstructorId, [v], Map v v) Identity a
-> (a -> StateT (ConstructorId, [v], Map v v) Identity b)
-> StateT (ConstructorId, [v], Map v v) Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= v -> v -> StateT (ConstructorId, [v], Map v v) Identity ()
forall v. Var v => v -> v -> PPM v ()
renameTo v
u) StateT (ConstructorId, [v], Map v v) Identity ()
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a b.
StateT (ConstructorId, [v], Map v v) Identity a
-> StateT (ConstructorId, [v], Map v v) Identity b
-> StateT (ConstructorId, [v], Map v v) Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Pattern a
-> v -> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> v -> PPM v (Pattern v)
prepareAs Pattern a
p v
u
prepareAs (P.Var a
_) v
u = v -> Pattern v
forall loc. loc -> Pattern loc
P.Var v
u Pattern v
-> StateT (ConstructorId, [v], Map v v) Identity ()
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a b.
a
-> StateT (ConstructorId, [v], Map v v) Identity b
-> StateT (ConstructorId, [v], Map v v) Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (v -> v -> StateT (ConstructorId, [v], Map v v) Identity ()
forall v. Var v => v -> v -> PPM v ()
renameTo v
u (v -> StateT (ConstructorId, [v], Map v v) Identity ())
-> PPM v v -> StateT (ConstructorId, [v], Map v v) Identity ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PPM v v
forall v. PPM v v
useVar)
prepareAs (P.Constructor a
_ GConstructorReference Reference
r [Pattern a]
ps) v
u = do
  v -> GConstructorReference Reference -> [Pattern v] -> Pattern v
forall loc.
loc
-> GConstructorReference Reference -> [Pattern loc] -> Pattern loc
P.Constructor v
u GConstructorReference Reference
r ([Pattern v] -> Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity [Pattern v]
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern a
 -> StateT (ConstructorId, [v], Map v v) Identity (Pattern v))
-> [Pattern a]
-> StateT (ConstructorId, [v], Map v v) Identity [Pattern v]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Pattern a
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern [Pattern a]
ps
prepareAs (P.EffectPure a
_ Pattern a
p) v
u = do
  v -> Pattern v -> Pattern v
forall loc. loc -> Pattern loc -> Pattern loc
P.EffectPure v
u (Pattern v -> Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern a
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern Pattern a
p
prepareAs (P.EffectBind a
_ GConstructorReference Reference
r [Pattern a]
ps Pattern a
k) v
u = do
  v
-> GConstructorReference Reference
-> [Pattern v]
-> Pattern v
-> Pattern v
forall loc.
loc
-> GConstructorReference Reference
-> [Pattern loc]
-> Pattern loc
-> Pattern loc
P.EffectBind v
u GConstructorReference Reference
r
    ([Pattern v] -> Pattern v -> Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity [Pattern v]
-> StateT
     (ConstructorId, [v], Map v v) Identity (Pattern v -> Pattern v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern a
 -> StateT (ConstructorId, [v], Map v v) Identity (Pattern v))
-> [Pattern a]
-> StateT (ConstructorId, [v], Map v v) Identity [Pattern v]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Pattern a
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern [Pattern a]
ps
    StateT
  (ConstructorId, [v], Map v v) Identity (Pattern v -> Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a b.
StateT (ConstructorId, [v], Map v v) Identity (a -> b)
-> StateT (ConstructorId, [v], Map v v) Identity a
-> StateT (ConstructorId, [v], Map v v) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pattern a
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern Pattern a
k
prepareAs (P.SequenceLiteral a
_ [Pattern a]
ps) v
u = do
  v -> [Pattern v] -> Pattern v
forall loc. loc -> [Pattern loc] -> Pattern loc
P.SequenceLiteral v
u ([Pattern v] -> Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity [Pattern v]
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Pattern a
 -> StateT (ConstructorId, [v], Map v v) Identity (Pattern v))
-> [Pattern a]
-> StateT (ConstructorId, [v], Map v v) Identity [Pattern v]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Pattern a
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern [Pattern a]
ps
prepareAs (P.SequenceOp a
_ Pattern a
p SeqOp
op Pattern a
q) v
u = do
  (Pattern v -> SeqOp -> Pattern v -> Pattern v)
-> SeqOp -> Pattern v -> Pattern v -> Pattern v
forall a b c. (a -> b -> c) -> b -> a -> c
flip (v -> Pattern v -> SeqOp -> Pattern v -> Pattern v
forall loc.
loc -> Pattern loc -> SeqOp -> Pattern loc -> Pattern loc
P.SequenceOp v
u) SeqOp
op
    (Pattern v -> Pattern v -> Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
-> StateT
     (ConstructorId, [v], Map v v) Identity (Pattern v -> Pattern v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern a
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern Pattern a
p
    StateT
  (ConstructorId, [v], Map v v) Identity (Pattern v -> Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a b.
StateT (ConstructorId, [v], Map v v) Identity (a -> b)
-> StateT (ConstructorId, [v], Map v v) Identity a
-> StateT (ConstructorId, [v], Map v v) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pattern a
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern Pattern a
q
prepareAs Pattern a
p v
u = Pattern v
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a. a -> StateT (ConstructorId, [v], Map v v) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Pattern v
 -> StateT (ConstructorId, [v], Map v v) Identity (Pattern v))
-> Pattern v
-> StateT (ConstructorId, [v], Map v v) Identity (Pattern v)
forall a b. (a -> b) -> a -> b
$ v
u v -> Pattern a -> Pattern v
forall a b. a -> Pattern b -> Pattern a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Pattern a
p

-- Prepares a pattern for compilation. This removes the existing
-- annotations and replaces them with a choice of variable that the
-- pattern is matching against. As patterns are eliminated and the
-- variables they bind are used as candidates for what that level of
-- the pattern matches against.
preparePattern :: (Var v) => P.Pattern a -> PPM v (P.Pattern v)
preparePattern :: forall v a. Var v => Pattern a -> PPM v (Pattern v)
preparePattern Pattern a
p = Pattern a -> v -> PPM v (Pattern v)
forall v a. Var v => Pattern a -> v -> PPM v (Pattern v)
prepareAs Pattern a
p (v -> PPM v (Pattern v))
-> StateT (ConstructorId, [v], Map v v) Identity v
-> PPM v (Pattern v)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< StateT (ConstructorId, [v], Map v v) Identity v
forall v. Var v => PPM v v
freshVar

buildPattern :: Bool -> ConstructorReference -> [v] -> Int -> P.Pattern ()
buildPattern :: forall v.
Bool -> GConstructorReference Reference -> [v] -> Int -> Pattern ()
buildPattern Bool
effect GConstructorReference Reference
r [v]
vs Int
nfields
  | Bool
effect, [] <- [Pattern ()]
vps = [Char] -> Pattern ()
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"too few patterns for effect bind"
  | Bool
effect = ()
-> GConstructorReference Reference
-> [Pattern ()]
-> Pattern ()
-> Pattern ()
forall loc.
loc
-> GConstructorReference Reference
-> [Pattern loc]
-> Pattern loc
-> Pattern loc
P.EffectBind () GConstructorReference Reference
r ([Pattern ()] -> [Pattern ()]
forall a. HasCallStack => [a] -> [a]
init [Pattern ()]
vps) ([Pattern ()] -> Pattern ()
forall a. HasCallStack => [a] -> a
last [Pattern ()]
vps)
  | Bool
otherwise = () -> GConstructorReference Reference -> [Pattern ()] -> Pattern ()
forall loc.
loc
-> GConstructorReference Reference -> [Pattern loc] -> Pattern loc
P.Constructor () GConstructorReference Reference
r [Pattern ()]
vps
  where
    vps :: [Pattern ()]
vps
      | [v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [v]
vs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nfields =
          Int -> Pattern () -> [Pattern ()]
forall a. Int -> a -> [a]
replicate Int
nfields (Pattern () -> [Pattern ()]) -> Pattern () -> [Pattern ()]
forall a b. (a -> b) -> a -> b
$ () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound ()
      | Bool
otherwise =
          () -> Pattern ()
forall loc. loc -> Pattern loc
P.Var () Pattern () -> [v] -> [Pattern ()]
forall a b. a -> [b] -> [a]
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [v]
vs

numberCons :: Cons -> NCons
numberCons :: Cons -> NCons
numberCons = Cons -> Cons -> NCons
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..]

lookupData :: Reference -> DataSpec -> Either String Cons
lookupData :: Reference -> DataSpec -> Either [Char] Cons
lookupData Reference
rf (Reference -> DataSpec -> Maybe (Either Cons Cons)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Reference
rf -> Just Either Cons Cons
econs) =
  case Either Cons Cons
econs of
    Left Cons
_ -> [Char] -> Either [Char] Cons
forall a b. a -> Either a b
Left ([Char] -> Either [Char] Cons) -> [Char] -> Either [Char] Cons
forall a b. (a -> b) -> a -> b
$ [Char]
"data type matching on ability: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Reference -> [Char]
forall a. Show a => a -> [Char]
show Reference
rf
    Right Cons
cs -> Cons -> Either [Char] Cons
forall a b. b -> Either a b
Right Cons
cs
lookupData Reference
rf DataSpec
_ = [Char] -> Either [Char] Cons
forall a b. a -> Either a b
Left ([Char] -> Either [Char] Cons) -> [Char] -> Either [Char] Cons
forall a b. (a -> b) -> a -> b
$ [Char]
"unknown data reference: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Reference -> [Char]
forall a. Show a => a -> [Char]
show Reference
rf

lookupAbil :: Reference -> DataSpec -> Either String Cons
lookupAbil :: Reference -> DataSpec -> Either [Char] Cons
lookupAbil Reference
rf (Reference -> DataSpec -> Maybe (Either Cons Cons)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Reference
rf -> Just Either Cons Cons
econs) =
  case Either Cons Cons
econs of
    Right Cons
_ -> [Char] -> Either [Char] Cons
forall a b. a -> Either a b
Left ([Char] -> Either [Char] Cons) -> [Char] -> Either [Char] Cons
forall a b. (a -> b) -> a -> b
$ [Char]
"ability matching on data: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Reference -> [Char]
forall a. Show a => a -> [Char]
show Reference
rf
    Left Cons
cs -> Cons -> Either [Char] Cons
forall a b. b -> Either a b
Right (Cons -> Either [Char] Cons) -> Cons -> Either [Char] Cons
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Cons -> Cons
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+) Cons
cs
lookupAbil Reference
rf DataSpec
_ = [Char] -> Either [Char] Cons
forall a b. a -> Either a b
Left ([Char] -> Either [Char] Cons) -> [Char] -> Either [Char] Cons
forall a b. (a -> b) -> a -> b
$ [Char]
"unknown ability reference: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Reference -> [Char]
forall a. Show a => a -> [Char]
show Reference
rf

compile :: (Var v) => DataSpec -> Ctx v -> PatternMatrix v -> Term v
compile :: forall v. Var v => DataSpec -> Ctx v -> PatternMatrix v -> Term v
compile DataSpec
_ Ctx v
_ (PM []) = Term2 v () () v () -> [Term2 v () () v ()] -> Term2 v () () v ()
forall v a vt at ap.
(Ord v, Semigroup a) =>
Term2 vt at ap v a -> [Term2 vt at ap v a] -> Term2 vt at ap v a
apps' Term2 v () () v ()
forall {vt} {at} {ap}. Term2 vt at ap v ()
bu [() -> Text -> Term2 v () () v ()
forall v a vt at ap. Ord v => a -> Text -> Term2 vt at ap v a
text () Text
"pattern match failure"]
  where
    bu :: Term2 vt at ap v ()
bu = () -> Reference -> Term2 vt at ap v ()
forall v a vt at ap. Ord v => a -> Reference -> Term2 vt at ap v a
ref () (Text -> Reference
forall t h. t -> Reference' t h
Builtin Text
"bug")
compile DataSpec
spec Ctx v
ctx m :: PatternMatrix v
m@(PM (PatternRow v
r : [PatternRow v]
rs))
  | PatternRow v -> Bool
forall v. PatternRow v -> Bool
rowIrrefutable PatternRow v
r =
      case PatternRow v -> Maybe (Term2 v () () v ())
forall v. PatternRow v -> Maybe (Term v)
guard PatternRow v
r of
        Maybe (Term2 v () () v ())
Nothing -> PatternRow v -> Term2 v () () v ()
forall v. PatternRow v -> Term v
body PatternRow v
r
        Just Term2 v () () v ()
g -> ()
-> Term2 v () () v ()
-> Term2 v () () v ()
-> Term2 v () () v ()
-> Term2 v () () v ()
forall v a vt at ap.
Ord v =>
a
-> Term2 vt at ap v a
-> Term2 vt at ap v a
-> Term2 vt at ap v a
-> Term2 vt at ap v a
iff ()
forall a. Monoid a => a
mempty Term2 v () () v ()
g (PatternRow v -> Term2 v () () v ()
forall v. PatternRow v -> Term v
body PatternRow v
r) (Term2 v () () v () -> Term2 v () () v ())
-> Term2 v () () v () -> Term2 v () () v ()
forall a b. (a -> b) -> a -> b
$ DataSpec -> Ctx v -> PatternMatrix v -> Term2 v () () v ()
forall v. Var v => DataSpec -> Ctx v -> PatternMatrix v -> Term v
compile DataSpec
spec Ctx v
ctx ([PatternRow v] -> PatternMatrix v
forall v. [PatternRow v] -> PatternMatrix v
PM [PatternRow v]
rs)
  | PData Reference
rf <- PType
ty,
    Reference
rf Reference -> Reference -> Bool
forall a. Eq a => a -> a -> Bool
== Reference
Rf.listRef =
      ()
-> Term2 v () () v ()
-> [MatchCase () (Term2 v () () v ())]
-> Term2 v () () v ()
forall v a vt at.
Ord v =>
a
-> Term2 vt at a v a
-> [MatchCase a (Term2 vt at a v a)]
-> Term2 vt at a v a
match () (() -> v -> Term2 v () () v ()
forall a v vt at ap. a -> v -> Term2 vt at ap v a
var () v
v) ([MatchCase () (Term2 v () () v ())] -> Term2 v () () v ())
-> [MatchCase () (Term2 v () () v ())] -> Term2 v () () v ()
forall a b. (a -> b) -> a -> b
$
        DataSpec
-> Ctx v
-> (Pattern (), [(v, PType)], PatternMatrix v)
-> MatchCase () (Term2 v () () v ())
forall v.
Var v =>
DataSpec
-> Ctx v
-> (Pattern (), [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCaseBuiltin DataSpec
spec Ctx v
ctx
          ((Pattern (), [(v, PType)], PatternMatrix v)
 -> MatchCase () (Term2 v () () v ()))
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
-> [MatchCase () (Term2 v () () v ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set v
-> v
-> PatternMatrix v
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
forall v.
Var v =>
Set v
-> v
-> PatternMatrix v
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
splitMatrixSeq (Ctx v -> Set v
forall k a. Map k a -> Set k
Map.keysSet Ctx v
ctx Set v -> Set v -> Set v
forall a. Semigroup a => a -> a -> a
<> PatternMatrix v -> Set v
forall v. Ord v => PatternMatrix v -> Set v
usedVars PatternMatrix v
m) v
v PatternMatrix v
m
  | PData Reference
rf <- PType
ty,
    Reference
rf Reference -> Set Reference -> Bool
forall a. Ord a => a -> Set a -> Bool
`member` Set Reference
builtinCase =
      ()
-> Term2 v () () v ()
-> [MatchCase () (Term2 v () () v ())]
-> Term2 v () () v ()
forall v a vt at.
Ord v =>
a
-> Term2 vt at a v a
-> [MatchCase a (Term2 vt at a v a)]
-> Term2 vt at a v a
match () (() -> v -> Term2 v () () v ()
forall a v vt at ap. a -> v -> Term2 vt at ap v a
var () v
v) ([MatchCase () (Term2 v () () v ())] -> Term2 v () () v ())
-> [MatchCase () (Term2 v () () v ())] -> Term2 v () () v ()
forall a b. (a -> b) -> a -> b
$
        DataSpec
-> Ctx v
-> (Pattern (), [(v, PType)], PatternMatrix v)
-> MatchCase () (Term2 v () () v ())
forall v.
Var v =>
DataSpec
-> Ctx v
-> (Pattern (), [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCaseBuiltin DataSpec
spec Ctx v
ctx
          ((Pattern (), [(v, PType)], PatternMatrix v)
 -> MatchCase () (Term2 v () () v ()))
-> [(Pattern (), [(v, PType)], PatternMatrix v)]
-> [MatchCase () (Term2 v () () v ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v
-> PatternMatrix v -> [(Pattern (), [(v, PType)], PatternMatrix v)]
forall v.
Var v =>
v
-> PatternMatrix v -> [(Pattern (), [(v, PType)], PatternMatrix v)]
splitMatrixBuiltin v
v PatternMatrix v
m
  | PData Reference
rf <- PType
ty =
      case Reference -> DataSpec -> Either [Char] Cons
lookupData Reference
rf DataSpec
spec of
        Right Cons
cons ->
          ()
-> Term2 v () () v ()
-> [MatchCase () (Term2 v () () v ())]
-> Term2 v () () v ()
forall v a vt at.
Ord v =>
a
-> Term2 vt at a v a
-> [MatchCase a (Term2 vt at a v a)]
-> Term2 vt at a v a
match () (() -> v -> Term2 v () () v ()
forall a v vt at ap. a -> v -> Term2 vt at ap v a
var () v
v) ([MatchCase () (Term2 v () () v ())] -> Term2 v () () v ())
-> [MatchCase () (Term2 v () () v ())] -> Term2 v () () v ()
forall a b. (a -> b) -> a -> b
$
            DataSpec
-> Reference
-> Bool
-> Cons
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term2 v () () v ())
forall v.
Var v =>
DataSpec
-> Reference
-> Bool
-> Cons
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCase DataSpec
spec Reference
rf Bool
False Cons
cons Ctx v
ctx
              ((Int, [(v, PType)], PatternMatrix v)
 -> MatchCase () (Term2 v () () v ()))
-> [(Int, [(v, PType)], PatternMatrix v)]
-> [MatchCase () (Term2 v () () v ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> v
-> Maybe Reference
-> NCons
-> PatternMatrix v
-> [(Int, [(v, PType)], PatternMatrix v)]
forall v.
Var v =>
v
-> Maybe Reference
-> NCons
-> PatternMatrix v
-> [(Int, [(v, PType)], PatternMatrix v)]
splitMatrix v
v (Reference -> Maybe Reference
forall a. a -> Maybe a
Just Reference
rf) (Cons -> NCons
numberCons Cons
cons) PatternMatrix v
m
        Left [Char]
err -> [Char] -> Term2 v () () v ()
forall a. HasCallStack => [Char] -> a
internalBug [Char]
err
  | PReq Set Reference
rfs <- PType
ty =
      ()
-> Term2 v () () v ()
-> [MatchCase () (Term2 v () () v ())]
-> Term2 v () () v ()
forall v a vt at.
Ord v =>
a
-> Term2 vt at a v a
-> [MatchCase a (Term2 vt at a v a)]
-> Term2 vt at a v a
match () (() -> v -> Term2 v () () v ()
forall a v vt at ap. a -> v -> Term2 vt at ap v a
var () v
v) ([MatchCase () (Term2 v () () v ())] -> Term2 v () () v ())
-> [MatchCase () (Term2 v () () v ())] -> Term2 v () () v ()
forall a b. (a -> b) -> a -> b
$
        [ DataSpec
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term2 v () () v ())
forall v.
Var v =>
DataSpec
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCasePure DataSpec
spec Ctx v
ctx (Int, [(v, PType)], PatternMatrix v)
tup
          | (Int, [(v, PType)], PatternMatrix v)
tup <- v
-> Maybe Reference
-> NCons
-> PatternMatrix v
-> [(Int, [(v, PType)], PatternMatrix v)]
forall v.
Var v =>
v
-> Maybe Reference
-> NCons
-> PatternMatrix v
-> [(Int, [(v, PType)], PatternMatrix v)]
splitMatrix v
v Maybe Reference
forall a. Maybe a
Nothing [(-Int
1, Int
1)] PatternMatrix v
m
        ]
          [MatchCase () (Term2 v () () v ())]
-> [MatchCase () (Term2 v () () v ())]
-> [MatchCase () (Term2 v () () v ())]
forall a. [a] -> [a] -> [a]
++ [ DataSpec
-> Reference
-> Bool
-> Cons
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term2 v () () v ())
forall v.
Var v =>
DataSpec
-> Reference
-> Bool
-> Cons
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCase DataSpec
spec Reference
rf Bool
True Cons
cons Ctx v
ctx (Int, [(v, PType)], PatternMatrix v)
tup
               | Reference
rf <- Set Reference -> [Reference]
forall a. Set a -> [a]
Set.toList Set Reference
rfs,
                 Right Cons
cons <- [Reference -> DataSpec -> Either [Char] Cons
lookupAbil Reference
rf DataSpec
spec],
                 (Int, [(v, PType)], PatternMatrix v)
tup <- v
-> Maybe Reference
-> NCons
-> PatternMatrix v
-> [(Int, [(v, PType)], PatternMatrix v)]
forall v.
Var v =>
v
-> Maybe Reference
-> NCons
-> PatternMatrix v
-> [(Int, [(v, PType)], PatternMatrix v)]
splitMatrix v
v (Reference -> Maybe Reference
forall a. a -> Maybe a
Just Reference
rf) (Cons -> NCons
numberCons Cons
cons) PatternMatrix v
m
             ]
  | PType
Unknown <- PType
ty =
      [Char] -> Term2 v () () v ()
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"unknown pattern compilation type"
  where
    v :: v
v = [Heuristic v] -> PatternMatrix v -> v
forall v. [Heuristic v] -> PatternMatrix v -> v
choose [Heuristic v]
forall v. [Heuristic v]
heuristics PatternMatrix v
m
    ty :: PType
ty = PType -> v -> Ctx v -> PType
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault PType
Unknown v
v Ctx v
ctx

buildCaseBuiltin ::
  (Var v) =>
  DataSpec ->
  Ctx v ->
  (P.Pattern (), [(v, PType)], PatternMatrix v) ->
  MatchCase () (Term v)
buildCaseBuiltin :: forall v.
Var v =>
DataSpec
-> Ctx v
-> (Pattern (), [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCaseBuiltin DataSpec
spec Map v PType
ctx0 (Pattern ()
p, [(v, PType)]
vrs, PatternMatrix v
m) =
  Pattern () -> Maybe (Term v) -> Term v -> MatchCase () (Term v)
forall loc a. Pattern loc -> Maybe a -> a -> MatchCase loc a
MatchCase Pattern ()
p Maybe (Term v)
forall a. Maybe a
Nothing (Term v -> MatchCase () (Term v))
-> (Term v -> Term v) -> Term v -> MatchCase () (Term v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((), v)] -> Term v -> Term v
forall v a (f :: * -> *).
Ord v =>
[(a, v)] -> Term f v a -> Term f v a
absChain' [((), v)]
vs (Term v -> MatchCase () (Term v))
-> Term v -> MatchCase () (Term v)
forall a b. (a -> b) -> a -> b
$ DataSpec -> Map v PType -> PatternMatrix v -> Term v
forall v. Var v => DataSpec -> Ctx v -> PatternMatrix v -> Term v
compile DataSpec
spec Map v PType
ctx PatternMatrix v
m
  where
    vs :: [((), v)]
vs = ((),) (v -> ((), v)) -> ((v, PType) -> v) -> (v, PType) -> ((), v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v, PType) -> v
forall a b. (a, b) -> a
fst ((v, PType) -> ((), v)) -> [(v, PType)] -> [((), v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, PType)]
vrs
    ctx :: Map v PType
ctx = [(v, PType)] -> Map v PType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(v, PType)]
vrs Map v PType -> Map v PType -> Map v PType
forall a. Semigroup a => a -> a -> a
<> Map v PType
ctx0

buildCasePure ::
  (Var v) =>
  DataSpec ->
  Ctx v ->
  (Int, [(v, PType)], PatternMatrix v) ->
  MatchCase () (Term v)
buildCasePure :: forall v.
Var v =>
DataSpec
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCasePure DataSpec
spec Map v PType
ctx0 (Int
_, [(v, PType)]
vts, PatternMatrix v
m) =
  Pattern () -> Maybe (Term v) -> Term v -> MatchCase () (Term v)
forall loc a. Pattern loc -> Maybe a -> a -> MatchCase loc a
MatchCase Pattern ()
pat Maybe (Term v)
forall a. Maybe a
Nothing (Term v -> MatchCase () (Term v))
-> (Term v -> Term v) -> Term v -> MatchCase () (Term v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((), v)] -> Term v -> Term v
forall v a (f :: * -> *).
Ord v =>
[(a, v)] -> Term f v a -> Term f v a
absChain' [((), v)]
vs (Term v -> MatchCase () (Term v))
-> Term v -> MatchCase () (Term v)
forall a b. (a -> b) -> a -> b
$ DataSpec -> Map v PType -> PatternMatrix v -> Term v
forall v. Var v => DataSpec -> Ctx v -> PatternMatrix v -> Term v
compile DataSpec
spec Map v PType
ctx PatternMatrix v
m
  where
    vp :: Pattern ()
vp
      | [] <- [(v, PType)]
vts = () -> Pattern ()
forall loc. loc -> Pattern loc
P.Unbound ()
      | Bool
otherwise = () -> Pattern ()
forall loc. loc -> Pattern loc
P.Var ()
    pat :: Pattern ()
pat = () -> Pattern () -> Pattern ()
forall loc. loc -> Pattern loc -> Pattern loc
P.EffectPure () Pattern ()
vp
    vs :: [((), v)]
vs = ((),) (v -> ((), v)) -> ((v, PType) -> v) -> (v, PType) -> ((), v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v, PType) -> v
forall a b. (a, b) -> a
fst ((v, PType) -> ((), v)) -> [(v, PType)] -> [((), v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, PType)]
vts
    ctx :: Map v PType
ctx = [(v, PType)] -> Map v PType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(v, PType)]
vts Map v PType -> Map v PType -> Map v PType
forall a. Semigroup a => a -> a -> a
<> Map v PType
ctx0

buildCase ::
  (Var v) =>
  DataSpec ->
  Reference ->
  Bool ->
  Cons ->
  Ctx v ->
  (Int, [(v, PType)], PatternMatrix v) ->
  MatchCase () (Term v)
buildCase :: forall v.
Var v =>
DataSpec
-> Reference
-> Bool
-> Cons
-> Ctx v
-> (Int, [(v, PType)], PatternMatrix v)
-> MatchCase () (Term v)
buildCase DataSpec
spec Reference
r Bool
eff Cons
cons Map v PType
ctx0 (Int
t, [(v, PType)]
vts, PatternMatrix v
m) =
  Pattern () -> Maybe (Term v) -> Term v -> MatchCase () (Term v)
forall loc a. Pattern loc -> Maybe a -> a -> MatchCase loc a
MatchCase Pattern ()
pat Maybe (Term v)
forall a. Maybe a
Nothing (Term v -> MatchCase () (Term v))
-> (Term v -> Term v) -> Term v -> MatchCase () (Term v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((), v)] -> Term v -> Term v
forall v a (f :: * -> *).
Ord v =>
[(a, v)] -> Term f v a -> Term f v a
absChain' [((), v)]
vs (Term v -> MatchCase () (Term v))
-> Term v -> MatchCase () (Term v)
forall a b. (a -> b) -> a -> b
$ DataSpec -> Map v PType -> PatternMatrix v -> Term v
forall v. Var v => DataSpec -> Ctx v -> PatternMatrix v -> Term v
compile DataSpec
spec Map v PType
ctx PatternMatrix v
m
  where
    pat :: Pattern ()
pat = Bool
-> GConstructorReference Reference
-> [((), v)]
-> Int
-> Pattern ()
forall v.
Bool -> GConstructorReference Reference -> [v] -> Int -> Pattern ()
buildPattern Bool
eff (Reference -> ConstructorId -> GConstructorReference Reference
forall r. r -> ConstructorId -> GConstructorReference r
ConstructorReference Reference
r (Int -> ConstructorId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
t)) [((), v)]
vs (Int -> Pattern ()) -> Int -> Pattern ()
forall a b. (a -> b) -> a -> b
$ Cons
cons Cons -> Int -> Int
forall a. HasCallStack => [a] -> Int -> a
!! Int
t
    vs :: [((), v)]
vs = ((),) (v -> ((), v)) -> ((v, PType) -> v) -> (v, PType) -> ((), v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v, PType) -> v
forall a b. (a, b) -> a
fst ((v, PType) -> ((), v)) -> [(v, PType)] -> [((), v)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(v, PType)]
vts
    ctx :: Map v PType
ctx = [(v, PType)] -> Map v PType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(v, PType)]
vts Map v PType -> Map v PType -> Map v PType
forall a. Semigroup a => a -> a -> a
<> Map v PType
ctx0

mkRow ::
  (Var v) =>
  v ->
  MatchCase a (Term v) ->
  State Word64 (PatternRow v)
mkRow :: forall v a.
Var v =>
v -> MatchCase a (Term v) -> State ConstructorId (PatternRow v)
mkRow v
sv (MatchCase (Pattern a -> Pattern a
forall a. Pattern a -> Pattern a
normalizeSeqP -> Pattern a
p0) Maybe (Term v)
g0 (AbsN' [v]
vs Term v
b)) =
  (ConstructorId -> (PatternRow v, ConstructorId))
-> StateT ConstructorId Identity (PatternRow v)
forall a.
(ConstructorId -> (a, ConstructorId))
-> StateT ConstructorId Identity a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state ((ConstructorId -> (PatternRow v, ConstructorId))
 -> StateT ConstructorId Identity (PatternRow v))
-> (ConstructorId -> (PatternRow v, ConstructorId))
-> StateT ConstructorId Identity (PatternRow v)
forall a b. (a -> b) -> a -> b
$ \ConstructorId
w -> case State (ConstructorId, [v], Map v v) (Pattern v)
-> (ConstructorId, [v], Map v v)
-> (Pattern v, (ConstructorId, [v], Map v v))
forall s a. State s a -> s -> (a, s)
runState (Pattern a -> v -> State (ConstructorId, [v], Map v v) (Pattern v)
forall v a. Var v => Pattern a -> v -> PPM v (Pattern v)
prepareAs Pattern a
p0 v
sv) (ConstructorId
w, [v]
vs, Map v v
forall a. Monoid a => a
mempty) of
    (Pattern v
p, (ConstructorId
w, [], Map v v
rn)) ->
      (,ConstructorId
w) (PatternRow v -> (PatternRow v, ConstructorId))
-> PatternRow v -> (PatternRow v, ConstructorId)
forall a b. (a -> b) -> a -> b
$
        [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
forall v. [Pattern v] -> Maybe (Term v) -> Term v -> PatternRow v
PR
          ((Pattern v -> Bool) -> [Pattern v] -> [Pattern v]
forall a. (a -> Bool) -> [a] -> [a]
filter Pattern v -> Bool
forall a. Pattern a -> Bool
refutable [Pattern v
p])
          (Map v v -> Term v -> Term v
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
rn (Term v -> Term v) -> Maybe (Term v) -> Maybe (Term v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Term v)
g)
          (Map v v -> Term v -> Term v
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames Map v v
rn Term v
b)
    (Pattern v, (ConstructorId, [v], Map v v))
_ -> [Char] -> (PatternRow v, ConstructorId)
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"mkRow: not all variables used"
  where
    g :: Maybe (Term v)
g = case Maybe (Term v)
g0 of
      Just (AbsN' [v]
us Term v
g)
        | [v]
us [v] -> [v] -> Bool
forall a. Eq a => a -> a -> Bool
== [v]
vs -> Term v -> Maybe (Term v)
forall a. a -> Maybe a
Just Term v
g
        | [v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [v]
us Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [v]
vs ->
            Term v -> Maybe (Term v)
forall a. a -> Maybe a
Just (Term v -> Maybe (Term v)) -> Term v -> Maybe (Term v)
forall a b. (a -> b) -> a -> b
$ Map v v -> Term v -> Term v
forall (f :: * -> *) v a.
(Foldable f, Functor f, Var v) =>
Map v v -> Term f v a -> Term f v a
renames ([(v, v)] -> Map v v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([v] -> [v] -> [(v, v)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
us [v]
vs)) Term v
g
        | Bool
otherwise ->
            [Char] -> Maybe (Term v)
forall a. HasCallStack => [Char] -> a
internalBug [Char]
"mkRow: guard variables do not match body"
      Maybe (Term v)
Nothing -> Maybe (Term v)
forall a. Maybe a
Nothing

initialize ::
  (Var v) =>
  PType ->
  Term v ->
  [MatchCase () (Term v)] ->
  (Maybe v, (v, PType), PatternMatrix v)
initialize :: forall v.
Var v =>
PType
-> Term v
-> [MatchCase () (Term v)]
-> (Maybe v, (v, PType), PatternMatrix v)
initialize PType
r Term v
sc [MatchCase () (Term v)]
cs =
  ( Maybe v
lv,
    (v
sv, PType
r),
    [PatternRow v] -> PatternMatrix v
forall v. [PatternRow v] -> PatternMatrix v
PM ([PatternRow v] -> PatternMatrix v)
-> [PatternRow v] -> PatternMatrix v
forall a b. (a -> b) -> a -> b
$ State ConstructorId [PatternRow v]
-> ConstructorId -> [PatternRow v]
forall s a. State s a -> s -> a
evalState ((MatchCase () (Term v)
 -> StateT ConstructorId Identity (PatternRow v))
-> [MatchCase () (Term v)] -> State ConstructorId [PatternRow v]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (v
-> MatchCase () (Term v)
-> StateT ConstructorId Identity (PatternRow v)
forall v a.
Var v =>
v -> MatchCase a (Term v) -> State ConstructorId (PatternRow v)
mkRow v
sv) [MatchCase () (Term v)]
cs) ConstructorId
1
  )
  where
    (Maybe v
lv, v
sv)
      | Var' v
v <- Term v
sc = (Maybe v
forall a. Maybe a
Nothing, v
v)
      | v
pv <- ConstructorId -> v -> v
forall v. Var v => ConstructorId -> v -> v
freshenId ConstructorId
0 (v -> v) -> v -> v
forall a b. (a -> b) -> a -> b
$ Type -> v
forall v. Var v => Type -> v
typed Type
Pattern =
          (v -> Maybe v
forall a. a -> Maybe a
Just v
pv, v
pv)

splitPatterns :: (Var v) => DataSpec -> Term v -> Term v
splitPatterns :: forall v. Var v => DataSpec -> Term v -> Term v
splitPatterns DataSpec
spec0 = (Term (F v () ()) v () -> Maybe (Term (F v () ()) v ()))
-> Term (F v () ()) v () -> Term (F v () ()) v ()
forall (f :: * -> *) v a.
(Traversable f, Ord v) =>
(Term f v a -> Maybe (Term f v a)) -> Term f v a -> Term f v a
visitPure ((Term (F v () ()) v () -> Maybe (Term (F v () ()) v ()))
 -> Term (F v () ()) v () -> Term (F v () ()) v ())
-> (Term (F v () ()) v () -> Maybe (Term (F v () ()) v ()))
-> Term (F v () ()) v ()
-> Term (F v () ()) v ()
forall a b. (a -> b) -> a -> b
$ \case
  Match' Term (F v () ()) v ()
sc0 [MatchCase () (Term (F v () ()) v ())]
cs0
    | PType
ty <- [Pattern ()] -> PType
forall a. Show a => [Pattern a] -> PType
determineType ([Pattern ()] -> PType) -> [Pattern ()] -> PType
forall a b. (a -> b) -> a -> b
$ MatchCase () (Term (F v () ()) v ()) -> Pattern ()
forall {loc} {a}. MatchCase loc a -> Pattern loc
p (MatchCase () (Term (F v () ()) v ()) -> Pattern ())
-> [MatchCase () (Term (F v () ()) v ())] -> [Pattern ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MatchCase () (Term (F v () ()) v ())]
cs0,
      (Maybe v
lv, (v, PType)
scrut, PatternMatrix v
pm) <- PType
-> Term (F v () ()) v ()
-> [MatchCase () (Term (F v () ()) v ())]
-> (Maybe v, (v, PType), PatternMatrix v)
forall v.
Var v =>
PType
-> Term v
-> [MatchCase () (Term v)]
-> (Maybe v, (v, PType), PatternMatrix v)
initialize PType
ty Term (F v () ()) v ()
sc [MatchCase () (Term (F v () ()) v ())]
cs,
      Term (F v () ()) v ()
body <- DataSpec -> Ctx v -> PatternMatrix v -> Term (F v () ()) v ()
forall v. Var v => DataSpec -> Ctx v -> PatternMatrix v -> Term v
compile DataSpec
spec ((v -> PType -> Ctx v) -> (v, PType) -> Ctx v
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> PType -> Ctx v
forall k a. k -> a -> Map k a
Map.singleton (v, PType)
scrut) PatternMatrix v
pm ->
        Term (F v () ()) v () -> Maybe (Term (F v () ()) v ())
forall a. a -> Maybe a
Just (Term (F v () ()) v () -> Maybe (Term (F v () ()) v ()))
-> Term (F v () ()) v () -> Maybe (Term (F v () ()) v ())
forall a b. (a -> b) -> a -> b
$ case Maybe v
lv of
          Just v
v -> Bool
-> [(((), v), Term (F v () ()) v ())]
-> Term (F v () ()) v ()
-> Term (F v () ()) v ()
forall v a vt at ap.
(Ord v, Semigroup a) =>
Bool
-> [((a, v), Term2 vt at ap v a)]
-> Term2 vt at ap v a
-> Term2 vt at ap v a
let1 Bool
False [(((), v
v), Term (F v () ()) v ()
sc)] Term (F v () ()) v ()
body
          Maybe v
_ -> Term (F v () ()) v ()
body
    where
      sc :: Term (F v () ()) v ()
sc = DataSpec -> Term (F v () ()) v () -> Term (F v () ()) v ()
forall v. Var v => DataSpec -> Term v -> Term v
splitPatterns DataSpec
spec Term (F v () ()) v ()
sc0
      cs :: [MatchCase () (Term (F v () ()) v ())]
cs = (Term (F v () ()) v () -> Term (F v () ()) v ())
-> MatchCase () (Term (F v () ()) v ())
-> MatchCase () (Term (F v () ()) v ())
forall a b. (a -> b) -> MatchCase () a -> MatchCase () b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DataSpec -> Term (F v () ()) v () -> Term (F v () ()) v ()
forall v. Var v => DataSpec -> Term v -> Term v
splitPatterns DataSpec
spec) (MatchCase () (Term (F v () ()) v ())
 -> MatchCase () (Term (F v () ()) v ()))
-> [MatchCase () (Term (F v () ()) v ())]
-> [MatchCase () (Term (F v () ()) v ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MatchCase () (Term (F v () ()) v ())]
cs0
  Term (F v () ()) v ()
_ -> Maybe (Term (F v () ()) v ())
forall a. Maybe a
Nothing
  where
    p :: MatchCase loc a -> Pattern loc
p (MatchCase Pattern loc
pp Maybe a
_ a
_) = Pattern loc
pp
    spec :: DataSpec
spec = Reference -> Either Cons Cons -> DataSpec -> DataSpec
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Reference
Rf.booleanRef (Cons -> Either Cons Cons
forall a b. b -> Either a b
Right [Int
0, Int
0]) DataSpec
spec0

builtinCase :: Set Reference
builtinCase :: Set Reference
builtinCase =
  [Reference] -> Set Reference
forall a. Ord a => [a] -> Set a
Set.fromList
    [ Reference
Rf.intRef,
      Reference
Rf.natRef,
      Reference
Rf.floatRef,
      Reference
Rf.textRef,
      Reference
Rf.charRef
    ]

determineType :: (Show a) => [P.Pattern a] -> PType
determineType :: forall a. Show a => [Pattern a] -> PType
determineType = (Pattern a -> PType) -> [Pattern a] -> PType
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Pattern a -> PType
forall {loc}. Pattern loc -> PType
f
  where
    f :: Pattern loc -> PType
f (P.As loc
_ Pattern loc
p) = Pattern loc -> PType
f Pattern loc
p
    f P.Int {} = Reference -> PType
PData Reference
Rf.intRef
    f P.Nat {} = Reference -> PType
PData Reference
Rf.natRef
    f P.Float {} = Reference -> PType
PData Reference
Rf.floatRef
    f P.Boolean {} = Reference -> PType
PData Reference
Rf.booleanRef
    f P.Text {} = Reference -> PType
PData Reference
Rf.textRef
    f P.Char {} = Reference -> PType
PData Reference
Rf.charRef
    f P.SequenceLiteral {} = Reference -> PType
PData Reference
Rf.listRef
    f P.SequenceOp {} = Reference -> PType
PData Reference
Rf.listRef
    f (P.Constructor loc
_ GConstructorReference Reference
r [Pattern loc]
_) = Reference -> PType
PData (GConstructorReference Reference
r GConstructorReference Reference
-> Getting Reference (GConstructorReference Reference) Reference
-> Reference
forall s a. s -> Getting a s a -> a
^. Getting Reference (GConstructorReference Reference) Reference
forall r s (f :: * -> *).
Functor f =>
(r -> f s)
-> GConstructorReference r -> f (GConstructorReference s)
ConstructorReference.reference_)
    f (P.EffectBind loc
_ GConstructorReference Reference
r [Pattern loc]
_ Pattern loc
_) = Set Reference -> PType
PReq (Set Reference -> PType) -> Set Reference -> PType
forall a b. (a -> b) -> a -> b
$ Reference -> Set Reference
forall a. a -> Set a
Set.singleton (GConstructorReference Reference
r GConstructorReference Reference
-> Getting Reference (GConstructorReference Reference) Reference
-> Reference
forall s a. s -> Getting a s a -> a
^. Getting Reference (GConstructorReference Reference) Reference
forall r s (f :: * -> *).
Functor f =>
(r -> f s)
-> GConstructorReference r -> f (GConstructorReference s)
ConstructorReference.reference_)
    f P.EffectPure {} = Set Reference -> PType
PReq Set Reference
forall a. Monoid a => a
mempty
    f Pattern loc
_ = PType
Unknown