Mercurial > urweb

comparison src/reduce.sml @ 74:144d082b47ae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reduce efold
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Jun 2008 12:12:06 -0400
parents 2e0f3b21fb85
children 813e5a52063d
comparison
equal deleted inserted replaced
73:8b611ecc5f2d 74:144d082b47ae
39 val subConInCon = 39 val subConInCon =
40 U.Con.mapB {kind = fn k => k, 40 U.Con.mapB {kind = fn k => k,
41 con = fn (xn, rep) => fn c => 41 con = fn (xn, rep) => fn c =>
42 case c of 42 case c of
43 CRel xn' => 43 CRel xn' =>
44 if xn = xn' then 44 (case Int.compare (xn', xn) of
45 #1 rep 45 EQUAL => #1 rep
46 else 46 | GREATER => CRel (xn' - 1)
47 c 47 | LESS => 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 = 52 val liftExpInExp =
67 U.Exp.mapB {kind = fn k => k, 67 U.Exp.mapB {kind = fn k => k,
68 con = fn _ => fn c => c, 68 con = fn _ => fn c => c,
69 exp = fn (xn, rep) => fn e => 69 exp = fn (xn, rep) => fn e =>
70 case e of 70 case e of
71 ERel xn' => 71 ERel xn' =>
72 if xn = xn' then 72 (case Int.compare (xn', xn) of
73 #1 rep 73 EQUAL => #1 rep
74 else 74 | GREATER=> ERel (xn' - 1)
75 e 75 | LESS => e)
76 | _ => e, 76 | _ => e,
77 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) 77 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
78 | (ctx, _) => ctx} 78 | (ctx, _) => ctx}
79 79
80 val liftConInExp = 80 val liftConInExp =
94 val subConInExp = 94 val subConInExp =
95 U.Exp.mapB {kind = fn k => k, 95 U.Exp.mapB {kind = fn k => k,
96 con = fn (xn, rep) => fn c => 96 con = fn (xn, rep) => fn c =>
97 case c of 97 case c of
98 CRel xn' => 98 CRel xn' =>
99 if xn = xn' then 99 (case Int.compare (xn', xn) of
100 #1 rep 100 EQUAL => #1 rep
101 else 101 | GREATER => CRel (xn' - 1)
102 c 102 | LESS => c)
103 | _ => c, 103 | _ => c,
104 exp = fn _ => fn e => e, 104 exp = fn _ => fn e => e,
105 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) 105 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
106 | (ctx, _) => ctx} 106 | (ctx, _) => ctx}
107 107
144 ENamed n => 144 ENamed n =>
145 (case E.lookupENamed env n of 145 (case E.lookupENamed env n of
146 (_, _, SOME e') => #1 e' 146 (_, _, SOME e') => #1 e'
147 | _ => e) 147 | _ => e)
148 148
149 | ECApp ((EApp ((EApp ((ECApp ((EFold ks, _), ran), _), f), _), i), _), (CRecord (k, xcs), loc)) =>
150 (case xcs of
151 [] => #1 i
152 | (n, v) :: rest =>
153 #1 (reduceExp env (EApp ((ECApp ((ECApp ((ECApp (f, n), loc), v), loc), (CRecord (k, rest), loc)), loc),
154 (ECApp ((EApp ((EApp ((ECApp ((EFold ks, loc), ran), loc), f), loc), i), loc),
155 (CRecord (k, rest), loc)), loc)), loc)))
156
149 | EApp ((EAbs (_, _, _, e1), loc), e2) => 157 | EApp ((EAbs (_, _, _, e1), loc), e2) =>
150 #1 (reduceExp env (subExpInExp (0, e2) e1)) 158 #1 (reduceExp env (subExpInExp (0, e2) e1))
151 | ECApp ((ECAbs (_, _, e1), loc), c) => 159 | ECApp ((ECAbs (_, _, e1), loc), c) =>
152 #1 (reduceExp env (subConInExp (0, c) e1)) 160 #1 (reduceExp env (subConInExp (0, c) e1))
153 161