Mercurial > meta

comparison variant.ur @ 20:296807a9fd50

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Variant.foldR and appR
author Adam Chlipala <adam@chlipala.net>
date Mon, 02 Jan 2012 17:23:31 -0500
parents 744bf911dcc6
children e7d64ea0f922
comparison
equal deleted inserted replaced
19:875221eee987 20:296807a9fd50
52 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t) 52 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t)
53 [r' ::_] [[nm] ++ r ~ r'] f' acc' => 53 [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
54 f' (make [nm] {}) (acc [[nm] ++ r'] f' acc')) 54 f' (make [nm] {}) (acc [[nm] ++ r'] f' acc'))
55 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f 55 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
56 56
57 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]
59 (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr)
60 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t)
61 [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
62 f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc'))
63 (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f
64
65 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 ())
67
57 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] 68 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
58 (f : p :: K -> f p -> fr p -> t) 69 (f : p :: K -> f p -> fr p -> t)
59 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t = 70 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
60 match v 71 match v
61 (@Top.mp [fr] [fn p => f p -> t] 72 (@Top.mp [fr] [fn p => f p -> t]
64 75
65 fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type] 76 fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type]
66 (f : p :: K -> f1 p -> f2 p -> fr p -> t) 77 (f : p :: K -> f1 p -> f2 p -> fr p -> t)
67 [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t = 78 [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t =
68 match v1 79 match v1
69 (@foldR [fr] [fn r => others :: {K} -> [others ~ r] => 80 (@Top.foldR [fr] [fn r => others :: {K} -> [others ~ r] =>
70 folder (r ++ others) 81 folder (r ++ others)
71 -> variant (map f2 (r ++ others)) 82 -> variant (map f2 (r ++ others))
72 -> $(map (fn p => f1 p -> option t) r)] 83 -> $(map (fn p => f1 p -> option t) r)]
73 (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p) 84 (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p)
74 (acc : others :: {K} -> [others ~ r] => 85 (acc : others :: {K} -> [others ~ r] =>