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

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 :: 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 forall a. Int -> [a] -> [a]
drop Int
k [a]
str of
    []  -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    a
f:[a]
_ -> forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch (a -> b -> Env -> Rewrite Env
p a
f b
pat Env
env) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            Left IException
ie | IException -> Bool
failsRule IException
ie  -> forall (m :: * -> *) a. Monad m => a -> m a
return []
                    | Bool
otherwise     -> forall a. IException -> Rewrite a
rewrite_rethrow IException
ie
            Right Env
env'              -> forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
kforall 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 ((forall a. Ord a => a -> a -> Bool
<=Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length)
    SeqSortOp
PlusOp         -> case [a]
str of  
                        [] -> forall (m :: * -> *) a. Monad m => a -> m a
return []
                        [a]
_  -> ([[a]] -> Bool) -> Rewrite [(Int, Env)]
makeResults ((forall a. Ord a => a -> a -> Bool
>=Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length)
    SeqSortOp
StarOp         -> ([[a]] -> Bool) -> Rewrite [(Int, Env)]
makeResults (forall a b. a -> b -> a
const Bool
True)
    where makeResults :: ([[a]] -> Bool) -> Rewrite [(Int, Env)]
makeResults [[a]] -> Bool
filter_op = do
            [[a]]
furthest <- 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) (forall a. Int -> [a] -> [a]
drop Int
k [a]
str)
            forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Env)] -> [(Int, Env)]
sortWithPref forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {t :: * -> *}. Foldable t => t [a] -> (Int, Env)
ins (forall a. (a -> Bool) -> [a] -> [a]
filter [[a]] -> Bool
filter_op forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]]
ordered_subsequences [[a]]
furthest))
            where
              ins :: t [a] -> (Int, Env)
ins t [a]
fs  = (Int
kforall a. Num a => a -> a -> a
+forall (t :: * -> *) a. Foldable t => t a -> Int
length t [a]
fs, [Char] -> Levelled -> Env -> Env
envInsert [Char]
var ([a] -> Levelled
level (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])
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
              takeWhileM a -> Rewrite (Maybe [a])
p (a
x:[a]
xs) = forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch (a -> Rewrite (Maybe [a])
p a
x) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                Right (Just [a]
fs)     -> ([a]
fs forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Rewrite (Maybe [a])) -> [a] -> Rewrite [[a]]
takeWhileM a -> Rewrite (Maybe [a])
p [a]
xs
                Right Maybe [a]
Nothing       -> forall (m :: * -> *) a. Monad m => a -> m a
return []
                Left IException
ie | IException -> Bool
failsRule IException
ie  -> forall (m :: * -> *) a. Monad m => a -> m a
return []
                        | Bool
otherwise     -> 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 = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int -> Int -> Ordering
comparison forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
                where comparison :: Int -> Int -> Ordering
comparison = case Maybe FTerm
mty of
                        Maybe FTerm
Nothing   -> forall a. Ord a => a -> a -> Ordering
compare      -- no annotation => shortest match
                        Just  FTerm
_   -> forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 <- forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Matcher a -> Matcher a -> Matcher a
seqWith 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: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," (forall a b. (a -> b) -> [a] -> [b]
map a -> [Char]
show [a]
str) forall a. [a] -> [a] -> [a]
++ [Char]
" does not match " forall a. [a] -> [a] -> [a]
++ [Char]
pats)
    case [(Int, Env)]
matches of
        [] -> forall a. IE -> Rewrite a
rewrite_throw IE
rule_fail
        [(Int
_,Env
env')] -> forall (m :: * -> *) a. Monad m => a -> m a
return Env
env'
        [(Int, Env)]
_  -> forall a. [Char] -> Rewrite a
internal ([Char]
"ambiguity not resolved") 
    where   m :: Int
m = 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 forall a. Eq a => a -> a -> Bool
== Int
m       = forall (m :: * -> *) a. Monad m => a -> m a
return [(Int
k,Env
env)]
                                | Bool
otherwise    = 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 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 [] = 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) <- 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)]
_   -> 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 = 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 forall a. a -> [a] -> [a]
: [a] -> [a] -> [[a]]
ordered_subsequences' [a]
xs ([a]
accforall 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 -> ShowS
[FPattern] -> ShowS
FPattern -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [FPattern] -> ShowS
$cshowList :: [FPattern] -> ShowS
show :: FPattern -> [Char]
$cshow :: FPattern -> [Char]
showsPrec :: Int -> FPattern -> ShowS
$cshowsPrec :: Int -> FPattern -> ShowS
Show, FPattern -> FPattern -> Bool
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
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
Ord, ReadPrec [FPattern]
ReadPrec FPattern
Int -> ReadS FPattern
ReadS [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 [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 -> ShowS
[VPattern] -> ShowS
VPattern -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [VPattern] -> ShowS
$cshowList :: [VPattern] -> ShowS
show :: VPattern -> [Char]
$cshow :: VPattern -> [Char]
showsPrec :: Int -> VPattern -> ShowS
$cshowsPrec :: Int -> VPattern -> ShowS
Show, VPattern -> VPattern -> Bool
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
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
Ord, ReadPrec [VPattern]
ReadPrec VPattern
Int -> ReadS VPattern
ReadS [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) = forall a. a -> Maybe a
Just TPattern
t
v2tPattern (VPMetaVar [Char]
var) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Char] -> TPattern
TPVar [Char]
var
v2tPattern (VPSeqVar [Char]
var SeqSortOp
op) = forall a. a -> Maybe a
Just 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 Funcons
lit) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ FTerm -> TPattern
TPLit (Funcons -> FTerm
TFuncon (Values Funcons -> Funcons
FValue Values Funcons
lit))
v2tPattern VPattern
VPWildCard = forall a. a -> Maybe a
Just TPattern
TPWildCard
--v2tPattern (PList _) = Nothing 
v2tPattern VPattern
VPEmptySet = forall a. Maybe a
Nothing 
v2tPattern (VPAnnotated VPattern
fp FTerm
t) = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [VPattern] -> Env -> Rewrite [VPattern]
subs_flatten [VPattern]
vpats Env
env
  VPattern
VPWildCard      -> forall (m :: * -> *) a. Monad m => a -> m a
return VPattern
VPWildCard
  VPattern
VPEmptySet      -> forall (m :: * -> *) a. Monad m => a -> m a
return VPattern
VPEmptySet
--  PList pats      -> PList <$> subs_flatten pats env
  VPMetaVar [Char]
var   -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
var Env
env of
                      Maybe Levelled
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> VPattern
VPMetaVar [Char]
var)
                      Just Levelled
v  -> Values Funcons -> VPattern
VPLit 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VPattern -> Env -> Rewrite VPattern
substitute_patt_signal VPattern
vpat Env
env 
                                       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return FTerm
ann 
  VPSeqVar [Char]
var SeqSortOp
op -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
var Env
env of
                      Maybe Levelled
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> SeqSortOp -> VPattern
VPSeqVar [Char]
var SeqSortOp
op)
                      Just Levelled
v  -> Values Funcons -> VPattern
VPLit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Levelled -> Rewrite (Values Funcons)
vLevel Levelled
v 
  VPLit Values Funcons
lit       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Values Funcons -> VPattern
VPLit Values Funcons
lit
  VPType TPattern
tpat     -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 = (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [VPattern]
terms 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                 -> (forall a. a -> [a] -> [a]
:[]) 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 forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup [Char]
k Env
env of
                            Maybe Levelled
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return [VPattern
vpat]
                            Just Levelled
lf -> forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> VPattern
VPLit 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 = forall a. Rewrite a -> MSOS a
liftRewrite 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 
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {t}. Values t -> Bool
isSort_ [Values Funcons]
str 
  , Just [TPattern]
tpats <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map VPattern -> Maybe TPattern
v2tPattern [VPattern]
pats)
        = [ComputationTypes] -> [TPattern] -> Env -> Rewrite Env
tsMatch (forall a b. (a -> b) -> [a] -> [b]
map (Funcons -> ComputationTypes
downcastSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values Funcons -> Funcons
FValue) [Values Funcons]
str) [TPattern]
tpats Env
env 
  | Bool
otherwise = forall a.
[Char] -> (a -> [Char]) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching (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 = 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   -> 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     -> 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 = forall a. Rewrite a -> MSOS a
liftRewrite (FTerm -> Env -> Rewrite (Rewritten, Env)
subsAndRewritesInEnv FTerm
x Env
env) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  (ValTerm [Values Funcons]
v, Env
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 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'   -> forall a. Rewrite a -> MSOS a
liftRewrite forall a b. (a -> b) -> a -> b
$ [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons
f'] [FPattern]
pats Env
env'
                  Right [Values Funcons]
vs' -> forall a. Rewrite a -> MSOS a
liftRewrite forall a b. (a -> b) -> a -> b
$ [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch (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 = forall a. Rewrite a -> MSOS a
liftRewrite 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
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
notforall b c a. (b -> c) -> (a -> b) -> a -> c
.Funcons -> Bool
hasStep) [Funcons]
str = 
          let downValues :: [Funcons] -> [Values Funcons]
downValues [Funcons]
vs = 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) (forall a b. (a -> b) -> [a] -> [b]
map FPattern -> VPattern
f2vPattern [FPattern]
pats) Env
env
    | Bool
otherwise = forall a.
[Char] -> (a -> [Char]) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching (forall a. Show a => a -> [Char]
show [FPattern]
pats) Funcons -> [Char]
showFuncons [Funcons]
str [Matcher Funcons]
matchers Env
env
    where   matchers :: [Matcher Funcons]
matchers = 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   -> 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     -> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
fMatch Funcons
f (PMetaVar [Char]
var) Env
env = forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Levelled -> Env -> Env
envInsert [Char]
var (Funcons -> Maybe (MSOS StepRes) -> Levelled
FunconTerm Funcons
f 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 = forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"pattern annotation check failed: " forall a. [a] -> [a] -> [a]
++ [Values Funcons] -> [Char]
showValuesSeq [Values Funcons]
tys))
    Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f 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 forall {a}. Rewrite a
fail
        Rewritten
otherwise   -> 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 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
_ -> forall a. IE -> Rewrite a
rewrite_throw --important, should remain last 
                ([Char] -> IE
PatternMismatch ([Char]
"could not rewrite to value: " 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 = forall a. Rewrite a -> MSOS a
liftRewrite 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 = 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 = 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 = forall a. Rewrite a -> MSOS a
liftRewrite 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 = 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 = 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 = forall a. Rewrite a -> MSOS a
liftRewrite 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)forall a. a -> [a] -> [a]
:[Funcons]
vs) [VPattern]
pats Env
env
vMatch Values Funcons
_ (VPattern
VPWildCard) Env
env = forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch (Set ValueSets (Values Funcons)
s) VPattern
VPEmptySet Env
env | forall (t :: * -> *) a. Foldable t => t a -> Bool
null ValueSets (Values Funcons)
s = forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch (Map ValueMaps (Values Funcons)
m) VPattern
VPEmptySet Env
env | forall (t :: * -> *) a. Foldable t => t a -> Bool
null ValueMaps (Values Funcons)
m = forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch Values Funcons
VAny VPattern
_ Env
env = forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
vMatch Values Funcons
v (VPMetaVar [Char]
var) Env
env = 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 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 -> forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"pattern annotation check failed: " 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 forall a. Eq a => a -> a -> Bool
== Values Funcons
v2 = 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
_ = 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 = forall a.
[Char] -> (a -> [Char]) -> [a] -> [Matcher a] -> Env -> Rewrite Env
matching (forall a. Show a => a -> [Char]
show [TPattern]
pats) ComputationTypes -> [Char]
showSorts [ComputationTypes]
str [Matcher ComputationTypes]
matchers Env
env
        where   matchers :: [Matcher ComputationTypes]
matchers = 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 -> forall a b. (a -> b -> Env -> Rewrite Env) -> b -> Matcher a
singleMatcher ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch TPattern
pat 
                  Just SeqVarInfo
info -> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Env
env
  TPVar [Char]
x -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    ComputationType ComputationTypes
ty ->   
      if ComputationTypes
t forall a. Eq a => a -> a -> Bool
== ComputationTypes
ty then forall (m :: * -> *) a. Monad m => a -> m a
return Env
env 
                 else forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"failed to match"))
    Values Funcons
_ -> 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 (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 (forall t. Types t -> ComputationTypes t
Type Types Funcons
ft) TPattern
fp Env
env forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ComputationTypes -> TPattern -> Env -> Rewrite Env
tMatch (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 forall a. Eq a => a -> a -> Bool
== Name
nm' ->
    [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
ts (forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue 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
_ -> 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 forall a. Eq a => a -> a -> Bool
/= Name
pat_con = forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PatternMismatch ([Char]
"failed to match constructors: (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Name
con,Name
pat_con) forall a. [a] -> [a] -> [a]
++ [Char]
")"))
    | Bool
otherwise = [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
vs (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) = forall a. a -> Maybe a
Just ([Char]
var, SeqSortOp
op, forall a. Maybe a
Nothing)
fpSeqVarInfo (PAnnotated (PSeqVar [Char]
var SeqSortOp
op) FTerm
term) = forall a. a -> Maybe a
Just ([Char]
var, SeqSortOp
op, forall a. a -> Maybe a
Just FTerm
term)
fpSeqVarInfo FPattern
_ = forall a. Maybe a
Nothing

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

tpSeqVarInfo :: TPattern -> Maybe SeqVarInfo
tpSeqVarInfo :: TPattern -> Maybe SeqVarInfo
tpSeqVarInfo (TPSeqVar [Char]
var SeqSortOp
op) = forall a. a -> Maybe a
Just ([Char]
var, SeqSortOp
op, forall a. Maybe a
Nothing)
tpSeqVarInfo TPattern
_ = 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 = forall a. Rewrite a -> MSOS a
liftRewrite 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" (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" (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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not) FTerm
term1 FTerm
term2 Env
env
    SCPatternMatch FTerm
term [VPattern]
vpats -> 
      forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch (FTerm -> Env -> Rewrite (Rewritten, Env)
subsAndRewritesInEnv FTerm
term Env
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 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] -> forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Levelled -> Env -> Env
envInsert [Char]
v (Funcons -> Maybe (MSOS StepRes) -> Levelled
FunconTerm Funcons
lf (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                     -> forall a. IException -> Rewrite a
rewrite_rethrow IException
ie
      where pats :: [FPattern]
pats = 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 forall (m :: * -> *) a. Monad m => a -> m a
return Env
env2
                 else forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
SideCondFail ([Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
" fails with " forall a. [a] -> [a] -> [a]
++ [Values Funcons] -> [Char]
showValuesSeq [Values Funcons]
vs1 forall a. [a] -> [a] -> [a]
++ [Char]
" and " 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 = 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 = 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 (forall a b. (a -> b) -> [a] -> [b]
map forall t. ComputationTypes t -> Values t
ComputationType [ComputationTypes]
tys) [VPattern]
param_pats 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
_ = 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just [Funcons
f])
rewritesToAnnotatedType Funcons
f (Just FTerm
term) Env
env = Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f 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 (forall a. a -> Maybe a
Just FTerm
term) Env
env forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                      Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just [Values Funcons -> Funcons
FValue Values Funcons
v])
                      Bool
_     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  ValTerm [Values Funcons]
vs    -> [Values Funcons] -> FTerm -> Env -> Rewrite Bool
isInMaybeTupleType [Values Funcons]
vs FTerm
term Env
env forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                      Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs))
                      Bool
_     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  CompTerm Funcons
_  MSOS StepRes
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Bool
True  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just [Values Funcons
v])
  Bool
_     -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return (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
_ = 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 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple [Values Funcons]
vs forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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 forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (forall a b. (a -> b) -> [a] -> [b]
map forall t. HasValues t => Values t -> Maybe (Types t)
castType [Values Funcons]
mtys) of
  Maybe [Types Funcons]
Nothing  -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Values Funcons -> Funcons
FValue forall a b. (a -> b) -> a -> b
$ forall t. Name -> [t] -> Values t
ADTVal Name
"" (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 (forall a b. (a -> b) -> [a] -> [b]
map 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, forall a. a -> Maybe a
Just SeqSortOp
op)
paramFromType Types t
ty = (Types t
ty, 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 forall t. HasValues t => Values t -> Maybe (Types t)
castType Values Funcons
mty of
    Maybe (Types Funcons)
Nothing -> 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" []) = forall (m :: * -> *) a. Monad m => a -> m a
return (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'
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence 
          [forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
kt) (forall k a. Map k a -> [k]
M.keys ValueMaps (Values Funcons)
m)
          ,forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip [Values Funcons] -> [TTParam] -> Rewrite Bool
Funcons.Patterns.isInTupleType [forall {t}. Types t -> (Types t, Maybe SeqSortOp)
paramFromType Types Funcons
vt]) (forall k a. Map k a -> [a]
M.elems ValueMaps (Values Funcons)
m)]
  Values Funcons
_ -> 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' 
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
ty) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList MultiSet (Values Funcons)
ls)
  Values Funcons
_ -> 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' 
    forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip Values Funcons -> Types Funcons -> Rewrite Bool
Funcons.Patterns.isInType Types Funcons
ty) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ValueSets (Values Funcons)
ls)
  Values Funcons
_ -> 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
    forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPattern -> VPattern
VPType) [TPattern]
tpats) forall {k} {a}. Map k a
emptyEnv
            FTerm -> Env -> Rewrite (Values Funcons)
subsAndRewritesToValue FTerm
ty_term Env
env 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' 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 (forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPattern -> VPattern
VPType) [TPattern]
tpats) forall {k} {a}. Map k a
emptyEnv
                  Maybe [TPattern]
Nothing    -> [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons]
tys (forall a b. (a -> b) -> [a] -> [b]
map (VPattern -> FPattern
PValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPattern -> VPattern
VPType) [TPattern]
tpats) forall {k} {a}. Map k a
emptyEnv
          case forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
notforall b c a. (b -> c) -> (a -> b) -> a -> c
.Funcons -> Bool
hasStep) [Funcons]
args of 
            Bool
True  -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> b -> a -> c
flip FTerm -> Env -> Rewrite [Values Funcons]
subsAndRewritesToValues Env
env) [FTerm]
ty_terms forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
                        [Values Funcons] -> [Values Funcons] -> Rewrite Bool
isInTuple (forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values Funcons
downcastValue [Funcons]
args) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
            Bool
_     -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True -- imprecision
       isInAlt [TPattern]
_ DataTypeAltt
_ = 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, forall a. a -> Maybe a
Just SeqSortOp
op)] 
isInType Values Funcons
v (Union Types Funcons
ty1 Types Funcons
ty2) = 
  Bool -> 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 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
(&&) 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 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 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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) forall (m :: * -> *) a. Monad m => a -> m a
return (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 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 
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
isUnicode,Bool
inRange])
isInUnicodeType Values Funcons
_ Name
_ = 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 = 
    forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch ([Values Funcons] -> [VPattern] -> Env -> Rewrite Env
vsMatch [Values Funcons]
vs (forall a b. (a -> b) -> [a] -> [b]
map TTParam -> VPattern
mkPattern [TTParam]
ttparams) forall {k} {a}. Map k a
emptyEnv) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Right Env
env' -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Left (Funcons
_,Funcons
_,PatternMismatch [Char]
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
        Left IException
ie -> 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 = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite 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 -> (forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception([Char] -> IE
Internal ([Char]
"type lookup failed: " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
con)) RewriteReader
ctxt)
                        , RewriteState
st, forall a. Monoid a => a
mempty)
      Just DataTypeMembers
members -> (forall a b. b -> Either a b
Right DataTypeMembers
members, RewriteState
st, 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 (forall t. ComputationTypes t -> Values t
ComputationType(forall t. Types t -> ComputationTypes t
Type(forall t. Name -> [t] -> Types t
ADT Name
nm (forall a b. (a -> b) -> [a] -> [b]
map 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 (forall a b. (a -> b) -> [a] -> [b]
map VPattern -> FTerm
vpat2term [VPattern]
pats)
  VPLit Values Funcons
lit         -> Funcons -> FTerm
TFuncon forall a b. (a -> b) -> a -> b
$ (Values Funcons -> Funcons
FValue Values Funcons
lit) 
  VPattern
VPEmptySet        -> Funcons -> FTerm
TFuncon 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 (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)