-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathQcert.Compiler.Lib.QSQL.html
More file actions
94 lines (90 loc) · 18.6 KB
/
Qcert.Compiler.Lib.QSQL.html
File metadata and controls
94 lines (90 loc) · 18.6 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module Qcert.Compiler.Lib.QSQL</title>
<meta name="description" content="Documentation of Coq module Qcert.Compiler.Lib.QSQL" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>
<body onload="hideAll('proofscript')">
<h1 class="title">Module Qcert.Compiler.Lib.QSQL</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Compiler.Model.CompilerRuntime.html">CompilerRuntime</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="Qcert.Compiler.Lib.QData.html">QData</a></span> <span class="id"><a href="Qcert.Compiler.Lib.QOperators.html">QOperators</a></span>.<br/>
<span class="kwd">Require</span> <span class="id"><a href="Qcert.SQL.Lang.SQL.html">SQL</a></span>.<br/>
<br/>
<span class="kwd">Module</span> <span class="id"><a name="QSQL">QSQL</a></span>(<span class="id">runtime</span>:<span class="id"><a href="Qcert.Compiler.Model.CompilerRuntime.html#CompilerRuntime">CompilerRuntime</a></span>).<br/>
<br/>
<span class="kwd">Module</span> <span class="id"><a name="QSQL.QData">QData</a></span> := <span class="id"><a href="Qcert.Compiler.Lib.QData.html#QData">QData.QData</a></span> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#runtime">runtime</a></span>.<br/>
<span class="kwd">Module</span> <span class="id"><a name="QSQL.QOps">QOps</a></span> := <span class="id"><a href="Qcert.Compiler.Lib.QOperators.html#QOperators">QOperators.QOperators</a></span> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#runtime">runtime</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql">sql</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql">SQL.sql</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.t">t</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql">sql</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.column">column</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.table">table</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_table_spec">sql_table_spec</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_table_spec">SQL.sql_table_spec</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_bin_cond">sql_bin_cond</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_bin_cond">SQL.sql_bin_cond</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_un_expr">sql_un_expr</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_un_expr">SQL.sql_un_expr</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_bin_expr">sql_bin_expr</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_bin_expr">SQL.sql_bin_expr</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_agg">sql_agg</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_agg">SQL.sql_agg</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_statement">sql_statement</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_statement">SQL.sql_statement</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_query">sql_query</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_query">SQL.sql_query</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_select">sql_select</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_select">SQL.sql_select</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_from">sql_from</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_from">SQL.sql_from</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_condition">sql_condition</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_condition">SQL.sql_condition</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr">sql_expr</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#sql_expr">SQL.sql_expr</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_sql_query">sql_sql_query</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SQuery">SQL.SQuery</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_sql_union">sql_sql_union</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SUnion">SQL.SUnion</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_sql_intersect">sql_sql_intersect</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SIntersect">SQL.SIntersect</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_sql_except">sql_sql_except</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExcept">SQL.SExcept</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_select_column">sql_select_column</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.column">column</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_select">sql_select</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SSelectColumn">SQL.SSelectColumn</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_select_column_deref">sql_select_column_deref</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.table">table</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.column">column</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_select">sql_select</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SSelectColumnDeref">SQL.SSelectColumnDeref</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_select_expr">sql_select_expr</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.column">column</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_select">sql_select</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SSelectExpr">SQL.SSelectExpr</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_select_star">sql_select_star</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_select">sql_select</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SSelectStar">SQL.SSelectStar</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_condition_and">sql_condition_and</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondAnd">SQL.SCondAnd</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_condition_or">sql_condition_or</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondOr">SQL.SCondOr</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_condition_not">sql_condition_not</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondNot">SQL.SCondNot</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_from_table">sql_from_table</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.table">table</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_from">sql_from</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SFromTable">SQL.SFromTable</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_from_table_alias">sql_from_table_alias</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.table">table</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.table">table</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_from">sql_from</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SFromTableAlias">SQL.SFromTableAlias</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_from_query">sql_from_query</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_table_spec">sql_table_spec</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_query">sql_query</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_from">sql_from</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SFromQuery">SQL.SFromQuery</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_and">sql_cond_and</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondAnd">SQL.SCondAnd</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_or">sql_cond_or</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondOr">SQL.SCondOr</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_not">sql_cond_not</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondNot">SQL.SCondNot</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_binary">sql_cond_binary</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondBinary">SQL.SCondBinary</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_exists">sql_cond_exists</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondExists">SQL.SCondExists</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_in">sql_cond_in</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondIn">SQL.SCondIn</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_like">sql_cond_like</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondLike">SQL.SCondLike</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_cond_between">sql_cond_between</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCondBetween">SQL.SCondBetween</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_const">sql_expr_const</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.qdata">QData.qdata</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprConst">SQL.SExprConst</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_column">sql_expr_column</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprColumn">SQL.SExprColumn</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_column_deref">sql_expr_column_deref</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprColumnDeref">SQL.SExprColumnDeref</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_star">sql_expr_star</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprStar">SQL.SExprStar</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_unary">sql_expr_unary</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_un_expr">sql_un_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprUnary">SQL.SExprUnary</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_binary">sql_expr_binary</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_bin_expr">sql_bin_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprBinary">SQL.SExprBinary</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_case">sql_expr_case</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_condition">sql_condition</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprCase">SQL.SExprCase</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_agg_expr">sql_expr_agg_expr</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_agg">sql_agg</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprAggExpr">SQL.SExprAggExpr</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_expr_query">sql_expr_query</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_query">sql_query</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_expr">sql_expr</a></span> := <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SExprQuery">SQL.SExprQuery</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_run_query">sql_run_query</a></span> : <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_query">sql_query</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_statement">sql_statement</a></span><br/>
:= <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SRunQuery">SQL.SRunQuery</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_create_view">sql_create_view</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_query">sql_query</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_statement">sql_statement</a></span><br/>
:= <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SCreateView">SQL.SCreateView</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="QSQL.sql_drop_view">sql_drop_view</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">String.string</a></span> -> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL.sql_statement">sql_statement</a></span><br/>
:= <span class="id"><a href="Qcert.SQL.Lang.SQL.html#SDropView">SQL.SDropView</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="Qcert.Compiler.Lib.QSQL.html#QSQL">QSQL</a></span>.<br/>
<br/>
</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>