← Back to branch summary

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

« back to all changes in this revision

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