Mercurial > urweb

comparison src/unpoly.sml @ 1185:338be96f8533

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Undo an Especialize change that turned out to be unecessary
author Adam Chlipala <adamc@hcoop.net>
date Tue, 16 Mar 2010 10:09:01 -0400
parents ac3dbbc85c6e
children 5b5c0b552f59
comparison
equal deleted inserted replaced
1184:d6f0e972b706 1185:338be96f8533
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
44 val subConInCon = E.subConInCon 44 val subConInCon = E.subConInCon
45 45
46 val liftConInExp = E.liftConInExp 46 val liftConInExp = E.liftConInExp
47 val subConInExp = E.subConInExp 47 val subConInExp = E.subConInExp
48 48
49 val isOpen = U.Con.exists {kind = fn _ => false, 49 val isOpen = U.Con.existsB {kind = fn _ => false,
50 con = fn c => 50 con = fn (n, c) =>
51 case c of 51 case c of
52 CRel _ => true 52 CRel n' => n' >= n
53 | _ => false} 53 | _ => false,
54 bind = fn (n, b) =>
55 case b of
56 U.Con.RelC _ => n + 1
57 | _ => n} 0
54 58
55 fun unpolyNamed (xn, rep) = 59 fun unpolyNamed (xn, rep) =
56 U.Exp.map {kind = fn k => k, 60 U.Exp.map {kind = fn k => k,
57 con = fn c => c, 61 con = fn c => c,
58 exp = fn e => 62 exp = fn e =>
140 end 144 end
141 | (_, _, []) => SOME (t, e) 145 | (_, _, []) => SOME (t, e)
142 | _ => NONE 146 | _ => NONE
143 in 147 in
144 (*Print.prefaces "specialize" 148 (*Print.prefaces "specialize"
145 [("t", CorePrint.p_con CoreEnv.empty t), 149 [("n", Print.PD.string (Int.toString n)),
146 ("e", CorePrint.p_exp CoreEnv.empty e), 150 ("nold", Print.PD.string (Int.toString n_old)),
147 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) 151 ("t", CorePrint.p_con CoreEnv.empty t),
152 ("e", CorePrint.p_exp CoreEnv.empty e),
153 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
148 Option.map (fn (t, e) => (x, n, n_old, t, e, s)) 154 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
149 (trim (t, e, cargs)) 155 (trim (t, e, cargs))
150 end 156 end
151 157
152 val vis = List.map specialize vis 158 val vis = List.map specialize vis
283 | _ => cn 289 | _ => cn
284 290
285 val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0 291 val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0
286 in 292 in
287 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then 293 if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
288 (print "Poppycock!\n"; (d, st)) 294 (d, st)
289 else 295 else
290 (d, {funcs = foldl (fn (vi, funcs) => 296 (d, {funcs = foldl (fn (vi, funcs) =>
291 IM.insert (funcs, #2 vi, {kinds = cargs, 297 IM.insert (funcs, #2 vi, {kinds = cargs,
292 defs = vis, 298 defs = vis,
293 replacements = M.empty})) 299 replacements = M.empty}))