Mercurial > urweb
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'