# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1308056115 14400
# Node ID 744bf911dcc6501c8de2b3abd4adb5eee1fe8751
# Parent  d05943db55e89588d32561db89268ce717b03664
Update to expect implicit argument insertion for local variables

diff -r d05943db55e8 -r 744bf911dcc6 eq.ur
--- 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
diff -r d05943db55e8 -r 744bf911dcc6 incl.ur
--- 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] [[]])
diff -r d05943db55e8 -r 744bf911dcc6 mem.ur
--- 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
diff -r d05943db55e8 -r 744bf911dcc6 sql.ur
--- 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 [_] [_] ! !
diff -r d05943db55e8 -r 744bf911dcc6 variant.ur
--- 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)