{-# 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.RunOptions (SourceOfND(..))

import Control.Monad (forM)
import Data.Function (on)
import Data.List (sortBy, intercalate)
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 :: forall a b. (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 a. a -> Rewrite a
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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
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 a. a -> Rewrite a
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 a. a -> Rewrite a
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 :: forall a.
(a -> Maybe FTerm -> Env -> Rewrite (Maybe [a]))
-> ([a] -> Levelled) -> SeqVarInfo -> Matcher a
seqMatcher a -> Maybe FTerm -> Env -> Rewrite (Maybe [a])
p [a] -> Levelled
level ([Char]
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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length)
    SeqSortOp
PlusOp         -> case [a]
str of  
                        [] -> [(Int, Env)] -> Rewrite [(Int, Env)]
forall a. a -> Rewrite a
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 a. [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 a. a -> Rewrite a
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 a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t [a]
fs, [Char] -> Levelled -> Env -> Env
envInsert [Char]
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 :: forall a. (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
takeWhileM a -> Rewrite (Maybe [a])
_ [] = [[a]] -> Rewrite [[a]]
forall 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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return []
                Left IException
ie | IException -> Bool
failsRule IException
ie  -> [[a]] -> Rewrite [[a]]
forall a. 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
forall a. Ord a => a -> a -> 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 :: Ord a => a -> a -> Ordering
                      comparison :: forall a. Ord a => a -> a -> Ordering
comparison = case Maybe FTerm
mty of
                        Maybe FTerm
Nothing   -> a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare      -- no annotation => shortest match
                        Just  FTerm
_   -> (a -> a -> Ordering) -> a -> a -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare -- annoration => longest match

matching :: String -> (a -> String) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching :: forall a.
[Char] -> (a -> [Char]) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching [Char]
pats a -> [Char]
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 a b. (a -> b -> b) -> b -> [a] -> b
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 = [Char] -> IE
PatternMismatch ([Char]
"Pattern match failed: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ((a -> [Char]) -> [a] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map a -> [Char]
show [a]
str) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" does not match " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
pats)
    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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env'
        [(Int, Env)]
_  -> [Char] -> Rewrite Env
forall a. [Char] -> Rewrite a
internal ([Char]
"ambiguity not resolved") 
    where   m :: Int
m = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
str
            -- sequencing of matchers specifically to disambiguate safely
            lastMatcher :: Matcher a
            lastMatcher :: forall a. 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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
k,Env
env)]
                                | Bool
otherwise    = [(Int, Env)] -> Rewrite [(Int, Env)]
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return []

            seqWith :: Matcher a -> Matcher a -> Matcher a
            seqWith :: forall a. 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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [(Int, Env)] -> Rewrite [(Int, Env)]
acceptFirst
             where  acceptFirst :: [(Int, Env)] -> Rewrite [(Int, Env)]
acceptFirst [] = [(Int, Env)] -> Rewrite [(Int, Env)]
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return []
                    acceptFirst xs :: [(Int, Env)]
xs@((Int
r,Env
env):[(Int, Env)]
rest) = do
--                    requires backtracking between premises and pattern matching to avoid unnecessary failure
                      ((Int
r, Env
env),[(Int, Env)]
rest) <- SourceOfND -> [(Int, Env)] -> Rewrite ((Int, Env), [(Int, Env)])
forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDPatternMatching [(Int, Env)]
xs
                      [(Int, Env)]
res <- Matcher a
q [a]
str Int
r Env
env
                      case [(Int, Env)]
res of []  -> [(Int, Env)] -> Rewrite [(Int, Env)]
acceptFirst [(Int, Env)]
rest
                                  [(Int, Env)]
_   -> [(Int, Env)] -> Rewrite [(Int, Env)]
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int, Env)]
res

ordered_subsequences :: [a] -> [[a]]
ordered_subsequences :: forall a. [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 -> [Char] -> [Char]
[FPattern] -> [Char] -> [Char]
FPattern -> [Char]
(Int -> FPattern -> [Char] -> [Char])
-> (FPattern -> [Char])
-> ([FPattern] -> [Char] -> [Char])
-> Show FPattern
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> FPattern -> [Char] -> [Char]
showsPrec :: Int -> FPattern -> [Char] -> [Char]
$cshow :: FPattern -> [Char]
show :: FPattern -> [Char]
$cshowList :: [FPattern] -> [Char] -> [Char]
showList :: [FPattern] -> [Char] -> [Char]
Show, FPattern -> FPattern -> Bool
(FPattern -> FPattern -> Bool)
-> (FPattern -> FPattern -> Bool) -> Eq FPattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FPattern -> FPattern -> Bool
== :: FPattern -> FPattern -> Bool
$c/= :: FPattern -> FPattern -> Bool
/= :: 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
$ccompare :: FPattern -> FPattern -> Ordering
compare :: FPattern -> FPattern -> Ordering
$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
>= :: FPattern -> FPattern -> Bool
$cmax :: FPattern -> FPattern -> FPattern
max :: FPattern -> FPattern -> FPattern
$cmin :: FPattern -> FPattern -> FPattern
min :: FPattern -> FPattern -> 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
$creadsPrec :: Int -> ReadS FPattern
readsPrec :: Int -> ReadS FPattern
$creadList :: ReadS [FPattern]
readList :: ReadS [FPattern]
$creadPrec :: ReadPrec FPattern
readPrec :: ReadPrec FPattern
$creadListPrec :: ReadPrec [FPattern]
readListPrec :: ReadPrec [FPattern]
Read)

f2vPattern :: FPattern -> VPattern
f2vPattern :: FPattern -> VPattern
f2vPattern (PValue VPattern
v) = VPattern
v
f2vPattern (PMetaVar [Char]
var) = [Char] -> VPattern
VPMetaVar [Char]
var
f2vPattern (PSeqVar [Char]
var SeqSortOp
op) = [Char] -> SeqSortOp -> VPattern
VPSeqVar [Char]
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 
                | VPEmptySet
                | VPType TPattern
                deriving (Int -> VPattern -> [Char] -> [Char]
[VPattern] -> [Char] -> [Char]
VPattern -> [Char]
(Int -> VPattern -> [Char] -> [Char])
-> (VPattern -> [Char])
-> ([VPattern] -> [Char] -> [Char])
-> Show VPattern
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> VPattern -> [Char] -> [Char]
showsPrec :: Int -> VPattern -> [Char] -> [Char]
$cshow :: VPattern -> [Char]
show :: VPattern -> [Char]
$cshowList :: [VPattern] -> [Char] -> [Char]
showList :: [VPattern] -> [Char] -> [Char]
Show, VPattern -> VPattern -> Bool
(VPattern -> VPattern -> Bool)
-> (VPattern -> VPattern -> Bool) -> Eq VPattern
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VPattern -> VPattern -> Bool
== :: VPattern -> VPattern -> Bool
$c/= :: VPattern -> VPattern -> Bool
/= :: 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
$ccompare :: VPattern -> VPattern -> Ordering
compare :: VPattern -> VPattern -> Ordering
$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
>= :: VPattern -> VPattern -> Bool
$cmax :: VPattern -> VPattern -> VPattern
max :: VPattern -> VPattern -> VPattern
$cmin :: VPattern -> VPattern -> VPattern
min :: VPattern -> VPattern -> 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
$creadsPrec :: Int -> ReadS VPattern
readsPrec :: Int -> ReadS VPattern
$creadList :: ReadS [VPattern]
readList :: ReadS [VPattern]
$creadPrec :: ReadPrec VPattern
readPrec :: ReadPrec VPattern
$creadListPrec :: ReadPrec [VPattern]
readListPrec :: ReadPrec [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 [Char]
var) = TPattern -> Maybe TPattern
forall a. a -> Maybe a
Just (TPattern -> Maybe TPattern) -> TPattern -> Maybe TPattern
forall a b. (a -> b) -> a -> b
$ [Char] -> TPattern
TPVar [Char]
var
v2tPattern (VPSeqVar [Char]
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
$ [Char] -> SeqSortOp -> TPattern
TPSeqVar [Char]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM VPattern -> Maybe TPattern
v2tPattern [VPattern]
pats
v2tPattern (VPLit Values Funcons
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 -> Funcons
FValue Values Funcons
lit))
v2tPattern VPattern
VPWildCard = TPattern -> Maybe TPattern
forall a. a -> Maybe a
Just TPattern
TPWildCard
--v2tPattern (PList _) = Nothing 
v2tPattern VPattern
VPEmptySet = Maybe TPattern
forall a. Maybe a
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 [Char]
x)          = [Char] -> FPattern
PMetaVar [Char]
x
v2fPattern (VPSeqVar [Char]
x SeqSortOp
op)        = [Char] -> SeqSortOp -> FPattern
PSeqVar [Char]
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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return VPattern
VPWildCard
  VPattern
VPEmptySet      -> VPattern -> Rewrite VPattern
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return VPattern
VPEmptySet
--  PList pats      -> PList <$> subs_flatten pats env
  VPMetaVar [Char]
var   -> case [Char] -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
var Env
env of
                      Maybe Levelled
Nothing -> VPattern -> Rewrite VPattern
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> VPattern
VPMetaVar [Char]
var)
                      Just Levelled
v  -> Values Funcons -> VPattern
VPLit (Values Funcons -> VPattern)
-> Rewrite (Values Funcons) -> Rewrite VPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Levelled -> Rewrite (Values Funcons)
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 a b. Rewrite (a -> b) -> Rewrite a -> Rewrite b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FTerm -> Rewrite FTerm
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return FTerm
ann 
  VPSeqVar [Char]
var SeqSortOp
op -> case [Char] -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
var Env
env of
                      Maybe Levelled
Nothing -> VPattern -> Rewrite VPattern
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> SeqSortOp -> VPattern
VPSeqVar [Char]
var SeqSortOp
op)
                      Just Levelled
v  -> Values Funcons -> VPattern
VPLit (Values Funcons -> VPattern)
-> Rewrite (Values Funcons) -> Rewrite VPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Levelled -> Rewrite (Values Funcons)
vLevel Levelled
v 
  VPLit Values Funcons
lit       -> VPattern -> Rewrite VPattern
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (VPattern -> Rewrite VPattern) -> VPattern -> Rewrite VPattern
forall a b. (a -> b) -> a -> b
$ Values Funcons -> VPattern
VPLit Values Funcons
lit
  VPType TPattern
tpat     -> VPattern -> Rewrite VPattern
forall a. a -> Rewrite a
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 [Char]
k)   -> Env -> [Char] -> VPattern -> Rewrite [VPattern]
envMaybeLookup Env
env [Char]
k VPattern
vpat
              vpat :: VPattern
vpat@(VPSeqVar [Char]
k SeqSortOp
op) -> Env -> [Char] -> VPattern -> Rewrite [VPattern]
envMaybeLookup Env
env [Char]
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 -> [Char] -> VPattern -> Rewrite [VPattern]
envMaybeLookup Env
env [Char]
k VPattern
vpat = case [Char] -> Env -> Maybe Levelled
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
k Env
env of
                            Maybe Levelled
Nothing -> [VPattern] -> Rewrite [VPattern]
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return [VPattern
vpat]
                            Just Levelled
lf -> (Values Funcons -> VPattern) -> [Values Funcons] -> [VPattern]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> VPattern
VPLit ([Values Funcons] -> [VPattern])
-> Rewrite [Values Funcons] -> Rewrite [VPattern]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Levelled -> Rewrite [Values Funcons]
vsLevel Levelled
lf


-- | Variant of 'vsMatch' that is lifted into the 'MSOS' monad.
lifted_vsMatch :: [Values Funcons] -> [VPattern] -> Env -> MSOS Env
lifted_vsMatch [Values Funcons]
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 Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons]
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 Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons]
str [VPattern]
pats Env
env = [Values Funcons] -> [VPattern] -> Env -> Rewrite Env
strict_vsMatch [Values Funcons]
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 Funcons] -> [VPattern] -> Env -> Rewrite Env
strict_vsMatch [Values Funcons]
str [VPattern]
pats Env
env 
  | (Values Funcons -> Bool) -> [Values Funcons] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Values Funcons -> Bool
forall {t}. Values t -> Bool
isSort_ [Values Funcons]
str 
  , Just [TPattern]
tpats <- [Maybe TPattern] -> Maybe [TPattern]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [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 Funcons -> ComputationTypes)
-> [Values Funcons] -> [ComputationTypes]
forall a b. (a -> b) -> [a] -> [b]
map (Funcons -> ComputationTypes
downcastSort (Funcons -> ComputationTypes)
-> (Values Funcons -> Funcons)
-> Values Funcons
-> ComputationTypes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values Funcons -> Funcons
FValue) [Values Funcons]
str) [TPattern]
tpats Env
env 
  | Bool
otherwise = [Char]
-> (Values Funcons -> [Char])
-> [Values Funcons]
-> [Matcher (Values Funcons)]
-> Env
-> Rewrite Env
forall a.
[Char] -> (a -> [Char]) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching ([VPattern] -> [Char]
forall a. Show a => a -> [Char]
show [VPattern]
pats) Values Funcons -> [Char]
showValues [Values Funcons]
str [Matcher (Values Funcons)]
matchers Env
env
        where   matchers :: [Matcher (Values Funcons)]
matchers = (VPattern -> Matcher (Values Funcons))
-> [VPattern] -> [Matcher (Values Funcons)]
forall a b. (a -> b) -> [a] -> [b]
map VPattern -> Matcher (Values Funcons)
toMatcher [VPattern]
pats
                toMatcher :: VPattern -> Matcher (Values Funcons)
toMatcher VPattern
pat = case VPattern -> Maybe SeqVarInfo
vpSeqVarInfo VPattern
pat of
                    Just SeqVarInfo
info   -> (Values Funcons
 -> Maybe FTerm -> Env -> Rewrite (Maybe [Values Funcons]))
-> ([Values Funcons] -> Levelled)
-> SeqVarInfo
-> Matcher (Values Funcons)
forall a.
(a -> Maybe FTerm -> Env -> Rewrite (Maybe [a]))
-> ([a] -> Levelled) -> SeqVarInfo -> Matcher a
seqMatcher Values Funcons
-> Maybe FTerm -> Env -> Rewrite (Maybe [Values Funcons])
isInMaybeTermTypePreserve [Values Funcons] -> Levelled
ValuesTerm SeqVarInfo
info
                    Maybe SeqVarInfo
Nothing     -> (Values Funcons -> VPattern -> Env -> Rewrite Env)
-> VPattern -> Matcher (Values Funcons)
forall a b. (a -> b -> Env -> Rewrite Env) -> b -> Matcher a
singleMatcher Values Funcons -> 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 a b. MSOS a -> (a -> MSOS b) -> MSOS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  (ValTerm [Values Funcons]
v, Env
env')       -> IE -> MSOS Env
forall b. IE -> MSOS b
msos_throw ([Values Funcons] -> IE
StepOnValue [Values Funcons]
v)
  (CompTerm Funcons
f MSOS StepRes
step,Env
env')  -> do 
      StepRes
ef' <- MSOS ()
count_delegation MSOS () -> MSOS StepRes -> MSOS StepRes
forall a b. MSOS a -> MSOS b -> MSOS b
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 Funcons]
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 -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
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 Funcons]
downValues [Funcons]
vs = (Funcons -> Values Funcons) -> [Funcons] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values Funcons
downcastValue [Funcons]
vs
          in [Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch ([Funcons] -> [Values Funcons]
downValues [Funcons]
str) ((FPattern -> VPattern) -> [FPattern] -> [VPattern]
forall a b. (a -> b) -> [a] -> [b]
map FPattern -> VPattern
f2vPattern [FPattern]
pats) Env
env
    | Bool
otherwise = [Char]
-> (Funcons -> [Char])
-> [Funcons]
-> [Matcher Funcons]
-> Env
-> Rewrite Env
forall a.
[Char] -> (a -> [Char]) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching ([FPattern] -> [Char]
forall a. Show a => a -> [Char]
show [FPattern]
pats) Funcons -> [Char]
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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
fMatch Funcons
f (PMetaVar [Char]
var) Env
env = Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Levelled -> Env -> Env
envInsert [Char]
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 Funcons]
tys <- FTerm -> Env -> Rewrite [Values Funcons]
subsAndRewritesToValues FTerm
term Env
env
    let fail :: Rewrite a
fail = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"pattern annotation check failed: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Values Funcons] -> [Char]
showValuesSeq [Values Funcons]
tys))
    Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten -> (Rewritten -> Rewrite Env) -> Rewrite Env
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case  
        ValTerm [Values Funcons]
vs  -> do   Bool
b <- [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple [Values Funcons]
vs [Values Funcons]
tys 
                            if Bool
b then [Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons]
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 [Char]
_ 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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
    \case   ValTerm [Values Funcons]
vs -> [Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons]
vs [VPattern
pat] Env
env
            CompTerm Funcons
_ MSOS StepRes
_ -> IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw --important, should remain last 
                ([Char] -> IE
PatternMismatch ([Char]
"could not rewrite to value: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Funcons -> [Char]
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 a. a -> Rewrite a
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 ([Char] -> IE
PatternMismatch [Char]
"fMaybeMatch")

lifted_vMaybeMatch :: Maybe (Values Funcons) -> Maybe VPattern -> Env -> MSOS Env
lifted_vMaybeMatch Maybe (Values Funcons)
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 Funcons) -> Maybe VPattern -> Env -> Rewrite Env
vMaybeMatch Maybe (Values Funcons)
mv Maybe VPattern
mp Env
env
vMaybeMatch :: Maybe Values -> Maybe VPattern -> Env -> Rewrite Env
vMaybeMatch :: Maybe (Values Funcons) -> Maybe VPattern -> Env -> Rewrite Env
vMaybeMatch Maybe (Values Funcons)
Nothing Maybe VPattern
Nothing Env
env = Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMaybeMatch (Just Values Funcons
v) (Just VPattern
p) Env
env = Values Funcons -> VPattern -> Env -> Rewrite Env
vMatch Values Funcons
v VPattern
p Env
env
vMaybeMatch Maybe (Values Funcons)
_ Maybe VPattern
_ Env
env = IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"vMaybeMatch")) 

lifted_vMatch :: Values Funcons -> VPattern -> Env -> MSOS Env
lifted_vMatch Values Funcons
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 Funcons -> VPattern -> Env -> Rewrite Env
vMatch Values Funcons
v VPattern
p Env
env
vMatch :: Values -> VPattern -> Env -> Rewrite Env
-- builtin special case for builtin value constructor `datatype-value`
vMatch :: Values Funcons -> 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
"" ([Char] -> Funcons
string_ (Name -> [Char]
unpack Name
str)Funcons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:[Funcons]
vs) [VPattern]
pats Env
env
vMatch Values Funcons
_ (VPattern
VPWildCard) Env
env = Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch (Set ValueSets (Values Funcons)
s) VPattern
VPEmptySet Env
env | ValueSets (Values Funcons) -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ValueSets (Values Funcons)
s = Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch (Map ValueMaps (Values Funcons)
m) VPattern
VPEmptySet Env
env | ValueMaps (Values Funcons) -> Bool
forall a. Map (Values Funcons) a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ValueMaps (Values Funcons)
m = Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch Values Funcons
VAny VPattern
_ Env
env = Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch Values Funcons
v (VPMetaVar [Char]
var) Env
env = Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Levelled -> Env -> Env
envInsert [Char]
var (Values Funcons -> Levelled
ValueTerm Values Funcons
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 Funcons
v (VPAnnotated VPattern
pat FTerm
term) Env
env = do
    Values Funcons
ty <- FTerm -> Env -> Rewrite (Values Funcons)
subsAndRewritesToValue FTerm
term Env
env
    Values Funcons -> Values Funcons -> Rewrite Bool
isIn Values Funcons
v Values Funcons
ty Rewrite Bool -> (Bool -> Rewrite Env) -> Rewrite Env
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True  -> Values Funcons -> VPattern -> Env -> Rewrite Env
vMatch Values Funcons
v VPattern
pat Env
env
        Bool
False -> IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"pattern annotation check failed: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Values Funcons -> [Char]
showValues Values Funcons
ty))
vMatch Values Funcons
v (VPLit Values Funcons
v2) Env
env | Values Funcons
v Values Funcons -> Values Funcons -> Bool
forall a. Eq a => a -> a -> Bool
== Values Funcons
v2 = Env -> Rewrite Env
forall a. a -> Rewrite a
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 Funcons
v pat :: VPattern
pat@(VPSeqVar [Char]
_ SeqSortOp
_) Env
env = [Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons
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 Funcons
v VPattern
_ Env
_ = IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"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 = [Char]
-> (ComputationTypes -> [Char])
-> [ComputationTypes]
-> [Matcher ComputationTypes]
-> Env
-> Rewrite Env
forall a.
[Char] -> (a -> [Char]) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching ([TPattern] -> [Char]
forall a. Show a => a -> [Char]
show [TPattern]
pats) ComputationTypes -> [Char]
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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
  TPVar [Char]
x -> Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Levelled -> Env -> Env
envInsert [Char]
x (ComputationTypes -> Levelled
TypeTerm ComputationTypes
t) Env
env)
  TPSeqVar [Char]
_ SeqSortOp
_ -> [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
tsMatch [ComputationTypes
t] [TPattern
p] Env
env
  TPLit FTerm
ft -> FTerm -> Env -> Rewrite (Values Funcons)
subsAndRewritesToValue FTerm
ft Env
env Rewrite (Values Funcons)
-> (Values Funcons -> Rewrite Env) -> Rewrite Env
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env 
                 else IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"failed to match"))
    Values Funcons
_ -> [Char] -> Rewrite Env
forall a. [Char] -> Rewrite a
internal [Char]
"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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
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 ([Char] -> IE
PatternMismatch ([Char]
"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 ([Char] -> IE
PatternMismatch ([Char]
"failed to match constructors: (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Name, Name) -> [Char]
forall a. Show a => a -> [Char]
show (Name
con,Name
pat_con) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")"))
    | 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 [Char]
var SeqSortOp
op) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just ([Char]
var, SeqSortOp
op, Maybe FTerm
forall a. Maybe a
Nothing)
fpSeqVarInfo (PAnnotated (PSeqVar [Char]
var SeqSortOp
op) FTerm
term) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just ([Char]
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 [Char]
var SeqSortOp
op) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just ([Char]
var, SeqSortOp
op, Maybe FTerm
forall a. Maybe a
Nothing)
vpSeqVarInfo (VPAnnotated (VPSeqVar [Char]
var SeqSortOp
op) FTerm
term) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just ([Char]
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 [Char]
var SeqSortOp
op) = SeqVarInfo -> Maybe SeqVarInfo
forall a. a -> Maybe a
Just ([Char]
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 -> 
        [Char]
-> ([Values Funcons] -> [Values Funcons] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop [Char]
"equality condition" (([Values Funcons] -> [Values Funcons] -> Bool)
-> [Values Funcons] -> [Values Funcons] -> Rewrite Bool
forall {m :: * -> *} {t} {t} {a}.
Monad m =>
(t -> t -> a) -> t -> t -> m a
lift [Values Funcons] -> [Values Funcons] -> Bool
allEqual) FTerm
term1 FTerm
term2 Env
env
    SCInequality FTerm
term1 FTerm
term2 ->     
        [Char]
-> ([Values Funcons] -> [Values Funcons] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop [Char]
"inequality condition" (([Values Funcons] -> [Values Funcons] -> Bool)
-> [Values Funcons] -> [Values Funcons] -> Rewrite Bool
forall {m :: * -> *} {t} {t} {a}.
Monad m =>
(t -> t -> a) -> t -> t -> m a
lift [Values Funcons] -> [Values Funcons] -> Bool
allUnEqual) FTerm
term1 FTerm
term2 Env
env
    SCIsInSort FTerm
term1 FTerm
term2 -> [Char]
-> ([Values Funcons] -> [Values Funcons] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop [Char]
"sort annotation" [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple FTerm
term1 FTerm
term2 Env
env
    SCNotInSort FTerm
term1 FTerm
term2 -> 
        [Char]
-> ([Values Funcons] -> [Values Funcons] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop [Char]
"neg. sort annotation" (\[Values Funcons]
a [Values Funcons]
b -> [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple [Values Funcons]
a [Values Funcons]
b Rewrite Bool -> (Bool -> Rewrite Bool) -> Rewrite Bool
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> Rewrite Bool
forall a. a -> Rewrite a
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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
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 Funcons]
vs, Env
env')        -> [Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons]
vs [VPattern]
vpats Env
env'
            Right (CompTerm Funcons
lf MSOS StepRes
step, Env
env')  -> case [VPattern]
vpats of 
              [VPMetaVar [Char]
v] -> Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Levelled -> Env -> Env
envInsert [Char]
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 [Char]
_)     -> [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 [Char]
var   -> [Char] -> FPattern
PMetaVar [Char]
var 
                      VPattern
value_pat       -> VPattern -> FPattern
PValue VPattern
value_pat
  where prop :: String -> ([Values] -> [Values] -> Rewrite Bool) -> FTerm -> FTerm -> Env -> Rewrite Env
        prop :: [Char]
-> ([Values Funcons] -> [Values Funcons] -> Rewrite Bool)
-> FTerm
-> FTerm
-> Env
-> Rewrite Env
prop [Char]
msg [Values Funcons] -> [Values Funcons] -> Rewrite Bool
op FTerm
term1 FTerm
term2 Env
env = do
            ([Values Funcons]
vs1,Env
env1) <- FTerm -> Env -> Rewrite ([Values Funcons], Env)
subsAndRewritesToValuesInEnv FTerm
term1 Env
env
            ([Values Funcons]
vs2,Env
env2) <- FTerm -> Env -> Rewrite ([Values Funcons], Env)
subsAndRewritesToValuesInEnv FTerm
term2 Env
env1
            Bool
b <- [Values Funcons] -> [Values Funcons] -> Rewrite Bool
op [Values Funcons]
vs1 [Values Funcons]
vs2
            if Bool
b then Env -> Rewrite Env
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Env
env2
                 else IE -> Rewrite Env
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
SideCondFail ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" fails with " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Values Funcons] -> [Char]
showValuesSeq [Values Funcons]
vs1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" and " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Values Funcons] -> [Char]
showValuesSeq [Values Funcons]
vs2))
        lift :: (t -> t -> a) -> t -> t -> m a
lift t -> t -> a
op t
xs t
ys = a -> m a
forall a. 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 [Char]
Nothing, Maybe SeqSortOp
_, FTerm
kind)  = VPattern -> FTerm -> VPattern
VPAnnotated VPattern
VPWildCard FTerm
kind
               mkPattern (Just [Char]
var, Maybe SeqSortOp
Nothing, FTerm
kind) = VPattern -> FTerm -> VPattern
VPAnnotated ([Char] -> VPattern
VPMetaVar [Char]
var) FTerm
kind
               mkPattern (Just [Char]
var, Just SeqSortOp
op, FTerm
kind) = VPattern -> FTerm -> VPattern
VPAnnotated ([Char] -> SeqSortOp -> VPattern
VPSeqVar [Char]
var SeqSortOp
op) FTerm
kind
    in [Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch ((ComputationTypes -> Values Funcons)
-> [ComputationTypes] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map ComputationTypes -> Values Funcons
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 a. a -> Rewrite a
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 a. a -> Rewrite a
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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
  ValTerm [Values Funcons
v]   -> Values Funcons -> Maybe FTerm -> Env -> Rewrite Bool
isInMaybeTermType Values Funcons
v (FTerm -> Maybe FTerm
forall a. a -> Maybe a
Just FTerm
term) Env
env Rewrite Bool
-> (Bool -> Rewrite (Maybe [Funcons])) -> Rewrite (Maybe [Funcons])
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                      Bool
True  -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Funcons] -> Maybe [Funcons]
forall a. a -> Maybe a
Just [Values Funcons -> Funcons
FValue Values Funcons
v])
                      Bool
_     -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Funcons]
forall a. Maybe a
Nothing
  ValTerm [Values Funcons]
vs    -> [Values Funcons] -> FTerm -> Env -> Rewrite Bool
isInMaybeTupleType [Values Funcons]
vs FTerm
term Env
env Rewrite Bool
-> (Bool -> Rewrite (Maybe [Funcons])) -> Rewrite (Maybe [Funcons])
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                      Bool
True  -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Funcons] -> Maybe [Funcons]
forall a. a -> Maybe a
Just ((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs))
                      Bool
_     -> Maybe [Funcons] -> Rewrite (Maybe [Funcons])
forall a. a -> Rewrite a
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 a. a -> Rewrite a
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 Funcons
-> Maybe FTerm -> Env -> Rewrite (Maybe [Values Funcons])
isInMaybeTermTypePreserve Values Funcons
v Maybe FTerm
mty Env
env = Values Funcons -> Maybe FTerm -> Env -> Rewrite Bool
isInMaybeTermType Values Funcons
v Maybe FTerm
mty Env
env Rewrite Bool
-> (Bool -> Rewrite (Maybe [Values Funcons]))
-> Rewrite (Maybe [Values Funcons])
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Bool
True  -> Maybe [Values Funcons] -> Rewrite (Maybe [Values Funcons])
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> Maybe [Values Funcons]
forall a. a -> Maybe a
Just [Values Funcons
v])
  Bool
_     -> Maybe [Values Funcons] -> Rewrite (Maybe [Values Funcons])
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [Values Funcons]
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 a. a -> Rewrite a
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 Funcons -> Maybe FTerm -> Env -> Rewrite Bool
isInMaybeTermType Values Funcons
v Maybe FTerm
Nothing Env
_ = Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isInMaybeTermType Values Funcons
v (Just FTerm
term) Env
env = 
    FTerm -> Env -> Rewrite (Values Funcons)
subsAndRewritesToValue FTerm
term Env
env Rewrite (Values Funcons)
-> (Values Funcons -> Rewrite Bool) -> Rewrite Bool
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Values Funcons -> Values Funcons -> Rewrite Bool
isIn Values Funcons
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 Funcons] -> FTerm -> Env -> Rewrite Bool
isInMaybeTupleType [Values Funcons]
vs FTerm
term Env
env = 
  FTerm -> Env -> Rewrite (Values Funcons)
subsAndRewritesToValue FTerm
term Env
env Rewrite (Values Funcons)
-> (Values Funcons -> Rewrite Bool) -> Rewrite Bool
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple [Values Funcons]
vs ([Values Funcons] -> Rewrite Bool)
-> (Values Funcons -> [Values Funcons])
-> Values Funcons
-> Rewrite Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values Funcons -> [Values Funcons] -> [Values Funcons]
forall a. a -> [a] -> [a]
:[])

isInTuple :: [Values] -> [Values] -> Rewrite Bool
isInTuple :: [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple [Values Funcons]
vs [Values Funcons]
mtys = case [Maybe (Types Funcons)] -> Maybe [Types Funcons]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ((Values Funcons -> Maybe (Types Funcons))
-> [Values Funcons] -> [Maybe (Types Funcons)]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Maybe (Types Funcons)
forall t. HasValues t => Values t -> Maybe (Types t)
castType [Values Funcons]
mtys) of
  Maybe [Types Funcons]
Nothing  -> Funcons -> [Char] -> Rewrite Bool
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Values Funcons -> Funcons
FValue (Values Funcons -> Funcons) -> Values Funcons -> Funcons
forall a b. (a -> b) -> a -> b
$ Name -> [Funcons] -> Values Funcons
forall t. Name -> [t] -> Values t
ADTVal Name
"" ((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
mtys)) 
                [Char]
"rhs of annotation is not a type"
  Just [Types Funcons]
tys -> [Values Funcons] -> [TTParam] -> Rewrite Bool
Funcons.Patterns.isInTupleType [Values Funcons]
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 Funcons -> Values Funcons -> Rewrite Bool
isIn Values Funcons
v Values Funcons
mty = case Values Funcons -> Maybe (Types Funcons)
forall t. HasValues t => Values t -> Maybe (Types t)
castType Values Funcons
mty of
    Maybe (Types Funcons)
Nothing -> Funcons -> [Char] -> Rewrite Bool
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Values Funcons -> Funcons
FValue Values Funcons
mty) [Char]
"rhs of annotation is not a type"
    Just Types Funcons
ty -> Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
v Types Funcons
ty
  
isInType :: Values -> Types -> Rewrite Bool
isInType :: Values Funcons -> Types Funcons -> Rewrite Bool
isInType Values Funcons
v (ADT Name
"ground-values" []) = Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (Values Funcons -> Bool
forall t. HasValues t => Values t -> Bool
isGround Values Funcons
v)
isInType Values Funcons
v (ADT Name
"maps" [Funcons
kt', Funcons
vt']) = case Values Funcons
v of
  Map ValueMaps (Values Funcons)
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)
forall (m :: * -> *) a. Monad m => [m a] -> m [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 Funcons -> Rewrite Bool)
-> [Values Funcons] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Values Funcons -> Types Funcons -> Rewrite Bool)
-> Types Funcons -> Values Funcons -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
kt) (ValueMaps (Values Funcons) -> [Values Funcons]
forall k a. Map k a -> [k]
M.keys ValueMaps (Values Funcons)
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 Funcons] -> Rewrite Bool)
-> [[Values Funcons]] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (([Values Funcons] -> [TTParam] -> Rewrite Bool)
-> [TTParam] -> [Values Funcons] -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Values Funcons] -> [TTParam] -> Rewrite Bool
Funcons.Patterns.isInTupleType [Types Funcons -> TTParam
forall {t}. Types t -> (Types t, Maybe SeqSortOp)
paramFromType Types Funcons
vt]) (ValueMaps (Values Funcons) -> [[Values Funcons]]
forall k a. Map k a -> [a]
M.elems ValueMaps (Values Funcons)
m)]
  Values Funcons
_ -> Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isInType Values Funcons
v (ADT Name
"multisets" [Funcons
ty']) = case Values Funcons
v of
  Multiset MultiSet (Values Funcons)
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 Funcons -> Rewrite Bool)
-> [Values Funcons] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Values Funcons -> Types Funcons -> Rewrite Bool)
-> Types Funcons -> Values Funcons -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
ty) (MultiSet (Values Funcons) -> [Values Funcons]
forall a. MultiSet a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList MultiSet (Values Funcons)
ls)
  Values Funcons
_ -> Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isInType Values Funcons
v (ADT Name
"sets" [Funcons
ty']) = case Values Funcons
v of
  Set ValueSets (Values Funcons)
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 Funcons -> Rewrite Bool)
-> [Values Funcons] -> Rewrite [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Values Funcons -> Types Funcons -> Rewrite Bool)
-> Types Funcons -> Values Funcons -> Rewrite Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
ty) (ValueSets (Values Funcons) -> [Values Funcons]
forall a. Set a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ValueSets (Values Funcons)
ls)
  Values Funcons
_ -> Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
-- characters
isInType Values Funcons
v Types Funcons
AsciiCharacters = Values Funcons -> Name -> Rewrite Bool
isInUnicodeType Values Funcons
v Name
"ascii-points"
isInType Values Funcons
v Types Funcons
ISOLatinCharacters = Values Funcons -> Name -> Rewrite Bool
isInUnicodeType Values Funcons
v Name
"iso-latin-1-points"
isInType Values Funcons
v Types Funcons
BMPCharacters = Values Funcons -> Name -> Rewrite Bool
isInUnicodeType Values Funcons
v Name
"basic-multilingual-plane-points"
-- type operators and datatypes
isInType Values Funcons
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 Funcons)
subsAndRewritesToValue FTerm
ty_term Env
env Rewrite (Values Funcons)
-> (Values Funcons -> Rewrite Bool) -> Rewrite Bool
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Values Funcons -> Values Funcons -> Rewrite Bool
isIn Values Funcons
v 
       isInAlt [TPattern]
tpats (DataTypeMemberConstructor Name
cons [FTerm]
ty_terms Maybe [TPattern]
mtpats)
        | ADTVal Name
cons' [Funcons]
args <- Values Funcons
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 Funcons])
-> [FTerm] -> Rewrite [[Values Funcons]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((FTerm -> Env -> Rewrite [Values Funcons])
-> Env -> FTerm -> Rewrite [Values Funcons]
forall a b c. (a -> b -> c) -> b -> a -> c
flip FTerm -> Env -> Rewrite [Values Funcons]
subsAndRewritesToValues Env
env) [FTerm]
ty_terms Rewrite [[Values Funcons]]
-> ([[Values Funcons]] -> Rewrite Bool) -> Rewrite Bool
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
                        [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple ((Funcons -> Values Funcons) -> [Funcons] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values Funcons
downcastValue [Funcons]
args) ([Values Funcons] -> Rewrite Bool)
-> ([[Values Funcons]] -> [Values Funcons])
-> [[Values Funcons]]
-> Rewrite Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Values Funcons]] -> [Values Funcons]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            Bool
_     -> Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- imprecision
       isInAlt [TPattern]
_ DataTypeAltt
_ = Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isInType Values Funcons
v (AnnotatedType Types Funcons
ty SeqSortOp
op) = [Values Funcons] -> [TTParam] -> Rewrite Bool
Funcons.Patterns.isInTupleType [Values Funcons
v] [(Types Funcons
ty, SeqSortOp -> Maybe SeqSortOp
forall a. a -> Maybe a
Just SeqSortOp
op)] 
isInType Values Funcons
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 Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
v Types Funcons
ty1 Rewrite (Bool -> Bool) -> Rewrite Bool -> Rewrite Bool
forall a b. Rewrite (a -> b) -> Rewrite a -> Rewrite b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
v Types Funcons
ty2
isInType Values Funcons
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 Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
v Types Funcons
ty1 Rewrite (Bool -> Bool) -> Rewrite Bool -> Rewrite Bool
forall a b. Rewrite (a -> b) -> Rewrite a -> Rewrite b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
v Types Funcons
ty2
isInType Values Funcons
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 Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
v Types Funcons
t
isInType Values Funcons
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 a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (Values Funcons -> Types Funcons -> Maybe Bool
forall t. HasValues t => Values t -> Types t -> Maybe Bool
Funcons.Types.isInType Values Funcons
v Types Funcons
t)

isInUnicodeType :: Values Funcons -> Name -> Rewrite Bool
isInUnicodeType v :: Values Funcons
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 Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
v Types Funcons
forall t. Types t
UnicodeCharacters
  Values Funcons
point     <- Funcons -> Rewrite (Values Funcons)
rewritesToValue Funcons
p
  Bool
inRange   <- Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Values Funcons
point Types Funcons
rangeTy 
  Bool -> Rewrite Bool
forall a. a -> Rewrite a
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 Funcons
_ Name
_ = Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False


isInTupleType :: [Values] -> [TTParam] -> Rewrite Bool
isInTupleType :: [Values Funcons] -> [TTParam] -> Rewrite Bool
isInTupleType [Values Funcons]
vs [TTParam]
ttparams = 
    Rewrite Env -> Rewrite (Either IException Env)
forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch ([Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons]
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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Env
env' -> Bool -> Rewrite Bool
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Left (Funcons
_,Funcons
_,PatternMismatch [Char]
_) -> Bool -> Rewrite Bool
forall a. a -> Rewrite a
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 -> [Char] -> VPattern
VPMetaVar [Char]
"Dummy"
                                Just SeqSortOp
op -> [Char] -> SeqSortOp -> VPattern
VPSeqVar [Char]
"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([Char] -> IE
Internal ([Char]
"type lookup failed: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
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 Funcons] -> Rewrite Rewritten
rewriteType Name
nm [Values Funcons]
vs = Values Funcons -> Rewrite Rewritten
rewritten (ComputationTypes -> Values Funcons
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 -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
forall t. HasValues t => Values t -> t
inject [Values Funcons]
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 [Char]
var      -> [Char] -> FTerm
TVar [Char]
var
  PSeqVar [Char]
var SeqSortOp
_     -> [Char] -> FTerm
TVar [Char]
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 Funcons
lit         -> Funcons -> FTerm
TFuncon (Funcons -> FTerm) -> Funcons -> FTerm
forall a b. (a -> b) -> a -> b
$ (Values Funcons -> Funcons
FValue Values Funcons
lit) 
  VPattern
VPEmptySet        -> Funcons -> FTerm
TFuncon (Funcons -> FTerm) -> Funcons -> FTerm
forall a b. (a -> b) -> a -> b
$ (Values Funcons -> Funcons
FValue ([Values Funcons] -> Values Funcons
set__ []))
  VPattern
VPWildCard        -> FTerm
TAny
--  PList pats        -> TList (map vpat2term pats)
  VPMetaVar [Char]
var     -> [Char] -> FTerm
TVar [Char]
var
  VPSeqVar [Char]
var SeqSortOp
_    -> [Char] -> FTerm
TVar [Char]
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 [Char]
var           -> [Char] -> FTerm
TVar [Char]
var
  TPSeqVar [Char]
var SeqSortOp
_      -> [Char] -> FTerm
TVar [Char]
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)