Mercurial > meta
comparison variant.ur @ 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 |
---|---|
34 | 34 |
35 fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t = | 35 fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t = |
36 match v ({nm = Some} | 36 match v ({nm = Some} |
37 ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl) | 37 ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl) |
38 | 38 |
39 fun weaken [r1 ::: {Type}] [r2 ::: {Type}] [r1 ~ r2] (fl : folder r1) (v : variant r1) : variant (r1 ++ r2) = | |
40 match v | |
41 (@fold [fn r => r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)] | |
42 (fn [nm :: Name] [t ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Type} -> [r ~ r'] => $(map (fn t => t -> variant (r ++ r')) r)) [r'::_] [[nm = t] ++ r ~ r'] => | |
43 {nm = make [nm]} ++ acc [[nm = t] ++ r']) | |
44 (fn [r'::_] [[] ~ r'] => {}) fl [r2] !) | |
45 | |
39 fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool = | 46 fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool = |
40 match v1 | 47 match v1 |
41 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)] | 48 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)] |
42 (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r] | 49 (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r] |
43 (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)) | 50 (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)) |
52 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t) | 59 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t) |
53 [r' ::_] [[nm] ++ r ~ r'] f' acc' => | 60 [r' ::_] [[nm] ++ r ~ r'] f' acc' => |
54 f' (make [nm] {}) (acc [[nm] ++ r'] f' acc')) | 61 f' (make [nm] {}) (acc [[nm] ++ r'] f' acc')) |
55 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f | 62 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f |
56 | 63 |
64 fun mp [r ::: {Unit}] [t ::: Type] (fl : folder r) (f : variant (mapU {} r) -> t) : $(mapU t r) = | |
65 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r)] | |
66 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] | |
67 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t) -> $(mapU t r)) | |
68 [r' ::_] [[nm] ++ r ~ r'] f' => | |
69 {nm = f' (make [nm] {})} ++ acc [[nm] ++ r'] f') | |
70 (fn [r' ::_] [[] ~ r'] _ => {}) fl [[]] ! f | |
71 | |
57 fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t = | 72 fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t = |
58 @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t] | 73 @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t] |
59 (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr) | 74 (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr) |
60 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t) | 75 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t) |
61 [r' ::_] [[nm] ++ r ~ r'] f' acc' => | 76 [r' ::_] [[nm] ++ r ~ r'] f' acc' => |
62 f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc')) | 77 f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc')) |
63 (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f | 78 (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f |
64 | 79 |
65 fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} = | 80 fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} = |
66 @foldR fl (fn var this acc => f var this; acc) record (return ()) | 81 @foldR fl (fn var this acc => f var this; acc) record (return ()) |
82 | |
83 fun mapR [tr] [t] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> t) (record : $(mapU tr r)) : $(mapU t r) = | |
84 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)] | |
85 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] | |
86 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t) -> $(mapU tr r) -> $(mapU t r)) | |
87 [r' ::_] [[nm] ++ r ~ r'] f' vs => | |
88 {nm = f' (make [nm] {}) vs.nm} ++ acc [[nm] ++ r'] f' (vs -- nm)) | |
89 (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! f record | |
67 | 90 |
68 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] | 91 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] |
69 (f : p :: K -> f p -> fr p -> t) | 92 (f : p :: K -> f p -> fr p -> t) |
70 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = | 93 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = |
71 match v | 94 match v |