-
Notifications
You must be signed in to change notification settings - Fork 11
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
the-blarney-fairy
committed
Oct 2, 2024
0 parents
commit 527be97
Showing
113 changed files
with
3,008 additions
and
0 deletions.
There are no files selected for viewing
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,28 @@ | ||
| <!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><meta name="viewport" content="width=device-width, initial-scale=1" /><title>Blarney.Backend.SMT.BasicDefinitions</title><link href="linuwial.css" rel="stylesheet" type="text/css" title="Linuwial" /><link rel="stylesheet" type="text/css" href="quick-jump.css" /><link rel="stylesheet" type="text/css" href="https://fonts.googleapis.com/css?family=PT+Sans:400,400i,700" /><script src="haddock-bundle.min.js" async="async" type="text/javascript"></script><script type="text/x-mathjax-config">MathJax.Hub.Config({ tex2jax: { processClass: "mathjax", ignoreClass: ".*" } });</script><script src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/MathJax.js?config=TeX-AMS-MML_HTMLorMML" type="text/javascript"></script></head><body><div id="package-header"><span class="caption">blarney-0.1.0.0</span><ul class="links" id="page-menu"><li><a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul></div><div id="content"><div id="module-header"><table class="info"><tr><th valign="top">Copyright</th><td>(c) Alexandre Joannou 2020-2021</td></tr><tr><th>License</th><td>MIT</td></tr><tr><th>Stability</th><td>experimental</td></tr><tr><th>Safe Haskell</th><td>Safe-Inferred</td></tr><tr><th>Language</th><td>GHC2021</td></tr></table><p class="caption">Blarney.Backend.SMT.BasicDefinitions</p></div><div id="table-of-contents"><div id="contents-list"><p class="caption" onclick="window.scrollTo(0,0)">Contents</p><ul><li><a href="#g:1">datatypes declaration</a></li><li><a href="#g:2">list creation</a></li><li><a href="#g:3">list reduction</a></li><li><a href="#g:4">miscellaneous</a></li></ul></div></div><div id="description"><p class="caption">Description</p><div class="doc"><p>This module provides basic SMT types and functions to assist in blarney Netlist | ||
| code generation</p></div></div><div id="synopsis"><details id="syn"><summary>Synopsis</summary><ul class="details-toggle" data-details-id="syn"><li class="src short"><a href="#v:declareTupleTypes">declareTupleTypes</a> :: [<a href="Blarney-Prelude.html#t:Int" title="Blarney.Prelude">Int</a>] -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li><li class="src short"><a href="#v:declareListXType">declareListXType</a> :: <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li><li class="src short"><a href="#v:mkListX">mkListX</a> :: [<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>] -> <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a> -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li><li class="src short"><a href="#v:defineAndReduce">defineAndReduce</a> :: <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li><li class="src short"><a href="#v:defineImpliesReduce">defineImpliesReduce</a> :: <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li><li class="src short"><a href="#v:defineDistinctListX">defineDistinctListX</a> :: <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a> -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li><li class="src short"><a href="#v:defineChain">defineChain</a> :: <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a> -> (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>), <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>) -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li><li class="src short"><a href="#v:inlineChain">inlineChain</a> :: <a href="Blarney-Prelude.html#t:Int" title="Blarney.Prelude">Int</a> -> (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>), <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>) -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a></li></ul></details></div><div id="interface"><a href="#g:1" id="g:1"><h1>datatypes declaration</h1></a><div class="top"><p class="src"><a id="v:declareTupleTypes" class="def">declareTupleTypes</a> :: [<a href="Blarney-Prelude.html#t:Int" title="Blarney.Prelude">Int</a>] -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L39" class="link">Source</a> <a href="#v:declareTupleTypes" class="selflink">#</a></p><div class="doc"><p>Declare an SMT tuple sort per entry in the argument list. Each sort is | ||
| defined as a function of the <code><a href="Blarney-Prelude.html#t:Int" title="Blarney.Prelude">Int</a></code> <a href="N.html">N</a>, as the parametric sort <a href="TupleN.html">TupleN</a> | ||
| parameterised on <a href="X.html">X</a>, and a constructor "mkTupleN" with N fields named | ||
| "tplN_i" for i ranging from 1 to N</p></div></div><div class="top"><p class="src"><a id="v:declareListXType" class="def">declareListXType</a> :: <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L51" class="link">Source</a> <a href="#v:declareListXType" class="selflink">#</a></p><div class="doc"><p>Declare a <a href="ListX.html">ListX</a> parametric Sort parameterised on <a href="X.html">X</a> with 2 constructors: | ||
| * a "nil" constructor | ||
| * a "cons" constructor with 2 fields: | ||
| + "head" of sort <a href="X.html">X</a> | ||
| + "tail" of sort "(ListX X)"</p></div></div><a href="#g:2" id="g:2"><h1>list creation</h1></a><div class="top"><p class="src"><a id="v:mkListX" class="def">mkListX</a> :: [<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>] -> <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a> -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L59" class="link">Source</a> <a href="#v:mkListX" class="selflink">#</a></p><div class="doc"><p>Construct a ListX from a '[Sting]' by chaining the appropriate sequence of | ||
| "cons" and a "nil" adequately qualified</p></div></div><a href="#g:3" id="g:3"><h1>list reduction</h1></a><div class="top"><p class="src"><a id="v:defineAndReduce" class="def">defineAndReduce</a> :: <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L65" class="link">Source</a> <a href="#v:defineAndReduce" class="selflink">#</a></p><div class="doc"><p>Define the "andReduce" SMT function operating on a "(ListX Bool)", | ||
| reducing it using "and"</p></div></div><div class="top"><p class="src"><a id="v:defineImpliesReduce" class="def">defineImpliesReduce</a> :: <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L80" class="link">Source</a> <a href="#v:defineImpliesReduce" class="selflink">#</a></p><div class="doc"><p>Define the "impliesReduce" SMT function operating on a "(ListX Bool)", | ||
| reducing it using "=>" (implication)</p></div></div><div class="top"><p class="src"><a id="v:defineDistinctListX" class="def">defineDistinctListX</a> :: <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a> -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L103" class="link">Source</a> <a href="#v:defineDistinctListX" class="selflink">#</a></p><div class="doc"><p>Define the "init", "allDifferent" and "distinctFrom" family of functions on | ||
| ListX parameterised on the provided sort. For a given sort S, the defined | ||
| functions are: | ||
| * "init_ListX_S" - return all but the last element of the list or nil for | ||
| an empty list | ||
| * "allDifferent_ListX_S" - return true if all elements of the list are | ||
| distinct | ||
| * "distinctFrom_ListX_S" - return true if the first argument is distinct | ||
| from all the elements in the second argument</p></div></div><a href="#g:4" id="g:4"><h1>miscellaneous</h1></a><div class="top"><p class="src"><a id="v:defineChain" class="def">defineChain</a> :: <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a> -> (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>), <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>) -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L146" class="link">Source</a> <a href="#v:defineChain" class="selflink">#</a></p><div class="doc"><p>Define the repeated application of a function f of 2 arguments returning a | ||
| pair where | ||
| * the first argument of f is taken from an overall argument list | ||
| * the second argument of f is an explicit argument of first invocation, and | ||
| is the second member of the pair returned by the previous invocation on | ||
| subsequent calls | ||
| * the call depth is defined by the length of the explicit argument list | ||
| * the overall return is a pair of reversed lists of individual returned | ||
| values</p></div></div><div class="top"><p class="src"><a id="v:inlineChain" class="def">inlineChain</a> :: <a href="Blarney-Prelude.html#t:Int" title="Blarney.Prelude">Int</a> -> (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, (<a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>, <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>), <a href="Blarney-Prelude.html#t:String" title="Blarney.Prelude">String</a>) -> <a href="file:///usr/local/.ghcup/ghc/9.2.1/share/doc/ghc-9.2.1/html/libraries/pretty-1.1.3.6/Text-PrettyPrint.html#t:Doc" title="Text.PrettyPrint">Doc</a> <a href="https://github.com/blarney-lang/blarney/tree/4f8a196bf4aaa57329aa44beaa6da18d6e3c1d48/Haskell/Blarney/Backend/SMT/BasicDefinitions.hs#L173" class="link">Source</a> <a href="#v:inlineChain" class="selflink">#</a></p><div class="doc"><p>Inlined chaining (avoiding recursion in SMT output)</p></div></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.26.0</p></div></body></html> |
Oops, something went wrong.