Mercurial > meta

annotate 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
rev   line source
adam@6 1 fun read [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) : t =
adam@6 2 match v
adam@6 3 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)]
adam@6 4 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r =>
adam@14 5 {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] r)
adam@6 6 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
adam@6 7
adam@6 8 fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) =
adam@6 9 match v
adam@6 10 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> $(mapU t (r ++ r'))) r)]
adam@6 11 (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us]
adam@6 12 (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us))
adam@6 13 [r'::_] [[nm = u] ++ us ~ r'] r =>
adam@14 14 {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] r)
adam@6 15 (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r)
adam@6 16
adam@6 17 fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t =
adam@6 18 @fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t]
adam@6 19 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
adam@6 20 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t)
adam@6 21 [r' ::_] [[nm] ++ r ~ r'] f' =>
adam@6 22 case f' (make [nm] {}) of
adam@14 23 None => acc [[nm] ++ r'] f'
adam@6 24 | v => v)
adam@6 25 (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f
adam@6 26
adam@6 27 fun find [r] (f : variant (mapU {} r) -> bool) (fl : folder r) : option (variant (mapU {} r)) =
adam@6 28 @search (fn v => if f v then Some v else None) fl
adam@6 29
adam@6 30 fun test [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ([nm = t] ++ ts))
adam@6 31 (v : variant ([nm = t] ++ ts)) : option t =
adam@6 32 match v ({nm = Some}
adam@6 33 ++ (@map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl -- nm))
adam@6 34
adam@6 35 fun testLess [nm :: Name] [t ::: Type] [ts ::: {Type}] [[nm] ~ ts] (fl : folder ts) (v : variant ([nm = t] ++ ts)) : option t =
adam@6 36 match v ({nm = Some}
adam@6 37 ++ @map0 [fn t' => t' -> option t] (fn [t' :: Type] _ => None) fl)
adam@6 38
adam@6 39 fun eq [r] (fl : folder r) (v1 : variant (mapU {} r)) (v2 : variant (mapU {} r)) : bool =
adam@6 40 match v1
adam@6 41 (@fold [fn r => r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)]
adam@6 42 (fn [nm ::_] [u ::_] [r ::_] [[nm] ~ r]
adam@6 43 (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r))
adam@6 44 [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v =>
adam@6 45 {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)}
adam@14 46 ++ @acc [[nm] ++ r'] ! fl' v)
adam@6 47 (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2)
adam@6 48
adam@6 49 fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t =
adam@6 50 @Top.fold [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t]
adam@6 51 (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r]
adam@6 52 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t)
adam@6 53 [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
adam@14 54 f' (make [nm] {}) (acc [[nm] ++ r'] f' acc'))
adam@6 55 (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f
adam@6 56
adam@20 57 fun foldR [tr] [r] [t] (fl : folder r) (f : variant (mapU {} r) -> tr -> t -> t) (record : $(mapU tr r)) : t -> t =
adam@20 58 @Top.foldUR [tr] [fn r => r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t]
adam@20 59 (fn [nm :: Name] [r ::_] [[nm] ~ r] (v : tr)
adam@20 60 (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> tr -> t -> t) -> t -> t)
adam@20 61 [r' ::_] [[nm] ++ r ~ r'] f' acc' =>
adam@20 62 f' (make [nm] {}) v (acc [[nm] ++ r'] f' acc'))
adam@20 63 (fn [r' ::_] [[] ~ r'] _ x => x) fl record [[]] ! f
adam@20 64
adam@20 65 fun appR [m] (_ : monad m) [tr] [r] (fl : folder r) (f : variant (mapU {} r) -> tr -> m {}) (record : $(mapU tr r)) : m {} =
adam@20 66 @foldR fl (fn var this acc => f var this; acc) record (return ())
adam@20 67
adam@6 68 fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type]
adam@6 69 (f : p :: K -> f p -> fr p -> t)
adam@6 70 [r ::: {K}] (fl : folder r) (v : variant (map f r)) (r : $(map fr r)) : t =
adam@6 71 match v
adam@6 72 (@Top.mp [fr] [fn p => f p -> t]
adam@6 73 (fn [p] (m : fr p) (v : f p) => f [p] v m)
adam@6 74 fl r)
adam@6 75
adam@6 76 fun destr2R [K] [f1 :: K -> Type] [f2 :: K -> Type] [fr :: K -> Type] [t ::: Type]
adam@6 77 (f : p :: K -> f1 p -> f2 p -> fr p -> t)
adam@6 78 [r ::: {K}] (fl : folder r) (v1 : variant (map f1 r)) (v2 : variant (map f2 r)) (r : $(map fr r)) : option t =
adam@6 79 match v1
adam@20 80 (@Top.foldR [fr] [fn r => others :: {K} -> [others ~ r] =>
adam@6 81 folder (r ++ others)
adam@6 82 -> variant (map f2 (r ++ others))
adam@6 83 -> $(map (fn p => f1 p -> option t) r)]
adam@6 84 (fn [nm ::_] [p ::_] [r ::_] [[nm] ~ r] (meta : fr p)
adam@6 85 (acc : others :: {K} -> [others ~ r] =>
adam@6 86 folder (r ++ others)
adam@6 87 -> variant (map f2 (r ++ others))
adam@6 88 -> $(map (fn p => f1 p -> option t) r))
adam@6 89 [others :: {K}] [others ~ [nm = p] ++ r]
adam@6 90 (fl : folder ([nm = p] ++ r ++ others))
adam@6 91 (v2 : variant (map f2 ([nm = p] ++ r ++ others))) =>
adam@6 92 {nm = fn x1 => match v2
adam@6 93 ({nm = fn x2 => Some (f [p] x1 x2 meta)}
adam@6 94 ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))}
adam@14 95 ++ @acc [[nm = p] ++ others] ! fl v2)
adam@6 96 (fn [others ::_] [others ~ []] _ _ => {})
adam@6 97 fl r [[]] ! fl v2)
adam@6 98
adam@6 99 fun testEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
adam@6 100 (pf : Eq.eq r ([nm = t] ++ ts)) (fl : folder r) (v : variant (map f r)) : option (f t) =
adam@6 101 @test [nm] ! (@Folder.mp (@Eq.cast pf [folder] fl))
adam@6 102 (Eq.cast pf [fn r => variant (map f r)] v)
adam@6 103
adam@6 104 fun makeEq [K] [f :: K -> Type] [nm :: Name] [t ::: K] [ts ::: {K}] [r ::: {K}] [[nm] ~ ts]
adam@6 105 (pf : Eq.eq r ([nm = t] ++ ts)) (x : f t) : variant (map f r) =
adam@6 106 Eq.cast (Eq.sym pf) [fn r => variant (map f r)] (make [nm] x)