From 5ec949e910342f6212c85c8df75283d091817408 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 15 Jan 2011 14:53:13 -0500 Subject: Allow subqueries to reference aggregate-only columns of free tables; treat non-COUNT aggregate functions as possibly returning NULL --- lib/ur/basis.urs | 54 ++++++++++++++++++++++++--------------------- lib/ur/list.ur | 6 ++--- lib/ur/list.urs | 6 ++--- lib/ur/top.ur | 36 +++++++++++++++--------------- lib/ur/top.urs | 36 +++++++++++++++--------------- src/compiler.sml | 10 +++++++-- src/mono_env.sig | 3 ++- src/mono_env.sml | 13 +++++++++++ src/mono_reduce.sml | 39 +++++++++++++++++++++------------ src/monoize.sml | 63 ++++++++++++++++++++++------------------------------- 10 files changed, 145 insertions(+), 121 deletions(-) diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index a91fd498..8ca2e81c 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -291,8 +291,8 @@ val check : fs ::: {Type} (*** Queries *) -con sql_query :: {{Type}} -> {{Type}} -> {Type} -> Type -con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type +con sql_query :: {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type +con sql_query1 :: {{Type}} -> {{Type}} -> {{Type}} -> {{Type}} -> {Type} -> Type con sql_subset :: {{Type}} -> {{Type}} -> Type val sql_subset : keep_drop :: {({Type} * {Type})} @@ -314,7 +314,7 @@ val sql_from_table : free ::: {{Type}} -> t ::: Type -> fs ::: {Type} -> fieldsOf t fs -> name :: Name -> t -> sql_from_items free [name = fs] val sql_from_query : free ::: {{Type}} -> fs ::: {Type} -> name :: Name - -> sql_query free [] fs + -> sql_query free [] [] fs -> sql_from_items free [name = fs] val sql_from_comma : free ::: {{Type}} -> tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} -> [tabs1 ~ tabs2] @@ -353,6 +353,7 @@ val sql_full_join : free ::: {{Type}} -> tabs1 ::: {{(Type * Type)}} -> tabs2 :: -> sql_from_items free (map (map (fn p :: (Type * Type) => p.2)) (tabs1 ++ tabs2)) val sql_query1 : free ::: {{Type}} + -> afree ::: {{Type}} -> tables ::: {{Type}} -> grouped ::: {{Type}} -> selectedFields ::: {{Type}} @@ -360,33 +361,35 @@ val sql_query1 : free ::: {{Type}} -> empties :: {Unit} -> [free ~ tables] => [free ~ grouped] + => [afree ~ tables] => [empties ~ selectedFields] => {Distinct : bool, From : sql_from_items free tables, - Where : sql_exp (free ++ tables) [] [] bool, + Where : sql_exp (free ++ tables) afree [] bool, GroupBy : sql_subset tables grouped, - Having : sql_exp (free ++ grouped) tables [] bool, + Having : sql_exp (free ++ grouped) (afree ++ tables) [] bool, SelectFields : sql_subset grouped (map (fn _ => []) empties ++ selectedFields), - SelectExps : $(map (sql_exp (free ++ grouped) tables []) + SelectExps : $(map (sql_exp (free ++ grouped) (afree ++ tables) []) selectedExps) } - -> sql_query1 free tables selectedFields selectedExps + -> sql_query1 free afree tables selectedFields selectedExps type sql_relop val sql_union : sql_relop val sql_intersect : sql_relop val sql_except : sql_relop val sql_relop : free ::: {{Type}} + -> afree ::: {{Type}} -> tables1 ::: {{Type}} -> tables2 ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} -> sql_relop - -> sql_query1 free tables1 selectedFields selectedExps - -> sql_query1 free tables2 selectedFields selectedExps - -> sql_query1 free [] selectedFields selectedExps -val sql_forget_tables : free ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} - -> sql_query1 free tables selectedFields selectedExps - -> sql_query1 free [] selectedFields selectedExps + -> sql_query1 free afree tables1 selectedFields selectedExps + -> sql_query1 free afree tables2 selectedFields selectedExps + -> sql_query1 free afree [] selectedFields selectedExps +val sql_forget_tables : free ::: {{Type}} -> afree ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} + -> sql_query1 free afree tables selectedFields selectedExps + -> sql_query1 free afree [] selectedFields selectedExps type sql_direction val sql_asc : sql_direction @@ -408,15 +411,16 @@ val sql_no_offset : sql_offset val sql_offset : int -> sql_offset val sql_query : free ::: {{Type}} + -> afree ::: {{Type}} -> tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} -> [free ~ tables] - => {Rows : sql_query1 free tables selectedFields selectedExps, + => {Rows : sql_query1 free afree tables selectedFields selectedExps, OrderBy : sql_order_by (free ++ tables) selectedExps, Limit : sql_limit, Offset : sql_offset} - -> sql_query free selectedFields selectedExps + -> sql_query free afree selectedFields selectedExps val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}} @@ -493,8 +497,8 @@ class sql_summable val sql_summable_int : sql_summable int val sql_summable_float : sql_summable float val sql_summable_option : t ::: Type -> sql_summable t -> sql_summable (option t) -val sql_avg : t ::: Type -> sql_summable t -> sql_aggregate t t -val sql_sum : t ::: Type -> sql_summable t -> sql_aggregate t t +val sql_avg : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt +val sql_sum : t ::: Type -> nt ::: Type -> sql_summable t -> nullify t nt -> sql_aggregate t nt class sql_maxable val sql_maxable_int : sql_maxable int @@ -502,8 +506,8 @@ val sql_maxable_float : sql_maxable float val sql_maxable_string : sql_maxable string val sql_maxable_time : sql_maxable time val sql_maxable_option : t ::: Type -> sql_maxable t -> sql_maxable (option t) -val sql_max : t ::: Type -> sql_maxable t -> sql_aggregate t t -val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t t +val sql_max : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt +val sql_min : t ::: Type -> nt ::: Type -> sql_maxable t -> nullify t nt -> sql_aggregate t nt con sql_nfunc :: Type -> Type val sql_nfunc : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} @@ -526,7 +530,7 @@ val sql_nullable : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> -> sql_exp tables agg exps (option t) val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> nm ::: Name -> t ::: Type - -> sql_query tables [] [nm = t] + -> sql_query tables agg [] [nm = t] -> sql_exp tables agg exps t (*** Executing queries *) @@ -534,7 +538,7 @@ val sql_subquery : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> val query : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] => state ::: Type - -> sql_query [] tables exps + -> sql_query [] [] tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> state -> transaction state) @@ -838,21 +842,21 @@ val periodic : int -> task_kind unit type sql_policy val sendClient : tables ::: {{Type}} -> exps ::: {Type} - -> [tables ~ exps] => sql_query [] tables exps + -> [tables ~ exps] => sql_query [] [] tables exps -> sql_policy val sendOwnIds : sql_sequence -> sql_policy val mayInsert : fs ::: {Type} -> tables ::: {{Type}} -> [[New] ~ tables] - => sql_query [] ([New = fs] ++ tables) [] + => sql_query [] [] ([New = fs] ++ tables) [] -> sql_policy val mayDelete : fs ::: {Type} -> tables ::: {{Type}} -> [[Old] ~ tables] - => sql_query [] ([Old = fs] ++ tables) [] + => sql_query [] [] ([Old = fs] ++ tables) [] -> sql_policy val mayUpdate : fs ::: {Type} -> tables ::: {{Type}} -> [[Old, New] ~ tables] - => sql_query [] ([Old = fs, New = fs] ++ tables) [] + => sql_query [] [] ([Old = fs, New = fs] ++ tables) [] -> sql_policy val also : sql_policy -> sql_policy -> sql_policy diff --git a/lib/ur/list.ur b/lib/ur/list.ur index 3153cc32..d0c2e7a1 100644 --- a/lib/ur/list.ur +++ b/lib/ur/list.ur @@ -254,7 +254,7 @@ fun app [m] (_ : monad m) [a] f = end fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type] - [tables ~ exps] (q : sql_query [] tables exps) + [tables ~ exps] (q : sql_query [] [] tables exps) (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) = ls <- query q (fn fs acc => return (f fs :: acc)) @@ -262,7 +262,7 @@ fun mapQuery [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type] return (rev ls) fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type] - [tables ~ exps] (q : sql_query [] tables exps) + [tables ~ exps] (q : sql_query [] [] tables exps) (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) = ls <- query q (fn fs acc => v <- f fs; return (v :: acc)) @@ -270,7 +270,7 @@ fun mapQueryM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type] return (rev ls) fun mapQueryPartialM [tables ::: {{Type}}] [exps ::: {Type}] [t ::: Type] - [tables ~ exps] (q : sql_query [] tables exps) + [tables ~ exps] (q : sql_query [] [] tables exps) (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) = ls <- query q (fn fs acc => v <- f fs; diff --git a/lib/ur/list.urs b/lib/ur/list.urs index 9ad738f1..8284510d 100644 --- a/lib/ur/list.urs +++ b/lib/ur/list.urs @@ -53,19 +53,19 @@ val app : m ::: (Type -> Type) -> monad m -> a ::: Type val mapQuery : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> t) -> transaction (list t) val mapQueryM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction t) -> transaction (list t) val mapQueryPartialM : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (option t)) -> transaction (list t) diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 83d5b6af..0fdbae7a 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -215,40 +215,40 @@ fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: { {f [nm] [t] [rest] ! r1 r2 r3}{acc}) -fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] []) +fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] []) (f : $fs -> state -> transaction state) (i : state) = query q (fn r => f r.t) i -fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [t = fs] []) +fun query1' [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] []) (f : $fs -> state -> state) (i : state) = query q (fn r s => return (f r.t s)) i -fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] tables exps) = +fun queryL [tables] [exps] [tables ~ exps] (q : sql_query [] [] tables exps) = query q (fn r ls => return (r :: ls)) [] -fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [t = fs] []) = +fun queryL1 [t ::: Name] [fs ::: {Type}] (q : sql_query [] [] [t = fs] []) = query q (fn r ls => return (r.t :: ls)) [] fun queryI [tables ::: {{Type}}] [exps ::: {Type}] - [tables ~ exps] (q : sql_query [] tables exps) + [tables ~ exps] (q : sql_query [] [] tables exps) (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction unit) = query q (fn fs _ => f fs) () -fun queryI1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) +fun queryI1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) (f : $fs -> transaction unit) = query q (fn fs _ => f fs.nm) () fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] - [tables ~ exps] (q : sql_query [] tables exps) + [tables ~ exps] (q : sql_query [] [] tables exps) (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> xml ctx inp []) = query q @@ -256,14 +256,14 @@ fun queryX [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Ty fun queryX1 [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] - (q : sql_query [] [nm = fs] []) + (q : sql_query [] [] [nm = fs] []) (f : $fs -> xml ctx inp []) = query q (fn fs acc => return {acc}{f fs.nm}) fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] - [tables ~ exps] (q : sql_query [] tables exps) + [tables ~ exps] (q : sql_query [] [] tables exps) (f : $(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (xml ctx inp [])) = query q @@ -273,7 +273,7 @@ fun queryX' [tables ::: {{Type}}] [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {T fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] - (q : sql_query [] [nm = fs] []) + (q : sql_query [] [] [nm = fs] []) (f : $fs -> transaction (xml ctx inp [])) = query q (fn fs acc => @@ -282,7 +282,7 @@ fun queryX1' [nm ::: Name] [fs ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] - (q : sql_query [] [] exps) + (q : sql_query [] [] [] exps) (f : $exps -> transaction (xml ctx inp [])) = query q (fn fs acc => @@ -292,42 +292,42 @@ fun queryXE' [exps ::: {Type}] [ctx ::: {Unit}] [inp ::: {Type}] fun hasRows [tables ::: {{Type}}] [exps ::: {Type}] [tables ~ exps] - (q : sql_query [] tables exps) = + (q : sql_query [] [] tables exps) = query q (fn _ _ => return True) False fun oneOrNoRows [tables ::: {{Type}}] [exps ::: {Type}] [tables ~ exps] - (q : sql_query [] tables exps) = + (q : sql_query [] [] tables exps) = query q (fn fs _ => return (Some fs)) None -fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) = +fun oneOrNoRows1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) = query q (fn fs _ => return (Some fs.nm)) None -fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) = +fun oneOrNoRowsE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) = query q (fn fs _ => return (Some fs.nm)) None fun oneRow [tables ::: {{Type}}] [exps ::: {Type}] - [tables ~ exps] (q : sql_query [] tables exps) = + [tables ~ exps] (q : sql_query [] [] tables exps) = o <- oneOrNoRows q; return (case o of None => error Query returned no rows | Some r => r) -fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [nm = fs] []) = +fun oneRow1 [nm ::: Name] [fs ::: {Type}] (q : sql_query [] [] [nm = fs] []) = o <- oneOrNoRows q; return (case o of None => error Query returned no rows | Some r => r.nm) -fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] (mapU [] tabs) [nm = t]) = +fun oneRowE1 [tabs ::: {Unit}] [nm ::: Name] [t ::: Type] [tabs ~ [nm]] (q : sql_query [] [] (mapU [] tabs) [nm = t]) = o <- oneOrNoRows q; return (case o of None => error Query returned no rows diff --git a/lib/ur/top.urs b/lib/ur/top.urs index d86ae553..ed3b4c14 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -126,100 +126,100 @@ val mapX3 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) val queryL : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> transaction (list $(exps ++ map (fn fields :: {Type} => $fields) tables)) val queryL1 : t ::: Name -> fs ::: {Type} - -> sql_query [] [t = fs] [] + -> sql_query [] [] [t = fs] [] -> transaction (list $fs) val query1 : t ::: Name -> fs ::: {Type} -> state ::: Type - -> sql_query [] [t = fs] [] + -> sql_query [] [] [t = fs] [] -> ($fs -> state -> transaction state) -> state -> transaction state val query1' : t ::: Name -> fs ::: {Type} -> state ::: Type - -> sql_query [] [t = fs] [] + -> sql_query [] [] [t = fs] [] -> ($fs -> state -> state) -> state -> transaction state val queryI : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction unit) -> transaction unit val queryI1 : nm ::: Name -> fs ::: {Type} - -> sql_query [] [nm = fs] [] + -> sql_query [] [] [nm = fs] [] -> ($fs -> transaction unit) -> transaction unit val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type} -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> xml ctx inp []) -> transaction (xml ctx inp []) val queryX1 : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type} - -> sql_query [] [nm = fs] [] + -> sql_query [] [] [nm = fs] [] -> ($fs -> xml ctx inp []) -> transaction (xml ctx inp []) val queryX' : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type} -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> ($(exps ++ map (fn fields :: {Type} => $fields) tables) -> transaction (xml ctx inp [])) -> transaction (xml ctx inp []) val queryX1' : nm ::: Name -> fs ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type} - -> sql_query [] [nm = fs] [] + -> sql_query [] [] [nm = fs] [] -> ($fs -> transaction (xml ctx inp [])) -> transaction (xml ctx inp []) val queryXE' : exps ::: {Type} -> ctx ::: {Unit} -> inp ::: {Type} - -> sql_query [] [] exps + -> sql_query [] [] [] exps -> ($exps -> transaction (xml ctx inp [])) -> transaction (xml ctx inp []) val hasRows : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> transaction bool val oneOrNoRows : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> transaction (option $(exps ++ map (fn fields :: {Type} => $fields) tables)) val oneOrNoRows1 : nm ::: Name -> fs ::: {Type} - -> sql_query [] [nm = fs] [] + -> sql_query [] [] [nm = fs] [] -> transaction (option $fs) val oneOrNoRowsE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type -> [tabs ~ [nm]] => - sql_query [] (mapU [] tabs) [nm = t] + sql_query [] [] (mapU [] tabs) [nm = t] -> transaction (option t) val oneRow : tables ::: {{Type}} -> exps ::: {Type} -> [tables ~ exps] => - sql_query [] tables exps + sql_query [] [] tables exps -> transaction $(exps ++ map (fn fields :: {Type} => $fields) tables) val oneRow1 : nm ::: Name -> fs ::: {Type} - -> sql_query [] [nm = fs] [] + -> sql_query [] [] [nm = fs] [] -> transaction $fs val oneRowE1 : tabs ::: {Unit} -> nm ::: Name -> t ::: Type -> [tabs ~ [nm]] => - sql_query [] (mapU [] tabs) [nm = t] + sql_query [] [] (mapU [] tabs) [nm = t] -> transaction t val nonempty : fs ::: {Type} -> us ::: {{Unit}} -> sql_table fs us diff --git a/src/compiler.sml b/src/compiler.sml index c8bb036a..61fa23b1 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -1311,9 +1311,15 @@ fun compileC {cname, oname, ename, libs, profile, debug, link = link'} = (compile, link) val link = foldl (fn (s, link) => link ^ " " ^ s) link link' + + fun system s = + (if debug then + print (s ^ "\n") + else + (); + OS.Process.isSuccess (OS.Process.system s)) in - OS.Process.isSuccess (OS.Process.system compile) - andalso OS.Process.isSuccess (OS.Process.system link) + system compile andalso system link end fun compile job = diff --git a/src/mono_env.sig b/src/mono_env.sig index c5ca7c0b..97d7d9ea 100644 --- a/src/mono_env.sig +++ b/src/mono_env.sig @@ -50,5 +50,6 @@ signature MONO_ENV = sig val patBindsN : Mono.pat -> int val liftExpInExp : int -> Mono.exp -> Mono.exp - + val subExpInExp : (int * Mono.exp) -> Mono.exp -> Mono.exp + end diff --git a/src/mono_env.sml b/src/mono_env.sml index 1df38db3..7f9a6e62 100644 --- a/src/mono_env.sml +++ b/src/mono_env.sml @@ -85,6 +85,19 @@ val liftExpInExp = bind = fn (bound, U.Exp.RelE _) => bound + 1 | (bound, _) => bound} +val subExpInExp = + U.Exp.mapB {typ = fn t => t, + exp = fn (xn, rep) => fn e => + case e of + ERel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER=> ERel (xn' - 1) + | LESS => e) + | _ => e, + bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) + | (ctx, _) => ctx} + fun pushERel (env : env) x t eo = {datatypes = #datatypes env, constructors = #constructors env, diff --git a/src/mono_reduce.sml b/src/mono_reduce.sml index e61ed237..82d0a63d 100644 --- a/src/mono_reduce.sml +++ b/src/mono_reduce.sml @@ -57,7 +57,6 @@ fun simpleImpure (tsyms, syms) = | ERecv _ => true | ESleep _ => true | ENamed n => IS.member (syms, n) - | EError _ => true | ERel n => let val (_, t, _) = E.lookupERel env n @@ -398,7 +397,10 @@ fun reduce file = summarize d e @ [ReadCookie] | EFfiApp (m, x, es) => if Settings.isEffectful (m, x) orelse Settings.isBenignEffectful (m, x) then - List.concat (map (summarize d) es) @ [Unsure] + List.concat (map (summarize d) es) @ [if m = "Basis" andalso String.isSuffix "_w" x then + WritePage + else + Unsure] else List.concat (map (summarize d) es) | EApp ((EFfi _, _), e) => summarize d e @@ -429,6 +431,7 @@ fun reduce file = | EApp (f, x) => unravel (#1 f, passed + 1, List.revAppend (summarize d x, ls)) + | EError _ => [Abort] | _ => [Unsure] in unravel (e, 0, []) @@ -445,17 +448,25 @@ fun reduce file = | ECase (e, pes, _) => let val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes + + fun splitRel ls acc = + case ls of + [] => (acc, false, ls) + | UseRel :: ls => (acc, true, ls) + | v :: ls => splitRel ls (v :: acc) + + val (pre, used, post) = foldl (fn (ls, (pre, used, post)) => + let + val (pre', used', post') = splitRel ls [] + in + (pre' @ pre, used' orelse used, post' @ post) + end) + ([], false, []) lss in - case lss of - [] => summarize d e - | ls :: lss => - summarize d e - @ (if List.all (fn ls' => ls' = ls) lss then - ls - else if length (List.filter (not o List.null) (ls :: lss)) <= 1 then - valOf (List.find (not o List.null) (ls :: lss)) - else - [Unsure]) + summarize d e + @ pre + @ (if used then [UseRel] else []) + @ post end | EStrcat (e1, e2) => summarize d e1 @ summarize d e2 @@ -534,8 +545,8 @@ fun reduce file = val effs_e' = List.filter (fn x => x <> UseRel) effs_e' val effs_b = summarize 0 b - (*val () = Print.prefaces "Try" - [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)), + (*val () = Print.fprefaces outf "Try" + [(*("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)),*) ("e'", MonoPrint.p_exp env e'), ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b), ("e'_eff", p_events effs_e'), diff --git a/src/monoize.sml b/src/monoize.sml index 30dfdd46..4295811a 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -236,9 +236,9 @@ fun monoType env = (L'.TFfi ("Basis", "string"), loc) | L.CFfi ("Basis", "sql_sequence") => (L'.TFfi ("Basis", "string"), loc) - | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query"), _), _), _), _), _), _) => + | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query"), _), _), _), _), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) - | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query1"), _), _), _), _), _), _), _), _) => + | L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_query1"), _), _), _), _), _), _), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_from_items"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) @@ -1908,7 +1908,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = end | _ => poly ()) - | L.ECApp ((L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_query"), _), _), _), _), _), _), _), _) => + | L.ECApp ((L.ECApp ((L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_query"), _), _), _), _), _), _), _), _), _), _) => let fun sc s = (L'.EPrim (Prim.String s), loc) val s = (L'.TFfi ("Basis", "string"), loc) @@ -1934,7 +1934,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_query1"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_query1"), _), + _), _), _), _), (L.CRecord (_, tables), _)), _), (L.CRecord (_, grouped), _)), _), @@ -2592,7 +2594,9 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.ECApp ( - (L.EFfi ("Basis", "sql_forget_tables"), _), + (L.ECApp ( + (L.EFfi ("Basis", "sql_forget_tables"), _), + _), _), _), _), _), _), _), _), @@ -2625,7 +2629,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.EFfi ("Basis", "sql_count"), _), _), _), _), _), - _) => ((L'.EPrim (Prim.String "COALESCE(COUNT(*),0)"), loc), + _) => ((L'.EPrim (Prim.String "COUNT(*)"), loc), fm) | L.ECApp ( @@ -2640,18 +2644,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) = _), _), t) => let - val default = - case #1 t of - L.CFfi ("Basis", s) => - SOME (case s of - "int" => "0" - | "float" => "0.0" - | "string" => "''" - | "time" => "0" - | _ => raise Fail "Illegal type of sql_aggregate [1]") - | L.CApp ((L.CFfi ("Basis", "option"), _), _) => NONE - | _ => raise Fail "Illegal type of sql_aggregate [2]" - val s = (L'.TFfi ("Basis", "string"), loc) fun sc s = (L'.EPrim (Prim.String s), loc) @@ -2659,13 +2651,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) = sc "(", (L'.ERel 0, loc), sc ")"] - - val main = case default of - NONE => main - | SOME default => - strcat [sc "COALESCE(", - main, - sc ("," ^ default ^ ")")] in ((L'.EAbs ("c", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), (L'.EAbs ("e1", s, (L'.TFun (s, s), loc), main), loc)), loc), @@ -2682,13 +2667,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) = ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TRecord [], loc), (L'.ERecord [], loc)), loc), fm) - | L.ECApp ((L.EFfi ("Basis", "sql_avg"), _), _) => - ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), - (L'.EPrim (Prim.String "AVG"), loc)), loc), + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_avg"), _), _), _), _) => + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc), + (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EPrim (Prim.String "AVG"), loc)), loc)), loc), fm) - | L.ECApp ((L.EFfi ("Basis", "sql_sum"), _), _) => - ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), - (L'.EPrim (Prim.String "SUM"), loc)), loc), + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_sum"), _), _), _), _) => + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc), + (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EPrim (Prim.String "SUM"), loc)), loc)), loc), fm) | L.EFfi ("Basis", "sql_arith_int") => ((L'.ERecord [], loc), fm) @@ -2701,13 +2688,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) = ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TRecord [], loc), (L'.ERecord [], loc)), loc), fm) - | L.ECApp ((L.EFfi ("Basis", "sql_max"), _), _) => - ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), - (L'.EPrim (Prim.String "MAX"), loc)), loc), + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_max"), _), _), _), _) => + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc), + (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EPrim (Prim.String "MAX"), loc)), loc)), loc), fm) - | L.ECApp ((L.EFfi ("Basis", "sql_min"), _), _) => - ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), - (L'.EPrim (Prim.String "MIN"), loc)), loc), + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_min"), _), _), _), _) => + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFun ((L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc)), loc), + (L'.EAbs ("_", (L'.TRecord [], loc), (L'.TFfi ("Basis", "string"), loc), + (L'.EPrim (Prim.String "MIN"), loc)), loc)), loc), fm) | L.EFfi ("Basis", "sql_asc") => ((L'.EPrim (Prim.String ""), loc), fm) -- cgit v1.2.3