Mercurial > urweb
comparison lib/basis.lig @ 234:82409ef72019
SELECTed expressions in ORDER BY
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 28 Aug 2008 11:49:38 -0400 |
parents | c466678af854 |
children | 0608a0cfd32a |
comparison
equal
deleted
inserted
replaced
233:c466678af854 | 234:82409ef72019 |
---|---|
13 | 13 |
14 (*** Queries *) | 14 (*** Queries *) |
15 | 15 |
16 con sql_query :: {{Type}} -> {Type} -> Type | 16 con sql_query :: {{Type}} -> {Type} -> Type |
17 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type | 17 con sql_query1 :: {{Type}} -> {{Type}} -> {Type} -> Type |
18 con sql_exp :: {{Type}} -> {{Type}} -> Type -> Type | 18 con sql_exp :: {{Type}} -> {{Type}} -> {Type} -> Type -> Type |
19 | 19 |
20 con sql_subset :: {{Type}} -> {{Type}} -> Type | 20 con sql_subset :: {{Type}} -> {{Type}} -> Type |
21 val sql_subset : keep_drop :: {({Type} * {Type})} | 21 val sql_subset : keep_drop :: {({Type} * {Type})} |
22 -> sql_subset | 22 -> sql_subset |
23 (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => | 23 (fold (fn nm => fn fields :: ({Type} * {Type}) => fn acc => |
33 -> grouped ::: {{Type}} | 33 -> grouped ::: {{Type}} |
34 -> selectedFields ::: {{Type}} | 34 -> selectedFields ::: {{Type}} |
35 -> selectedExps ::: {Type} | 35 -> selectedExps ::: {Type} |
36 -> {From : $(fold (fn nm => fn fields :: {Type} => fn acc => | 36 -> {From : $(fold (fn nm => fn fields :: {Type} => fn acc => |
37 [nm] ~ acc => [nm = sql_table fields] ++ acc) [] tables), | 37 [nm] ~ acc => [nm = sql_table fields] ++ acc) [] tables), |
38 Where : sql_exp tables [] bool, | 38 Where : sql_exp tables [] [] bool, |
39 GroupBy : sql_subset tables grouped, | 39 GroupBy : sql_subset tables grouped, |
40 Having : sql_exp grouped tables bool, | 40 Having : sql_exp grouped tables [] bool, |
41 SelectFields : sql_subset grouped selectedFields, | 41 SelectFields : sql_subset grouped selectedFields, |
42 SelectExps : $(fold (fn nm => fn t :: Type => fn acc => | 42 SelectExps : $(fold (fn nm => fn t :: Type => fn acc => |
43 [nm] ~ acc => [nm = sql_exp grouped tables t] ++ acc) [] selectedExps) } | 43 [nm] ~ acc => [nm = sql_exp grouped tables [] t] ++ acc) [] selectedExps) } |
44 -> sql_query1 tables selectedFields selectedExps | 44 -> sql_query1 tables selectedFields selectedExps |
45 | 45 |
46 type sql_relop | 46 type sql_relop |
47 val sql_union : sql_relop | 47 val sql_union : sql_relop |
48 val sql_intersect : sql_relop | 48 val sql_intersect : sql_relop |
58 | 58 |
59 type sql_direction | 59 type sql_direction |
60 val sql_asc : sql_direction | 60 val sql_asc : sql_direction |
61 val sql_desc : sql_direction | 61 val sql_desc : sql_direction |
62 | 62 |
63 con sql_order_by :: {{Type}} -> Type | 63 con sql_order_by :: {{Type}} -> {Type} -> Type |
64 val sql_order_by_Nil : tables :: {{Type}} -> sql_order_by tables | 64 val sql_order_by_Nil : tables ::: {{Type}} -> exps :: {Type} -> sql_order_by tables exps |
65 val sql_order_by_Cons : tables ::: {{Type}} -> t ::: Type | 65 val sql_order_by_Cons : tables ::: {{Type}} -> exps ::: {Type} -> t ::: Type |
66 -> sql_exp tables [] t -> sql_order_by tables | 66 -> sql_exp tables [] exps t -> sql_order_by tables exps |
67 -> sql_order_by tables | 67 -> sql_order_by tables exps |
68 | 68 |
69 type sql_limit | 69 type sql_limit |
70 val sql_no_limit : sql_limit | 70 val sql_no_limit : sql_limit |
71 val sql_limit : int -> sql_limit | 71 val sql_limit : int -> sql_limit |
72 | 72 |
76 | 76 |
77 val sql_query : tables ::: {{Type}} | 77 val sql_query : tables ::: {{Type}} |
78 -> selectedFields ::: {{Type}} | 78 -> selectedFields ::: {{Type}} |
79 -> selectedExps ::: {Type} | 79 -> selectedExps ::: {Type} |
80 -> {Rows : sql_query1 tables selectedFields selectedExps, | 80 -> {Rows : sql_query1 tables selectedFields selectedExps, |
81 OrderBy : sql_order_by tables, | 81 OrderBy : sql_order_by tables selectedExps, |
82 Limit : sql_limit, | 82 Limit : sql_limit, |
83 Offset : sql_offset} | 83 Offset : sql_offset} |
84 -> sql_query selectedFields selectedExps | 84 -> sql_query selectedFields selectedExps |
85 | 85 |
86 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}} | 86 val sql_field : otherTabs ::: {{Type}} -> otherFields ::: {Type} -> fieldType ::: Type -> agg ::: {{Type}} |
87 -> exps ::: {Type} | |
87 -> tab :: Name -> field :: Name | 88 -> tab :: Name -> field :: Name |
88 -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg fieldType | 89 -> sql_exp ([tab = [field = fieldType] ++ otherFields] ++ otherTabs) agg exps fieldType |
90 | |
91 val sql_exp : tabs ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> rest ::: {Type} -> nm :: Name | |
92 -> sql_exp tabs agg ([nm = t] ++ rest) t | |
89 | 93 |
90 class sql_injectable | 94 class sql_injectable |
91 val sql_bool : sql_injectable bool | 95 val sql_bool : sql_injectable bool |
92 val sql_int : sql_injectable int | 96 val sql_int : sql_injectable int |
93 val sql_float : sql_injectable float | 97 val sql_float : sql_injectable float |
94 val sql_string : sql_injectable string | 98 val sql_string : sql_injectable string |
95 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> t -> sql_injectable t -> sql_exp tables agg t | 99 val sql_inject : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> t ::: Type |
100 -> sql_injectable t -> t -> sql_exp tables agg exps t | |
96 | 101 |
97 con sql_unary :: Type -> Type -> Type | 102 con sql_unary :: Type -> Type -> Type |
98 val sql_not : sql_unary bool bool | 103 val sql_not : sql_unary bool bool |
99 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> arg ::: Type -> res ::: Type | 104 val sql_unary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} -> arg ::: Type -> res ::: Type |
100 -> sql_unary arg res -> sql_exp tables agg arg -> sql_exp tables agg res | 105 -> sql_unary arg res -> sql_exp tables agg exps arg -> sql_exp tables agg exps res |
101 | 106 |
102 con sql_binary :: Type -> Type -> Type -> Type | 107 con sql_binary :: Type -> Type -> Type -> Type |
103 val sql_and : sql_binary bool bool bool | 108 val sql_and : sql_binary bool bool bool |
104 val sql_or : sql_binary bool bool bool | 109 val sql_or : sql_binary bool bool bool |
105 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type | 110 val sql_binary : tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} |
106 -> sql_binary arg1 arg2 res -> sql_exp tables agg arg1 -> sql_exp tables agg arg2 -> sql_exp tables agg res | 111 -> arg1 ::: Type -> arg2 ::: Type -> res ::: Type |
112 -> sql_binary arg1 arg2 res -> sql_exp tables agg exps arg1 -> sql_exp tables agg exps arg2 | |
113 -> sql_exp tables agg exps res | |
107 | 114 |
108 type sql_comparison | 115 type sql_comparison |
109 val sql_eq : sql_comparison | 116 val sql_eq : sql_comparison |
110 val sql_ne : sql_comparison | 117 val sql_ne : sql_comparison |
111 val sql_lt : sql_comparison | 118 val sql_lt : sql_comparison |
112 val sql_le : sql_comparison | 119 val sql_le : sql_comparison |
113 val sql_gt : sql_comparison | 120 val sql_gt : sql_comparison |
114 val sql_ge : sql_comparison | 121 val sql_ge : sql_comparison |
115 val sql_comparison : sql_comparison | 122 val sql_comparison : sql_comparison |
116 -> tables ::: {{Type}} -> agg ::: {{Type}} -> t ::: Type -> sql_exp tables agg t -> sql_exp tables agg t | 123 -> tables ::: {{Type}} -> agg ::: {{Type}} -> exps ::: {Type} |
117 -> sql_injectable t -> sql_exp tables agg bool | 124 -> t ::: Type -> sql_injectable t |
125 -> sql_exp tables agg exps t -> sql_exp tables agg exps t | |
126 -> sql_exp tables agg exps bool | |
118 | 127 |
119 (** XML *) | 128 (** XML *) |
120 | 129 |
121 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type | 130 con tag :: {Type} -> {Unit} -> {Unit} -> {Type} -> {Type} -> Type |
122 | 131 |