# HG changeset patch # User Adam Chlipala # Date 1252782496 14400 # Node ID 51bc7681c47edee9ebbff0f916f6a0857e252765 # Parent 095df8f710e040aeae405b969d91900be2a6d005 Nullable columns *might* be working, but too much JS is generated for the page to load in finite time diff -r 095df8f710e0 -r 51bc7681c47e demo/more/dbgrid.ur --- a/demo/more/dbgrid.ur Sat Sep 12 10:36:17 2009 -0400 +++ b/demo/more/dbgrid.ur Sat Sep 12 15:08:16 2009 -0400 @@ -15,53 +15,93 @@ Handlers : global_t.1 -> colMeta' row global_t.2} structure Direct = struct + con metaBase = fn actual_input :: (Type * Type) => + {Display : actual_input.2 -> xbody, + Edit : actual_input.2 -> xbody, + Initialize : actual_input.1 -> transaction actual_input.2, + Parse : actual_input.2 -> signal (option actual_input.1)} + + datatype metaBoth actual input = + NonNull of metaBase (actual, input) * metaBase (option actual, input) + | Nullable of metaBase (actual, input) + con meta = fn global_actual_input :: (Type * Type * Type) => {Initialize : transaction global_actual_input.1, Handlers : global_actual_input.1 - -> {Display : global_actual_input.3 -> xbody, - Edit : global_actual_input.3 -> xbody, - Initialize : global_actual_input.2 -> transaction global_actual_input.3, - Parse : global_actual_input.3 -> signal (option global_actual_input.2)}} + -> metaBoth global_actual_input.2 global_actual_input.3} con editableState (ts :: (Type * Type * Type)) = (ts.1, ts.3) fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest) (editableState ts) = - {Initialize = m.Initialize, - Handlers = fn data => {Header = name, - Project = fn r => (m.Handlers data).Initialize r.nm, - Update = fn r s => - vo <- current ((m.Handlers data).Parse s); - return (case vo of - None => r - | Some v => r -- nm ++ {nm = v}), - Display = (m.Handlers data).Display, - Edit = (m.Handlers data).Edit, - Validate = fn s => vo <- (m.Handlers data).Parse s; return (Option.isSome vo)}} + let + fun doMr mr = {Header = name, + Project = fn r => mr.Initialize r.nm, + Update = fn r s => + vo <- current (mr.Parse s); + return (case vo of + None => r + | Some v => r -- nm ++ {nm = v}), + Display = mr.Display, + Edit = mr.Edit, + Validate = fn s => vo <- mr.Parse s; return (Option.isSome vo)} + in + {Initialize = m.Initialize, + Handlers = fn data => case m.Handlers data of + NonNull (mr, _) => doMr mr + | Nullable mr => doMr mr} + end con readOnlyState (ts :: (Type * Type * Type)) = (ts.1, ts.3) fun readOnly [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest) (readOnlyState ts) = - {Initialize = m.Initialize, - Handlers = fn data => {Header = name, - Project = fn r => (m.Handlers data).Initialize r.nm, - Update = fn r _ => return r, - Display = (m.Handlers data).Display, - Edit = (m.Handlers data).Display, - Validate = fn _ => return True}} + let + fun doMr mr = {Header = name, + Project = fn r => mr.Initialize r.nm, + Update = fn r _ => return r, + Display = mr.Display, + Edit = mr.Display, + Validate = fn _ => return True} + in + {Initialize = m.Initialize, + Handlers = fn data => case m.Handlers data of + NonNull (mr, _) => doMr mr + | Nullable mr => doMr mr} + end con metaBasic = fn actual_input :: (Type * Type) => - {Display : actual_input.2 -> xbody, - Edit : source actual_input.2 -> xbody, - Initialize : actual_input.1 -> actual_input.2, - Parse : actual_input.2 -> option actual_input.1} + {Display : actual_input.2 -> xbody, + Edit : source actual_input.2 -> xbody, + Initialize : actual_input.1 -> actual_input.2, + InitializeNull : actual_input.2, + IsNull : actual_input.2 -> bool, + Parse : actual_input.2 -> option actual_input.1} con basicState = source fun basic [ts ::: (Type * Type)] (m : metaBasic ts) : meta (unit, ts.1, basicState ts.2) = {Initialize = return (), - Handlers = fn () => {Display = fn s => , + Handlers = fn () => NonNull ( + {Display = fn s => , Edit = m.Edit, Initialize = fn v => source (m.Initialize v), - Parse = fn s => v <- signal s; return (m.Parse v)}} + Parse = fn s => v <- signal s; return (m.Parse v)}, + {Display = fn s => , + Edit = m.Edit, + Initialize = fn v => source (case v of + None => m.InitializeNull + | Some v => m.Initialize v), + Parse = fn s => v <- signal s; + return (if m.IsNull v then + Some None + else + case m.Parse v of + None => None + | Some v' => Some (Some v'))})} + + fun nullable [global] [actual] [input] (m : meta (global, actual, input)) = + {Initialize = m.Initialize, + Handlers = fn d => case m.Handlers d of + Nullable _ => error Don't stack calls to Direct.nullable! + | NonNull (_, ho) => Nullable ho} type intGlobal = unit type intInput = basicState string @@ -69,6 +109,8 @@ basic {Display = fn s => {[s]}, Edit = fn s => , Initialize = fn n => show n, + InitializeNull = "", + IsNull = eq "", Parse = fn v => read v} type stringGlobal = unit @@ -77,6 +119,8 @@ basic {Display = fn s => {[s]}, Edit = fn s => , Initialize = fn s => s, + InitializeNull = "", + IsNull = eq "", Parse = fn s => Some s} type boolGlobal = unit @@ -85,6 +129,8 @@ basic {Display = fn b => {[b]}, Edit = fn s => , Initialize = fn b => b, + InitializeNull = False, + IsNull = fn _ => False, Parse = fn b => Some b} functor Foreign (M : sig @@ -102,7 +148,7 @@ open M con global = list (t * string) - con input = source string * t * $row + con input = source string * option (t * $row) val getChoices = List.mapQuery (SELECT * FROM tab AS T) (fn r => (r.T.nm, render r.T)) @@ -111,21 +157,57 @@ r <- oneRow (SELECT T.{{row}} FROM tab AS T WHERE T.{nm} = {[k]}); return r.T - val meta = + val meta : meta (global, M.t, input) = {Initialize = getChoices, Handlers = fn choices => - {Display = fn (_, k, r) => {[render ({nm = k} ++ r)]}, - Edit = fn (s, k, _) => + NonNull ( + {Display = fn (_, kr) => case kr of + None => error Unexpected Foreign null + | Some (k, r) => {[render ({nm = k} ++ r)]}, + Edit = fn (s, kr) => {List.mapX (fn (k', rend) => - {[rend]} + False + | Some (k, _) => + k' = k}>{[rend]} ) choices} , Initialize = fn k => s <- source (show k); r <- rpc (getChoice k); - return (s, k, r), - Parse = fn (s, _, _) => k <- signal s; return (read k)}} + return (s, Some (k, r)), + Parse = fn (s, _) => k <- signal s; return (read k : option t)}, + {Display = fn (_, kr) => case kr of + None => NULL + | Some (k, r) => {[render ({nm = k} ++ r)]}, + Edit = fn (s, kr) => + + True + | _ => False}>NULL + {List.mapX (fn (k', rend) => + False + | Some (k, _) => + k' = k}>{[rend]} + ) + choices} + , + Initialize = fn k => case k of + None => + s <- source ""; + return (s, None) + | Some k => + s <- source (show k); + r <- rpc (getChoice k); + return (s, Some (k, r)), + Parse = fn (s, _) => ks <- signal s; + return (case ks of + "" => Some None + | _ => case read ks : option t of + None => None + | Some k => Some (Some k))})} end end diff -r 095df8f710e0 -r 51bc7681c47e demo/more/dbgrid.urs --- a/demo/more/dbgrid.urs Sat Sep 12 10:36:17 2009 -0400 +++ b/demo/more/dbgrid.urs Sat Sep 12 15:08:16 2009 -0400 @@ -15,13 +15,20 @@ Handlers : global_t.1 -> colMeta' row global_t.2} structure Direct : sig + con metaBase = fn actual_input :: (Type * Type) => + {Display : actual_input.2 -> xbody, + Edit : actual_input.2 -> xbody, + Initialize : actual_input.1 -> transaction actual_input.2, + Parse : actual_input.2 -> signal (option actual_input.1)} + + datatype metaBoth actual input = + NonNull of metaBase (actual, input) * metaBase (option actual, input) + | Nullable of metaBase (actual, input) + con meta = fn global_actual_input :: (Type * Type * Type) => {Initialize : transaction global_actual_input.1, Handlers : global_actual_input.1 - -> {Display : global_actual_input.3 -> xbody, - Edit : global_actual_input.3 -> xbody, - Initialize : global_actual_input.2 -> transaction global_actual_input.3, - Parse : global_actual_input.3 -> signal (option global_actual_input.2)}} + -> metaBoth global_actual_input.2 global_actual_input.3} con editableState :: (Type * Type * Type) -> (Type * Type) val editable : ts ::: (Type * Type * Type) -> rest ::: {Type} @@ -35,6 +42,10 @@ -> colMeta ([nm = ts.2] ++ rest) (readOnlyState ts) + val nullable : global ::: Type -> actual ::: Type -> input ::: Type + -> meta (global, actual, input) + -> meta (global, option actual, input) + type intGlobal type intInput val int : meta (intGlobal, int, intInput) diff -r 095df8f710e0 -r 51bc7681c47e demo/more/grid1.ur --- a/demo/more/grid1.ur Sat Sep 12 10:36:17 2009 -0400 +++ b/demo/more/grid1.ur Sat Sep 12 15:08:16 2009 -0400 @@ -4,11 +4,11 @@ PRIMARY KEY Id sequence s -table t : {Id : int, A : int, B : string, C : bool, D : int} +table t : {Id : int, A : int, B : string, C : bool, D : int, E : option int} PRIMARY KEY Id, CONSTRAINT Foreign FOREIGN KEY (D) REFERENCES t1(Id) ON DELETE CASCADE -fun page (n, s) = return A = {[n]}, B = {[s]} +(*fun page (n, s) = return A = {[n]}, B = {[s]}*) open Make(struct val tab = t @@ -23,6 +23,8 @@ C = {New = return False, Inj = _}, D = {New = return 0, + Inj = _}, + E = {New = return None, Inj = _}} structure F = Direct.Foreign(struct @@ -34,10 +36,11 @@ val cols = {Id = Direct.readOnly [#Id] ! "Id" Direct.int, A = Direct.editable [#A] ! "A" Direct.int, B = Direct.editable [#B] ! "B" Direct.string, - C = Direct.editable [#C] ! "C" Direct.bool, + C = Direct.editable [#C] ! "C" Direct.bool(*, D = Direct.editable [#D] ! "D" F.meta, + E = Direct.editable [#E] ! "E" (Direct.nullable Direct.int), DA = computed "2A" (fn r => 2 * r.A), - Link = computedHtml "Link" (fn r => Go)} + Link = computedHtml "Link" (fn r => Go)*)} end) fun main () = diff -r 095df8f710e0 -r 51bc7681c47e src/reduce.sml --- a/src/reduce.sml Sat Sep 12 10:36:17 2009 -0400 +++ b/src/reduce.sml Sat Sep 12 15:08:16 2009 -0400 @@ -101,6 +101,69 @@ @ List.tabulate (ne, fn _ => UnknownE) | x => [x]) +datatype result = Yes of env | No | Maybe + +fun match (env, p : pat, e : exp) = + case (#1 p, #1 e) of + (PWild, _) => Yes env + | (PVar (x, t), _) => Yes (KnownE e :: env) + + | (PPrim p, EPrim p') => + if Prim.equal (p, p') then + Yes env + else + No + + | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) => + if n1 = n2 then + Yes env + else + No + + | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) => + if n1 = n2 then + match (env, p, e) + else + No + + | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE), + ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) => + if m1 = m2 andalso con1 = con2 then + Yes env + else + No + + | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep), + ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) => + if m1 = m2 andalso con1 = con2 then + match (env, p, e) + else + No + + | (PRecord xps, ERecord xes) => + if List.exists (fn ((CName _, _), _, _) => false + | _ => true) xes then + Maybe + else + let + fun consider (xps, env) = + case xps of + [] => Yes env + | (x, p, _) :: rest => + case List.find (fn ((CName x', _), _, _) => x' = x + | _ => false) xes of + NONE => No + | SOME (_, e, _) => + case match (env, p, e) of + No => No + | Maybe => Maybe + | Yes env => consider (rest, env) + in + consider (xps, env) + end + + | _ => Maybe + fun kindConAndExp (namedC, namedE) = let fun kind env (all as (k, loc)) = @@ -690,11 +753,24 @@ | PCon (dk, pc, cs, po) => (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) + + fun push () = + (ECase (exp env e, + map (fn (p, e) => (pat p, + exp (List.tabulate (patBinds p, + fn _ => UnknownE) @ env) e)) + pes, {disc = con env disc, result = con env result}), loc) + + fun search pes = + case pes of + [] => push () + | (p, body) :: pes => + case match (env, p, e) of + No => search pes + | Maybe => push () + | Yes env' => exp env' body in - (ECase (exp env e, - map (fn (p, e) => (pat p, - exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e)) - pes, {disc = con env disc, result = con env result}), loc) + search pes end | EWrite e => (EWrite (exp env e), loc)