GenericInterpreter.hs 10.7 KB
Newer Older
Sven Keidel's avatar
Sven Keidel committed
1
2
{-# LANGUAGE Arrows #-}
{-# LANGUAGE ConstraintKinds #-}
3
4
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
Sven Keidel's avatar
Sven Keidel committed
5
{-# LANGUAGE FunctionalDependencies #-}
6
{-# LANGUAGE OverloadedStrings #-}
7
{-# LANGUAGE UndecidableInstances #-}
8
module GenericInterpreter where
Sven Keidel's avatar
Sven Keidel committed
9

10
import           Prelude hiding ((.),id,all,sequence,curry, uncurry,fail,map)
Sven Keidel's avatar
Sven Keidel committed
11

Sven Keidel's avatar
Sven Keidel committed
12
import           Syntax (Strategy(..),Strat(..),StratVar,TermPattern,TermVar)
Sven Keidel's avatar
Sven Keidel committed
13
import qualified Syntax as S
Sven Keidel's avatar
Sven Keidel committed
14
import           TermEnv as TEnv
Sven Keidel's avatar
Sven Keidel committed
15
16
import           Utils

17
import           Control.Category
Jente Hidskes's avatar
Jente Hidskes committed
18
import           Control.Arrow hiding ((<+>))
19
20
import           Control.Arrow.Fail
import           Control.Arrow.Fix
Sven Keidel's avatar
Sven Keidel committed
21
22
import           Control.Arrow.Environment as SEnv
import           Control.Arrow.Closure as Cls
23
import           Control.Arrow.Except as Exc
24
import           Control.Arrow.Utils(map)
Sven Keidel's avatar
Sven Keidel committed
25

Sven Keidel's avatar
Sven Keidel committed
26
27
import           Data.Constructor
import           Data.Text(Text)
28
import           Data.Identifiable
29
import           Data.Label
Sven Keidel's avatar
Sven Keidel committed
30
31

import           Text.Printf
32
import           GHC.Exts(IsString(..))
33
-- import qualified Debug.Trace as Debug
Sven Keidel's avatar
Sven Keidel committed
34

35
-- | Generic interpreter for Stratego
Sven Keidel's avatar
Sven Keidel committed
36
37
38
39
40
41
42
eval :: (
  ArrowChoice c, ArrowFail e c, ArrowExcept () c,
  ArrowApply c, ArrowFix (c (Strat,t) t), Identifiable t, Show t, Show env,
  ArrowLetRec StratVar cls c, ArrowClosure Strategy cls c,
  IsTerm t c, IsTermEnv env t c, IsString e,
  Exc.Join t c, Exc.Join (t,[t]) c, SEnv.Join t c, TEnv.Join env c, TEnv.Join t c, Cls.Join t c
  ) => (Strat -> c t t)
43
eval = fix' $ \ev s0 -> case s0 of
Sven Keidel's avatar
Sven Keidel committed
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
  Match f _ -> proc t -> match -< (f,t)
  Build f _ -> proc _ -> build -< f

  Id _ -> id
  S.Fail _ -> proc _ -> throw -< ()
  Seq s1 s2 _ -> proc t1 -> do t2 <- ev s1 -< t1; ev s2 -< t2
  GuardedChoice s1 s2 s3 _ -> try' (ev s1) (ev s2) (ev s3)

  One s _  -> mapSubterms (one  (ev s))
  Some s _ -> mapSubterms (some (ev s))
  All s _  -> mapSubterms (all  (ev s))

  Scope xs s _ -> proc t -> scope (ev s) -< (xs,t)
  Let bnds body _ -> let_ bnds body ev
  Call f ss ts _ -> call f ss ts ev
  Apply body _ -> ev body

  Prim {} -> proc _ -> failString -< "We do not support primitive operations."
62
{-# INLINEABLE eval #-}
Sven Keidel's avatar
Sven Keidel committed
63

Sven Keidel's avatar
Sven Keidel committed
64
-- | Apply a strategy non-determenistically to one of the subterms.
65
one :: (ArrowChoice c, ArrowExcept () c, Exc.Join (t,[t]) c) => c t t -> c [t] [t]
Sven Keidel's avatar
Sven Keidel committed
66
67
68
69
one f = proc l -> case l of
  (t:ts) -> do
    (t',ts') <- first f <+> second (one f) -< (t,ts)
    returnA -< (t':ts')
70
  [] -> throw -< ()
71
{-# INLINEABLE one #-}
Sven Keidel's avatar
Sven Keidel committed
72

Sven Keidel's avatar
Sven Keidel committed
73
74
-- | Apply a strategy to as many subterms as possible (as long as the
-- strategy does not fail).
75
some :: (ArrowChoice c, ArrowExcept () c, Exc.Join (t,[t]) c) => c t t -> c [t] [t]
Sven Keidel's avatar
Sven Keidel committed
76
77
78
79
some f = go
  where
    go = proc l -> case l of
      (t:ts) -> do
80
        (t',ts') <- try' (first f) (second go') (second go) -< (t,ts)
Sven Keidel's avatar
Sven Keidel committed
81
82
        returnA -< t':ts'
      -- the strategy did not succeed for any of the subterms, i.e. some(s) fails
83
      [] -> throw -< ()
Sven Keidel's avatar
Sven Keidel committed
84
85
    go' = proc l -> case l of
      (t:ts) -> do
86
        (t',ts') <- try' (first f) (second go') (second go') -< (t,ts)
Sven Keidel's avatar
Sven Keidel committed
87
88
        returnA -< t':ts'
      [] -> returnA -< []
89
{-# INLINEABLE some #-}
Sven Keidel's avatar
Sven Keidel committed
90

Sven Keidel's avatar
Sven Keidel committed
91
-- | Apply a strategy to all subterms.
Sven Keidel's avatar
Sven Keidel committed
92
all :: ArrowChoice c => c x y -> c [x] [y]
93
94
all = map
{-# INLINEABLE all #-}
Sven Keidel's avatar
Sven Keidel committed
95

Sven Keidel's avatar
Sven Keidel committed
96
97
98
99
100
101
102
103
104
105
scope :: (IsTermEnv env t c, ArrowChoice c, ArrowExcept e c, TEnv.Join env c, Exc.Join y c)
      => c x y -> c ([TermVar],x) y
scope s = proc (v0,x) -> case v0 of
  [] -> s -< x
  vars -> do
    oldEnv <- getTermEnv -< ()
    deleteTermVars -< vars
    finally
      (proc (t,_) -> s -< t)
      (proc (_,(vars,oldEnv)) -> unionTermEnvs -< (vars,oldEnv))
Sven Keidel's avatar
Sven Keidel committed
106
        -< (x, (vars,oldEnv))
107
{-# INLINE scope #-}
108

Sven Keidel's avatar
Sven Keidel committed
109
-- | Let binding for strategies.
Sven Keidel's avatar
Sven Keidel committed
110
111
112
113
114
115
let_ :: (ArrowClosure Strategy cls c, ArrowLetRec StratVar cls c, ArrowChoice c) => [(StratVar,Strategy)] -> Strat -> (Strat -> c t t) -> c t t
let_ bs body ev = proc t -> do
  let vars = fst <$> bs
  let strats = snd <$> bs
  cls <- map Cls.closure -< strats
  letRec (ev body) -< (zip vars cls,t)
116
{-# INLINE let_ #-}
Sven Keidel's avatar
Sven Keidel committed
117

Sven Keidel's avatar
Sven Keidel committed
118
-- | Strategy calls bind strategy variables and term variables.
Sven Keidel's avatar
Sven Keidel committed
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
call :: (ArrowChoice c, ArrowExcept () c, ArrowFail e c, IsString e,
         ArrowLetRec StratVar cls c, ArrowClosure Strategy cls c,
         ArrowApply c, IsTermEnv env t c,
         TEnv.Join env c, TEnv.Join t c, SEnv.Join t c, Exc.Join t c, Cls.Join t c)
       => StratVar -> [Strat] -> [TermVar] -> (Strat -> c t t) -> c t t
call f actualStratArgs termArgVars ev = proc t ->

  -- Lookup the strategy in the strategy environment.
  SEnv.lookup
    (proc (cls,t) -> do

       -- Close the strategy arguments in the call-site environment.
       sargs <- map Cls.closure -< [ Strategy [] [] s (label s) | s <- actualStratArgs]
       Cls.apply
         (proc (Strategy formalStratArgs formalTermArgs body _, (sargs,t)) -> do

            -- Extend the strategy environment with the strategy arguments.
            let stratArgs = zip formalStratArgs sargs
            SEnv.extend'
              (proc (formalTermArgs,body,t) -> do
                 -- Lookup the term arguments in the call-site term environment.
                 actualTermArgs <- map lookupTermVarOrFail -< termArgVars

                 -- Extend the term environment with the term arguments.
                 let termBindings = zip formalTermArgs actualTermArgs

                 case body of
                   -- If the body of the strategy is a scope, apply the fixpoint
                   -- algorithm inside the scope such that term variables don't leak.
                   Scope vars b l -> scope (bindings (ev (Apply b l)))
                     -<< (formalTermArgs ++ vars,(termBindings,t))
                   _ -> scope (bindings (ev (Apply body (label body))))
                     -<< (formalTermArgs,(termBindings,t))

              ) -< (stratArgs,(formalTermArgs,body,t))

         ) -< (cls,(sargs,t))
    )
    (proc _ -> failString -< printf "strategy %s not in scope" (show f))
    -< (f,t)

  -- senv <- readStratEnv -< ()
  -- case Env.lookup f senv of
  --   Just (Closure (Strategy formalStratArgs formalTermArgs body l) closureEnv) -> do
  --     -- let senv' = Env.fromList' [ (v,Closure (Strategy [] [] s (label s)) ())
  --     --                           | (v,s) <- zip formalStratArgs actualStratArgs] senv
  --     --             `Env.union` closureEnv

  --     actualTermArgs <- map lookupTermVarOrFail -< termArgVars
  --     let termBindings = zip formalTermArgs actualTermArgs
  --     -- case body of
  --     --   Scope vars b _ -> localStratEnv (scope (bindings (ev (Apply b l))))
  --     --     -<< (senv', (formalTermArgs ++ vars, (termBindings,t)))
  --     --   b -> localStratEnv (scope (bindings (ev (Apply b l))))
  --     --     -<< (senv', (formalTermArgs, (termBindings,t)))
  --   Nothing -> failString -< printf "strategy %s not in scope" (show f)
{-# INLINE call #-}
Sven Keidel's avatar
Sven Keidel committed
176
177
178

-- | Matches a pattern against the current term. Pattern variables are
-- bound in the term environment.
Sven Keidel's avatar
Sven Keidel committed
179
match :: (Show env, Show t, ArrowChoice c, ArrowApply c, ArrowExcept () c, IsTerm t c, IsTermEnv env t c, TEnv.Join t c)
Sven Keidel's avatar
Sven Keidel committed
180
181
182
183
184
185
      => c (TermPattern,t) t
match = proc (p,t) -> case p of
  S.As v p2 -> do
    t' <- match -< (S.Var v,t)
    match -< (p2,t')
  S.Var "_" ->
186
    returnA -< t
187
  S.Var x ->
188
    -- Stratego implements non-linear pattern matching, i.e., if a
Sven Keidel's avatar
Sven Keidel committed
189
190
    -- variable appears multiple times in a term pattern, the terms at
    -- these positions are compared for equality.
Sebastian Erdweg's avatar
Sebastian Erdweg committed
191
    lookupTermVar
192
193
194
195
196
197
198
199
      (proc (t',(x,t)) -> do
        t'' <- equal -< (t,t')
        insertTerm -< (x,t'')
        returnA -< t'')
      (proc (x,t) -> do
        insertTerm -< (x,t)
        returnA -< t)
      -< (x,(x,t))
Sven Keidel's avatar
Sven Keidel committed
200
  S.Cons c ts ->
201
202
203
204
205
    matchCons (zipWithA match) -< (c,ts,t)
  S.StringLiteral s ->
    matchString -< (s,t)
  S.NumberLiteral n ->
    matchNum -< (n,t)
Sven Keidel's avatar
Sven Keidel committed
206
  S.Explode c ts ->
207
    matchExplode
Sven Keidel's avatar
Sven Keidel committed
208
209
      (proc c' ->  match -< (c,c'))
      (proc ts' -> match -< (ts,ts')) -<< t
210
{-# INLINABLE match #-}
Sven Keidel's avatar
Sven Keidel committed
211

Sven Keidel's avatar
Sven Keidel committed
212
213
-- | Build a new term from a pattern. Variables are pattern are
-- replaced by terms in the current term environment.
Sven Keidel's avatar
Sven Keidel committed
214
build :: (ArrowChoice c, ArrowFail e c, IsString e, IsTerm t c, IsTermEnv env t c, TEnv.Join t c)
Sven Keidel's avatar
Sven Keidel committed
215
216
      => c TermPattern t
build = proc p -> case p of
217
  S.As _ _ -> fail -< "As-pattern in build is disallowed"
Sven Keidel's avatar
Sven Keidel committed
218
  S.Var x ->
219
220
221
222
    lookupTermVar
      (proc (term,_) -> returnA -< term)
      (proc (x,p) -> fail -< fromString ("unbound term variable " ++ show x ++ " in build pattern " ++ show p))
      -< (x,(x,p))
Sven Keidel's avatar
Sven Keidel committed
223
  S.Cons c ts -> do
224
    ts' <- map build -< ts
225
226
227
228
229
    buildCons -< (c,ts')
  S.StringLiteral s ->
    buildString -< s
  S.NumberLiteral n ->
    buildNum -< n
Sven Keidel's avatar
Sven Keidel committed
230
231
232
  S.Explode c ts -> do
    c'  <- build -< c
    ts' <- build -< ts
233
    buildExplode -< (c',ts')
234
235
{-# INLINABLE build #-}

Sven Keidel's avatar
Sven Keidel committed
236

237
---- Interface of the generic interpreter ----
Sven Keidel's avatar
Sven Keidel committed
238
239

-- | Arrow-based interface for matching and constructing terms.
240
class Arrow c => IsTerm t c | c -> t where
Sven Keidel's avatar
Sven Keidel committed
241
  -- | Match a term against a constructor and a list of subterms.
242
  matchCons :: c ([t'],[t]) [t] -> c (Constructor, [t'], t) t 
Sven Keidel's avatar
Sven Keidel committed
243
244

  -- | Match a term against a string literal.
245
  matchString :: c (Text,t) t
Sven Keidel's avatar
Sven Keidel committed
246
247

  -- | Match a term against a number literal.
248
  matchNum :: c (Int,t) t
Sven Keidel's avatar
Sven Keidel committed
249
250
251
252

  -- | Match a term against an explode pattern. The first strategy
  -- matches against the constructor, the second against the 'Cons'
  -- list of subterms.
253
254
255
256
257
258
259
260
261
262
263
264
265
  matchExplode :: c t t -> c t t -> c t t

  -- | Construct a term from a constructor and subterms.
  buildCons :: c (Constructor,[t]) t

  -- | Construct a term from a number literal.
  buildNum :: c Int t

  -- | Construct a term from a string literal.
  buildString :: c Text t

  -- | Convert a string literal and a 'Cons' list of subterms into a new term.
  buildExplode :: c (t,t) t
Sven Keidel's avatar
Sven Keidel committed
266
267
268
269
270
271
272
273

  -- | Checks if a given term is equal to another term and return one
  -- of the terms. If the terms are not equal, this operation fails.
  equal :: c (t,t) t

  -- | Map a strategy over the subterms of a given term.
  mapSubterms :: c [t] [t] -> c t t

274
275
---- Helper functions ----

Sven Keidel's avatar
Sven Keidel committed
276
-- | Fixpoint combinator used by Stratego.
277
278
fix' :: (ArrowFix (c (z,x) y), ArrowApply c) => ((z -> c x y) -> (z -> c x y)) -> (z -> c x y)
fix' f = curry (fix (uncurry . f . curry))
Sven Keidel's avatar
Sven Keidel committed
279
280
281
  where
    curry :: Arrow c => c (z,x) y -> (z -> c x y)
    curry g z = proc x -> g -< (z,x)
282

Sven Keidel's avatar
Sven Keidel committed
283
284
    uncurry :: ArrowApply c => (z -> c x y) -> c (z,x) y
    uncurry g = proc (z,x) -> g z -<< x
285
286
287
288
289
290
291
292
293
294
295
296
    {-# INLINE uncurry #-}
    {-# INLINE curry #-}
{-# INLINE fix' #-}

-- trace :: (Show t, Arrow c, IsTermEnv env t c, Show env) => Strat -> c t t -> c t t
-- trace s f = proc t -> do
--    env <- getTermEnv -< ()
--    () <- returnA -< Debug.trace (printf "%s: %s, %s" (show s) (show t) (show env)) ()
--    t' <- f -< t
--    env' <- getTermEnv -< ()
--    () <- returnA -< Debug.trace (printf "%s: %s, %s ---> %s, %s" (show s) (show t) (show env) (show t') (show env')) ()
--    returnA -< t'