Mercurial > urweb

comparison src/reduce.sml @ 21:067029c748e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Beta reductions for expressions
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 16:02:26 -0400
parents 1ab48e37d0ef
children d8850cc06d24
comparison
equal deleted inserted replaced
20:1ab48e37d0ef 21:067029c748e9
47 c 47 c
48 | _ => c, 48 | _ => c,
49 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) 49 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
50 | (ctx, _) => ctx} 50 | (ctx, _) => ctx}
51 51
52 val liftExpInExp =
53 U.Exp.mapB {kind = fn k => k,
54 con = fn _ => fn c => c,
55 exp = fn bound => fn e =>
56 case e of
57 ERel xn =>
58 if xn < bound then
59 e
60 else
61 ERel (xn + 1)
62 | _ => e,
63 bind = fn (bound, U.Exp.RelE _) => bound + 1
64 | (bound, _) => bound}
65
66 val subExpInExp =
67 U.Exp.mapB {kind = fn k => k,
68 con = fn _ => fn c => c,
69 exp = fn (xn, rep) => fn e =>
70 case e of
71 ERel xn' =>
72 if xn = xn' then
73 #1 rep
74 else
75 e
76 | _ => e,
77 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
78 | (ctx, _) => ctx}
79
80 val liftConInExp =
81 U.Exp.mapB {kind = fn k => k,
82 con = fn bound => fn c =>
83 case c of
84 CRel xn =>
85 if xn < bound then
86 c
87 else
88 CRel (xn + 1)
89 | _ => c,
90 exp = fn _ => fn e => e,
91 bind = fn (bound, U.Exp.RelC _) => bound + 1
92 | (bound, _) => bound}
93
94 val subConInExp =
95 U.Exp.mapB {kind = fn k => k,
96 con = fn (xn, rep) => fn c =>
97 case c of
98 CRel xn' =>
99 if xn = xn' then
100 #1 rep
101 else
102 c
103 | _ => c,
104 exp = fn _ => fn e => e,
105 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
106 | (ctx, _) => ctx}
107
52 fun bindC (env, b) = 108 fun bindC (env, b) =
53 case b of 109 case b of
54 U.Con.Rel (x, k) => E.pushCRel env x k 110 U.Con.Rel (x, k) => E.pushCRel env x k
55 | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co 111 | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co
56 112
74 | CConcat ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => CRecord (k, xcs1 @ xcs2) 130 | CConcat ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => CRecord (k, xcs1 @ xcs2)
75 | _ => c 131 | _ => c
76 132
77 and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env 133 and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
78 134
79 fun exp env e = e 135 fun exp env e =
136 case e of
137 ENamed n =>
138 (case E.lookupENamed env n of
139 (_, _, SOME e') => #1 e'
140 | _ => e)
141
142 | EApp ((EAbs (_, _, e1), loc), e2) =>
143 #1 (reduceExp env (subExpInExp (0, e2) e1))
144 | ECApp ((ECAbs (_, _, e1), loc), c) =>
145 #1 (reduceExp env (subConInExp (0, c) e1))
146
147 | _ => e
148
149 and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env
80 150
81 fun decl env d = d 151 fun decl env d = d
82 152
83 val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} CoreEnv.basis 153 val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} CoreEnv.basis
84 154