{-# 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
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
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
Just FTerm
_ -> forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> a -> Ordering
compare
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
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
((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])
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
data VPattern = PADT Name [VPattern]
| VPWildCard
| 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 VPattern
VPEmptySet = forall a. Maybe a
Nothing
v2tPattern (VPAnnotated VPattern
fp FTerm
t) = forall a. Maybe a
Nothing
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
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
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
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
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
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
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'
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
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
| 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
fMatch Funcons
f pat :: FPattern
pat@(PSeqVar [Char]
_ SeqSortOp
_) Env
env = [Funcons] -> [FPattern] -> Env -> Rewrite Env
fsMatch [Funcons
f] [FPattern
pat] Env
env
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
([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
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
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
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
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
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
data SideCondition
= SCEquality FTerm FTerm
| SCInequality FTerm FTerm
| SCIsInSort FTerm FTerm
| SCNotInSort FTerm FTerm
| SCPatternMatch FTerm [VPattern]
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
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
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)
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
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])
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
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
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"
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
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
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)
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
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)