ContractWrapper extended with contract simplifcation, initial curry2verify tool added

.gitignore

@@ -12,6 +12,7 @@ CASS/cass_worker
 createmakefile/CreateMakefile
 curry2js/Curry2JS
 currypp/Main
+currypp/ContractWrapper/cwrapper
 currycheck/CurryCheck
 currydoc/CurryDoc
 currytest/CurryTest
@@ -24,4 +25,5 @@ optimize/bindingopt
 optimize/binding_optimization/BindingOpt
 runcurry/RunCurry
 spicey/spiceup
+verification/ToVerifier
 xmldata/Data2Xml

currycheck/TheoremUsage.curry

@@ -6,7 +6,7 @@
 --- * A theorem is represented in a source file by the prefix
 ---   `theorem`, e.g.:
 ---
----       theorem'sortlength xs ys = length xs -=- length (sort xs)
+---       theorem'sortlength xs = length xs -=- length (sort xs)
 ---
 --- * A theorem is considered as proven and, thus, not be checked
 ---   by CurryCheck or the contract wrapper (see `currypp`), if there exists

currypp/ContractWrapper/Makefile

@@ -12,7 +12,7 @@ PPPATH = $(TOOLDIR)/analysis:$(TOOLDIR)/CASS:$(TOOLDIR)/currycheck
 all: cwrapper
 
 # generate saved state for contract wrapper:
-cwrapper: TransContracts.curry
+cwrapper: TransContracts.curry SimplifyPostConds.curry
 	pakcs :set path $(PPPATH) :l TransContracts :save :q && mv TransContracts cwrapper
 
 .PHONY: clean

currypp/ContractWrapper/SimplifyPostConds.curry

+------------------------------------------------------------------------
+--- The implementation of the "postcondition" reducer that simplifies
+--- postconditions w.r.t. a given list of theorems.
+---
+--- @author Michael Hanus
+--- @version May 2016
+------------------------------------------------------------------------
+
+module SimplifyPostConds(simplifyPostConditionWithTheorems) where
+
+import AbstractCurry.Types
+import AbstractCurry.Select
+import AbstractCurry.Build
+import ContractUsage
+import List (last, maximum)
+import Maybe (maybeToList)
+import ReadShowTerm(readQTerm)
+import Rewriting.Files
+import Rewriting.Term
+import Rewriting.Position
+import Rewriting.Substitution
+import Rewriting.Rules
+
+simplifyPostConditionWithTheorems :: Int -> [CFuncDecl] -> [CFuncDecl]
+                                  -> IO [CFuncDecl]
+simplifyPostConditionWithTheorems verb theofuncs postconds
+ | null theofuncs
+ = return postconds
+ | otherwise
+ = mapIO (simplifyPostCondition verb theofuncs) postconds >>= return . concat
+
+simplifyPostCondition :: Int -> [CFuncDecl] ->  CFuncDecl ->  IO [CFuncDecl]
+simplifyPostCondition verb theofuncs (CFunc qn ar vis texp rs) =
+  simplifyPostCondition verb theofuncs (CmtFunc "" qn ar vis texp rs)
+simplifyPostCondition verb theofuncs (CmtFunc cmt qn ar vis texp rules) = do
+  when (verb>0) $ putStr $ unlines
+    ["THEOREMS:", showTRS' theoTRS, "SIMPLIFICATION RULES:", showTRS' simprules]
+  redrules <- mapIO (simplifyRule verb simprules qn) rules
+  return $ if all isTrivial redrules
+            then []
+            else [CmtFunc cmt qn ar vis texp redrules]
+ where
+  theoTRS   = concatMap (snd . fromFunc) theofuncs
+  simprules = concatMap theoremToSimpRules theoTRS ++ standardSimpRules
+
+theoremToSimpRules :: Rule String -> [Rule String]
+theoremToSimpRules rl@(_, TermCons f args)
+  | f == "Test.EasyCheck.-=-" || f == "Test.EasyCheck.<~>"
+  = [(TermCons "Prelude.==" args, trueTerm),
+     (TermCons "Prelude.==" (reverse args), trueTerm)]
+  | f == "Test.EasyCheck.always" = [(head args, trueTerm)]
+  | otherwise = [rl]
+
+isTrivial :: CRule -> Bool
+isTrivial (CRule _ rhs) = case rhs of
+  CSimpleRhs exp [] -> exp == constF (pre "True")
+  _                 -> False
+
+-- To avoid infinite loops during simplification, we define a maximum number
+-- of allowed simplification steps:
+maxSimpSteps :: Int
+maxSimpSteps = 100
+
+-- Simplify a rule of a postcondition.
+simplifyRule :: Int -> TRS String ->  QName -> CRule ->  IO CRule
+simplifyRule verb simprules qn crule@(CRule rpats _) = do
+  when (verb > 0 ) $ putStrLn $ unlines
+    ["POSTCONDITION: " ++ showRule' (lhs,rhs),
+     "POSTCONDEXP:   " ++ showTerm' postcondexp,
+     "SIMPLIFIEDEXP: " ++ showTerm' simpterm,
+     "SIMPPOSTCOND:  " ++ showRule' simppostcond ]     
+  return (simpleRule rpats (term2acy (concatMap varsOfPat rpats) simppostrhs))
+ where
+   (lhs,rhs)   = fromRule (showQN qn) crule
+   postcondexp = postCondition2Term lhs rhs
+   simpterm = simplifyTerm maxSimpSteps simprules postcondexp
+   simppostrhs  = postConditionTermToRule lhs simpterm
+   simppostcond = (lhs, simppostrhs)
+
+--- Transform a post-condition rule into a term by substituting
+---  the last argument variable by the function call.
+postCondition2Term :: Term String -> Term String -> Term String
+postCondition2Term (TermCons f args) rhs =
+  let TermVar i  = last args
+      (qn,fn)    = readQN f
+      fcall      = TermCons (showQN (qn, fromPostCondName fn))
+                            (take (length args - 1) args)
+      fcallsubst = extendSubst emptySubst i fcall
+   in applySubst fcallsubst rhs
+
+--- Transform (simplified) post-condition back into rule by replacing
+--- function call by the last argument variable. by the function call.
+postConditionTermToRule :: Term String -> Term String -> Term String
+postConditionTermToRule (TermCons f args) term =
+  let TermVar i  = last args
+      (qn,fn)    = readQN f
+      fcall      = TermCons (showQN (qn, fromPostCondName fn))
+                            (take (length args - 1) args)
+   in replaceAllTerms (fcall, TermVar i) term
+
+replaceAllTerms :: Rule String -> Term String -> Term String
+replaceAllTerms (lhs,rhs) term =
+  if null oneStep
+   then term
+   else replaceAllTerms (lhs,rhs) (head oneStep)
+ where
+  oneStep = [ replaceTerm term p rhs | p <- positions term, (term |> p) == lhs ]
+
+------------------------------------------------------------------------
+
+simplifyTerm :: Int -> TRS String -> Term String -> Term String
+simplifyTerm maxsteps simprules term =
+  if null oneStep || maxsteps==0
+   then term
+   else simplifyTerm (maxsteps-1) simprules (head oneStep)
+ where
+  oneStep = [ replaceTerm term p (applySubst sub rhs)
+            | p <- positions term,
+              rule <- simprules,
+              let vMax = maximum (0: tVars term) + 1,
+              let (lhs,rhs) = renameVarsBy vMax rule,
+              sub <- maybeToList (match (term |> p) lhs) ]
+
+-- match t1 t2 = sub  iff  sub(t2) = t1
+match :: Term String -> Term String -> Maybe (Subst String)
+match = matchTerm emptySubst
+ where
+  matchTerm sub t1 (TermVar i) =
+    maybe (Just (extendSubst sub i t1))
+          (\t2 -> matchTerm sub t1 t2)
+          (lookupSubst sub i)
+  matchTerm sub (TermCons f1 args1) (TermCons f2 args2) =
+    if f1 /= f2 then Nothing else matchArgs sub args1 args2
+  matchTerm _ (TermVar _) (TermCons _ _) = Nothing
+
+  matchArgs _ (_:_) [] = Nothing
+  matchArgs _ [] (_:_) = Nothing
+  matchArgs sub []  [] = Just sub
+  matchArgs sub (x:xs) (y:ys) = maybe Nothing
+                                      (\s -> matchArgs s xs ys)
+                                      (matchTerm sub x y)
+
+
+-- Some additional simplifcation rules (based on Prelude definitions):
+standardSimpRules :: TRS String
+standardSimpRules =
+  [ (TermCons "Prelude.&&" [trueTerm, x1], x1)
+  , (TermCons "Prelude.&&" [x1, trueTerm], x1)
+  ]
+ where
+  x1 = TermVar 1
+
+trueTerm :: Term String
+trueTerm = TermCons "Prelude.True" []
+
+------------------------------------------------------------------------
+--- Translate terms into AbstractCurry expressions
+
+-- to be extended
+term2acy :: [CVarIName] -> Term String -> CExpr
+term2acy cvars (TermVar i) =
+  maybe (error "term2acy: cannot find variable")
+        (\s -> CVar (i,s))
+        (lookup i cvars)
+term2acy cvars (TermCons f args)
+ | null args && head f == '%' = CLit (const2literal (tail f))
+ | otherwise
+ = foldl CApply (CSymbol (readQN f)) (map (term2acy cvars) args)
+
+const2literal :: String -> CLiteral
+const2literal sl = case sl of
+  ('i':_:s) -> CIntc   (readQTerm s)
+  ('f':_:s) -> CFloatc (readQTerm s)
+  ('c':_:s) -> CCharc  (head s)
+  ('s':_:s) -> CStringc s
+  _   -> error "const2literal: unknown literal"
+
+------------------------------------------------------------------------
+-- for better readable output: drop module prefix
+dropMod :: String -> String
+dropMod = snd . readQN
+
+showTerm' :: Term String -> String
+showTerm' = showTerm . mapTerm dropMod
+
+showRule' :: Rule String -> String
+showRule' (lhs,rhs) = showRule (mapTerm dropMod lhs, mapTerm dropMod rhs)
+
+showTRS' :: TRS String -> String
+showTRS' = unlines . map showRule'
+
+------------------------------------------------------------------------

currypp/ContractWrapper/TransContracts.curry

@@ -31,14 +31,17 @@ import Char
 import ContractUsage
 import Directory
 import Distribution
+import FilePath      (takeDirectory)
 import List
 import Maybe(fromJust)
+import SimplifyPostConds
 import System
+import TheoremUsage
 
 banner :: String
 banner = unlines [bannerLine,bannerText,bannerLine]
  where
-   bannerText = "Contract Transformation Tool (Version of 05/05/16)"
+   bannerText = "Contract Transformation Tool (Version of 22/05/16)"
    bannerLine = take (length bannerText) (repeat '=')
 
 ------------------------------------------------------------------------
@@ -120,7 +123,7 @@ transformStandalone opts modname outfile = do
                                        else error "Source program incorrect"
   let outmodname = transformedModName modname
   newprog <- transformCProg 1 opts srcprog prog outmodname
-  writeFile outfile (showCProg newprog)
+  writeFile outfile (showCProg newprog ++ "\n")
   when (executeProg opts) $ loadIntoCurry outmodname
 
 -- Specifies how the name of the transformed module is built from the
@@ -145,7 +148,8 @@ loadIntoCurry m = do
 transformCProg :: Int -> Options -> String -> CurryProg -> String
                -> IO CurryProg
 transformCProg verb opts srctxt orgprog outmodname = do
-  let prog = addCmtFuncInProg orgprog -- to avoid constructor CFunc
+  let -- to avoid constructor CFunc and references to Test.Prop
+      prog = addCmtFuncInProg (renameProp2EasyCheck orgprog)
   usageerrors <- checkContractUse prog
   unless (null usageerrors) $ do
     putStr (unlines $ "ERROR: ILLEGAL USE OF CONTRACTS:" :
@@ -158,8 +162,16 @@ transformCProg verb opts srctxt orgprog outmodname = do
       specnames = map (fromSpecName . snd . funcName) funspecs
       preconds  = getFunDeclsWith isPreCondName prog
       prenames  = map (fromPreCondName  . snd . funcName) preconds
-      postconds = getFunDeclsWith isPostCondName prog
-      postnames = map (fromPostCondName  . snd . funcName) postconds
+      opostconds= getFunDeclsWith isPostCondName prog
+      dtheofuncs= getFunDeclsWith isTheoremName prog -- declared theorems
+  -- filter theorems which have a proof file:
+  prooffiles <- getProofFiles (takeDirectory (modNameToPath (progName prog)))
+  let theofuncs = filter (\fd -> existsProofFor
+                                   (fromTheoremName (snd (funcName fd)))
+                                   prooffiles)
+                         dtheofuncs
+  postconds <- simplifyPostConditionWithTheorems verb theofuncs opostconds
+  let postnames = map (fromPostCondName  . snd . funcName) postconds
       checkfuns = union specnames (union prenames postnames)
   if null checkfuns
    then do
@@ -179,18 +191,24 @@ transformCProg verb opts srctxt orgprog outmodname = do
 getFunDeclsWith :: (String -> Bool) -> CurryProg -> [CFuncDecl]
 getFunDeclsWith pred prog = filter (pred . snd . funcName) (functions prog)
 
+------------------------------------------------------------------------
 -- Transform a given program w.r.t. given specifications and pre/postconditions
 transformProgram :: Options -> [(QName,Int)]-> [CFuncDecl]
                  -> ProgInfo Deterministic -> [CFuncDecl]
                  -> [CFuncDecl] -> [CFuncDecl] -> CurryProg -> CurryProg
 transformProgram opts funposs allfdecls detinfo specdecls predecls postdecls
-                 (CurryProg mname imps tdecls fdecls opdecls) =
- let newpostconds = concatMap
+                 (CurryProg mname imps tdecls orgfdecls opdecls) =
+ let -- replace in program old postconditions by new simplified postconditions:
+     fdecls = filter (\fd -> funcName fd `notElem` map funcName postdecls)
+                     orgfdecls ++ postdecls
+     newpostconds = concatMap
                       (genPostCond4Spec opts allfdecls detinfo postdecls)
                       specdecls
      newfunnames  = map (snd . funcName) newpostconds
+     -- remove old postconditions which are transformed into postconditions
+     -- with specification checking:
      wonewfuns    = filter (\fd -> snd (funcName fd) `notElem` newfunnames)
-                           fdecls -- remove functions having new gen. defs.
+                           fdecls
      -- compute postconditions actually used for contract checking:
      contractpcs  = postdecls++newpostconds
   in CurryProg mname
@@ -402,3 +420,23 @@ infixIDs :: String
 infixIDs =  "~!@#$%^&*+-=<>?./|\\:"
 
 ------------------------------------------------------------------------
+-- Auxiliaries
+
+-- Rename all module references to "Test.Prog" into "Test.EasyCheck"
+renameProp2EasyCheck :: CurryProg -> CurryProg
+renameProp2EasyCheck prog =
+  updCProg id (map rnmMod) id id id
+           (updQNamesInCProg (\ (mod,n) -> (rnmMod mod,n)) prog)
+ where
+  rnmMod mod | mod == propModule = easyCheckModule
+             | otherwise         = mod
+
+--- Name of the Test.Prop module (the clone of the EasyCheck module).
+propModule :: String
+propModule = "Test.Prop" 
+
+--- Name of the EasyCheck module.
+easyCheckModule :: String
+easyCheckModule = "Test.EasyCheck" 
+
+------------------------------------------------------------------------

currypp/Makefile

@@ -20,13 +20,14 @@ SQLDIR        = $(PARSEDIR)/SQL
 SEQRULESDIR   = $(CURDIR)/SequentialRules
 DEFRULESDIR   = $(CURDIR)/DefaultRules
 CONTRACTDIR   = $(CURDIR)/ContractWrapper
+REWRITINGDIR  = $(CURDIR)/../verification
 # for modules ContractUsage and DefaultRuleUsage:
 CURRYCHECKDIR = $(CURDIR)/../currycheck
 # for determinism analysis used in contract wrapper:
 DETANAPATH    = ../analysis:../CASS
 
 # preprocessor input path and dependencies:
-PPPATH = $(ICODEDIR):$(PARSEDIR):$(MLDIR):$(SQLDIR):$(SEQRULESDIR):$(DEFRULESDIR):$(CONTRACTDIR):$(CURRYCHECKDIR):$(DETANAPATH)
+PPPATH = $(ICODEDIR):$(PARSEDIR):$(MLDIR):$(SQLDIR):$(SEQRULESDIR):$(DEFRULESDIR):$(CONTRACTDIR):$(REWRITINGDIR):$(CURRYCHECKDIR):$(DETANAPATH)
 DEPS   = Main.curry $(ICODEDIR)/*.curry $(PARSEDIR)/*.curry $(MLDIR)/*.curry \
           $(SQLDIR)/*.curry $(SEQRULESDIR)/*.curry $(DEFRULESDIR)/*.curry \
 	  $(CONTRACTDIR)/*.curry $(CURRYCHECKDIR)/ContractUsage.curry \

verification/Makefile

+# Makefile for generating the curry2verify tool
+
+TOOL=$(BINDIR)/curry2verify
+
+# for determinism analysis and for module TheoremUsage:
+TOOLDIR=..
+CVPATH = $(TOOLDIR)/analysis:$(TOOLDIR)/CASS:$(TOOLDIR)/currycheck
+
+DEPS = *.curry
+
+.PHONY: all compile install clean uninstall
+
+all: install
+
+compile: ToVerifier
+
+install: ToVerifier
+	rm -f $(TOOL)
+	ln -s $(CURDIR)/ToVerifier $(TOOL)
+
+clean:
+	$(CLEANCURRY)
+	rm -f ToVerifier
+
+uninstall: clean
+	rm -f $(TOOL)
+
+ToVerifier: $(DEPS)
+	$(REPL) $(REPL_OPTS) :set path $(CVPATH) :l ToVerifier :save :q

verification/Rewriting/CriticalPairs.curry

+------------------------------------------------------------------------------
+--- Library for representation and computation of critical pairs.
+---
+--- @author Jan-Hendrik Matthes
+--- @version May 2016
+--- @category algorithm
+------------------------------------------------------------------------------
+
+module Rewriting.CriticalPairs
+  ( CPair
+  , showCPair, cPairs
+  ) where
+
+import Either (rights)
+import List (maximum, nub)
+import Rewriting.Position (eps, positions, (|>), replaceTerm)
+import Rewriting.Rules (TRS, rVars, isVariantOf, renameVarsBy)
+import Rewriting.Substitution (applySubst)
+import Rewriting.Term (Term, showTerm, isVarTerm)
+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 :: CPair String -> String
+showCPair (l, r) = "\x3008" ++ showTerm l ++ ", " ++ showTerm r ++ "\x3009"
+
+-- ---------------------------------------------------------------------------
+-- Computation of critical pairs
+-- ---------------------------------------------------------------------------
+
+--- Computes the critical pairs of a term rewriting system.
+cPairs :: TRS f -> [CPair f]
+cPairs trs = nub [(applySubst sub r1,
+                   replaceTerm (applySubst sub l1) p (applySubst sub r2)) |
+                  rule1@(l1, r1) <- trs,
+                  let vMax = maximum (0:(rVars rule1)) + 1,
+                  rule2@(l2, r2) <- map (renameVarsBy vMax) trs,
+                  p <- positions l1,
+                  let l1_p = l1 |> p, not (isVarTerm l1_p),
+                  sub <- rights [unify [(l1_p, l2)]],
+                  p /= eps || not (isVariantOf rule1 rule2)]
\ No newline at end of file

verification/Rewriting/Files.curry

+------------------------------------------------------------------------------
+--- Library to read and transform a Curry program into an equivalent
+--- representation where every function gets assigned the corresponding term
+--- rewriting system.
+---
+--- @author Jan-Hendrik Matthes
+--- @version May 2016
+--- @category algorithm
+------------------------------------------------------------------------------
+
+module Rewriting.Files
+  ( RWData
+  , emptyRWData, extendRWData, lookupRWData, readCurryProgram
+  , fromFunc, fromRule, fromExpr
+  , showQN, readQN
+  ) where
+
+import AbstractCurry.Files (tryReadCurryFile)
+import AbstractCurry.Types
+import FiniteMap (FM, emptyFM, addToFM, lookupFM)
+import Rewriting.Rules (TRS, Rule)
+import Rewriting.Term (Term (..), tConst)
+
+type RWData = FM String (TRS String)
+
+emptyRWData :: RWData
+emptyRWData = emptyFM (<)
+
+extendRWData :: RWData -> String -> TRS String-> RWData
+extendRWData = addToFM
+
+lookupRWData :: RWData -> String -> Maybe (TRS String)
+lookupRWData = lookupFM
+
+readCurryProgram :: String -> IO (Either String RWData)
+readCurryProgram f = do res <- tryReadCurryFile f
+                        case res of
+                          (Left err) -> return (Left err)
+                          (Right cp) -> return (Right (fromCurryProg cp))
+
+fromCurryProg :: CurryProg -> RWData
+fromCurryProg (CurryProg _ _ _ fs _) = extend emptyRWData (map fromFunc fs)
+  where
+    extend :: RWData -> [(String, TRS String)] -> RWData
+    extend = foldr (\(f, trs) rwd -> extendRWData rwd f trs)
+
+fromFunc :: CFuncDecl -> (String, TRS String)
+fromFunc (CFunc f _ _ _ rs)     = (showQN f, map (fromRule (showQN f)) rs)
+fromFunc (CmtFunc _ f _ _ _ rs) = (showQN f, map (fromRule (showQN f)) rs)
+
+fromRule :: String -> CRule -> Rule String
+fromRule f (CRule ps rhs) = (TermCons f (map fromPattern ps), fromRhs rhs)
+
+fromPattern :: CPattern -> Term String
+fromPattern (CPVar v)        = TermVar (fst v)
+fromPattern (CPLit l)        = fromLiteral l
+fromPattern (CPComb f ps)    = TermCons (showQN f) (map fromPattern ps)
+fromPattern (CPAs _ _)       = error "CPAs not supported!"
+fromPattern (CPFuncComb _ _) = error "CPFuncComb not supported!"
+fromPattern (CPLazy _)       = error "CPLazy not supported!"
+fromPattern (CPRecord _ _)   = error "CPRecord not supported!"
+
+fromLiteral :: CLiteral -> Term String
+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)
+
+fromRhs :: CRhs -> Term String
+fromRhs (CSimpleRhs expr _) = fromExpr expr
+fromRhs (CGuardedRhs _ _)   = error "CGuardedRhs not supported!"
+
+fromExpr :: CExpr -> Term String
+fromExpr (CVar v)         = TermVar (fst v)
+fromExpr (CLit l)         = fromLiteral l
+fromExpr (CSymbol s)      = tConst (showQN s)
+fromExpr (CApply f e)     = case fromExpr f of
+                              TermCons n ts -> TermCons n (ts ++ [fromExpr e])
+                              TermVar _     -> error "Argument is not a function!"
+fromExpr (CLambda _ _)    = error "CLambda not supported!"
+fromExpr (CLetDecl _ _)   = error "CLetDecl not supported!"
+fromExpr (CDoExpr _)      = error "CDoExpr not supported!"
+fromExpr (CListComp _ _)  = error "CListComp not supported!"
+fromExpr (CCase _ _ _)    = error "CCase not supported!"
+fromExpr (CTyped _ _)     = error "CTyped not supported!"
+fromExpr (CRecConstr _ _) = error "CRecConstr not supported!"
+fromExpr (CRecUpdate _ _) = error "CRecUpdate not supported!"
+
+--- Shows a qualified name as a string.
+showQN :: QName -> String
+showQN (qn,fn) = qn ++ "." ++ fn
+
+--- Reads a qualified name string back into a QName.
+readQN :: String -> QName
+readQN s = let (rfn,rqn) = break (=='.') (reverse s)
+            in (reverse (tail rqn), reverse rfn)

verification/Rewriting/Position.curry

+------------------------------------------------------------------------------
+--- Library for representation of positions in first-order terms.
+---
+--- @author Jan-Hendrik Matthes
+--- @version May 2016
+--- @category algorithm
+------------------------------------------------------------------------------
+
+module Rewriting.Position
+  ( Pos
+  , eps, showPos, isPosAbove, isPosBelow, isPosLeft, isPosRight
+  , isPosDisjunct, positions, (|>), replaceTerm
+  ) where
+
+import List (intercalate, isPrefixOf)
+import Rewriting.Term (Term (..))
+
+-- ---------------------------------------------------------------------------
+-- Representation of positions in first-order terms
+-- ---------------------------------------------------------------------------
+
+--- A position in a term represented as a list of integers greater than zero.
+type Pos = [Int]
+
+--- The root position of a term.
+eps :: Pos
+eps = []
+
+-- ---------------------------------------------------------------------------
+-- Pretty-printing of positions in first-order terms
+-- ---------------------------------------------------------------------------
+
+-- \x00b7 = MIDDLE DOT
+-- \x03b5 = GREEK SMALL LETTER EPSILON
+
+--- Transforms a position into a string representation.
+showPos :: Pos -> String
+showPos []       = "\x03b5"
+showPos ps@(_:_) = intercalate "\x00b7" (map show ps)
+
+-- ---------------------------------------------------------------------------
+-- Functions for positions in first-order terms
+-- ---------------------------------------------------------------------------
+
+--- Checks whether position `p` is above position `q`.
+isPosAbove :: Pos -> Pos -> Bool
+isPosAbove = isPrefixOf
+
+--- Checks whether position `p` is below position `q`.
+isPosBelow :: Pos -> Pos -> Bool
+isPosBelow = flip isPrefixOf
+
+--- Checks whether position `p` is left from position `q`.
+isPosLeft :: Pos -> Pos -> Bool
+isPosLeft []     _      = False
+isPosLeft (_:_)  []     = False
+isPosLeft (p:ps) (q:qs) = case compare p q of
+                            LT -> True
+                            EQ -> isPosLeft ps qs
+                            GT -> False
+
+--- Checks whether position `p` is right from position `q`.
+isPosRight :: Pos -> Pos -> Bool
+isPosRight []     _      = False
+isPosRight (_:_)  []     = False
+isPosRight (p:ps) (q:qs) = case compare p q of
+                             LT -> False
+                             EQ -> isPosRight ps qs
+                             GT -> True
+
+--- Checks whether position `p` is disjunct from position `q`.
+isPosDisjunct :: Pos -> Pos -> Bool
+isPosDisjunct p q = not (isPosAbove p q || isPosAbove q p)
+
+--- Returns a list of all positions within the given term.
+positions :: Term _ -> [Pos]
+positions (TermVar _)     = [eps]
+positions (TermCons _ ts) = eps:[i:p | (i, t) <- zip [1..] ts,
+                                       p <- positions t]
+
+-- ---------------------------------------------------------------------------
+-- Subterms and term replacement
+-- ---------------------------------------------------------------------------
+
+--- Selects the subterm at the given position.
+(|>) :: Term f -> Pos -> Term f
+t               |> []                              = t
+(TermCons _ ts) |> (i:p) | i > 0 && i <= length ts = (ts !! (i - 1)) |> p
+
+--- Replaces the subterm at the given position with the given term.
+---
+--- @param term  - The term with the subterm to replace.
+--- @param pos   - The position of the subterm.
+--- @param rterm - The new subterm.
+--- @return The term with the new subterm.
+replaceTerm :: Term f -> Pos -> Term f -> Term f
+replaceTerm _               []    s = s
+replaceTerm (TermCons f ts) (i:p) s
+  | i > 0 && i <= length ts = TermCons f (ts1 ++ (replaceTerm ti p s):ts2)
+  where
+    (ts1, ti:ts2) = splitAt (i - 1) ts
\ No newline at end of file