Mercurial > meta
changeset 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 | d05943db55e8 |
| children | 6ebc2ca594b7 |
| files | eq.ur incl.ur mem.ur sql.ur variant.ur |
| diffstat | 5 files changed, 38 insertions(+), 38 deletions(-) [+] |
line wrap: on
line diff
--- a/eq.ur Mon Mar 21 10:16:12 2011 -0400 +++ b/eq.ur Tue Jun 14 08:55:15 2011 -0400 @@ -18,7 +18,7 @@ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : pre :: {K} -> [pre ~ rest] => eq r (pre ++ rest) -> tf rest) [pre :: {K}] [pre ~ [nm = t] ++ rest] pf => - f [pre] [nm] [t] [rest] ! ! pf (acc [[nm = t] ++ pre] ! pf)) + f [pre] [nm] [t] [rest] pf (acc [[nm = t] ++ pre] pf)) (fn [pre :: {K}] [pre ~ []] _ => i) [r] fl [[]] ! refl fun foldUR [tr :: Type] [tf :: {Unit} -> Type] [r ::: {Unit}] @@ -27,7 +27,7 @@ (i : tf []) (fl : folder r) (r : $(mapU tr r)) : tf r = @@fold [fn r' => $(mapU tr r') -> tf r'] [r] (fn [pre :: {Unit}] [nm :: Name] [u :: Unit] [post :: {Unit}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r => - f [pre] [nm] [post] ! ! pf r.nm (acc (r -- nm))) + f [pre] [nm] [post] pf r.nm (acc (r -- nm))) (fn _ => i) fl r fun foldR [K] [tr :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] @@ -36,7 +36,7 @@ (i : tf []) (fl : folder r) (r : $(map tr r)) : tf r = @@fold [fn r' => $(map tr r') -> tf r'] [r] (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r => - f [pre] [nm] [t] [post] ! ! pf r.nm (acc (r -- nm))) + f [pre] [nm] [t] [post] pf r.nm (acc (r -- nm))) (fn _ => i) fl r fun foldR2 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] @@ -45,7 +45,7 @@ (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) : tf r = @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> tf r'] [r] (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 => - f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + f [pre] [nm] [t] [post] pf r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) (fn _ _ => i) fl r1 r2 fun foldR3 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] @@ -54,7 +54,7 @@ (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) : tf r = @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> tf r'] [r] (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 => - f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) + f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) (fn _ _ _ => i) fl r1 r2 r3 fun foldR4 [K] [tr1 :: K -> Type] [tr2 :: K -> Type] [tr3 :: K -> Type] [tr4 :: K -> Type] [tf :: {K} -> Type] [r ::: {K}] @@ -63,7 +63,7 @@ (i : tf []) (fl : folder r) (r1 : $(map tr1 r)) (r2 : $(map tr2 r)) (r3 : $(map tr3 r)) (r4 : $(map tr4 r)) : tf r = @@fold [fn r' => $(map tr1 r') -> $(map tr2 r') -> $(map tr3 r') -> $(map tr4 r') -> tf r'] [r] (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf acc r1 r2 r3 r4 => - f [pre] [nm] [t] [post] ! ! pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm))) + f [pre] [nm] [t] [post] pf r1.nm r2.nm r3.nm r4.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm) (r4 -- nm))) (fn _ _ _ _ => i) fl r1 r2 r3 r4 fun mp [K] [tr :: K -> Type] [tf :: K -> Type] [r ::: {K}] @@ -72,5 +72,5 @@ (fl : folder r) (r : $(map tr r)) : $(map tf r) = @@foldR [tr] [fn r => $(map tf r)] [r] (fn [pre :: {K}] [nm :: Name] [t :: K] [post :: {K}] [pre ~ post] [[nm] ~ pre ++ post] pf r acc => - {nm = f [nm] [t] [pre ++ post] ! pf r} ++ acc) + {nm = f [nm] [t] [pre ++ post] pf r} ++ acc) {} fl r
--- a/incl.ur Mon Mar 21 10:16:12 2011 -0400 +++ b/incl.ur Tue Jun 14 08:55:15 2011 -0400 @@ -1,15 +1,15 @@ con incl' = K ==> fn (r1 :: {K}) (r2 :: {K}) (r' :: {K}) => - [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'), - Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2} + [r1 ~ r'] => {Expose : f :: ({K} -> Type) -> f r2 -> f (r1 ++ r'), + Hide : f :: ({K} -> Type) -> f (r1 ++ r') -> f r2} con incl = K ==> fn (r1 :: {K}) (r2 :: {K}) => tp :: Type -> (r' :: {K} -> [r1 ~ r'] => incl' r1 r2 r' -> tp) -> tp fun incl [K] [r1 :: {K}] [r2 :: {K}] [r1 ~ r2] = - fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) => - f [r2] ! (fn [r1 ~ r2] => {Expose = fn [f :: ({K} -> Type)] x => x, - Hide = fn [f :: ({K} -> Type)] x => x}) - + fn [tp :: Type] (f : r' :: {K} -> [r1 ~ r'] => incl' r1 (r1 ++ r2) r' -> tp) => + f [r2] (fn [r1 ~ r2] => {Expose = fn [f :: ({K} -> Type)] x => x, + Hide = fn [f :: ({K} -> Type)] x => x}) + fun proj [r1 ::: {Type}] [r2 ::: {Type}] (i : incl r1 r2) (r : $r2) = i [$r1] (fn [r' :: {Type}] [r1 ~ r'] (i' : incl' r1 r2 r') => i'.Expose [fn r => $r] r --- r') @@ -19,22 +19,22 @@ (i : incl ([nm = t] ++ r) r') (f : nm :: Name -> t :: K -> r :: {K} -> [[nm] ~ r] => f nm t ([nm = t] ++ r)) = i [f nm t r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => - i'.Hide [f nm t] (f [nm] [t] [r ++ r''] !)) + i'.Hide [f nm t] (f [nm] [t] [r ++ r''])) fun inv2 [K] [nm :: Name] [t :: K] [r :: {K}] [r' :: {K}] [[nm] ~ r] (i : incl ([nm = t] ++ r) r') = i [incl r r'] (fn [r'' :: {K}] [[nm = t] ++ r ~ r''] (i' : incl' ([nm = t] ++ r) r' r'') => - fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) => - f [[nm = t] ++ r''] ! (fn [r ~ [nm = t] ++ r''] => - {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x, - Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x})) + fn [tp :: Type] (f : r''' :: {K} -> [r ~ r'''] => incl' r r' r''' -> tp) => + f [[nm = t] ++ r''] (fn [r ~ [nm = t] ++ r''] => + {Expose = fn [f :: ({K} -> Type)] (x : f r') => i'.Expose [f] x, + Hide = fn [f :: ({K} -> Type)] x => i'.Hide [f] x})) fun fold [K] [tf :: {K} -> Type] [r ::: {K}] - (f : nm :: Name -> v :: K -> r' :: {K} - -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r')) - (i : tf []) (fl : folder r) = + (f : nm :: Name -> v :: K -> r' :: {K} + -> [[nm] ~ r'] => incl ([nm = v] ++ r') r -> tf r' -> tf ([nm = v] ++ r')) + (i : tf []) (fl : folder r) = @Top.fold [fn r' => incl r' r -> tf r'] (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] acc i => - f [nm] [v] [r'] ! i (acc (inv2 [nm] [v] [r'] [r] i))) + f [nm] [v] [r'] i (acc (inv2 [nm] [v] [r'] [r] i))) (fn _ => i) fl (incl [r] [[]])
--- a/mem.ur Mon Mar 21 10:16:12 2011 -0400 +++ b/mem.ur Tue Jun 14 08:55:15 2011 -0400 @@ -7,18 +7,18 @@ fun mem [K] [nm :: Name] [t :: K] [r :: {K}] [[nm] ~ r] = fn [tp :: Type] (f : r' :: {K} -> [[nm] ~ r'] => mem' nm t ([nm = t] ++ r) r' -> tp) => - f [r] ! (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x, - Hide = fn [f :: {K} -> Type] x => x}) + f [r] (fn [[nm] ~ r] => {Expose = fn [f :: {K} -> Type] x => x, + Hide = fn [f :: {K} -> Type] x => x}) fun mp [K] [K2] [f :: K -> K2] [nm ::: Name] [t ::: K] [r ::: {K}] (m : mem nm t r) = m [mem nm (f t) (map f r)] (fn [r' :: {K}] [[nm] ~ r'] (m' : mem' nm t r r') => fn [tp :: Type] (f : r' :: {K2} -> [[nm] ~ r'] => mem' nm (f t) (map f r) r' -> tp) => - f [map f r'] ! (fn [[nm] ~ map f r'] => - {Expose = fn [f' :: {K2} -> Type] x => - m'.Expose [fn r => f' (map f r)] x, - Hide = fn [f' :: {K2} -> Type] x => - m'.Hide [fn r => f' (map f r)] x})) + f [map f r'] (fn [[nm] ~ map f r'] => + {Expose = fn [f' :: {K2} -> Type] x => + m'.Expose [fn r => f' (map f r)] x, + Hide = fn [f' :: {K2} -> Type] x => + m'.Hide [fn r => f' (map f r)] x})) fun proj [nm ::: Name] [t ::: Type] [r ::: {Type}] (m : mem nm t r) (r : $r) = m [t] (fn [r' :: {Type}] [[nm] ~ r'] (m' : mem' nm t r r') => @@ -34,5 +34,5 @@ (i : tf []) (fl : folder r) = @@Incl.fold [tf] [r] (fn [nm :: Name] [v :: K] [r' :: {K}] [[nm] ~ r'] (i : Incl.incl ([nm = v] ++ r') r) acc => - f [nm] [v] [r'] ! (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) + f [nm] [v] [r'] (Incl.inv1 [nm] [v] [r'] [r] [mem] i mem) acc) i fl
--- a/sql.ur Mon Mar 21 10:16:12 2011 -0400 +++ b/sql.ur Tue Jun 14 08:55:15 2011 -0400 @@ -10,7 +10,7 @@ (inj : sql_injectable t) (v : t) (exp : rest :: {Type} -> [rest ~ key] => sql_exp [tn = key ++ rest] [] [] bool) [rest :: {Type}] [rest ~ [nm = t] ++ key] => - (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest] !})) + (WHERE {{tn}}.{nm} = {@sql_inject inj v} AND {exp [[nm = t] ++ rest]})) (fn [rest :: {Type}] [rest ~ []] => (WHERE TRUE)) fl m r [_] ! @@ -22,6 +22,6 @@ (exp : rest1 :: {Type} -> rest2 :: {Type} -> [rest1 ~ key] => [rest2 ~ key] => sql_exp [tn1 = key ++ rest1, tn2 = key ++ rest2] [] [] bool) [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ [nm = t] ++ key] [rest2 ~ [nm = t] ++ key] => - (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2] ! !})) + (WHERE {{tn1}}.{nm} = {{tn2}}.{nm} AND {exp [[nm = t] ++ rest1] [[nm = t] ++ rest2]})) (fn [rest1 :: {Type}] [rest2 :: {Type}] [rest1 ~ []] [rest2 ~ []] => (WHERE TRUE)) fl [_] [_] ! !
--- 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)