-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathQcert.Compiler.Model.CompilerModel.html
More file actions
118 lines (114 loc) · 24.9 KB
/
Qcert.Compiler.Model.CompilerModel.html
File metadata and controls
118 lines (114 loc) · 24.9 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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
<!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.Model.CompilerModel</title>
<meta name="description" content="Documentation of Coq module Qcert.Compiler.Model.CompilerModel" />
<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.Model.CompilerModel</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.Compiler.Model.CompilerRuntime.html">CompilerRuntime</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.EJson.Model.ForeignEJson.html">ForeignEJson</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Model.ForeignDataToEJson.html">ForeignDataToEJson</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Operators.ForeignToEJsonRuntime.html">ForeignToEJsonRuntime</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Model.ForeignEJsonToJSON.html">ForeignEJsonToJSON</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Model.ForeignTypeToJSON.html">ForeignTypeToJSON</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.NNRCMR.Lang.ForeignReduceOps.html">ForeignReduceOps</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Operators.ForeignToReduceOps.html">ForeignToReduceOps</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.Translation.Operators.ForeignToJavaScriptAst.html">ForeignToJavaScriptAst</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Operators.ForeignToScala.html">ForeignToScala</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Translation.Operators.ForeignToSpark.html">ForeignToSpark</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Utils.OptimizerLogger.html">OptimizerLogger</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.TypeSystem.ForeignType.html">ForeignType</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.Data.ModelTyping.ForeignDataTyping.html">ForeignDataTyping</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.cNNRC.Lang.cNNRC.html">cNNRC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.cNRAEnv.Lang.cNRAEnv.html">cNRAEnv</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.NRAEnv.Lang.NRAEnv.html">NRAEnv</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.DNNRC.Lang.DNNRC.html">DNNRC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.tDNNRC.Lang.tDNNRC.html">tDNNRC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="Qcert.NNRSimp.Lang.NNRSimp.html">NNRSimp</a></span>.<br/>
<br/>
<span class="kwd">Module</span> <span class="kwd">Type</span> <span class="id"><a name="CompilerModel">CompilerModel</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_basic_model">compiler_basic_model</a></span> : <span class="id"><a href="Qcert.Data.DataSystem.html#basic_model">basic_model</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_runtime">compiler_model_foreign_runtime</a></span> : <span class="id"><a href="Qcert.Data.ForeignRuntime.html#foreign_runtime">foreign_runtime</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_ejson">compiler_model_foreign_ejson</a></span> : <span class="id"><a href="Qcert.EJson.Model.ForeignEJson.html#foreign_ejson">foreign_ejson</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_to_ejson">compiler_model_foreign_to_ejson</a></span> : <span class="id"><a href="Qcert.Translation.Model.ForeignDataToEJson.html#foreign_to_ejson">foreign_to_ejson</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_to_ejson_runtime">compiler_model_foreign_to_ejson_runtime</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToEJsonRuntime.html#foreign_to_ejson_runtime">foreign_to_ejson_runtime</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_to_json">compiler_model_foreign_to_json</a></span> : <span class="id"><a href="Qcert.Translation.Model.ForeignEJsonToJSON.html#foreign_to_json">foreign_to_json</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_to_java">compiler_model_foreign_to_java</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToJava.html#foreign_to_java">foreign_to_java</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_ejson_to_ajavascript">compiler_model_foreign_ejson_to_ajavascript</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToJavaScriptAst.html#foreign_ejson_to_ajavascript">foreign_ejson_to_ajavascript</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_to_scala">compiler_model_foreign_to_scala</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToScala.html#foreign_to_scala">foreign_to_scala</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_type_to_JSON">compiler_model_foreign_type_to_JSON</a></span> : <span class="id"><a href="Qcert.Translation.Model.ForeignTypeToJSON.html#foreign_type_to_JSON">foreign_type_to_JSON</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_reduce_op">compiler_model_foreign_reduce_op</a></span> : <span class="id"><a href="Qcert.NNRCMR.Lang.ForeignReduceOps.html#foreign_reduce_op">foreign_reduce_op</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_to_reduce_op">compiler_model_foreign_to_reduce_op</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToReduceOps.html#foreign_to_reduce_op">foreign_to_reduce_op</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_to_spark">compiler_model_foreign_to_spark</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToSpark.html#foreign_to_spark">foreign_to_spark</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_nraenv_optimizer_logger">compiler_model_nraenv_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NRAEnv.Lang.NRAEnv.html#nraenv">nraenv</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_nnrc_optimizer_logger">compiler_model_nnrc_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.cNNRC.Lang.cNNRC.html#nnrc">nnrc</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_nnrs_imp_expr_optimizer_logger">compiler_model_nnrs_imp_expr_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NNRSimp.Lang.NNRSimp.html#nnrs_imp_expr">nnrs_imp_expr</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_nnrs_imp_stmt_optimizer_logger">compiler_model_nnrs_imp_stmt_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NNRSimp.Lang.NNRSimp.html#nnrs_imp_stmt">nnrs_imp_stmt</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_nnrs_imp_optimizer_logger">compiler_model_nnrs_imp_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NNRSimp.Lang.NNRSimp.html#nnrs_imp">nnrs_imp</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_dnnrc_optimizer_logger">compiler_model_dnnrc_optimizer_logger</a></span> : <span class="kwd">forall</span> {<span class="id">br</span>:<span class="id"><a href="Qcert.Brands.BrandRelation.html#brand_relation">brand_relation</a></span>}, <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> (<span class="id"><a href="Qcert.tDNNRC.Lang.tDNNRC.html#dnnrc_typed">dnnrc_typed</a></span>).<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerModel.compiler_model_foreign_data_typing">compiler_model_foreign_data_typing</a></span> : <span class="id"><a href="Qcert.Data.ModelTyping.ForeignDataTyping.html#foreign_data_typing">foreign_data_typing</a></span>.<br/>
<span class="kwd">End</span> <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#CompilerModel">CompilerModel</a></span>.<br/>
<br/>
<span class="kwd">Module</span> <span class="id"><a name="CompilerModelRuntime">CompilerModelRuntime</a></span>(<span class="id">model</span>:<span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#CompilerModel">CompilerModel</a></span>) <: <span class="id"><a href="Qcert.Compiler.Model.CompilerRuntime.html#CompilerRuntime">CompilerRuntime</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_type">compiler_foreign_type</a></span> : <span class="id"><a href="Qcert.TypeSystem.ForeignType.html#foreign_type">foreign_type</a></span><br/>
:= <span class="id"><a href="Qcert.Data.DataSystem.html#basic_model_foreign_type">basic_model_foreign_type</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_runtime">compiler_foreign_runtime</a></span> : <span class="id"><a href="Qcert.Data.ForeignRuntime.html#foreign_runtime">foreign_runtime</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_runtime">model.compiler_model_foreign_runtime</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_ejson">compiler_foreign_ejson</a></span> : <span class="id"><a href="Qcert.EJson.Model.ForeignEJson.html#foreign_ejson">foreign_ejson</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_ejson">model.compiler_model_foreign_ejson</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_to_ejson">compiler_foreign_to_ejson</a></span> : <span class="id"><a href="Qcert.Translation.Model.ForeignDataToEJson.html#foreign_to_ejson">foreign_to_ejson</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_to_ejson">model.compiler_model_foreign_to_ejson</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_to_ejson_runtime">compiler_foreign_to_ejson_runtime</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToEJsonRuntime.html#foreign_to_ejson_runtime">foreign_to_ejson_runtime</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_to_ejson_runtime">model.compiler_model_foreign_to_ejson_runtime</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_to_json">compiler_foreign_to_json</a></span> : <span class="id"><a href="Qcert.Translation.Model.ForeignEJsonToJSON.html#foreign_to_json">foreign_to_json</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_to_json">model.compiler_model_foreign_to_json</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_to_java">compiler_foreign_to_java</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToJava.html#foreign_to_java">foreign_to_java</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_to_java">model.compiler_model_foreign_to_java</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_ejson_to_ajavascript">compiler_foreign_ejson_to_ajavascript</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToJavaScriptAst.html#foreign_ejson_to_ajavascript">foreign_ejson_to_ajavascript</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_ejson_to_ajavascript">model.compiler_model_foreign_ejson_to_ajavascript</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_to_scala">compiler_foreign_to_scala</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToScala.html#foreign_to_scala">foreign_to_scala</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_to_scala">model.compiler_model_foreign_to_scala</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_type_to_JSON">compiler_foreign_type_to_JSON</a></span> : <span class="id"><a href="Qcert.Translation.Model.ForeignTypeToJSON.html#foreign_type_to_JSON">foreign_type_to_JSON</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_type_to_JSON">model.compiler_model_foreign_type_to_JSON</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_reduce_op">compiler_foreign_reduce_op</a></span> : <span class="id"><a href="Qcert.NNRCMR.Lang.ForeignReduceOps.html#foreign_reduce_op">foreign_reduce_op</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_reduce_op">model.compiler_model_foreign_reduce_op</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_to_reduce_op">compiler_foreign_to_reduce_op</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToReduceOps.html#foreign_to_reduce_op">foreign_to_reduce_op</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_to_reduce_op">model.compiler_model_foreign_to_reduce_op</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_to_spark">compiler_foreign_to_spark</a></span> : <span class="id"><a href="Qcert.Translation.Operators.ForeignToSpark.html#foreign_to_spark">foreign_to_spark</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_to_spark">model.compiler_model_foreign_to_spark</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_nraenv_optimizer_logger">compiler_nraenv_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NRAEnv.Lang.NRAEnv.html#nraenv">nraenv</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_nraenv_optimizer_logger">model.compiler_model_nraenv_optimizer_logger</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_nnrc_optimizer_logger">compiler_nnrc_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.cNNRC.Lang.cNNRC.html#nnrc">nnrc</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_nnrc_optimizer_logger">model.compiler_model_nnrc_optimizer_logger</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_nnrs_imp_expr_optimizer_logger">compiler_nnrs_imp_expr_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NNRSimp.Lang.NNRSimp.html#nnrs_imp_expr">nnrs_imp_expr</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_nnrs_imp_expr_optimizer_logger">model.compiler_model_nnrs_imp_expr_optimizer_logger</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_nnrs_imp_stmt_optimizer_logger">compiler_nnrs_imp_stmt_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NNRSimp.Lang.NNRSimp.html#nnrs_imp_stmt">nnrs_imp_stmt</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_nnrs_imp_stmt_optimizer_logger">model.compiler_model_nnrs_imp_stmt_optimizer_logger</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_nnrs_imp_optimizer_logger">compiler_nnrs_imp_optimizer_logger</a></span> : <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> <span class="id"><a href="Qcert.NNRSimp.Lang.NNRSimp.html#nnrs_imp">nnrs_imp</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_nnrs_imp_optimizer_logger">model.compiler_model_nnrs_imp_optimizer_logger</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_dnnrc_optimizer_logger">compiler_dnnrc_optimizer_logger</a></span> {<span class="id">br</span>:<span class="id"><a href="Qcert.Brands.BrandRelation.html#brand_relation">brand_relation</a></span>}: <span class="id"><a href="Qcert.Utils.OptimizerLogger.html#optimizer_logger">optimizer_logger</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> (<span class="id"><a href="Qcert.tDNNRC.Lang.tDNNRC.html#dnnrc_typed">dnnrc_typed</a></span>)<br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_dnnrc_optimizer_logger">model.compiler_model_dnnrc_optimizer_logger</a></span>.<br/>
<span class="kwd">Definition</span> <span class="id"><a name="CompilerModelRuntime.compiler_foreign_data_typing">compiler_foreign_data_typing</a></span> : <span class="id"><a href="Qcert.Data.ModelTyping.ForeignDataTyping.html#foreign_data_typing">foreign_data_typing</a></span><br/>
:= <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#model.compiler_model_foreign_data_typing">model.compiler_model_foreign_data_typing</a></span>.<br/>
<span class="kwd">End</span> <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#CompilerModelRuntime">CompilerModelRuntime</a></span>.<br/>
<br/>
<span class="kwd">Module</span> <span class="kwd">Type</span> <span class="id"><a name="CompilerForeignType">CompilerForeignType</a></span>.<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerForeignType.compiler_foreign_type">compiler_foreign_type</a></span> : <span class="id"><a href="Qcert.TypeSystem.ForeignType.html#foreign_type">foreign_type</a></span>.<br/>
<span class="kwd">End</span> <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#CompilerForeignType">CompilerForeignType</a></span>.<br/>
<span class="kwd">Module</span> <span class="kwd">Type</span> <span class="id"><a name="CompilerBrandModel">CompilerBrandModel</a></span>(<span class="id">ftype</span>:<span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#CompilerForeignType">CompilerForeignType</a></span>).<br/>
<span class="id">Declare</span> <span class="kwd">Instance</span> <span class="id"><a name="CompilerBrandModel.compiler_brand_model">compiler_brand_model</a></span> : <span class="id"><a href="Qcert.TypeSystem.TBrandModel.html#brand_model">brand_model</a></span>.<br/>
<span class="kwd">End</span> <span class="id"><a href="Qcert.Compiler.Model.CompilerModel.html#CompilerBrandModel">CompilerBrandModel</a></span>.<br/>
<br/>
</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</a></div>
</body>
</html>