summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-10-06 10:15:26 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-10-06 10:15:26 -0400
commit0e84370511179878aa0ebae8bf43810efac194a5 (patch)
treebbb81bd1c2dfd38b74df44ae8c236f5353a7a043
parent2ed54658340ec7c94084ed21d9a4964b2c6d0afc (diff)
Fix a de Bruijn index bug in map fusion
-rw-r--r--demo/more/orm.ur68
-rw-r--r--demo/more/orm.urs25
-rw-r--r--src/elab_ops.sml3
3 files changed, 57 insertions, 39 deletions
diff --git a/demo/more/orm.ur b/demo/more/orm.ur
index f976fcb2..a0fd82a3 100644
--- a/demo/more/orm.ur
+++ b/demo/more/orm.ur
@@ -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 --git a/demo/more/orm.urs b/demo/more/orm.urs
index f284d3ec..429d2380 100644
--- a/demo/more/orm.urs
+++ b/demo/more/orm.urs
@@ -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
- val inj : sql_injectable id
- val id : meta id
+ type row' = $(map fst M.cols)
+ type row = $([Id = id] ++ map fst M.cols)
- type row = $([Id = id] ++ M.cols)
+ val inj : sql_injectable id
+ val id : meta (id, row)
- 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 @@ functor Table(M : sig
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 --git a/src/elab_ops.sml b/src/elab_ops.sml
index b5292e9b..f005ab04 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -242,6 +242,9 @@ fun hnormCon env (cAll as (c, loc)) =
(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)