Mercurial > meta

comparison variant.ur @ 27:ca1c07d49b5e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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))