aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-04-21 13:03:20 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2013-04-21 13:03:20 -0400
commit52a39c41846b52cd9b93bf53fb709eea75704cca (patch)
treee3bfbf4b7ed4c4dd06ff2fb3675f12b681aab5db
parenteb7b751e19b527f8d72ba9b24a3158afb192750f (diff)
Get Iflow working again
-rw-r--r--src/iflow.sml95
-rw-r--r--src/mono_reduce.sig4
-rw-r--r--src/mono_reduce.sml36
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)))