Mercurial > urweb
comparison lib/ur/top.urs @ 631:effa7d43aac3
Make folders abstract
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 24 Feb 2009 14:04:07 -0500 |
parents | 6a6eb9882d57 |
children | 6c4643880df5 |
comparison
equal
deleted
inserted
replaced
630:6a6eb9882d57 | 631:effa7d43aac3 |
---|---|
1 (** Row folding *) | 1 (** Row folding *) |
2 | 2 |
3 con folder = K ==> fn r :: {K} => | 3 con folder :: K --> {K} -> Type |
4 tf :: ({K} -> Type) | |
5 -> (nm :: Name -> v :: K -> r :: {K} -> tf r | |
6 -> [[nm] ~ r] => tf ([nm = v] ++ r)) | |
7 -> tf [] -> tf r | |
8 | 4 |
9 structure Folder : sig | 5 structure Folder : sig |
6 val fold : K --> r ::: {K} -> folder r | |
7 -> tf :: ({K} -> Type) | |
8 -> (nm :: Name -> v :: K -> r :: {K} -> tf r | |
9 -> [[nm] ~ r] => tf ([nm = v] ++ r)) | |
10 -> tf [] -> tf r | |
11 | |
10 val nil : K --> folder (([]) :: {K}) | 12 val nil : K --> folder (([]) :: {K}) |
11 val cons : K --> r ::: {K} -> nm :: Name -> v :: K | 13 val cons : K --> r ::: {K} -> nm :: Name -> v :: K |
12 -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) | 14 -> [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) |
13 val concat : K --> r1 ::: {K} -> r2 ::: {K} | 15 val concat : K --> r1 ::: {K} -> r2 ::: {K} |
14 -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2) | 16 -> [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2) |