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
|
module Renaming (renameExpr) where
import Function (second)
import List (find)
import Text.Pretty (($$), (<+>), pPrint, text)
import Utils (dropLast)
import FlatCurry.Types
import System.Console.ANSI.Codes ( yellow )
import FlatCurryGoodies (completePartCall, onBranchExps, sq', getSQ)
import FlatCurryPretty (ppExp, indent)
import Instance (instanceWith)
import Normalization (normalizeFreeExpr)
import Output (colorWith, traceDetail)
import PevalBase (Renaming, ppRenaming, mkFuncCall)
import PevalOpts (Options (optAbstract), Abstraction (..))
import Subst (Subst, isDetSubst, isVariableRenaming, subst)
renameExpr :: Options -> Renaming -> Expr -> Expr
renameExpr opts rho e = rename (initEnv opts rho) e
data RenameEnv = RenameEnv
{ rnOptions :: Options
, rnRenaming :: Renaming
}
initEnv :: Options -> Renaming -> RenameEnv
initEnv opts rho = RenameEnv opts rho
rnTrace :: RenameEnv -> Expr -> Expr -> Expr
rnTrace RenameEnv { rnOptions = o } e e'
= traceDetail o (colorWith o yellow str) e'
where str = pPrint (indent (text "Renaming" $$ ppExp e )
$$ indent (text "to" $$ ppExp e')) ++ "\n"
rename :: RenameEnv -> Expr -> Expr
rename _ v@(Var _) = v
rename _ l@(Lit _) = l
rename env c@(Comb ct qn es) = case getSQ c of
Just e -> renameSQ env e
_ -> Comb ct qn (map (rename env) es)
rename env (Free vs e) = Free vs (rename env e)
rename env (Case ct e bs) = Case ct (rename env e)
(rename env `onBranchExps` bs)
rename env (Or e1 e2) = Or (rename env e1) (rename env e2)
rename env (Let bs e) = Let (map (second (rename env)) bs)
(rename env e)
rename env (Typed e ty) = Typed (rename env e) ty
renameSQ :: RenameEnv -> Expr -> Expr
renameSQ env e = case e of
Comb ct@(FuncPartCall n) f es -> let e' = completePartCall ct f es
Comb FuncCall f' es' = renameRedex env e'
in Comb ct f' (dropLast n es')
_ -> renameRedex env e
renameRedex :: RenameEnv -> Expr -> Expr
renameRedex env e
| pea == None = renameVariant env e def
| otherwise = renameVariant env e (renameInstance env e def)
where
def = rename env (sq' (normalizeFreeExpr e))
pea = optAbstract (rnOptions env)
renameVariant :: RenameEnv -> Expr -> Expr -> Expr
renameVariant env e def = case findInstance env (\_ -> isVariableRenaming) e of
Nothing -> def
Just e' -> rnTrace env e e'
renameInstance :: RenameEnv -> Expr -> Expr -> Expr
renameInstance env e def = case findInstance env isDetSubst e of
Nothing -> def
Just e' -> rename env (sq' (rnTrace env e e'))
findInstance :: RenameEnv -> (Expr -> Subst -> Bool) -> Expr -> Maybe Expr
findInstance env p e = lookupInstance (rnRenaming env)
where
lookupInstance [] = Nothing
lookupInstance ((e', lhs) : es) = case instanceWith (normalizeFreeExpr e) e' of
Just s | p e' s -> Just (subst s (mkFuncCall lhs))
_ -> lookupInstance es
|