Mercurial > urweb

comparison src/elab_env.sml @ 1796:0de0daab5fbb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove misguided type class optimization
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 10:04:58 -0400
parents d28adceef22a
children bb942416bf1c
comparison
equal deleted inserted replaced
1795:d28adceef22a 1796:0de0daab5fbb
161 | _ => e, 161 | _ => e,
162 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) 162 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
163 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) 163 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
164 | (ctx, _) => ctx} 164 | (ctx, _) => ctx}
165 165
166 val openCon =
167 U.Con.existsB {kind = fn ((nk, _), k) =>
168 case k of
169 KRel n => n >= nk
170 | _ => false,
171 con = fn ((_, nc), c) =>
172 case c of
173 CRel n => n >= nc
174 | _ => false,
175 bind = fn (all as (nk, nc), b) =>
176 case b of
177 U.Con.RelK _ => (nk+1, nc)
178 | U.Con.RelC _ => (nk, nc+1)
179 | _ => all}
180 (0, 0)
181
182 (* Back to environments *) 166 (* Back to environments *)
183 167
184 datatype 'a var' = 168 datatype 'a var' =
185 Rel' of int * 'a 169 Rel' of int * 'a
186 | Named' of int * 'a 170 | Named' of int * 'a
853 NONE => classes 837 NONE => classes
854 | SOME class => 838 | SOME class =>
855 let 839 let
856 val rule = (nvs, cs, c, (ERel 0, #2 t)) 840 val rule = (nvs, cs, c, (ERel 0, #2 t))
857 841
858 val class = 842 val class = {openRules = rule :: #openRules class,
859 if openCon t then 843 closedRules = #closedRules class}
860 {openRules = rule :: #openRules class,
861 closedRules = #closedRules class}
862 else
863 {closedRules = rule :: #closedRules class,
864 openRules = #openRules class}
865 in 844 in
866 CM.insert (classes, f, class) 845 CM.insert (classes, f, class)
867 end 846 end
868 in 847 in
869 {renameK = #renameK env, 848 {renameK = #renameK env,