Skip to content

Commit

Permalink
Deploying to gh-pages from @ 446af7c 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@Gbury
Gbury committed Oct 10, 2023
1 parent bc48136 commit 52d56c2
Show file tree
Hide file tree
Showing 21 changed files with 56 additions and 14 deletions.
2 changes: 2 additions & 0 deletions dev/dolmen/Dolmen_class/Logic/Make/argument-5-E/Smtlib2/index.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Smtlib2 (dolmen.Dolmen_class.Logic.Make.E.Smtlib2)</title><link rel="stylesheet" href="../../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc v2.3.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../../index.html">dolmen</a> &#x00BB; <a href="../../../../index.html">Dolmen_class</a> &#x00BB; <a href="../../../index.html">Logic</a> &#x00BB; <a href="../../index.html">Make</a> &#x00BB; <a href="../index.html">E</a> &#x00BB; Smtlib2</nav><header class="odoc-preamble"><h1>Module <code><span>E.Smtlib2</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value anchored" id="val-statement"><a href="#val-statement" class="anchor"></a><code><span><span class="keyword">val</span> statement : <span>string <span class="arrow">&#45;&gt;</span></span> <span><span>(<span><span class="optlabel">?loc</span>:<a href="../../argument-1-L/index.html#type-t">L.t</a> <span class="arrow">&#45;&gt;</span></span> <span><span><a href="../../argument-3-T/index.html#type-t">T.t</a> list</span> <span class="arrow">&#45;&gt;</span></span> <a href="../../argument-4-S/index.html#type-t">S.t</a>)</span> option</span></span></code></div><div class="spec-doc"><p>Called on statements of the form `(&lt;id&gt; &lt;term&gt;)` where `&lt;id&gt;` is not the name of a statement in the official smtlib specification.</p></div></div></div></body></html>
2 changes: 2 additions & 0 deletions dev/dolmen/Dolmen_class/Logic/Make/argument-5-E/index.html
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>E (dolmen.Dolmen_class.Logic.Make.E)</title><link rel="stylesheet" href="../../../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc v2.3.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../../index.html">dolmen</a> &#x00BB; <a href="../../../index.html">Dolmen_class</a> &#x00BB; <a href="../../index.html">Logic</a> &#x00BB; <a href="../index.html">Make</a> &#x00BB; E</nav><header class="odoc-preamble"><h1>Parameter <code><span>Make.E</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec module anchored" id="module-Smtlib2"><a href="#module-Smtlib2" class="anchor"></a><code><span><span class="keyword">module</span> <a href="Smtlib2/index.html">Smtlib2</a></span><span> : <span class="keyword">sig</span> ... <span class="keyword">end</span></span></code></div></div></div></body></html>
6 changes: 5 additions & 1 deletion dev/dolmen/Dolmen_class/Logic/Make/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,11 @@
<a href="../../../Dolmen_intf/Stmt/module-type-Logic/index.html">Dolmen_intf.Stmt.Logic</a>
<span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-location">location</a> := <a href="argument-1-L/index.html#type-t">L.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-id">id</a> := <a href="argument-2-I/index.html#type-t">I.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-term">term</a> := <a href="argument-3-T/index.html#type-t">T.t</a></span></span></code></div></div><h2 id="signature"><a href="#signature" class="anchor"></a>Signature</h2><div class="odoc-spec"><div class="spec exception anchored" id="exception-Extension_not_found"><a href="#exception-Extension_not_found" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Extension_not_found</span> <span class="keyword">of</span> string</span></code></div><div class="spec-doc"><p>Raised when trying to find a language given a file extension.</p></div></div><h3 id="supported-languages"><a href="#supported-languages" class="anchor"></a>Supported languages</h3><div class="odoc-spec"><div class="spec type anchored" id="type-language"><a href="#type-language" class="anchor"></a><code><span><span class="keyword">type</span> language</span><span> = </span></code><ol><li id="type-language.Alt_ergo" class="def variant constructor anchored"><a href="#type-language.Alt_ergo" class="anchor"></a><code><span>| </span><span><span class="constructor">Alt_ergo</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Alt-ergo's native language</p><span class="comment-delim">*)</span></div></li><li id="type-language.Dimacs" class="def variant constructor anchored"><a href="#type-language.Dimacs" class="anchor"></a><code><span>| </span><span><span class="constructor">Dimacs</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Dimacs CNF format</p><span class="comment-delim">*)</span></div></li><li id="type-language.ICNF" class="def variant constructor anchored"><a href="#type-language.ICNF" class="anchor"></a><code><span>| </span><span><span class="constructor">ICNF</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>iCNF format</p><span class="comment-delim">*)</span></div></li><li id="type-language.Smtlib2" class="def variant constructor anchored"><a href="#type-language.Smtlib2" class="anchor"></a><code><span>| </span><span><span class="constructor">Smtlib2</span> <span class="keyword">of</span> <a href="../../../Dolmen_smtlib2/Script/index.html#type-version">Dolmen_smtlib2.Script.version</a></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Smtlib v2 latest version</p><span class="comment-delim">*)</span></div></li><li id="type-language.Tptp" class="def variant constructor anchored"><a href="#type-language.Tptp" class="anchor"></a><code><span>| </span><span><span class="constructor">Tptp</span> <span class="keyword">of</span> <a href="../../../Dolmen_tptp/index.html#type-version">Dolmen_tptp.version</a></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>TPTP format (including THF), latest version</p><span class="comment-delim">*)</span></div></li><li id="type-language.Zf" class="def variant constructor anchored"><a href="#type-language.Zf" class="anchor"></a><code><span>| </span><span><span class="constructor">Zf</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Zipperposition format</p><span class="comment-delim">*)</span></div></li></ol></div><div class="spec-doc"><p>The languages supported by the Logic class.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-enum"><a href="#val-enum" class="anchor"></a><code><span><span class="keyword">val</span> enum : <span><span>(string * <a href="#type-language">language</a>)</span> list</span></span></code></div><div class="spec-doc"><p>Enumeration of languages together with an appropriate name. Can be used for command-line arguments (for instance, with cmdliner).</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-string_of_language"><a href="#val-string_of_language" class="anchor"></a><code><span><span class="keyword">val</span> string_of_language : <span><a href="#type-language">language</a> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p>String representation of the variant</p></div></div><h3 id="high-level-parsing"><a href="#high-level-parsing" class="anchor"></a>High-level parsing</h3><div class="odoc-spec"><div class="spec value anchored" id="val-find"><a href="#val-find" class="anchor"></a><code><span><span class="keyword">val</span> find : <span><span class="optlabel">?language</span>:<a href="#type-language">language</a> <span class="arrow">&#45;&gt;</span></span> <span><span class="optlabel">?dir</span>:string <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <span>string option</span></span></code></div><div class="spec-doc"><p>Tries and find the given file, using the language specification.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_file"><a href="#val-parse_file" class="anchor"></a><code><span><span class="keyword">val</span> parse_file : <span><span class="optlabel">?language</span>:<a href="#type-language">language</a> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <a href="#type-language">language</a> * <a href="argument-1-L/index.html#type-file">L.file</a> * <span><a href="argument-4-S/index.html#type-t">S.t</a> list</span></span></code></div><div class="spec-doc"><p>Given a filename, parse the file, and return the detected language together with the list of statements parsed.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">language</span> <p>specify a language; overrides auto-detection.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_file_lazy"><a href="#val-parse_file_lazy" class="anchor"></a><code><span><span class="keyword">val</span> parse_file_lazy :
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-term">term</a> := <a href="argument-3-T/index.html#type-t">T.t</a></span></span></code></div></div><div class="odoc-spec"><div class="spec parameter anchored" id="argument-5-E"><a href="#argument-5-E" class="anchor"></a><code><span><span class="keyword">module</span> </span><span><a href="argument-5-E/index.html">E</a></span><span> :
<a href="../../../Dolmen_intf/Ext/module-type-Logic/index.html">Dolmen_intf.Ext.Logic</a>
<span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../Dolmen_intf/Ext/module-type-Logic/index.html#type-location">location</a> := <a href="argument-1-L/index.html#type-t">L.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../Dolmen_intf/Ext/module-type-Logic/index.html#type-term">term</a> := <a href="argument-3-T/index.html#type-t">T.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../../Dolmen_intf/Ext/module-type-Logic/index.html#type-statement">statement</a> := <a href="argument-4-S/index.html#type-t">S.t</a></span></span></code></div></div><h2 id="signature"><a href="#signature" class="anchor"></a>Signature</h2><div class="odoc-spec"><div class="spec exception anchored" id="exception-Extension_not_found"><a href="#exception-Extension_not_found" class="anchor"></a><code><span><span class="keyword">exception</span> </span><span><span class="exception">Extension_not_found</span> <span class="keyword">of</span> string</span></code></div><div class="spec-doc"><p>Raised when trying to find a language given a file extension.</p></div></div><h3 id="supported-languages"><a href="#supported-languages" class="anchor"></a>Supported languages</h3><div class="odoc-spec"><div class="spec type anchored" id="type-language"><a href="#type-language" class="anchor"></a><code><span><span class="keyword">type</span> language</span><span> = </span></code><ol><li id="type-language.Alt_ergo" class="def variant constructor anchored"><a href="#type-language.Alt_ergo" class="anchor"></a><code><span>| </span><span><span class="constructor">Alt_ergo</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Alt-ergo's native language</p><span class="comment-delim">*)</span></div></li><li id="type-language.Dimacs" class="def variant constructor anchored"><a href="#type-language.Dimacs" class="anchor"></a><code><span>| </span><span><span class="constructor">Dimacs</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Dimacs CNF format</p><span class="comment-delim">*)</span></div></li><li id="type-language.ICNF" class="def variant constructor anchored"><a href="#type-language.ICNF" class="anchor"></a><code><span>| </span><span><span class="constructor">ICNF</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>iCNF format</p><span class="comment-delim">*)</span></div></li><li id="type-language.Smtlib2" class="def variant constructor anchored"><a href="#type-language.Smtlib2" class="anchor"></a><code><span>| </span><span><span class="constructor">Smtlib2</span> <span class="keyword">of</span> <a href="../../../Dolmen_smtlib2/Script/index.html#type-version">Dolmen_smtlib2.Script.version</a></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Smtlib v2 latest version</p><span class="comment-delim">*)</span></div></li><li id="type-language.Tptp" class="def variant constructor anchored"><a href="#type-language.Tptp" class="anchor"></a><code><span>| </span><span><span class="constructor">Tptp</span> <span class="keyword">of</span> <a href="../../../Dolmen_tptp/index.html#type-version">Dolmen_tptp.version</a></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>TPTP format (including THF), latest version</p><span class="comment-delim">*)</span></div></li><li id="type-language.Zf" class="def variant constructor anchored"><a href="#type-language.Zf" class="anchor"></a><code><span>| </span><span><span class="constructor">Zf</span></span></code><div class="def-doc"><span class="comment-delim">(*</span><p>Zipperposition format</p><span class="comment-delim">*)</span></div></li></ol></div><div class="spec-doc"><p>The languages supported by the Logic class.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-enum"><a href="#val-enum" class="anchor"></a><code><span><span class="keyword">val</span> enum : <span><span>(string * <a href="#type-language">language</a>)</span> list</span></span></code></div><div class="spec-doc"><p>Enumeration of languages together with an appropriate name. Can be used for command-line arguments (for instance, with cmdliner).</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-string_of_language"><a href="#val-string_of_language" class="anchor"></a><code><span><span class="keyword">val</span> string_of_language : <span><a href="#type-language">language</a> <span class="arrow">&#45;&gt;</span></span> string</span></code></div><div class="spec-doc"><p>String representation of the variant</p></div></div><h3 id="high-level-parsing"><a href="#high-level-parsing" class="anchor"></a>High-level parsing</h3><div class="odoc-spec"><div class="spec value anchored" id="val-find"><a href="#val-find" class="anchor"></a><code><span><span class="keyword">val</span> find : <span><span class="optlabel">?language</span>:<a href="#type-language">language</a> <span class="arrow">&#45;&gt;</span></span> <span><span class="optlabel">?dir</span>:string <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <span>string option</span></span></code></div><div class="spec-doc"><p>Tries and find the given file, using the language specification.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_file"><a href="#val-parse_file" class="anchor"></a><code><span><span class="keyword">val</span> parse_file : <span><span class="optlabel">?language</span>:<a href="#type-language">language</a> <span class="arrow">&#45;&gt;</span></span> <span>string <span class="arrow">&#45;&gt;</span></span> <a href="#type-language">language</a> * <a href="argument-1-L/index.html#type-file">L.file</a> * <span><a href="argument-4-S/index.html#type-t">S.t</a> list</span></span></code></div><div class="spec-doc"><p>Given a filename, parse the file, and return the detected language together with the list of statements parsed.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">language</span> <p>specify a language; overrides auto-detection.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_file_lazy"><a href="#val-parse_file_lazy" class="anchor"></a><code><span><span class="keyword">val</span> parse_file_lazy :
<span><span class="optlabel">?language</span>:<a href="#type-language">language</a> <span class="arrow">&#45;&gt;</span></span>
<span>string <span class="arrow">&#45;&gt;</span></span>
<a href="#type-language">language</a> * <a href="argument-1-L/index.html#type-file">L.file</a> * <span><span><a href="argument-4-S/index.html#type-t">S.t</a> list</span> <span class="xref-unresolved">Stdlib</span>.Lazy.t</span></span></code></div><div class="spec-doc"><p>Given a filename, parse the file, and return the detected language together with the list of statements parsed.</p><ul class="at-tags"><li class="parameter"><span class="at-tag">parameter</span> <span class="value">language</span> <p>specify a language; overrides auto-detection.</p></li></ul></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-parse_raw_lazy"><a href="#val-parse_raw_lazy" class="anchor"></a><code><span><span class="keyword">val</span> parse_raw_lazy :
Expand Down
7 changes: 6 additions & 1 deletion dev/dolmen/Dolmen_class/Logic/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,5 +7,10 @@
<a href="../../Dolmen_intf/Stmt/module-type-Logic/index.html">Dolmen_intf.Stmt.Logic</a>
<span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-location">location</a> := <a href="Make/argument-1-L/index.html#type-t">L.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-id">id</a> := <a href="Make/argument-2-I/index.html#type-t">I.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-term">term</a> := <a href="Make/argument-3-T/index.html#type-t">T.t</a></span>) :
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../Dolmen_intf/Stmt/module-type-Logic/index.html#type-term">term</a> := <a href="Make/argument-3-T/index.html#type-t">T.t</a></span>)
(<a href="Make/argument-5-E/index.html">E</a> :
<a href="../../Dolmen_intf/Ext/module-type-Logic/index.html">Dolmen_intf.Ext.Logic</a>
<span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Dolmen_intf/Ext/module-type-Logic/index.html#type-location">location</a> := <a href="Make/argument-1-L/index.html#type-t">L.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../Dolmen_intf/Ext/module-type-Logic/index.html#type-term">term</a> := <a href="Make/argument-3-T/index.html#type-t">T.t</a></span>
<span class="keyword">and</span> <span><span class="keyword">type</span> <a href="../../Dolmen_intf/Ext/module-type-Logic/index.html#type-statement">statement</a> := <a href="Make/argument-4-S/index.html#type-t">S.t</a></span>) :
<a href="module-type-S/index.html">S</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="module-type-S/index.html#type-statement">statement</a> := <a href="Make/argument-4-S/index.html#type-t">S.t</a></span> <span class="keyword">and</span> <span><span class="keyword">type</span> <a href="module-type-S/index.html#type-file">file</a> := <a href="Make/argument-1-L/index.html#type-file">L.file</a></span></span></code></div></div></div></body></html>
Loading

0 comments on commit 52d56c2

Please sign in to comment.