Mercurial > urweb

comparison src/reduce.sml @ 417:e0e9e9eca1cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix nasty de Bruijn substitution bug; TcSum demo
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 12:58:35 -0400
parents 075b36dbb1a4
children bd9ee9aeca2f
comparison
equal deleted inserted replaced
416:679b2fbbd4d0 417:e0e9e9eca1cb
34 structure E = CoreEnv 34 structure E = CoreEnv
35 structure U = CoreUtil 35 structure U = CoreUtil
36 36
37 val liftConInCon = E.liftConInCon 37 val liftConInCon = E.liftConInCon
38 val subConInCon = E.subConInCon 38 val subConInCon = E.subConInCon
39 val liftConInExp = E.liftConInExp
39 40
40 val liftExpInExp = 41 val liftExpInExp =
41 U.Exp.mapB {kind = fn k => k, 42 U.Exp.mapB {kind = fn k => k,
42 con = fn _ => fn c => c, 43 con = fn _ => fn c => c,
43 exp = fn bound => fn e => 44 exp = fn bound => fn e =>
61 EQUAL => #1 rep 62 EQUAL => #1 rep
62 | GREATER=> ERel (xn' - 1) 63 | GREATER=> ERel (xn' - 1)
63 | LESS => e) 64 | LESS => e)
64 | _ => e, 65 | _ => e,
65 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) 66 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
67 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
66 | (ctx, _) => ctx} 68 | (ctx, _) => ctx}
67 69
68 val liftConInExp = E.liftConInExp 70 val liftConInExp = E.liftConInExp
69 val subConInExp = E.subConInExp 71 val subConInExp = E.subConInExp
70 72
104 | _ => c 106 | _ => c
105 107
106 and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env 108 and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
107 109
108 fun exp env e = 110 fun exp env e =
109 case e of 111 let
110 ENamed n => 112 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan))]*)
111 (case E.lookupENamed env n of
112 (_, _, SOME e', _) => #1 e'
113 | _ => e)
114 113
115 | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) => 114 val r = case e of
116 (case xcs of 115 ENamed n =>
117 [] => #1 i 116 (case E.lookupENamed env n of
118 | (n, v) :: rest => 117 (_, _, SOME e', _) => #1 e'
119 #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc), 118 | _ => e)
120 (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc),
121 (CRecord (k, rest), loc)), loc)), loc)))
122 119
123 | EApp ((EAbs (_, _, _, e1), loc), e2) => 120 | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) =>
124 #1 (reduceExp env (subExpInExp (0, e2) e1)) 121 (case xcs of
125 | ECApp ((ECAbs (_, _, e1), loc), c) => 122 [] => #1 i
126 #1 (reduceExp env (subConInExp (0, c) e1)) 123 | (n, v) :: rest =>
124 #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc),
125 (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc),
126 (CRecord (k, rest), loc)), loc)), loc)))
127 127
128 | EField ((ERecord xes, _), (CName x, _), _) => 128 | EApp ((EAbs (_, _, _, e1), loc), e2) =>
129 (case List.find (fn ((CName x', _), _, _) => x' = x 129 #1 (reduceExp env (subExpInExp (0, e2) e1))
130 | _ => false) xes of 130 | ECApp ((ECAbs (_, _, e1), loc), c) =>
131 SOME (_, e, _) => #1 e 131 #1 (reduceExp env (subConInExp (0, c) e1))
132 | NONE => e)
133 | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) =>
134 let
135 fun fields (remaining, passed) =
136 case remaining of
137 [] => []
138 | (x, t) :: rest =>
139 (x,
140 (EField (r, x, {field = t,
141 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
142 t) :: fields (rest, (x, t) :: passed)
143 in
144 #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc))
145 end
146 | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
147 let
148 fun fields (remaining, passed) =
149 case remaining of
150 [] => []
151 | (x, t) :: rest =>
152 (x,
153 (EField (r, x, {field = t,
154 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
155 t) :: fields (rest, (x, t) :: passed)
156 in
157 #1 (reduceExp env (ERecord (fields (xts, [])), loc))
158 end
159 132
160 | _ => e 133 | EField ((ERecord xes, _), (CName x, _), _) =>
134 (case List.find (fn ((CName x', _), _, _) => x' = x
135 | _ => false) xes of
136 SOME (_, e, _) => #1 e
137 | NONE => e)
138 | EWith (r as (_, loc), x, e, {rest = (CRecord (k, xts), _), field}) =>
139 let
140 fun fields (remaining, passed) =
141 case remaining of
142 [] => []
143 | (x, t) :: rest =>
144 (x,
145 (EField (r, x, {field = t,
146 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
147 t) :: fields (rest, (x, t) :: passed)
148 in
149 #1 (reduceExp env (ERecord ((x, e, field) :: fields (xts, [])), loc))
150 end
151 | ECut (r as (_, loc), _, {rest = (CRecord (k, xts), _), ...}) =>
152 let
153 fun fields (remaining, passed) =
154 case remaining of
155 [] => []
156 | (x, t) :: rest =>
157 (x,
158 (EField (r, x, {field = t,
159 rest = (CRecord (k, List.revAppend (passed, rest)), loc)}), loc),
160 t) :: fields (rest, (x, t) :: passed)
161 in
162 #1 (reduceExp env (ERecord (fields (xts, [])), loc))
163 end
164
165 | _ => e
166 in
167 (*Print.prefaces "exp'" [("e", CorePrint.p_exp env (e, ErrorMsg.dummySpan)),
168 ("r", CorePrint.p_exp env (r, ErrorMsg.dummySpan))];*)
169
170 r
171 end
161 172
162 and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env 173 and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env
163 174
164 fun decl env d = 175 fun decl env d =
165 case d of 176 case d of