Skip to content

Commit

Permalink
Merge pull request #1521 from GaloisInc/instance-doc
Browse files Browse the repository at this point in the history
Document the classes that inhabit the various overloading classes.
  • Loading branch information
yav authored May 24, 2023
2 parents 7585094 + 90585dc commit db557b4
Show file tree
Hide file tree
Showing 36 changed files with 15,297 additions and 2,820 deletions.
149 changes: 149 additions & 0 deletions docs/RefMan/OverloadedOperations.rst
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,28 @@ Equality
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``Integer``
-
* - ``Rational``
-
* - ``Z n``
- ``fin n``, ``n >= 1``
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] a``
- ``fin n``, ``Eq a``
* - ``(a,b)``
- ``Eq a``, ``Eq b``



Comparisons
-----------

Expand All @@ -27,6 +49,27 @@ Comparisons
abs : {a} (Cmp a, Ring a) => a -> a
.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``Integer``
-
* - ``Rational``
-
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] a``
- ``fin n``, ``Cmp a``
* - ``(a,b)``
- ``Cmp a``, ``Cmp b``





Signed Comparisons
------------------

Expand All @@ -38,6 +81,17 @@ Signed Comparisons
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit
.. list-table:: Instances

* - Type
- Condition
* - ``[n] Bit``
- ``fin n``, ``n >= 1``
* - ``[n] a``
- ``fin n``, ``SignedCmp a``, ``a /= Bit``
* - ``(a,b)``
- ``SignedCmp a``, ``SignedCmp b``


Zero
----
Expand All @@ -47,6 +101,27 @@ Zero
Zero
zero : {a} (Zero a) => a
.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``Integer``
-
* - ``Rational``
-
* - ``Z n``
- ``fin n``, ``n >= 1``
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] a``
- ``Zero a``
* - ``a -> b``
- ``Zero b``
* - ``(a,b)``
- ``Zero a``, ``Zero b``

Logical Operations
------------------

Expand All @@ -58,6 +133,21 @@ Logical Operations
(^) : {a} (Logic a) => a -> a -> a
complement : {a} (Logic a) => a -> a
.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``[n] a``
- ``Logic a``
* - ``a -> b``
- ``Logic b``
* - ``(a,b)``
- ``Logic a``, ``Logic b``



Basic Arithmetic
----------------

Expand All @@ -71,6 +161,29 @@ Basic Arithmetic
negate : {a} (Ring a) => a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a
.. list-table:: Instances

* - Type
- Condition
* - ``Integer``
-
* - ``Rational``
-
* - ``Z n``
- ``fin n``, ``n >= 1``
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] Bit``
- ``fin n``
* - ``[n] a``
- ``Ring a``, ``a /= Bit``
* - ``a -> b``
- ``Ring b``
* - ``(a,b)``
- ``Ring a``, ``Ring b``



Integral Operations
-------------------

Expand All @@ -84,6 +197,18 @@ Integral Operations
infFrom : {a} (Integral a) => a -> [inf]a
infFromThen : {a} (Integral a) => a -> a -> [inf]a
.. list-table:: Instances

* - Type
- Condition
* - ``Integer``
-
* - ``[n] Bit``
- ``fin n``





Division
--------
Expand All @@ -94,6 +219,20 @@ Division
recip : {a} (Field a) => a -> a
(/.) : {a} (Field a) => a -> a -> a
.. list-table:: Instances

* - Type
- Condition
* - ``Rational``
-
* - ``Z n``
- ``prime n``
* - ``Float e p``
- ``ValidFloat e p``



Rounding
--------

Expand All @@ -105,3 +244,13 @@ Rounding
trunc : {a} (Round a) => a -> Integer
roundAway : {a} (Round a) => a -> Integer
roundToEven : {a} (Round a) => a -> Integer
.. list-table:: Instances

* - Type
- Condition
* - ``Float e p``
- ``ValidFloat e p``


Binary file modified docs/RefMan/_build/doctrees/BasicSyntax.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/BasicTypes.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/Expressions.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/FFI.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/Modules.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/OverloadedOperations.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/RefMan.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/TypeDeclarations.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/environment.pickle
Binary file not shown.
2 changes: 1 addition & 1 deletion docs/RefMan/_build/html/.buildinfo
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: 69485412ee215e2257ea16f8a42506fe
config: 49d6d89345e8bba027ef627e0adeb689
tags: 645f666f9bcd5a90fca523b33c5a78b7
Loading

0 comments on commit db557b4

Please sign in to comment.