@@ -14,14 +14,16 @@ module HERMIT.Dictionary.Composite
14
14
) where
15
15
16
16
import Control.Arrow
17
- import Control.Monad.IO.Class
17
+
18
+ import Data.String (fromString )
18
19
19
20
import HERMIT.Context
20
21
import HERMIT.Core
22
+ import HERMIT.External
21
23
import HERMIT.GHC
22
- import HERMIT.Monad
23
24
import HERMIT.Kure
24
- import HERMIT.External
25
+ import HERMIT.Monad
26
+ import HERMIT.Name
25
27
26
28
import HERMIT.Dictionary.Debug hiding (externals )
27
29
import HERMIT.Dictionary.GHC hiding (externals )
@@ -56,19 +58,19 @@ externals =
56
58
57
59
------------------------------------------------------------------------------------------------------
58
60
59
- basicCombinators :: [String ]
60
- basicCombinators = [" $" ," ." ," id" ," flip" ," const" ," fst" ," snd" ," curry" ," uncurry" ]
61
+ basicCombinators :: [HermitName ]
62
+ basicCombinators = map fromString [" $" ," ." ," id" ," flip" ," const" ," fst" ," snd" ," curry" ," uncurry" ]
61
63
62
64
-- | Unfold the current expression if it is one of the basic combinators:
63
65
-- ('$'), ('.'), 'id', 'flip', 'const', 'fst', 'snd', 'curry', and 'uncurry'.
64
66
-- This is intended to be used as a component of simplification traversals such as 'simplifyR' or 'bashR'.
65
- unfoldBasicCombinatorR :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
66
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
67
+ unfoldBasicCombinatorR :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
68
+ , MonadCatch m )
67
69
=> Rewrite c m CoreExpr
68
70
unfoldBasicCombinatorR = setFailMsg " unfold-basic-combinator failed." $ unfoldNamesR basicCombinators
69
71
70
- simplifyR :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
71
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
72
+ simplifyR :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
73
+ , MonadCatch m , MonadUnique m )
72
74
=> Rewrite c m Core
73
75
simplifyR = setFailMsg " Simplify failed: nothing to simplify." $
74
76
innermostR ( promoteBindR recToNonrecR
@@ -87,14 +89,14 @@ simplifyR = setFailMsg "Simplify failed: nothing to simplify." $
87
89
-- basic combinators. See 'bashComponents' for a list of rewrites performed.
88
90
-- Bash also performs occurrence analysis and de-zombification on the result, to update
89
91
-- IdInfo attributes relied-upon by GHC.
90
- bashR :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
91
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
92
+ bashR :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
93
+ , MonadCatch m , MonadUnique m )
92
94
=> Rewrite c m Core
93
95
bashR = bashExtendedWithR []
94
96
95
97
-- | An extensible bash. Given rewrites are performed before normal bash rewrites.
96
- bashExtendedWithR :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
97
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
98
+ bashExtendedWithR :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
99
+ , MonadCatch m , MonadUnique m )
98
100
=> [Rewrite c m Core ] -> Rewrite c m Core
99
101
bashExtendedWithR rs = bashUsingR (rs ++ map fst bashComponents)
100
102
@@ -104,14 +106,13 @@ bashExtendedWithR rs = bashUsingR (rs ++ map fst bashComponents)
104
106
-- Note: core fragment which fails linting is still returned! Otherwise would behave differently than bashR.
105
107
-- Useful for debugging the bash command itself.
106
108
bashDebugR :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
107
- , HasDebugChan m , HasDynFlags m , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m
108
- , MonadThings m , MonadUnique m )
109
+ , HasDebugChan m , HasDynFlags m , MonadCatch m , MonadUnique m )
109
110
=> Rewrite c m Core
110
111
bashDebugR = bashUsingR [ bracketR nm r >>> catchM (promoteT lintExprT >> idR) traceR
111
112
| (r,nm) <- bashComponents ]
112
113
113
114
-- | Perform the 'bash' algorithm with a given list of rewrites.
114
- bashUsingR :: (ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , HasEmptyContext c , MonadCatch m )
115
+ bashUsingR :: (AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadPath c Crumb , MonadCatch m )
115
116
=> [Rewrite c m Core ] -> Rewrite c m Core
116
117
bashUsingR rs = setFailMsg " bash failed: nothing to do." $
117
118
repeatR (occurAnalyseR >>> onetdR (catchesT rs)) >+> anytdR (promoteExprR dezombifyR) >+> occurAnalyseChangedR
@@ -136,8 +137,8 @@ bashHelp = "Iteratively apply the following rewrites until nothing changes:"
136
137
: map snd (bashComponents :: [(RewriteH Core ,String )] -- to resolve ambiguity
137
138
)
138
139
-- TODO: Think about a good order for bash.
139
- bashComponents :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
140
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
140
+ bashComponents :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
141
+ , MonadCatch m , MonadUnique m )
141
142
=> [(Rewrite c m Core , String )]
142
143
bashComponents =
143
144
[ -- (promoteExprR occurAnalyseExprChangedR, "occur-analyse-expr") -- ??
@@ -173,13 +174,13 @@ bashComponents =
173
174
-- | Smash is a more powerful but less efficient version of bash.
174
175
-- Unlike bash, smash is not concerned with whether it duplicates work,
175
176
-- and is intended for use during proving tasks.
176
- smashR :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
177
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
177
+ smashR :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
178
+ , MonadCatch m , MonadUnique m )
178
179
=> Rewrite c m Core
179
180
smashR = smashExtendedWithR []
180
181
181
- smashExtendedWithR :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
182
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
182
+ smashExtendedWithR :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
183
+ , MonadCatch m , MonadUnique m )
183
184
=> [Rewrite c m Core ] -> Rewrite c m Core
184
185
smashExtendedWithR rs = smashUsingR (rs ++ map fst smashComponents1) (map fst smashComponents2)
185
186
@@ -197,8 +198,8 @@ smashHelp = "A more powerful but less efficient version of \"bash\", intended fo
197
198
198
199
199
200
-- | As bash, but with "let-nonrec-subst" instead of "let-nonrec-subst-safe".
200
- smashComponents1 :: ( ExtendPath c Crumb , ReadPath c Crumb , AddBindings c , ReadBindings c , HasEmptyContext c
201
- , HasHermitMEnv m , HasHscEnv m , MonadCatch m , MonadIO m , MonadThings m , MonadUnique m )
201
+ smashComponents1 :: ( AddBindings c , ExtendPath c Crumb , HasEmptyContext c , ReadBindings c , ReadPath c Crumb
202
+ , MonadCatch m , MonadUnique m )
202
203
=> [(Rewrite c m Core , String )]
203
204
smashComponents1 =
204
205
[ -- (promoteExprR occurAnalyseExprChangedR, "occur-analyse-expr") -- ??
0 commit comments