module GF.Grammar.PatternMatch (
matchPattern,
testOvershadow,
findMatch,
measurePatt
) where
import GF.Data.Operations
import GF.Grammar.Grammar
import GF.Infra.Ident
import GF.Grammar.Macros
import Control.Monad
import GF.Text.Pretty
matchPattern :: ErrorMonad m => [(Patt,rhs)] -> Term -> m (rhs, Substitution)
matchPattern :: [(Patt, rhs)] -> Term -> m (rhs, Substitution)
matchPattern [(Patt, rhs)]
pts Term
term =
if Bool -> Bool
not (Term -> Bool
isInConstantForm Term
term)
then String -> m (rhs, Substitution)
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"variables occur in" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Term -> Doc
forall a. Pretty a => a -> Doc
pp Term
term))
else do
Term
term' <- Term -> m Term
forall (m :: * -> *). ErrorMonad m => Term -> m Term
mkK Term
term
String -> m (rhs, Substitution) -> m (rhs, Substitution)
forall (m :: * -> *) a. ErrorMonad m => String -> m a -> m a
errIn (Doc -> String
forall a. Pretty a => a -> String
render (String
"trying patterns" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
hsep (Char -> [Patt] -> [Doc]
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> [a2] -> [Doc]
punctuate Char
',' (((Patt, rhs) -> Patt) -> [(Patt, rhs)] -> [Patt]
forall a b. (a -> b) -> [a] -> [b]
map (Patt, rhs) -> Patt
forall a b. (a, b) -> a
fst [(Patt, rhs)]
pts)))) (m (rhs, Substitution) -> m (rhs, Substitution))
-> m (rhs, Substitution) -> m (rhs, Substitution)
forall a b. (a -> b) -> a -> b
$
[([Patt], rhs)] -> [Term] -> m (rhs, Substitution)
forall (m :: * -> *) rhs.
ErrorMonad m =>
[([Patt], rhs)] -> [Term] -> m (rhs, Substitution)
findMatch [([Patt
p],rhs
t) | (Patt
p,rhs
t) <- [(Patt, rhs)]
pts] [Term
term']
where
mkK :: Term -> m Term
mkK Term
s = case Term
s of
C Term
_ Term
_ -> do
[String]
s' <- Term -> m [String]
forall (m :: * -> *). ErrorMonad m => Term -> m [String]
getS Term
s
Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Term
K ([String] -> String
unwords [String]
s'))
Term
_ -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
s
getS :: Term -> m [String]
getS Term
s = case Term
s of
K String
w -> [String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return [String
w]
C Term
v Term
w -> ([String] -> [String] -> [String])
-> m [String] -> m [String] -> m [String]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
(++) (Term -> m [String]
getS Term
v) (Term -> m [String]
getS Term
w)
Term
Empty -> [String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Term
_ -> String -> m [String]
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"cannot get string from" String -> Term -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Term
s))
testOvershadow :: ErrorMonad m => [Patt] -> [Term] -> m [Patt]
testOvershadow :: [Patt] -> [Term] -> m [Patt]
testOvershadow [Patt]
pts [Term]
vs = do
let numpts :: [(Patt, Int)]
numpts = [Patt] -> [Int] -> [(Patt, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Patt]
pts [Int
0..]
let cases :: [(Patt, Term)]
cases = [(Patt
p,Int -> Term
EInt Int
i) | (Patt
p,Int
i) <- [(Patt, Int)]
numpts]
[Term]
ts <- (Term -> m Term) -> [Term] -> m [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (((Term, Substitution) -> Term) -> m (Term, Substitution) -> m Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Term, Substitution) -> Term
forall a b. (a, b) -> a
fst (m (Term, Substitution) -> m Term)
-> (Term -> m (Term, Substitution)) -> Term -> m Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Patt, Term)] -> Term -> m (Term, Substitution)
forall (m :: * -> *) rhs.
ErrorMonad m =>
[(Patt, rhs)] -> Term -> m (rhs, Substitution)
matchPattern [(Patt, Term)]
cases) [Term]
vs
[Patt] -> m [Patt]
forall (m :: * -> *) a. Monad m => a -> m a
return [Patt
p | (Patt
p,Int
i) <- [(Patt, Int)]
numpts, Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Int
i [Int
i | EInt Int
i <- [Term]
ts] ]
findMatch :: ErrorMonad m => [([Patt],rhs)] -> [Term] -> m (rhs, Substitution)
findMatch :: [([Patt], rhs)] -> [Term] -> m (rhs, Substitution)
findMatch [([Patt], rhs)]
cases [Term]
terms = case [([Patt], rhs)]
cases of
[] -> String -> m (rhs, Substitution)
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"no applicable case for" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Doc] -> Doc
forall a. Pretty a => [a] -> Doc
hsep (Char -> [Term] -> [Doc]
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> [a2] -> [Doc]
punctuate Char
',' [Term]
terms)))
([Patt]
patts,rhs
_):[([Patt], rhs)]
_ | [Patt] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Patt]
patts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
terms ->
String -> m (rhs, Substitution)
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"wrong number of args for patterns :" String -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Patt] -> Doc
forall a. Pretty a => [a] -> Doc
hsep [Patt]
patts Doc -> String -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+>
String
"cannot take" Doc -> Doc -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> [Term] -> Doc
forall a. Pretty a => [a] -> Doc
hsep [Term]
terms))
([Patt]
patts,rhs
val):[([Patt], rhs)]
cc -> case ((Patt, Term) -> Err Substitution)
-> [(Patt, Term)] -> Err [Substitution]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Patt, Term) -> Err Substitution
tryMatch ([Patt] -> [Term] -> [(Patt, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Patt]
patts [Term]
terms) of
Ok [Substitution]
substs -> (rhs, Substitution) -> m (rhs, Substitution)
forall (m :: * -> *) a. Monad m => a -> m a
return (rhs
val, [Substitution] -> Substitution
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Substitution]
substs)
Err [Substitution]
_ -> [([Patt], rhs)] -> [Term] -> m (rhs, Substitution)
forall (m :: * -> *) rhs.
ErrorMonad m =>
[([Patt], rhs)] -> [Term] -> m (rhs, Substitution)
findMatch [([Patt], rhs)]
cc [Term]
terms
tryMatch :: (Patt, Term) -> Err [(Ident, Term)]
tryMatch :: (Patt, Term) -> Err Substitution
tryMatch (Patt
p,Term
t) = do
([(BindType, Ident)], Term, [Term])
t' <- Term -> Err ([(BindType, Ident)], Term, [Term])
forall (m :: * -> *).
Monad m =>
Term -> m ([(BindType, Ident)], Term, [Term])
termForm Term
t
Patt -> ([(BindType, Ident)], Term, [Term]) -> Err Substitution
forall a. Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p ([(BindType, Ident)], Term, [Term])
t'
where
trym :: Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p ([a], Term, [Term])
t' =
case (Patt
p,([a], Term, [Term])
t') of
(Patt
_,([a]
x,Term
Empty,[Term]
y)) -> Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p ([a]
x,String -> Term
K [],[Term]
y)
(Patt
PW, ([a], Term, [Term])
_) -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
(PV Ident
x,([],K String
s,[])) -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return [(Ident
x,[String] -> Term
words2term (String -> [String]
words String
s))]
(PV Ident
x, ([a], Term, [Term])
_) -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return [(Ident
x,Term
t)]
(PString String
s, ([],K String
i,[])) | String
sString -> String -> Bool
forall a. Eq a => a -> a -> Bool
==String
i -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
(PInt Int
s, ([],EInt Int
i,[])) | Int
sInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
i -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
(PFloat Double
s,([],EFloat Double
i,[])) | Double
sDouble -> Double -> Bool
forall a. Eq a => a -> a -> Bool
==Double
i -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
(PC Ident
p [Patt]
pp, ([], Con Ident
f, [Term]
tt)) |
Ident
p Ident -> Ident -> Bool
`eqStrIdent` Ident
f Bool -> Bool -> Bool
&& [Patt] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Patt]
pp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
tt ->
do [Substitution]
matches <- ((Patt, Term) -> Err Substitution)
-> [(Patt, Term)] -> Err [Substitution]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Patt, Term) -> Err Substitution
tryMatch ([Patt] -> [Term] -> [(Patt, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Patt]
pp [Term]
tt)
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return ([Substitution] -> Substitution
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Substitution]
matches)
(PP (ModuleName
q,Ident
p) [Patt]
pp, ([], QC (ModuleName
r,Ident
f), [Term]
tt)) |
Ident
p Ident -> Ident -> Bool
`eqStrIdent` Ident
f Bool -> Bool -> Bool
&& [Patt] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Patt]
pp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
tt ->
do [Substitution]
matches <- ((Patt, Term) -> Err Substitution)
-> [(Patt, Term)] -> Err [Substitution]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Patt, Term) -> Err Substitution
tryMatch ([Patt] -> [Term] -> [(Patt, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Patt]
pp [Term]
tt)
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return ([Substitution] -> Substitution
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Substitution]
matches)
(PP (ModuleName
q,Ident
p) [Patt]
pp, ([], Q (ModuleName
r,Ident
f), [Term]
tt)) |
Ident
p Ident -> Ident -> Bool
`eqStrIdent` Ident
f Bool -> Bool -> Bool
&& [Patt] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Patt]
pp Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
tt ->
do [Substitution]
matches <- ((Patt, Term) -> Err Substitution)
-> [(Patt, Term)] -> Err [Substitution]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Patt, Term) -> Err Substitution
tryMatch ([Patt] -> [Term] -> [(Patt, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Patt]
pp [Term]
tt)
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return ([Substitution] -> Substitution
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Substitution]
matches)
(PR [(Label, Patt)]
r, ([],R [Assign]
r',[])) |
(Label -> Bool) -> [Label] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Label -> [Label] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Assign -> Label) -> [Assign] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map Assign -> Label
forall a b. (a, b) -> a
fst [Assign]
r') (((Label, Patt) -> Label) -> [(Label, Patt)] -> [Label]
forall a b. (a -> b) -> [a] -> [b]
map (Label, Patt) -> Label
forall a b. (a, b) -> a
fst [(Label, Patt)]
r) ->
do [Substitution]
matches <- ((Patt, Term) -> Err Substitution)
-> [(Patt, Term)] -> Err [Substitution]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Patt, Term) -> Err Substitution
tryMatch
[(Patt
p,(Maybe Term, Term) -> Term
forall a b. (a, b) -> b
snd (Maybe Term, Term)
a) | (Label
l,Patt
p) <- [(Label, Patt)]
r, let Just (Maybe Term, Term)
a = Label -> [Assign] -> Maybe (Maybe Term, Term)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Label
l [Assign]
r']
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return ([Substitution] -> Substitution
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Substitution]
matches)
(PT Term
_ Patt
p',([a], Term, [Term])
_) -> Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p' ([a], Term, [Term])
t'
(PAs Ident
x Patt
p',([],K String
s,[])) -> do
Substitution
subst <- Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p' ([a], Term, [Term])
t'
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution -> Err Substitution)
-> Substitution -> Err Substitution
forall a b. (a -> b) -> a -> b
$ (Ident
x,[String] -> Term
words2term (String -> [String]
words String
s)) (Ident, Term) -> Substitution -> Substitution
forall a. a -> [a] -> [a]
: Substitution
subst
(PAs Ident
x Patt
p',([a], Term, [Term])
_) -> do
Substitution
subst <- Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p' ([a], Term, [Term])
t'
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return (Substitution -> Err Substitution)
-> Substitution -> Err Substitution
forall a b. (a -> b) -> a -> b
$ (Ident
x,Term
t) (Ident, Term) -> Substitution -> Substitution
forall a. a -> [a] -> [a]
: Substitution
subst
(PAlt Patt
p1 Patt
p2,([a], Term, [Term])
_) -> [Err Substitution] -> Err Substitution
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p1 ([a], Term, [Term])
t', Patt -> ([a], Term, [Term]) -> Err Substitution
trym Patt
p2 ([a], Term, [Term])
t']
(PNeg Patt
p',([a], Term, [Term])
_) -> case (Patt, Term) -> Err Substitution
tryMatch (Patt
p',Term
t) of
Bad String
_ -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
Err Substitution
_ -> String -> Err Substitution
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"no match with negative pattern" String -> Patt -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Patt
p))
(PSeq Patt
p1 Patt
p2, ([],K String
s, [])) -> Patt -> Patt -> String -> Err Substitution
matchPSeq Patt
p1 Patt
p2 String
s
(PMSeq MPatt
mp1 MPatt
mp2, ([],K String
s, [])) -> MPatt -> MPatt -> String -> Err Substitution
matchPMSeq MPatt
mp1 MPatt
mp2 String
s
(PRep Patt
p1, ([],K String
s, [])) -> [Err Substitution] -> Err Substitution
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [
Patt -> ([a], Term, [Term]) -> Err Substitution
trym ((Int -> Patt -> Patt) -> Patt -> [Int] -> Patt
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Patt -> Patt) -> Int -> Patt -> Patt
forall a b. a -> b -> a
const (Patt -> Patt -> Patt
PSeq Patt
p1)) (String -> Patt
PString String
"")
[Int
1..Int
n]) ([a], Term, [Term])
t' | Int
n <- [Int
0 .. String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s]
] Err Substitution -> Err Substitution -> Err Substitution
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Patt
PChar, ([],K [Char
_], [])) -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
(PChars String
cs, ([],K [Char
c], [])) | Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
c String
cs -> Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return []
(Patt, ([a], Term, [Term]))
_ -> String -> Err Substitution
forall (m :: * -> *) a. ErrorMonad m => String -> m a
raise (Doc -> String
forall a. Pretty a => a -> String
render (String
"no match in case expr for" String -> Term -> Doc
forall a1 a2. (Pretty a1, Pretty a2) => a1 -> a2 -> Doc
<+> Term
t))
words2term :: [String] -> Term
words2term [] = Term
Empty
words2term [String
w] = String -> Term
K String
w
words2term (String
w:[String]
ws) = Term -> Term -> Term
C (String -> Term
K String
w) ([String] -> Term
words2term [String]
ws)
matchPMSeq :: MPatt -> MPatt -> String -> Err Substitution
matchPMSeq ((Int, Int)
m1,Patt
p1) ((Int, Int)
m2,Patt
p2) String
s = (Int, Int)
-> Patt -> (Int, Int) -> Patt -> String -> Err Substitution
matchPSeq' (Int, Int)
m1 Patt
p1 (Int, Int)
m2 Patt
p2 String
s
matchPSeq :: Patt -> Patt -> String -> Err Substitution
matchPSeq Patt
p1 Patt
p2 String
s = (Int, Int)
-> Patt -> (Int, Int) -> Patt -> String -> Err Substitution
matchPSeq' (Patt -> (Int, Int)
lengthBounds Patt
p1) Patt
p1 (Patt -> (Int, Int)
lengthBounds Patt
p2) Patt
p2 String
s
matchPSeq' :: (Int, Int)
-> Patt -> (Int, Int) -> Patt -> String -> Err Substitution
matchPSeq' b1 :: (Int, Int)
b1@(Int
min1,Int
max1) Patt
p1 b2 :: (Int, Int)
b2@(Int
min2,Int
max2) Patt
p2 String
s =
do let n :: Int
n = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s
lo :: Int
lo = Int
min1 Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
max2)
hi :: Int
hi = (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
min2) Int -> Int -> Int
forall a. Ord a => a -> a -> a
`min` Int
max1
cuts :: [(String, String)]
cuts = [Int -> String -> (String, String)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
i String
s | Int
i <- [Int
lo..Int
hi]]
[Substitution]
matches <- [Err [Substitution]] -> Err [Substitution]
forall (m :: * -> *) a. ErrorMonad m => [m a] -> m a
checks [((Patt, Term) -> Err Substitution)
-> [(Patt, Term)] -> Err [Substitution]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Patt, Term) -> Err Substitution
tryMatch [(Patt
p1,String -> Term
K String
s1),(Patt
p2,String -> Term
K String
s2)] | (String
s1,String
s2) <- [(String, String)]
cuts]
Substitution -> Err Substitution
forall (m :: * -> *) a. Monad m => a -> m a
return ([Substitution] -> Substitution
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Substitution]
matches)
minLength :: Patt -> Int
minLength = Int
-> (Int -> Int)
-> (Int -> Int -> Int)
-> (Int -> Int -> Int)
-> Patt
-> Int
forall p.
p -> (Int -> p) -> (p -> p -> p) -> (p -> p -> p) -> Patt -> p
matchLength Int
0 Int -> Int
forall a. a -> a
id Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int -> Int -> Int
forall a. Ord a => a -> a -> a
min
maxLength :: Patt -> Int
maxLength =
Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
forall a. Bounded a => a
maxBound Int -> Int
forall a. a -> a
id (Maybe Int -> Int) -> (Patt -> Maybe Int) -> Patt -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Int
-> (Int -> Maybe Int)
-> (Maybe Int -> Maybe Int -> Maybe Int)
-> (Maybe Int -> Maybe Int -> Maybe Int)
-> Patt
-> Maybe Int
forall p.
p -> (Int -> p) -> (p -> p -> p) -> (p -> p -> p) -> Patt -> p
matchLength Maybe Int
forall a. Maybe a
Nothing Int -> Maybe Int
forall a. a -> Maybe a
Just ((Int -> Int -> Int) -> Maybe Int -> Maybe Int -> Maybe Int
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Int -> Int -> Int
forall a. Num a => a -> a -> a
(+)) ((Int -> Int -> Int) -> Maybe Int -> Maybe Int -> Maybe Int
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Int -> Int -> Int
forall a. Ord a => a -> a -> a
max)
matchLength :: p -> (Int -> p) -> (p -> p -> p) -> (p -> p -> p) -> Patt -> p
matchLength p
unknown Int -> p
known p -> p -> p
seq p -> p -> p
alt = Patt -> p
len
where
len :: Patt -> p
len Patt
p =
case Patt
p of
PString String
s -> Int -> p
known (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s)
PSeq Patt
p1 Patt
p2 -> p -> p -> p
seq (Patt -> p
len Patt
p1) (Patt -> p
len Patt
p2)
PAlt Patt
p1 Patt
p2 -> p -> p -> p
alt (Patt -> p
len Patt
p1) (Patt -> p
len Patt
p2)
Patt
PChar -> Int -> p
known Int
1
PChars String
_ -> Int -> p
known Int
1
PAs Ident
x Patt
p' -> Patt -> p
len Patt
p'
PT Term
t Patt
p' -> Patt -> p
len Patt
p'
Patt
_ -> p
unknown
lengthBounds :: Patt -> (Int, Int)
lengthBounds Patt
p = (Patt -> Int
minLength Patt
p,Patt -> Int
maxLength Patt
p)
mPatt :: Patt -> MPatt
mPatt Patt
p = (Patt -> (Int, Int)
lengthBounds Patt
p,Patt -> Patt
measurePatt Patt
p)
measurePatt :: Patt -> Patt
measurePatt Patt
p =
case Patt
p of
PSeq Patt
p1 Patt
p2 -> MPatt -> MPatt -> Patt
PMSeq (Patt -> MPatt
mPatt Patt
p1) (Patt -> MPatt
mPatt Patt
p2)
Patt
_ -> (Patt -> Patt) -> Patt -> Patt
composSafePattOp Patt -> Patt
measurePatt Patt
p
isInConstantForm :: Term -> Bool
isInConstantForm :: Term -> Bool
isInConstantForm Term
trm = case Term
trm of
Cn Ident
_ -> Bool
True
Con Ident
_ -> Bool
True
Q (ModuleName, Ident)
_ -> Bool
True
QC (ModuleName, Ident)
_ -> Bool
True
Abs BindType
_ Ident
_ Term
_ -> Bool
True
C Term
c Term
a -> Term -> Bool
isInConstantForm Term
c Bool -> Bool -> Bool
&& Term -> Bool
isInConstantForm Term
a
App Term
c Term
a -> Term -> Bool
isInConstantForm Term
c Bool -> Bool -> Bool
&& Term -> Bool
isInConstantForm Term
a
R [Assign]
r -> (Assign -> Bool) -> [Assign] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Term -> Bool
isInConstantForm (Term -> Bool) -> (Assign -> Term) -> Assign -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Term, Term) -> Term
forall a b. (a, b) -> b
snd ((Maybe Term, Term) -> Term)
-> (Assign -> (Maybe Term, Term)) -> Assign -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assign -> (Maybe Term, Term)
forall a b. (a, b) -> b
snd) [Assign]
r
K String
_ -> Bool
True
Term
Empty -> Bool
True
EInt Int
_ -> Bool
True
V Term
ty [Term]
ts -> Term -> Bool
isInConstantForm Term
ty Bool -> Bool -> Bool
&& (Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Term -> Bool
isInConstantForm [Term]
ts
Term
_ -> Bool
False