Mercurial > meta
comparison variant.ur @ 27:ca1c07d49b5e
Type-directed case matching for variants.
author | Edward Z. Yang <ezyang@mit.edu> |
---|---|
date | Thu, 26 Jul 2012 16:39:02 -0400 |
parents | e7d64ea0f922 |
children | f55f66c6fdee |
comparison
equal
deleted
inserted
replaced
26:c1da0e3749b3 | 27:ca1c07d49b5e |
---|---|
125 (Eq.cast pf [fn r => variant (map f r)] v) | 125 (Eq.cast pf [fn r => variant (map f r)] v) |
126 | 126 |
127 fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts] | 127 fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts] |
128 (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) = | 128 (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) = |
129 Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x) | 129 Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x) |
130 | |
131 con variantMake ts' ts = $(map (fn t => t -> variant ts') ts) | |
132 con mkLabelsAccum r = s :: {Type} -> [r ~ s] => variantMake (r ++ s) r | |
133 fun mkLabels [ts ::: {Type}] (fl : folder ts) : variantMake ts ts | |
134 = @Top.fold [mkLabelsAccum] | |
135 (fn [nm::_] [v::_] [r::_] [[nm] ~ r] | |
136 (k : mkLabelsAccum r) | |
137 [s::_] [[nm = v] ++ r ~ s] => k [[nm = v] ++ s] ++ {nm = make [nm]}) | |
138 (fn [s::_] [[] ~ s] => {}) fl [[]] ! | |
139 | |
140 class type_case = fn ts t a => (a -> variant ts) -> a -> t | |
141 | |
142 fun declareCase [ts] [t] [a] (f : (a -> variant ts) -> a -> t) : type_case ts t a = f | |
143 fun typeCase [ts] [t] (v : variant ts) (dstrs : $(map (type_case ts t) ts)) (fl : folder ts) : t | |
144 (* Ur/Web not clever enough to calculate these folders, it seems *) | |
145 = match v (@ap [fn a => a -> variant ts] [fn a => a -> t] fl dstrs (@mkLabels fl)) |