Mercurial > urweb

changeset 354:527529a083d9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basis indents and type-checks with new twiddle syntax
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Oct 2008 11:44:43 -0400
parents 9390c55b9f1f
children fa2d25fe75ce
files lib/basis.urs src/elisp/urweb-move.el src/urweb.grm tests/empty.urp
diffstat 4 files changed, 167 insertions(+), 114 deletions(-) [+]
line wrap: on
line diff
--- a/lib/basis.urs	Sun Oct 12 10:48:01 2008 -0400
+++ b/lib/basis.urs	Sun Oct 12 11:44:43 2008 -0400
@@ -52,42 +52,46 @@
 
 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 @@
 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
+                -> 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_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
+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 @@
         -> 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 @@
 
 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 @@
 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
+             -> 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
+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 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 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 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 @@
 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 *)
 
--- a/src/elisp/urweb-move.el	Sun Oct 12 10:48:01 2008 -0400
+++ b/src/elisp/urweb-move.el	Sun Oct 12 11:44:43 2008 -0400
@@ -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)))
--- a/src/urweb.grm	Sun Oct 12 10:48:01 2008 -0400
+++ b/src/urweb.grm	Sun Oct 12 11:44:43 2008 -0400
@@ -529,7 +529,6 @@
        | 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 @@
                                                   ((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 @@
                                          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 @@
                                                 ((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 @@
                                                 ((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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/empty.urp	Sun Oct 12 11:44:43 2008 -0400
@@ -0,0 +1,2 @@
+debug
+