diff options
author | 2008-10-12 11:44:43 -0400 | |
---|---|---|
committer | 2008-10-12 11:44:43 -0400 | |
commit | db7a947275c7bcb44a095b25ccf95526af68d737 (patch) | |
tree | d2c3e249ae3f66b0dc3092b7dc465c606e4dae16 | |
parent | 036679102be68e0f1bb12c3e9a354bb743fde219 (diff) |
Basis indents and type-checks with new twiddle syntax
-rw-r--r-- | lib/basis.urs | 256 | ||||
-rw-r--r-- | src/elisp/urweb-move.el | 6 | ||||
-rw-r--r-- | src/urweb.grm | 23 | ||||
-rw-r--r-- | tests/empty.urp | 2 |
4 files changed, 170 insertions, 117 deletions
diff --git a/lib/basis.urs b/lib/basis.urs index c1030874..352cd77a 100644 --- a/lib/basis.urs +++ b/lib/basis.urs @@ -52,42 +52,46 @@ con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type con sql_subset :: {{Type}} -> {{Type}} -> Type val sql_subset : keep_drop :: {({Type} * {Type})} - -> sql_subset - (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => - [nm] ~ acc => fields.1 ~ fields.2 => - [nm = fields.1 ++ fields.2] ++ acc) [] keep_drop) - (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => - [nm] ~ acc => - [nm = fields.1] ++ acc) [] keep_drop) -val sql_subset_all : tables :: {{Type}} - -> sql_subset tables tables + -> sql_subset + (fold (fn nm (fields :: ({Type} * {Type})) + acc [[nm] ~ acc] + [fields.1 ~ fields.2] => + [nm = fields.1 ++ fields.2] + ++ acc) [] keep_drop) + (fold (fn nm (fields :: ({Type} * {Type})) + acc [[nm] ~ acc] => + [nm = fields.1] ++ acc) + [] keep_drop) +val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables val sql_query1 : tables ::: {{Type}} - -> grouped ::: {{Type}} - -> selectedFields ::: {{Type}} - -> selectedExps ::: {Type} - -> {From : $(fold (fn nm => fn fields :: {Type} => fn acc => - [nm] ~ acc => [nm = sql_table fields] ++ acc) [] tables), - Where : sql_exp tables [] [] bool, - GroupBy : sql_subset tables grouped, - Having : sql_exp grouped tables [] bool, - SelectFields : sql_subset grouped selectedFields, - SelectExps : $(fold (fn nm => fn t :: Type => fn acc => - [nm] ~ acc => [nm = sql_exp grouped tables [] t] ++ acc) [] selectedExps) } - -> sql_query1 tables selectedFields selectedExps + -> grouped ::: {{Type}} + -> selectedFields ::: {{Type}} + -> selectedExps ::: {Type} + -> {From : $(fold (fn nm (fields :: {Type}) acc [[nm] ~ acc] => + [nm = sql_table fields] ++ acc) + [] tables), + Where : sql_exp tables [] [] bool, + GroupBy : sql_subset tables grouped, + Having : sql_exp grouped tables [] bool, + SelectFields : sql_subset grouped selectedFields, + SelectExps : $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => + [nm = sql_exp grouped tables [] t] + ++ acc) [] selectedExps) } + -> sql_query1 tables selectedFields selectedExps type sql_relop val sql_union : sql_relop val sql_intersect : sql_relop val sql_except : sql_relop val sql_relop : tables1 ::: {{Type}} - -> tables2 ::: {{Type}} - -> selectedFields ::: {{Type}} - -> selectedExps ::: {Type} - -> sql_relop - -> sql_query1 tables1 selectedFields selectedExps - -> sql_query1 tables2 selectedFields selectedExps - -> sql_query1 selectedFields selectedFields selectedExps + -> tables2 ::: {{Type}} + -> selectedFields ::: {{Type}} + -> selectedExps ::: {Type} + -> sql_relop + -> sql_query1 tables1 selectedFields selectedExps + -> sql_query1 tables2 selectedFields selectedExps + -> sql_query1 selectedFields selectedFields selectedExps type sql_direction val sql_asc : sql_direction @@ -96,54 +100,63 @@ val sql_desc : sql_direction con sql_order_by :: {{Type}} -> {Type} -> Type val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type - -> sql_exp tables [] exps t -> sql_direction -> sql_order_by tables exps - -> sql_order_by tables exps + -> sql_exp tables [] exps t -> sql_direction + -> sql_order_by tables exps + -> sql_order_by tables exps type sql_limit val sql_no_limit : sql_limit val sql_limit : int -> sql_limit - + type sql_offset val sql_no_offset : sql_offset val sql_offset : int -> sql_offset val sql_query : tables ::: {{Type}} - -> selectedFields ::: {{Type}} - -> selectedExps ::: {Type} - -> {Rows : sql_query1 tables selectedFields selectedExps, - OrderBy : sql_order_by tables selectedExps, - Limit : sql_limit, - Offset : sql_offset} - -> sql_query selectedFields selectedExps - -val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}} - -> exps ::: {Type} - -> tab :: Name -> field :: Name - -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg exps fieldType - -val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} -> nm :: Name - -> sql_exp tabs agg ([nm = t] ++ rest) t + -> selectedFields ::: {{Type}} + -> selectedExps ::: {Type} + -> {Rows : sql_query1 tables selectedFields selectedExps, + OrderBy : sql_order_by tables selectedExps, + Limit : sql_limit, + Offset : sql_offset} + -> sql_query selectedFields selectedExps + +val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} + -> fieldType ::: Type -> agg ::: {{Type}} + -> exps ::: {Type} + -> tab :: Name -> field :: Name + -> sql_exp + ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) + agg exps fieldType + +val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} + -> nm :: Name + -> sql_exp tabs agg ([nm = t] ++ rest) t class sql_injectable val sql_bool : sql_injectable bool val sql_int : sql_injectable int val sql_float : sql_injectable float val sql_string : sql_injectable string -val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type - -> sql_injectable t -> t -> sql_exp tables agg exps t +val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type + -> sql_injectable t -> t -> sql_exp tables agg exps t con sql_unary :: Type -> Type -> Type val sql_not : sql_unary bool bool -val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> arg ::: Type -> res ::: Type - -> sql_unary arg res -> sql_exp tables agg exps arg -> sql_exp tables agg exps res +val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> arg ::: Type -> res ::: Type + -> sql_unary arg res -> sql_exp tables agg exps arg + -> sql_exp tables agg exps res con sql_binary :: Type -> Type -> Type -> Type val sql_and : sql_binary bool bool bool val sql_or : sql_binary bool bool bool val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type - -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 -> sql_exp tables agg exps arg2 - -> sql_exp tables agg exps res + -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type + -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 + -> sql_exp tables agg exps arg2 + -> sql_exp tables agg exps res type sql_comparison val sql_eq : sql_comparison @@ -159,11 +172,13 @@ val sql_comparison : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> sql_exp tables agg exps bool val sql_count : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} - -> unit -> sql_exp tables agg exps int + -> unit -> sql_exp tables agg exps int con sql_aggregate :: Type -> Type -val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type - -> sql_aggregate t -> sql_exp agg agg exps t -> sql_exp tables agg exps t +val sql_aggregate : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} + -> t ::: Type + -> sql_aggregate t -> sql_exp agg agg exps t + -> sql_exp tables agg exps t class sql_summable val sql_summable_int : sql_summable int @@ -183,19 +198,21 @@ val sql_min : t ::: Type -> sql_maxable t -> sql_aggregate t con transaction :: Type -> Type val return : t ::: Type - -> t -> transaction t + -> t -> transaction t val bind : t1 ::: Type -> t2 ::: Type - -> transaction t1 -> (t1 -> transaction t2) - -> transaction t2 + -> transaction t1 -> (t1 -> transaction t2) + -> transaction t2 -val query : tables ::: {{Type}} -> exps ::: {Type} -> tables ~ exps - => state ::: Type - -> sql_query tables exps - -> ($(exps ++ fold (fn nm (fields :: {Type}) acc => [nm] ~ acc => [nm = $fields] ++ acc) [] tables) - -> state - -> transaction state) - -> state - -> transaction state +val query : tables ::: {{Type}} -> exps ::: {Type} + -> fn [tables ~ exps] => + state ::: Type + -> sql_query tables exps + -> ($(exps ++ fold (fn nm (fields :: {Type}) [[nm] ~ acc] => + [nm = $fields] ++ acc) [] tables) + -> state + -> transaction state) + -> state + -> transaction state (*** Database mutators *) @@ -204,22 +221,26 @@ type dml val dml : dml -> transaction unit val insert : fields ::: {Type} - -> sql_table fields - -> $(fold (fn nm (t :: Type) acc => [nm] ~ acc => - [nm = sql_exp [] [] [] t] ++ acc) [] fields) - -> dml - -val update : changed :: {Type} -> unchanged ::: {Type} -> changed ~ unchanged - => $(fold (fn nm (t :: Type) acc => [nm] ~ acc => - [nm = sql_exp [T = changed ++ unchanged] [] [] t] ++ acc) [] changed) - -> sql_table (changed ++ unchanged) - -> sql_exp [T = changed ++ unchanged] [] [] bool - -> dml + -> sql_table fields + -> $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => + [nm = sql_exp [] [] [] t] ++ acc) + [] fields) + -> dml + +val update : changed :: {Type} -> unchanged ::: {Type} -> + fn [changed ~ unchanged] => + $(fold (fn nm (t :: Type) acc [[nm] ~ acc] => + [nm = sql_exp [T = changed ++ unchanged] [] [] t] + ++ acc) + [] changed) + -> sql_table (changed ++ unchanged) + -> sql_exp [T = changed ++ unchanged] [] [] bool + -> dml val delete : fields ::: {Type} - -> sql_table fields - -> sql_exp [T = fields] [] [] bool - -> dml + -> sql_table fields + -> sql_exp [T = fields] [] [] bool + -> dml (*** Sequences *) @@ -234,24 +255,29 @@ con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type con xml :: {Unit} -> {Type} -> {Type} -> Type val cdata : ctx ::: {Unit} -> use ::: {Type} -> string -> xml ctx use [] -val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} -> attrsGiven ~ attrsAbsent - => ctxOuter ::: {Unit} -> ctxInner ::: {Unit} - -> useOuter ::: {Type} -> useInner ::: {Type} -> useOuter ~ useInner - => bindOuter ::: {Type} -> bindInner ::: {Type} -> bindOuter ~ bindInner - => $attrsGiven - -> tag (attrsGiven ++ attrsAbsent) ctxOuter ctxInner useOuter bindOuter - -> xml ctxInner useInner bindInner - -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) +val tag : attrsGiven ::: {Type} -> attrsAbsent ::: {Type} + -> ctxOuter ::: {Unit} -> ctxInner ::: {Unit} + -> useOuter ::: {Type} -> useInner ::: {Type} + -> bindOuter ::: {Type} -> bindInner ::: {Type} + -> fn [attrsGiven ~ attrsAbsent] + [useOuter ~ useInner] + [bindOuter ~ bindInner] => + $attrsGiven + -> tag (attrsGiven ++ attrsAbsent) + ctxOuter ctxInner useOuter bindOuter + -> xml ctxInner useInner bindInner + -> xml ctxOuter (useOuter ++ useInner) (bindOuter ++ bindInner) val join : ctx ::: {Unit} -> use1 ::: {Type} -> bind1 ::: {Type} -> bind2 ::: {Type} - -> use1 ~ bind1 => bind1 ~ bind2 - => xml ctx use1 bind1 - -> xml ctx (use1 ++ bind1) bind2 - -> xml ctx use1 (bind1 ++ bind2) -val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} -> bind ::: {Type} - -> use1 ~ use2 - => xml ctx use1 bind - -> xml ctx (use1 ++ use2) bind + -> fn [use1 ~ bind1] [bind1 ~ bind2] => + xml ctx use1 bind1 + -> xml ctx (use1 ++ bind1) bind2 + -> xml ctx use1 (bind1 ++ bind2) +val useMore : ctx ::: {Unit} -> use1 ::: {Type} -> use2 ::: {Type} + -> bind ::: {Type} + -> fn [use1 ~ use2] => + xml ctx use1 bind + -> xml ctx (use1 ++ use2) bind con xhtml = xml [Html] con page = xhtml [] [] @@ -272,10 +298,14 @@ val head : unit -> tag [] html head [] [] val title : unit -> tag [] head [] [] [] val body : unit -> tag [] html body [] [] -con bodyTag = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit - -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] -con bodyTagStandalone = fn attrs :: {Type} => ctx ::: {Unit} -> [Body] ~ ctx => unit - -> tag attrs ([Body] ++ ctx) [] [] [] +con bodyTag = fn (attrs :: {Type}) => + ctx ::: {Unit} -> + fn [[Body] ~ ctx] => + unit -> tag attrs ([Body] ++ ctx) ([Body] ++ ctx) [] [] +con bodyTagStandalone = fn (attrs :: {Type}) => + ctx ::: {Unit} + -> fn [[Body] ~ ctx] => + unit -> tag attrs ([Body] ++ ctx) [] [] [] val br : bodyTagStandalone [] @@ -289,13 +319,15 @@ val li : bodyTag [] val a : bodyTag [Link = transaction page] -val lform : ctx ::: {Unit} -> [Body] ~ ctx => bind ::: {Type} - -> xml form [] bind - -> xml ([Body] ++ ctx) [] [] -con lformTag = fn ty :: Type => fn inner :: {Unit} => fn attrs :: {Type} => - ctx ::: {Unit} -> [LForm] ~ ctx - => nm :: Name -> unit - -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty] +val lform : ctx ::: {Unit} -> bind ::: {Type} + -> fn [[Body] ~ ctx] => + xml form [] bind + -> xml ([Body] ++ ctx) [] [] +con lformTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => + ctx ::: {Unit} + -> fn [[LForm] ~ ctx] => + nm :: Name -> unit + -> tag attrs ([LForm] ++ ctx) inner [] [nm = ty] val textbox : lformTag string [] [Value = string] val password : lformTag string [] [] val ltextarea : lformTag string [] [] @@ -310,9 +342,11 @@ con select = [Select] val lselect : lformTag string select [] val loption : unit -> tag [Value = string] select [] [] [] -val submit : ctx ::: {Unit} -> [LForm] ~ ctx - => use ::: {Type} -> unit - -> tag [Action = $use -> transaction page] ([LForm] ++ ctx) ([LForm] ++ ctx) use [] +val submit : ctx ::: {Unit} -> use ::: {Type} + -> fn [[LForm] ~ ctx] => + unit + -> tag [Action = $use -> transaction page] + ([LForm] ++ ctx) ([LForm] ++ ctx) use [] (*** Tables *) diff --git a/src/elisp/urweb-move.el b/src/elisp/urweb-move.el index 3c7d5b21..41fc4cc5 100644 --- a/src/elisp/urweb-move.el +++ b/src/elisp/urweb-move.el @@ -76,9 +76,7 @@ ((">" ">=" "<>" "<" "<=" "=") . 4) (("+" "-" "^") . 6) (("/" "*" "%") . 7) - (("++" "--") 8) - (("NOT") 9) - (("~") 10))) + (("NOT") 9))) "Alist of Ur/Web infix operators and their precedence.") (defconst urweb-syntax-prec @@ -91,7 +89,7 @@ (("<-") . 55) ("||" . 70) ("&&" . 80) - ((":" "::" ":::" ":>") . 90) + ((":" ":>") . 90) ("->" . 95) ("with" . 100) (,(cons "end" urweb-begin-syms) . 10000))) diff --git a/src/urweb.grm b/src/urweb.grm index b7b09227..3c270100 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -529,7 +529,6 @@ cexp : capps (capps) | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) - | cterm TWIDDLE cterm DARROW cexp(CDisjoint (cterm1, cterm2, cexp), s (cterm1left, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -592,6 +591,13 @@ cargp : SYMBOL (fn (c, k) => ((CAbs (SYMBOL, SOME kind, c), loc), (KArrow (kind, k), loc)) end) + | LBRACK cterm TWIDDLE cterm RBRACK (fn (c, k) => + let + val loc = s (LBRACKleft, RBRACKright) + in + ((CDisjoint (cterm1, cterm2, c), loc), + k) + end) path : SYMBOL ([], SYMBOL) | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) @@ -650,7 +656,6 @@ eexp : eapps (eapps) in #1 (eargs (eexp, (CWild (KType, loc), loc))) end) - | LBRACK cterm TWIDDLE cterm RBRACK DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (LBRACKleft, RBRACKright)) | eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright)) | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright)) | CASE eexp OF barOpt branch branchs (ECase (eexp, branch :: branchs), s (CASEleft, branchsright)) @@ -709,6 +714,13 @@ earg : SYMBOL kcolon kind (fn (e, t) => ((EAbs ("_", SOME cexp, e), loc), (TFun (cexp, t), loc)) end) + | cterm TWIDDLE cterm (fn (e, t) => + let + val loc = s (cterm1left, cterm2right) + in + ((EDisjoint (cterm1, cterm2, e), loc), + (CDisjoint (cterm1, cterm2, t), loc)) + end) | eargp (eargp) eargp : SYMBOL (fn (e, t) => @@ -754,6 +766,13 @@ eargp : SYMBOL (fn (e, t) => ((EAbs ("_", SOME cexp, e), loc), (TFun (cexp, t), loc)) end) + | LPAREN cterm TWIDDLE cterm RPAREN(fn (e, t) => + let + val loc = s (LPARENleft, RPARENright) + in + ((EDisjoint (cterm1, cterm2, e), loc), + (CDisjoint (cterm1, cterm2, t), loc)) + end) eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) | LPAREN etuple RPAREN (let diff --git a/tests/empty.urp b/tests/empty.urp new file mode 100644 index 00000000..7387128d --- /dev/null +++ b/tests/empty.urp @@ -0,0 +1,2 @@ +debug + |