Commit 415798dc authored by Michael Hanus's avatar Michael Hanus
Browse files

Prelude and Rewriting.Narrowing updated

parent b7a9248c
......@@ -14,7 +14,7 @@ module Prelude
, elem, notElem, lookup
, Ord(..)
, Show(..), print, shows, showChar, showString, showParen
, Read (..)
, Read (..), lex, read, reads, readParen
, Bounded (..), Enum (..), boundedEnumFrom, boundedEnumFromThen
, asTypeOf
, Num(..), Fractional(..), Real(..), Integral(..)
......@@ -992,7 +992,7 @@ instance Eq a => Eq [a] where
instance Eq () where
() == () = True
instance (Eq a, Eq b) => Eq (a, b) where
(a, b) == (a', b') = a == a' && b == b'
......@@ -1206,7 +1206,7 @@ instance (Show a, Show b) => Show (Either a b) where
(showString "Left " . showsPrec appPrec1 x)
showsPrec p (Right y) = showParen (p > appPrec)
(showString "Right " . showsPrec appPrec1 y)
showTuple :: [ShowS] -> ShowS
showTuple ss = showChar '('
. foldr1 (\s r -> s . showChar ',' . r) ss
......@@ -1232,20 +1232,134 @@ class Read a where
readsPrec :: Int -> ReadS a
readList :: ReadS [a]
readList = readParen False (\r -> [pr | ("[",s) <- lex r
, pr <- readl s])
where readl s = [([], t) | ("]", t) <- lex s] ++
[(x : xs, u) | (x, t) <- reads s, (xs, u) <- readl' t]
readl' s = [([], t) | ("]", t) <- lex s] ++
[(x : xs, v) | (",", t) <- lex s, (x, u) <- reads t
, (xs,v) <- readl' u]
reads :: Read a => ReadS a
reads = readsPrec minPrec
-- readParen :: Bool -> ReadS a -> ReadS a
-- readParen b =
-- read :: Read a => String -> a
-- read s =
minPrec :: Int
minPrec = 0
reads = readsPrec 0
readParen :: Bool -> ReadS a -> ReadS a
readParen b g = if b then mandatory else optional
where optional r = g r ++ mandatory r
mandatory r =
[(x, u) | ("(", s) <- lex r, (x, t) <- optional s, (")", u) <- lex t]
read :: (Read a) => String -> a
read s = case [x | (x, t) <- reads s, ("", "") <- lex t] of
[x] -> x
[] -> error "Prelude.read: no parse"
_ -> error "Prelude.read: ambiguous parse"
lex :: ReadS String
lex s = case s of
"" -> [("","")]
(c:s)
| isSpace c -> lex $ dropWhile isSpace s
('\'':s) ->
[('\'' : ch ++ "'", t) | (ch, '\'' : t) <- lexLitChar s, ch /= "'"]
('"':s) -> [('"' : str, t) | (str, t) <- lexString s]
(c:s)
| isSingle c -> [([c], s)]
| isSym c -> [(c : sym, t) | (sym, t) <- [span isSym s]]
| isAlpha c -> [(c : nam, t) | (nam, t) <- [span isIdChar s]]
| isDigit c ->
[(c : ds ++ fe, t)| (ds, s) <- [span isDigit s], (fe, t) <- lexFracExp s]
| otherwise -> []
where
isSingle c = c `elem` ",;()[]{}_`"
isSym c = c `elem` "!@#$%&⋆+./<=>?\\^|:-~"
isIdChar c = isAlphaNum c || c `elem` "_'"
lexFracExp s = case s of
('.':c:cs)
| isDigit c ->
[('.' : ds ++ e, u) | (ds, t) <- lexDigits (c : cs), (e, u) <- lexExp t]
s -> lexExp s
lexExp s = case s of
(e:s) | e `elem` "eE" ->
[(e : c : ds, u) | (c:t) <- [s], c `elem` "+-"
, (ds, u) <- lexDigits t] ++
[(e : ds, t) | (ds, t) <- lexDigits s]
s -> [("", s)]
lexString s = case s of
('"':s) -> [("\"", s)]
s -> [(ch ++ str, u) | (ch, t) <- lexStrItem s, (str, u) <- lexString t]
lexStrItem s = case s of
('\\':'&':s) -> [("\\&", s)]
('\\':c:s)
| isSpace c -> [("\\&", t) | '\\':t <- [dropWhile isSpace s]]
s -> lexLitChar s
lexLitChar :: ReadS String
lexLitChar s = case s of
"" -> []
('\\':s) -> map (prefix '\\') (lexEsc s)
(c:s) -> [([c], s)]
where
lexEsc s = case s of
(c:s)
| c `elem` "abfnrtv\\\"'" -> [([c], s)]
('^':c:s)
| c >= '@' && c <= '_' -> [(['^',c], s)]
('b':s) -> [prefix 'b' (span isBinDigit s)]
('o':s) -> [prefix 'o' (span isOctDigit s)]
('x':s) -> [prefix 'x' (span isHexDigit s)]
s@(d:_)
| isDigit d -> [span isDigit s]
s@(c:_)
| isUpper c -> [span isCharName s]
_ -> []
isCharName c = isUpper c || isDigit c
prefix c (t, s) = (c : t, s)
lexDigits :: ReadS String
lexDigits = nonNull isDigit
nonNull :: (Char -> Bool) -> ReadS String
nonNull p s = [(cs, t) | (cs@(_:_), t) <- [span p s]]
--- Returns true if the argument is an uppercase letter.
isUpper :: Char -> Bool
isUpper c = c >= 'A' && c <= 'Z'
--- Returns true if the argument is an lowercase letter.
isLower :: Char -> Bool
isLower c = c >= 'a' && c <= 'z'
--- Returns true if the argument is a letter.
isAlpha :: Char -> Bool
isAlpha c = isUpper c || isLower c
--- Returns true if the argument is a decimal digit.
isDigit :: Char -> Bool
isDigit c = c >= '0' && c <= '9'
--- Returns true if the argument is a letter or digit.
isAlphaNum :: Char -> Bool
isAlphaNum c = isAlpha c || isDigit c
--- Returns true if the argument is a binary digit.
isBinDigit :: Char -> Bool
isBinDigit c = c >= '0' || c <= '1'
--- Returns true if the argument is an octal digit.
isOctDigit :: Char -> Bool
isOctDigit c = c >= '0' && c <= '7'
--- Returns true if the argument is a hexadecimal digit.
isHexDigit :: Char -> Bool
isHexDigit c = isDigit c || c >= 'A' && c <= 'F'
|| c >= 'a' && c <= 'f'
--- Returns true if the argument is a white space.
isSpace :: Char -> Bool
isSpace c = c == ' ' || c == '\t' || c == '\n' ||
c == '\r' || c == '\f' || c == '\v' ||
c == '\xa0' || ord c `elem` [5760,6158,8192,8239,8287,12288]
-- -------------------------------------------------------------------------
-- Bounded and Enum classes and instances
......@@ -1257,10 +1371,10 @@ class Bounded a where
class Enum a where
succ :: a -> a
pred :: a -> a
toEnum :: Int -> a
fromEnum :: a -> Int
enumFrom :: a -> [a]
enumFromThen :: a -> a -> [a]
enumFromTo :: a -> a -> [a]
......@@ -1276,7 +1390,7 @@ class Enum a where
instance Bounded () where
minBound = ()
maxBound = ()
instance Enum () where
succ _ = error "Prelude.Enum.().succ: bad argument"
pred _ = error "Prelude.Enum.().pred: bad argument"
......@@ -1293,7 +1407,7 @@ instance Enum () where
instance Bounded Bool where
minBound = False
maxBound = True
instance Enum Bool where
succ False = True
succ True = error "Prelude.Enum.Bool.succ: bad argument"
......@@ -1435,7 +1549,7 @@ instance Num Int where
abs x | x >= 0 = x
| otherwise = negate x
signum x | x > 0 = 1
| x == 0 = 0
| otherwise = -1
......@@ -1486,7 +1600,7 @@ class Real a => Integral a where
rem :: a -> a -> a
divMod :: a -> a -> (a, a)
quotRem :: a -> a -> (a,a)
quotRem :: a -> a -> (a, a)
n `div` d = q where (q, _) = divMod n d
n `mod` d = r where (_, r) = divMod n d
......
......@@ -73,7 +73,7 @@ data NarrowingGraph f = NGraph (Term f) [(Pos, Subst f, NarrowingGraph f)]
data NOptions f = NOptions { normalize :: Bool, rStrategy :: RStrategy f }
--- The default narrowing options.
defaultNOptions :: NOptions _
defaultNOptions :: Eq f => NOptions f
defaultNOptions = NOptions { normalize = False, rStrategy = poRStrategy }
-- ---------------------------------------------------------------------------
......@@ -95,28 +95,28 @@ showNarrowing s (NStep t p sub n)
-- ---------------------------------------------------------------------------
--- The standard narrowing strategy.
stdNStrategy :: NStrategy _
stdNStrategy :: Eq f => NStrategy f
stdNStrategy trs t = [(p, rule, sub) |
p <- positions t, let tp = t |> p, isConsTerm tp,
rule@(l, _) <- trs,
(Right sub) <- [unify [(tp, l)]]]
--- The innermost narrowing strategy.
imNStrategy :: NStrategy _
imNStrategy :: Eq f => NStrategy f
imNStrategy trs t = [(p, rule, sub) |
p <- positions t, let tp = t |> p, isPattern trs tp,
rule@(l, _) <- trs,
(Right sub) <- [unify [(tp, l)]]]
--- The outermost narrowing strategy.
omNStrategy :: NStrategy _
omNStrategy :: Eq f => NStrategy f
omNStrategy trs t = let ns = stdNStrategy trs t
in [n | n@(p, _, _) <- ns,
all (\p' -> not (isPosAbove p' p))
[p' | (p', _, _) <- ns, p' /= p]]
--- The leftmost outermost narrowing strategy.
loNStrategy :: NStrategy _
loNStrategy :: Eq f => NStrategy f
loNStrategy trs t
= let ns = stdNStrategy trs t
in [n | n@(p, _, _) <- ns,
......@@ -124,14 +124,14 @@ loNStrategy trs t
[p' | (p', _, _) <- ns, p' /= p]]
--- The lazy narrowing strategy.
lazyNStrategy :: NStrategy _
lazyNStrategy :: Eq f => NStrategy f
lazyNStrategy trs t
= let lps = lazyPositions trs t
in filter (\(p, _, _) -> elem p lps) (stdNStrategy trs t)
--- Returns a list of all lazy positions in a term according to the given term
--- rewriting system.
lazyPositions :: TRS f -> Term f -> [Pos]
lazyPositions :: Eq f => TRS f -> Term f -> [Pos]
lazyPositions _ (TermVar _) = []
lazyPositions trs t@(TermCons _ ts)
| hasRule trs t = if null rs then lps else eps:lps
......@@ -143,7 +143,7 @@ lazyPositions trs t@(TermCons _ ts)
lps = [i:p | i <- dps, p <- lazyPositions trs (ts !! (i - 1))]
--- The weakly needed narrowing strategy.
wnNStrategy :: NStrategy _
wnNStrategy :: Eq f => NStrategy f
wnNStrategy trs t
= let dts = defTrees trs
v = fromMaybe 0 (minVarInTRS trs)
......@@ -156,7 +156,7 @@ wnNStrategy trs t
--- Returns the narrowing steps for the weakly needed narrowing strategy
--- according to the given definitional tree and the given next possible
--- variable.
wnNStrategy' :: [DefTree f] -> VarIdx -> Term f -> DefTree f
wnNStrategy' :: Eq f => [DefTree f] -> VarIdx -> Term f -> DefTree f
-> [(Pos, Rule f, Subst f)]
wnNStrategy' _ v t (Leaf r)
= let rule@(l, _) = renameRuleVars v (normalizeRule r)
......@@ -173,7 +173,6 @@ wnNStrategy' dts v t (Branch pat p dts')
in [(p .> p', rule, composeSubst sub tau') |
(p', rule, sub) <- wnNStrategy' dts v' (t' |> p) dt]
where
filterDTS :: [DefTree f] -> [DefTree f]
filterDTS = filter (\dt -> let dtp = renameTermVars v (dtPattern dt)
in unifiable [(t, dtp)])
wnNStrategy' dts v t (Or _ dts') = concatMap (wnNStrategy' dts v t) dts'
......@@ -205,7 +204,6 @@ narrowBy' v sub s trs n t
[] -> [(sub, t)]
ns@(_:_) -> concatMap combine ns
where
combine :: (Pos, Rule f, Subst f) -> [(Subst f, Term f)]
combine (p, (_, r), sub')
= let t' = applySubst sub' (replaceTerm t p r)
rsub' = restrictSubst sub' (tVars t)
......@@ -237,7 +235,7 @@ narrowingBy' v sub s trs n t
[] -> [NTerm t]
ns@(_:_) -> concatMap combine ns
where
combine :: (Pos, Rule f, Subst f) -> [Narrowing f]
-- combine :: (Pos, Rule f, Subst f) -> [Narrowing f]
combine (p, (_, r), sub')
= let t' = applySubst sub' (replaceTerm t p r)
rsub' = restrictSubst sub' (tVars t)
......@@ -271,7 +269,7 @@ narrowingGraphBy' v sub s trs n t
| otherwise = NGraph t (map combine (s trs' t))
where
trs' = renameTRSVars v (normalizeTRS trs)
combine :: (Pos, Rule f, Subst f) -> (Pos, Subst f, NarrowingGraph f)
--combine :: (Pos, Rule f, Subst f) -> (Pos, Subst f, NarrowingGraph f)
combine (p, (_, r), sub')
= let t' = applySubst sub' (replaceTerm t p r)
rsub' = restrictSubst sub' (tVars t)
......@@ -286,7 +284,7 @@ narrowingGraphBy' v sub s trs n t
--- `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l`
--- and the term `r` are the left-hand side and the right-hand side of the
--- term equation.
solveEq :: NOptions f -> NStrategy f -> TRS f -> Term f -> [Subst f]
solveEq :: Eq f => NOptions f -> NStrategy f -> TRS f -> Term f -> [Subst f]
solveEq _ _ _ (TermVar _) = []
solveEq opts s trs t@(TermCons _ ts)
= case ts of
......@@ -301,7 +299,7 @@ solveEq opts s trs t@(TermCons _ ts)
--- `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l`
--- and the term `r` are the left-hand side and the right-hand side of the
--- term equation.
solveEqL :: NOptions f -> NStrategy f -> [TRS f] -> Term f -> [Subst f]
solveEqL :: Eq f => NOptions f -> NStrategy f -> [TRS f] -> Term f -> [Subst f]
solveEqL opts s trss = solveEq opts s (concat trss)
--- Solves a term equation with the given strategy, the given term rewriting
......@@ -310,7 +308,8 @@ solveEqL opts s trss = solveEq opts s (concat trss)
--- `TermCons c [l, r]` with `c` being a constructor like `=`. The term `l`
--- and the term `r` are the left-hand side and the right-hand side of the
--- term equation.
solveEq' :: NOptions f -> VarIdx -> Subst f -> NStrategy f -> TRS f -> Term f
solveEq' :: Eq f =>
NOptions f -> VarIdx -> Subst f -> NStrategy f -> TRS f -> Term f
-> [Subst f]
solveEq' _ _ _ _ _ (TermVar _) = []
solveEq' opts v sub s trs t@(TermCons _ ts)
......@@ -327,7 +326,7 @@ solveEq' opts v sub s trs t@(TermCons _ ts)
nt@(TermCons _ [l, r]) = if (normalize opts)
then reduce (rStrategy opts) trs t
else t
solve :: (Pos, Rule f, Subst f) -> [Subst f]
--solve :: (Pos, Rule f, Subst f) -> [Subst f]
solve (p, (_, r'), sub')
= let t' = applySubst sub' (replaceTerm nt p r')
rsub' = restrictSubst sub' (tVars nt)
......@@ -381,10 +380,10 @@ dotifyNarrowingGraph s ng
++ (unlines (map showEdge es)) ++ "}"
where
(ns, es) = toGraph ng
showNode :: Node _ -> String
showNode (n, t) = "\t" ++ (showVarIdx n) ++ " [label=\"" ++ (showTerm s t)
++ "\"];"
showEdge :: Edge _ -> String
showEdge ((n1, t), sub, (n2, _))
= "\t" ++ (showVarIdx n1) ++ " -> " ++ (showVarIdx n2) ++ " [label=\""
++ (showSubst s (restrictSubst sub (tVars t))) ++ "\"];"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment