mirror of
https://github.com/anoma/juvix.git
synced 2024-08-17 04:01:05 +03:00
Update to the latest juvix-stdlib (#2546)
This PR updates the juvix-stdlib submodule ref to the current juvix-stdlib/main. NB: The Markdown test is not stable after changes to the stdlib - the ids (deriving from internal name ids?) will change and so the expected file must be regenerated.
This commit is contained in:
parent
c237f292a7
commit
77b29c6963
@ -1 +1 @@
|
||||
Subproject commit 708d920c6ec9c12b684e17546854a61099920a08
|
||||
Subproject commit 183d4e9329a648b339ebecf2122b3e9621c99ee8
|
@ -33,9 +33,9 @@ extra-source-files:
|
||||
- assets/css/*.css
|
||||
- assets/js/*.js
|
||||
- assets/images/*.svg
|
||||
- juvix-stdlib/juvix.yaml
|
||||
- juvix-stdlib/**/*.juvix
|
||||
- include/package/**/*.juvix
|
||||
- include/package-base/**/*.juvix
|
||||
- runtime/include/**/*.h
|
||||
- runtime/**/*.a
|
||||
- runtime/src/vampir/*.pir
|
||||
|
@ -83,6 +83,7 @@ tests =
|
||||
"Test Markdown"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Test.juvix.md")
|
||||
-- Cmd to regenerate the expected file: juvix markdown --prefix-url X --prefix-id Y --no-path Test.juvix.md
|
||||
$(mkRelFile "markdown/Test.md")
|
||||
"X"
|
||||
"Y"
|
||||
|
@ -9,11 +9,11 @@ Certain blocks can be hidden from the output by adding the `hide` attribute, as
|
||||
|
||||
|
||||
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="Y740"><span class="annot"><a href="X#Y740"><span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y112"><span class="ju-constructor">zero</span></a></span> <span id="Y743"><span class="annot"><a href="X#Y743"><span class="annot"><a href="X#Y743"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y743"><span class="ju-var">x1</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y744"><span class="annot"><a href="X#Y744"><span class="annot"><a href="X#Y744"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="Y745"><span class="annot"><a href="X#Y745"><span class="annot"><a href="X#Y745"><span class="ju-var">x1</span></a></span></a></span></span> <span id="Y746"><span class="annot"><a href="X#Y746"><span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y744"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#Y745"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#Y510"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#Y746"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><br/><span id="Y741"><span class="annot"><a href="X#Y741"><span class="annot"><a href="X#Y741"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#Y747"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y740"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y747"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="Y748"><span class="annot"><a href="X#Y748"><span class="annot"><a href="X#Y748"><span class="ju-function">fib</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">→</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y124"><span class="ju-constructor">zero</span></a></span> <span id="Y751"><span class="annot"><a href="X#Y751"><span class="annot"><a href="X#Y751"><span class="ju-var">x1</span></a></span></a></span></span> <span class="ju-keyword">_</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y751"><span class="ju-var">x1</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y125"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y752"><span class="annot"><a href="X#Y752"><span class="annot"><a href="X#Y752"><span class="ju-var">n</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span id="Y753"><span class="annot"><a href="X#Y753"><span class="annot"><a href="X#Y753"><span class="ju-var">x1</span></a></span></a></span></span> <span id="Y754"><span class="annot"><a href="X#Y754"><span class="annot"><a href="X#Y754"><span class="ju-var">x2</span></a></span></a></span></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y748"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y752"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y754"><span class="ju-var">x2</span></a></span> <span class="annot"><a href="X#Y753"><span class="ju-var"><span class="ju-delimiter">(</span>x1</span></a></span> <span class="annot"><a href="X#Y517"><span class="ju-function">+</span></a></span> <span class="annot"><a href="X#Y754"><span class="ju-var">x2</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><br/><span id="Y749"><span class="annot"><a href="X#Y749"><span class="annot"><a href="X#Y749"><span class="ju-function">fibonacci</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#Y755"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y748"><span class="ju-function">fib</span></a></span> <span class="annot"><a href="X#Y755"><span class="ju-var">n</span></a></span> <span class="ju-number">0</span> <span class="ju-number">1</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
|
||||
Commands like `typecheck` and `compile` can be used with Juvix Markdown files.
|
||||
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="Y742"><span class="annot"><a href="X#Y742"><span class="annot"><a href="X#Y742"><span class="ju-function">main</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y714"><span class="ju-axiom">IO</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y719"><span class="ju-axiom">readLn</span></a></span> <span class="annot"><a href="X#Y727"><span class="ju-function"><span class="ju-delimiter">(</span>printNatLn</span></a></span> <span class="annot"><a href="X#Y188"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#Y741"><span class="ju-function">fibonacci</span></a></span> <span class="annot"><a href="X#Y188"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#Y551"><span class="ju-axiom">stringToNat</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span id="Y750"><span class="annot"><a href="X#Y750"><span class="annot"><a href="X#Y750"><span class="ju-function">main</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y722"><span class="ju-axiom">IO</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y727"><span class="ju-axiom">readLn</span></a></span> <span class="annot"><a href="X#Y735"><span class="ju-function"><span class="ju-delimiter">(</span>printNatLn</span></a></span> <span class="annot"><a href="X#Y200"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#Y749"><span class="ju-function">fibonacci</span></a></span> <span class="annot"><a href="X#Y200"><span class="ju-function">∘</span></a></span> <span class="annot"><a href="X#Y566"><span class="ju-axiom">stringToNat</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
|
||||
Other code blocks are not touched, e.g:
|
||||
|
||||
@ -57,8 +57,8 @@ We also use other markup for documentation such as:
|
||||
Initial function arguments that match variables or wildcards in all clauses can
|
||||
be moved to the left of the colon in the function definition. For example,
|
||||
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y751"><span class="annot"><a href="X#Y751"><span class="annot"><a href="X#Y751"><span class="ju-var">move-to-left</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span class="annot"><a href="X#Y506"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="Y748"><span class="annot"><a href="X#Y748"><span class="annot"><a href="X#Y748"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#Y749"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-></span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y112"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y749"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y750"><span class="annot"><a href="X#Y750"><span class="annot"><a href="X#Y750"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#Y748"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#Y749"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y750"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y759"><span class="annot"><a href="X#Y759"><span class="annot"><a href="X#Y759"><span class="ju-var">move-to-left</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span class="annot"><a href="X#Y512"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="Y756"><span class="annot"><a href="X#Y756"><span class="annot"><a href="X#Y756"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-delimiter">(</span><span class="annot"><a href="X#Y757"><span class="ju-var">n</span></a></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-></span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y124"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y757"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span class="annot"><a href="X#Y125"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y758"><span class="annot"><a href="X#Y758"><span class="annot"><a href="X#Y758"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y125"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#Y756"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#Y757"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y758"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
|
||||
is equivalent to
|
||||
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y756"><span class="annot"><a href="X#Y756"><span class="annot"><a href="X#Y756"><span class="ju-var">example-add</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span class="annot"><a href="X#Y506"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="Y752"><span class="annot"><a href="X#Y752"><span class="annot"><a href="X#Y752"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-></span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-></span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span id="Y753"><span class="annot"><a href="X#Y753"><span class="annot"><a href="X#Y753"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#Y112"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y753"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span id="Y754"><span class="annot"><a href="X#Y754"><span class="annot"><a href="X#Y754"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#Y113"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y755"><span class="annot"><a href="X#Y755"><span class="annot"><a href="X#Y755"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y113"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#Y752"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#Y754"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y755"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
<pre class="highlight"><code class="juvix"><pre class="src-content"><span class="ju-keyword">module</span> <span id="Y764"><span class="annot"><a href="X#Y764"><span class="annot"><a href="X#Y764"><span class="ju-var">example-add</span></a></span></a></span></span><span class="ju-delimiter">;</span><br/> <span class="ju-keyword">import</span> <span class="annot"><a href="X#Y512"><span class="ju-var">Stdlib<span class="ju-delimiter">.</span>Data<span class="ju-delimiter">.</span>Nat</span></a></span> <span class="ju-keyword">open</span><span class="ju-delimiter">;</span><br/> <span id="Y760"><span class="annot"><a href="X#Y760"><span class="annot"><a href="X#Y760"><span class="ju-function"><br/> add</span></a></span></a></span></span> <span class="ju-keyword">:</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-></span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-></span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span><br/> <span class="ju-keyword">|</span> <span id="Y761"><span class="annot"><a href="X#Y761"><span class="annot"><a href="X#Y761"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#Y124"><span class="ju-constructor">zero</span></a></span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y761"><span class="ju-var">n</span></a></span><br/> <span class="ju-keyword">|</span> <span id="Y762"><span class="annot"><a href="X#Y762"><span class="annot"><a href="X#Y762"><span class="ju-var">n</span></a></span></a></span></span> <span class="annot"><a href="X#Y125"><span class="ju-constructor"><span class="ju-delimiter">(</span>suc</span></a></span> <span id="Y763"><span class="annot"><a href="X#Y763"><span class="annot"><a href="X#Y763"><span class="ju-var">m</span></a></span></a></span></span><span class="ju-delimiter">)</span> <span class="ju-keyword">:=</span> <span class="annot"><a href="X#Y125"><span class="ju-constructor">suc</span></a></span> <span class="annot"><a href="X#Y760"><span class="ju-function"><span class="ju-delimiter">(</span>add</span></a></span> <span class="annot"><a href="X#Y762"><span class="ju-var">n</span></a></span> <span class="annot"><a href="X#Y763"><span class="ju-var">m</span></a></span><span class="ju-delimiter">)</span><span class="ju-delimiter">;</span><br/><span class="ju-keyword">end</span><span class="ju-delimiter">;</span></pre></code></pre>
|
||||
|
Loading…
Reference in New Issue
Block a user