diff demo/more/versioned.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 166ea3944b91
children e2611b5dafce
line wrap: on
line diff
--- a/demo/more/versioned.ur	Fri Dec 25 10:48:02 2009 -0500
+++ b/demo/more/versioned.ur	Sat Dec 26 11:56:40 2009 -0500
@@ -24,33 +24,33 @@
                          Eq : eq t}
 
     fun keyRecd (r : $(M.key ++ M.data)) =
-        map2 [sql_injectable] [id] [sql_exp [] [] []]
-             (fn [t] => @sql_inject)
-             [_] M.keyFolder M.key (r --- M.data)
+        @map2 [sql_injectable] [id] [sql_exp [] [] []]
+         (fn [t] => @sql_inject)
+         M.keyFolder M.key (r --- M.data)
 
     fun insert r =
         vr <- nextval s;
         dml (Basis.insert t
                           ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
                                ++ keyRecd r
-                               ++ map2 [dmeta] [id]
+                               ++ @map2 [dmeta] [id]
                                [fn t => sql_exp [] [] [] (option t)]
                                (fn [t] x v => @sql_inject (@sql_option_prim x.Inj)
                                                (Some v))
-                               [_] M.dataFolder M.data (r --- M.key)))
+                               M.dataFolder M.data (r --- M.key)))
 
     fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool =
-        foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after]
-                                         => sql_exp [T = before ++ after] [] [] bool]
-               (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
-                                (inj : sql_injectable t) (v : t)
-                   (e : after :: {Type} -> [before ~ after]
-                    => sql_exp [T = before ++ after] [] [] bool)
-                   [after :: {Type}] [[nm = t] ++ before ~ after] =>
-                   (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
-               (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
-               [_] M.keyFolder M.key r
-               [_] !
+        @foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after]
+                                          => sql_exp [T = before ++ after] [] [] bool]
+         (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
+                          (inj : sql_injectable t) (v : t)
+                          (e : after :: {Type} -> [before ~ after]
+                           => sql_exp [T = before ++ after] [] [] bool)
+                          [after :: {Type}] [[nm = t] ++ before ~ after] =>
+             (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
+         (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
+         M.keyFolder M.key r
+         [_] !
 
     datatype bound =
              NoBound
@@ -61,13 +61,13 @@
         let
             fun current' vro r =
                 let
-                    val complete = foldR [option] [fn ts => option $ts]
-                                   (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
-                                                    v r =>
-                                       case (v, r) of
-                                           (Some v, Some r) => Some ({nm = v} ++ r)
-                                         | _ => None)
-                                   (Some {}) [_] M.dataFolder r
+                    val complete = @foldR [option] [fn ts => option $ts]
+                                    (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
+                                                     v r =>
+                                        case (v, r) of
+                                            (Some v, Some r) => Some ({nm = v} ++ r)
+                                          | _ => None)
+                                    (Some {}) M.dataFolder r
                 in
                     case complete of
                         Some r => return (Some r)
@@ -88,19 +88,19 @@
                                 None => return None
                               | Some r' =>
                                 let
-                                    val r = map2 [option] [option] [option]
-                                            (fn [t ::: Type] old new =>
-                                                case old of
-                                                    None => new
-                                                  | Some _ => old)
-                                            [_] M.dataFolder r (r'.T -- #Version)
+                                    val r = @map2 [option] [option] [option]
+                                             (fn [t ::: Type] old new =>
+                                                 case old of
+                                                     None => new
+                                                   | Some _ => old)
+                                             M.dataFolder r (r'.T -- #Version)
                                 in
                                     current' (Lt r'.T.Version) r
                                 end
                         end
                 end
         in
-            current' vro (map0 [option] (fn [t :: Type] => None : option t) [_] M.dataFolder)
+            current' vro (@map0 [option] (fn [t :: Type] => None : option t) M.dataFolder)
         end
 
     val current = seek NoBound
@@ -113,14 +113,14 @@
           | Some cur =>
             vr <- nextval s;
             let
-                val r' = map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)]
-                              (fn [t] (meta : dmeta t) old new =>
-                                  @sql_inject (@sql_option_prim meta.Inj)
-                                   (if @@eq [_] meta.Eq old new then
-                                        None
-                                    else
-                                        Some new))
-                              [_] M.dataFolder M.data cur (r --- M.key)
+                val r' = @map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)]
+                          (fn [t] (meta : dmeta t) old new =>
+                              @sql_inject (@sql_option_prim meta.Inj)
+                               (if @@eq [_] meta.Eq old new then
+                                    None
+                                else
+                                    Some new))
+                          M.dataFolder M.data cur (r --- M.key)
                 val r' = {Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
                              ++ keyRecd r
                              ++ r'