Mercurial > meta
diff variant.ur @ 14:744bf911dcc6
Update to expect implicit argument insertion for local variables
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 14 Jun 2011 08:55:15 -0400 |
parents | 799f43bce62b |
children | 296807a9fd50 |
line wrap: on
line diff
--- a/variant.ur Mon Mar 21 10:16:12 2011 -0400 +++ b/variant.ur Tue Jun 14 08:55:15 2011 -0400 @@ -2,7 +2,7 @@ match v (@fold [fn r => r' :: {Unit} -> [r ~ r'] => $(mapU t (r ++ r')) -> $(mapU ({} -> t) r)] (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> _) [r'::_] [[nm = u] ++ us ~ r'] r => - {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] ! r) + {nm = fn () => r.nm} ++ cs [[nm = u] ++ r'] r) (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) fun write [r ::: {Unit}] [t ::: Type] (fl : folder r) (r : $(mapU t r)) (v : variant (mapU {} r)) (x : t) : $(mapU t r) = @@ -11,7 +11,7 @@ (fn [nm :: Name] [u::_] [us::_] [[nm] ~ us] (cs : r' :: {Unit} -> [us ~ r'] => $(mapU t (us ++ r')) -> $(mapU ({} -> $(mapU t (us ++ r'))) us)) [r'::_] [[nm = u] ++ us ~ r'] r => - {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] ! r) + {nm = fn () => r -- nm ++ {nm = x}} ++ cs [[nm = u] ++ r'] r) (fn [r'::_] [[] ~ r'] _ => {}) fl [[]] ! r) fun search [r] [t] (f : variant (mapU {} r) -> option t) (fl : folder r) : option t = @@ -20,7 +20,7 @@ (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> option t) -> option t) [r' ::_] [[nm] ++ r ~ r'] f' => case f' (make [nm] {}) of - None => acc [[nm] ++ r'] ! f' + None => acc [[nm] ++ r'] f' | v => v) (fn [r' ::_] [[] ~ r'] _ => None) fl [[]] ! f @@ -43,7 +43,7 @@ (acc : r' :: {Unit} -> [r ~ r'] => folder (r ++ r') -> variant (mapU {} (r ++ r')) -> $(mapU ({} -> bool) r)) [r' ::_] [[nm] ++ r ~ r'] (fl' : folder ([nm] ++ r ++ r')) v => {nm = fn () => Option.isSome (@test [nm] ! (@Folder.mp fl') v)} - ++ acc [[nm] ++ r'] ! fl' v) + ++ @acc [[nm] ++ r'] ! fl' v) (fn [r' ::_] [[] ~ r'] _ _ => {}) fl [[]] ! fl v2) fun fold [r] [t] (fl : folder r) (f : variant (mapU {} r) -> t -> t) : t -> t = @@ -51,7 +51,7 @@ (fn [nm :: Name] [u ::_] [r ::_] [[nm] ~ r] (acc : r' :: {Unit} -> [r ~ r'] => (variant (mapU {} (r ++ r')) -> t -> t) -> t -> t) [r' ::_] [[nm] ++ r ~ r'] f' acc' => - f' (make [nm] {}) (acc [[nm] ++ r'] ! f' acc')) + f' (make [nm] {}) (acc [[nm] ++ r'] f' acc')) (fn [r' ::_] [[] ~ r'] _ x => x) fl [[]] ! f fun destrR [K] [f :: K -> Type] [fr :: K -> Type] [t ::: Type] @@ -81,7 +81,7 @@ {nm = fn x1 => match v2 ({nm = fn x2 => Some (f [p] x1 x2 meta)} ++ (@map0 [fn p => f2 p -> option t] (fn [p' ::_] _ => None) fl -- nm))} - ++ acc [[nm = p] ++ others] ! fl v2) + ++ @acc [[nm = p] ++ others] ! fl v2) (fn [others ::_] [others ~ []] _ _ => {}) fl r [[]] ! fl v2)