Skip to content

Add patricia tree doc #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 47 commits into from
May 31, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
1dbc2af
Integrate some odoc stuff from frama-c
dlesbre May 6, 2024
8d4da97
highlightjs
dlesbre May 7, 2024
50622cc
404 page
dlesbre May 7, 2024
0878e27
label
dlesbre May 7, 2024
9b1a757
No link on last breadcrumb
dlesbre May 7, 2024
691b569
Add github icon
dlesbre May 7, 2024
7e92cfc
move css to frontmatter
dlesbre May 7, 2024
ddaa4c3
Credit source
dlesbre May 8, 2024
1a7cbf2
Fix newlines not preserved in code blocks
dlesbre May 8, 2024
698d8a3
Fix duplicate headings
dlesbre May 10, 2024
745a8ff
Page TOC
dlesbre May 10, 2024
8044895
Customize color a bit
dlesbre May 10, 2024
57212bf
Style callouts
dlesbre May 13, 2024
5b73c4d
odoc rb now add package and version number
dlesbre May 13, 2024
1a3adca
Fix breadcrumbs
dlesbre May 13, 2024
094cc61
Warning on non latest version
dlesbre May 13, 2024
da4ca11
sherlodoc search bar
dlesbre May 13, 2024
dfb20bc
Fix warning message
dlesbre May 13, 2024
5e7153a
JSON and DBs
dlesbre May 13, 2024
0954641
Add redirects
dlesbre May 14, 2024
7d6a8e2
API and package
dlesbre May 14, 2024
2f6e5da
Description
dlesbre May 14, 2024
e611788
Move API
dlesbre May 17, 2024
d816bf1
Heading anchors
dlesbre May 17, 2024
9153100
Fix conditional assign
dlesbre May 17, 2024
72ed2f8
No html in path
dlesbre May 17, 2024
a9f4c28
inline code color
dlesbre May 17, 2024
66fe5b3
Nav order
dlesbre May 21, 2024
236ac54
API to md
dlesbre May 21, 2024
d764baa
Patricia-tree page
dlesbre May 21, 2024
9225392
Text on search bar
dlesbre May 21, 2024
4fc2e08
404 search
dlesbre May 21, 2024
52466b2
DBs in folder
dlesbre May 21, 2024
b881c7e
Redirect from latest
dlesbre May 21, 2024
92bb1bd
Comments
dlesbre May 21, 2024
bef69cc
comment + just the doc search
dlesbre May 21, 2024
413d178
Fix URLs
dlesbre May 21, 2024
5e1e1a1
Warning above name
dlesbre May 21, 2024
f749339
Add odoc to search
dlesbre May 21, 2024
be1bd46
Comment
dlesbre May 21, 2024
7ca3574
Update PatriciaTree doc to v0.10.0
dlesbre May 21, 2024
f6094e0
Fix redirect link
dlesbre May 21, 2024
49f5b31
Fix include parameter
dlesbre May 22, 2024
7ca8141
RM accidentaly commited vscode config
dlesbre May 22, 2024
079590c
Clean up packages.yml
dlesbre May 22, 2024
82311c5
Update mld
dlesbre May 27, 2024
97e6062
v0.10.0 + link to examples
dlesbre May 31, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
6 changes: 4 additions & 2 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -12,5 +12,7 @@ _site/

# Ignore folders generated by Bundler
.bundle/
vendor/
*~
*~

# VS Code editor config
.vscode/
12 changes: 12 additions & 0 deletions 404.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
---
layout: default
title: 404
nav_exclude: true
search_exclude: true
permalink: /404.html
---

<h1>Error 404</h1>

<p><strong>Page not found :(</strong></p>
<p>The requested page could not be found.</p>
1 change: 1 addition & 0 deletions Gemfile
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,4 @@ source "https://rubygems.org"
gem "just-the-docs", "0.8.2" # pinned to the current release
gem "github-pages"
gem "webrick"
gem "jekyll-redirect-from"
1 change: 1 addition & 0 deletions Gemfile.lock
Original file line number Diff line number Diff line change
Expand Up @@ -270,6 +270,7 @@ PLATFORMS

DEPENDENCIES
github-pages
jekyll-redirect-from
just-the-docs (= 0.8.2)
webrick

Expand Down
31 changes: 25 additions & 6 deletions _config.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,31 @@ color_scheme: myscheme
url: https://codex-semantics-library.github.io

aux_links:
Repository: https://github.com/codex-semantics-library/codex
'<i class="fab fa-github"></i> &nbsp; Repository': https://github.com/codex-semantics-library/codex

logo: "/assets/codex.png"

nav_external_links:
- title: Patricia Tree Library
url: patricia-tree
hide_icon: true # set to true to hide the external link icon - defaults to false
opens_in_new_tab: false # set to true to open this link in a new tab - defaults to false
callouts:
warning:
title: Warning
color: red
note:
color: blue

exclude: [
Makefile,
README.md,
.sass-cache/,
.jekyll-cache/,
gemfiles/,
Gemfile,
Gemfile.lock
node_modules/,
vendor/bundle/,
vendor/cache/,
vendor/gems/,
vendor/ruby/,
]

plugins:
- jekyll-redirect-from
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"type":"documentation","uses_katex":false,"breadcrumbs":[{"name":"patricia-tree","href":"../../../index.html","kind":"page"},{"name":"PatriciaTree","href":"../../index.html","kind":"module"},{"name":"HashconsedNode","href":"../index.html","kind":"module"},{"name":"Key","href":"#","kind":"argument-1"}],"toc":[],"source_anchor":null,"preamble":"","content":"<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> <span>'key t</span></span></code></div><div class=\"spec-doc\"><p>The type of generic/heterogeneous keys.</p><p><b>It is recommended to use immutable keys.</b> If keys are mutable, any mutations to keys must preserve <a href=\"#val-to_int\"><code>to_int</code></a>. Failing to do so will break the patricia trees' invariants.</p></div></div><div class=\"odoc-spec\"><div class=\"spec value anchored\" id=\"val-to_int\"><a href=\"#val-to_int\" class=\"anchor\"></a><code><span><span class=\"keyword\">val</span> to_int : <span><span><span class=\"type-var\">'key</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> int</span></code></div><div class=\"spec-doc\"><p>A unique identifier for values of the type. Usually, we use a fresh counter that is increased to give a unique id to each object. Correctness of the operations requires that different values in a tree correspond to different integers.</p><p><b>Must be injective, and ideally fast.</b> <a href=\"https://en.wikipedia.org/wiki/Hash_consing\">hash-consing</a> keys is a good way to generate such unique identifiers.</p><p>Note that since Patricia Trees use <a href=\"../../index.html#val-unsigned_lt\" title=\"unsigned_lt\">unsigned order</a>, negative keys are seen as bigger than positive keys. Be wary of this when using negative keys combined with functions like <a href=\"../../module-type-BASE_MAP/index.html#val-unsigned_max_binding\" title=\"BASE_MAP.unsigned_max_binding\"><code>unsigned_max_binding</code></a> and <a href=\"../../module-type-BASE_MAP/index.html#val-pop_unsigned_maximum\" title=\"BASE_MAP.pop_unsigned_maximum\"><code>pop_unsigned_maximum</code></a>.</p></div></div><div class=\"odoc-spec\"><div class=\"spec value anchored\" id=\"val-polyeq\"><a href=\"#val-polyeq\" class=\"anchor\"></a><code><span><span class=\"keyword\">val</span> polyeq : <span><span><span class=\"type-var\">'a</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> <span><span><span class=\"type-var\">'b</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> <span><span>(<span class=\"type-var\">'a</span>, <span class=\"type-var\">'b</span>)</span> <a href=\"../../index.html#type-cmp\">cmp</a></span></span></code></div><div class=\"spec-doc\"><p>Polymorphic equality function used to compare our keys. It should satisfy <code>(to_int a) = (to_int b) ==&gt; polyeq a b = Eq</code>, and be fast.</p></div></div>"}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"type":"documentation","uses_katex":false,"breadcrumbs":[{"name":"patricia-tree","href":"../../../index.html","kind":"page"},{"name":"PatriciaTree","href":"../../index.html","kind":"module"},{"name":"HashconsedNode","href":"../index.html","kind":"module"},{"name":"Value","href":"#","kind":"argument-2"}],"toc":[],"source_anchor":null,"preamble":"","content":"<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> <span>('key, 'map) t</span></span></code></div><div class=\"spec-doc\"><p>The type of values for a hash-consed maps.</p><p>Unlike <a href=\"../../module-type-HETEROGENEOUS_VALUE/index.html#type-t\"><code>HETEROGENEOUS_VALUE.t</code></a>, <b>hash-consed values should be immutable</b>. Or, if they do mutate, they must not change their <a href=\"#val-hash\"><code>hash</code></a> value, and still be equal to the same values via <a href=\"#val-polyeq\"><code>polyeq</code></a></p></div></div><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><span><span>(<span class=\"type-var\">'key</span>, <span class=\"type-var\">'map</span>)</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> int</span></code></div><div class=\"spec-doc\"><p><code>hash v</code> should return an integer hash for the value <code>v</code>. It is used for <a href=\"../../index.html#hash_consed\" title=\"hash_consed\">hash-consing</a>.</p><p>Hashing should be fast, avoid mapping too many values to the same integer and compatible with <a href=\"#val-polyeq\"><code>polyeq</code></a> (equal values must have the same hash: <code>polyeq v1 v2 = true ==&gt; hash v1 = hash v2</code>).</p></div></div><div class=\"odoc-spec\"><div class=\"spec value anchored\" id=\"val-polyeq\"><a href=\"#val-polyeq\" class=\"anchor\"></a><code><span><span class=\"keyword\">val</span> polyeq : <span><span><span>(<span class=\"type-var\">'key</span>, <span class=\"type-var\">'map_a</span>)</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> <span><span><span>(<span class=\"type-var\">'key</span>, <span class=\"type-var\">'map_b</span>)</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> bool</span></code></div><div class=\"spec-doc\"><p>Polymorphic equality on values.</p><p><b>WARNING: if <code>polyeq a b</code> is true, then casting <code>b</code> to the type of <code>a</code> (and <code>a</code> to the type of <code>b</code>) must be type-safe.</b> Eg. if <code>a : (k, t1) t</code> and <code>b : (k, t2) t</code> yield <code>polyeq a b = true</code>, then <code>let a' : (k,t2) t = Obj.magic a</code> and <code>let b' : (k,t1) t = Obj.magic b</code> must be safe.</p><p>Examples of safe implementations include:</p><ul><li><p>Having a type <code>('key, 'map) t</code> which doesn't depend on <code>'map</code> (i can depend on <code>'key</code>), in which case casting form <code>('key, 'a) t</code> to <code>('key, 'b) t</code> is always safe:</p><pre class=\"language-ocaml\"><code>type ('k, _) t = 'k list\u000Alet cast : type a b. ('k, a) t -&gt; ('k, b) t = fun x -&gt; x\u000Alet polyeq : type a b. ('k, a) t -&gt; ('k, b) t -&gt; bool = fun x y -&gt; x = y</code></pre></li><li><p>Using a GADT type and examining its constructors to only return <code>true</code> when the constructors are equal:</p><pre class=\"language-ocaml\"><code>type (_, _) t =\u000A | T_Int : int -&gt; (unit, int) t\u000A | T_Bool : bool -&gt; (unit, bool) t\u000Alet polyeq : type k a b. (k, a) t -&gt; (k, b) t -&gt; bool = fun x y -&gt;\u000A match x, y with\u000A | T_Int i, T_Int j -&gt; i = j (* Here type a = b = int, we can return true *)\u000A | T_Bool i, T_Bool j -&gt; i &amp;&amp; j (* same here, but with a = b = bool *)\u000A | _ -&gt; false (* never return true on heterogeneous cases. *)</code></pre></li><li><p>Using physical equality:</p><pre class=\"language-ocaml\"><code>let polyeq a b = a == Obj.magic b</code></pre><p>While this contains an <code>Obj.magic</code>, it is still type safe (OCaml just compares the immediate values) and we can safely cast values from one type to the other if they satisfy this (since they are already physically equal).</p><p>This is the implementation used in <a href=\"../../HeterogeneousHashedValue/index.html\"><code>HeterogeneousHashedValue</code></a>. Note however that using this function can lead to <b>identifiers no longer being unique across types</b>. See <a href=\"../../module-type-HASHED_VALUE/index.html#val-polyeq\"><code>HASHED_VALUE.polyeq</code></a> for more information on this.</p></li></ul></div></div>"}

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"type":"documentation","uses_katex":false,"breadcrumbs":[{"name":"patricia-tree","href":"../../../index.html","kind":"page"},{"name":"PatriciaTree","href":"../../index.html","kind":"module"},{"name":"HashconsedSetNode","href":"../index.html","kind":"module"},{"name":"Key","href":"#","kind":"argument-1"}],"toc":[],"source_anchor":null,"preamble":"","content":"<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> <span>'key t</span></span></code></div><div class=\"spec-doc\"><p>The type of generic/heterogeneous keys.</p><p><b>It is recommended to use immutable keys.</b> If keys are mutable, any mutations to keys must preserve <a href=\"#val-to_int\"><code>to_int</code></a>. Failing to do so will break the patricia trees' invariants.</p></div></div><div class=\"odoc-spec\"><div class=\"spec value anchored\" id=\"val-to_int\"><a href=\"#val-to_int\" class=\"anchor\"></a><code><span><span class=\"keyword\">val</span> to_int : <span><span><span class=\"type-var\">'key</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> int</span></code></div><div class=\"spec-doc\"><p>A unique identifier for values of the type. Usually, we use a fresh counter that is increased to give a unique id to each object. Correctness of the operations requires that different values in a tree correspond to different integers.</p><p><b>Must be injective, and ideally fast.</b> <a href=\"https://en.wikipedia.org/wiki/Hash_consing\">hash-consing</a> keys is a good way to generate such unique identifiers.</p><p>Note that since Patricia Trees use <a href=\"../../index.html#val-unsigned_lt\" title=\"unsigned_lt\">unsigned order</a>, negative keys are seen as bigger than positive keys. Be wary of this when using negative keys combined with functions like <a href=\"../../module-type-BASE_MAP/index.html#val-unsigned_max_binding\" title=\"BASE_MAP.unsigned_max_binding\"><code>unsigned_max_binding</code></a> and <a href=\"../../module-type-BASE_MAP/index.html#val-pop_unsigned_maximum\" title=\"BASE_MAP.pop_unsigned_maximum\"><code>pop_unsigned_maximum</code></a>.</p></div></div><div class=\"odoc-spec\"><div class=\"spec value anchored\" id=\"val-polyeq\"><a href=\"#val-polyeq\" class=\"anchor\"></a><code><span><span class=\"keyword\">val</span> polyeq : <span><span><span class=\"type-var\">'a</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> <span><span><span class=\"type-var\">'b</span> <a href=\"#type-t\">t</a></span> <span class=\"arrow\">&#45;&gt;</span></span> <span><span>(<span class=\"type-var\">'a</span>, <span class=\"type-var\">'b</span>)</span> <a href=\"../../index.html#type-cmp\">cmp</a></span></span></code></div><div class=\"spec-doc\"><p>Polymorphic equality function used to compare our keys. It should satisfy <code>(to_int a) = (to_int b) ==&gt; polyeq a b = Eq</code>, and be fast.</p></div></div>"}
Loading
Loading