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)