# HG changeset patch # User Adam Chlipala # Date 1256048957 14400 # Node ID bb3fc575cfe778e810a710ef80a0ecbe2db68a38 # Parent 1d456a06ea4e3d50522defdd7d227124c568f8ca Adapted existing demos to tuple pattern-matching diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/batchFun.ur --- a/demo/batchFun.ur Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/batchFun.ur Tue Oct 20 10:29:17 2009 -0400 @@ -1,11 +1,11 @@ -con colMeta = fn t_state :: (Type * Type) => +con colMeta = fn (db :: Type, state :: Type) => {Nam : string, - Show : t_state.1 -> xbody, - Inject : sql_injectable t_state.1, + Show : db -> xbody, + Inject : sql_injectable db, - NewState : transaction t_state.2, - Widget : t_state.2 -> xbody, - ReadState : t_state.2 -> transaction t_state.1} + NewState : transaction state, + Widget : state -> xbody, + ReadState : state -> transaction db} con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols) fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/batchFun.urs --- a/demo/batchFun.urs Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/batchFun.urs Tue Oct 20 10:29:17 2009 -0400 @@ -1,11 +1,11 @@ -con colMeta = fn t_state :: (Type * Type) => +con colMeta = fn (db :: Type, state :: Type) => {Nam : string, - Show : t_state.1 -> xbody, - Inject : sql_injectable t_state.1, + Show : db -> xbody, + Inject : sql_injectable db, - NewState : transaction t_state.2, - Widget : t_state.2 -> xbody, - ReadState : t_state.2 -> transaction t_state.1} + NewState : transaction state, + Widget : state -> xbody, + ReadState : state -> transaction db} con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols) val int : string -> colMeta (int, source string) diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/crud.ur --- a/demo/crud.ur Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/crud.ur Tue Oct 20 10:29:17 2009 -0400 @@ -1,11 +1,10 @@ -con colMeta = fn t_formT :: (Type * Type) => { - Nam : string, - Show : t_formT.1 -> xbody, - Widget : nm :: Name -> xml form [] [nm = t_formT.2], - WidgetPopulated : nm :: Name -> t_formT.1 -> xml form [] [nm = t_formT.2], - Parse : t_formT.2 -> t_formT.1, - Inject : sql_injectable t_formT.1 - } +con colMeta = fn (db :: Type, widget :: Type) => + {Nam : string, + Show : db -> xbody, + Widget : nm :: Name -> xml form [] [nm = widget], + WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], + Parse : widget -> db, + Inject : sql_injectable db} con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols) fun default [t] (sh : show t) (rd : read t) (inj : sql_injectable t) diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/crud.urs --- a/demo/crud.urs Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/crud.urs Tue Oct 20 10:29:17 2009 -0400 @@ -1,11 +1,10 @@ -con colMeta = fn t_formT :: (Type * Type) => +con colMeta = fn (db :: Type, widget :: Type) => {Nam : string, - Show : t_formT.1 -> xbody, - Widget : nm :: Name -> xml form [] [nm = t_formT.2], - WidgetPopulated : nm :: Name -> t_formT.1 - -> xml form [] [nm = t_formT.2], - Parse : t_formT.2 -> t_formT.1, - Inject : sql_injectable t_formT.1} + Show : db -> xbody, + Widget : nm :: Name -> xml form [] [nm = widget], + WidgetPopulated : nm :: Name -> db -> xml form [] [nm = widget], + Parse : widget -> db, + Inject : sql_injectable db} con colsMeta = fn cols :: {(Type * Type)} => $(map colMeta cols) val int : string -> colMeta (int, string) diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/more/grid.ur --- a/demo/more/grid.ur Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/more/grid.ur Tue Oct 20 10:29:17 2009 -0400 @@ -9,10 +9,10 @@ DisplayFilter : filter -> xbody, Filter : filter -> row -> signal bool, Sort : option (row -> row -> bool)} - -con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) => - {Initialize : transaction global_input_filter.1, - Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3} + +con colMeta = fn (row :: Type) (global :: Type, input :: Type, filter :: Type) => + {Initialize : transaction global, + Handlers : global -> colMeta' row input filter} con aggregateMeta = fn (row :: Type) (acc :: Type) => {Initial : acc, diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/more/grid.urs --- a/demo/more/grid.urs Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/more/grid.urs Tue Oct 20 10:29:17 2009 -0400 @@ -10,9 +10,9 @@ Filter : filter -> row -> signal bool, Sort : option (row -> row -> bool)} -con colMeta = fn (row :: Type) (global_input_filter :: (Type * Type * Type)) => - {Initialize : transaction global_input_filter.1, - Handlers : global_input_filter.1 -> colMeta' row global_input_filter.2 global_input_filter.3} +con colMeta = fn (row :: Type) (global :: Type, input :: Type, filter :: Type) => + {Initialize : transaction global, + Handlers : global -> colMeta' row input filter} con aggregateMeta = fn (row :: Type) (acc :: Type) => {Initial : acc, diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/more/orm.ur --- a/demo/more/orm.ur Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/more/orm.ur Tue Oct 20 10:29:17 2009 -0400 @@ -1,9 +1,9 @@ con link = fn col_parent :: (Type * Type) => col_parent.1 -> transaction (option col_parent.2) fun noParent [t ::: Type] (_ : t) = return None -con meta = fn col_parent :: (Type * Type) => { - Link : link col_parent, - Inj : sql_injectable col_parent.1 +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, @@ -55,10 +55,10 @@ con col = fn t => {Exp : sql_exp [T = fs] [] [] t, Inj : sql_injectable t} val idCol = {Exp = sql_field [#T] [#Id], Inj = _} - 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)} + con meta' = fn (fs :: {Type}) (col :: Type, parent :: Type) => + {Col : {Exp : sql_exp [T = fs] [] [] col, + Inj : sql_injectable col}, + Parent : $fs -> transaction (option parent)} 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)}] diff -r 1d456a06ea4e -r bb3fc575cfe7 demo/more/orm.urs --- a/demo/more/orm.urs Tue Oct 20 10:19:00 2009 -0400 +++ b/demo/more/orm.urs Tue Oct 20 10:29:17 2009 -0400 @@ -1,9 +1,9 @@ con link :: (Type * Type) -> Type val noParent : t ::: Type -> link (t, unit) -con meta = fn col_parent :: (Type * Type) => { - Link : link col_parent, - Inj : sql_injectable col_parent.1 +con meta = fn (col :: Type, parent :: Type) => { + Link : link (col, parent), + Inj : sql_injectable col } val local : t :: Type -> sql_injectable t -> meta (t, unit) @@ -29,9 +29,9 @@ con col :: Type -> Type val idCol : col id - val cols : $(map (fn col_parent :: (Type * Type) => - {Col : col col_parent.1, - Parent : row -> transaction (option col_parent.2)}) M.cols) + val cols : $(map (fn (colm :: Type, parent :: Type) => + {Col : col colm, + Parent : row -> transaction (option parent)}) M.cols) type filter val find : filter -> transaction (option row)