Mercurial > urweb
annotate tests/pquery.ur @ 635:75c7a69354d6
Coq formalization uses TDisjoint
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 24 Feb 2009 16:08:14 -0500 |
| parents | 43f35291433d |
| children |
| rev | line source |
|---|---|
| adamc@296 | 1 table t1 : {A : int, B : string, C : float, D : bool} |
| adamc@280 | 2 |
| adamc@297 | 3 fun display (q : sql_query [T1 = [A = int, B = string, C = float, D = bool]] []) = |
| adamc@297 | 4 s <- query q |
| adamc@297 | 5 (fn fs _ => return (Some fs.T1)) |
| adamc@297 | 6 None; |
| adamc@280 | 7 return <html><body> |
| adamc@297 | 8 {case s of |
| adamc@297 | 9 None => cdata "Row not found." |
| adamc@297 | 10 | Some s => |
| adamc@297 | 11 <body> |
| adamc@297 | 12 A: {cdata (show _ s.A)}<br/> |
| adamc@297 | 13 B: {cdata (show _ s.B)}<br/> |
| adamc@297 | 14 C: {cdata (show _ s.C)}<br/> |
| adamc@297 | 15 D: {cdata (show _ s.D)}<br/> |
| adamc@297 | 16 </body>} |
| adamc@280 | 17 </body></html> |
| adamc@280 | 18 |
| adamc@297 | 19 fun lookupA (inp : {A : string}) = |
| adamc@298 | 20 display (SELECT * FROM t1 WHERE t1.A = {readError _ inp.A}) |
| adamc@297 | 21 |
| adamc@297 | 22 fun lookupB (inp : {B : string}) = |
| adamc@297 | 23 display (SELECT * FROM t1 WHERE t1.B = {inp.B}) |
| adamc@297 | 24 |
| adamc@297 | 25 fun lookupC (inp : {C : string}) = |
| adamc@298 | 26 display (SELECT * FROM t1 WHERE t1.C = {readError _ inp.C}) |
| adamc@297 | 27 |
| adamc@297 | 28 fun lookupD (inp : {D : string}) = |
| adamc@298 | 29 display (SELECT * FROM t1 WHERE t1.D = {readError _ inp.D}) |
| adamc@297 | 30 |
| adamc@280 | 31 fun main () : transaction page = return <html><body> |
| adamc@280 | 32 <lform> |
| adamc@297 | 33 A: <textbox{#A}/> |
| adamc@297 | 34 <submit action={lookupA}/> |
| adamc@297 | 35 </lform> |
| adamc@297 | 36 |
| adamc@297 | 37 <lform> |
| adamc@280 | 38 B: <textbox{#B}/> |
| adamc@297 | 39 <submit action={lookupB}/> |
| adamc@297 | 40 </lform> |
| adamc@297 | 41 |
| adamc@297 | 42 <lform> |
| adamc@297 | 43 C: <textbox{#C}/> |
| adamc@297 | 44 <submit action={lookupC}/> |
| adamc@297 | 45 </lform> |
| adamc@297 | 46 |
| adamc@297 | 47 <lform> |
| adamc@297 | 48 D: <textbox{#D}/> |
| adamc@297 | 49 <submit action={lookupD}/> |
| adamc@280 | 50 </lform> |
| adamc@280 | 51 </body></html> |