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