1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178

--------------------------------------------------------------------------------
--- 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 February 2020
--- @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 Data.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
-- -----------------------------------------------------------------------------

--- Returns an 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!"