Mercurial > feed
annotate src/ur/feed.urs @ 4:af95d9d73eb5
Feed.tree
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 11 Jan 2011 18:04:15 -0500 |
| parents | ea0ca570c121 |
| children | 2717458d8951 |
| rev | line source |
|---|---|
| adam@1 | 1 con pattern :: Type -> Type -> Type |
| adam@1 | 2 |
| adam@1 | 3 con tagInternal :: {Unit} -> Type |
| adam@1 | 4 |
| adam@4 | 5 val null : pattern unit (variant []) |
| adam@4 | 6 |
| adam@1 | 7 val tag : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs) |
| adam@1 | 8 -> pattern (tagInternal attrs) {Attrs : $(mapU string attrs), Cdata : option string} |
| adam@1 | 9 |
| adam@3 | 10 val tagA : attrs ::: {Unit} -> folder attrs -> string -> $(mapU string attrs) |
| adam@3 | 11 -> pattern (tagInternal attrs) $(mapU string attrs) |
| adam@3 | 12 val tagC : string -> pattern (tagInternal []) string |
| adam@3 | 13 |
| adam@1 | 14 con childrenInternal :: Type -> {Type} -> Type |
| adam@1 | 15 |
| adam@1 | 16 val children : parentI ::: Type -> parent ::: Type -> children ::: {(Type * Type)} |
| adam@1 | 17 -> pattern parentI parent -> $(map (fn (i, d) => pattern i d) children) -> folder children |
| adam@1 | 18 -> pattern (childrenInternal parentI (map fst children)) (parent * $(map snd children)) |
| adam@1 | 19 |
| adam@4 | 20 con treeInternal :: Type -> Type -> Type |
| adam@4 | 21 |
| adam@4 | 22 val tree : parentI ::: Type -> parent ::: Type -> childI ::: Type -> child ::: Type |
| adam@4 | 23 -> pattern parentI parent -> pattern childI child |
| adam@4 | 24 -> pattern (treeInternal parentI childI) (parent * child) |
| adam@4 | 25 |
| adam@1 | 26 val app : internal ::: Type -> data ::: Type -> pattern internal data -> (data -> transaction {}) -> string -> transaction {} |