Mercurial > meta
comparison variant.urs @ 21:e7d64ea0f922
Variant.weaken, mp, and mapR
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Thu, 05 Jan 2012 18:04:04 -0500 |
parents | 296807a9fd50 |
children | ca1c07d49b5e |
comparison
equal
deleted
inserted
replaced
20:296807a9fd50 | 21:e7d64ea0f922 |
---|---|
7 val find : r ::: {Unit} -> (variant (mapU {} r) -> bool) -> folder r -> option (variant (mapU {} r)) | 7 val find : r ::: {Unit} -> (variant (mapU {} r) -> bool) -> folder r -> option (variant (mapU {} r)) |
8 | 8 |
9 val test : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ([nm = t] ++ ts) | 9 val test : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ([nm = t] ++ ts) |
10 -> variant ([nm = t] ++ ts) -> option t | 10 -> variant ([nm = t] ++ ts) -> option t |
11 val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t | 11 val testLess : nm :: Name -> t ::: Type -> ts ::: {Type} -> [[nm] ~ ts] => folder ts -> variant ([nm = t] ++ ts) -> option t |
12 | |
13 val weaken : r1 ::: {Type} -> r2 ::: {Type} -> [r1 ~ r2] => folder r1 | |
14 -> variant r1 -> variant (r1 ++ r2) | |
12 | 15 |
13 val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] => | 16 val testEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] => |
14 Eq.eq r ([nm = t] ++ ts) | 17 Eq.eq r ([nm = t] ++ ts) |
15 -> folder r | 18 -> folder r |
16 -> variant (map f r) -> option (f t) | 19 -> variant (map f r) -> option (f t) |
20 val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] => | 23 val makeEq : K --> f :: (K -> Type) -> nm :: Name -> t ::: K -> ts ::: {K} -> r ::: {K} -> [[nm] ~ ts] => |
21 Eq.eq r ([nm = t] ++ ts) | 24 Eq.eq r ([nm = t] ++ ts) |
22 -> f t | 25 -> f t |
23 -> variant (map f r) | 26 -> variant (map f r) |
24 | 27 |
28 val mp : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t) -> $(mapU t r) | |
29 | |
25 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t | 30 val fold : r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> t -> t) -> t -> t |
26 | 31 |
27 val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t | 32 val foldR : tr ::: Type -> r ::: {Unit} -> t ::: Type -> folder r -> (variant (mapU {} r) -> tr -> t -> t) -> $(mapU tr r) -> t -> t |
28 | 33 |
29 val appR : m ::: (Type -> Type) -> monad m | 34 val appR : m ::: (Type -> Type) -> monad m |
30 -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {} | 35 -> tr ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> m {}) -> $(mapU tr r) -> m {} |
36 | |
37 val mapR : tr ::: Type -> t ::: Type -> r ::: {Unit} -> folder r -> (variant (mapU {} r) -> tr -> t) -> $(mapU tr r) -> $(mapU t r) | |
31 | 38 |
32 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type | 39 val destrR : K --> f :: (K -> Type) -> fr :: (K -> Type) -> t ::: Type |
33 -> (p :: K -> f p -> fr p -> t) | 40 -> (p :: K -> f p -> fr p -> t) |
34 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t | 41 -> r ::: {K} -> folder r -> variant (map f r) -> $(map fr r) -> t |
35 | 42 |