# HG changeset patch # User Adam Chlipala # Date 1216568003 14400 # Node ID 63c699450281937edba07b50dfbccbc8938f18f8 # Parent f214c535d25338f0021cd0ca49d63ab0bbfad75a Initial form support diff -r f214c535d253 -r 63c699450281 lib/basis.lig --- 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 [] diff -r f214c535d253 -r 63c699450281 src/elaborate.sml --- 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) => diff -r f214c535d253 -r 63c699450281 src/lacweb.grm --- 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) diff -r f214c535d253 -r 63c699450281 src/monoize.sml --- 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 "
"), loc), + (L'.EStrcat (monoExp env xml, + (L'.EPrim (Prim.String "
"), 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) diff -r f214c535d253 -r 63c699450281 tests/form.lac --- /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 () => + + Name:
+ Color:
+ +