Mercurial > urweb

comparison src/unnest.sml @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 366676f7bc88
children f152f215a02c
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
35 structure U = ElabUtil 35 structure U = ElabUtil
36 36
37 structure IS = IntBinarySet 37 structure IS = IntBinarySet
38 38
39 fun liftExpInExp by = 39 fun liftExpInExp by =
40 U.Exp.mapB {kind = fn k => k, 40 U.Exp.mapB {kind = fn _ => fn k => k,
41 con = fn _ => fn c => c, 41 con = fn _ => fn c => c,
42 exp = fn bound => fn e => 42 exp = fn bound => fn e =>
43 case e of 43 case e of
44 ERel xn => 44 ERel xn =>
45 if xn < bound then 45 if xn < bound then
49 | _ => e, 49 | _ => e,
50 bind = fn (bound, U.Exp.RelE _) => bound + 1 50 bind = fn (bound, U.Exp.RelE _) => bound + 1
51 | (bound, _) => bound} 51 | (bound, _) => bound}
52 52
53 val subExpInExp = 53 val subExpInExp =
54 U.Exp.mapB {kind = fn k => k, 54 U.Exp.mapB {kind = fn _ => fn k => k,
55 con = fn _ => fn c => c, 55 con = fn _ => fn c => c,
56 exp = fn (xn, rep) => fn e => 56 exp = fn (xn, rep) => fn e =>
57 case e of 57 case e of
58 ERel xn' => 58 ERel xn' =>
59 if xn' = xn then 59 if xn' = xn then
63 | _ => e, 63 | _ => e,
64 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep) 64 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep)
65 | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep) 65 | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep)
66 | (ctx, _) => ctx} 66 | (ctx, _) => ctx}
67 67
68 val fvsCon = U.Con.foldB {kind = fn (_, st) => st, 68 val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st,
69 con = fn (cb, c, cvs) => 69 con = fn (cb, c, cvs) =>
70 case c of 70 case c of
71 CRel n => 71 CRel n =>
72 if n >= cb then 72 if n >= cb then
73 IS.add (cvs, n - cb) 73 IS.add (cvs, n - cb)
74 else 74 else
75 cvs 75 cvs
76 | _ => cvs, 76 | _ => cvs,
77 bind = fn (cb, b) => 77 bind = fn (cb, b) =>
78 case b of 78 case b of
79 U.Con.Rel _ => cb + 1 79 U.Con.RelC _ => cb + 1
80 | _ => cb} 80 | _ => cb}
81 0 IS.empty 81 0 IS.empty
82 82
83 fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st, 83 fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st,
84 con = fn ((cb, eb), c, st as (cvs, evs)) => 84 con = fn ((cb, eb), c, st as (cvs, evs)) =>
85 case c of 85 case c of
86 CRel n => 86 CRel n =>
87 if n >= cb then 87 if n >= cb then
88 (IS.add (cvs, n - cb), evs) 88 (IS.add (cvs, n - cb), evs)
122 ^ String.concatWith ";" (map Int.toString ls) 122 ^ String.concatWith ";" (map Int.toString ls)
123 ^ ")") 123 ^ ")")
124 end 124 end
125 125
126 fun squishCon cfv = 126 fun squishCon cfv =
127 U.Con.mapB {kind = fn k => k, 127 U.Con.mapB {kind = fn _ => fn k => k,
128 con = fn cb => fn c => 128 con = fn cb => fn c =>
129 case c of 129 case c of
130 CRel n => 130 CRel n =>
131 if n >= cb then 131 if n >= cb then
132 CRel (positionOf (n - cb) cfv + cb) 132 CRel (positionOf (n - cb) cfv + cb)
133 else 133 else
134 c 134 c
135 | _ => c, 135 | _ => c,
136 bind = fn (cb, b) => 136 bind = fn (cb, b) =>
137 case b of 137 case b of
138 U.Con.Rel _ => cb + 1 138 U.Con.RelC _ => cb + 1
139 | _ => cb} 139 | _ => cb}
140 0 140 0
141 141
142 fun squishExp (nr, cfv, efv) = 142 fun squishExp (nr, cfv, efv) =
143 U.Exp.mapB {kind = fn k => k, 143 U.Exp.mapB {kind = fn _ => fn k => k,
144 con = fn (cb, eb) => fn c => 144 con = fn (cb, eb) => fn c =>
145 case c of 145 case c of
146 CRel n => 146 CRel n =>
147 if n >= cb then 147 if n >= cb then
148 CRel (positionOf (n - cb) cfv + cb) 148 CRel (positionOf (n - cb) cfv + cb)
167 type state = { 167 type state = {
168 maxName : int, 168 maxName : int,
169 decls : (string * int * con * exp) list 169 decls : (string * int * con * exp) list
170 } 170 }
171 171
172 fun kind (k, st) = (k, st) 172 fun kind (_, k, st) = (k, st)
173 173
174 fun exp ((ks, ts), e as old, st : state) = 174 fun exp ((ks, ts), e as old, st : state) =
175 case e of 175 case e of
176 ELet (eds, e) => 176 ELet (eds, e) =>
177 let 177 let