summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--demo/more/dbgrid.ur35
-rw-r--r--demo/more/dlist.ur17
-rw-r--r--demo/more/grid.ur29
-rw-r--r--demo/more/grid0.ur4
-rw-r--r--demo/more/orm.ur13
-rw-r--r--lib/ur/string.ur2
-rw-r--r--src/elaborate.sml34
7 files changed, 86 insertions, 48 deletions
diff --git a/demo/more/dbgrid.ur b/demo/more/dbgrid.ur
index b6cd94ae..43ad7725 100644
--- a/demo/more/dbgrid.ur
+++ b/demo/more/dbgrid.ur
@@ -38,7 +38,7 @@ structure Direct = struct
NonNull of metaBase (actual, input, filter) * metaBase (option actual, input, filter)
| Nullable of metaBase (actual, input, filter)
- con meta = fn global_actual_input_filter :: (Type * Type * Type * Type) =>
+ con meta = fn global_actual_input_filter =>
{Initialize : transaction global_actual_input_filter.1,
Handlers : global_actual_input_filter.1
-> metaBoth global_actual_input_filter.2 global_actual_input_filter.3
@@ -48,25 +48,26 @@ structure Direct = struct
fun editable [ts] [rest] [nm :: Name] [[nm] ~ rest] name (m : meta ts) : colMeta ([nm = ts.2] ++ rest)
(editableState ts) =
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),
- CreateFilter = mr.CreateFilter,
- DisplayFilter = mr.DisplayFilter,
- Filter = fn i r => mr.Filter i r.nm,
- Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
+ fun doMr (mr : metaBase (ts.2, ts.3, ts.4)) : colMeta' ([nm = ts.2] ++ rest) ts.3 ts.4 =
+ {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),
+ CreateFilter = mr.CreateFilter,
+ DisplayFilter = mr.DisplayFilter,
+ Filter = fn i r => mr.Filter i r.nm,
+ Sort = Some (fn r1 r2 => mr.Sort r1.nm r2.nm)}
in
{Initialize = m.Initialize,
Handlers = fn data => case m.Handlers data of
- NonNull (mr, _) => doMr mr
- | Nullable mr => doMr mr}
+ NonNull (mr, _) => doMr mr
+ | Nullable mr => doMr mr}
end
con readOnlyState (ts :: (Type * Type * Type * Type)) = (ts.1, ts.3, ts.4)
diff --git a/demo/more/dlist.ur b/demo/more/dlist.ur
index 1e5b8020..884ab8a1 100644
--- a/demo/more/dlist.ur
+++ b/demo/more/dlist.ur
@@ -119,7 +119,8 @@ fun renderDyn [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) []
end}/>
</xml>
-fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] []) filter =
+fun renderFlat [ctx] [ctx ~ body] [t] (f : t -> position -> xml (ctx ++ body) [] [])
+ : option int -> list (t * position) -> xml (ctx ++ body) [] [] =
let
fun renderFlat' len ls =
case len of
@@ -233,13 +234,13 @@ fun render [ctx] [ctx ~ body] [t] f (r : {Filter : t -> signal bool,
None => elems
| Some pos => skip pos elems
in
- return (renderFlat f r.Filter len elems)
+ return (renderFlat f len elems)
end}/>
</xml>
fun delete pos = pos
-fun elements' [t] (dl'' : dlist'' t) =
+fun elements' [t] (dl'' : dlist'' t) : signal (list t) =
case dl'' of
Nil => return []
| Cons (x, dl'') =>
@@ -247,13 +248,13 @@ fun elements' [t] (dl'' : dlist'' t) =
tl <- elements' dl'';
return (x :: tl)
-fun elements [t] (dl : dlist t) =
+fun elements [t] (dl : dlist t) : signal (list t) =
dl' <- signal dl;
case dl' of
Empty => return []
| Nonempty {Head = hd, ...} => elements' hd
-fun size' [t] (dl'' : dlist'' t) =
+fun size' [t] (dl'' : dlist'' t) : signal int =
case dl'' of
Nil => return 0
| Cons (x, dl'') =>
@@ -261,13 +262,13 @@ fun size' [t] (dl'' : dlist'' t) =
n <- size' dl'';
return (n + 1)
-fun size [t] (dl : dlist t) =
+fun size [t] (dl : dlist t) : signal int =
dl' <- signal dl;
case dl' of
Empty => return 0
| Nonempty {Head = hd, ...} => size' hd
-fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) =
+fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) : signal int =
case dl'' of
Nil => return 0
| Cons (x, dl'') =>
@@ -276,7 +277,7 @@ fun numPassing' [t] (f : t -> signal bool) (dl'' : dlist'' t) =
n <- numPassing' f dl'';
return (if b then n + 1 else n)
-fun numPassing [t] (f : t -> signal bool) (dl : dlist t) =
+fun numPassing [t] (f : t -> signal bool) (dl : dlist t) : signal int =
dl' <- signal dl;
case dl' of
Empty => return 0
diff --git a/demo/more/grid.ur b/demo/more/grid.ur
index d560c556..e0b4a351 100644
--- a/demo/more/grid.ur
+++ b/demo/more/grid.ur
@@ -49,16 +49,18 @@ functor Make(M : sig
fun make (row : M.row) [input] [filter] (m : colMeta' M.row input filter) : transaction input = m.Project row
fun makeAll cols row = @@Monad.exec [transaction] _ [map snd3 M.cols]
- (@map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
- (fn [p] data meta => make row(meta.Handlers data))
- M.folder cols M.cols)
- (@@Folder.mp [_] [_] M.folder)
+ (@map2 [fst3] [colMeta M.row] [fn p => transaction (snd3 p)]
+ (fn [p] data meta => make row (meta.Handlers data))
+ M.folder cols M.cols)
+ (@@Folder.mp [_] [_] M.folder)
+
+ type listT = {Row : source M.row,
+ Cols : source ($(map snd3 M.cols)),
+ Updating : source bool,
+ Selected : source bool}
type grid = {Cols : $(map fst3 M.cols),
- Rows : Dlist.dlist {Row : source M.row,
- Cols : source ($(map snd3 M.cols)),
- Updating : source bool,
- Selected : source bool},
+ Rows : Dlist.dlist listT,
Selection : source bool,
Filters : $(map thd3 M.cols),
Sort : source (option (M.row -> M.row -> bool)),
@@ -250,11 +252,12 @@ functor Make(M : sig
return (f r1 r2)) f)}
grid.Rows}
- <dyn signal={rows <- Dlist.foldl (fn row => @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
- (fn [nm :: Name] [t :: Type] meta acc =>
- Monad.mp (fn v => meta.Step v acc)
- (signal row.Row))
- M.aggFolder M.aggregates)
+ <dyn signal={rows <- Dlist.foldl (fn row : listT =>
+ @Monad.mapR2 _ [aggregateMeta M.row] [id] [id]
+ (fn [nm :: Name] [t :: Type] meta acc =>
+ Monad.mp (fn v => meta.Step v acc)
+ (signal row.Row))
+ M.aggFolder M.aggregates)
(@mp [aggregateMeta M.row] [id]
(fn [t] meta => meta.Initial)
M.aggFolder M.aggregates) grid.Rows;
diff --git a/demo/more/grid0.ur b/demo/more/grid0.ur
index 3e3d27ab..410554c9 100644
--- a/demo/more/grid0.ur
+++ b/demo/more/grid0.ur
@@ -13,8 +13,8 @@ open Make(struct
A = {New = return 0,
Inj = _}}
- val cols = {Id = Direct.readOnly [#Id] ! "Id" Direct.int,
- A = Direct.editable [#A] ! "A" Direct.int}
+ val cols = {Id = Direct.readOnly [#Id] "Id" Direct.int,
+ A = Direct.editable [#A] "A" Direct.int}
val aggregates = {}
diff --git a/demo/more/orm.ur b/demo/more/orm.ur
index d9f57f3b..068e3b5c 100644
--- a/demo/more/orm.ur
+++ b/demo/more/orm.ur
@@ -1,13 +1,14 @@
con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2)
-fun noParent [t ::: Type] (_ : t) = return None
+fun noParent [t ::: Type] (_ : t) : transaction (option unit) = return None
con meta = fn (col :: Type, parent :: Type) => {
Link : link (col, parent),
Inj : sql_injectable col
}
-fun local [t :: Type] (inj : sql_injectable t) = {Link = noParent,
- Inj = inj}
+fun local [t :: Type] (inj : sql_injectable t) : meta (t, unit) =
+ {Link = noParent,
+ Inj = inj}
functor Table(M : sig
con cols :: {(Type * Type)}
@@ -31,19 +32,19 @@ functor Table(M : sig
val id = {Link = fn id => resultOut (SELECT * FROM t WHERE t.Id = {[id]}),
Inj = inj}
- fun ensql [avail] (r : row') : $(map (sql_exp avail [] []) fs') =
+ 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 : row') =
id <- nextval s;
- dml (insert t ({Id = sql_inject id} ++ ensql r));
+ 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 [fs'] (ensql (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
+ fun save r = dml (update [fs'] (ensql [[T = [Id = int] ++ map fst M.cols]] (r -- #Id)) t (WHERE T.Id = {[r.Id]}))
fun lookup id =
ro <- oneOrNoRows (SELECT * FROM t WHERE t.Id = {[id]});
diff --git a/lib/ur/string.ur b/lib/ur/string.ur
index f7781e01..6a269373 100644
--- a/lib/ur/string.ur
+++ b/lib/ur/string.ur
@@ -57,7 +57,7 @@ fun mp f s =
mp' (length s - 1) ""
end
-fun newlines [ctx] [[Body] ~ ctx] s : xml ([Body] ++ ctx) [] [] =
+fun newlines [ctx] [[Body] ~ ctx] (s : string) : xml ([Body] ++ ctx) [] [] =
case split s #"\n" of
None => cdata s
| Some (s1, s2) => <xml>{[s1]}<br/>{newlines s2}</xml>
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 37ca4b25..12047b9f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -655,6 +655,24 @@
val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list)
+ exception CantSquish
+
+ fun squish by =
+ U.Con.mapB {kind = fn _ => fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ L'.CRel xn =>
+ if xn < bound then
+ c
+ else if bound <= xn andalso xn < bound + by then
+ raise CantSquish
+ else
+ L'.CRel (xn - by)
+ | L'.CUnif _ => raise CantSquish
+ | _ => c,
+ bind = fn (bound, U.Con.RelC _) => bound + 1
+ | (bound, _) => bound} 0
+
fun unifyRecordCons env (loc, c1, c2) =
let
fun rkindof c =
@@ -1056,6 +1074,19 @@
else
r := SOME c1All
+ | (L'.CUnif (nl, _, _, _, r), _) =>
+ if occursCon r c2All then
+ err COccursCheckFailed
+ else
+ (r := SOME (squish nl c2All)
+ handle CantSquish => err CIncompatible)
+ | (_, L'.CUnif (nl, _, _, _, r)) =>
+ if occursCon r c1All then
+ err COccursCheckFailed
+ else
+ (r := SOME (squish nl c1All)
+ handle CantSquish => err CIncompatible)
+
| (L'.CUnit, L'.CUnit) => ()
| (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
@@ -1290,7 +1321,8 @@ fun elabPat (pAll as (p, loc), (env, bound)) =
val k = (L'.KType, loc)
val unifs = map (fn _ => cunif (loc, k)) xs
val nxs = length unifs - 1
- val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, u) t) t unifs
+ val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
+ E.mliftConInCon (nxs - i) u) t) t unifs
val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
in
ignore (checkPatCon env p' pt t);
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 02:33:18 +0000