Skip to content

Commit

Permalink
[ docs ] CI docs generation
Browse files Browse the repository at this point in the history
  • Loading branch information
github-actions[bot] committed Mar 6, 2025
1 parent 448cf19 commit f077b25
Show file tree
Hide file tree
Showing 16 changed files with 1,397 additions and 1,356 deletions.

Large diffs are not rendered by default.

21 changes: 11 additions & 10 deletions docs/deptycheck/docs/docs/Deriving.DepTyCheck.Gen.Checked.src.html

Large diffs are not rendered by default.

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -61,4 +61,4 @@
</script>

</header>
<div class="container"><div id="module-header"><h1>Deriving.DepTyCheck.Gen.Core.Util</h1><span style="float:right">(<a href="Deriving.DepTyCheck.Gen.Core.Util.src.html">source</a>)</span><pre></pre></div><h2>Reexports</h2><code><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Data.Fin.Split<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Decidable.Equality<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Gen.Derive</code><h2>Definitions</h2><dl class="decls"><dt id="Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><code><span class="keyword">data</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;:&ensp;<span class="name type">Type</span></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span><br> <b>Constructors</b>:<br><dl class="decls"> <dt id="Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><span class="name constructor">DeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt> <dt id="Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><span class="name constructor">NotDeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl><br> <b>Hints</b>:<br><dl class="decls"> <dt id="$resolved16512"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt> <dt id="$resolved16511"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span></code></dt> <dt id="$resolved16510"><code><span class="type resolved" title="Prelude.Interfaces.Monoid"><span class="name type">Monoid</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt> <dt id="$resolved16509"><code><span class="type resolved" title="Prelude.Interfaces.Semigroup"><span class="name type">Semigroup</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><span class="name function">BindExprFun</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Types.Nat"><span class="name type">Nat</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><span class="name function">analyseDeepConsApp</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Util.Reflection.html#Deriving.DepTyCheck.Util.Reflection.NamesInfoInTypes"><span class="name type">NamesInfoInTypes</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;(<span class="boundvar">collectConsDetermInfo</span>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Data.SortedSet.SortedSet"><span class="name type">SortedSet</span></span>&ensp;<span class="type resolved" title="Language.Reflection.TT.Name"><span class="name type">Name</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Language.Reflection.TTImp.TTImp"><span class="name type">TTImp</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Prelude.Types.Either"><span class="name type">Either</span></span>&ensp;<span class="name type">String</span>&ensp;(<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;<span class="boundvar">collectConsDetermInfo</span>)</code></dt><dd><pre> Analyses whether the given expression can be an expression of free variables applied (maybe deeply) to a number of data constructors.<br> <br> Returns which of given free names are actually used in the given expression, in order of appearance in the expression.<br> Notice that applied free names may repeat as soon as one name is used several times in the given expression.<br> <br> Also, a function returning a bind expression (an expression replacing all free names with bind names (`IBindVar`))<br> is also returned.<br> This function requires bind variable names as input.<br> It returns correct bind expression only when all given bind names are different.</pre><br> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd></dl></div><footer>Produced by Idris 2 version 0.7.0-1678b4676</footer></body></html>
<div class="container"><div id="module-header"><h1>Deriving.DepTyCheck.Gen.Core.Util</h1><span style="float:right">(<a href="Deriving.DepTyCheck.Gen.Core.Util.src.html">source</a>)</span><pre></pre></div><h2>Reexports</h2><code><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Data.Fin.Split<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Decidable.Equality<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Gen.Derive</code><h2>Definitions</h2><dl class="decls"><dt id="Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><code><span class="keyword">data</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;:&ensp;<span class="name type">Type</span></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span><br> <b>Constructors</b>:<br><dl class="decls"> <dt id="Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeterminedByType"><span class="name constructor">DeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt> <dt id="Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.NotDeterminedByType"><span class="name constructor">NotDeterminedByType</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl><br> <b>Hints</b>:<br><dl class="decls"> <dt id="$resolved16515"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt> <dt id="$resolved16514"><code><span class="type resolved" title="Prelude.Cast.Cast"><span class="name type">Cast</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a>&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span></code></dt> <dt id="$resolved16513"><code><span class="type resolved" title="Prelude.Interfaces.Monoid"><span class="name type">Monoid</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt> <dt id="$resolved16512"><code><span class="type resolved" title="Prelude.Interfaces.Semigroup"><span class="name type">Semigroup</span></span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.ConsDetermInfo"><span class="name type">ConsDetermInfo</span></a></code></dt></dl></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.BindExprFun"><span class="name function">BindExprFun</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Types.Nat"><span class="name type">Nat</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.analyseDeepConsApp"><span class="name function">analyseDeepConsApp</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Util.Reflection.html#Deriving.DepTyCheck.Util.Reflection.NamesInfoInTypes"><span class="name type">NamesInfoInTypes</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;(<span class="boundvar">collectConsDetermInfo</span>&ensp;:&ensp;<span class="type resolved" title="Prelude.Basics.Bool"><span class="name type">Bool</span></span>)&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Data.SortedSet.SortedSet"><span class="name type">SortedSet</span></span>&ensp;<span class="type resolved" title="Language.Reflection.TT.Name"><span class="name type">Name</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Language.Reflection.TTImp.TTImp"><span class="name type">TTImp</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Prelude.Types.Either"><span class="name type">Either</span></span>&ensp;<span class="name type">String</span>&ensp;(<a class="type" href="Deriving.DepTyCheck.Gen.Core.Util.html#Deriving.DepTyCheck.Gen.Core.Util.DeepConsAnalysisRes"><span class="name function">DeepConsAnalysisRes</span></a>&ensp;<span class="boundvar">collectConsDetermInfo</span>)</code></dt><dd><pre> Analyses whether the given expression can be an expression of free variables applied (maybe deeply) to a number of data constructors.<br> <br> Returns which of given free names are actually used in the given expression, in order of appearance in the expression.<br> Notice that applied free names may repeat as soon as one name is used several times in the given expression.<br> <br> Also, a function returning a bind expression (an expression replacing all free names with bind names (`IBindVar`))<br> is also returned.<br> This function requires bind variable names as input.<br> It returns correct bind expression only when all given bind names are different.</pre><br> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd></dl></div><footer>Produced by Idris 2 version 0.7.0-1678b4676</footer></body></html>
Original file line number Diff line number Diff line change
Expand Up @@ -62,4 +62,4 @@

</header>
<div class="container"><div id="module-header"><h1>Deriving.DepTyCheck.Gen.Core</h1><span style="float:right">(<a href="Deriving.DepTyCheck.Gen.Core.src.html">source</a>)</span><pre>Main implementation of the derivator core interface
</pre></div><h2>Reexports</h2><code><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Gen.Core.ConsEntry<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Util.Reflection</code><h2>Definitions</h2><dl class="decls"><dt id="Deriving.DepTyCheck.Gen.Core.ProbabilityTuning"><code><span class="keyword">interface</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.ProbabilityTuning"><span class="name type">ProbabilityTuning</span></a>&ensp;:&ensp;<span class="type resolved" title="Language.Reflection.TT.Name"><span class="name type">Name</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="name type">Type</span></code></dt><dd> <b>Parameters</b>:&ensp;n<br><b>Methods</b>:<br><dl class="decls"> <dt id="Deriving.DepTyCheck.Gen.Core.isConstructor"><code><span class="keyword">0</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.isConstructor"><span class="name function">isConstructor</span></a>&ensp;:&ensp;(<span class="boundvar">con</span>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Util.Reflection.html#Deriving.DepTyCheck.Util.Reflection.IsConstructor"><span class="name type">IsConstructor</span></a>&ensp;<span class="boundvar">n</span>&ensp;<span class="keyword">**</span>&ensp;<span class="type resolved" title="Deriving.DepTyCheck.Util.Reflection.IsConstructor.GenuineProof"><span class="name type">GenuineProof</span></span>&ensp;<span class="boundvar">con</span>)</code></dt> <dt id="Deriving.DepTyCheck.Gen.Core.tuneWeight"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.tuneWeight"><span class="name function">tuneWeight</span></a>&ensp;:&ensp;<span class="type resolved" title="Data.Nat1.Nat1"><span class="name type">Nat1</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Data.Nat1.Nat1"><span class="name type">Nat1</span></span></code></dt></dl></dd><dt id="Deriving.DepTyCheck.Gen.Core.isConstructor"><code><span class="keyword">0</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.isConstructor"><span class="name function">isConstructor</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.ProbabilityTuning"><span class="name type">ProbabilityTuning</span></a>&ensp;<span class="boundvar">n</span>&ensp;<span class="keyword">=&gt;</span>&ensp;(<span class="boundvar">con</span>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Util.Reflection.html#Deriving.DepTyCheck.Util.Reflection.IsConstructor"><span class="name type">IsConstructor</span></a>&ensp;<span class="boundvar">n</span>&ensp;<span class="keyword">**</span>&ensp;<span class="type resolved" title="Deriving.DepTyCheck.Util.Reflection.IsConstructor.GenuineProof"><span class="name type">GenuineProof</span></span>&ensp;<span class="boundvar">con</span>)</code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Deriving.DepTyCheck.Gen.Core.tuneWeight"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.tuneWeight"><span class="name function">tuneWeight</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.ProbabilityTuning"><span class="name type">ProbabilityTuning</span></a>&ensp;<span class="boundvar">n</span>&ensp;<span class="keyword">=&gt;</span>&ensp;<span class="type resolved" title="Data.Nat1.Nat1"><span class="name type">Nat1</span></span>&ensp;<span class="keyword">-&gt;</span>&ensp;<span class="type resolved" title="Data.Nat1.Nat1"><span class="name type">Nat1</span></span></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">public&ensp;export</span></dd><dt id="Deriving.DepTyCheck.Gen.Core.MainCoreDerivator"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.MainCoreDerivator"><span class="name function">MainCoreDerivator</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.ConsDerive.html#Deriving.DepTyCheck.Gen.Core.ConsDerive.ConstructorDerivator"><span class="name type">ConstructorDerivator</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Derive.html#Deriving.DepTyCheck.Gen.Derive.DerivatorCore"><span class="name type">DerivatorCore</span></a></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd></dl></div><footer>Produced by Idris 2 version 0.7.0-1678b4676</footer></body></html>
</pre></div><h2>Reexports</h2><code><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Gen.Core.ConsEntry<br><span class="keyword">import</span>&ensp;<span class="keyword">public</span>&ensp;Deriving.DepTyCheck.Util.Reflection</code><h2>Definitions</h2><dl class="decls"><dt id="Deriving.DepTyCheck.Gen.Core.MainCoreDerivator"><code><a class="type" href="Deriving.DepTyCheck.Gen.Core.html#Deriving.DepTyCheck.Gen.Core.MainCoreDerivator"><span class="name function">MainCoreDerivator</span></a>&ensp;:&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Core.ConsDerive.html#Deriving.DepTyCheck.Gen.Core.ConsDerive.ConstructorDerivator"><span class="name type">ConstructorDerivator</span></a>&ensp;<span class="keyword">=&gt;</span>&ensp;<a class="type" href="Deriving.DepTyCheck.Gen.Derive.html#Deriving.DepTyCheck.Gen.Derive.DerivatorCore"><span class="name type">DerivatorCore</span></a></code></dt><dd> <b>Totality</b>:&ensp;<span class="keyword">total</span><br> <b>Visibility</b>:&ensp;<span class="keyword">export</span></dd></dl></div><footer>Produced by Idris 2 version 0.7.0-1678b4676</footer></body></html>
Loading

0 comments on commit f077b25

Please sign in to comment.