-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathQcert.Compiler.Enhanced.EnhancedToJava.html
More file actions
65 lines (61 loc) · 9.39 KB
/
Qcert.Compiler.Enhanced.EnhancedToJava.html
File metadata and controls
65 lines (61 loc) · 9.39 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
<!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.Enhanced.EnhancedToJava</title>
<meta name="description" content="Documentation of Coq module Qcert.Compiler.Enhanced.EnhancedToJava" />
<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.Enhanced.EnhancedToJava</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</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="kwd">Import</span> <span class="id"><a href="Qcert.Utils.Utils.html">Utils</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Data.DataSystem.html">DataSystem</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Java.JavaSystem.html">JavaSystem</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Operators.ForeignToJava.html">ForeignToJava</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Compiler.Component.SqlDateComponent.html">SqlDateComponent</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Compiler.Component.UriComponent.html">UriComponent</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html">EnhancedData</a></span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="enhanced_to_java_data">enhanced_to_java_data</a></span><br/>
(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">fd</span>:<span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_data">enhanced_data</a></span>) : <span class="id"><a href="Qcert.Java.Lang.Java.html#java_json">java_json</a></span><br/>
:= <span class="kwd">match</span> <span class="id">fd</span> <span class="kwd">with</span><br/>
| <span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhancedsqldate">enhancedsqldate</a></span> <span class="id">tp</span> => <span class="id"><a href="Qcert.Java.Lang.Java.html#mk_java_json">mk_java_json</a></span> (@<span class="id"><a href="Qcert.Utils.CoqLibAdd.html#toString">toString</a></span> <span class="id">_</span> <span class="id"><a href="Qcert.Compiler.Component.SqlDateComponent.html#sql_date_foreign_data">sql_date_foreign_data</a></span>.(@<span class="id"><a href="Qcert.Data.Model.ForeignData.html#foreign_data_tostring">foreign_data_tostring</a></span>) <span class="id">tp</span>)<br/>
| <span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhancedsqldateperiod">enhancedsqldateperiod</a></span> <span class="id">tp</span> => <span class="id"><a href="Qcert.Java.Lang.Java.html#mk_java_json">mk_java_json</a></span> (@<span class="id"><a href="Qcert.Utils.CoqLibAdd.html#toString">toString</a></span> <span class="id">_</span> <span class="id"><a href="Qcert.Compiler.Component.SqlDateComponent.html#sql_date_period_foreign_data">sql_date_period_foreign_data</a></span>.(@<span class="id"><a href="Qcert.Data.Model.ForeignData.html#foreign_data_tostring">foreign_data_tostring</a></span> ) <span class="id">tp</span>)<br/>
<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="enhanced_to_java_unary_op">enhanced_to_java_unary_op</a></span><br/>
(<span class="id">indent</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>) (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">fu</span>:<span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_unary_op">enhanced_unary_op</a></span>)<br/>
(<span class="id">d</span>:<span class="id"><a href="Qcert.Java.Lang.Java.html#java_json">java_json</a></span>) : <span class="id"><a href="Qcert.Java.Lang.Java.html#java_json">java_json</a></span><br/>
:= <span class="kwd">match</span> <span class="id">fu</span> <span class="kwd">with</span><br/>
| <span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_unary_sql_date_op">enhanced_unary_sql_date_op</a></span> <span class="id">op</span> =><br/>
<span class="id"><a href="Qcert.Compiler.Component.SqlDateComponent.html#sql_date_to_java_unary_op">sql_date_to_java_unary_op</a></span> <span class="id">indent</span> <span class="id">eol</span> <span class="id">quotel</span> <span class="id">op</span> <span class="id">d</span><br/>
| <span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_unary_uri_op">enhanced_unary_uri_op</a></span> <span class="id">op</span> =><br/>
<span class="id"><a href="Qcert.Compiler.Component.UriComponent.html#uri_to_java_unary_op">uri_to_java_unary_op</a></span> <span class="id">indent</span> <span class="id">eol</span> <span class="id">quotel</span> <span class="id">op</span> <span class="id">d</span><br/>
<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Definition</span> <span class="id"><a name="enhanced_to_java_binary_op">enhanced_to_java_binary_op</a></span><br/>
(<span class="id">indent</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nat">nat</a></span>) (<span class="id">eol</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
(<span class="id">quotel</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) (<span class="id">fb</span>:<span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_binary_op">enhanced_binary_op</a></span>)<br/>
(<span class="id">d1</span> <span class="id">d2</span>:<span class="id"><a href="Qcert.Java.Lang.Java.html#java_json">java_json</a></span>) : <span class="id"><a href="Qcert.Java.Lang.Java.html#java_json">java_json</a></span><br/>
:= <span class="kwd">match</span> <span class="id">fb</span> <span class="kwd">with</span><br/>
| <span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_binary_sql_date_op">enhanced_binary_sql_date_op</a></span> <span class="id">op</span> =><br/>
<span class="id"><a href="Qcert.Compiler.Component.SqlDateComponent.html#sql_date_to_java_binary_op">sql_date_to_java_binary_op</a></span> <span class="id">indent</span> <span class="id">eol</span> <span class="id">quotel</span> <span class="id">op</span> <span class="id">d1</span> <span class="id">d2</span><br/>
<span class="kwd">end</span>.<br/>
<br/>
<span class="kwd">Global</span> <span class="kwd">Instance</span> <span class="id"><a name="enhanced_foreign_to_java">enhanced_foreign_to_java</a></span> :<br/>
@<span class="id"><a href="Qcert.Translation.Operators.ForeignToJava.html#foreign_to_java">foreign_to_java</a></span> <span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_foreign_runtime">enhanced_foreign_runtime</a></span><br/>
:= <span class="id"><a href="Qcert.Translation.Operators.ForeignToJava.html#mk_foreign_to_java">mk_foreign_to_java</a></span><br/>
<span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedData.html#enhanced_foreign_runtime">enhanced_foreign_runtime</a></span><br/>
<span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedToJava.html#enhanced_to_java_data">enhanced_to_java_data</a></span><br/>
<span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedToJava.html#enhanced_to_java_unary_op">enhanced_to_java_unary_op</a></span><br/>
<span class="id"><a href="Qcert.Compiler.Enhanced.EnhancedToJava.html#enhanced_to_java_binary_op">enhanced_to_java_binary_op</a></span>.<br/>
<br/>
</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>