Skip to content

bmorphism/geb

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2,008 Commits
.github/workflows
.github/workflows
 
 
docs
docs
 
 
geb-agda
geb-agda
 
 
geb-idris
geb-idris
 
 
src
src
 
 
test
test
 
 
.gitignore
.gitignore
 
 
CHANGELOG.org
CHANGELOG.org
 
 
LICENSE
LICENSE
 
 
Makefile
Makefile
 
 
README
README
 
 
README.md
README.md
 
 
geb.asd
geb.asd
 
 

Repository files navigation

The GEB Manual

Table of Contents

[in package GEB-DOCS/DOCS]

Welcome to the GEB project.

1 Links

Here is the official repository

and HTML documentation for the latest version.

1.1 code coverage

For test coverage it can be found at the following links:

SBCL test coverage

CCL test coverage: current under maintenance

Note that due to #34 CCL tests are not currently displaying

I recommend reading the CCL code coverage version, as it has proper tags.

Currently they are manually generated, and thus for a more accurate assessment see GEB-TEST:CODE-COVERAGE

2 Getting Started

Welcome to the GEB Project!

2.1 installation

This project uses common lisp, so a few dependencies are needed to get around the code-base and start hacking. Namely:

  1. lisp with quicklisp.

  2. Emacs along with one of the following:

2.2 loading

Now that we have an environment setup, we can load the project, this can be done in a few steps.

  1. Open the REPL (sbcl (terminal), M-x sly, M-x swank)

    • For the terminal, this is just calling the common lisp implementation from the terminal.

      user@system:geb-directory % sbcl.

    • For Emacs, this is simply calling either M-x sly or M-x slime if you are using either sly or slime

  2. From Emacs: open geb.asd and press C-ck (sly-compile-and-load-file, or swank-compile-and-load-file if you are using swank).

Now that we have the file open, we can now load the system by writing:

;; only necessary for the first time!
(ql:quickload :geb/documentation)

;; if you want to load it in the future
(asdf:load-system :geb/documentation)

;; if you want to load the codbase and run tests at the same time
(asdf:test-system :geb/documentation)

;; if you want to run the tests once the system is loaded!
(geb-test:run-tests)

2.3 Geb as a binary

[in package GEB.ENTRY]

The standard way to use geb currently is by loading the code into one's lisp environment

(ql:quickload :geb)

However, one may be interested in running geb in some sort of compilation process, that is why we also give out a binary for people to use

An example use of this binary is as follows

mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.spec::*entry*" -l -v -o "foo.pir"

mariari@Gensokyo % cat foo.pir
def *entry* x {
  0
}%
mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.spec::*entry*" -l -v
def *entry* x {
  0
}

./geb.image -h
  -i --input                      string   Input geb file location
  -e --entry-point                string   The function to run, should be fully qualified I.E.
                                           geb::my-main
  -l --stlc                       boolean  Use the simply typed lambda calculus frontend
  -o --output                     string   Save the output to a file rather than printing
  -v --vampir                     string   Return a vamp-ir expression
  -h -? --help                    boolean  The current help message

starting from a file foo.lisp that has

(in-package :geb.lambda.spec)

(defparameter *entry*
  (typed unit geb:so1))

inside of it.

The command needs an entry-point (-e or --entry-point), as we are simply call LOAD on the given file, and need to know what to translate.

from STLC, we expect the form to be wrapped in the GEB.LAMBDA.SPEC.TYPED which takes both the type and the value to properly have enough context to evaluate.

It is advised to bind this to a parameter like in our example as -e expects a symbol.

the -l flag means that we are not expecting a geb term, but rather a lambda frontend term, this is to simply notify us to compile it as a lambda term rather than a geb term. In time this will go away

  • [function] COMPILE-DOWN &KEY VAMPIR STLC ENTRY (STREAM *STANDARD-OUTPUT*)

3 Glossary

  • [glossary-term] closed type

    A closed type is a type that can not be extended dynamically. A good example of this kind of term is an ML ADT.

    data Tree = Empty
          | Leaf Int
          | Node Tree Tree

    In our lisp code we have a very similar convention:

    (in-package :geb.spec)

(deftype substmorph ()
  `(or substobj
       alias
       comp init terminal case pair distribute
       inject-left inject-right
       project-left project-right))

    This type is closed, as only one of GEB:SUBSTOBJ, GEB:INJECT-LEFT, GEB:INJECT-RIGHT etc can form the GEB:SUBSTMORPH type.

    The main benefit of this form is that we can be exhaustive over what can be found in GEB:SUBSTMORPH.

    (defun so-hom-obj (x z)
  (match-of substobj x
    (so0          so1)
    (so1          z)
    (alias        (so-hom-obj (obj x) z))
    ((coprod x y) (prod (so-hom-obj x z)
                        (so-hom-obj y z)))
    ((prod x y)   (so-hom-obj x (so-hom-obj y z)))))

    If we forget a case, like GEB:COPROD it wanrs us with an non exhaustion warning.

    Meaning that if we update definitions this works well.

    The main downside is that we can not extend the type after the fact, meaning that all interfaces on SO-HOM-OBJ must take the unaltered type. This is in stark contrast to open types. To find out more about the trade offs and usage in the code-base read the section Open Types versus Closed Types.

  • [glossary-term] open type

    An open type is a type that can be extended by user code down the line. A good example of this in ML is the type class system found in Haskell.

    In our code base, it is simple as creating a Common Lisp Object System (CLOS) term

    (defclass <substobj> (direct-pointwise-mixin) ())

    and to create a child of it all we need to do is.

    (defclass so0 (<substobj>) ())

    Now any methods on GEB:<SUBSTOBJ> will cover GEB:SO0(0 1).

    The main disadvantage of these is that exhaustion can not be checked, and thus the user has to know what methods to fill out. In a system with a bit more checks this is not a problem in practice. To find out more about the trade offs and usage in the code-base read the section Open Types versus Closed Types.

  • [glossary-term] Common Lisp Object System (CLOS)

    The object system found in CL. Has great features like a Meta Object Protocol that helps it facilitate extensions.

4 Original Efforts

Originally GEB started off as an Idris codebase written by the designer and creator of GEB, Terence Rokop, However further efforts spawned for even further formal verification by Artem Gureev. Due to this, we have plenty of code not in Common Lisp that ought to be a good read.

4.1 Geb's Idris Code

The Idris folder can be found in the geb-idris folder provided in the codebase

At the time of this document, there is over 16k lines of Idris code written. This serves as the bulk of the POC that is GEB and is a treasure trove of interesting information surrounding category theory.

4.2 Geb's Agda Code

The Agda folder can be found in the geb-agda folder provided in the codebase

The Agda codebase serves as a great place to view formally verified properties about the GEB project. Although Geb's Idris Code is written in a dependently typed language, it serves as reference example of GEB, while Geb's Agda Code serves as the mathematical formalism proving various conjectures about GEB

5 Categorical Model

Geb is organizing programming language concepts (and entities!) using category theory, originally developed by mathematicians, but very much alive in programming language theory. Let us look at a simple well-known example: the category of sets and functions. It is the bread and butter example: sets $A,B,C,…$ play the role of objects, functions are arrows between objects $A—f→B$, and the latter compose as functions do, such that every path of matching functions $$A—f→B—g→C—h→D$$ composes to a corresponding composite function $$A—f;g;h→D$$ (or $h∘g∘f$ if you prefer) and we enjoy the luxury of not having to worry about the order in which we compose; for the sake of completeness, there are identify functions $A —\mathrm{id}_A→ A$ on each set $A$, serving as identities (which correspond to the composite of the empty path on an object). Sets and functions together form a category—based on function composition; thus, let's call this category sets-'n'-functions. This example, even “restricted” to finite sets-'n'-functions, will permeate through Geb.

One of the first lessons (in any introduction to category theory) about sets-'n'-functions is the characterization of products and disjoint sums of sets in terms of functions alone, i.e., without ever talking about elements of sets. Products and co-products are the simplest examples of universal constructions. One of the first surprises follows suit when we generalize functions to partial functions, relations, or even multi-relations: we obtain very different categories! For example, in the category sets-'n'-relations, the disjoint union of sets features as both a product and a co-product, as a categorical construction.

Do not fear! The usual definition of products in terms of elements of sets are absolutely compatible with the universal construction in sets-'n'-functions. However we gain the possibility to compare the “result” of the universal constructions in sets-'n'-functions with the one in sets-'n'-relations (as both actually do have products).

for the purposes of Geb, many things can be expressed in analogy to the category of sets-'n'-functions; thus a solid understanding of the latter will be quite useful. In particular, we shall rely on the following universal constructions:

  1. The construction of binary products $A × B$ of sets $A,B$, and the empty product $\mathsf{1}$.

  2. The construction of “function spaces” $B^A$ of sets $A,B$, called exponentials, i.e., collections of functions between pairs of sets.

  3. The so-called currying of functions, $C^{(B^A)} \cong C^{(A × B)}$, such that providing several arguments to a function can done either simultaneously, or in sequence.

  4. The construction of sums (a.k.a. co-products) $A + B$ of sets $A,B$, corresponding to forming disjoint unions of sets; the empty sum is $\varnothing$.

Product, sums and exponentials are the (almost) complete tool chest for writing polynomial expressions, e.g., $$Ax^{\sf 2} +x^{\sf 1} - Dx^{\sf 0}.$$ (We need these later to define “algebraic data types”.) In the above expression, we have sets instead of numbers/constants where $ \mathsf{2} = \lbrace 1, 2 \rbrace$, $ \mathsf{1} = \lbrace 1 \rbrace$, $ \mathsf{0} = \lbrace \rbrace = \varnothing$, and $A$ and $B$ are arbitrary (finite) sets. We are only missing a counterpart for the variable! Raising an arbitrary set to “the power” of a constant set happens to have a very natural counterpart: the central actor of the most-well known fundamental result about categories, which generalizes Cayley's Theorem, i.e., the Yoneda embedding.

If you are familiar with the latter, buckle up and jump to Poly in Sets. Have a look at our streamlined account of The Yoneda Lemma if you are familiar with Cartesian closed categories, or take it slow and read up on the background in one of the classic or popular textbooks. Tastes tend to vary. However, Benjamin Pierce's Basic Category Theory for Computer Scientists deserves being pointed out as it is very amenable and covers the background we need in 60 short pages.

5.1 Morphisms

5.2 Objects

5.3 The Yoneda Lemma

5.4 Poly in Sets

6 Project Idioms and Conventions

The Geb Project is written in Common Lisp, which means the authors have a great choice in freedom in how the project is laid out and operates. In particular the style of Common Lisp here is a functional style with some OO idioms in the style of Smalltalk.

The subsections will outline many idioms that can be found throughout the codebase.

6.1 Spec Files, Main Files and Project Layout

[in package GEB.SPECS]

The codebase is split between many files. Each folder can be seen as a different idea within geb itself! Thus the poly has packages revolving around polynomials, the geb folder has packages regarding the main types of geb Subst Obj and Subst Morph, etc etc.

The general layout quirk of the codebase is that packages like geb.package.spec defines the specification for the base types for any category we wish to model, and these reside in the specs folder not in the folder that talks about the packages of those types. This is due to loading order issues, we thus load the specs packages before each of their surrounding packages, so that each package can built off the last. Further, packages like geb.package.main define out most of the functionality of the package to be used by other packages in geb.package, then all of these are reexported out in the geb.package package

Further to make working with each package of an idea is easy, we have the main package of the folder (typically named the same as the folder name) reexport most important components so if one wants to work with the fully fledged versions of the package they can simply without having to import too many packages at once.

For example, the geb.poly.spec defines out the types and data structures of the Polynomial Types, this is then rexported in geb.poly, giving the module geb.poly a convenient interface for all functions that operate on geb.poly.

6.2 Open Types versus Closed Types

closed type's and open type's both have their perspective tradeoff of openness versus exhaustiveness (see the linked articles for more on that). Due to this, they both have their own favorable applications. I would argue that a closed ADT type is great tool for looking at a function mathematically and treating the object as a whole rather than piecemeal. Whereas a more open extension is great for thinking about how a particular object/case behaves. They are different mindsets for different styles of code.

In the geb project, we have chosen to accept both styles, and allow both to coexist in the same setting. We have done this with a two part idiom.

(deftype substobj ()
  `(or alias prod coprod so0 so1))

(defclass <substobj> (direct-pointwise-mixin) ())

(defclass so0 (<substobj>) ...)

(defclass prod (<substobj>) ...)

The closed type is GEB:SUBSTOBJ, filling and defining every structure it knows about. This is a fixed idea that a programmer may statically update and get exhaustive warnings about. Whereas GEB:<SUBSTOBJ> is the open interface for the type. Thus we can view GEB:<SUBSTOBJ> as the general idea of a GEB:SUBSTOBJ. Before delving into how we combine these methods, let us look at two other benefits given by GEB:<SUBSTOBJ>

  1. We can put all the Mixins into the superclass to enforce that any type that extends it has the extended behaviors we wish. This is a great way to generically enhance the capabilities of the type without operating on it directly.

  2. We can dispatch on GEB:<SUBSTOBJ> since DEFMETHOD only works on Common Lisp Object System (CLOS) types and not generic types in CL.

Methods for closed and open types

With these pieces in play let us explore how we write a method in a way that is conducive to open and closed code.

(in-package :geb)

(defgeneric to-poly (morphism))

(defmethod to-poly ((obj <substmorph>))
  (typecase-of substmorph obj
    (alias        ...)
    (substobj     (error "Impossible")
    (init          0)
    (terminal      0)
    (inject-left   poly:ident)
    (inject-right  ...)
    (comp          ...)
    (case          ...)
    (pair          ...)
    (project-right ...)
    (project-left  ...)
    (distribute    ...)
    (otherwise (subclass-responsibility obj))))

(defmethod to-poly ((obj <substobj>))
  (declare (ignore obj))
  poly:ident)

In this piece of code we can notice a few things:

  1. We case on GEB:SUBSTMORPH exhaustively

  2. We cannot hit the GEB:<SUBSTOBJ> case due to method dispatch

  3. We have this GEB.UTILS:SUBCLASS-RESPONSIBILITY function getting called.

  4. We can write further methods extending the function to other subtypes.

Thus the GEB:TO-POLY function is written in such a way that it supports a closed definition and open extensions, with GEB.UTILS:SUBCLASS-RESPONSIBILITY serving to be called if an extension a user wrote has no handling of this method.

Code can also be naturally written in a more open way as well, by simply running methods on each class instead.

Potential Drawback and Fixes

One nasty drawback is that we can't guarantee the method exists. In java this can easily be done with interfaces and then enforcing they are fulfilled. Sadly CL has no such equivalent. However, this is all easily implementable. If this ever becomes a major problem, it is trivial to implement this by registering the subclasses, and the perspective methods, and scouring the image for instance methods, and computing if any parent class that isn't the one calling responsibility fulfills it. Thus, in practice, you should be able to ask the system if any particular extension fulfills what extension sets that the base object has and give CI errors if they are not fulfilled, thus enforcing closed behavior when warranted.

6.3 ≺Types≻

These refer to the open type variant to a closed type. Thus when one sees a type like GEB: it is the open version of GEB:SUBSTOBJ. Read Open Types versus Closed Types for information on how to use them.

7 The Geb Model

[in package GEB]

Everything here relates directly to the underlying machinery of GEB, or to abstractions that help extend it.

7.1 The Categorical Interface

[in package GEB.MIXINS]

This covers the main Categorical interface required to be used and contained in various data structures

  • [class] CAT-OBJ

    I offer the service of being a base category objects with no extesnions

  • [class] CAT-MORPH

    I offer the service of being a base categorical morphism with no extesnions

  • [generic-function] DOM CAT-MORPH

    Grabs the domain of the morphism. Returns a CAT-OBJ

  • [generic-function] CODOM CAT-MORPH

    Grabs the codomain of the morphism. Returns a CAT-OBJ

  • [generic-function] CURRY-PROD CAT-MORPH CAT-LEFT CAT-RIGHT

    Curries the given product type given the product. This returns a CAT-MORPH.

    This interface version takes the left and right product type to properly dispatch on. Instances should specalize on the CAT-RIGHT argument

    Use GEB.MAIN:CURRY instead.

7.2 Core Category

[in package GEB.SPEC]

The underlying category of GEB. With Subst Obj covering the shapes and forms (Objects) of data while Subst Morph deals with concrete Morphisms within the category.

From this category, most abstractions will be made, with SUBSTOBJ serving as a concrete type layout, with SUBSTMORPH serving as the morphisms between different SUBSTOBJ types. This category is equivalent to finset.

A good example of this category at work can be found within the Booleans section.

7.2.1 Subst Obj

This section covers the objects of the SUBSTMORPH category. Note that SUBSTOBJ refers to the closed type, whereas <SUBSTOBJ> refers to the open type that allows for user extension.

  • [type] SUBSTOBJ

SUBSTOBJ type is not a constructor itself, instead it's best viewed as the sum type, with the types below forming the constructors for the term. In ML we would write it similarly to:

type substobj = so0
              | so1
              | prod
              | coprod

  • [type] PROD

    The PRODUCT object. Takes two CAT-OBJ values that get put into a pair.

    The formal grammar of PRODUCT is

    (prod mcar mcadr)

    where PROD is the constructor, MCAR is the left value of the product, and MCADR is the right value of the product.

    Example:

    (geb-gui::visualize (prod geb-bool:bool geb-bool:bool))

    Here we create a product of two GEB-BOOL:BOOL types.

  • [type] COPROD

    the CO-PRODUCT object. Takes CAT-OBJ values that get put into a choice of either value.

    The formal grammar of PRODUCT is

    (coprod mcar mcadr)

    Where CORPOD is the constructor, MCAR is the left choice of the sum, and MCADR is the right choice of the sum.

    Example:

    (geb-gui::visualize (coprod so1 so1))

    Here we create the boolean type, having a choice between two unit values.

  • [type] SO0

    The Initial Object. This is sometimes known as the VOID type.

    the formal grammar of SO0 is

    so0

    where SO0 is THE initial object.

    Example

    lisp

  • [type] SO1

    The Terminal Object. This is sometimes referred to as the Unit type.

    the formal grammar or SO1 is

    so1

    where SO1 is THE terminal object

    Example

    (coprod so1 so1)

    Here we construct GEB-BOOL:BOOL by simply stating that we have the terminal object on either side, giving us two possible ways to fill the type.

    (->left so1 so1)

(->right so1 so1)

    where applying ->LEFT gives us the left unit, while ->RIGHT gives us the right unit.

The Accessors specific to Subst Obj

  • [method] MCAR (PROD PROD)

  • [method] MCADR (PROD PROD)

  • [method] MCAR (COPROD COPROD)

  • [method] MCADR (COPROD COPROD)

7.2.2 Subst Morph

The overarching types that categorizes the SUBSTMORPH category. Note that SUBSTMORPH refers to the closed type, whereas <SUBSTMORPH> refers to the open type that allows for user extension.

  • [type] SUBSTMORPH

    The morphisms of the SUBSTMORPH category

SUBSTMORPH type is not a constructor itself, instead it's best viewed as the sum type, with the types below forming the constructors for the term. In ML we would write it similarly to:

type substmorph = comp
                | substobj
                | case
                | init
                | terminal
                | pair
                | distribute
                | inject-left
                | inject-right
                | project-left
                | project-right

Note that an instance of SUBSTOBJ, acts like the identity morphism to the layout specified by the given SUBSTOBJ. Thus we can view this as automatically lifting a SUBSTOBJ into a SUBSTMORPH

  • [type] COMP

    The composition morphism. Takes two CAT-MORPH values that get applied in standard composition order.

    The formal grammar of COMP is

    (comp mcar mcadr)

    which may be more familiar as

    g 。f

    Where COMP( 。) is the constructor, MCAR(g) is the second morphism that gets applied, and MCADR(f) is the first morphism that gets applied.

    Example:

    (geb-gui::visualize
 (comp
  (<-right so1 geb-bool:bool)
  (pair (<-left so1 geb-bool:bool)
        (<-right so1 geb-bool:bool))))

    In this example we are composing two morphisms. the first morphism that gets applied (PAIR ...) is the identity function on the type (PROD SO1 GEB-BOOL:BOOL), where we pair the left projection and the right projection, followed by taking the right projection of the type.

    Since we know (COMP f id) is just f per the laws of category theory, this expression just reduces to

    (<-right so1 geb-bool:bool)

  • [type] CASE

    Eliminates coproducts. Namely Takes two CAT-MORPH values, one gets applied on the left coproduct while the other gets applied on the right coproduct. The result of each CAT-MORPH values must be the same.

    The formal grammar of CASE is:

    (mcase mcar mcadr)

    Where MCASE is the constructor, MCAR is the morphism that gets applied to the left coproduct, and MCADR is the morphism that gets applied to the right coproduct.

    Example:

    (comp
 (mcase geb-bool:true
        geb-bool:not)
 (->right so1 geb-bool:bool))

    In the second example, we inject a term with the shape GEB-BOOL:BOOL into a pair with the shape (SO1 × GEB-BOOL:BOOL), then we use MCASE to denote a morphism saying. IF the input is of the shape SO1(0 1), then give us True, otherwise flip the value of the boolean coming in.

  • [type] INIT

    The INITIAL Morphism, takes any CAT-OBJ and creates a moprhism from SO0 (also known as void) to the object given.

    The formal grammar of INITIAL is

    (init obj)

    where INIT is the constructor. OBJ is the type of object that will be conjured up from SO0, when the morphism is applied onto an object.

    Example:

    (init so1)

    In this example we are creating a unit value out of void.

  • [type] TERMINAL

    The TERMINAL morphism, Takes any CAT-OBJ and creates a morphism from that object to SO1 (also known as unit).

    The formal grammar of TERMINAL is

    (terminal obj)

    where TERMINAL is the constructor. OBJ is the type of object that will be mapped to SO1, when the morphism is applied onto an object.

    Example:

    (terminal (coprod so1 so1))

(geb-gui::visualize (terminal (coprod so1 so1)))

(comp value (terminal (codomain value)))

(comp true (terminal bool))

    In the first example, we make a morphism from the corpoduct of SO1 and SO1 (essentially GEB-BOOL:BOOL) to SO1.

    In the third example we can proclaim a constant function by ignoring the input value and returning a morphism from unit to the desired type.

    The fourth example is taking a GEB-BOOL:BOOL and returning GEB-BOOL:TRUE.

  • [type] PAIR

    Introduces products. Namely Takes two CAT-MORPH values. When the PAIR morphism is applied on data, these two CAT-MORPH's are applied to the object, returning a pair of the results

    The formal grammar of constructing an instance of pair is:

    (pair mcar mcdr)

    where PAIR is the constructor, MCAR is the left morphism, and MCDR is the right morphism

    Example:

    (pair (<-left so1 geb-bool:bool)
      (<-right so1 geb-bool:bool))

(geb-gui::visualize (pair (<-left so1 geb-bool:bool)
                          (<-right so1 geb-bool:bool)))

    Here this pair morphism takes the pair SO1(0 1) × GEB-BOOL:BOOL, and projects back the left field SO1 as the first value of the pair and projects back the GEB-BOOL:BOOL field as the second values.

  • [type] DISTRIBUTE

    The distributive law

  • [type] INJECT-LEFT

    The left injection morphism. Takes two CAT-OBJ values. It is the dual of INJECT-RIGHT

    The formal grammar is

    (->left mcar mcadr)

    Where ->LEFT is the constructor, MCAR is the value being injected into the coproduct of MCAR + MCADR, and the MCADR is just the type for the unused right constructor.

    Example:

    (geb-gui::visualize (->left so1 geb-bool:bool))

(comp
 (mcase geb-bool:true
        geb-bool:not)
 (->left so1 geb-bool:bool))

    In the second example, we inject a term with the shape SO1(0 1) into a pair with the shape (SO1 × GEB-BOOL:BOOL), then we use MCASE to denote a morphism saying. IF the input is of the shape SO1(0 1), then give us True, otherwise flip the value of the boolean coming in.

  • [type] INJECT-RIGHT

    The right injection morphism. Takes two CAT-OBJ values. It is the dual of INJECT-LEFT

    The formal grammar is

    (->right mcar mcadr)

    Where ->RIGHT is the constructor, MCADR is the value being injected into the coproduct of MCAR + MCADR, and the MCAR is just the type for the unused left constructor.

    Example:

    (geb-gui::visualize (->right so1 geb-bool:bool))

(comp
 (mcase geb-bool:true
        geb-bool:not)
 (->right so1 geb-bool:bool))

    In the second example, we inject a term with the shape GEB-BOOL:BOOL into a pair with the shape (SO1 × GEB-BOOL:BOOL), then we use MCASE to denote a morphism saying. IF the input is of the shape SO1(0 1), then give us True, otherwise flip the value of the boolean coming in.

  • [type] FUNCTOR

The Accessors specific to Subst Morph

  • [method] MCAR (COMP COMP)

    The first composed morphism

  • [method] MCADR (COMP COMP)

    the second morphism

  • [method] OBJ (INIT INIT)

  • [method] OBJ (INIT INIT)

  • [method] MCAR (CASE CASE)

    The morphism that gets applied on the left coproduct

  • [method] MCADR (CASE CASE)

    The morphism that gets applied on the right coproduct

  • [method] MCAR (PAIR PAIR)

    The left morphism

  • [method] MCDR (PAIR PAIR)

    The right morphism

  • [method] MCAR (DISTRIBUTE DISTRIBUTE)

  • [method] MCADR (DISTRIBUTE DISTRIBUTE)

  • [method] MCADDR (DISTRIBUTE DISTRIBUTE)

  • [method] MCAR (INJECT-LEFT INJECT-LEFT)

  • [method] MCADR (INJECT-LEFT INJECT-LEFT)

  • [method] MCAR (INJECT-RIGHT INJECT-RIGHT)

  • [method] MCADR (INJECT-RIGHT INJECT-RIGHT)

  • [method] MCAR (PROJECT-LEFT PROJECT-LEFT)

  • [method] MCADR (PROJECT-LEFT PROJECT-LEFT)

  • [method] MCAR (PROJECT-RIGHT PROJECT-RIGHT)

  • [method] MCADR (PROJECT-RIGHT PROJECT-RIGHT)

    Right projection (product elimination)

7.3 Accessors

[in package GEB.UTILS]

These functions are generic lenses of the GEB codebase. If a class is defined, where the names are not known, then these accessors are likely to be used. They may even augment existing classes.

  • [generic-function] MCAR OBJ

    Can be seen as calling CAR on a generic CLOS object

  • [generic-function] MCADR OBJ

    like MCAR but for the CADR

  • [generic-function] MCADDR OBJ

    like MCAR but for the CADDR

  • [generic-function] MCADDDR OBJ

    like MCAR but for the CADDDR

  • [generic-function] MCDR OBJ

    Similar to MCAR, however acts like a CDR for classes that we wish to view as a SEQUENCE

  • [generic-function] OBJ OBJ

    Grabs the underlying object

  • [generic-function] NAME OBJ

    the name of the given object

  • [generic-function] FUNC OBJ

    the function of the object

  • [generic-function] PREDICATE OBJ

    the PREDICATE of the object

  • [generic-function] THEN OBJ

    the then branch of the object

  • [generic-function] ELSE OBJ

    the then branch of the object

7.4 Constructors

[in package GEB.SPEC]

The API for creating GEB terms. All the functions and variables here relate to instantiating a term

  • [variable] *SO0* s-0

    The Initial Object

  • [variable] *SO1* s-1

    The Terminal Object

More Ergonomic API variants for *SO0* and *SO1*

  • [symbol-macro] SO0

  • [symbol-macro] SO1

  • [macro] ALIAS NAME OBJ

  • [function] MAKE-ALIAS &KEY NAME OBJ

  • [function] HAS-ALIASP OBJ

  • [function] <-LEFT MCAR MCADR

    projects left constructor

  • [function] <-RIGHT MCAR MCADR

    projects right constructor

  • [function] ->LEFT MCAR MCADR

    injects left constructor

  • [function] ->RIGHT MCAR MCADR

    injects right constructor

  • [function] MCASE MCAR MCADR

  • [function] MAKE-FUNCTOR &KEY OBJ FUNC

7.5 API

Various forms and structures built on-top of Core Category

7.5.1 Booleans

[in package GEB-BOOL]

Here we define out the idea of a boolean. It comes naturally from the concept of coproducts. In ML they often define a boolean like

data Bool = False | True

We likewise define it with coproducts

(def bool (coprod so1 so1))

(def true  (->right so1 so1))
(def false (->left  so1 so1))

The functions given work on this.

  • [symbol-macro] TRUE

    The true value of a boolean type. In this case we've defined true as the right unit

  • [symbol-macro] FALSE

    The false value of a boolean type. In this case we've defined true as the left unit

  • [symbol-macro] FALSE-OBJ

  • [symbol-macro] TRUE-OBJ

  • [symbol-macro] BOOL

    The Boolean Type, composed of a coproduct of two unit objects

    (coprod so1 so1)

  • [symbol-macro] NOT

    Turns a TRUE into a FALSE and vice versa

  • [symbol-macro] AND

  • [symbol-macro] OR

7.5.2 Translation Functions

[in package GEB.TRANS]

These cover various conversions from Subst Morph and Subst Obj into other categorical data structures.

  • [function] TO-CIRCUIT OBJ NAME

    Turns a Subst Morph to a Vamp-IR Term

7.5.3 Utility

[in package GEB.MAIN]

Various utility functions ontop of Core Category

  • [function] PAIR-TO-LIST PAIR &OPTIONAL ACC

    converts excess pairs to a list format

  • [function] SAME-TYPE-TO-LIST PAIR TYPE &OPTIONAL ACC

    converts the given type to a list format

  • [function] CLEAVE V1 &REST VALUES

    Applies each morphism to the object in turn.

  • [function] CONST F X

    The constant morphism.

    Takes a morphism from SO1 to a desired value of type $B$, along with a <SUBSTOBJ> that represents the input type say of type $A$, giving us a morphism from $A$ to $B$.

    Thus if: F : SO1 → a, X : b

    then: (const f x) : a → b

    Γ, f : so1 → b, x : a
----------------------
(const f x) : a → b

    Further, If the input F is an ALIAS, then we wrap the output in a new alias to denote it's a constant version of that value.

    Example:

    (const true bool) ; bool -> bool

  • [function] COMMUTES X Y

  • [function] COMMUTES-LEFT MORPH

    swap the input domain of the given cat-morph

    In order to swap the domain we expect the cat-morph to be a PROD

    Thus if: (dom morph) ≡ (prod x y), for any x, y CAT-OBJ

    then: (commutes-left (dom morph)) ≡ (prod y x) u ` Γ, f : x × y → a

    (commutes-left f) : y × x → a `

  • [function] !-> A B

  • [function] SO-EVAL X Y

  • [function] SO-HOM-OBJ X Z

  • [generic-function] SO-CARD-ALG OBJ

    Gets the cardinality of the given object, returns a FIXNUM

  • [method] SO-CARD-ALG (OBJ <SUBSTOBJ>)

  • [function] CURRY F

    Curries the given object, returns a cat-morph

    The cat-morph given must have its DOM be of a PROD type, as CURRY invokes the idea of

    if f : (PROD a b) → c

    for all a, b, and c being an element of cat-morph

    then: (curry f): a → c^b

    where c^b means c to the exponent of b (EXPT c b)

    Γ, f : a × b → c,
--------------------
(curry f) : a → c^b

    In category terms, a → c^b is isomorphic to a → b → c

  • [generic-function] TEXT-NAME MORPH

    Gets the name of the moprhism

7.6 Examples

PLACEHOLDER: TO SHOW OTHERS HOW EXAMPLEs WORK

Let's see the transcript of a real session of someone working with GEB:

(values (princ :hello) (list 1 2))
.. HELLO
=> :HELLO
=> (1 2)

(+ 1 2 3 4)
=> 10

8 The GEB GUI

[in package GEB-GUI]

This section covers the suite of tools that help visualize geb objects and make the system nice to work with

8.1 Visualizer

The GEB visualizer deals with visualizing any objects found in the Core Category

if the visualizer gets a Subst Morph, then it will show how the GEB:SUBSTMORPH changes any incoming term.

if the visualizer gets a Subst Obj, then it shows the data layout of the term, showing what kind of data

  • [function] KILL-RUNNING

    Kills all threads and open gui objects created by VISUALIZE

8.1.1 Aiding the Visualizer

One can aid the visualization process a bit, this can be done by simply playing GEB:ALIAS around the object, this will place it in a box with a name to better identify it in the graphing procedure.

8.2 The GEB Graphizer

[in package GEB-GUI.GRAPHING]

This section covers the GEB Graph representation

8.2.1 The GEB Graphizer Core

[in package GEB-GUI.CORE]

This section covers the graphing procedure in order to turn a GEB object into a format for a graphing backend.

The core types that facilittate the functionality

  • [type] NOTE

    A note is a note about a new node in the graph or a note about a NODE which should be merged into an upcoming NODE.

    An example of a NODE-NOTE would be in the case of pair

    (pair g f)
                   Π₁
     --f--> Y------
X----|            |-----> [Y × Z]
     --g--> Z-----
               Π₂

    An example of a MERGE-NOTE

    (Case f g)
(COMP g f)
               χ₁
         -------> X --f---
[X + Y]--|                ---> A
         -------> Y --g---/
           χ₂

X -f-> Y --> Y -g-> Z

    Notice that in the pair case, we have a note and a shared node to place down, where as in both of the MERGE-NOTE examples, the Note at the end is not pre-pended by any special information

  • [class] NODE META-MIXIN

    I represent a graphical node structure. I contain my children and a value to display, along with the representation for which the node really stands for.

    Further, we derive the meta-mixin, as it's important for arrow drawing to know if we are the left or the right or the nth child of a particular node. This information is tracked, by storing the object that goes to it in the meta table and recovering the note.

  • [function] MAKE-NOTE &REST INITARGS &KEY FROM NOTE VALUE &ALLOW-OTHER-KEYS

  • [function] MAKE-SQUASH &REST INITARGS &KEY VALUE &ALLOW-OTHER-KEYS

  • [generic-function] GRAPHIZE MORPH NOTES

    Turns a morphism into a node graph.

    The NOTES serve as a way of sharing and continuing computation.

    If the NOTE is a :SHARED NOTE then it represents a NODE without children, along with saying where it came from. This is to be stored in parent of the NOTE

    If the NOTE is a :CONTINUE NOTE, then the computation is continued at the spot.

    The parent field is to set the note on the parent if the NOTE is going to be merged

  • [generic-function] VALUE OBJECT

  • [function] CONS-NOTE NOTE NOTES

    Adds a note to the notes list.

  • [function] APPLY-NOTE NOTE-TO-BE-ON NOTE

    Here we apply the NOTE to the NODE.

    In the case of a new node, we record down the information in the note, and set the note as the child of the current NODE. The NODE is returned.

    In the case of a squash-note, we instead just return the squash-note as that is the proper NODE to continue from

  • [generic-function] REPRESENTATION OBJECT

  • [generic-function] CHILDREN OBJECT

  • [function] DETERMINE-TEXT-AND-OBJECT-FROM-NODE FROM TO

    Helps lookup the text from the node

  • [function] NOTERIZE-CHILDREN NODE FUNC

    Applies a specified note to the CHILDREN of the NODE.

    It does this by applying FUNC on all the CHILDREN and the index of the child in the list

  • [function] NOTORIZE-CHILDREN-WITH-INDEX-SCHEMA PREFIX NODE

    Notorizes the node with a prefix appended with the subscripted number

8.2.2 The GEB Graphizer Passes

[in package GEB-GUI.GRAPHING.PASSES]

This changes how the graph is visualized, simplifying the graph in ways that are intuitive to the user

  • [function] PASSES NODE

    Runs all the passes that simplify viewing the graph. These simplifications should not change the semantics of the graph, only display it in a more bearable way

9 Polynomial Specification

[in package GEB.POLY]

This covers a GEB view of Polynomials. In particular this type will be used in translating GEB's view of Polynomials into Vampir

9.1 Polynomial Types

[in package GEB.POLY.SPEC]

This section covers the types of things one can find in the POLY constructors

  • [type] POLY

  • [type] <POLY>

  • [type] IDENT

    The Identity Element

  • [type] +

  • [type] *

  • [type] /

  • [type] -

  • [type] MOD

  • [type] COMPOSE

  • [type] IF-ZERO

    compare with zero: equal takes first branch; not-equal takes second branch

  • [type] IF-LT

    If the MCAR argument is strictly less than the MCADR then the THEN branch is taken, otherwise the ELSE branch is taken.

9.2 Polynomial Constructors

[in package GEB.POLY.SPEC]

Every accessor for each of the CLASS's found here are from Accessors

  • [symbol-macro] IDENT

  • [function] + MCAR MCADR &REST ARGS

    Creates a multiway constructor for +

  • [function] * MCAR MCADR &REST ARGS

    Creates a multiway constructor for *

  • [function] / MCAR MCADR &REST ARGS

    Creates a multiway constructor for /

  • [function] - MCAR MCADR &REST ARGS

    Creates a multiway constructor for -

  • [function] MOD MCAR MCADR

    MOD ARG1 by ARG2

  • [function] COMPOSE MCAR MCADR &REST ARGS

    Creates a multiway constructor for COMPOSE

  • [function] IF-ZERO PRED THEN ELSE

    checks if PREDICATE is zero then take the THEN branch otherwise the ELSE branch

  • [function] IF-LT MCAR MCADR THEN ELSE

    Checks if the MCAR is less than the MCADR and chooses the appropriate branch

9.3 Polynomial Transformations

[in package GEB.POLY.TRANS]

This covers transformation functions from

  • [generic-function] TO-VAMPIR MORPHISM VALUE

    Turns a POLY term into a Vamp-IR term with a given value

  • [function] TO-CIRCUIT MORPHISM NAME

    Turns a POLY term into a Vamp-IR Gate with the given name

10 The Simply Typed Lambda Calculus model

[in package GEB.LAMBDA]

This covers GEB's view on simply typed lambda calculus

10.1 Lambda Specification

[in package GEB.LAMBDA.SPEC]

This covers the various the abstract data type that is the simply typed lambda calculus within GEB.

The specification follows from the sum type declaration

(defunion stlc
  (absurd (value t))
  unit
  (left (value t))
  (right (value t))
  (case-on (lty geb.spec:substmorph)
           (rty geb.spec:substmorph)
           (cod geb.spec:substmorph)
           (on t) (left t) (right t))
  (pair (lty geb.spec:substmorph) (rty geb.spec:substmorph) (left t) (right t))
  (fst  (lty geb.spec:substmorph) (rty geb.spec:substmorph) (value t))
  (snd  (lty geb.spec:substmorph) (rty geb.spec:substmorph) (value t))
  (lamb (vty geb.spec:substmorph) (tty geb.spec:substmorph) (value t))
  (app  (dom geb.spec:substmorph) (cod geb.spec:substmorph) (func t) (obj t))
  (index (index fixnum)))

  • [type] <STLC>

  • [type] STLC

  • [type] ABSURD

  • [function] ABSURD-VALUE INSTANCE

  • [type] UNIT

  • [type] PAIR

  • [function] PAIR-LTY INSTANCE

  • [function] PAIR-RTY INSTANCE

  • [function] PAIR-LEFT INSTANCE

  • [function] PAIR-RIGHT INSTANCE

  • [type] LEFT

  • [function] LEFT-VALUE INSTANCE

  • [type] RIGHT

  • [function] RIGHT-VALUE INSTANCE

  • [type] CASE-ON

  • [function] CASE-ON-LTY INSTANCE

  • [function] CASE-ON-RTY INSTANCE

  • [function] CASE-ON-COD INSTANCE

  • [function] CASE-ON-ON INSTANCE

  • [function] CASE-ON-LEFT INSTANCE

  • [function] CASE-ON-RIGHT INSTANCE

  • [type] FST

  • [function] FST-LTY INSTANCE

  • [function] FST-RTY INSTANCE

  • [function] FST-VALUE INSTANCE

  • [type] SND

  • [function] SND-LTY INSTANCE

  • [function] SND-RTY INSTANCE

  • [function] SND-VALUE INSTANCE

  • [type] LAMB

  • [function] LAMB-VTY INSTANCE

  • [function] LAMB-TTY INSTANCE

  • [function] LAMB-VALUE INSTANCE

  • [type] APP

  • [function] APP-DOM INSTANCE

  • [function] APP-COD INSTANCE

  • [function] APP-FUNC INSTANCE

  • [function] APP-OBJ INSTANCE

  • [type] INDEX

  • [function] INDEX-INDEX INSTANCE

  • [function] TYPED V TYP

    Puts together the type declaration with the value itself for lambda terms

  • [function] TYPED-STLC-TYPE INSTANCE

  • [function] TYPED-STLC-VALUE INSTANCE

10.2 Main functionality

[in package GEB.LAMBDA.MAIN]

This covers the main API for the STLC module

10.3 Transition Functions

[in package GEB.LAMBDA.TRANS]

These functions deal with transforming the data structure to other data types

  • [generic-function] COMPILE-CHECKED-TERM CONTEXT TYPE TERM

    Compiles a checked term into SubstMorph category

  • [function] TO-POLY CONTEXT TYPE OBJ

  • [function] TO-CIRCUIT CONTEXT TYPE OBJ NAME

10.3.1 Utility Functionality

These are utility functions relating to translating lambda terms to other types

  • [function] STLC-CTX-TO-MU CONTEXT

    Converts a generic (CODE ) context into a SUBSTMORPH

  • [function] SO-HOM DOM COD

    Computes the hom-object of two SUBSTMORPHs

11 Mixins

[in package GEB.MIXINS]

Various mixins of the project. Overall all these offer various services to the rest of the project

11.1 Pointwise Mixins

Here we provide various mixins that deal with classes in a pointwise manner. Normally, objects can not be compared in a pointwise manner, instead instances are compared. This makes functional idioms like updating a slot in a pure manner (allocating a new object), or even checking if two objects are EQUAL-able adhoc. The pointwise API, however, derives the behavior and naturally allows such idioms

  • [class] POINTWISE-MIXIN

    Provides the service of giving point wise operations to classes

Further we may wish to hide any values inherited from our superclass due to this we can instead compare only the slots defined directly in our class

11.2 Pointwise API

These are the general API functions on any class that have the POINTWISE-MIXIN service.

Functions like TO-POINTWISE-LIST allow generic list traversal APIs to be built off the key-value pair of the raw object form, while OBJ-EQUALP allows the checking of functional equality between objects. Overall the API is focused on allowing more generic operations on classes that make them as useful for generic data traversal as LIST(0 1)'s are

  • [generic-function] TO-POINTWISE-LIST OBJ

    Turns a given object into a pointwise LIST(0 1). listing the KEYWORD slot-name next to their value.

  • [generic-function] OBJ-EQUALP OBJECT1 OBJECT2

    Compares objects with pointwise equality. This is a much weaker form of equality comparison than STANDARD-OBJECT EQUALP, which does the much stronger pointer quality

  • [generic-function] POINTWISE-SLOTS OBJ

    Works like C2MOP:COMPUTE-SLOTS however on the object rather than the class

11.3 Mixins Examples

Let's see some example uses of POINTWISE-MIXIN:

(obj-equalp (geb:terminal geb:so1)
            (geb:terminal geb:so1))
=> t

(to-pointwise-list (geb:coprod geb:so1 geb:so1))
=> ((:MCAR . s-1) (:MCADR . s-1))

11.4 Metadata Mixin

Metadata is a form of meta information about a particular object. Having metadata about an object may be useful if the goal requires annotating some data with type information, identification information, or even various levels of compiler information. The possibilities are endless and are a standard technique.

For this task we offer the META-MIXIN which will allow metadata to be stored for any type that uses its service.

  • [class] META-MIXIN

    Use my service if you want to have metadata capabilities associated with the given object. Performance covers my performance characteristics

For working with the structure it is best to have operations to treat it like an ordinary hashtable

  • [function] META-INSERT OBJECT KEY VALUE &KEY WEAK

    Inserts a value into storage. If the key is a one time object, then the insertion is considered to be volatile, which can be reclaimed when no more references to the data exists.

    If the data is however a constant like a string, then the insertion is considered to be long lived and will always be accessible

    The :weak keyword specifies if the pointer stored in the value is weak

  • [function] META-LOOKUP OBJECT KEY

    Lookups the requested key in the metadata table of the object. We look past weak pointers if they exist

11.4.1 Performance

The data stored is at the CLASS level. So having your type take the META-MIXIN does interfere with the cache.

Due to concerns about meta information being populated over time, the table which it is stored with is in a weak hashtable, so if the object that the metadata is about gets deallocated, so does the metadata table.

The full layout can be observed from this interaction

;; any class that uses the service
(defparameter *x* (make-instance 'meta-mixin))

(meta-insert *x* :a 3)

(defparameter *y* (make-instance 'meta-mixin))

(meta-insert *y* :b 3)

(defparameter *z* (make-instance 'meta-mixin))

;; where {} is a hashtable
{*x* {:a 3}
 *y* {:b 3}}

Since *z* does not interact with storage no overhead of storage is had. Further if `x goes out of scope, gc would reclaim the table leaving

{*y* {:b 3}}

for the hashtable.

Even the tables inside each object's map are weak, thus we can make storage inside metadata be separated into volatile and stable storage.

12 Geb Utilities

[in package GEB.UTILS]

The Utilities package provides general utility functionality that is used throughout the GEB codebase

  • [type] LIST-OF TY

    Allows us to state a list contains a given type.

    NOTE

    This does not type check the whole list, but only the first element. This is an issue with how lists are defined in the language. Thus this should be be used for intent purposes.

    For a more proper version that checks all elements please look at writing code like

    (deftype normal-form-list ()
  `(satisfies normal-form-list))

(defun normal-form-list (list)
  (and (listp list)
       (every (lambda (x) (typep x 'normal-form)) list)))

(deftype normal-form ()
  `(or wire constant))

    Example usage of this can be used with typep

    (typep '(1 . 23) '(list-of fixnum))
=> NIL

(typep '(1 23) '(list-of fixnum))
=> T

(typep '(1 3 4 "hi" 23) '(list-of fixnum))
=> T

(typep '(1 23 . 5) '(list-of fixnum))
=> T

    Further this can be used in type signatures

    (-> foo (fixnum) (list-of fixnum))
(defun foo (x)
  (list x))

  • [function] SYMBOL-TO-KEYWORD SYMBOL

    Turns a symbol into a keyword

  • [macro] MUFFLE-PACKAGE-VARIANCE &REST PACKAGE-DECLARATIONS

    Muffle any errors about package variance and stating exports out of order. This is particularly an issue for SBCL as it will error when using MGL-PAX to do the export instead of DEFPACKAGE.

    This is more modular thank MGL-PAX:DEFINE-PACKAGE in that this can be used with any package creation function like UIOP:DEFINE-PACKAGE.

    Here is an example usage:

         (geb.utils:muffle-package-variance
       (uiop:define-package #:geb.lambda.trans
         (:mix #:trivia #:geb #:serapeum #:common-lisp)
         (:export
          :compile-checked-term :stlc-ctx-to-mu)))

  • [function] SUBCLASS-RESPONSIBILITY OBJ

    Denotes that the given method is the subclasses responsibility. Inspired from Smalltalk

  • [function] SHALLOW-COPY-OBJECT ORIGINAL

  • [macro] MAKE-PATTERN OBJECT-NAME &REST CONSTRUCTOR-NAMES

    make pattern matching position style instead of record style. This removes the record constructor style, however it can be brought back if wanted

    (defclass alias (<substmorph> <substobj>)
  ((name :initarg :name
         :accessor name
         :type     symbol
         :documentation "The name of the GEB object")
   (obj :initarg :obj
        :accessor obj
        :documentation "The underlying geb object"))
  (:documentation "an alias for a geb object"))

(make-pattern alias name obj)

  • [function] NUMBER-TO-DIGITS NUMBER &OPTIONAL REM

    turns an INTEGER into a list of its digits

  • [function] DIGIT-TO-UNDER DIGIT

    Turns a digit into a subscript string version of the number

  • [function] NUMBER-TO-UNDER INDEX

    Turns an INTEGER into a subscripted STRING

12.1 Accessors

These functions are generic lenses of the GEB codebase. If a class is defined, where the names are not known, then these accessors are likely to be used. They may even augment existing classes.

  • [generic-function] MCAR OBJ

    Can be seen as calling CAR on a generic CLOS object

  • [generic-function] MCADR OBJ

    like MCAR but for the CADR

  • [generic-function] MCADDR OBJ

    like MCAR but for the CADDR

  • [generic-function] MCADDDR OBJ

    like MCAR but for the CADDDR

  • [generic-function] MCDR OBJ

    Similar to MCAR, however acts like a CDR for classes that we wish to view as a SEQUENCE

  • [generic-function] OBJ OBJ

    Grabs the underlying object

  • [generic-function] NAME OBJ

    the name of the given object

  • [generic-function] FUNC OBJ

    the function of the object

  • [generic-function] PREDICATE OBJ

    the PREDICATE of the object

  • [generic-function] THEN OBJ

    the then branch of the object

  • [generic-function] ELSE OBJ

    the then branch of the object

13 Testing

[in package GEB-TEST]

We use parachute as our testing framework.

Please read the manual for extra features and how to better lay out future tests

  • [function] RUN-TESTS &KEY (INTERACTIVE? NIL) (SUMMARY? NIL) (PLAIN? T) (DESIGNATORS '(GEB-TEST-SUITE))

    Here we run all the tests. We have many flags to determine how the tests ought to work

    (run-tests :plain? nil :interactive? t) ==> 'interactive
(run-tests :summary? t :interactive? t) ==> 'noisy-summary
(run-tests :interactive? t)             ==> 'noisy-interactive
(run-tests :summary? t)                 ==> 'summary
(run-tests)                             ==> 'plain

(run-tests :designators '(geb geb.lambda)) ==> run only those packages

  • [function] RUN-TESTS-ERROR

  • [function] CODE-COVERAGE &OPTIONAL (PATH NIL)

    generates code coverage, for CCL the coverage can be found at

    CCL test coverage

    SBCL test coverage

    simply run this function to generate a fresh one

[generated by MGL-PAX]

About

A Categorical View of Computation

anoma.github.io/geb/

Resources

Readme

License

GPL-3.0 license
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

 
 
 

Contributors

Languages

  • Idris 77.6%
  • Common Lisp 11.7%
  • Agda 10.7%