diff lib/ur/monad.ur @ 1093:8d3aa6c7cee0

Make summary unification more conservative; infer implicit arguments after applications
author Adam Chlipala <adamc@hcoop.net>
date Sat, 26 Dec 2009 11:56:40 -0500
parents 37dd42935dad
children ad15700272f6
line wrap: on
line diff
--- a/lib/ur/monad.ur	Fri Dec 25 10:48:02 2009 -0500
+++ b/lib/ur/monad.ur	Sat Dec 26 11:56:40 2009 -0500
@@ -1,10 +1,10 @@
 fun exec [m ::: Type -> Type] (_ : monad m) [ts ::: {Type}] r (fd : folder ts) =
-    foldR [m] [fn ts => m $ts]
-    (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
-        this <- action;
-        others <- acc;
-        return ({nm = this} ++ others))
-    (return {}) [ts] fd r
+    @foldR [m] [fn ts => m $ts]
+     (fn [nm :: Name] [v :: Type] [rest :: {Type}] [[nm] ~ rest] action acc =>
+         this <- action;
+         others <- acc;
+         return ({nm = this} ++ others))
+     (return {}) fd r
 
 fun ignore [m ::: Type -> Type] (_ : monad m) [t] (v : m t) = x <- v; return ()
 
@@ -16,40 +16,40 @@
           (f : nm :: Name -> t :: K -> rest :: {K}
                -> [[nm] ~ rest] =>
            tf t -> tr rest -> m (tr ([nm = t] ++ rest)))
-          (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
-             (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                              (acc : _ -> m (tr rest)) r =>
-                 acc' <- acc (r -- nm);
-                 f [nm] [t] [rest] ! r.nm acc')
-             (fn _ => return i)
-             [_] fl
+          (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> m (tr rest)) r =>
+         acc' <- acc (r -- nm);
+         f [nm] [t] [rest] ! r.nm acc')
+     (fn _ => return i)
+     fl
 
 fun foldR2 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type]
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
             tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-           (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
-       (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                        (acc : _ -> _ -> m (tr rest)) r1 r2 =>
-           acc' <- acc (r1 -- nm) (r2 -- nm);
-           f [nm] [t] [rest] ! r1.nm r2.nm acc')
-       (fn _ _ => return i)
-       [_] fl
+           (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> _ -> m (tr rest)) r1 r2 =>
+         acc' <- acc (r1 -- nm) (r2 -- nm);
+         f [nm] [t] [rest] ! r1.nm r2.nm acc')
+     (fn _ _ => return i)
+     fl
 
 fun foldR3 [K] [m] (_ : monad m) [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type]
            (f : nm :: Name -> t :: K -> rest :: {K}
                 -> [[nm] ~ rest] =>
             tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest)))
-           (i : tr []) [r :: {K}] (fl : folder r) =
-    Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
-       (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
-                        (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
-           acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
-           f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
-       (fn _ _ _ => return i)
-       [_] fl
+           (i : tr []) [r ::: {K}] (fl : folder r) =
+    @Top.fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r)]
+     (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] 
+                      (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 =>
+         acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm);
+         f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc')
+     (fn _ _ _ => return i)
+     fl
 
 fun mapR [K] [m] (_ : monad m) [tf :: K -> Type] [tr :: K -> Type]
          (f : nm :: Name -> t :: K -> tf t -> m (tr t)) =