diff options
author | Adam Chlipala <adam@chlipala.net> | 2013-04-21 13:03:20 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2013-04-21 13:03:20 -0400 |
commit | 2a577b6ff33994cd53f015296e545ae8d4840bfd (patch) | |
tree | e3bfbf4b7ed4c4dd06ff2fb3675f12b681aab5db /src | |
parent | 26a07c6a5fbf7b0c5791b1ccf2a933c0e2011d4a (diff) |
Get Iflow working again
Diffstat (limited to 'src')
-rw-r--r-- | src/iflow.sml | 95 | ||||
-rw-r--r-- | src/mono_reduce.sig | 4 | ||||
-rw-r--r-- | src/mono_reduce.sml | 36 |
3 files changed, 115 insertions, 20 deletions
diff --git a/src/iflow.sml b/src/iflow.sml index 8c933dc4..0c94cd47 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2010, Adam Chlipala +(* Copyright (c) 2010, 2013, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -1249,7 +1249,8 @@ type 'a doQuery = { fun doQuery (arg : 'a doQuery) (e as (_, loc)) = let - fun default () = ErrorMsg.errorAt loc "Information flow checker can't parse SQL query" + fun default () = (ErrorMsg.errorAt loc "Information flow checker can't parse SQL query"; + Print.preface ("Query", MonoPrint.p_exp MonoEnv.empty e)) in case parse query e of NONE => default () @@ -1795,16 +1796,103 @@ fun evalExp env (e as (_, loc)) k = datatype var_source = Input of int | SubInput of int | Unknown +structure U = MonoUtil + +fun mliftExpInExp by = + U.Exp.mapB {typ = fn t => t, + exp = fn bound => fn e => + case e of + ERel xn => + if xn < bound then + e + else + ERel (xn + by) + | _ => e, + bind = fn (bound, U.Exp.RelE _) => bound + 1 + | (bound, _) => bound} + +fun nameSubexps k (e : Mono.exp) = + let + fun numParams (e : Mono.exp) = + case #1 e of + EStrcat (e1, e2) => numParams e1 + numParams e2 + | EPrim (Prim.String _) => 0 + | _ => 1 + + val nps = numParams e + + fun getParams (e : Mono.exp) x = + case #1 e of + EStrcat (e1, e2) => + let + val (ps1, e1') = getParams e1 x + val (ps2, e2') = getParams e2 (x - length ps1) + in + (ps2 @ ps1, (EStrcat (e1', e2'), #2 e)) + end + | EPrim (Prim.String _) => ([], e) + | _ => + let + val (e', k) = + case #1 e of + EFfiApp (m, f, [(e', t)]) => + if Settings.isEffectful (m, f) orelse Settings.isBenignEffectful (m, f) then + (e, fn x => x) + else + (e', fn e' => (EFfiApp (m, f, [(e', t)]), #2 e)) + | ECase (e', ps as + [((PCon (_, PConFfi {mod = "Basis", con = "True", ...}, NONE), _), + (EPrim (Prim.String "TRUE"), _)), + ((PCon (_, PConFfi {mod = "Basis", con = "False", ...}, NONE), _), + (EPrim (Prim.String "FALSE"), _))], q) => + (e', fn e' => (ECase (e', ps, q), #2 e)) + | _ => (e, fn x => x) + in + ([e'], k (ERel x, #2 e)) + end + + val (ps, e') = getParams e (nps - 1) + + val string = (TFfi ("Basis", "string"), #2 e) + + val (e', _) = foldl (fn (p, (e', liftBy)) => + ((ELet ("p" ^ Int.toString liftBy, + string, + mliftExpInExp liftBy 0 p, + e'), #2 e), liftBy - 1)) (k (nps, e'), nps - 1) ps + in + #1 e' + end + +val namer = MonoUtil.File.map {typ = fn t => t, + exp = fn e => + case e of + EDml (e, fm) => + nameSubexps (fn (_, e') => (EDml (e', fm), #2 e)) e + | EQuery {exps, tables, state, query, body, initial} => + nameSubexps (fn (liftBy, e') => + (EQuery {exps = exps, + tables = tables, + state = state, + query = e', + body = mliftExpInExp liftBy 2 body, + initial = mliftExpInExp liftBy 0 initial}, + #2 query)) query + | _ => e, + decl = fn d => d} + fun check (file : file) = let val () = (St.reset (); rfuns := IM.empty) + (*val () = Print.preface ("FilePre", MonoPrint.p_file MonoEnv.empty file)*) val file = MonoReduce.reduce file val file = MonoOpt.optimize file val file = Fuse.fuse file val file = MonoOpt.optimize file val file = MonoShake.shake file + val file = namer file (*val () = Print.preface ("File", MonoPrint.p_file MonoEnv.empty file)*) val exptd = foldl (fn ((d, _), exptd) => @@ -2077,13 +2165,16 @@ fun check (file : file) = val check = fn file => let val oldInline = Settings.getMonoInline () + val oldFull = !MonoReduce.fullMode in (Settings.setMonoInline (case Int.maxInt of NONE => 1000000 | SOME n => n); + MonoReduce.fullMode := true; check file; Settings.setMonoInline oldInline) handle ex => (Settings.setMonoInline oldInline; + MonoReduce.fullMode := oldFull; raise ex) end diff --git a/src/mono_reduce.sig b/src/mono_reduce.sig index a6b6cc81..8990b21d 100644 --- a/src/mono_reduce.sig +++ b/src/mono_reduce.sig @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008, 2013, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -35,4 +35,6 @@ signature MONO_REDUCE = sig val impure : Mono.exp -> bool + val fullMode : bool ref + end diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml index 73adafa3..5bac235c 100644 --- a/src/mono_reduce.sml +++ b/src/mono_reduce.sml @@ -31,6 +31,8 @@ structure MonoReduce :> MONO_REDUCE = struct open Mono +val fullMode = ref false + structure E = MonoEnv structure U = MonoUtil @@ -531,27 +533,27 @@ fun reduce (file : file) = simpleImpure (timpures, impures) env e andalso impure e andalso not (List.null (summarize ~1 e)) + fun passive (e : exp) = + case #1 e of + EPrim _ => true + | ERel _ => true + | ENamed _ => true + | ECon (_, _, NONE) => true + | ECon (_, _, SOME e) => passive e + | ENone _ => true + | ESome (_, e) => passive e + | EFfi _ => true + | EAbs _ => true + | ERecord xets => List.all (passive o #2) xets + | EField (e, _) => passive e + | _ => false + fun exp env e = let (*val () = Print.prefaces "exp" [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan))]*) fun doLet (x, t, e', b) = let - fun passive (e : exp) = - case #1 e of - EPrim _ => true - | ERel _ => true - | ENamed _ => true - | ECon (_, _, NONE) => true - | ECon (_, _, SOME e) => passive e - | ENone _ => true - | ESome (_, e) => passive e - | EFfi _ => true - | EAbs _ => true - | ERecord xets => List.all (passive o #2) xets - | EField (e, _) => passive e - | _ => false - fun doSub () = let val r = subExpInExp (0, e') b @@ -630,7 +632,7 @@ fun reduce (file : file) = else e end - else if countFree 0 0 b > 1 andalso not (passive e') then + else if countFree 0 0 b > 1 andalso not (!fullMode) andalso not (passive e') then e else trySub () @@ -653,7 +655,7 @@ fun reduce (file : file) = ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp (E.pushERel env x t NONE) e1), ("e2", MonoPrint.p_exp env e2), ("sub", MonoPrint.p_exp env (reduceExp env (subExpInExp (0, e2) e1)))];*) - if impure env e2 orelse countFree 0 0 e1 > 1 then + if impure env e2 orelse (not (!fullMode) andalso countFree 0 0 e1 > 1) then #1 (reduceExp env (ELet (x, t, e2, e1), loc)) else #1 (reduceExp env (subExpInExp (0, e2) e1))) |