Mercurial > urweb

annotate demo/more/versioned.ur @ 1249:7c6fc92f6c31

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Complain about DValRec; optimizations for unit-valued ECase and forgetting of path conditions across ESeq
author Adam Chlipala <adamc@hcoop.net>
date Thu, 29 Apr 2010 11:47:24 -0400
parents 8d3aa6c7cee0
children e2611b5dafce
rev   line source
adamc@993 1 functor Make(M : sig
adamc@993 2 con key :: {Type}
adamc@993 3 con data :: {Type}
adamc@993 4 constraint key ~ data
adamc@995 5 constraint [When, Version] ~ (key ++ data)
adamc@993 6
adamc@993 7 val key : $(map sql_injectable key)
adamc@993 8 val data : $(map (fn t => {Inj : sql_injectable_prim t,
adamc@993 9 Eq : eq t}) data)
adamc@993 10
adamc@993 11 val keyFolder : folder key
adamc@993 12 val dataFolder : folder data
adamc@993 13 end) = struct
adamc@995 14 type version = int
adamc@995 15 con all = [When = time, Version = version] ++ M.key ++ map option M.data
adamc@995 16 sequence s
adamc@993 17 table t : all
adamc@993 18
adamc@993 19 val keys = List.mapQuery (SELECT DISTINCT t.{{M.key}} FROM t) (fn r => r.T)
adamc@995 20 fun keysAt vr = List.mapQuery (SELECT DISTINCT t.{{M.key}} FROM t
adamc@995 21 WHERE t.Version <= {[vr]}) (fn r => r.T)
adamc@993 22
adamc@993 23 con dmeta = fn t => {Inj : sql_injectable_prim t,
adamc@993 24 Eq : eq t}
adamc@993 25
adamc@993 26 fun keyRecd (r : $(M.key ++ M.data)) =
adamc@1093 27 @map2 [sql_injectable] [id] [sql_exp [] [] []]
adamc@1093 28 (fn [t] => @sql_inject)
adamc@1093 29 M.keyFolder M.key (r --- M.data)
adamc@993 30
adamc@995 31 fun insert r =
adamc@995 32 vr <- nextval s;
adamc@995 33 dml (Basis.insert t
adamc@995 34 ({Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
adamc@995 35 ++ keyRecd r
adamc@1093 36 ++ @map2 [dmeta] [id]
adamc@995 37 [fn t => sql_exp [] [] [] (option t)]
adamc@995 38 (fn [t] x v => @sql_inject (@sql_option_prim x.Inj)
adamc@995 39 (Some v))
adamc@1093 40 M.dataFolder M.data (r --- M.key)))
adamc@993 41
adamc@993 42 fun keyExp (r : $M.key) : sql_exp [T = all] [] [] bool =
adamc@1093 43 @foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after]
adamc@1093 44 => sql_exp [T = before ++ after] [] [] bool]
adamc@1093 45 (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
adamc@1093 46 (inj : sql_injectable t) (v : t)
adamc@1093 47 (e : after :: {Type} -> [before ~ after]
adamc@1093 48 => sql_exp [T = before ++ after] [] [] bool)
adamc@1093 49 [after :: {Type}] [[nm = t] ++ before ~ after] =>
adamc@1093 50 (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
adamc@1093 51 (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
adamc@1093 52 M.keyFolder M.key r
adamc@1093 53 [_] !
adamc@993 54
adamc@995 55 datatype bound =
adamc@995 56 NoBound
adamc@995 57 | Lt of int
adamc@995 58 | Le of int
adamc@995 59
adamc@995 60 fun seek vro k =
adamc@993 61 let
adamc@995 62 fun current' vro r =
adamc@993 63 let
adamc@1093 64 val complete = @foldR [option] [fn ts => option $ts]
adamc@1093 65 (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
adamc@1093 66 v r =>
adamc@1093 67 case (v, r) of
adamc@1093 68 (Some v, Some r) => Some ({nm = v} ++ r)
adamc@1093 69 | _ => None)
adamc@1093 70 (Some {}) M.dataFolder r
adamc@993 71 in
adamc@993 72 case complete of
adamc@993 73 Some r => return (Some r)
adamc@993 74 | None =>
adamc@993 75 let
adamc@995 76 val filter = case vro of
adamc@995 77 NoBound => (WHERE TRUE)
adamc@995 78 | Lt vr => (WHERE t.Version < {[vr]})
adamc@995 79 | Le vr => (WHERE t.Version <= {[vr]})
adamc@993 80 in
adamc@995 81 ro <- oneOrNoRows (SELECT t.Version, t.{{map option M.data}}
adamc@993 82 FROM t
adamc@993 83 WHERE {filter}
adamc@993 84 AND {keyExp k}
adamc@993 85 ORDER BY t.When DESC
adamc@993 86 LIMIT 1);
adamc@993 87 case ro of
adamc@993 88 None => return None
adamc@993 89 | Some r' =>
adamc@993 90 let
adamc@1093 91 val r = @map2 [option] [option] [option]
adamc@1093 92 (fn [t ::: Type] old new =>
adamc@1093 93 case old of
adamc@1093 94 None => new
adamc@1093 95 | Some _ => old)
adamc@1093 96 M.dataFolder r (r'.T -- #Version)
adamc@993 97 in
adamc@995 98 current' (Lt r'.T.Version) r
adamc@993 99 end
adamc@993 100 end
adamc@993 101 end
adamc@993 102 in
adamc@1093 103 current' vro (@map0 [option] (fn [t :: Type] => None : option t) M.dataFolder)
adamc@993 104 end
adamc@993 105
adamc@995 106 val current = seek NoBound
adamc@995 107 fun archive vr = seek (Le vr)
adamc@995 108
adamc@993 109 fun update r =
adamc@993 110 cur <- current (r --- M.data);
adamc@993 111 case cur of
adamc@993 112 None => error <xml>Tried to update nonexistent key</xml>
adamc@993 113 | Some cur =>
adamc@995 114 vr <- nextval s;
adamc@993 115 let
adamc@1093 116 val r' = @map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)]
adamc@1093 117 (fn [t] (meta : dmeta t) old new =>
adamc@1093 118 @sql_inject (@sql_option_prim meta.Inj)
adamc@1093 119 (if @@eq [_] meta.Eq old new then
adamc@1093 120 None
adamc@1093 121 else
adamc@1093 122 Some new))
adamc@1093 123 M.dataFolder M.data cur (r --- M.key)
adamc@995 124 val r' = {Version = (SQL {[vr]}), When = (SQL CURRENT_TIMESTAMP)}
adamc@993 125 ++ keyRecd r
adamc@993 126 ++ r'
adamc@993 127 in
adamc@993 128 dml (Basis.insert t r')
adamc@993 129 end
adamc@995 130
adamc@995 131 val updateTimes = List.mapQuery (SELECT t.Version, t.When
adamc@995 132 FROM t
adamc@995 133 ORDER BY t.When) (fn r => (r.T.Version, r.T.When))
adamc@993 134 end