Commit 8fd57c6f authored by Michael Hanus's avatar Michael Hanus
Browse files

State lib added, Rewriting libraries extended

parent 2e6a810e
------------------------------------------------------------------------------
--- Library for representation and computation of critical pairs.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.CriticalPairs
( CPair
, showCPair, showCPairs, cPairs, isOrthogonal, isWeakOrthogonal
) where
import List (nub)
import Rewriting.Position (eps, positions, (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Substitution (applySubst)
import Rewriting.Term (Term, showTerm, isConsTerm)
import Rewriting.Unification (unify)
-- ---------------------------------------------------------------------------
-- Representation of critical pairs
-- ---------------------------------------------------------------------------
--- A critical pair represented as a pair of terms and parameterized over the
--- kind of function symbols, e.g., strings.
type CPair f = (Term f, Term f)
-- ---------------------------------------------------------------------------
-- Pretty-printing of critical pairs
-- ---------------------------------------------------------------------------
-- \x3008 = LEFT ANGLE BRACKET
-- \x3009 = RIGHT ANGLE BRACKET
--- Transforms a critical pair into a string representation.
showCPair :: (f -> String) -> CPair f -> String
showCPair s (l, r) = "\x3008" ++ (showTerm s l) ++ ", " ++ (showTerm s r)
++ "\x3009"
--- Transforms a list of critical pairs into a string representation.
showCPairs :: (f -> String) -> [CPair f] -> String
showCPairs s = unlines . (map (showCPair s))
-- ---------------------------------------------------------------------------
-- Computation of critical pairs
-- ---------------------------------------------------------------------------
--- Returns the critical pairs of a term rewriting system.
cPairs :: TRS f -> [CPair f]
cPairs trs
= let trs' = maybe trs (\v -> renameTRSVars (v + 1) trs) (maxVarInTRS trs)
in nub [(applySubst sub r1,
replaceTerm (applySubst sub l1) p (applySubst sub r2)) |
rule1@(l1, r1) <- trs',
p <- positions l1, let l1p = l1 |> p, isConsTerm l1p,
rule2@(l2, r2) <- trs,
(Right sub) <- [unify [(l1p, l2)]],
(p /= eps) || (not (isVariantOf rule1 rule2))]
-- ---------------------------------------------------------------------------
-- Functions for term rewriting systems and critical pairs
-- ---------------------------------------------------------------------------
--- Checks whether a term rewriting system is orthogonal.
isOrthogonal :: TRS _ -> Bool
isOrthogonal trs = (isLeftLinear trs) && (null (cPairs trs))
--- Checks whether a term rewriting system is weak-orthogonal.
isWeakOrthogonal :: TRS _ -> Bool
isWeakOrthogonal trs = (isLeftLinear trs) && (all (uncurry (==)) (cPairs trs))
\ No newline at end of file
------------------------------------------------------------------------------
--- Library for representation and computation of definitional trees and
--- representation of the reduction strategy phi.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.DefinitionalTree
( DefTree (..)
, dtRoot, dtPattern, hasDefTree, selectDefTrees, fromDefTrees, idtPositions
, defTrees, defTreesL, loDefTrees, phiRStrategy, dotifyDefTree, writeDefTree
) where
import Function (on, both)
import List
import Maybe (listToMaybe, catMaybes)
import Rewriting.Position (Pos, eps, positions, (.>), (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Strategy (RStrategy)
import Rewriting.Substitution (applySubst)
import Rewriting.Term
import Rewriting.Unification (unify, unifiable)
import State
-- ---------------------------------------------------------------------------
-- Representation of definitional trees
-- ---------------------------------------------------------------------------
--- Representation of a definitional tree, parameterized over the kind of
--- function symbols, e.g., strings.
---
--- @cons Leaf r - The leaf with rule `r`.
--- @cons Branch pat p dts - The branch with pattern `pat`, inductive position
--- `p` and definitional subtrees `dts`.
--- @cons Or pat dts - The or node with pattern `pat` and definitional
--- subtrees `dts`.
data DefTree f = Leaf (Rule f)
| Branch (Term f) Pos [DefTree f]
| Or (Term f) [DefTree f]
-- ---------------------------------------------------------------------------
-- Functions for definitional trees
-- ---------------------------------------------------------------------------
--- Returns the root symbol (variable or constructor) of a definitional tree.
dtRoot :: DefTree f -> Either VarIdx f
dtRoot (Leaf r) = rRoot r
dtRoot (Branch pat _ _) = tRoot pat
dtRoot (Or pat _) = tRoot pat
--- Returns the pattern of a definitional tree.
dtPattern :: DefTree f -> Term f
dtPattern (Leaf (l, _)) = l
dtPattern (Branch pat _ _) = pat
dtPattern (Or pat _) = pat
--- Checks whether a term has a definitional tree with the same constructor
--- pattern in the given list of definitional trees.
hasDefTree :: [DefTree f] -> Term f -> Bool
hasDefTree dts t = any ((eqConsPattern t) . dtPattern) dts
--- Returns a list of definitional trees with the same constructor pattern for
--- a term from the given list of definitional trees.
selectDefTrees :: [DefTree f] -> Term f -> [DefTree f]
selectDefTrees dts t = filter ((eqConsPattern t) . dtPattern) dts
--- Returns the definitional tree with the given index from the given list of
--- definitional trees or the provided default definitional tree if the given
--- index is not in the given list of definitional trees.
fromDefTrees :: DefTree f -> Int -> [DefTree f] -> DefTree f
fromDefTrees dt _ [] = dt
fromDefTrees dt n dts@(_:_) | (n >= 0) && (n < (length dts)) = dts !! n
| otherwise = dt
--- Returns a list of all inductive positions in a term rewriting system.
idtPositions :: TRS _ -> [Pos]
idtPositions [] = []
idtPositions trs@((l, _):_)
= case l of
(TermVar _) -> []
(TermCons _ ts) -> [[i] | i <- [1..(length ts)],
all (isDemandedAt i) trs]
--- Returns a list of definitional trees for a term rewriting system.
defTrees :: TRS f -> [DefTree f]
defTrees = (concatMap defTreesS) . (groupBy eqCons) . (sortBy eqCons)
where
eqCons :: Rule f -> Rule f -> Bool
eqCons = on eqConsPattern fst
--- Returns a list of definitional trees for a list of term rewriting systems.
defTreesL :: [TRS f] -> [DefTree f]
defTreesL = defTrees . concat
--- Returns a list of definitional trees for a term rewriting system, whose
--- rules have the same constructor pattern.
defTreesS :: TRS f -> [DefTree f]
defTreesS [] = []
defTreesS trs@((l, _):_)
= case l of
(TermVar _) -> []
(TermCons c ts) ->
let arity = length ts
pat = TermCons c (map TermVar [0..(arity - 1)])
pss = permutations (idtPositions trs)
in catMaybes [defTreesS' arity trs ps pat | ps <- pss]
--- Returns a definitional tree for a term rewriting system, whose rules have
--- the same constructor pattern, with the given list of inductive positions,
--- the given pattern and the given next possible variable or `Nothing` if no
--- such definitional tree exists.
defTreesS' :: VarIdx -> TRS f -> [Pos] -> Term f -> Maybe (DefTree f)
defTreesS' _ [] [] _ = Nothing
defTreesS' v [r] [] pat = mkLeaf v pat r
defTreesS' v trs@(_:_:_) [] pat
= mkOr v pat (partition (isDemandedAt 1) trs)
defTreesS' v trs (p:ps) pat = Just (Branch pat p dts)
where
nls = nub [normalizeTerm (l |> p) | (l, _) <- trs]
ts = map (renameTermVars v) nls
pats = [replaceTerm pat p t | t <- ts]
dts = catMaybes [defTreesS' v' (selectRules v' pat') ps pat' |
pat' <- pats,
let v' = max v (maybe 0 (+ 1) (maxVarInTerm pat'))]
selectRules :: VarIdx -> Term f -> TRS f
selectRules v' t = [r | r@(l, _) <- renameTRSVars v' trs,
unifiable [(l, t)]]
--- Returns a definitional tree for the given pattern, the given rule and the
--- given next possible variable or `Nothing` if no such definitional tree
--- exists.
mkLeaf :: VarIdx -> Term f -> Rule f -> Maybe (DefTree f)
mkLeaf v pat r
= case unify [(l, pat)] of
(Left _) -> Nothing
(Right sub)
| pat == (applySubst sub l) -> Just (Leaf (both (applySubst sub) r'))
| otherwise ->
let (ip:ips) = [p | p <- positions pat, isVarTerm (pat |> p)]
pat' = replaceTerm pat ip (l |> ip)
v' = max v (maybe 0 (+ 1) (maxVarInTerm pat'))
in Just (Branch pat ip (catMaybes [defTreesS' v' [r] ips pat']))
where
r'@(l, _) = renameRuleVars v (normalizeRule r)
--- Returns a definitional tree for the given pattern, the given pair of term
--- rewriting systems and the given next possible variable or `Nothing` if no
--- such definitional tree exists. Only the rules in the first term rewriting
--- system of the pair have a demanded first argument position.
mkOr :: VarIdx -> Term f -> (TRS f, TRS f) -> Maybe (DefTree f)
mkOr _ _ ([], []) = Nothing
mkOr v pat ([], rs2@(_:_)) = let mdts = map (mkLeaf v pat) rs2
in Just (Or pat (catMaybes mdts))
mkOr v pat (rs1@(_:_), [])
= defTreesS' v rs1 (intersect (idtPositions rs1) (varPositions pat)) pat
mkOr v pat (rs1@(_:_), rs2@(_:_))
= let vps = varPositions pat
mdts = [defTreesS' v rs (intersect (idtPositions rs) vps) pat |
rs <- [rs1, rs2]]
in Just (Or pat (catMaybes mdts))
--- Returns a list of all variable argument positions in a term.
varPositions :: Term _ -> [Pos]
varPositions (TermVar _) = []
varPositions (TermCons _ ts) = [[i] | i <- [1..(length ts)],
isVarTerm (ts !! (i - 1))]
-- ---------------------------------------------------------------------------
-- Functions for the reduction strategy phi
-- ---------------------------------------------------------------------------
--- Returns the position and the definitional trees from the given list of
--- definitional trees for the leftmost outermost defined constructor in a
--- term or `Nothing` if no such pair exists.
loDefTrees :: [DefTree f] -> Term f -> Maybe (Pos, [DefTree f])
loDefTrees [] _ = Nothing
loDefTrees dts@(_:_) t = listToMaybe (loDefTrees' eps t)
where
loDefTrees' :: Pos -> Term f -> [(Pos, [DefTree f])]
loDefTrees' _ (TermVar _) = []
loDefTrees' p c@(TermCons _ ts)
| hasDefTree dts c = [(p, selectDefTrees dts c)]
| otherwise = [lp | (p', t') <- zip [1..] ts,
lp <- loDefTrees' (p .> [p']) t']
--- The reduction strategy phi. It uses the definitional tree with the given
--- index for all constructor terms if possible or at least the first one.
phiRStrategy :: Int -> RStrategy _
phiRStrategy n trs t
= let dts = defTrees trs
in case loDefTrees dts t of
Nothing -> []
(Just (_, [])) -> []
(Just (p, dts'@(dt:_))) ->
case phiRStrategy' n dts (t |> p) (fromDefTrees dt n dts') of
Nothing -> []
(Just p') -> [p .> p']
--- Returns the position for the reduction strategy phi where a term should be
--- reduced according to the given definitional tree or `Nothing` if no such
--- position exists. It uses the definitional tree with the given index for
--- all constructor terms if possible or at least the first one.
phiRStrategy' :: Int -> [DefTree f] -> Term f -> DefTree f -> Maybe Pos
phiRStrategy' _ _ t (Leaf (l, _))
| unifiable [(l', t)] = Just eps
| otherwise = Nothing
where
l' = maybe l (\v -> renameTermVars (v + 1) l) (maxVarInTerm t)
phiRStrategy' _ _ (TermVar _) (Branch _ _ _) = Nothing
phiRStrategy' n dts t@(TermCons _ _) (Branch _ p dts')
= case t |> p of
(TermVar _) -> Nothing
tp@(TermCons _ _) ->
case selectDefTrees dts tp of
[] ->
case find (\dt -> eqConsPattern tp ((dtPattern dt) |> p)) dts' of
Nothing -> Nothing
(Just dt) -> phiRStrategy' n dts t dt
x@(dt:_) -> case phiRStrategy' n dts tp (fromDefTrees dt n x) of
Nothing -> Nothing
(Just p') -> Just (p .> p')
phiRStrategy' _ _ _ (Or _ _) = Nothing
-- ---------------------------------------------------------------------------
-- Graphical representation of definitional trees
-- ---------------------------------------------------------------------------
--- A node represented as a tuple of an integer, a possible inductive position
--- and a term and parameterized over the kind of function symbols, e.g.,
--- strings.
type Node f = (Int, Maybe Pos, Term f)
--- An edge represented as a tuple of a boolean to distinguish between branch
--- (`False`) and rule (`True`) edges, a start node and an end node and
--- parameterized over the kind of function symbols, e.g., strings.
type Edge f = (Bool, Node f, Node f)
--- A graph represented as a tuple of nodes and edges and parameterized over
--- the kind of function symbols, e.g., strings.
type Graph f = ([Node f], [Edge f])
--- Transforms a definitional tree into a graph representation.
toGraph :: DefTree f -> Graph f
toGraph dt = fst (fst (runState (toGraph' dt) 0))
where
toGraph' :: DefTree f -> State Int (Graph f, Node f)
toGraph' (Leaf (l, r))
= newIdx `bindS`
(\i -> let n = (i, Nothing, l)
in (mapS (ruleEdge n) [r]) `bindS` (addNode n))
toGraph' (Branch pat p dts)
= newIdx `bindS`
(\i -> let n = (i, Just p, pat)
in (mapS (branchEdge n) dts) `bindS` (addNode n))
toGraph' (Or pat dts)
= newIdx `bindS`
(\i -> let n = (i, Nothing, pat)
in (mapS (branchEdge n) dts) `bindS` (addNode n))
addNode :: Node f -> [Graph f] -> State Int (Graph f, Node f)
addNode n gs = let (ns, es) = unzip gs
in returnS ((n:(concat ns), concat es), n)
branchEdge :: Node f -> DefTree f -> State Int (Graph f)
branchEdge n1 dt'
= (toGraph' dt') `bindS`
(\((ns, es), n2) -> returnS (ns, (False, n1, n2):es))
ruleEdge :: Node f -> Term f -> State Int (Graph f)
ruleEdge n1 t = newIdx `bindS` (\i -> let n = (i, Nothing, t)
in returnS ([n], [(True, n1, n)]))
newIdx :: State Int Int
newIdx = getS `bindS` (\i -> (putS (i + 1)) `bindS_` (returnS i))
--- Transforms a term into a string representation and surrounds the subterm
--- at the given position with the html `<u>` and `</u>` tags.
showTermWithPos :: (f -> String) -> (Maybe Pos, Term f) -> String
showTermWithPos s = showTP False
where
showTerm' :: Bool -> Term f -> String
showTerm' _ (TermVar v) = showVarIdx v
showTerm' b (TermCons c ts)
= case ts of
[] -> s c
[l, r] -> parensIf b ((showTerm' True l) ++ " " ++ (s c) ++ " "
++ (showTerm' True r))
_ -> (s c) ++ "("
++ (intercalate "," (map (showTerm' False) ts)) ++ ")"
showTP :: Bool -> (Maybe Pos, Term f) -> String
showTP b (Nothing, t) = showTerm' b t
showTP b (Just [], t) = "<u>" ++ (showTerm' b t) ++ "</u>"
showTP _ (Just (_:_), TermVar v) = showVarIdx v
showTP b (Just (p:ps), TermCons c ts)
= case [(mp, t) | (i, t) <- zip [1..] ts,
let mp = if i == p then (Just ps) else Nothing] of
[] -> s c
[l, r] -> parensIf b ((showTP True l) ++ " " ++ (s c) ++ " "
++ (showTP True r))
ts' -> (s c) ++ "(" ++ (intercalate "," (map (showTP False) ts'))
++ ")"
--- Transforms a definitional tree into a graphical representation by using
--- the *DOT graph description language*.
dotifyDefTree :: (f -> String) -> DefTree f -> String
dotifyDefTree s dt = "digraph DefinitionalTree {\n\t"
++ "node [fontname=Helvetica,fontsize=10,shape=box];\n"
++ (unlines (map showNode ns))
++ "\tedge [arrowhead=none];\n"
++ (unlines (map showEdge es)) ++ "}"
where
(ns, es) = toGraph dt
showNode :: Node _ -> String
showNode (n, p, t) = "\t" ++ (showVarIdx n) ++ " [label=<"
++ (showTermWithPos s (p, t)) ++ ">];"
showEdge :: Edge _ -> String
showEdge (b, (n1, _, _), (n2, _, _))
= let opts = if b then " [arrowhead=normal];" else ";"
in "\t" ++ (showVarIdx n1) ++ " -> " ++ (showVarIdx n2) ++ opts
--- Writes the graphical representation of a definitional tree with the
--- *DOT graph description language* to a file with the given filename.
writeDefTree :: (f -> String) -> DefTree f -> String -> IO ()
writeDefTree s dt fn = writeFile fn (dotifyDefTree s dt)
-- ---------------------------------------------------------------------------
-- Definition of helper functions
-- ---------------------------------------------------------------------------
--- Encloses a string in parenthesis if the given condition is true.
parensIf :: Bool -> String -> String
parensIf b s = if b then "(" ++ s ++ ")" else s
\ No newline at end of file
------------------------------------------------------------------------------
--- Library to read and transform a curry program into an equivalent
--- representation, where every function gets assigned the corresponding term
--- rewriting system and every type has a corresponding type declaration.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Files
( TRSData, TypeData, RWData
, showQName, readQName, condQName, condTRS, readCurryProgram, fromCurryProg
, fromFuncDecl, fromRule, fromLiteral, fromPattern, fromRhs, fromExpr
) where
import AbstractCurry.Files (tryReadCurryFile)
import AbstractCurry.Types
import FiniteMap (FM, listToFM)
import Rewriting.Rules (Rule, TRS, rCons)
import Rewriting.Substitution
import Rewriting.Term (Term (..), tConst)
-- ---------------------------------------------------------------------------
-- Representation of term rewriting system data and type data
-- ---------------------------------------------------------------------------
--- Mappings from a function name to the corresponding term rewriting system
--- represented as a finite map from qualified names to term rewriting
--- systems.
type TRSData = FM QName (TRS QName)
--- Information about types represented as a list of type declarations.
type TypeData = [CTypeDecl]
--- Representation of term rewriting system data and type data as a pair.
type RWData = (TRSData, TypeData)
-- ---------------------------------------------------------------------------
-- Pretty-printing and reading of qualified names
-- ---------------------------------------------------------------------------
--- Transforms a qualified name into a string representation.
showQName :: QName -> String
showQName (mn, fn) | null mn = fn
| otherwise = mn ++ "." ++ fn
--- Transforms a string into a qualified name.
readQName :: String -> QName
readQName s = case break (== '.') s of
qn@(_, []) -> qn
(mn, _:fn) -> (mn, fn)
-- ---------------------------------------------------------------------------
-- Functions for transforming (abstract) curry programs
-- ---------------------------------------------------------------------------
--- Returns the qualified name for an `if-then-else`-constructor.
condQName :: QName
condQName = pre "_if_"
--- Returns the term rewriting system for an `if-then-else`-function.
condTRS :: TRS QName
condTRS = let tTrue = tConst (pre "True")
tFalse = tConst (pre "False")
in [(TermCons condQName [tTrue, TermVar 0, TermVar 1], TermVar 0),
(TermCons condQName [tFalse, TermVar 0, TermVar 1], TermVar 1)]
--- Tries to read and transform a curry program into an equivalent
--- representation, where every function gets assigned the corresponding term
--- rewriting system and every type has a corresponding type declaration.
readCurryProgram :: String -> IO (Either String RWData)
readCurryProgram fn = do res <- tryReadCurryFile fn
case res of
(Left e) -> return (Left e)
(Right cp) -> return (Right (fromCurryProg cp))
--- Transforms an abstract curry program into an equivalent representation,
--- where every function gets assigned the corresponding term rewriting system
--- and every type has a corresponding type declaration.
fromCurryProg :: CurryProg -> RWData
fromCurryProg (CurryProg _ _ ts fs _)
= (listToFM (<) (map fromFuncDecl fs), ts)
--- Transforms an abstract curry function declaration into a pair with
--- function name and corresponding term rewriting system.
fromFuncDecl :: CFuncDecl -> (QName, TRS QName)
fromFuncDecl (CFunc fn _ _ _ rs)
= let (trs, trss) = unzip (map (fromRule fn) rs)
cond = if elem condQName (concatMap rCons trs) then condTRS else []
in (fn, trs ++ (concat trss) ++ cond)
fromFuncDecl (CmtFunc _ fn a v t rs) = fromFuncDecl (CFunc fn a v t rs)
--- Transforms an abstract curry rule for the function with the given name
--- into a pair of a rule and a term rewriting system.
fromRule :: QName -> CRule -> (Rule QName, TRS QName)
fromRule fn (CRule ps rhs)
= let (ts, subs) = unzip (map (fromPattern fn) ps)
(r, sub, trs) = fromRhs fn rhs
sub' = foldr composeSubst emptySubst (sub:subs)
in ((TermCons fn ts, applySubst sub' r), trs)
--- Transforms an abstract curry literal into a term.
fromLiteral :: CLiteral -> Term QName
fromLiteral (CIntc i) = tConst ("%i", show i)
fromLiteral (CFloatc f) = tConst ("%f", show f)
fromLiteral (CCharc c) = tConst ("%c", [c])
fromLiteral (CStringc s) = tConst ("%s", s)
--- Transforms an abstract curry pattern for the function with the given name
--- into a pair of a term and a substitution.
fromPattern :: QName -> CPattern -> (Term QName, Subst QName)
fromPattern _ (CPVar (v, _)) = (TermVar v, emptySubst)
fromPattern _ (CPLit l) = (fromLiteral l, emptySubst)
fromPattern fn (CPComb c ps)
= let (ts, subs) = unzip (map (fromPattern fn) ps)
in (TermCons c ts, foldr composeSubst emptySubst subs)
fromPattern fn (CPAs (v, _) p) = let (t, sub) = fromPattern fn p
in (t, extendSubst sub v t)
fromPattern fn (CPFuncComb c ps)
= let (ts, subs) = unzip (map (fromPattern fn) ps)
in (TermCons c ts, foldr composeSubst emptySubst subs)
fromPattern fn (CPLazy p) = fromPattern fn p
fromPattern fn (CPRecord _ _) = error (pError "fromPattern" "CPRecord" fn)
--- Transforms an abstract curry right-hand side of a rule for the function
--- with the given name into a tuple of a term, a substitution and a term
--- rewriting system.
fromRhs :: QName -> CRhs -> (Term QName, Subst QName, TRS QName)
fromRhs fn (CSimpleRhs e _) = fromExpr fn e
fromRhs fn (CGuardedRhs gs _) = fromGuard fn gs
--- Transforms a list of abstract curry guarded expressions for the function
--- with the given name into a tuple of a term, a substitution and a term
--- rewriting system.
fromGuard :: QName -> [(CExpr, CExpr)] -> (Term QName, Subst QName, TRS QName)
fromGuard _ [] = (tConst (pre "failed"), emptySubst, [])
fromGuard fn ((c, e):gs)
= let (ct, cs, ctrs) = fromExpr fn c
(et, es, etrs) = fromExpr fn e
(gt, gsub, gtrs) = fromGuard fn gs
sub = composeSubst cs (composeSubst es gsub)
in (TermCons condQName [ct, et, gt], sub, ctrs ++ etrs ++ gtrs)
--- Transforms an abstract curry expression for the function with the given
--- name into a tuple of a term, a substitution and a term rewriting system.
fromExpr :: QName -> CExpr -> (Term QName, Subst QName, TRS QName)
fromExpr _ (CVar (v, _)) = (TermVar v, emptySubst, [])
fromExpr _ (CLit l) = (fromLiteral l, emptySubst, [])
fromExpr _ (CSymbol s) = (tConst s, emptySubst, [])
fromExpr fn (CApply fe e)
= let (ft, fs, ftrs) = fromExpr fn fe
(et, es, etrs) = fromExpr fn e
sub = composeSubst fs es
in case ft of
(TermVar _) -> error "fromExpr: Argument is not a function!"
(TermCons c ts) -> (TermCons c (ts ++ [et]), sub, ftrs ++ etrs)
fromExpr fn (CLambda _ _) = error (pError "fromExpr" "CLambda" fn)
fromExpr fn (CLetDecl _ _) = error (pError "fromExpr" "CLetDecl" fn)
fromExpr fn (CDoExpr _) = error (pError "fromExpr" "CDoExpr" fn)
fromExpr fn (CListComp _ _) = error (pError "fromExpr" "CListComp" fn)
fromExpr fn (CCase _ _ _) = error (pError "fromExpr" "CCase" fn)
fromExpr fn (CTyped e _) = fromExpr fn e
fromExpr fn (CRecConstr _ _) = error (pError "fromExpr" "CRecConstr" fn)
fromExpr fn (CRecUpdate _ _) = error (pError "fromExpr" "CRecUpdate" fn)
-- ---------------------------------------------------------------------------
-- Definition of helper functions
-- ---------------------------------------------------------------------------
--- Error message for the given function and the feature, that is not
--- supported within the given abstract curry function.
pError :: String -> String -> QName -> String
pError fn f acf
= let fn' = if null fn then "" else fn ++ ": "
f' = if null f then "Feature" else f
in case showQName acf of
[] -> fn' ++ f' ++ " currently not supported!"
x@(_:_) -> fn' ++ f' ++ " in " ++ x ++ " currently not supported!"
\ No newline at end of file
------------------------------------------------------------------------------
--- Library for representation and computation of narrowings on first-order
--- terms and representation of narrowing strategies.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------
module Rewriting.Narrowing
( NStrategy, Narrowing (..), NarrowingGraph (..), NOptions (..)
, defaultNOptions, showNarrowing, stdNStrategy, imNStrategy, omNStrategy
, loNStrategy, lazyNStrategy, wnNStrategy, narrowBy, narrowByL, narrowingBy
, narrowingByL, narrowingGraphBy, narrowingGraphByL, solveEq, solveEqL
, dotifyNarrowingGraph, writeNarrowingGraph
) where
import FiniteMap (eltsFM)
import Maybe (fromMaybe, mapMaybe)
import List (maximum)
import Rewriting.DefinitionalTree
import Rewriting.Position
import Rewriting.Rules
import Rewriting.Strategy (RStrategy, poRStrategy, reduce)
import Rewriting.Substitution
import Rewriting.Term
import Rewriting.Unification (UnificationError (..), unify, unifiable)
import State
-- ---------------------------------------------------------------------------
-- Representation of narrowing strategies
-- ---------------------------------------------------------------------------
--- A narrowing strategy represented as a function that takes a term rewriting
--- system and a term and returns a list of triples consisting of a position,
--- a rule and a substitution, parameterized over the kind of function
--- symbols, e.g., strings.
type NStrategy f = TRS f -> Term f -> [(Pos, Rule f, Subst f)]
-- ---------------------------------------------------------------------------
-- Representation of narrowings on first-order terms
-- ---------------------------------------------------------------------------
--- Representation of a narrowing on first-order terms, parameterized over the
--- kind of function symbols, e.g., strings.
---
--- @cons NTerm t - The narrowed term `t`.
--- @cons NStep t p sub n - The narrowing of term `t` at position `p` with
--- substitution `sub` to narrowing `n`.
data Narrowing f = NTerm (Term f) | NStep (Term f) Pos (Subst f) (Narrowing f)
-- ---------------------------------------------------------------------------
-- Representation of narrowing graphs for first-order terms
-- ---------------------------------------------------------------------------
--- Representation of a narrowing graph for first-order terms, parameterized
--- over the kind of function symbols, e.g., strings.
---
--- @cons NGraph t ns - The narrowing of term `t` to a new term with a list of
--- narrowing steps `ns`.
data NarrowingGraph f = NGraph (Term f) [(Pos, Subst f, NarrowingGraph f)]