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'