Mercurial > urweb

annotate demo/more/versioned.ur @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents 166ea3944b91
children 8d3aa6c7cee0
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@993 27 map2 [sql_injectable] [id] [sql_exp [] [] []]
adamc@993 28 (fn [t] => @sql_inject)
adamc@993 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@995 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@995 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@993 43 foldR2 [sql_injectable] [id] [fn before => after :: {Type} -> [before ~ after]
adamc@993 44 => sql_exp [T = before ++ after] [] [] bool]
adamc@993 45 (fn [nm :: Name] [t :: Type] [before :: {Type}] [[nm] ~ before]
adamc@993 46 (inj : sql_injectable t) (v : t)
adamc@993 47 (e : after :: {Type} -> [before ~ after]
adamc@993 48 => sql_exp [T = before ++ after] [] [] bool)
adamc@993 49 [after :: {Type}] [[nm = t] ++ before ~ after] =>
adamc@993 50 (SQL t.{nm} = {[v]} AND {e [[nm = t] ++ after] !}))
adamc@993 51 (fn [after :: {Type}] [[] ~ after] => (SQL TRUE))
adamc@993 52 [_] M.keyFolder M.key r
adamc@993 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@993 64 val complete = foldR [option] [fn ts => option $ts]
adamc@993 65 (fn [nm :: Name] [v :: Type] [r :: {Type}] [[nm] ~ r]
adamc@993 66 v r =>
adamc@993 67 case (v, r) of
adamc@993 68 (Some v, Some r) => Some ({nm = v} ++ r)
adamc@993 69 | _ => None)
adamc@993 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@993 91 val r = map2 [option] [option] [option]
adamc@993 92 (fn [t ::: Type] old new =>
adamc@993 93 case old of
adamc@993 94 None => new
adamc@993 95 | Some _ => old)
adamc@995 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@995 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@993 116 val r' = map3 [dmeta] [id] [id] [fn t => sql_exp [] [] [] (option t)]
adamc@993 117 (fn [t] (meta : dmeta t) old new =>
adamc@993 118 @sql_inject (@sql_option_prim meta.Inj)
adamc@993 119 (if @@eq [_] meta.Eq old new then
adamc@993 120 None
adamc@993 121 else
adamc@993 122 Some new))
adamc@993 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