Commit 809c4423 authored by Michael Hanus's avatar Michael Hanus
Browse files

Merge branch 'libs_refactor'

parents 90b2527b 3954e816
## 2.1.0 (2020-02-13)
* Modernized the DOT output for definitional trees and narrowing graphs
* Added the `Rewriting.UnificationSpec` module to the list of exported modules
## 2.0.1 (2019-11-05)
* Fixed an infinite loop in the construction of definitional trees
## 2.0.0 (2019-10-16)
* First release
\ No newline at end of file
Copyright (c) 2016–2021, Jan-Hendrik Matthes
All rights reserved.
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
* Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
* Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
* Neither the name of the copyright holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
{
"name": "rewriting",
"version": "2.0.0",
"version": "3.0.0",
"author": "Jan-Hendrik Matthes, Michael Hanus <mh@informatik.uni-kiel.de>",
"maintainer": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "Libraries for term rewriting and narrowing",
"description":
"These libraries provide a representation of first-order terms
"This package provides a representation of first-order terms
and various notions of term rewriting, like position, substitution,
unification, critical pairs, etc. Moreover, it defines also
operations for rewriting and narrowing strategies and a
representation of definitional trees.
A previous version of these libraries were part of the
A previous version of the contained libraries was part of the
PAKCS/KiCS2 distributions.",
"category": [ "Rewriting", "Narrowing" ],
"homepage": "https://github.com/matthesjh/rewriting-curry",
"repository": "https://github.com/matthesjh/rewriting-curry.git",
"bugReports": "https://github.com/matthesjh/rewriting-curry/issues",
"license": "BSD-3-Clause",
"licenseFile": "LICENSE.md",
"dependencies": {
"base" : ">= 1.0.0, < 2.0.0",
"abstract-curry": ">= 2.0.0",
"finite-map" : ">= 0.0.1"
},
"compilerCompatibility": {
"pakcs": ">= 2.0.0",
"kics2": ">= 2.0.0"
"base" : ">= 3.0.0, < 4.0.0",
"abstract-curry": ">= 3.0.0, < 4.0.0",
"containers" : ">= 3.0.0, < 4.0.0",
"transformers" : ">= 3.0.0, < 4.0.0"
},
"exportedModules": [
"Rewriting.CriticalPairs", "Rewriting.Narrowing", "Rewriting.Strategy",
......
module Data.Tuple.Extra (first, second, (***), (&&&), both) where
--- Apply a function to the first component of a tuple.
first :: (a -> b) -> (a, c) -> (b, c)
first f (x, y) = (f x, y)
--- Apply a function to the second component of a tuple.
second :: (a -> b) -> (c, a) -> (c, b)
second f (x, y) = (x, f y)
--- Apply two functions to the two components of a tuple.
(***) :: (a -> b) -> (c -> d) -> (a, c) -> (b, d)
f *** g = \ (x, y) -> (f x, g y)
--- Apply two functions to a value and returns a tuple of the results.
(&&&) :: (a -> b) -> (a -> c) -> a -> (b, c)
f &&& g = \x -> (f x, g x)
--- Apply a function to both components of a tuple.
both :: (a -> b) -> (a, a) -> (b, b)
both f (x, y) = (f x, f y)
......@@ -2,8 +2,7 @@
--- Library for representation and computation of critical pairs.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
--- @version February 2020
------------------------------------------------------------------------------
module Rewriting.CriticalPairs
......@@ -11,7 +10,7 @@ module Rewriting.CriticalPairs
, showCPair, showCPairs, cPairs, isOrthogonal, isWeakOrthogonal
) where
import List (nub)
import Data.List (nub)
import Rewriting.Position (eps, positions, (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Substitution (applySubst)
......@@ -48,15 +47,16 @@ showCPairs s = unlines . (map (showCPair s))
--- Returns the critical pairs of a term rewriting system.
cPairs :: Eq f => 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))]
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 (rule1 `isVariantOf` rule2)]
-- ---------------------------------------------------------------------------
-- Functions for term rewriting systems and critical pairs
......@@ -64,8 +64,8 @@ cPairs trs
--- Checks whether a term rewriting system is orthogonal.
isOrthogonal :: Eq f => TRS f -> Bool
isOrthogonal trs = (isLeftLinear trs) && (null (cPairs trs))
isOrthogonal trs = isLeftLinear trs && null (cPairs trs)
--- Checks whether a term rewriting system is weak-orthogonal.
isWeakOrthogonal :: Eq f => TRS f -> Bool
isWeakOrthogonal trs = (isLeftLinear trs) && (all (uncurry (==)) (cPairs trs))
\ No newline at end of file
isWeakOrthogonal trs = isLeftLinear trs && all (uncurry (==)) (cPairs trs)
......@@ -3,8 +3,7 @@
--- representation of the reduction strategy phi.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
--- @version February 2020
------------------------------------------------------------------------------
module Rewriting.DefinitionalTree
......@@ -13,16 +12,18 @@ module Rewriting.DefinitionalTree
, defTrees, defTreesL, loDefTrees, phiRStrategy, dotifyDefTree, writeDefTree
) where
import Function (on, both)
import List
import Maybe (listToMaybe, catMaybes)
import Data.Function (on)
import Data.Tuple.Extra (both)
import Data.List
import Data.Maybe (listToMaybe, catMaybes, mapMaybe )
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
import Control.Monad.Trans.State
-- ---------------------------------------------------------------------------
-- Representation of definitional trees
......@@ -64,28 +65,26 @@ 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 :: Eq f => [DefTree f] -> Term f -> [DefTree f]
selectDefTrees dts t = filter ((eqConsPattern t) . dtPattern) dts
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
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]
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 :: Eq f => TRS f -> [DefTree f]
defTrees = (concatMap defTreesS) . (groupBy eqCons) . (sortBy eqCons)
defTrees = concatMap defTreesS . groupBy eqCons . sortBy eqCons
where
eqCons = on eqConsPattern fst
......@@ -97,14 +96,12 @@ defTreesL = defTrees . concat
--- rules have the same constructor pattern.
defTreesS :: Eq f => 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]
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,
......@@ -113,8 +110,8 @@ defTreesS trs@((l, _):_)
defTreesS' :: Eq f => 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@(_:_:_) [] 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]
......@@ -131,39 +128,38 @@ defTreesS' v trs (p:ps) pat = Just (Branch pat p dts)
--- given next possible variable or `Nothing` if no such definitional tree
--- exists.
mkLeaf :: Eq f => 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)
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 :: Eq f => 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))
mkOr _ _ ([], []) = Nothing
mkOr v pat ([], rs2@(_:_)) = Just (Or pat (mapMaybe (mkLeaf v pat) rs2))
mkOr v pat (rs1@(_:_), []) =
case intersect (idtPositions rs1) (varPositions pat) of
[] -> Just (Or pat (mapMaybe (mkLeaf v pat) rs1))
ps -> defTreesS' v rs1 ps 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)],
varPositions (TermCons _ ts) = [[i] | i <- [1 .. length ts],
isVarTerm (ts !! (i - 1))]
-- ---------------------------------------------------------------------------
......@@ -186,15 +182,15 @@ loDefTrees dts@(_:_) t = listToMaybe (loDefTrees' eps 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 :: Eq f => Int -> RStrategy f
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']
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
......@@ -207,18 +203,17 @@ phiRStrategy' _ _ t (Leaf (l, _))
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' 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
-- ---------------------------------------------------------------------------
......@@ -245,73 +240,72 @@ toGraph dt = fst (fst (runState (toGraph' dt) 0))
where
toGraph' :: DefTree f -> State Int (Graph f, Node f)
toGraph' (Leaf (l, r))
= newIdx `bindS`
= newIdx >>=
(\i -> let n = (i, Nothing, l)
in (mapS (ruleEdge n) [r]) `bindS` (addNode n))
in (mapM (ruleEdge n) [r]) >>= (addNode n))
toGraph' (Branch pat p dts)
= newIdx `bindS`
= newIdx >>=
(\i -> let n = (i, Just p, pat)
in (mapS (branchEdge n) dts) `bindS` (addNode n))
in (mapM (branchEdge n) dts) >>= (addNode n))
toGraph' (Or pat dts)
= newIdx `bindS`
= newIdx >>=
(\i -> let n = (i, Nothing, pat)
in (mapS (branchEdge n) dts) `bindS` (addNode n))
in (mapM (branchEdge n) dts) >>= (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)
in return ((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))
= (toGraph' dt') >>=
(\((ns, es), n2) -> return (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)]))
ruleEdge n1 t = newIdx >>= (\i -> let n = (i, Nothing, t)
in return ([n], [(True, n1, n)]))
newIdx :: State Int Int
newIdx = getS `bindS` (\i -> (putS (i + 1)) `bindS_` (returnS i))
newIdx = modify (+1) >> get
--- Transforms a term into a string representation and surrounds the subterm
--- at the given position with the html `<u>` and `</u>` tags.
--- 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' _ (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)) ++ ")"
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 b (Nothing, t) = showTerm' b t
showTP b (Just [], t) = "<u>" ++ (showTerm' b t) ++ "</u>"
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'))
++ ")"
showTP b (Just (p:ps), TermCons c ts) =
case [(if i == p then Just ps else Nothing, t) |
(i, t) <- zip [1..] ts] 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)) ++ "}"
dotifyDefTree s dt = "digraph definitional_tree {\n"
++ " graph [margin=0.0];\n"
++ " node [fontname=\"Menlo\",fontsize=10.0,shape=box];\n"
++ unlines (map showNode ns)
++ " edge [fontname=\"Menlo\",fontsize=7.0,arrowhead=none];\n"
++ unlines (map showEdge es)
++ "}"
where
(ns, es) = toGraph dt
showNode (n, p, t) = "\t" ++ (showVarIdx n) ++ " [label=<"
++ (showTermWithPos s (p, t)) ++ ">];"
showNode (n, p, t) =
" " ++ showVarIdx n ++ " [label=<" ++ showTermWithPos s (p, t) ++ ">];"
showEdge (b, (n1, _, _), (n2, _, _))
= let opts = if b then " [arrowhead=normal];" else ";"
in "\t" ++ (showVarIdx n1) ++ " -> " ++ (showVarIdx n2) ++ opts
showEdge (b, (n1, _, _), (n2, _, _)) =
let opts = if b then " [arrowhead=normal];" else ";"
in " " ++ 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.
......@@ -324,4 +318,4 @@ writeDefTree s dt fn = writeFile fn (dotifyDefTree s dt)
--- 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
parensIf b s = if b then "(" ++ s ++ ")" else s
------------------------------------------------------------------------------
--- Library to read and transform a curry program into an equivalent
--- 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 October 2016
--- @category algorithm
--- @version February 2020
------------------------------------------------------------------------------
module Rewriting.Files
......@@ -16,8 +15,7 @@ module Rewriting.Files
import AbstractCurry.Files (tryReadCurryFile)
import AbstractCurry.Types
import Data.FiniteMap (FM, listToFM)
import qualified Data.Map as Map
import Rewriting.Rules (Rule, TRS, rCons)
import Rewriting.Substitution
import Rewriting.Term (Term (..), tConst)
......@@ -29,7 +27,7 @@ import Rewriting.Term (Term (..), tConst)
--- 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)
type TRSData = Map.Map QName (TRS QName)
--- Information about types represented as a list of type declarations.
type TypeData = [CTypeDecl]
......@@ -53,7 +51,7 @@ readQName s = case break (== '.') s of
(mn, _:fn) -> (mn, fn)
-- ---------------------------------------------------------------------------
-- Functions for transforming (abstract) curry programs
-- Functions for transforming (abstract) Curry programs
-- ---------------------------------------------------------------------------
--- Returns the qualified name for an `if-then-else`-constructor.
......@@ -67,95 +65,94 @@ condTRS = let tTrue = tConst (pre "True")
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
--- 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))
Left e -> return (Left e)
Right cp -> return (Right (fromCurryProg cp))
--- Transforms an abstract curry program into an equivalent representation,
--- 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)
= (Map.fromList (map fromFuncDecl fs), ts)
--- Transforms an abstract curry function declaration into a pair with
--- 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 (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)
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.
--- 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
--- 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 (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 (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.
--- 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
--- 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
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