mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-07 11:45:41 -05:00
40 lines
42 KiB
HTML
40 lines
42 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Term (sidekick-base.Sidekick_base.Term)</title><meta charset="utf-8"/><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta name="generator" content="odoc 2.4.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">sidekick-base</a> » <a href="../index.html">Sidekick_base</a> » Term</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_base.Term</span></code></h1></header><div class="odoc-content"><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_core/Term/index.html">Sidekick_core.Term</a> <span class="keyword">end</span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html">Sidekick_core_logic.Term</a> <span class="keyword">end</span></span></code></summary><div class="odoc-spec"><div class="spec type anchored" id="type-var"><a href="#type-var" class="anchor"></a><code><span><span class="keyword">type</span> var</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Var/index.html#type-t">Sidekick_core_logic.Var.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-bvar"><a href="#type-bvar" class="anchor"></a><code><span><span class="keyword">type</span> bvar</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Bvar/index.html#type-t">Sidekick_core_logic.Bvar.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>A term, in the calculus of constructions</p></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-store"><a href="#type-store" class="anchor"></a><code><span><span class="keyword">type</span> store</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a></span></code></div><div class="spec-doc"><p>The store for terms.</p><p>The store is responsible for allocating unique IDs to terms, and enforcing their hashconsing (so that syntactic equality is just a pointer comparison).</p></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-view"><a href="#type-view" class="anchor"></a><code><span><span class="keyword">type</span> view</span><span> = </span></code><ol><li id="type-view.E_type" class="def variant constructor anchored"><a href="#type-view.E_type" class="anchor"></a><code><span>| </span><span><span class="constructor">E_type</span> <span class="keyword">of</span> int</span></code></li><li id="type-view.E_var" class="def variant constructor anchored"><a href="#type-view.E_var" class="anchor"></a><code><span>| </span><span><span class="constructor">E_var</span> <span class="keyword">of</span> <a href="#type-var">var</a></span></code></li><li id="type-view.E_bound_var" class="def variant constructor anchored"><a href="#type-view.E_bound_var" class="anchor"></a><code><span>| </span><span><span class="constructor">E_bound_var</span> <span class="keyword">of</span> <a href="#type-bvar">bvar</a></span></code></li><li id="type-view.E_app" class="def variant constructor anchored"><a href="#type-view.E_app" class="anchor"></a><code><span>| </span><span><span class="constructor">E_app</span> <span class="keyword">of</span> <a href="#type-t">t</a> * <a href="#type-t">t</a></span></code></li><li id="type-view.E_lam" class="def variant constructor anchored"><a href="#type-view.E_lam" class="anchor"></a><code><span>| </span><span><span class="constructor">E_lam</span> <span class="keyword">of</span> string * <a href="#type-t">t</a> * <a href="#type-t">t</a></span></code></li><li id="type-view.E_pi" class="def variant constructor anchored"><a href="#type-view.E_pi" class="anchor"></a><code><span>| </span><span><span class="constructor">E_pi</span> <span class="keyword">of</span> string * <a href="#type-t">t</a> * <a href="#type-t">t</a></span></code></li></ol></div><div class="spec-doc"><p>View.</p><p>A view is the shape of the root node of a term.</p></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ_ORD_HASH/index.html">Sidekick_sigs.EQ_ORD_HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ_ORD_HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ/index.html">Sidekick_sigs.EQ</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-EQ/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-equal"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-ORD/index.html">Sidekick_sigs.ORD</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-ORD/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span><span class="keyword">val</span> compare : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-HASH/index.html">Sidekick_sigs.HASH</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-HASH/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-hash"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> int</span></code></div></div></details></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp_debug"><a href="#val-pp_debug" class="anchor"></a><code><span><span class="keyword">val</span> pp_debug : <span><a href="#type-t">t</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp_debug_with_ids"><a href="#val-pp_debug_with_ids" class="anchor"></a><code><span><span class="keyword">val</span> pp_debug_with_ids : <span><a href="#type-t">t</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div></div><h3 id="containers"><a href="#containers" class="anchor"></a>Containers</h3><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-WITH_SET_MAP_TBL/index.html">Sidekick_sigs.WITH_SET_MAP_TBL</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-WITH_SET_MAP_TBL/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec module anchored" id="module-Set"><a href="#module-Set" class="anchor"></a><code><span><span class="keyword">module</span> Set</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Set/index.html">Sidekick_core.Term.Set</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Map"><a href="#module-Map" class="anchor"></a><code><span><span class="keyword">module</span> Map</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Map/index.html">Sidekick_core.Term.Map</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Tbl"><a href="#module-Tbl" class="anchor"></a><code><span><span class="keyword">module</span> Tbl</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Tbl/index.html">Sidekick_core.Term.Tbl</a></span></code></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../../sidekick/Sidekick_sigs/module-type-WITH_WEAK/index.html">Sidekick_sigs.WITH_WEAK</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../../sidekick/Sidekick_sigs/module-type-WITH_WEAK/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec module anchored" id="module-Weak_set"><a href="#module-Weak_set" class="anchor"></a><code><span><span class="keyword">module</span> Weak_set</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Weak_set/index.html">Sidekick_core.Term.Weak_set</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Weak_map"><a href="#module-Weak_map" class="anchor"></a><code><span><span class="keyword">module</span> Weak_map</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Weak_map/index.html">Sidekick_core.Term.Weak_map</a></span></code></div></div></details></div><h3 id="utils"><a href="#utils" class="anchor"></a>Utils</h3><div class="odoc-spec"><div class="spec value anchored" id="val-view"><a href="#val-view" class="anchor"></a><code><span><span class="keyword">val</span> view : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-view">view</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-unfold_app"><a href="#val-unfold_app" class="anchor"></a><code><span><span class="keyword">val</span> unfold_app : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a> * <span><a href="#type-t">t</a> list</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_app"><a href="#val-is_app" class="anchor"></a><code><span><span class="keyword">val</span> is_app : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_const"><a href="#val-is_const" class="anchor"></a><code><span><span class="keyword">val</span> is_const : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_pi"><a href="#val-is_pi" class="anchor"></a><code><span><span class="keyword">val</span> is_pi : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_dag"><a href="#val-iter_dag" class="anchor"></a><code><span><span class="keyword">val</span> iter_dag : <span><span class="optlabel">?seen</span>:<span>unit <span class="xref-unresolved">Tbl</span>.t</span> <span class="arrow">-></span></span> <span><span class="label">iter_ty</span>:bool <span class="arrow">-></span></span> <span><span class="label">f</span>:<span>(<span><a href="#type-t">t</a> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>iter_dag t ~f</code> calls <code>f</code> once on each subterm of <code>t</code>, <code>t</code> included. It must <b>not</b> traverse <code>t</code> as a tree, but rather as a perfectly shared DAG.</p><p>For example, in:</p><pre class="language-ocaml"><code>let x = 2 in
|
||
let y = f x x in
|
||
let z = g y x in
|
||
z = z</code></pre><p>the DAG has the following nodes:</p><pre class="language-ocaml"><code>n1: 2
|
||
n2: f n1 n1
|
||
n3: g n2 n1
|
||
n4: = n3 n3</code></pre></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-iter_shallow"><a href="#val-iter_shallow" class="anchor"></a><code><span><span class="keyword">val</span> iter_shallow : <span><span class="label">f</span>:<span>(<span>bool <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> unit)</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> unit</span></code></div><div class="spec-doc"><p><code>iter_shallow f e</code> iterates on immediate subterms of <code>e</code>, calling <code>f trdb e'</code> for each subterm <code>e'</code>, with <code>trdb = true</code> iff <code>e'</code> is directly under a binder.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-map_shallow"><a href="#val-map_shallow" class="anchor"></a><code><span><span class="keyword">val</span> map_shallow : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><span class="label">f</span>:<span>(<span>bool <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a>)</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-exists_shallow"><a href="#val-exists_shallow" class="anchor"></a><code><span><span class="keyword">val</span> exists_shallow : <span><span class="label">f</span>:<span>(<span>bool <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool)</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-for_all_shallow"><a href="#val-for_all_shallow" class="anchor"></a><code><span><span class="keyword">val</span> for_all_shallow : <span><span class="label">f</span>:<span>(<span>bool <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool)</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-contains"><a href="#val-contains" class="anchor"></a><code><span><span class="keyword">val</span> contains : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span class="label">sub</span>:<a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-free_vars_iter"><a href="#val-free_vars_iter" class="anchor"></a><code><span><span class="keyword">val</span> free_vars_iter : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-var">var</a> <span class="xref-unresolved">Iter</span>.t</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-free_vars"><a href="#val-free_vars" class="anchor"></a><code><span><span class="keyword">val</span> free_vars :
|
||
<span><span class="optlabel">?init</span>:<span class="xref-unresolved">Sidekick_core_logic__</span>.Var.Set.t <span class="arrow">-></span></span>
|
||
<span><a href="#type-t">t</a> <span class="arrow">-></span></span>
|
||
<span class="xref-unresolved">Sidekick_core_logic__</span>.Var.Set.t</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_type"><a href="#val-is_type" class="anchor"></a><code><span><span class="keyword">val</span> is_type : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p><code>is_type t</code> is true iff <code>view t</code> is <code>Type _</code></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_a_type"><a href="#val-is_a_type" class="anchor"></a><code><span><span class="keyword">val</span> is_a_type : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p><code>is_a_type t</code> is true if <code>is_ty (ty t)</code></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_closed"><a href="#val-is_closed" class="anchor"></a><code><span><span class="keyword">val</span> is_closed : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Is the term closed (all bound variables are paired with a binder)? time: O(1)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-has_fvars"><a href="#val-has_fvars" class="anchor"></a><code><span><span class="keyword">val</span> has_fvars : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> bool</span></code></div><div class="spec-doc"><p>Does the term contain free variables? time: O(1)</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-ty"><a href="#val-ty" class="anchor"></a><code><span><span class="keyword">val</span> ty : <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Return the type of this term.</p></div></div><h3 id="creation"><a href="#creation" class="anchor"></a>Creation</h3><div class="odoc-spec"><div class="spec module anchored" id="module-Store"><a href="#module-Store" class="anchor"></a><code><span><span class="keyword">module</span> Store</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/Store/index.html">Sidekick_core.Term.Store</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-type_"><a href="#val-type_" class="anchor"></a><code><span><span class="keyword">val</span> type_ : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-type_of_univ"><a href="#val-type_of_univ" class="anchor"></a><code><span><span class="keyword">val</span> type_of_univ : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-var"><a href="#val-var" class="anchor"></a><code><span><span class="keyword">val</span> var : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-var">var</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-var_str"><a href="#val-var_str" class="anchor"></a><code><span><span class="keyword">val</span> var_str : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span>string <span class="arrow">-></span></span> <span><span class="label">ty</span>:<a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-bvar"><a href="#val-bvar" class="anchor"></a><code><span><span class="keyword">val</span> bvar : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-bvar">bvar</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-bvar_i"><a href="#val-bvar_i" class="anchor"></a><code><span><span class="keyword">val</span> bvar_i : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span>int <span class="arrow">-></span></span> <span><span class="label">ty</span>:<a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-const"><a href="#val-const" class="anchor"></a><code><span><span class="keyword">val</span> const : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><span class="xref-unresolved">Sidekick_core_logic__.Types_.const</span> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-app"><a href="#val-app" class="anchor"></a><code><span><span class="keyword">val</span> app : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-app_l"><a href="#val-app_l" class="anchor"></a><code><span><span class="keyword">val</span> app_l : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span><a href="#type-t">t</a> list</span> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-app_fold"><a href="#val-app_fold" class="anchor"></a><code><span><span class="keyword">val</span> app_fold : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><span class="label">f</span>:<a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span class="label">acc0</span>:<a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span><a href="#type-t">t</a> list</span> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-lam"><a href="#val-lam" class="anchor"></a><code><span><span class="keyword">val</span> lam : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-var">var</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pi"><a href="#val-pi" class="anchor"></a><code><span><span class="keyword">val</span> pi : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-var">var</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-arrow"><a href="#val-arrow" class="anchor"></a><code><span><span class="keyword">val</span> arrow : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-arrow_l"><a href="#val-arrow_l" class="anchor"></a><code><span><span class="keyword">val</span> arrow_l : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><span><a href="#type-t">t</a> list</span> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-open_lambda"><a href="#val-open_lambda" class="anchor"></a><code><span><span class="keyword">val</span> open_lambda : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <span><span>(<a href="#type-var">var</a> * <a href="#type-t">t</a>)</span> option</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-open_lambda_exn"><a href="#val-open_lambda_exn" class="anchor"></a><code><span><span class="keyword">val</span> open_lambda_exn : <span><a href="#type-store">store</a> <span class="arrow">-></span></span> <span><a href="#type-t">t</a> <span class="arrow">-></span></span> <a href="#type-var">var</a> * <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-DB"><a href="#module-DB" class="anchor"></a><code><span><span class="keyword">module</span> DB</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/DB/index.html">Sidekick_core.Term.DB</a></span></code></div><div class="spec-doc"><p>De bruijn indices</p></div></div></details></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <span class="keyword">module</span> <span class="keyword">type</span> <span class="keyword">of</span> <span class="keyword">struct</span> <span class="keyword">include</span> <a href="../../../sidekick/Sidekick_core_logic/T_builtins/index.html">Sidekick_core_logic.T_builtins</a> <span class="keyword">end</span></span></code></summary><div class="odoc-spec"><div class="spec type extension anchored" id="extension-decl-C_bool"><a href="#extension-decl-C_bool" class="anchor"></a><code><span><span class="keyword">type</span> <span class="xref-unresolved">Sidekick_core_logic__.Types_.const_view</span> += </span></code><ol><li id="extension-C_bool" class="def variant extension anchored"><a href="#extension-C_bool" class="anchor"></a><code><span>| </span><span><span class="extension">C_bool</span></span></code></li><li id="extension-C_eq" class="def variant extension anchored"><a href="#extension-C_eq" class="anchor"></a><code><span>| </span><span><span class="extension">C_eq</span></span></code></li><li id="extension-C_ite" class="def variant extension anchored"><a href="#extension-C_ite" class="anchor"></a><code><span>| </span><span><span class="extension">C_ite</span></span></code></li><li id="extension-C_not" class="def variant extension anchored"><a href="#extension-C_not" class="anchor"></a><code><span>| </span><span><span class="extension">C_not</span></span></code></li><li id="extension-C_true" class="def variant extension anchored"><a href="#extension-C_true" class="anchor"></a><code><span>| </span><span><span class="extension">C_true</span></span></code></li><li id="extension-C_false" class="def variant extension anchored"><a href="#extension-C_false" class="anchor"></a><code><span>| </span><span><span class="extension">C_false</span></span></code></li><li id="extension-C_proof" class="def variant extension anchored"><a href="#extension-C_proof" class="anchor"></a><code><span>| </span><span><span class="extension">C_proof</span></span></code></li></ol></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-bool"><a href="#val-bool" class="anchor"></a><code><span><span class="keyword">val</span> bool : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-proof"><a href="#val-proof" class="anchor"></a><code><span><span class="keyword">val</span> proof : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-c_not"><a href="#val-c_not" class="anchor"></a><code><span><span class="keyword">val</span> c_not : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-c_eq"><a href="#val-c_eq" class="anchor"></a><code><span><span class="keyword">val</span> c_eq : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-c_ite"><a href="#val-c_ite" class="anchor"></a><code><span><span class="keyword">val</span> c_ite : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-true_"><a href="#val-true_" class="anchor"></a><code><span><span class="keyword">val</span> true_ : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-false_"><a href="#val-false_" class="anchor"></a><code><span><span class="keyword">val</span> false_ : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span> <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-bool_val"><a href="#val-bool_val" class="anchor"></a><code><span><span class="keyword">val</span> bool_val :
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span>
|
||
<span>bool <span class="arrow">-></span></span>
|
||
<a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-const_decoders"><a href="#val-const_decoders" class="anchor"></a><code><span><span class="keyword">val</span> const_decoders : <a href="../../../sidekick/Sidekick_core_logic/Const/index.html#type-decoders">Sidekick_core_logic.Const.decoders</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-eq"><a href="#val-eq" class="anchor"></a><code><span><span class="keyword">val</span> eq :
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div><div class="spec-doc"><p><code>eq a b</code> is <code>a = b</code></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-not"><a href="#val-not" class="anchor"></a><code><span><span class="keyword">val</span> not :
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-ite"><a href="#val-ite" class="anchor"></a><code><span><span class="keyword">val</span> ite :
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div><div class="spec-doc"><p><code>ite a b c</code> is <code>if a then b else c</code></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_eq"><a href="#val-is_eq" class="anchor"></a><code><span><span class="keyword">val</span> is_eq : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-is_bool"><a href="#val-is_bool" class="anchor"></a><code><span><span class="keyword">val</span> is_bool : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-abs"><a href="#val-abs" class="anchor"></a><code><span><span class="keyword">val</span> abs :
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
bool * <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div><div class="spec-doc"><p><code>abs t</code> returns an "absolute value" for the term, along with the sign of <code>t</code>.</p><p>The idea is that we want to turn <code>not a</code> into <code>(false, a)</code>, or <code>(a != b)</code> into <code>(false, a=b)</code>. For terms without a negation this should return <code>(true, t)</code>.</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-as_bool_val"><a href="#val-as_bool_val" class="anchor"></a><code><span><span class="keyword">val</span> as_bool_val : <span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span> <span>bool option</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-open_eq"><a href="#val-open_eq" class="anchor"></a><code><span><span class="keyword">val</span> open_eq :
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><span>(<a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> * <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a>)</span> option</span></span></code></div><div class="spec-doc"><p><code>open_eq (a=b)</code> returns <code>Some (a,b)</code>, <code>None</code> for other terms.</p></div></div></details></div><div class="odoc-spec"><div class="spec type anchored" id="type-term"><a href="#type-term" class="anchor"></a><code><span><span class="keyword">type</span> term</span><span> = <a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type anchored" id="type-hook"><a href="#type-hook" class="anchor"></a><code><span><span class="keyword">type</span> hook</span><span> =
|
||
<span><span class="label">recurse</span>:<span><a href="#type-term">term</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span> <span class="arrow">-></span></span>
|
||
<span><span class="xref-unresolved">Sidekick_util</span>.Fmt.t <span class="arrow">-></span></span>
|
||
<span><a href="#type-term">term</a> <span class="arrow">-></span></span>
|
||
bool</span></code></div><div class="spec-doc"><p>Printing hook, responsible for printing certain subterms</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Hooks"><a href="#module-Hooks" class="anchor"></a><code><span><span class="keyword">module</span> Hooks</span><span> = <a href="../../../sidekick/Sidekick_core/Term/Hooks/index.html">Sidekick_core.Term.Hooks</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-default_hooks"><a href="#val-default_hooks" class="anchor"></a><code><span><span class="keyword">val</span> default_hooks : <span><a href="../../../sidekick/Sidekick_core/Term/Hooks/index.html#type-t">Hooks.t</a> <span class="xref-unresolved">Stdlib</span>.ref</span></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp_with"><a href="#val-pp_with" class="anchor"></a><code><span><span class="keyword">val</span> pp_with : <span><a href="../../../sidekick/Sidekick_core/Term/Hooks/index.html#type-t">Hooks.t</a> <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div><div class="spec-doc"><p>Print using the hooks</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-term">term</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div><div class="spec-doc"><p>Print using <a href="#val-default_hooks"><code>default_hooks</code></a></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-pp_limit"><a href="#val-pp_limit" class="anchor"></a><code><span><span class="keyword">val</span> pp_limit : <span><span class="label">max_depth</span>:int <span class="arrow">-></span></span> <span><span class="label">max_nodes</span>:int <span class="arrow">-></span></span> <span><a href="#type-term">term</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div><div class="spec-doc"><p>Print with a limit on the number of nodes printed. An ellipsis is displayed otherwise.</p></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Tracer"><a href="#module-Tracer" class="anchor"></a><code><span><span class="keyword">module</span> Tracer</span><span> = <a href="../../../sidekick/Sidekick_core/Term/Tracer/index.html">Sidekick_core.Term.Tracer</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Trace_reader"><a href="#module-Trace_reader" class="anchor"></a><code><span><span class="keyword">module</span> Trace_reader</span><span> = <a href="../../../sidekick/Sidekick_core/Term/Trace_reader/index.html">Sidekick_core.Term.Trace_reader</a></span></code></div></div><div class="odoc-spec"><div class="spec module anchored" id="module-Ref"><a href="#module-Ref" class="anchor"></a><code><span><span class="keyword">module</span> Ref</span><span> = <a href="../../../sidekick/Sidekick_core/Term/Ref/index.html">Sidekick_core.Term.Ref</a></span></code></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-view_as_cc"><a href="#val-view_as_cc" class="anchor"></a><code><span><span class="keyword">val</span> view_as_cc :
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><span>(<a href="../../../sidekick/Sidekick_core_logic/Const/index.html#type-t">Sidekick_core_logic.Const.t</a>,
|
||
<a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a>,
|
||
<span><a href="../../../sidekick/Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a> list</span>)</span>
|
||
<a href="../../../sidekick/Sidekick_core/CC_view/index.html#type-t">Sidekick_core.CC_view.t</a></span></span></code></div></div></div></body></html>
|