Skip to content

Commit

Permalink
Update to the latest juvix-stdlib (#2546)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@paulcadman
paulcadman committed Dec 1, 2023
1 parent c237f29 commit 77b29c6
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 6 deletions.
2 changes: 1 addition & 1 deletion juvix-stdlib
Submodule juvix-stdlib updated 18 files
+9 −0 Package.juvix
+1 −6 Stdlib/Data/Bool/Base.juvix
+1 −21 Stdlib/Data/Fixity.juvix
+1 −10 Stdlib/Data/List/Base.juvix
+1 −5 Stdlib/Data/Maybe/Base.juvix
+1 −11 Stdlib/Data/Nat.juvix
+1 −45 Stdlib/Data/Nat/Base.juvix
+1 −2 Stdlib/Data/Range.juvix
+0 −1 Stdlib/Data/String.juvix
+1 −9 Stdlib/Data/String/Base.juvix
+1 −2 Stdlib/Extra/Gcd.juvix
+0 −1 Stdlib/System/IO/Base.juvix
+1 −17 Stdlib/Trait/Natural.juvix
+0 −3 juvix.yaml
+10 −0 test/Package.juvix
+18 −7 test/Test.juvix
+8 −6 test/juvix.lock.yaml
+0 −8 test/juvix.yaml
2 changes: 1 addition & 1 deletion package.yaml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions test/BackendMarkdown/Positive.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
8 changes: 4 additions & 4 deletions tests/positive/Markdown/markdown/Test.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down Expand Up @@ -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">-&gt;</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">-&gt;</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">-&gt;</span> <span class="annot"><a href="X#Y111"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</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">-&gt;</span> <span class="annot"><a href="X#Y123"><span class="ju-inductive">Nat</span></a></span> <span class="ju-keyword">-&gt;</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>

0 comments on commit 77b29c6

Please sign in to comment.