Mercurial > urweb

comparison demo/more/versioned.ur @ 995:166ea3944b91

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