Mercurial > urweb

comparison src/elab_util.sml @ 345:b85e6ba56618

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge CDisjoint and TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 15:50:28 -0400
parents 075b36dbb1a4
children dfc8c991abd0
comparison
equal deleted inserted replaced
344:3c0feecd057d 345:b85e6ba56618
117 S.bind2 (mfk k, 117 S.bind2 (mfk k,
118 fn k' => 118 fn k' =>
119 S.map2 (mfc (bind (ctx, Rel (x, k))) c, 119 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
120 fn c' => 120 fn c' =>
121 (TCFun (e, x, k', c'), loc))) 121 (TCFun (e, x, k', c'), loc)))
122 | TDisjoint (ai, c1, c2, c3) => 122 | CDisjoint (ai, c1, c2, c3) =>
123 S.bind2 (mfc ctx c1, 123 S.bind2 (mfc ctx c1,
124 fn c1' => 124 fn c1' =>
125 S.bind2 (mfc ctx c2, 125 S.bind2 (mfc ctx c2,
126 fn c2' => 126 fn c2' =>
127 S.map2 (mfc ctx c3, 127 S.map2 (mfc ctx c3,
128 fn c3' => 128 fn c3' =>
129 (TDisjoint (ai, c1', c2', c3'), loc)))) 129 (CDisjoint (ai, c1', c2', c3'), loc))))
130 | TRecord c => 130 | TRecord c =>
131 S.map2 (mfc ctx c, 131 S.map2 (mfc ctx c,
132 fn c' => 132 fn c' =>
133 (TRecord c', loc)) 133 (TRecord c', loc))
134 134
145 S.bind2 (mfk k, 145 S.bind2 (mfk k,
146 fn k' => 146 fn k' =>
147 S.map2 (mfc (bind (ctx, Rel (x, k))) c, 147 S.map2 (mfc (bind (ctx, Rel (x, k))) c,
148 fn c' => 148 fn c' =>
149 (CAbs (x, k', c'), loc))) 149 (CAbs (x, k', c'), loc)))
150 | CDisjoint (c1, c2, c3) =>
151 S.bind2 (mfc ctx c1,
152 fn c1' =>
153 S.bind2 (mfc ctx c2,
154 fn c2' =>
155 S.map2 (mfc ctx c3,
156 fn c3' =>
157 (CDisjoint (c1', c2', c3'), loc))))
158 150
159 | CName _ => S.return2 cAll 151 | CName _ => S.return2 cAll
160 152
161 | CRecord (k, xcs) => 153 | CRecord (k, xcs) =>
162 S.bind2 (mfk k, 154 S.bind2 (mfk k,