← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/prototyping/eval/DeBruijnCBN.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/DeBruijnCBN.hs
1
 
{-# OPTIONS -fglasgow-exts #-}
2
 
 
3
 
module DeBruijnCBN where
4
 
 
5
 
import Data.Maybe
6
 
import Data.Monoid
7
 
import Data.Map (Map)
8
 
import qualified Data.Map as Map
9
 
 
10
 
import Syntax
11
 
 
12
 
 
13
 
raiseFrom :: Int -> Int -> Exp -> Exp
14
 
raiseFrom n k e = case e of
15
 
    Var m
16
 
        | m < n     -> Var m
17
 
        | otherwise -> Var (m + k)
18
 
    Con c           -> Con c
19
 
    Def c           -> Def c
20
 
    App s t         -> App (raiseFrom n k s) (raiseFrom n k t)
21
 
    Lam e           -> Lam $ raiseFrom (n + 1) k e
22
 
 
23
 
raise :: Int -> Exp -> Exp
24
 
raise = raiseFrom 0
25
 
 
26
 
substUnder :: Int -> Exp -> Exp -> Exp
27
 
substUnder n u v = case v of
28
 
    Var m
29
 
        | n == m    -> raise n u
30
 
        | m < n     -> Var m
31
 
        | otherwise -> Var (m - 1)
32
 
    Con c           -> Con c
33
 
    Def c           -> Def c
34
 
    App s t         -> App (substUnder n u s) (substUnder n u t)
35
 
    Lam t           -> Lam $ substUnder (n + 1) u t
36
 
 
37
 
subst :: Exp -> Exp -> Exp
38
 
subst = substUnder 0
39
 
 
40
 
substs :: [Exp] -> Exp -> Exp
41
 
substs us v = foldr subst v $ zipWith raise [0..] us
42
 
 
43
 
data Match a = No | DontKnow | Yes a
44
 
 
45
 
newtype FirstMatch a = FirstMatch { firstMatch :: Match a }
46
 
newtype AllMatch a = AllMatch { allMatch :: Match a }
47
 
 
48
 
instance Monoid (FirstMatch a) where
49
 
    mempty = FirstMatch No
50
 
    mappend (FirstMatch No) m       = m
51
 
    mappend (FirstMatch DontKnow) _ = FirstMatch DontKnow
52
 
    mappend (FirstMatch (Yes v)) _  = FirstMatch $ Yes v
53
 
 
54
 
instance Monoid a => Monoid (AllMatch a) where
55
 
    mempty                                         = AllMatch $ Yes mempty
56
 
    mappend (AllMatch No) _                        = AllMatch No
57
 
    mappend (AllMatch DontKnow) _                  = AllMatch DontKnow
58
 
    mappend (AllMatch (Yes _)) (AllMatch No)       = AllMatch No
59
 
    mappend (AllMatch (Yes _)) (AllMatch DontKnow) = AllMatch DontKnow
60
 
    mappend (AllMatch (Yes x)) (AllMatch (Yes y))  = AllMatch $ Yes $ mappend x y
61
 
 
62
 
yes :: Match a -> Maybe a
63
 
yes (Yes x) = Just x
64
 
yes _       = Nothing
65
 
 
66
 
matchDef :: Sig -> [Clause] -> [Exp] -> Maybe Exp
67
 
matchDef sig cs vs = yes $ firstMatch $ mconcat $ map (flip (match sig) vs) cs
68
 
 
69
 
match :: Sig -> Clause -> [Exp] -> FirstMatch Exp
70
 
match sig (Clause ps v) vs
71
 
    | length vs < nargs = FirstMatch DontKnow
72
 
    | otherwise         = case allMatch $ matchPats sig ps vs0 of
73
 
        Yes us   -> FirstMatch $ Yes $ substs us v `apps` vs1
74
 
        No       -> FirstMatch No
75
 
        DontKnow -> FirstMatch DontKnow
76
 
        where
77
 
            nargs     = length ps
78
 
            (vs0,vs1) = splitAt nargs vs
79
 
 
80
 
matchPats :: Sig -> [Pat] -> [Exp] -> AllMatch [Exp]
81
 
matchPats sig ps vs = mconcat $ zipWith (matchPat sig) ps vs
82
 
 
83
 
matchPat :: Sig -> Pat -> Exp -> AllMatch [Exp]
84
 
matchPat _ VarP v          = AllMatch $ Yes [v]
85
 
matchPat _ WildP v         = AllMatch $ Yes [v]
86
 
matchPat sig (ConP c ps) v = case appView $ whnf sig v of
87
 
    Apps (Con c') vs
88
 
        | c == c'   -> matchPats sig ps vs
89
 
        | otherwise -> AllMatch No
90
 
    _               -> AllMatch DontKnow
91
 
 
92
 
iota :: Sig -> String -> [Exp] -> Exp
93
 
iota sig c vs = fromMaybe (Con c `apps` vs) $ do
94
 
    cs <- Map.lookup c sig
95
 
    e  <- matchDef sig cs vs
96
 
    return $ whnf sig e
97
 
 
98
 
whnf :: Sig -> Exp -> Exp
99
 
whnf sig v = case appView v of
100
 
    Var n `Apps` vs -> Var n `apps` vs
101
 
    Con c `Apps` vs -> Con c `apps` vs
102
 
    Def c `Apps` vs -> iota sig c vs
103
 
    Lam u `Apps` (v : vs) -> whnf sig (subst v u `apps` vs)
104
 
    Lam u `Apps` []       -> Lam u
105
 
 
106
 
eval :: Sig -> Exp -> Exp
107
 
eval sig v = case whnf sig v of
108
 
    Lam u   -> Lam $ eval sig u
109
 
    App u v -> App (eval sig u) (eval sig v)
110
 
    u       -> u