comparison lib/ur/basis.urs @ 758:8323c1beef2e

Subforms type-checks; lists urlified and unurlified
author Adam Chlipala <adamc@hcoop.net>
date Thu, 30 Apr 2009 11:48:56 -0400
parents fa2019a63ea4
children 21f6d2e65685
comparison
equal deleted inserted replaced
757:fa2019a63ea4 758:8323c1beef2e
564 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type} 564 val subform : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
565 -> [[Form] ~ ctx] => 565 -> [[Form] ~ ctx] =>
566 nm :: Name -> [[nm] ~ use] => 566 nm :: Name -> [[nm] ~ use] =>
567 xml form [] bind 567 xml form [] bind
568 -> xml ([Form] ++ ctx) use [nm = $bind] 568 -> xml ([Form] ++ ctx) use [nm = $bind]
569 569
570 val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
571 -> [[Form] ~ ctx] =>
572 nm :: Name -> [[nm] ~ use] =>
573 xml [Body, Subform] [Entry = $bind] []
574 -> xml ([Form] ++ ctx) use [nm = list ($bind)]
575
576 val entry : ctx ::: {Unit} -> bind ::: {Type}
577 -> [[Subform] ~ ctx] =>
578 xml form [] bind
579 -> xml ([Subform] ++ ctx) [Entry = $bind] []
580
570 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) => 581 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
571 ctx ::: {Unit} 582 ctx ::: {Unit}
572 -> [[Form] ~ ctx] => 583 -> [[Form] ~ ctx] =>
573 nm :: Name -> unit 584 nm :: Name -> unit
574 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty] 585 -> tag attrs ([Form] ++ ctx) inner [] [nm = ty]