From e5e7bbaaae9cde0981c77e488a29e730876964ba Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 16 Mar 2010 10:09:01 -0400 Subject: Undo an Especialize change that turned out to be unecessary --- src/compiler.sml | 2 +- src/core_util.sig | 5 +++++ src/core_util.sml | 17 ++++++++++++++- src/especialize.sml | 62 +++++++++++------------------------------------------ src/unpoly.sml | 26 +++++++++++++--------- tests/unpoly.ur | 28 ++++++++++++++++++++++++ tests/unpoly.urp | 2 ++ tests/unpoly.urs | 1 + 8 files changed, 82 insertions(+), 61 deletions(-) create mode 100644 tests/unpoly.ur create mode 100644 tests/unpoly.urp create mode 100644 tests/unpoly.urs diff --git a/src/compiler.sml b/src/compiler.sml index f8c0cc34..a7a3c117 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -1085,7 +1085,7 @@ val toMono_reduce2 = transform mono_reduce "mono_reduce2" o toUntangle2 val toMono_shake2 = transform mono_shake "mono_shake2" o toMono_reduce2 val toMono_opt4 = transform mono_opt "mono_opt4" o toMono_shake2 val toMono_reduce3 = transform mono_reduce "mono_reduce3" o toMono_opt4 -val toFuse2 = transform fuse "shake2" o toMono_reduce3 +val toFuse2 = transform fuse "fuse2" o toMono_reduce3 val toUntangle3 = transform untangle "untangle3" o toFuse2 val toMono_shake3 = transform mono_shake "mono_shake3" o toUntangle3 diff --git a/src/core_util.sig b/src/core_util.sig index 807b477b..835577a3 100644 --- a/src/core_util.sig +++ b/src/core_util.sig @@ -73,6 +73,11 @@ structure Con : sig val exists : {kind : Core.kind' -> bool, con : Core.con' -> bool} -> Core.con -> bool + + val existsB : {kind : 'context * Core.kind' -> bool, + con : 'context * Core.con' -> bool, + bind : 'context * binder -> 'context} + -> 'context -> Core.con -> bool val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state, con : Core.con' * 'state -> Core.con' * 'state} diff --git a/src/core_util.sml b/src/core_util.sml index 599e1abc..247dd32e 100644 --- a/src/core_util.sml +++ b/src/core_util.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 @@ -375,6 +375,21 @@ fun exists {kind, con} k = S.Return _ => true | S.Continue _ => false +fun existsB {kind, con, bind} ctx c = + case mapfoldB {kind = fn ctx => fn k => fn () => + if kind (ctx, k) then + S.Return () + else + S.Continue (k, ()), + con = fn ctx => fn c => fn () => + if con (ctx, c) then + S.Return () + else + S.Continue (c, ()), + bind = bind} ctx c () of + S.Return _ => true + | S.Continue _ => false + fun foldMap {kind, con} s c = case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)), con = fn c => fn s => S.Continue (con (c, s))} c s of diff --git a/src/especialize.sml b/src/especialize.sml index b0a4a8c2..7d129b8b 100644 --- a/src/especialize.sml +++ b/src/especialize.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2009, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -43,13 +43,6 @@ structure KM = BinaryMapFn(K) structure IM = IntBinaryMap structure IS = IntBinarySet -val isOpen = U.Exp.exists {kind = fn _ => false, - con = fn c => - case c of - CRel _ => true - | _ => false, - exp = fn _ => false} - val freeVars = U.Exp.foldB {kind = fn (_, _, xs) => xs, con = fn (_, _, xs) => xs, exp = fn (bound, e, xs) => @@ -136,37 +129,6 @@ val mayNotSpec = ref SS.empty fun specialize' (funcs, specialized) file = let - fun functionInside functiony = U.Con.exists {kind = fn _ => false, - con = fn TFun _ => true - | CFfi ("Basis", "transaction") => true - | CFfi ("Basis", "eq") => true - | CFfi ("Basis", "num") => true - | CFfi ("Basis", "ord") => true - | CFfi ("Basis", "show") => true - | CFfi ("Basis", "read") => true - | CFfi ("Basis", "sql_injectable_prim") => true - | CFfi ("Basis", "sql_injectable") => true - | CNamed n => IS.member (functiony, n) - | _ => false} - - val functiony = foldl (fn ((d, _), functiony) => - case d of - DCon (_, n, _, c) => - if functionInside functiony c then - IS.add (functiony, n) - else - functiony - | DDatatype dts => - if List.exists (fn (_, _, _, cs) => - List.exists (fn (_, _, SOME c) => functionInside functiony c - | _ => false) cs) dts then - IS.addList (functiony, map #2 dts) - else - functiony - | _ => functiony) IS.empty file - - val functionInside = functionInside functiony - fun bind (env, b) = case b of U.Decl.RelE xt => xt :: env @@ -228,12 +190,7 @@ fun specialize' (funcs, specialized) file = in ((ECApp (e, c), loc), st) end - | ECAbs (x, k, e) => - let - val (e, st) = exp (env, e, st) - in - ((ECAbs (x, k, e), loc), st) - end + | ECAbs _ => (e, st) | EKAbs _ => (e, st) | EKApp (e, k) => let @@ -329,7 +286,17 @@ fun specialize' (funcs, specialized) file = (*val () = Print.prefaces "Consider" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*) - + val functionInside = U.Con.exists {kind = fn _ => false, + con = fn TFun _ => true + | CFfi ("Basis", "transaction") => true + | CFfi ("Basis", "eq") => true + | CFfi ("Basis", "num") => true + | CFfi ("Basis", "ord") => true + | CFfi ("Basis", "show") => true + | CFfi ("Basis", "read") => true + | CFfi ("Basis", "sql_injectable_prim") => true + | CFfi ("Basis", "sql_injectable") => true + | _ => false} val loc = ErrorMsg.dummySpan fun findSplit av (xs, typ, fxs, fvs, fin) = @@ -361,13 +328,10 @@ fun specialize' (funcs, specialized) file = if not fin orelse List.all (fn (ERel _, _) => true | _ => false) fxs' - orelse List.exists isOpen fxs' orelse (IS.numItems fvs >= length fxs andalso IS.exists (fn n => functionInside (#2 (List.nth (env, n)))) fvs) then ((*Print.prefaces "No" [("name", Print.PD.string name), ("f", Print.PD.string (Int.toString f)), - ("xs", - Print.p_list (CorePrint.p_exp CoreEnv.empty) xs), ("fxs'", Print.p_list (CorePrint.p_exp CoreEnv.empty) fxs')];*) default ()) 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, diff --git a/tests/unpoly.ur b/tests/unpoly.ur new file mode 100644 index 00000000..706f3653 --- /dev/null +++ b/tests/unpoly.ur @@ -0,0 +1,28 @@ +val current = return (Some "1") +fun resolve (_ : string) = return (Some "2") + +fun checkDeps deps = + u <- current; + List.foldlM (fn s (good, errs) => + v' <- resolve s; + case v' of + None => + return (False, + {errs} + Unknown library path {[s]}.
+ ) + | Some v' => + b <- return True; + if b then + return (good, errs) + else + return (False, + {errs} + Access denied to {[s]}.
+ )) (True, ) deps + +fun main () = + p <- checkDeps ("a" :: "b" :: []); + return + {p.2} + diff --git a/tests/unpoly.urp b/tests/unpoly.urp new file mode 100644 index 00000000..106bd20d --- /dev/null +++ b/tests/unpoly.urp @@ -0,0 +1,2 @@ +$/list +unpoly diff --git a/tests/unpoly.urs b/tests/unpoly.urs new file mode 100644 index 00000000..6ac44e0b --- /dev/null +++ b/tests/unpoly.urs @@ -0,0 +1 @@ +val main : unit -> transaction page -- cgit v1.2.3