← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/prototyping/eval/DeBruijnLazy4.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/prototyping/eval/DeBruijnLazy4.hs
1
 
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances -fno-warn-incomplete-patterns #-}
2
 
 
3
 
 
4
 
module DeBruijnLazy4 where
5
 
 
6
 
import Prelude hiding (mapM)
7
 
 
8
 
import Control.Monad.State hiding (mapM)
9
 
import Control.Applicative
10
 
import Data.Traversable
11
 
import Data.List
12
 
import Data.Maybe
13
 
import Data.Monoid
14
 
import Data.Map (Map, (!))
15
 
import Data.Set (Set)
16
 
import qualified Data.Map as Map
17
 
import qualified Data.Set as Set
18
 
 
19
 
import qualified Syntax as S
20
 
import Syntax ( AppView(..), Pat(..), appView )
21
 
import Utils
22
 
import Pretty
23
 
import PointerST
24
 
 
25
 
data ExpR s = Var Int [Exp s]
26
 
            | Con Name [Exp s]
27
 
            | Def Name [Exp s]
28
 
            | Lam (Exp s) [Exp s]
29
 
 
30
 
type Exp s = Ptr s (ExpR s)
31
 
 
32
 
data Case s
33
 
        = Done (Exp s)
34
 
        | Skip (Case s)
35
 
        | Bind (Case s)
36
 
        | Split (NameMap (Case s))
37
 
 
38
 
type Name = Int
39
 
type NameMap = Map Name
40
 
 
41
 
type M = HeapM
42
 
 
43
 
appsR :: ExpR s -> [Exp s] -> ExpR s
44
 
appsR e         []  = e
45
 
appsR (Var n es) es' = Var n $ es ++ es'
46
 
appsR (Con c es) es' = Con c $ es ++ es'
47
 
appsR (Def c es) es' = Def c $ es ++ es'
48
 
appsR (Lam e es) es' = Lam e $ es ++ es'
49
 
 
50
 
apps :: Exp s -> [Exp s] -> M s (Exp s)
51
 
apps e [] = return e
52
 
apps e es = do
53
 
    v <- deref e
54
 
    alloc (appsR v es)
55
 
 
56
 
var n es = alloc (Var n es)
57
 
con c es = alloc (Con c es)
58
 
def c es = alloc (Def c es)
59
 
lam e es = alloc (Lam e es)
60
 
 
61
 
type Sig s = NameMap (Case s)
62
 
 
63
 
class Names a where
64
 
    getNames :: a -> Set S.Name
65
 
 
66
 
instance Names S.Exp where
67
 
    getNames e = case e of
68
 
        S.Var _   -> Set.empty
69
 
        S.Def c   -> Set.singleton c
70
 
        S.Con c   -> Set.singleton c
71
 
        S.Lam e   -> getNames e
72
 
        S.App u v -> Set.union (getNames u) (getNames v)
73
 
 
74
 
instance Names S.Pat where
75
 
    getNames p = case p of
76
 
        VarP      -> Set.empty
77
 
        WildP     -> Set.empty
78
 
        ConP c ps -> Set.insert c $ getNames ps
79
 
 
80
 
instance Names S.Clause where
81
 
    getNames (S.Clause ps v) = getNames (ps, v)
82
 
 
83
 
instance Names a => Names (Map k a) where
84
 
    getNames = getNames . Map.elems
85
 
 
86
 
instance Names a => Names [a] where
87
 
    getNames = Set.unions . map getNames
88
 
 
89
 
instance (Names a, Names b) => Names (a, b) where
90
 
    getNames (x, y) = Set.union (getNames x) (getNames y)
91
 
 
92
 
class Compile a c | a -> c where
93
 
    compile :: a -> c
94
 
 
95
 
instance Compile S.Sig (M s (Sig s, NameMap S.Name, Map S.Name Name)) where
96
 
    compile sig = do
97
 
        sig' <- Map.fromList <$> mapM comp (Map.toList sig)
98
 
        return (sig', nameMap, idMap)
99
 
        where
100
 
            ns      = Set.toList $ Set.union (getNames sig) (Set.fromList $ Map.keys sig)
101
 
            nameMap = Map.fromList $ zip [0..] ns
102
 
            idMap   = Map.fromList $ zip ns [0..]
103
 
 
104
 
            comp (c, cl) = do
105
 
                cl' <- compile cl idMap
106
 
                return (idMap ! c, cl')
107
 
 
108
 
instance Compile S.Exp (Map S.Name Name -> M s (Exp s)) where
109
 
    compile e nmap = case appView e of
110
 
        Apps (S.Var n) es -> var n                =<< comps es
111
 
        Apps (S.Con c) es -> con (nmap ! c)       =<< comps es
112
 
        Apps (S.Def c) es -> def (nmap ! c)       =<< comps es
113
 
        Apps (S.Lam v) es -> do
114
 
            v' <- compile v nmap
115
 
            vs <- comps es
116
 
            lam v' vs
117
 
        where
118
 
            comps es = mapM (flip compile nmap) es
119
 
 
120
 
instance Compile [S.Clause] (Map S.Name Name -> M s (Case s)) where
121
 
    compile cs nmap = do
122
 
        np <- nextPatterns cs
123
 
        case np of
124
 
            Right [v]   -> return $ Done v
125
 
            Right []    -> error $ "no rhs: " ++ show cs
126
 
            Right (_:_) -> error $ "overlapping patterns: " ++ show cs
127
 
            Left pcs    -> case conOrVar pcs of
128
 
                Left cs   -> Bind <$> compile cs nmap
129
 
                Right ccs -> Split <$> mapM (flip compile nmap) (Map.fromList ccs)
130
 
        where
131
 
            patterns (S.Clause ps     _) = ps
132
 
            body     (S.Clause _      v) = compile v nmap
133
 
            next     (S.Clause (p:ps) v) = (p, S.Clause ps v)
134
 
            next     _ = error $ "bad clauses: " ++ show cs
135
 
 
136
 
            nextPatterns :: [S.Clause] -> M s (Either [(Pat, S.Clause)] [Exp s])
137
 
            nextPatterns cs
138
 
                | all null pss  = Right <$> mapM body cs
139
 
                | otherwise     = return $ Left $ map next cs
140
 
                where
141
 
                    pss = map patterns cs
142
 
 
143
 
            conOrVar :: [(Pat, S.Clause)] -> Either [S.Clause] [(Name, [S.Clause])]
144
 
            conOrVar cs
145
 
                | all (isVar . fst) cs = Left $ map snd cs
146
 
                | all (isCon . fst) cs = Right $
147
 
                    map splitCon
148
 
                    $ groupBy ((==) `on` conName `on` fst)
149
 
                    $ sortBy (compare `on` conName `on` fst)
150
 
                    $ cs
151
 
                | otherwise            = error $ "bad clauses: " ++ show cs
152
 
                where
153
 
                    splitCon :: [(Pat, S.Clause)] -> (Name, [S.Clause])
154
 
                    splitCon cs = ( nmap ! conName (fst $ head cs)
155
 
                                  , map amendClause cs
156
 
                                  )
157
 
                        where
158
 
                            amendClause (ConP _ ps, S.Clause qs v) = S.Clause (ps ++ qs) v
159
 
 
160
 
                    isVar VarP  = True
161
 
                    isVar WildP = True
162
 
                    isVar _     = False
163
 
 
164
 
                    isCon (ConP _ _) = True
165
 
                    isCon _          = False
166
 
 
167
 
                    conName (ConP c _ ) = c
168
 
                    conArgs (ConP c vs) = vs
169
 
 
170
 
decompile :: NameMap S.Name -> Exp s -> M s S.Exp
171
 
decompile nmap e = do
172
 
    e <- deref e
173
 
    case e of
174
 
        Var n es -> S.apps (S.Var n) <$> mapM dec es
175
 
        Con c es -> S.apps (S.Con (nmap ! c)) <$> mapM dec es
176
 
        Def c es -> S.apps (S.Def (nmap ! c)) <$> mapM dec es
177
 
        Lam e es -> do
178
 
            e <- dec e
179
 
            es <- mapM dec es
180
 
            return $ S.Lam e `S.apps` es
181
 
    where
182
 
        dec = decompile nmap
183
 
        (!) = (Map.!)
184
 
 
185
 
 
186
 
data Condition = Broken | Pristine
187
 
 
188
 
instance Monoid Condition where
189
 
    mempty = Pristine
190
 
    mappend Broken _   = Broken
191
 
    mappend Pristine c = c
192
 
 
193
 
type RaiseM s = StateT Condition (M s)
194
 
 
195
 
needRepairs :: a -> (b -> RaiseM s a) -> RaiseM s b -> RaiseM s a
196
 
needRepairs original repair takeApart = do
197
 
    parts <- takeApart
198
 
    c     <- get
199
 
    case c of
200
 
        Pristine -> return original
201
 
        Broken   -> repair parts
202
 
 
203
 
localRepairs :: RaiseM s a -> RaiseM s a
204
 
localRepairs m = do
205
 
    c <- get
206
 
    put Pristine
207
 
    x <- m
208
 
    modify (mappend c)
209
 
    return x
210
 
 
211
 
raiseFrom :: Int -> Int -> Exp s -> RaiseM s (Exp s)
212
 
raiseFrom n k e = localRepairs $ do
213
 
    v <- lift $ deref e
214
 
    case v of
215
 
        Var m es
216
 
            | m < n     -> needRepairs e (lift . var m) $ mapM (raiseFrom n k) es
217
 
            | otherwise -> do
218
 
                put Broken
219
 
                lift . var (m + k) =<< mapM (raiseFrom n k) es
220
 
        Con c es        -> needRepairs e (lift . con c) $ mapM (raiseFrom n k) es
221
 
        Def c es        -> needRepairs e (lift . def c) $ mapM (raiseFrom n k) es
222
 
        Lam b es        -> needRepairs e (lift . uncurry lam) $ do
223
 
            b  <- raiseFrom (n + 1) k b
224
 
            es <- mapM (raiseFrom n k) es
225
 
            return (b, es)
226
 
 
227
 
raise :: Int -> Exp s -> M s (Exp s)
228
 
raise n e = evalStateT (raiseFrom 0 n e) Pristine
229
 
 
230
 
subst :: [Exp s] -> Exp s -> M s (Exp s)
231
 
subst us v = do
232
 
    v <- deref v
233
 
    case v of
234
 
        Var m es -> apps (us !! m) =<< mapM (subst us) es
235
 
        Con c es -> con c =<< mapM (subst us) es
236
 
        Def c es -> def c =<< mapM (subst us) es
237
 
        Lam t es -> do
238
 
            vz  <- var 0 []
239
 
            us' <- mapM (raise 1) us
240
 
            e   <- subst (vz : us') t
241
 
            es  <- mapM (subst us) es
242
 
            lam e es
243
 
 
244
 
matchDef :: Int -> Sig s -> Case s -> [Exp s] -> M s (Maybe (Exp s))
245
 
matchDef ctx sig c vs = match c [] vs
246
 
    where
247
 
        match (Done v)  sub vs     = {-# SCC "matchDone" #-} Just <$> (flip apps vs =<< subst sub v)
248
 
        match _         sub []     = return Nothing
249
 
        match (Skip c)  sub (v:vs) = match c sub vs
250
 
        match (Bind c)  sub (v:vs) = match c (v : sub) vs
251
 
        match (Split m) sub (v:vs) = do
252
 
            v' <- {-# SCC "matchWHNF" #-} whnf ctx sig v
253
 
            case v' of
254
 
                Con c ws -> case {-# SCC "conLookup" #-} Map.lookup c m of
255
 
                    Just c' -> match c' sub (ws ++ vs)
256
 
                    Nothing -> return Nothing
257
 
                _ -> return Nothing
258
 
 
259
 
iota :: Int -> Sig s -> Name -> [Exp s] -> M s (ExpR s)
260
 
iota ctx sig c vs = case {-# SCC "lookupDef" #-} Map.lookup c sig of
261
 
    Nothing -> return $ Con c vs
262
 
    Just cs -> do
263
 
        mv <- matchDef ctx sig cs vs
264
 
        case mv of
265
 
            Nothing -> return $ Con c vs
266
 
            Just v  -> whnf ctx sig v
267
 
 
268
 
top :: Int -> Exp s -> M s [Exp s]
269
 
top n v = (v :) <$> mapM (flip var []) [0..n - 1]
270
 
 
271
 
whnf :: Int -> Sig s -> Exp s -> M s (ExpR s)
272
 
whnf ctx sig v = onThunk v $ \v -> case v of
273
 
    Var n vs       -> return $ Var n vs
274
 
    Con c vs       -> return $ Con c vs
275
 
    Def c vs       -> iota ctx sig c vs
276
 
    Lam u (v : vs) -> do
277
 
        sub <- top ctx v
278
 
        whnf ctx sig =<< flip apps vs =<< subst sub u
279
 
    Lam u []       -> return $ Lam u []
280
 
 
281
 
eval' :: Int -> Sig s -> Exp s -> M s ()
282
 
eval' ctx sig v = do
283
 
    whnf ctx sig v
284
 
    onThunk v $ \v -> case v of
285
 
        Lam u [] -> eval' (ctx + 1) sig u >> return v
286
 
        Var n vs -> mapM (eval' ctx sig) vs >> return v
287
 
        Con c vs -> mapM (eval' ctx sig) vs >> return v
288
 
        Def c vs -> mapM (eval' ctx sig) vs >> return v
289
 
    return ()
290
 
 
291
 
eval :: S.Sig -> S.Exp -> S.Exp
292
 
eval sig e = runHeap (do
293
 
        (sig', nmap, imap) <- compile sig
294
 
        v <- compile e imap
295
 
        eval' 0 sig' v
296
 
        decompile nmap v
297
 
    )