# HG changeset patch # User Adam Chlipala # Date 1254838526 14400 # Node ID 46803e668a8970625ba230cb17abaa94a2ef22d2 # Parent 0bdc4d538f1ca5f19665627561e244c17b65df00 Fix a de Bruijn index bug in map fusion diff -r 0bdc4d538f1c -r 46803e668a89 demo/more/orm.ur --- a/demo/more/orm.ur Mon Oct 05 17:24:21 2009 -0400 +++ b/demo/more/orm.ur Tue Oct 06 10:15:26 2009 -0400 @@ -1,68 +1,78 @@ -con link = fn t :: Type => unit +con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2) +fun noParent [t ::: Type] _ = return None -con meta = fn col :: Type => { - Link : link col, - Inj : sql_injectable col - } +con meta = fn col_parent :: (Type * Type) => { + Link : link col_parent, + Inj : sql_injectable col_parent.1 + } functor Table(M : sig - con cols :: {Type} + con cols :: {(Type * Type)} val cols : $(map meta cols) constraint [Id] ~ cols val folder : folder cols end) = struct type id = int - val inj = _ - val id : meta id = {Link = (), - Inj = inj} + con fs' = map fst M.cols + con fs = [Id = id] ++ fs' + type row' = $fs' + type row = $fs - con fs = [Id = id] ++ M.cols + fun resultsOut q = query q (fn r ls => return (r.T :: ls)) [] + fun resultOut q = ro <- oneOrNoRows q; return (Option.mp (fn r => r .T) ro) sequence s table t : fs - type row = $fs + val inj = _ + val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}), + Inj = inj} - fun ensql [avail] (r : $M.cols) : $(map (sql_exp avail [] []) M.cols) = - map2 [meta] [Top.id] [sql_exp avail [] []] - (fn [t] meta v => @sql_inject meta.Inj v) + fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') = + map2 [meta] [fst] [fn ts :: (Type * Type) => sql_exp avail [] [] ts.1] + (fn [ts] meta v => @sql_inject meta.Inj v) [_] M.folder M.cols r - fun create (r : $M.cols) = + fun create (r : row') = id <- nextval s; dml (insert t ({Id = sql_inject id} ++ ensql r)); return ({Id = id} ++ r) fun delete r = dml (DELETE FROM t WHERE t.Id = {[r.Id]}) - fun save r = dml (update [M.cols] ! (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]})) + fun save r = dml (update [fs'] ! (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]})) fun lookup id = ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]}); return (Option.mp (fn r => r.T) ro) - fun resultsOut q = query q (fn r ls => return (r.T :: ls)) [] val list = resultsOut (SELECT * FROM t) con col = fn t => {Exp : sql_exp [T = fs] [] [] t, Inj : sql_injectable t} val idCol = {Exp = sql_field [#T] [#Id], Inj = _} - val cols = foldR [meta] [fn before => after :: {Type} -> [before ~ after] => - $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t, - Inj : sql_injectable t}) before)] - (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before] (meta : meta t) - (acc : after :: {Type} -> [before ~ after] => - $(map (fn t => {Exp : sql_exp [T = before ++ after] [] [] t, - Inj : sql_injectable t}) before)) - [after :: {Type}] [[nm = t] ++ before ~ after] => - {nm = {Exp = sql_field [#T] [nm], - Inj = meta.Inj}} ++ acc [[nm = t] ++ after] !) - (fn [after :: {Type}] [[] ~ after] => {}) + con meta' = fn (fs :: {Type}) (col_parent :: (Type * Type)) => + {Col : {Exp : sql_exp [T = fs] [] [] col_parent.1, + Inj : sql_injectable col_parent.1}, + Parent : $fs -> transaction (option col_parent.2)} + val cols = foldR [meta] [fn before => after :: {(Type * Type)} -> [before ~ after] => + $(map (meta' (map fst (before ++ after))) before)] + (fn [nm :: Name] [ts :: (Type * Type)] [before :: {(Type * Type)}] + [[nm] ~ before] (meta : meta ts) + (acc : after :: {(Type * Type)} -> [before ~ after] => + $(map (meta' (map fst (before ++ after))) before)) + [after :: {(Type * Type)}] [[nm = ts] ++ before ~ after] => + {nm = {Col = {Exp = sql_field [#T] [nm], + Inj = meta.Inj}, + Parent = fn r => meta.Link r.nm}} + ++ acc [[nm = ts] ++ after] !) + (fn [after :: {(Type * Type)}] [[] ~ after] => {}) [_] M.folder M.cols - [[Id = id]] ! + [[Id = (id, row)]] ! type filter = sql_exp [T = fs] [] [] bool + fun find (f : filter) = resultOut (SELECT * FROM t WHERE {f}) fun search (f : filter) = resultsOut (SELECT * FROM t WHERE {f}) fun bin (b : t ::: Type -> sql_binary t t bool) [t] (c : col t) (v : t) = diff -r 0bdc4d538f1c -r 46803e668a89 demo/more/orm.urs --- a/demo/more/orm.urs Mon Oct 05 17:24:21 2009 -0400 +++ b/demo/more/orm.urs Tue Oct 06 10:15:26 2009 -0400 @@ -1,23 +1,25 @@ -con link :: Type -> Type +con link :: (Type * Type) -> Type +val noParent : t ::: Type -> link (t, unit) -con meta = fn col :: Type => { - Link : link col, - Inj : sql_injectable col +con meta = fn col_parent :: (Type * Type) => { + Link : link col_parent, + Inj : sql_injectable col_parent.1 } functor Table(M : sig - con cols :: {Type} + con cols :: {(Type * Type)} val cols : $(map meta cols) constraint [Id] ~ cols val folder : folder cols end) : sig type id + type row' = $(map fst M.cols) + type row = $([Id = id] ++ map fst M.cols) + val inj : sql_injectable id - val id : meta id + val id : meta (id, row) - type row = $([Id = id] ++ M.cols) - - val create : $M.cols -> transaction row + val create : row' -> transaction row val delete : row -> transaction unit val save : row -> transaction unit val lookup : id -> transaction (option row) @@ -25,9 +27,12 @@ con col :: Type -> Type val idCol : col id - val cols : $(map col M.cols) + val cols : $(map (fn col_parent :: (Type * Type) => + {Col : col col_parent.1, + Parent : row -> transaction (option col_parent.2)}) M.cols) type filter + val find : filter -> transaction (option row) val search : filter -> transaction (list row) val eq : t ::: Type -> col t -> t -> filter diff -r 0bdc4d538f1c -r 46803e668a89 src/elab_ops.sml --- a/src/elab_ops.sml Mon Oct 05 17:24:21 2009 -0400 +++ b/src/elab_ops.sml Tue Oct 06 10:15:26 2009 -0400 @@ -242,6 +242,9 @@ (case #1 (hnormCon env f') of CMap (dom, _) => let + val inner_f = liftConInCon 0 inner_f + val f = liftConInCon 0 f + val f' = (CApp (inner_f, (CRel 0, loc)), loc) val f' = (CApp (f, f'), loc) val f' = (CAbs ("v", dom, f'), loc)