{-# LANGUAGE LambdaCase, StandaloneDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE OverloadedStrings #-}

module Funcons.Patterns where

import Funcons.MSOS
import Funcons.Types
import Funcons.Substitution
import Funcons.Exceptions
import Funcons.Operations (isGround)

import Control.Applicative
import Control.Monad (foldM, forM)
import Data.Function (on)
import Data.List (sortBy, intercalate)
import Data.Monoid
import Data.Text (unpack)
import Data.Foldable (toList)
import qualified Data.Map as M 

-- pattern matching
type Matcher a = [a] -> Int -> Env -> Rewrite [(Int, Env)]
type SeqVarInfo = (MetaVar, SeqSortOp, Maybe FTerm)

singleMatcher :: (a -> b -> Env -> Rewrite Env) -> b -> Matcher a
singleMatcher :: (a -> b -> Env -> Rewrite Env) -> b -> Matcher a
singleMatcher a -> b -> Env -> Rewrite Env
p b
pat [a]
str Int
k Env
env = case Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
k [a]
str of
    []  -> [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    a
f:[a]
_ -> Rewrite Env -> Rewrite (Either IException Env)
forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch (a -> b -> Env -> Rewrite Env
p a
f b
pat Env
env) Rewrite (Either IException Env)
-> (Either IException Env -> Rewrite [(Int, Env)])
-> Rewrite [(Int, Env)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Left IException
ie | IException -> Bool
failsRule IException
ie  -> [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                    | Bool
otherwise     -> IException -> Rewrite [(Int, Env)]
forall a. IException -> Rewrite a
rewrite_rethrow IException
ie
            Right Env
env'              -> [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1,Env
env')]

seqMatcher :: (a -> Maybe FTerm -> Env -> Rewrite (Maybe [a])) -> ([a] -> Levelled) 
                -> SeqVarInfo -> Matcher a
seqMatcher :: (a -> Maybe FTerm -> Env -> Rewrite (Maybe [a]))
-> ([a] -> Levelled) -> SeqVarInfo -> Matcher a
seqMatcher a -> Maybe FTerm -> Env -> Rewrite (Maybe [a])
p [a] -> Levelled
level (MetaVar
var, SeqSortOp
op, Maybe FTerm
mty) [a]
str Int
k Env
env = case SeqSortOp
op of
    SeqSortOp
QuestionMarkOp -> ([[a]] -> Bool) -> Rewrite [(Int, Env)]
makeResults ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<=Int
1) (Int -> Bool) -> ([[a]] -> Int) -> [[a]] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[a]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length)
    SeqSortOp
PlusOp         -> case [a]
str of  
                        [] -> [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                        [a]
_  -> ([[a]] -> Bool) -> Rewrite [(Int, Env)]
makeResults ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
1) (Int -> Bool) -> ([[a]] -> Int) -> [[a]] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[a]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length)
    SeqSortOp
StarOp         -> ([[a]] -> Bool) -> Rewrite [(Int, Env)]
makeResults (Bool -> [[a]] -> Bool
forall a b. a -> b -> a
const Bool
True)
    where makeResults :: ([[a]] -> Bool) -> Rewrite [(Int, Env)]
makeResults [[a]] -> Bool
filter_op = do
            [[a]]
furthest <- (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
forall a. (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
takeWhileM (\a
a -> a -> Maybe FTerm -> Env -> Rewrite (Maybe [a])
p a
a Maybe FTerm
mty Env
env) (Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
k [a]
str)
            [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Env)] -> [(Int, Env)]
sortWithPref ([(Int, Env)] -> [(Int, Env)]) -> [(Int, Env)] -> [(Int, Env)]
forall a b. (a -> b) -> a -> b
$ ([[a]] -> (Int, Env)) -> [[[a]]] -> [(Int, Env)]
forall a b. (a -> b) -> [a] -> [b]
map [[a]] -> (Int, Env)
forall (t :: * -> *). Foldable t => t [a] -> (Int, Env)
ins (([[a]] -> Bool) -> [[[a]]] -> [[[a]]]
forall a. (a -> Bool) -> [a] -> [a]
filter [[a]] -> Bool
filter_op ([[[a]]] -> [[[a]]]) -> [[[a]]] -> [[[a]]]
forall a b. (a -> b) -> a -> b
$ [[a]] -> [[[a]]]
forall a. [a] -> [[a]]
ordered_subsequences [[a]]
furthest))
            where
              ins :: t [a] -> (Int, Env)
ins t [a]
fs  = (Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+t [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t [a]
fs, MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var ([a] -> Levelled
level (t [a] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat t [a]
fs)) Env
env)

              takeWhileM :: (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
              takeWhileM :: (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
takeWhileM a -> Rewrite (Maybe [a])
_ [] = [[a]] -> Rewrite [[a]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
              takeWhileM a -> Rewrite (Maybe [a])
p (a
x:[a]
xs) = Rewrite (Maybe [a]) -> Rewrite (Either IException (Maybe [a]))
forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch (a -> Rewrite (Maybe [a])
p a
x) Rewrite (Either IException (Maybe [a]))
-> (Either IException (Maybe [a]) -> Rewrite [[a]])
-> Rewrite [[a]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Right (Just [a]
fs)     -> ([a]
fs [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:) ([[a]] -> [[a]]) -> Rewrite [[a]] -> Rewrite [[a]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
forall a. (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
takeWhileM a -> Rewrite (Maybe [a])
p [a]
xs
                Right Maybe [a]
Nothing       -> [[a]] -> Rewrite [[a]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                Left IException
ie | IException -> Bool
failsRule IException
ie  -> [[a]] -> Rewrite [[a]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                        | Bool
otherwise     -> IException -> Rewrite [[a]]
forall a. IException -> Rewrite a
rewrite_rethrow IException
ie

              -- sorts the result in order of preference
              sortWithPref :: [(Int, Env)] -> [(Int, Env)] 
              sortWithPref :: [(Int, Env)] -> [(Int, Env)]
sortWithPref = ((Int, Env) -> (Int, Env) -> Ordering)
-> [(Int, Env)] -> [(Int, Env)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int -> Int -> Ordering
comparison (Int -> Int -> Ordering)
-> ((Int, Env) -> Int) -> (Int, Env) -> (Int, Env) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, Env) -> Int
forall a b. (a, b) -> a
fst)
                where comparison :: Int -> Int -> Ordering
comparison = case Maybe FTerm
mty of
                        Maybe FTerm
Nothing   -> Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare      -- no annotation => shortest match
                        Just  FTerm
_   -> (Int -> Int -> Ordering) -> Int -> Int -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- annoration => longest match

matching :: (a -> String) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching :: (a -> MetaVar) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching a -> MetaVar
show [a]
str [Matcher a]
ps Env
env = do 
    [(Int, Env)]
matches <- (Matcher a -> Matcher a -> Matcher a)
-> Matcher a -> [Matcher a] -> Matcher a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Matcher a -> Matcher a -> Matcher a
forall a. Matcher a -> Matcher a -> Matcher a
seqWith Matcher a
forall a. Matcher a
lastMatcher [Matcher a]
ps [a]
str Int
0 Env
env 
    let rule_fail :: IE
rule_fail = MetaVar -> IE
PatternMismatch (MetaVar
"Pattern match failed: " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ MetaVar -> [MetaVar] -> MetaVar
forall a. [a] -> [[a]] -> [a]
intercalate MetaVar
"," ((a -> MetaVar) -> [a] -> [MetaVar]
forall a b. (a -> b) -> [a] -> [b]
map a -> MetaVar
show [a]
str))
    case [(Int, Env)]
matches of
        [] -> IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw IE
rule_fail
        [(Int
_,Env
env')] -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env'
        [(Int, Env)]
_  -> MetaVar -> Rewrite Env
forall a. MetaVar -> Rewrite a
internal (MetaVar
"ambiguity not resolved") 
    where   m :: Int
m = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
str
            -- sequencing of matchers specifically to disambiguate safely
            lastMatcher :: Matcher a
            lastMatcher :: Matcher a
lastMatcher [a]
_ Int
k Env
env | Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m       = [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
k,Env
env)]
                                | Bool
otherwise    = [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return []

            seqWith :: Matcher a -> Matcher a -> Matcher a
            seqWith :: Matcher a -> Matcher a -> Matcher a
seqWith Matcher a
p Matcher a
q [a]
str Int
k Env
env = Matcher a
p [a]
str Int
k Env
env Rewrite [(Int, Env)]
-> ([(Int, Env)] -> Rewrite [(Int, Env)]) -> Rewrite [(Int, Env)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([(Int, Env)] -> (Int, Env) -> Rewrite [(Int, Env)])
-> [(Int, Env)] -> [(Int, Env)] -> Rewrite [(Int, Env)]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM [(Int, Env)] -> (Int, Env) -> Rewrite [(Int, Env)]
acceptFirst []
             where  acceptFirst :: [(Int, Env)] -> (Int, Env) -> Rewrite [(Int, Env)]
acceptFirst [(Int, Env)]
acc (Int
r, Env
env)
                        | [(Int, Env)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, Env)]
acc  = Matcher a
q [a]
str Int
r Env
env
                        | Bool
otherwise = [(Int, Env)] -> Rewrite [(Int, Env)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, Env)]
acc

ordered_subsequences :: [a] -> [[a]]
ordered_subsequences :: [a] -> [[a]]
ordered_subsequences [a]
xs = [a] -> [a] -> [[a]]
forall a. [a] -> [a] -> [[a]]
ordered_subsequences' [a]
xs []
    where   ordered_subsequences' :: [a] -> [a] -> [[a]]
ordered_subsequences' [] [a]
acc = [[a]
acc]
            ordered_subsequences' (a
x:[a]
xs) [a]
acc = [a]
acc [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [a] -> [a] -> [[a]]
ordered_subsequences' [a]
xs ([a]
acc[a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++[a
x])


-- | Patterns for matching funcon terms ('FTerm').
data FPattern   = PValue VPattern
                | PMetaVar MetaVar 
                | PSeqVar MetaVar SeqSortOp
                | PAnnotated FPattern FTerm 
                | PWildCard
                deriving (Int -> FPattern -> MetaVar -> MetaVar
[FPattern] -> MetaVar -> MetaVar
FPattern -> MetaVar
(Int -> FPattern -> MetaVar -> MetaVar)
-> (FPattern -> MetaVar)
-> ([FPattern] -> MetaVar -> MetaVar)
-> Show FPattern
forall a.
(Int -> a -> MetaVar -> MetaVar)
-> (a -> MetaVar) -> ([a] -> MetaVar -> MetaVar) -> Show a
showList :: [FPattern] -> MetaVar -> MetaVar
$cshowList :: [FPattern] -> MetaVar -> MetaVar
show :: FPattern -> MetaVar
$cshow :: FPattern -> MetaVar
showsPrec :: Int -> FPattern -> MetaVar -> MetaVar
$cshowsPrec :: Int -> FPattern -> MetaVar -> MetaVar
Show, FPattern -> FPattern -> Bool
(FPattern -> FPattern -> Bool)
-> (FPattern -> FPattern -> Bool) -> Eq FPattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FPattern -> FPattern -> Bool
$c/= :: FPattern -> FPattern -> Bool
== :: FPattern -> FPattern -> Bool
$c== :: FPattern -> FPattern -> Bool
Eq, Eq FPattern
Eq FPattern
-> (FPattern -> FPattern -> Ordering)
-> (FPattern -> FPattern -> Bool)
-> (FPattern -> FPattern -> Bool)
-> (FPattern -> FPattern -> Bool)
-> (FPattern -> FPattern -> Bool)
-> (FPattern -> FPattern -> FPattern)
-> (FPattern -> FPattern -> FPattern)
-> Ord FPattern
FPattern -> FPattern -> Bool
FPattern -> FPattern -> Ordering
FPattern -> FPattern -> FPattern
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
min :: FPattern -> FPattern -> FPattern
$cmin :: FPattern -> FPattern -> FPattern
max :: FPattern -> FPattern -> FPattern
$cmax :: FPattern -> FPattern -> FPattern
>= :: FPattern -> FPattern -> Bool
$c>= :: FPattern -> FPattern -> Bool
> :: FPattern -> FPattern -> Bool
$c> :: FPattern -> FPattern -> Bool
<= :: FPattern -> FPattern -> Bool
$c<= :: FPattern -> FPattern -> Bool
< :: FPattern -> FPattern -> Bool
$c< :: FPattern -> FPattern -> Bool
compare :: FPattern -> FPattern -> Ordering
$ccompare :: FPattern -> FPattern -> Ordering
$cp1Ord :: Eq FPattern
Ord, ReadPrec [FPattern]
ReadPrec FPattern
Int -> ReadS FPattern
ReadS [FPattern]
(Int -> ReadS FPattern)
-> ReadS [FPattern]
-> ReadPrec FPattern
-> ReadPrec [FPattern]
-> Read FPattern
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [FPattern]
$creadListPrec :: ReadPrec [FPattern]
readPrec :: ReadPrec FPattern
$creadPrec :: ReadPrec FPattern
readList :: ReadS [FPattern]
$creadList :: ReadS [FPattern]
readsPrec :: Int -> ReadS FPattern
$creadsPrec :: Int -> ReadS FPattern
Read)

f2vPattern :: FPattern -> VPattern
f2vPattern :: FPattern -> VPattern
f2vPattern (PValue VPattern
v) = VPattern
v
f2vPattern (PMetaVar MetaVar
var) = MetaVar -> VPattern
VPMetaVar MetaVar
var
f2vPattern (PSeqVar MetaVar
var SeqSortOp
op) = MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
var SeqSortOp
op
f2vPattern (PAnnotated FPattern
fp FTerm
t) = VPattern -> FTerm -> VPattern
VPAnnotated (FPattern -> VPattern
f2vPattern FPattern
fp) FTerm
t
f2vPattern FPattern
PWildCard = VPattern
VPWildCard

-- | Patterns for matching values ('Values').
data VPattern   = PADT Name [VPattern]
                | VPWildCard
--                | PList [VPattern]
                | VPMetaVar MetaVar 
                | VPAnnotated VPattern FTerm 
                | VPSeqVar MetaVar SeqSortOp
                | VPLit Values 
                | VPType TPattern
                deriving (Int -> VPattern -> MetaVar -> MetaVar
[VPattern] -> MetaVar -> MetaVar
VPattern -> MetaVar
(Int -> VPattern -> MetaVar -> MetaVar)
-> (VPattern -> MetaVar)
-> ([VPattern] -> MetaVar -> MetaVar)
-> Show VPattern
forall a.
(Int -> a -> MetaVar -> MetaVar)
-> (a -> MetaVar) -> ([a] -> MetaVar -> MetaVar) -> Show a
showList :: [VPattern] -> MetaVar -> MetaVar
$cshowList :: [VPattern] -> MetaVar -> MetaVar
show :: VPattern -> MetaVar
$cshow :: VPattern -> MetaVar
showsPrec :: Int -> VPattern -> MetaVar -> MetaVar
$cshowsPrec :: Int -> VPattern -> MetaVar -> MetaVar
Show, VPattern -> VPattern -> Bool
(VPattern -> VPattern -> Bool)
-> (VPattern -> VPattern -> Bool) -> Eq VPattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VPattern -> VPattern -> Bool
$c/= :: VPattern -> VPattern -> Bool
== :: VPattern -> VPattern -> Bool
$c== :: VPattern -> VPattern -> Bool
Eq, Eq VPattern
Eq VPattern
-> (VPattern -> VPattern -> Ordering)
-> (VPattern -> VPattern -> Bool)
-> (VPattern -> VPattern -> Bool)
-> (VPattern -> VPattern -> Bool)
-> (VPattern -> VPattern -> Bool)
-> (VPattern -> VPattern -> VPattern)
-> (VPattern -> VPattern -> VPattern)
-> Ord VPattern
VPattern -> VPattern -> Bool
VPattern -> VPattern -> Ordering
VPattern -> VPattern -> VPattern
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
min :: VPattern -> VPattern -> VPattern
$cmin :: VPattern -> VPattern -> VPattern
max :: VPattern -> VPattern -> VPattern
$cmax :: VPattern -> VPattern -> VPattern
>= :: VPattern -> VPattern -> Bool
$c>= :: VPattern -> VPattern -> Bool
> :: VPattern -> VPattern -> Bool
$c> :: VPattern -> VPattern -> Bool
<= :: VPattern -> VPattern -> Bool
$c<= :: VPattern -> VPattern -> Bool
< :: VPattern -> VPattern -> Bool
$c< :: VPattern -> VPattern -> Bool
compare :: VPattern -> VPattern -> Ordering
$ccompare :: VPattern -> VPattern -> Ordering
$cp1Ord :: Eq VPattern
Ord, ReadPrec [VPattern]
ReadPrec VPattern
Int -> ReadS VPattern
ReadS [VPattern]
(Int -> ReadS VPattern)
-> ReadS [VPattern]
-> ReadPrec VPattern
-> ReadPrec [VPattern]
-> Read VPattern
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [VPattern]
$creadListPrec :: ReadPrec [VPattern]
readPrec :: ReadPrec VPattern
$creadPrec :: ReadPrec VPattern
readList :: ReadS [VPattern]
$creadList :: ReadS [VPattern]
readsPrec :: Int -> ReadS VPattern
$creadsPrec :: Int -> ReadS VPattern
Read)

v2tPattern :: VPattern -> Maybe TPattern
v2tPattern :: VPattern -> Maybe TPattern
v2tPattern (VPType TPattern
t) = TPattern -> Maybe TPattern
forall a. a -> Maybe a
Just TPattern
t
v2tPattern (VPMetaVar MetaVar
var) = TPattern -> Maybe TPattern
forall a. a -> Maybe a
Just (TPattern -> Maybe TPattern) -> TPattern -> Maybe TPattern
forall a b. (a -> b) -> a -> b
$ MetaVar -> TPattern
TPVar MetaVar
var
v2tPattern (VPSeqVar MetaVar
var SeqSortOp
op) = TPattern -> Maybe TPattern
forall a. a -> Maybe a
Just (TPattern -> Maybe TPattern) -> TPattern -> Maybe TPattern
forall a b. (a -> b) -> a -> b
$ MetaVar -> SeqSortOp -> TPattern
TPSeqVar MetaVar
var SeqSortOp
op
v2tPattern (PADT Name
cons [VPattern]
pats) = Name -> [TPattern] -> TPattern
TPADT Name
cons ([TPattern] -> TPattern) -> Maybe [TPattern] -> Maybe TPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VPattern -> Maybe TPattern) -> [VPattern] -> Maybe [TPattern]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VPattern -> Maybe TPattern
v2tPattern [VPattern]
pats
v2tPattern (VPLit Values
lit) = TPattern -> Maybe TPattern
forall a. a -> Maybe a
Just (TPattern -> Maybe TPattern) -> TPattern -> Maybe TPattern
forall a b. (a -> b) -> a -> b
$ FTerm -> TPattern
TPLit (Funcons -> FTerm
TFuncon (Values -> Funcons
FValue Values
lit))
v2tPattern VPattern
VPWildCard = TPattern -> Maybe TPattern
forall a. a -> Maybe a
Just TPattern
TPWildCard
--v2tPattern (PList _) = Nothing  
v2tPattern (VPAnnotated VPattern
fp FTerm
t) = Maybe TPattern
forall a. Maybe a
Nothing 

-- required for "matching" lazy arguments (fields) of adt constructors
v2fPattern :: VPattern -> FPattern
v2fPattern :: VPattern -> FPattern
v2fPattern (VPMetaVar MetaVar
x)          = MetaVar -> FPattern
PMetaVar MetaVar
x
v2fPattern (VPSeqVar MetaVar
x SeqSortOp
op)        = MetaVar -> SeqSortOp -> FPattern
PSeqVar MetaVar
x SeqSortOp
op
v2fPattern (VPAnnotated VPattern
pat FTerm
ann)  = FPattern -> FTerm -> FPattern
PAnnotated (VPattern -> FPattern
v2fPattern VPattern
pat) FTerm
ann
v2fPattern VPattern
VPWildCard             = FPattern
PWildCard
v2fPattern VPattern
vp                     = VPattern -> FPattern
PValue VPattern
vp

substitute_patt_signal :: VPattern -> Env -> Rewrite VPattern
substitute_patt_signal :: VPattern -> Env -> Rewrite VPattern
substitute_patt_signal VPattern
vpat Env
env = case VPattern
vpat of 
  PADT Name
name [VPattern]
vpats -> Name -> [VPattern] -> VPattern
PADT Name
name ([VPattern] -> VPattern) -> Rewrite [VPattern] -> Rewrite VPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [VPattern] -> Env -> Rewrite [VPattern]
subs_flatten [VPattern]
vpats Env
env
  VPattern
VPWildCard      -> VPattern -> Rewrite VPattern
forall (m :: * -> *) a. Monad m => a -> m a
return VPattern
VPWildCard
--  PList pats      -> PList <$> subs_flatten pats env
  VPMetaVar MetaVar
var   -> case MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
var Env
env of
                      Maybe Levelled
Nothing -> VPattern -> Rewrite VPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVar -> VPattern
VPMetaVar MetaVar
var)
                      Just Levelled
v  -> Values -> VPattern
VPLit (Values -> VPattern) -> Rewrite Values -> Rewrite VPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Levelled -> Rewrite Values
vLevel Levelled
v
  VPAnnotated VPattern
vpat FTerm
ann  -> VPattern -> FTerm -> VPattern
VPAnnotated (VPattern -> FTerm -> VPattern)
-> Rewrite VPattern -> Rewrite (FTerm -> VPattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VPattern -> Env -> Rewrite VPattern
substitute_patt_signal VPattern
vpat Env
env 
                                       Rewrite (FTerm -> VPattern) -> Rewrite FTerm -> Rewrite VPattern
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FTerm -> Rewrite FTerm
forall (m :: * -> *) a. Monad m => a -> m a
return FTerm
ann 
  VPSeqVar MetaVar
var SeqSortOp
op -> case MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
var Env
env of
                      Maybe Levelled
Nothing -> VPattern -> Rewrite VPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
var SeqSortOp
op)
                      Just Levelled
v  -> Values -> VPattern
VPLit (Values -> VPattern) -> Rewrite Values -> Rewrite VPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Levelled -> Rewrite Values
vLevel Levelled
v 
  VPLit Values
lit       -> VPattern -> Rewrite VPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (VPattern -> Rewrite VPattern) -> VPattern -> Rewrite VPattern
forall a b. (a -> b) -> a -> b
$ Values -> VPattern
VPLit Values
lit
  VPType TPattern
tpat     -> VPattern -> Rewrite VPattern
forall (m :: * -> *) a. Monad m => a -> m a
return (VPattern -> Rewrite VPattern) -> VPattern -> Rewrite VPattern
forall a b. (a -> b) -> a -> b
$ TPattern -> VPattern
VPType TPattern
tpat -- assumes type patterns do not occur in signals
  where subs_flatten :: [VPattern] -> Env -> Rewrite [VPattern]
        subs_flatten :: [VPattern] -> Env -> Rewrite [VPattern]
subs_flatten [VPattern]
terms Env
env = ([[VPattern]] -> [VPattern]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[VPattern]] -> [VPattern])
-> Rewrite [[VPattern]] -> Rewrite [VPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Rewrite [[VPattern]] -> Rewrite [VPattern])
-> Rewrite [[VPattern]] -> Rewrite [VPattern]
forall a b. (a -> b) -> a -> b
$ [VPattern]
-> (VPattern -> Rewrite [VPattern]) -> Rewrite [[VPattern]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VPattern]
terms ((VPattern -> Rewrite [VPattern]) -> Rewrite [[VPattern]])
-> (VPattern -> Rewrite [VPattern]) -> Rewrite [[VPattern]]
forall a b. (a -> b) -> a -> b
$ \case
              vpat :: VPattern
vpat@(VPMetaVar MetaVar
k)   -> Env -> MetaVar -> VPattern -> Rewrite [VPattern]
envMaybeLookup Env
env MetaVar
k VPattern
vpat
              vpat :: VPattern
vpat@(VPSeqVar MetaVar
k SeqSortOp
op) -> Env -> MetaVar -> VPattern -> Rewrite [VPattern]
envMaybeLookup Env
env MetaVar
k VPattern
vpat
              VPattern
vpat                 -> (VPattern -> [VPattern] -> [VPattern]
forall a. a -> [a] -> [a]
:[]) (VPattern -> [VPattern]) -> Rewrite VPattern -> Rewrite [VPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VPattern -> Env -> Rewrite VPattern
substitute_patt_signal VPattern
vpat Env
env

        envMaybeLookup :: Env -> MetaVar -> VPattern -> Rewrite [VPattern] 
        envMaybeLookup :: Env -> MetaVar -> VPattern -> Rewrite [VPattern]
envMaybeLookup Env
env MetaVar
k VPattern
vpat = case MetaVar -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup MetaVar
k Env
env of
                            Maybe Levelled
Nothing -> [VPattern] -> Rewrite [VPattern]
forall (m :: * -> *) a. Monad m => a -> m a
return [VPattern
vpat]
                            Just Levelled
lf -> (Values -> VPattern) -> [Values] -> [VPattern]
forall a b. (a -> b) -> [a] -> [b]
map Values -> VPattern
VPLit ([Values] -> [VPattern]) -> Rewrite [Values] -> Rewrite [VPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Levelled -> Rewrite [Values]
vsLevel Levelled
lf


-- | Variant of 'vsMatch' that is lifted into the 'MSOS' monad.
lifted_vsMatch :: [Values] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values]
str [VPattern]
pats Env
env = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
str [VPattern]
pats Env
env
-- | Matching values with value patterns patterns.
-- If the list of patterns is a singleton list, then 'vsMatch' attempts
-- to match the values as a tuple against the pattern as well.
vsMatch :: [Values] -> [VPattern] -> Env -> Rewrite Env 
vsMatch :: [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
str [VPattern]
pats Env
env = [Values] -> [VPattern] -> Env -> Rewrite Env
strict_vsMatch [Values]
str [VPattern]
pats Env
env
{-case pats of
    [pat]   -> do
        e_ie_env <- eval_catch (strict_vsMatch str [pat] env)
        case e_ie_env of
            Right env' -> return env'
            Left ie | failsRule ie -> vMatch (safe_tuple_val str) pat env
                    | otherwise -> rewrite_rethrow ie
    _       -> strict_vsMatch str pats env
-}

-- | Match stricly values with patterns.
strict_vsMatch :: [Values] -> [VPattern] -> Env -> Rewrite Env
strict_vsMatch :: [Values] -> [VPattern] -> Env -> Rewrite Env
strict_vsMatch [Values]
str [VPattern]
pats Env
env 
  | (Values -> Bool) -> [Values] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Values -> Bool
forall t. Values t -> Bool
isSort_ [Values]
str 
  , Just [TPattern]
tpats <- [Maybe TPattern] -> Maybe [TPattern]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((VPattern -> Maybe TPattern) -> [VPattern] -> [Maybe TPattern]
forall a b. (a -> b) -> [a] -> [b]
map VPattern -> Maybe TPattern
v2tPattern [VPattern]
pats)
        = [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
tsMatch ((Values -> ComputationTypes) -> [Values] -> [ComputationTypes]
forall a b. (a -> b) -> [a] -> [b]
map (Funcons -> ComputationTypes
downcastSort (Funcons -> ComputationTypes)
-> (Values -> Funcons) -> Values -> ComputationTypes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values -> Funcons
FValue) [Values]
str) [TPattern]
tpats Env
env 
  | Bool
otherwise = (Values -> MetaVar)
-> [Values] -> [Matcher Values] -> Env -> Rewrite Env
forall a.
(a -> MetaVar) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching Values -> MetaVar
showValues [Values]
str [Matcher Values]
matchers Env
env
        where   matchers :: [Matcher Values]
matchers = (VPattern -> Matcher Values) -> [VPattern] -> [Matcher Values]
forall a b. (a -> b) -> [a] -> [b]
map VPattern -> Matcher Values
toMatcher [VPattern]
pats
                toMatcher :: VPattern -> Matcher Values
toMatcher VPattern
pat = case VPattern -> Maybe SeqVarInfo
vpSeqVarInfo VPattern
pat of
                    Just SeqVarInfo
info   -> (Values -> Maybe FTerm -> Env -> Rewrite (Maybe [Values]))
-> ([Values] -> Levelled) -> SeqVarInfo -> Matcher Values
forall a.
(a -> Maybe FTerm -> Env -> Rewrite (Maybe [a]))
-> ([a] -> Levelled) -> SeqVarInfo -> Matcher a
seqMatcher Values -> Maybe FTerm -> Env -> Rewrite (Maybe [Values])
isInMaybeTermTypePreserve [Values] -> Levelled
ValuesTerm SeqVarInfo
info
                    Maybe SeqVarInfo
Nothing     -> (Values -> VPattern -> Env -> Rewrite Env)
-> VPattern -> Matcher Values
forall a b. (a -> b -> Env -> Rewrite Env) -> b -> Matcher a
singleMatcher Values -> VPattern -> Env -> Rewrite Env
vMatch VPattern
pat 

-- | Variant of 'premiseStep' that applies substitute and pattern-matching.
premise :: FTerm -> [FPattern] -> Env -> MSOS Env
premise :: FTerm -> [FPattern] -> Env -> MSOS Env
premise FTerm
x [FPattern]
pats Env
env = Rewrite (Rewritten, Env) -> MSOS (Rewritten, Env)
forall a. Rewrite a -> MSOS a
liftRewrite (FTerm -> Env -> Rewrite (Rewritten, Env)
subsAndRewritesInEnv FTerm
x Env
env) MSOS (Rewritten, Env) -> ((Rewritten, Env) -> MSOS Env) -> MSOS Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  (ValTerm [Values]
v, Env
env')       -> IE -> MSOS Env
forall b. IE -> MSOS b
msos_throw ([Values] -> IE
StepOnValue [Values]
v)
  (CompTerm Funcons
f MSOS StepRes
step,Env
env')  -> do 
      StepRes
ef' <- MSOS ()
count_delegation MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes -> MSOS StepRes
optRefocus MSOS StepRes
step 
      case StepRes
ef' of Left Funcons
f'   -> Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons
f'] [FPattern]
pats Env
env'
                  Right [Values]
vs' -> Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs') [FPattern]
pats Env
env'

-- | Variant of 'fsMatch' that is lifted into the 'MSOS' monad.
-- If all given terms are values, then 'vsMatch' is used instead.
lifted_fsMatch :: [Funcons] -> [FPattern] -> Env -> MSOS Env
lifted_fsMatch [Funcons]
str [FPattern]
pats Env
env = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
str [FPattern]
pats Env
env
-- | Match a sequence of terms to a sequence of patterns.
fsMatch :: [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch = Bool -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatchStrictness Bool
False
strict_fsMatch :: [Funcons] -> [FPattern] -> Env -> Rewrite Env
strict_fsMatch = Bool -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatchStrictness Bool
True
fsMatchStrictness :: Bool -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatchStrictness :: Bool -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatchStrictness Bool
strict [Funcons]
str [FPattern]
pats Env
env 
    -- if all the given funcons are values, then perform value matching instead.
    | Bool -> Bool
not Bool
strict Bool -> Bool -> Bool
&& (Funcons -> Bool) -> [Funcons] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not(Bool -> Bool) -> (Funcons -> Bool) -> Funcons -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Funcons -> Bool
hasStep) [Funcons]
str = 
          let downValues :: [Funcons] -> [Values]
downValues [Funcons]
vs = (Funcons -> Values) -> [Funcons] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
downcastValue [Funcons]
vs
          in [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch ([Funcons] -> [Values]
downValues [Funcons]
str) ((FPattern -> VPattern) -> [FPattern] -> [VPattern]
forall a b. (a -> b) -> [a] -> [b]
map FPattern -> VPattern
f2vPattern [FPattern]
pats) Env
env
    | Bool
otherwise = (Funcons -> MetaVar)
-> [Funcons] -> [Matcher Funcons] -> Env -> Rewrite Env
forall a.
(a -> MetaVar) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching Funcons -> MetaVar
showFuncons [Funcons]
str [Matcher Funcons]
matchers Env
env
    where   matchers :: [Matcher Funcons]
matchers = (FPattern -> Matcher Funcons) -> [FPattern] -> [Matcher Funcons]
forall a b. (a -> b) -> [a] -> [b]
map FPattern -> Matcher Funcons
toMatcher [FPattern]
pats
            toMatcher :: FPattern -> Matcher Funcons
toMatcher FPattern
pat = case FPattern -> Maybe SeqVarInfo
fpSeqVarInfo FPattern
pat of
                Just SeqVarInfo
info   -> (Funcons -> Maybe FTerm -> Env -> Rewrite (Maybe [Funcons]))
-> ([Funcons] -> Levelled) -> SeqVarInfo -> Matcher Funcons
forall a.
(a -> Maybe FTerm -> Env -> Rewrite (Maybe [a]))
-> ([a] -> Levelled) -> SeqVarInfo -> Matcher a
seqMatcher Funcons -> Maybe FTerm -> Env -> Rewrite (Maybe [Funcons])
rewritesToAnnotatedType [Funcons] -> Levelled
FunconsTerm SeqVarInfo
info
                Maybe SeqVarInfo
Nothing     -> (Funcons -> FPattern -> Env -> Rewrite Env)
-> FPattern -> Matcher Funcons
forall a b. (a -> b -> Env -> Rewrite Env) -> b -> Matcher a
singleMatcher Funcons -> FPattern -> Env -> Rewrite Env
fMatch FPattern
pat

fMatch :: Funcons -> FPattern -> Env -> Rewrite Env 
fMatch :: Funcons -> FPattern -> Env -> Rewrite Env
fMatch Funcons
_ FPattern
PWildCard Env
env = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
fMatch Funcons
f (PMetaVar MetaVar
var) Env
env = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var (Funcons -> Maybe (MSOS StepRes) -> Levelled
FunconTerm Funcons
f Maybe (MSOS StepRes)
forall a. Maybe a
Nothing) Env
env)
fMatch Funcons
f (PAnnotated FPattern
pat FTerm
term) Env
env = do
    [Values]
tys <- FTerm -> Env -> Rewrite [Values]
subsAndRewritesToValues FTerm
term Env
env
    let fail :: Rewrite a
fail = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch (MetaVar
"pattern annotation check failed: " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ [Values] -> MetaVar
showValuesSeq [Values]
tys))
    Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten -> (Rewritten -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case  
        ValTerm [Values]
vs  -> do   Bool
b <- [Values] -> [Values] -> Rewrite Bool
isInTuple [Values]
vs [Values]
tys 
                            if Bool
b then [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
vs [FPattern -> VPattern
f2vPattern FPattern
pat] Env
env
                                 else Rewrite Env
forall a. Rewrite a
fail
        Rewritten
otherwise   -> Rewrite Env
forall a. Rewrite a
fail 
-- * a sequence variable can match the singleton sequence 
fMatch Funcons
f pat :: FPattern
pat@(PSeqVar MetaVar
_ SeqSortOp
_) Env
env = [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons
f] [FPattern
pat] Env
env
-- if the pattern is a value attempt evaluation by rewrite
fMatch Funcons
f (PValue VPattern
pat) Env
env = Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten -> (Rewritten -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
    \case   ValTerm [Values]
vs -> [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
vs [VPattern
pat] Env
env
            CompTerm Funcons
_ MSOS StepRes
_ -> IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw --important, should remain last 
                (MetaVar -> IE
PatternMismatch (MetaVar
"could not rewrite to value: " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ Funcons -> MetaVar
showFuncons Funcons
f))

lifted_fMaybeMatch :: Maybe Funcons -> Maybe FPattern -> Env -> MSOS Env
lifted_fMaybeMatch Maybe Funcons
mf Maybe FPattern
mp Env
env = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ Maybe Funcons -> Maybe FPattern -> Env -> Rewrite Env
fMaybeMatch Maybe Funcons
mf Maybe FPattern
mp Env
env
fMaybeMatch :: Maybe Funcons -> Maybe FPattern -> Env -> Rewrite Env
fMaybeMatch Maybe Funcons
Nothing Maybe FPattern
Nothing Env
env = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
fMaybeMatch (Just Funcons
f) (Just FPattern
p) Env
env = Funcons -> FPattern -> Env -> Rewrite Env
fMatch Funcons
f FPattern
p Env
env
fMaybeMatch Maybe Funcons
_ Maybe FPattern
_ Env
env = IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch MetaVar
"fMaybeMatch")

lifted_vMaybeMatch :: Maybe Values -> Maybe VPattern -> Env -> MSOS Env
lifted_vMaybeMatch Maybe Values
mv Maybe VPattern
mp Env
env = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ Maybe Values -> Maybe VPattern -> Env -> Rewrite Env
vMaybeMatch Maybe Values
mv Maybe VPattern
mp Env
env
vMaybeMatch :: Maybe Values -> Maybe VPattern -> Env -> Rewrite Env
vMaybeMatch :: Maybe Values -> Maybe VPattern -> Env -> Rewrite Env
vMaybeMatch Maybe Values
Nothing Maybe VPattern
Nothing Env
env = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMaybeMatch (Just Values
v) (Just VPattern
p) Env
env = Values -> VPattern -> Env -> Rewrite Env
vMatch Values
v VPattern
p Env
env
vMaybeMatch Maybe Values
_ Maybe VPattern
_ Env
env = IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch (MetaVar
"vMaybeMatch")) 

lifted_vMatch :: Values -> VPattern -> Env -> MSOS Env
lifted_vMatch Values
v VPattern
p Env
env = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ Values -> VPattern -> Env -> Rewrite Env
vMatch Values
v VPattern
p Env
env
vMatch :: Values -> VPattern -> Env -> Rewrite Env
-- builtin special case for builtin value constructor `datatype-value`
vMatch :: Values -> VPattern -> Env -> Rewrite Env
vMatch (ADTVal Name
str [Funcons]
vs) (PADT Name
"datatype-value" [VPattern]
pats) Env
env = 
  Name -> Name -> [Funcons] -> [VPattern] -> Env -> Rewrite Env
adtMatch Name
"" Name
"" (MetaVar -> Funcons
string_ (Name -> MetaVar
unpack Name
str)Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:[Funcons]
vs) [VPattern]
pats Env
env
vMatch Values
_ (VPattern
VPWildCard) Env
env = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch Values
VAny VPattern
_ Env
env = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch Values
v (VPMetaVar MetaVar
var) Env
env = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
var (Values -> Levelled
ValueTerm Values
v) Env
env)
vMatch (ADTVal Name
str [Funcons]
vs) (PADT Name
con [VPattern]
pats) Env
env = Name -> Name -> [Funcons] -> [VPattern] -> Env -> Rewrite Env
adtMatch Name
str Name
con [Funcons]
vs [VPattern]
pats Env
env
-- strict because we do not want to match the sequence "inside" the list
--vMatch (List vs) (PList ps) env = strict_vsMatch vs ps env 
vMatch Values
v (VPAnnotated VPattern
pat FTerm
term) Env
env = do
    Values
ty <- FTerm -> Env -> Rewrite Values
subsAndRewritesToValue FTerm
term Env
env
    Values -> Values -> Rewrite Bool
isIn Values
v Values
ty Rewrite Bool -> (Bool -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True  -> Values -> VPattern -> Env -> Rewrite Env
vMatch Values
v VPattern
pat Env
env
        Bool
False -> IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch (MetaVar
"pattern annotation check failed: " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ Values -> MetaVar
showValues Values
ty))
vMatch Values
v (VPLit Values
v2) Env
env | Values
v Values -> Values -> Bool
forall a. Eq a => a -> a -> Bool
== Values
v2 = Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
-- special treatment for sequence variables:
-- * a (single) sequence variable can match a tuple
-- * a sequence variable can match the singleton sequence
vMatch Values
v pat :: VPattern
pat@(VPSeqVar MetaVar
_ SeqSortOp
_) Env
env = [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values
v] [VPattern
pat] Env
env
-- * a single value can match a tuple of patterns if it contains sequences
vMatch (ComputationType ComputationTypes
ty) (VPType TPattern
pat) Env
env = ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch ComputationTypes
ty TPattern
pat Env
env
vMatch Values
v VPattern
_ Env
_ = IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch (MetaVar
"failed to match"))

tsMatch :: [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
tsMatch :: [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
tsMatch = [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
strict_tsMatch

strict_tsMatch :: [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
strict_tsMatch :: [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
strict_tsMatch [ComputationTypes]
str [TPattern]
pats Env
env = (ComputationTypes -> MetaVar)
-> [ComputationTypes]
-> [Matcher ComputationTypes]
-> Env
-> Rewrite Env
forall a.
(a -> MetaVar) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching ComputationTypes -> MetaVar
showSorts [ComputationTypes]
str [Matcher ComputationTypes]
matchers Env
env
        where   matchers :: [Matcher ComputationTypes]
matchers = (TPattern -> Matcher ComputationTypes)
-> [TPattern] -> [Matcher ComputationTypes]
forall a b. (a -> b) -> [a] -> [b]
map TPattern -> Matcher ComputationTypes
toMatcher [TPattern]
pats
                toMatcher :: TPattern -> Matcher ComputationTypes
toMatcher TPattern
pat = case TPattern -> Maybe SeqVarInfo
tpSeqVarInfo TPattern
pat of
                  Maybe SeqVarInfo
Nothing -> (ComputationTypes -> TPattern -> Env -> Rewrite Env)
-> TPattern -> Matcher ComputationTypes
forall a b. (a -> b -> Env -> Rewrite Env) -> b -> Matcher a
singleMatcher ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch TPattern
pat 
                  Just SeqVarInfo
info -> (ComputationTypes
 -> Maybe FTerm -> Env -> Rewrite (Maybe [ComputationTypes]))
-> ([ComputationTypes] -> Levelled)
-> SeqVarInfo
-> Matcher ComputationTypes
forall a.
(a -> Maybe FTerm -> Env -> Rewrite (Maybe [a]))
-> ([a] -> Levelled) -> SeqVarInfo -> Matcher a
seqMatcher ComputationTypes
-> Maybe FTerm -> Env -> Rewrite (Maybe [ComputationTypes])
isInMaybeTypeTypePreserve [ComputationTypes] -> Levelled
TypesTerm SeqVarInfo
info

tMatch :: ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch :: ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch ComputationTypes
t TPattern
p Env
env = case TPattern
p of
  TPattern
TPWildCard -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
  TPVar MetaVar
x -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
x (ComputationTypes -> Levelled
TypeTerm ComputationTypes
t) Env
env)
  TPSeqVar MetaVar
_ SeqSortOp
_ -> [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
tsMatch [ComputationTypes
t] [TPattern
p] Env
env
  TPLit FTerm
ft -> FTerm -> Env -> Rewrite Values
subsAndRewritesToValue FTerm
ft Env
env Rewrite Values -> (Values -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    ComputationType ComputationTypes
ty ->   
      if ComputationTypes
t ComputationTypes -> ComputationTypes -> Bool
forall a. Eq a => a -> a -> Bool
== ComputationTypes
ty then Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env 
                 else IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch (MetaVar
"failed to match"))
    Values
_ -> MetaVar -> Rewrite Env
forall a. MetaVar -> Rewrite a
internal MetaVar
"type-pattern literal not a type"
  TPComputes TPattern
fp | ComputesType Types Funcons
ft <- ComputationTypes
t -> ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch (Types Funcons -> ComputationTypes
forall t. Types t -> ComputationTypes t
Type Types Funcons
ft) TPattern
fp Env
env
  TPComputesFrom TPattern
fp TPattern
tp | ComputesFromType Types Funcons
ft Types Funcons
tt <- ComputationTypes
t -> 
    ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch (Types Funcons -> ComputationTypes
forall t. Types t -> ComputationTypes t
Type Types Funcons
ft) TPattern
fp Env
env Rewrite Env -> (Env -> Rewrite Env) -> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch (Types Funcons -> ComputationTypes
forall t. Types t -> ComputationTypes t
Type Types Funcons
tt) TPattern
tp 
  TPADT Name
nm [TPattern]
ps | Type (ADT Name
nm' [Funcons]
ts) <- ComputationTypes
t,  Name
nm Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
nm' ->
    [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
ts ((TPattern -> FPattern) -> [TPattern] -> [FPattern]
forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue (VPattern -> FPattern)
-> (TPattern -> VPattern) -> TPattern -> FPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPattern -> VPattern
VPType) [TPattern]
ps) Env
env -- TODO change ps to value pattern (also in generator, see other TODO)
  TPattern
_ -> IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch (MetaVar
"failed to match"))

adtMatch :: Name -> Name -> [Funcons] -> [VPattern] -> Env -> Rewrite Env
adtMatch :: Name -> Name -> [Funcons] -> [VPattern] -> Env -> Rewrite Env
adtMatch Name
con Name
pat_con [Funcons]
vs [VPattern]
vpats Env
env 
    | Name
con Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
pat_con = IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
PatternMismatch (MetaVar
"failed to match constructors: (" MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ (Name, Name) -> MetaVar
forall a. Show a => a -> MetaVar
show (Name
con,Name
pat_con) MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ MetaVar
")"))
    | Bool
otherwise = [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
vs ((VPattern -> FPattern) -> [VPattern] -> [FPattern]
forall a b. (a -> b) -> [a] -> [b]
map VPattern -> FPattern
v2fPattern [VPattern]
vpats) Env
env


fpSeqVarInfo :: FPattern -> Maybe SeqVarInfo
fpSeqVarInfo :: FPattern -> Maybe SeqVarInfo
fpSeqVarInfo (PSeqVar MetaVar
var SeqSortOp
op) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just (MetaVar
var, SeqSortOp
op, Maybe FTerm
forall a. Maybe a
Nothing)
fpSeqVarInfo (PAnnotated (PSeqVar MetaVar
var SeqSortOp
op) FTerm
term) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just (MetaVar
var, SeqSortOp
op, FTerm -> Maybe FTerm
forall a. a -> Maybe a
Just FTerm
term)
fpSeqVarInfo FPattern
_ = Maybe SeqVarInfo
forall a. Maybe a
Nothing

vpSeqVarInfo :: VPattern -> Maybe SeqVarInfo 
vpSeqVarInfo :: VPattern -> Maybe SeqVarInfo
vpSeqVarInfo (VPSeqVar MetaVar
var SeqSortOp
op) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just (MetaVar
var, SeqSortOp
op, Maybe FTerm
forall a. Maybe a
Nothing)
vpSeqVarInfo (VPAnnotated (VPSeqVar MetaVar
var SeqSortOp
op) FTerm
term) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just (MetaVar
var, SeqSortOp
op, FTerm -> Maybe FTerm
forall a. a -> Maybe a
Just FTerm
term)
vpSeqVarInfo VPattern
_ = Maybe SeqVarInfo
forall a. Maybe a
Nothing

tpSeqVarInfo :: TPattern -> Maybe SeqVarInfo
tpSeqVarInfo :: TPattern -> Maybe SeqVarInfo
tpSeqVarInfo (TPSeqVar MetaVar
var SeqSortOp
op) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just (MetaVar
var, SeqSortOp
op, Maybe FTerm
forall a. Maybe a
Nothing)
tpSeqVarInfo TPattern
_ = Maybe SeqVarInfo
forall a. Maybe a
Nothing

-- | CSB supports five kinds of side conditions.
-- Each of the side conditions are explained below.
-- When a side condition is not accepted an exception is thrown that 
-- is caught by the backtrackign procedure 'evalRules'.
-- A value is a /ground value/ if it is not a thunk (and not composed out of
--  thunks).
data SideCondition  
    -- | /T1 == T2/. Accepted only when /T1/ and /T2/ rewrite to /equal/ ground values.
    = SCEquality FTerm FTerm 
    -- | /T1 =\/= T2/. Accepted only when /T1/ and /T2/ rewrite to /unequal/ ground values.
    | SCInequality FTerm FTerm 
    -- | /T1 : T2/. Accepted only when /T2/ rewrites to a type and /T1/ rewrites to a value of that type.
    | SCIsInSort FTerm FTerm
    -- | /~(T1 : T2)/. Accepted only when /T2/ rewrites to a type and /T1/ rewrites to a value /not/ of that type.
    | SCNotInSort FTerm FTerm
    -- | /T = P/. Accepted only when /T/ rewrites to a value that matches the pattern /P/. (May produce new bindings in 'Env').
    | SCPatternMatch FTerm [VPattern]

-- | Variant of 'sideCondition' that is lifted into the 'MSOS' monad.
lifted_sideCondition :: SideCondition -> Env -> MSOS Env
lifted_sideCondition SideCondition
sc Env
env = Rewrite Env -> MSOS Env
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite Env -> MSOS Env) -> Rewrite Env -> MSOS Env
forall a b. (a -> b) -> a -> b
$ SideCondition -> Env -> Rewrite Env
sideCondition SideCondition
sc Env
env

-- | Executes a side condition, given an 'Env' environment, throwing possible exceptions, and 
-- possibly extending the environment.
sideCondition :: SideCondition -> Env -> Rewrite Env
sideCondition :: SideCondition -> Env -> Rewrite Env
sideCondition SideCondition
cs Env
env = case SideCondition
cs of
    SCEquality FTerm
term1 FTerm
term2 -> 
        MetaVar
-> ([Values] -> [Values] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop MetaVar
"equality condition" (([Values] -> [Values] -> Bool)
-> [Values] -> [Values] -> Rewrite Bool
forall (m :: * -> *) t t a.
Monad m =>
(t -> t -> a) -> t -> t -> m a
lift [Values] -> [Values] -> Bool
allEqual) FTerm
term1 FTerm
term2 Env
env
    SCInequality FTerm
term1 FTerm
term2 ->     
        MetaVar
-> ([Values] -> [Values] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop MetaVar
"inequality condition" (([Values] -> [Values] -> Bool)
-> [Values] -> [Values] -> Rewrite Bool
forall (m :: * -> *) t t a.
Monad m =>
(t -> t -> a) -> t -> t -> m a
lift [Values] -> [Values] -> Bool
allUnEqual) FTerm
term1 FTerm
term2 Env
env
    SCIsInSort FTerm
term1 FTerm
term2 -> MetaVar
-> ([Values] -> [Values] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop MetaVar
"sort annotation" [Values] -> [Values] -> Rewrite Bool
isInTuple FTerm
term1 FTerm
term2 Env
env
    SCNotInSort FTerm
term1 FTerm
term2 -> 
        MetaVar
-> ([Values] -> [Values] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop MetaVar
"neg. sort annotation" (\[Values]
a [Values]
b -> [Values] -> [Values] -> Rewrite Bool
isInTuple [Values]
a [Values]
b Rewrite Bool -> (Bool -> Rewrite Bool) -> Rewrite Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Rewrite Bool) -> (Bool -> Bool) -> Bool -> Rewrite Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) FTerm
term1 FTerm
term2 Env
env
    SCPatternMatch FTerm
term [VPattern]
vpats -> 
      Rewrite (Rewritten, Env)
-> Rewrite (Either IException (Rewritten, Env))
forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch (FTerm -> Env -> Rewrite (Rewritten, Env)
subsAndRewritesInEnv FTerm
term Env
env) Rewrite (Either IException (Rewritten, Env))
-> (Either IException (Rewritten, Env) -> Rewrite Env)
-> Rewrite Env
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
            -- env' binds term to step or value, if possible 
            --  courtesy of subsAndRewritesInEnv
            Right (ValTerm [Values]
vs, Env
env')        -> [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
vs [VPattern]
vpats Env
env'
            Right (CompTerm Funcons
lf MSOS StepRes
step, Env
env')  -> case [VPattern]
vpats of 
              [VPMetaVar MetaVar
v] -> Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return (MetaVar -> Levelled -> Env -> Env
envInsert MetaVar
v (Funcons -> Maybe (MSOS StepRes) -> Levelled
FunconTerm Funcons
lf (MSOS StepRes -> Maybe (MSOS StepRes)
forall a. a -> Maybe a
Just MSOS StepRes
step)) Env
env')
              [VPattern]
_             -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons
lf] [FPattern]
pats Env
env'
            Left (Funcons
_,Funcons
lf,PartialOp MetaVar
_)     -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons
lf] [FPattern]
pats Env
env
            Left IException
ie                     -> IException -> Rewrite Env
forall a. IException -> Rewrite a
rewrite_rethrow IException
ie
      where pats :: [FPattern]
pats = (VPattern -> FPattern) -> [VPattern] -> [FPattern]
forall a b. (a -> b) -> [a] -> [b]
map VPattern -> FPattern
toFPat [VPattern]
vpats
              where toFPat :: VPattern -> FPattern
toFPat VPattern
vpat = case VPattern
vpat of
                      VPMetaVar MetaVar
var   -> MetaVar -> FPattern
PMetaVar MetaVar
var 
                      VPattern
value_pat       -> VPattern -> FPattern
PValue VPattern
value_pat
  where prop :: String -> ([Values] -> [Values] -> Rewrite Bool) -> FTerm -> FTerm -> Env -> Rewrite Env
        prop :: MetaVar
-> ([Values] -> [Values] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop MetaVar
msg [Values] -> [Values] -> Rewrite Bool
op FTerm
term1 FTerm
term2 Env
env = do
            ([Values]
vs1,Env
env1) <- FTerm -> Env -> Rewrite ([Values], Env)
subsAndRewritesToValuesInEnv FTerm
term1 Env
env
            ([Values]
vs2,Env
env2) <- FTerm -> Env -> Rewrite ([Values], Env)
subsAndRewritesToValuesInEnv FTerm
term2 Env
env1
            Bool
b <- [Values] -> [Values] -> Rewrite Bool
op [Values]
vs1 [Values]
vs2
            if Bool
b then Env -> Rewrite Env
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env2
                 else IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw (MetaVar -> IE
SideCondFail (MetaVar
msg MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ MetaVar
" fails with " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ [Values] -> MetaVar
showValuesSeq [Values]
vs1 MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ MetaVar
" and " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ [Values] -> MetaVar
showValuesSeq [Values]
vs2))
        lift :: (t -> t -> a) -> t -> t -> m a
lift t -> t -> a
op t
xs t
ys = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (t -> t -> a
op t
xs t
ys)
      
-- piggy back on 
matchTypeParams :: [ComputationTypes] -> [TypeParam] -> Rewrite Env
matchTypeParams :: [ComputationTypes] -> [TypeParam] -> Rewrite Env
matchTypeParams [ComputationTypes]
tys [TypeParam]
tparams = 
    let param_pats :: [VPattern]
param_pats = (TypeParam -> VPattern) -> [TypeParam] -> [VPattern]
forall a b. (a -> b) -> [a] -> [b]
map TypeParam -> VPattern
mkPattern [TypeParam]
tparams
         where mkPattern :: TypeParam -> VPattern
mkPattern (Maybe MetaVar
Nothing, Maybe SeqSortOp
_, FTerm
kind)  = VPattern -> FTerm -> VPattern
VPAnnotated VPattern
VPWildCard FTerm
kind
               mkPattern (Just MetaVar
var, Maybe SeqSortOp
Nothing, FTerm
kind) = VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> VPattern
VPMetaVar MetaVar
var) FTerm
kind
               mkPattern (Just MetaVar
var, Just SeqSortOp
op, FTerm
kind) = VPattern -> FTerm -> VPattern
VPAnnotated (MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
var SeqSortOp
op) FTerm
kind
    in [Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch ((ComputationTypes -> Values) -> [ComputationTypes] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map ComputationTypes -> Values
forall t. ComputationTypes t -> Values t
ComputationType [ComputationTypes]
tys) [VPattern]
param_pats Env
forall k a. Map k a
emptyEnv 


alwaysAccept :: Funcons -> Maybe FTerm -> Env -> Rewrite Bool
alwaysAccept :: Funcons -> Maybe FTerm -> Env -> Rewrite Bool
alwaysAccept Funcons
_ Maybe FTerm
_ Env
_ = Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

rewritesToAnnotatedType :: Funcons -> Maybe FTerm -> Env -> Rewrite (Maybe [Funcons])
rewritesToAnnotatedType :: Funcons -> Maybe FTerm -> Env -> Rewrite (Maybe [Funcons])
rewritesToAnnotatedType Funcons
f Maybe FTerm
Nothing Env
_ = Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Funcons] -> Maybe [Funcons]
forall a. a -> Maybe a
Just [Funcons
f])
rewritesToAnnotatedType Funcons
f (Just FTerm
term) Env
env = Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten
-> (Rewritten -> Rewrite (Maybe [Funcons]))
-> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
  ValTerm [Values
v]   -> Values -> Maybe FTerm -> Env -> Rewrite Bool
isInMaybeTermType Values
v (FTerm -> Maybe FTerm
forall a. a -> Maybe a
Just FTerm
term) Env
env Rewrite Bool
-> (Bool -> Rewrite (Maybe [Funcons])) -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                      Bool
True  -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Funcons] -> Maybe [Funcons]
forall a. a -> Maybe a
Just [Values -> Funcons
FValue Values
v])
                      Bool
_     -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Funcons]
forall a. Maybe a
Nothing
  ValTerm [Values]
vs    -> [Values] -> FTerm -> Env -> Rewrite Bool
isInMaybeTupleType [Values]
vs FTerm
term Env
env Rewrite Bool
-> (Bool -> Rewrite (Maybe [Funcons])) -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                      Bool
True  -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Funcons] -> Maybe [Funcons]
forall a. a -> Maybe a
Just ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs))
                      Bool
_     -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Funcons]
forall a. Maybe a
Nothing
  CompTerm Funcons
_  MSOS StepRes
_ -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Funcons]
forall a. Maybe a
Nothing

-- to be used by seqMatcher
isInMaybeTermTypePreserve :: Values -> Maybe FTerm -> Env -> Rewrite (Maybe [Values])
isInMaybeTermTypePreserve :: Values -> Maybe FTerm -> Env -> Rewrite (Maybe [Values])
isInMaybeTermTypePreserve Values
v Maybe FTerm
mty Env
env = Values -> Maybe FTerm -> Env -> Rewrite Bool
isInMaybeTermType Values
v Maybe FTerm
mty Env
env Rewrite Bool
-> (Bool -> Rewrite (Maybe [Values])) -> Rewrite (Maybe [Values])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Bool
True  -> Maybe [Values] -> Rewrite (Maybe [Values])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values] -> Maybe [Values]
forall a. a -> Maybe a
Just [Values
v])
  Bool
_     -> Maybe [Values] -> Rewrite (Maybe [Values])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Values]
forall a. Maybe a
Nothing

isInMaybeTypeTypePreserve :: ComputationTypes -> Maybe FTerm -> Env -> Rewrite (Maybe [ComputationTypes])
isInMaybeTypeTypePreserve :: ComputationTypes
-> Maybe FTerm -> Env -> Rewrite (Maybe [ComputationTypes])
isInMaybeTypeTypePreserve ComputationTypes
ty Maybe FTerm
_ Env
_ = Maybe [ComputationTypes] -> Rewrite (Maybe [ComputationTypes])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ComputationTypes] -> Maybe [ComputationTypes]
forall a. a -> Maybe a
Just [ComputationTypes
ty])

-- type checking
isInMaybeTermType :: Values -> (Maybe FTerm) -> Env -> Rewrite Bool
isInMaybeTermType :: Values -> Maybe FTerm -> Env -> Rewrite Bool
isInMaybeTermType Values
v Maybe FTerm
Nothing Env
_ = Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isInMaybeTermType Values
v (Just FTerm
term) Env
env = 
    FTerm -> Env -> Rewrite Values
subsAndRewritesToValue FTerm
term Env
env Rewrite Values -> (Values -> Rewrite Bool) -> Rewrite Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Values -> Values -> Rewrite Bool
isIn Values
v

-- | To type check a sequence values simply checker whether all elements
-- of the sequence are of the given type
isInMaybeTupleType :: [Values] -> FTerm -> Env -> Rewrite Bool
isInMaybeTupleType :: [Values] -> FTerm -> Env -> Rewrite Bool
isInMaybeTupleType [Values]
vs FTerm
term Env
env = 
  FTerm -> Env -> Rewrite Values
subsAndRewritesToValue FTerm
term Env
env Rewrite Values -> (Values -> Rewrite Bool) -> Rewrite Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Values] -> [Values] -> Rewrite Bool
isInTuple [Values]
vs ([Values] -> Rewrite Bool)
-> (Values -> [Values]) -> Values -> Rewrite Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values -> [Values] -> [Values]
forall a. a -> [a] -> [a]
:[])

isInTuple :: [Values] -> [Values] -> Rewrite Bool
isInTuple :: [Values] -> [Values] -> Rewrite Bool
isInTuple [Values]
vs [Values]
mtys = case [Maybe (Types Funcons)] -> Maybe [Types Funcons]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ((Values -> Maybe (Types Funcons))
-> [Values] -> [Maybe (Types Funcons)]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Maybe (Types Funcons)
forall t. HasValues t => Values t -> Maybe (Types t)
castType [Values]
mtys) of
  Maybe [Types Funcons]
Nothing  -> Funcons -> MetaVar -> Rewrite Bool
forall a. Funcons -> MetaVar -> Rewrite a
sortErr (Values -> Funcons
FValue (Values -> Funcons) -> Values -> Funcons
forall a b. (a -> b) -> a -> b
$ Name -> [Funcons] -> Values
forall t. Name -> [t] -> Values t
ADTVal Name
"" ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
mtys)) 
                MetaVar
"rhs of annotation is not a type"
  Just [Types Funcons]
tys -> [Values] -> [TTParam] -> Rewrite Bool
Funcons.Patterns.isInTupleType [Values]
vs ((Types Funcons -> TTParam) -> [Types Funcons] -> [TTParam]
forall a b. (a -> b) -> [a] -> [b]
map Types Funcons -> TTParam
forall t. Types t -> (Types t, Maybe SeqSortOp)
paramFromType [Types Funcons]
tys)

paramFromType :: Types t -> (Types t, Maybe SeqSortOp)
paramFromType (AnnotatedType Types t
ty SeqSortOp
op) = (Types t
ty, SeqSortOp -> Maybe SeqSortOp
forall a. a -> Maybe a
Just SeqSortOp
op)
paramFromType Types t
ty = (Types t
ty, Maybe SeqSortOp
forall a. Maybe a
Nothing)
 
isIn :: Values -> Values -> Rewrite Bool
isIn :: Values -> Values -> Rewrite Bool
isIn Values
v Values
mty = case Values -> Maybe (Types Funcons)
forall t. HasValues t => Values t -> Maybe (Types t)
castType Values
mty of
    Maybe (Types Funcons)
Nothing -> Funcons -> MetaVar -> Rewrite Bool
forall a. Funcons -> MetaVar -> Rewrite a
sortErr (Values -> Funcons
FValue Values
mty) MetaVar
"rhs of annotation is not a type"
    Just Types Funcons
ty -> Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
v Types Funcons
ty
  
isInType :: Values -> Types -> Rewrite Bool
isInType :: Values -> Types Funcons -> Rewrite Bool
isInType Values
v (ADT Name
"ground-values" []) = Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Values -> Bool
forall t. HasValues t => Values t -> Bool
isGround Values
v)
isInType Values
v (ADT Name
"maps" [Funcons
kt', Funcons
vt']) = case Values
v of
  Map ValueMaps Values
m -> do
    Types Funcons
kt <- Funcons -> Rewrite (Types Funcons)
rewritesToType Funcons
kt'
    Types Funcons
vt <- Funcons -> Rewrite (Types Funcons)
rewritesToType Funcons
vt'
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Rewrite [Bool] -> Rewrite Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite Bool] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence 
          [[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Rewrite [Bool] -> Rewrite Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Values -> Rewrite Bool) -> [Values] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Values -> Types Funcons -> Rewrite Bool)
-> Types Funcons -> Values -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
kt) (ValueMaps Values -> [Values]
forall k a. Map k a -> [k]
M.keys ValueMaps Values
m)
          ,[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Rewrite [Bool] -> Rewrite Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Values] -> Rewrite Bool) -> [[Values]] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (([Values] -> [TTParam] -> Rewrite Bool)
-> [TTParam] -> [Values] -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Values] -> [TTParam] -> Rewrite Bool
Funcons.Patterns.isInTupleType [Types Funcons -> TTParam
forall t. Types t -> (Types t, Maybe SeqSortOp)
paramFromType Types Funcons
vt]) (ValueMaps Values -> [[Values]]
forall k a. Map k a -> [a]
M.elems ValueMaps Values
m)]
  Values
_ -> Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isInType Values
v (ADT Name
"multisets" [Funcons
ty']) = case Values
v of
  Multiset MultiSet Values
ls -> do
    Types Funcons
ty <- Funcons -> Rewrite (Types Funcons)
rewritesToType Funcons
ty' 
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Rewrite [Bool] -> Rewrite Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Values -> Rewrite Bool) -> [Values] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Values -> Types Funcons -> Rewrite Bool)
-> Types Funcons -> Values -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
ty) (MultiSet Values -> [Values]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList MultiSet Values
ls)
  Values
_ -> Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isInType Values
v (ADT Name
"sets" [Funcons
ty']) = case Values
v of
  Set ValueSets Values
ls -> do
    Types Funcons
ty <- Funcons -> Rewrite (Types Funcons)
rewritesToType Funcons
ty' 
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Rewrite [Bool] -> Rewrite Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Values -> Rewrite Bool) -> [Values] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Values -> Types Funcons -> Rewrite Bool)
-> Types Funcons -> Values -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
ty) (ValueSets Values -> [Values]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ValueSets Values
ls)
  Values
_ -> Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
-- characters
isInType Values
v Types Funcons
AsciiCharacters = Values -> Name -> Rewrite Bool
isInUnicodeType Values
v Name
"ascii-points"
isInType Values
v Types Funcons
ISOLatinCharacters = Values -> Name -> Rewrite Bool
isInUnicodeType Values
v Name
"iso-latin-1-points"
isInType Values
v Types Funcons
BMPCharacters = Values -> Name -> Rewrite Bool
isInUnicodeType Values
v Name
"basic-multilingual-plane-points"
-- type operators and datatypes
isInType Values
v (ADT Name
nm [Funcons]
tys) = do
    DataTypeMemberss Name
_ [TPattern]
tpats [DataTypeAltt]
alts <- Name -> Rewrite DataTypeMembers
typeEnvLookup Name
nm
    [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> Rewrite [Bool] -> Rewrite Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataTypeAltt -> Rewrite Bool) -> [DataTypeAltt] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([TPattern] -> DataTypeAltt -> Rewrite Bool
isInAlt [TPattern]
tpats) [DataTypeAltt]
alts 
 where isInAlt :: [TPattern] -> DataTypeAltt -> Rewrite Bool
isInAlt [TPattern]
tpats (DataTypeInclusionn FTerm
ty_term) = do 
            -- TODO change DataTypeMember so that tpats are value-patterns
            --      requires change in the generator
            Env
env <- [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
tys ((TPattern -> FPattern) -> [TPattern] -> [FPattern]
forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue (VPattern -> FPattern)
-> (TPattern -> VPattern) -> TPattern -> FPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPattern -> VPattern
VPType) [TPattern]
tpats) Env
forall k a. Map k a
emptyEnv
            FTerm -> Env -> Rewrite Values
subsAndRewritesToValue FTerm
ty_term Env
env Rewrite Values -> (Values -> Rewrite Bool) -> Rewrite Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Values -> Values -> Rewrite Bool
isIn Values
v 
       isInAlt [TPattern]
tpats (DataTypeMemberConstructor Name
cons [FTerm]
ty_terms Maybe [TPattern]
mtpats)
        | ADTVal Name
cons' [Funcons]
args <- Values
v, Name
cons' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
cons = do
          Env
env <- case Maybe [TPattern]
mtpats of 
                  Just [TPattern]
tpats -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
tys ((TPattern -> FPattern) -> [TPattern] -> [FPattern]
forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue (VPattern -> FPattern)
-> (TPattern -> VPattern) -> TPattern -> FPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPattern -> VPattern
VPType) [TPattern]
tpats) Env
forall k a. Map k a
emptyEnv
                  Maybe [TPattern]
Nothing    -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
tys ((TPattern -> FPattern) -> [TPattern] -> [FPattern]
forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue (VPattern -> FPattern)
-> (TPattern -> VPattern) -> TPattern -> FPattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPattern -> VPattern
VPType) [TPattern]
tpats) Env
forall k a. Map k a
emptyEnv
          case (Funcons -> Bool) -> [Funcons] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not(Bool -> Bool) -> (Funcons -> Bool) -> Funcons -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Funcons -> Bool
hasStep) [Funcons]
args of 
            Bool
True  -> (FTerm -> Rewrite [Values]) -> [FTerm] -> Rewrite [[Values]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((FTerm -> Env -> Rewrite [Values])
-> Env -> FTerm -> Rewrite [Values]
forall a b c. (a -> b -> c) -> b -> a -> c
flip FTerm -> Env -> Rewrite [Values]
subsAndRewritesToValues Env
env) [FTerm]
ty_terms Rewrite [[Values]] -> ([[Values]] -> Rewrite Bool) -> Rewrite Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
                        [Values] -> [Values] -> Rewrite Bool
isInTuple ((Funcons -> Values) -> [Funcons] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
downcastValue [Funcons]
args) ([Values] -> Rewrite Bool)
-> ([[Values]] -> [Values]) -> [[Values]] -> Rewrite Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Values]] -> [Values]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            Bool
_     -> Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- imprecision
       isInAlt [TPattern]
_ DataTypeAltt
_ = Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isInType Values
v (AnnotatedType Types Funcons
ty SeqSortOp
op) = [Values] -> [TTParam] -> Rewrite Bool
Funcons.Patterns.isInTupleType [Values
v] [(Types Funcons
ty, SeqSortOp -> Maybe SeqSortOp
forall a. a -> Maybe a
Just SeqSortOp
op)] 
isInType Values
v (Union Types Funcons
ty1 Types Funcons
ty2) = 
  Bool -> Bool -> Bool
(||) (Bool -> Bool -> Bool) -> Rewrite Bool -> Rewrite (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
v Types Funcons
ty1 Rewrite (Bool -> Bool) -> Rewrite Bool -> Rewrite Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
v Types Funcons
ty2
isInType Values
v (Intersection Types Funcons
ty1 Types Funcons
ty2) = 
  Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool) -> Rewrite Bool -> Rewrite (Bool -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
v Types Funcons
ty1 Rewrite (Bool -> Bool) -> Rewrite Bool -> Rewrite Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
v Types Funcons
ty2
isInType Values
v (Complement Types Funcons
t) = 
  Bool -> Bool
not (Bool -> Bool) -> Rewrite Bool -> Rewrite Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
v Types Funcons
t
isInType Values
v Types Funcons
t = Rewrite Bool
-> (Bool -> Rewrite Bool) -> Maybe Bool -> Rewrite Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Values -> Types Funcons -> Maybe Bool
forall t. HasValues t => Values t -> Types t -> Maybe Bool
Funcons.Types.isInType Values
v Types Funcons
t)

isInUnicodeType :: Values -> Name -> Rewrite Bool
isInUnicodeType v :: Values
v@(ADTVal Name
c [Funcons
p]) Name
fname = do
  Types Funcons
rangeTy   <- Funcons -> Rewrite (Types Funcons)
rewritesToType (Name -> [Funcons] -> Funcons
applyFuncon Name
fname [])
  Bool
isUnicode <- Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
v Types Funcons
forall t. Types t
UnicodeCharacters
  Values
point     <- Funcons -> Rewrite Values
rewritesToValue Funcons
p
  Bool
inRange   <- Values -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values
point Types Funcons
rangeTy 
  Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
isUnicode,Bool
inRange])
isInUnicodeType Values
_ Name
_ = Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False


isInTupleType :: [Values] -> [TTParam] -> Rewrite Bool
isInTupleType :: [Values] -> [TTParam] -> Rewrite Bool
isInTupleType [Values]
vs [TTParam]
ttparams = 
    Rewrite Env -> Rewrite (Either IException Env)
forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch ([Values] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values]
vs ((TTParam -> VPattern) -> [TTParam] -> [VPattern]
forall a b. (a -> b) -> [a] -> [b]
map TTParam -> VPattern
mkPattern [TTParam]
ttparams) Env
forall k a. Map k a
emptyEnv) Rewrite (Either IException Env)
-> (Either IException Env -> Rewrite Bool) -> Rewrite Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Env
env' -> Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Left (Funcons
_,Funcons
_,PatternMismatch MetaVar
_) -> Bool -> Rewrite Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Left IException
ie -> IException -> Rewrite Bool
forall a. IException -> Rewrite a
rewrite_rethrow IException
ie 
    where mkPattern :: TTParam -> VPattern
mkPattern (Types Funcons
ty, Maybe SeqSortOp
mop) = VPattern -> FTerm -> VPattern
VPAnnotated VPattern
ty_pat (Funcons -> FTerm
TFuncon (Types Funcons -> Funcons
type_ Types Funcons
ty))
            where ty_pat :: VPattern
ty_pat = case Maybe SeqSortOp
mop of 
                                Maybe SeqSortOp
Nothing -> MetaVar -> VPattern
VPMetaVar MetaVar
"Dummy"
                                Just op -> MetaVar -> SeqSortOp -> VPattern
VPSeqVar MetaVar
"Dummy" SeqSortOp
op

typeEnvLookup :: Name -> Rewrite DataTypeMembers 
typeEnvLookup :: Name -> Rewrite DataTypeMembers
typeEnvLookup Name
con = (RewriteReader
 -> RewriteState
 -> (Either IException DataTypeMembers, RewriteState,
     RewriteWriterr))
-> Rewrite DataTypeMembers
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException DataTypeMembers, RewriteState,
      RewriteWriterr))
 -> Rewrite DataTypeMembers)
-> (RewriteReader
    -> RewriteState
    -> (Either IException DataTypeMembers, RewriteState,
        RewriteWriterr))
-> Rewrite DataTypeMembers
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    case Name -> TypeRelation -> Maybe DataTypeMembers
typeLookup Name
con (RewriteReader -> TypeRelation
ty_env RewriteReader
ctxt) of
      Maybe DataTypeMembers
Nothing -> (IException -> Either IException DataTypeMembers
forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception(MetaVar -> IE
Internal (MetaVar
"type lookup failed: " MetaVar -> MetaVar -> MetaVar
forall a. [a] -> [a] -> [a]
++ Name -> MetaVar
unpack Name
con)) RewriteReader
ctxt)
                        , RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)
      Just DataTypeMembers
members -> (DataTypeMembers -> Either IException DataTypeMembers
forall a b. b -> Either a b
Right DataTypeMembers
members, RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)

-- | 
-- Parameterisable evaluation function function for types.
rewriteType :: Name -> [Values] -> Rewrite Rewritten
rewriteType :: Name -> [Values] -> Rewrite Rewritten
rewriteType Name
nm [Values]
vs = Values -> Rewrite Rewritten
rewritten (ComputationTypes -> Values
forall t. ComputationTypes t -> Values t
ComputationType(Types Funcons -> ComputationTypes
forall t. Types t -> ComputationTypes t
Type(Name -> [Funcons] -> Types Funcons
forall t. Name -> [t] -> Types t
ADT Name
nm ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
forall t. HasValues t => Values t -> t
inject [Values]
vs))))

pat2term :: FPattern -> FTerm
pat2term :: FPattern -> FTerm
pat2term FPattern
pat = case FPattern
pat of
  PAnnotated FPattern
pat FTerm
_  -> FPattern -> FTerm
pat2term FPattern
pat
  FPattern
PWildCard         -> FTerm
TAny
  PMetaVar MetaVar
var      -> MetaVar -> FTerm
TVar MetaVar
var
  PSeqVar MetaVar
var SeqSortOp
_     -> MetaVar -> FTerm
TVar MetaVar
var
  PValue VPattern
vpat       -> VPattern -> FTerm
vpat2term VPattern
vpat

vpat2term :: VPattern -> FTerm 
vpat2term :: VPattern -> FTerm
vpat2term VPattern
vpat = case VPattern
vpat of 
  PADT Name
cons [VPattern]
pats    -> case [VPattern]
pats of [] -> Name -> FTerm
TName Name
cons
                                    [VPattern]
_  -> Name -> [FTerm] -> FTerm
TApp Name
cons ((VPattern -> FTerm) -> [VPattern] -> [FTerm]
forall a b. (a -> b) -> [a] -> [b]
map VPattern -> FTerm
vpat2term [VPattern]
pats)
  VPLit Values
lit         -> Funcons -> FTerm
TFuncon (Funcons -> FTerm) -> Funcons -> FTerm
forall a b. (a -> b) -> a -> b
$ (Values -> Funcons
FValue Values
lit) 
  VPattern
VPWildCard        -> FTerm
TAny
--  PList pats        -> TList (map vpat2term pats)
  VPMetaVar MetaVar
var     -> MetaVar -> FTerm
TVar MetaVar
var
  VPSeqVar MetaVar
var SeqSortOp
_    -> MetaVar -> FTerm
TVar MetaVar
var
  VPAnnotated VPattern
pat FTerm
_ -> VPattern -> FTerm
vpat2term VPattern
pat
  VPType TPattern
typat      -> TPattern -> FTerm
typat2term TPattern
typat

typat2term :: TPattern -> FTerm
typat2term :: TPattern -> FTerm
typat2term TPattern
typat = case TPattern
typat of 
  TPADT Name
cons [TPattern]
pats     -> case [TPattern]
pats of [] -> Name -> FTerm
TName Name
cons
                                      [TPattern]
_  -> Name -> [FTerm] -> FTerm
TApp Name
cons ((TPattern -> FTerm) -> [TPattern] -> [FTerm]
forall a b. (a -> b) -> [a] -> [b]
map TPattern -> FTerm
typat2term [TPattern]
pats)
  TPLit FTerm
lit           -> FTerm
lit 
  TPattern
TPWildCard          -> FTerm
TAny
  TPVar MetaVar
var           -> MetaVar -> FTerm
TVar MetaVar
var
  TPSeqVar MetaVar
var SeqSortOp
_      -> MetaVar -> FTerm
TVar MetaVar
var
  TPComputes TPattern
f        -> FTerm -> FTerm
TSortComputes (TPattern -> FTerm
typat2term TPattern
f)
  TPComputesFrom TPattern
f TPattern
t  -> FTerm -> FTerm -> FTerm
TSortComputesFrom (TPattern -> FTerm
typat2term TPattern
f) (TPattern -> FTerm
typat2term TPattern
t)