changeset 141:63c699450281

Initial form support
author Adam Chlipala <adamc@hcoop.net>
date Sun, 20 Jul 2008 11:33:23 -0400
parents f214c535d253
children 6f9e224692ec
files lib/basis.lig src/elaborate.sml src/lacweb.grm src/monoize.sml tests/form.lac
diffstat 5 files changed, 100 insertions(+), 55 deletions(-) [+]
line wrap: on
line diff
--- a/lib/basis.lig	Sun Jul 20 10:40:25 2008 -0400
+++ b/lib/basis.lig	Sun Jul 20 11:33:23 2008 -0400
@@ -9,7 +9,7 @@
 
 
 con xml :: {Unit} -> {Type} -> {Type} -> Type
-val cdata : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} -> string -> xml ctx use bind
+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
@@ -32,7 +32,7 @@
 con html = [Html]
 con head = [Head]
 con body = [Body]
-con form = [Body, Form]
+con lform = [Body, LForm]
 
 val head : unit -> tag [] html head [] []
 val title : unit -> tag [] head [] [] []
@@ -40,6 +40,10 @@
 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) [] [] []
+
+val br : bodyTagStandalone []
 
 val p : bodyTag []
 val b : bodyTag []
@@ -51,4 +55,11 @@
 
 val a : bodyTag [Link = page]
 
-val form : unit -> tag [] [Body] [Form] [] []
+val lform : ctx ::: {Unit} -> [Body] ~ ctx -> bind ::: {Type}
+        -> xml lform [] bind
+        -> xml ([Body] ++ ctx) [] []
+con lformTag = fn ty :: Type => fn attrs :: {Type} =>
+        ctx ::: {Unit} -> [LForm] ~ ctx
+        -> nm :: Name -> unit
+        -> tag attrs ([LForm] ++ ctx) [] [] [nm = ty]
+val textbox : lformTag string []
--- a/src/elaborate.sml	Sun Jul 20 10:40:25 2008 -0400
+++ b/src/elaborate.sml	Sun Jul 20 11:33:23 2008 -0400
@@ -444,7 +444,7 @@
        | COccursCheckFailed of L'.con * L'.con
        | CIncompatible of L'.con * L'.con
        | CExplicitness of L'.con * L'.con
-       | CKindof of L'.con
+       | CKindof of L'.kind * L'.con
        | CRecordFailure
 
 exception CUnify' of cunify_error
@@ -468,9 +468,10 @@
         eprefaces "Differing constructor function explicitness"
                   [("Con 1", p_con env c1),
                    ("Con 2", p_con env c2)]
-      | CKindof c =>
+      | CKindof (k, c) =>
         eprefaces "Kind unification variable blocks kindof calculation"
-                  [("Con", p_con env c)]
+                  [("Kind", p_kind k),
+                   ("Con", p_con env c)]
       | CRecordFailure =>
         eprefaces "Can't unify record constructors" []
 
@@ -526,10 +527,10 @@
         end
 
       | L'.CApp (c, _) =>
-        (case #1 (hnormKind (kindof env c)) of
-             L'.KArrow (_, k) => k
-           | L'.KError => kerror
-           | _ => raise CUnify' (CKindof c))
+        (case hnormKind (kindof env c) of
+             (L'.KArrow (_, k), _) => k
+           | (L'.KError, _) => kerror
+           | k => raise CUnify' (CKindof (k, c)))
       | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
       | L'.CDisjoint (_, _, c) => kindof env c
 
@@ -551,7 +552,8 @@
         fun rkindof c =
             case kindof env c of
                 (L'.KRecord k, _) => k
-              | _ => raise CUnify' (CKindof c)
+              | (L'.KError, _) => kerror
+              | k => raise CUnify' (CKindof (k, c))
 
         val k1 = rkindof c1
         val k2 = rkindof c2
@@ -643,7 +645,8 @@
               | (_, _, (_, r) :: rest) =>
                 let
                     val r' = ref NONE
-                    val cr' = (L'.CUnif (dummy, k, "recd", r'), dummy)
+                    val kr = (L'.KRecord k, dummy)
+                    val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
 
                     val prefix = case (fs, others) of
                                      ([], other :: others) =>
--- a/src/lacweb.grm	Sun Jul 20 10:40:25 2008 -0400
+++ b/src/lacweb.grm	Sun Jul 20 11:33:23 2008 -0400
@@ -90,6 +90,8 @@
  | rexp of (con * exp) list
  | xml of exp
  | xmlOne of exp
+ | tag of string * exp
+ | tagHead of string * exp
 
  | attrs of (con * exp) list
  | attr of con * exp
@@ -306,47 +308,61 @@
        | ident EQ eexp                  ([(ident, eexp)])
        | ident EQ eexp COMMA rexp       ((ident, eexp) :: rexp)
 
-xml    : xmlOne xml                  (let
-                                          val pos = s (xmlOneleft, xmlright)
-                                      in
-                                          (EApp ((EApp (
-                                                  (EVar (["Basis"], "join"), pos),
+xml    : xmlOne xml                     (let
+                                             val pos = s (xmlOneleft, xmlright)
+                                         in
+                                             (EApp ((EApp (
+                                                     (EVar (["Basis"], "join"), pos),
                                                   xmlOne), pos),
-                                                 xml), pos)
-                                      end)
-       | xmlOne                      (xmlOne)
+                                                    xml), pos)
+                                         end)
+       | xmlOne                         (xmlOne)
 
-xmlOne : NOTAGS                      (EApp ((EVar (["Basis"], "cdata"), s (NOTAGSleft, NOTAGSright)),
-                                            (EPrim (Prim.String NOTAGS), s (NOTAGSleft, NOTAGSright))),
-                                      s (NOTAGSleft, NOTAGSright))
-       | BEGIN_TAG attrs DIVIDE GT   (let
-                                          val pos = s (BEGIN_TAGleft, GTright)
-                                      in
-                                          (EApp ((EApp ((EApp ((EVar (["Basis"], "tag"), pos),
-                                                               (ERecord attrs, pos)), pos),
-                                                        ((EApp ((EVar ([], BEGIN_TAG), pos),
-                                                                (ERecord [], pos)), pos))),
-                                                  pos),
-                                                 (EApp ((EVar (["Basis"], "cdata"), pos),
-                                                        (EPrim (Prim.String ""), pos)),
-                                                  pos)), pos)
-                                      end)
+xmlOne : NOTAGS                         (EApp ((EVar (["Basis"], "cdata"), s (NOTAGSleft, NOTAGSright)),
+                                               (EPrim (Prim.String NOTAGS), s (NOTAGSleft, NOTAGSright))),
+                                         s (NOTAGSleft, NOTAGSright))
+       | tag DIVIDE GT                  (let
+                                             val pos = s (tagleft, GTright)
+                                         in
+                                             (EApp (#2 tag,
+                                                    (EApp ((EVar (["Basis"], "cdata"), pos),
+                                                           (EPrim (Prim.String ""), pos)),
+                                                     pos)), pos)
+                                         end)
+         
+       | tag GT xml END_TAG             (let
+                                             val pos = s (tagleft, GTright)
+                                         in
+                                             if #1 tag = END_TAG then
+                                                 if END_TAG = "lform" then
+                                                     (EApp ((EVar (["Basis"], "lform"), pos),
+                                                            xml), pos)
+                                                 else
+                                                     (EApp (#2 tag, xml), pos)
+                                             else
+                                                 (ErrorMsg.errorAt pos "Begin and end tags don't match.";
+                                                  (EFold, pos))
+                                         end)
+       | LBRACE eexp RBRACE             (eexp)
 
-       | BEGIN_TAG attrs GT xml END_TAG(let
-                                            val pos = s (BEGIN_TAGleft, GTright)
-                                        in
-                                            if BEGIN_TAG = END_TAG then
-                                                (EApp ((EApp ((EApp ((EVar (["Basis"], "tag"), pos),
-                                                                     (ERecord attrs, pos)), pos),
-                                                              (EApp ((EVar ([], BEGIN_TAG), pos),
-                                                                     (ERecord [], pos)), pos)),
-                                                        pos),
-                                                       xml), pos)
-                                            else
-                                                (ErrorMsg.errorAt pos "Begin and end tags don't match.";
-                                                 (EFold, pos))
-                                        end)
-       | LBRACE eexp RBRACE          (eexp)
+tag    : tagHead attrs                  (let
+                                             val pos = s (tagHeadleft, attrsright)
+                                         in
+                                             (#1 tagHead,
+                                              (EApp ((EApp ((EVar (["Basis"], "tag"), pos),
+                                                            (ERecord attrs, pos)), pos),
+                                                     (EApp (#2 tagHead,
+                                                            (ERecord [], pos)), pos)),
+                                               pos))
+                                         end)
+
+tagHead: BEGIN_TAG                      (let
+                                             val pos = s (BEGIN_TAGleft, BEGIN_TAGright)
+                                         in
+                                             (BEGIN_TAG,
+                                              (EVar ([], BEGIN_TAG), pos))
+                                         end)
+       | tagHead LBRACE cexp RBRACE     (#1 tagHead, (ECApp (#2 tagHead, cexp), s (tagHeadleft, RBRACEright)))
                                           
 attrs  :                                ([])
        | attr attrs                     (attr :: attrs)
--- a/src/monoize.sml	Sun Jul 20 10:40:25 2008 -0400
+++ b/src/monoize.sml	Sun Jul 20 11:33:23 2008 -0400
@@ -140,9 +140,7 @@
 
           | L.EApp (
             (L.ECApp (
-             (L.ECApp (
-              (L.ECApp ((L.EFfi ("Basis", "cdata"), _), _), _),
-              _), _),
+             (L.ECApp ((L.EFfi ("Basis", "cdata"), _), _), _),
              _), _),
             se) => (L'.EFfiApp ("Basis", "htmlifyString", [monoExp env se]), loc)
           | L.EApp (
@@ -234,8 +232,11 @@
 
             in
                 case xml of
-                    (L.EApp ((L.ECApp ((L.EFfi ("Basis", "cdata"), _),
-                                       _), _), (L.EPrim (Prim.String s), _)), _) =>
+                    (L.EApp ((L.ECApp (
+                              (L.ECApp ((L.EFfi ("Basis", "cdata"), _),
+                                        _), _),
+                              _), _),
+                             (L.EPrim (Prim.String s), _)), _) =>
                     if CharVector.all Char.isSpace s then
                         (L'.EStrcat (tagStart, (L'.EPrim (Prim.String "/>"), loc)), loc)
                     else
@@ -243,6 +244,14 @@
                   | _ => normal ()
             end
 
+          | L.EApp ((L.ECApp (
+                     (L.ECApp ((L.EFfi ("Basis", "lform"), _), _), _),
+                     _), _),
+                    xml) =>
+            (L'.EStrcat ((L'.EPrim (Prim.String "<form>"), loc),
+                         (L'.EStrcat (monoExp env xml,
+                                      (L'.EPrim (Prim.String "</form>"), loc)), loc)), loc)
+
           | L.EApp (e1, e2) => (L'.EApp (monoExp env e1, monoExp env e2), loc)
           | L.EAbs (x, dom, ran, e) =>
             (L'.EAbs (x, monoType env dom, monoType env ran, monoExp (Env.pushERel env x dom) e), loc)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/form.lac	Sun Jul 20 11:33:23 2008 -0400
@@ -0,0 +1,6 @@
+val main : unit -> page = fn () => <html><body>
+        <lform>
+                Name: <textbox{#Nam} /><br/>
+                Color: <textbox{#Color} /><br/>
+        </lform>
+</body></html>