diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-03-16 10:09:01 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-03-16 10:09:01 -0400 |
| commit | e5e7bbaaae9cde0981c77e488a29e730876964ba (patch) | |
| tree | 32012eb864854a36e74947956e1133ce84cd64a7 /src/unpoly.sml | |
| parent | a00e028f21afd87ef9dd3ed143f52fe648275d45 (diff) | |
Undo an Especialize change that turned out to be unecessary
Diffstat (limited to 'src/unpoly.sml')
| -rw-r--r-- | src/unpoly.sml | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/src/unpoly.sml b/src/unpoly.sml index 41532b85..324e045c 100644 --- a/src/unpoly.sml +++ b/src/unpoly.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -46,11 +46,15 @@ val subConInCon = E.subConInCon val liftConInExp = E.liftConInExp val subConInExp = E.subConInExp -val isOpen = U.Con.exists {kind = fn _ => false, - con = fn c => - case c of - CRel _ => true - | _ => false} +val isOpen = U.Con.existsB {kind = fn _ => false, + con = fn (n, c) => + case c of + CRel n' => n' >= n + | _ => false, + bind = fn (n, b) => + case b of + U.Con.RelC _ => n + 1 + | _ => n} 0 fun unpolyNamed (xn, rep) = U.Exp.map {kind = fn k => k, @@ -142,9 +146,11 @@ fun exp (e, st : state) = | _ => NONE in (*Print.prefaces "specialize" - [("t", CorePrint.p_con CoreEnv.empty t), - ("e", CorePrint.p_exp CoreEnv.empty e), - ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) + [("n", Print.PD.string (Int.toString n)), + ("nold", Print.PD.string (Int.toString n_old)), + ("t", CorePrint.p_con CoreEnv.empty t), + ("e", CorePrint.p_exp CoreEnv.empty e), + ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*) Option.map (fn (t, e) => (x, n, n_old, t, e, s)) (trim (t, e, cargs)) end @@ -285,7 +291,7 @@ fun decl (d, st : state) = val irregular = U.Exp.existsB {kind = kind, con = con, exp = exp, bind = bind} 0 in if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then - (print "Poppycock!\n"; (d, st)) + (d, st) else (d, {funcs = foldl (fn (vi, funcs) => IM.insert (funcs, #2 vi, {kinds = cargs, |