From 9e432c095f611059cb507c47b03ce97da14f0a1e Mon Sep 17 00:00:00 2001 From: mariari Date: Thu, 13 Jul 2023 02:04:35 +0800 Subject: [PATCH] Docs Generation Batch Simply generate out the docs batch --- README | 134 +++++---- README.md | 793 ++++++++++++++++++++++++++++++++++++++++++------------ 2 files changed, 690 insertions(+), 237 deletions(-) diff --git a/README b/README index d4c5931d6..10796d30c 100644 --- a/README +++ b/README @@ -9,6 +9,8 @@ Here is the [official repository](https://github.com/anoma/geb/) and [HTML documentation](https://anoma.github.io/geb/) for the latest version. +Maintainers: please read the [maintainers guide](https://github.com/anoma/geb/blob/main/docs/maintainers-guide.org) + ### code coverage For test coverage it can be found at the following links: @@ -104,26 +106,28 @@ to use An example use of this binary is as follows ```bash -mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -v -o "foo.pir" +mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -p -o "foo.pir" mariari@Gensokyo % cat foo.pir def entry x1 = { (x1) };% -mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -v +mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -p def *entry* x { 0 } -./geb.image -h +mariari@Gensokyo % ./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 + -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 + -v --version boolean Prints the current version of the compiler + -p --vampir string Return a vamp-ir expression -h -? --help boolean The current help message +mariari@Gensokyo % ./geb.image -v +0.3.2 ``` starting from a file *foo.lisp* that has @@ -300,7 +304,7 @@ $$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$, +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 @@ -350,14 +354,14 @@ 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}$. +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*](https://en.wikipedia.org/wiki/Currying) of functions, - $C^{(B^A)} \cong C^{(A × B)}$, + $C^\{(B^A)\} \cong C^\{(A × B)\}$, such that providing several arguments to a function can done either simultaneously, or in sequence. @@ -368,13 +372,13 @@ of functions, 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}.$$ +$$Ax^\{\sf 2\} +x^\{\sf 1\} - Dx^\{\sf 0\}.$$ (We need these later to define [“algebraic data types”](https://en.wikipedia.org/wiki/Polynomial_functor_(type_theory)).) 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$, +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 @@ -1491,7 +1495,7 @@ The functions given work on this. ###### \[in package GEB-LIST\] Here we define out the idea of a List. It comes naturally from the concept of coproducts. Since we lack polymorphism this list is -concrete over [GEB-BOOL:@GEB-BOOL][section] In ML syntax it looks like +concrete over GEB-BOOL:@GEB-BOOL In ML syntax it looks like ```haskell data List = Nil | Cons Bool List @@ -1801,6 +1805,25 @@ One can aid the visualization process a bit, this can be done by simply placing ALIAS around the object, this will place it in a box with a name to better identify it in the graphing procedure. +### Export Visualizer + +This works like the normal visualizer except it exports it to a +file to be used by other projects or perhaps in papers + +- [function] SVG OBJECT PATH &KEY (DEFAULT-VIEW (MAKE-INSTANCE 'SHOW-VIEW)) + + Runs the visualizer, outputting a static SVG image at the directory of choice. + + You can customize the view. By default it uses the show-view, which is + the default of the visualizer. + + A good example usage is + + ```lisp + GEB-TEST> (geb-gui:svg (shallow-copy-object geb-bool:and) "/tmp/foo.svg") + ``` + + ### The GEB Graphizer ###### \[in package GEB-GUI.GRAPHING\] @@ -2196,28 +2219,28 @@ constructors - [class] DIRECT-POINTWISE-MIXIN -- [type] IDENT +- [class] IDENT \ The Identity Element -- [type] + +- [class] + \ -- [type] * +- [class] * \ -- [type] / +- [class] / \ -- [type] - +- [class] - \ -- [type] MOD +- [class] MOD \ -- [type] COMPOSE +- [class] COMPOSE \ -- [type] IF-ZERO +- [class] IF-ZERO \ compare with zero: equal takes first branch; not-equal takes second branch -- [type] IF-LT +- [class] IF-LT \ If the MCAR argument is strictly less than the MCADR then the THEN branch is taken, otherwise the ELSE branch is taken. @@ -2459,9 +2482,9 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. This corresponds to the elimination rule of the empty type. Namely, given - $$\Gamma \vdash \text{tcod : Type}$$ and - $$\Gamma \vdash \text{term : so0}$$ one deduces - $$\Gamma \vdash \text{(absurd tcod term) : tcod}$$ + $$\Gamma \vdash \text\{tcod : Type\}$$ and + $$\Gamma \vdash \text\{term : so0\}$$ one deduces + $$\Gamma \vdash \text\{(absurd tcod term) : tcod\}$$ - [class] UNIT \ @@ -2482,7 +2505,7 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. we provide all terms untyped. This grammar corresponds to the introduction rule of the unit type. Namely - $$\Gamma \dashv \text{(unit) : so1}$$ + $$\Gamma \dashv \text\{(unit) : so1\}$$ - [class] LEFT \ @@ -2506,11 +2529,11 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. is TERM. This corresponds to the introduction rule of the coproduct type. Namely, given - $$\Gamma \dashv \text{(ttype term) : Type}$$ and - $$\Gamma \dashv \text{rty : Type}$$ + $$\Gamma \dashv \text\{(ttype term) : Type\}$$ and + $$\Gamma \dashv \text\{rty : Type\}$$ with - $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce - $$\Gamma \dashv \text{(left rty term) : (coprod (ttype term) rty)}$$ + $$\Gamma \dashv \text\{term : (ttype term)\}$$ we deduce + $$\Gamma \dashv \text\{(left rty term) : (coprod (ttype term) rty)\}$$ - [class] RIGHT \ @@ -2533,11 +2556,11 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. hence an STLC) we are injecting is TERM. This corresponds to the introduction rule of the coproduct type. Namely, given - $$\Gamma \dashv \text{(ttype term) : Type}$$ and - $$\Gamma \dashv \text{lty : Type}$$ + $$\Gamma \dashv \text\{(ttype term) : Type\}$$ and + $$\Gamma \dashv \text\{lty : Type\}$$ with - $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce - $$\Gamma \dashv \text{(right lty term) : (coprod lty (ttype term))}$$ + $$\Gamma \dashv \text\{term : (ttype term)\}$$ we deduce + $$\Gamma \dashv \text\{(right lty term) : (coprod lty (ttype term))\}$$ - [class] CASE-ON \ @@ -2560,12 +2583,12 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. - (mcar (ttype on)) and (mcadr (ttype on)). This corresponds to the elimination rule of the coprodut type. Namely, given - $$\Gamma \vdash \text{on : (coprod (mcar (ttype on)) (mcadr (ttype on)))}$$ + $$\Gamma \vdash \text\{on : (coprod (mcar (ttype on)) (mcadr (ttype on)))\}$$ and - $$\text{(mcar (ttype on))} , \Gamma \vdash \text{ltm : (ttype ltm)}$$ - , $$\text{(mcadr (ttype on))} , \Gamma \vdash \text{rtm : (ttype ltm)}$$ + $$\text\{(mcar (ttype on))\} , \Gamma \vdash \text\{ltm : (ttype ltm)\}$$ + , $$\text\{(mcadr (ttype on))\} , \Gamma \vdash \text\{rtm : (ttype ltm)\}$$ we get - $$\Gamma \vdash \text{(case-on on ltm rtm) : (ttype ltm)}$$ + $$\Gamma \vdash \text\{(case-on on ltm rtm) : (ttype ltm)\}$$ Note that in practice we append contexts on the left as computation of INDEX is done from the left. Otherwise, the rules are the same as in usual type theory if context was read from right to left. @@ -2591,9 +2614,9 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. of the product. The grammar corresponds to the introdcution rule of the pair type. Given - $$\Gamma \vdash \text{ltm : (mcar (ttype (pair ltm rtm)))}$$ and - $$\Gamma \vdash \text{rtm : (mcadr (ttype (pair ltm rtm)))}$$ we have - $$\Gamma \vdash \text{(pair ltm rtm) : (ttype (pair ltm rtm))}$$ + $$\Gamma \vdash \text\{ltm : (mcar (ttype (pair ltm rtm)))\}$$ and + $$\Gamma \vdash \text\{rtm : (mcadr (ttype (pair ltm rtm)))\}$$ we have + $$\Gamma \vdash \text\{(pair ltm rtm) : (ttype (pair ltm rtm))\}$$ - [class] FST \ @@ -2666,9 +2689,9 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. For a list of length 1, corresponds to the introduction rule of the function type. Namely, given - $$\Gamma \vdash \text{tdom : Type}$$ and - $$\Gamma, \text{tdom} \vdash \text{term : (ttype term)}$$ we have - $$\Gamma \vdash \text{(lamb tdom term) : (so-hom-obj tdom (ttype term))}$$ + $$\Gamma \vdash \text\{tdom : Type\}$$ and + $$\Gamma, \text\{tdom\} \vdash \text\{term : (ttype term)\}$$ we have + $$\Gamma \vdash \text\{(lamb tdom term) : (so-hom-obj tdom (ttype term))\}$$ For a list of length n, this coreesponds to the iterated lambda type, e.g. @@ -2718,7 +2741,7 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. function type with a corresponding codomain iteratively to terms in the domains. APP takes as argument for the FUN accessor a function - and hence an STLC - whose function type has domain an - iterated GEB:PROD of [SUBSTOBJ][clas] and for the TERM + iterated GEB:PROD of SUBSTOBJ and for the TERM a list of terms - and hence of STLC - matching the types of the product. The formal grammar of APP is @@ -2740,9 +2763,9 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. For a one-argument term list, this corresponds to the elimination rule of the function type. Given - $$\Gamma \vdash \text{fun : (so-hom-obj (ttype term) y)}$$ and - $$\Gamma \vdash \text{term : (ttype term)}$$ we get - $$\Gamma \vdash \text{(app fun term) : y}$$ + $$\Gamma \vdash \text\{fun : (so-hom-obj (ttype term) y)\}$$ and + $$\Gamma \vdash \text\{term : (ttype term)\}$$ we get + $$\Gamma \vdash \text\{(app fun term) : y\}$$ For several arguments, this corresponds to successive function application. Using currying, this corresponds to, given @@ -2781,9 +2804,9 @@ typed lambda calculus within GEB. The class presents untyped STLC terms. natural number indicating the position of a type in a context. This corresponds to the variable rule. Namely given a context - $$\Gamma\_1 , \ldots , \Gamma\_{pos} , \ldots , \Gamma\_k $$ we have + $$\Gamma\_1 , \ldots , \Gamma\_\{pos\} , \ldots , \Gamma\_k $$ we have - $$\Gamma\_1 , \ldots , \Gamma\_k \vdash \text{(index pos) :} \Gamma\_{pos}$$ + $$\Gamma\_1 , \ldots , \Gamma\_k \vdash \text\{(index pos) :\} \Gamma\_\{pos\}$$ Note that we add contexts on the left rather than on the right contra classical type-theoretic notation. @@ -2992,7 +3015,7 @@ This covers the main API for the STLC module (ann-term1 (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0)))) ``` - produces an error trying to use HOM-COD. This warning applies to other + produces an error trying to use. This warning applies to other functions taking in context and terms below as well. Moreover, note that for terms whose typing needs addition of new context @@ -3008,13 +3031,6 @@ This covers the main API for the STLC module as we count indeces from the left of the context while appending new types to the context on the left as well. For more info check LAMB -- [function] HOM-COD CTX F - - Given a context of SUBSTOBJ with occurences of - SO-HOM-OBJ replaced by FUN-TYPE, and similarly - an STLC term of the stand-in for the hom object, produces the stand-in - to the codomain. - - [function] INDEX-CHECK I CTX Given an natural number I and a context, checks that the context is of diff --git a/README.md b/README.md index 770aac2d1..62402615f 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,5 @@ + # The GEB Manual ## Table of Contents @@ -41,9 +42,10 @@ - [9 The GEB GUI][6f67] - [9.1 Visualizer][c6cf] - [9.1.1 Aiding the Visualizer][603e] - - [9.2 The GEB Graphizer][1b98] - - [9.2.1 The GEB Graphizer Core][71e9] - - [9.2.2 The GEB Graphizer Passes][e429] + - [9.2 Export Visualizer][f0f8] + - [9.3 The GEB Graphizer][1b98] + - [9.3.1 The GEB Graphizer Core][71e9] + - [9.3.2 The GEB Graphizer Passes][e429] - [10 Bits (Boolean Circuit) Specification][6b63] - [10.1 Bits Types][2172] - [10.2 Bits (Boolean Circuit) Constructors][fc10] @@ -73,13 +75,17 @@ Welcome to the GEB project. + ## 1 Links Here is the [official repository](https://github.com/anoma/geb/) and [HTML documentation](https://anoma.github.io/geb/) for the latest version. +Maintainers: please read the [maintainers guide](https://github.com/anoma/geb/blob/main/docs/maintainers-guide.org) + + ### 1.1 code coverage For test coverage it can be found at the following links: @@ -100,11 +106,13 @@ 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`][417f] + ## 2 Getting Started Welcome to the GEB Project! + ### 2.1 installation This project uses [common lisp](https://common-lisp.net/), so a few @@ -124,6 +132,7 @@ This project uses [common lisp](https://common-lisp.net/), so a few + ### 2.2 loading Now that we have an environment setup, we can load the project, this @@ -162,6 +171,7 @@ writing: + ### 2.3 Geb as a binary ###### \[in package GEB.ENTRY\] @@ -179,26 +189,28 @@ to use An example use of this binary is as follows ```bash -mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -v -o "foo.pir" +mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -p -o "foo.pir" mariari@Gensokyo % cat foo.pir def entry x1 = { (x1) };% -mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -v +mariari@Gensokyo % ./geb.image -i "foo.lisp" -e "geb.lambda.main::*entry*" -l -p def *entry* x { 0 } -./geb.image -h +mariari@Gensokyo % ./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 + -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 + -v --version boolean Prints the current version of the compiler + -p --vampir string Return a vamp-ir expression -h -? --help boolean The current help message +mariari@Gensokyo % ./geb.image -v +0.3.2 ``` starting from a file *foo.lisp* that has @@ -220,7 +232,7 @@ with the term bound to some global variable inside of it. The command needs an entry-point (-e or --entry-point), as we are -simply call [`LOAD`][f766] on the given file, and need to know what to +simply call [`LOAD`][b5ec] on the given file, and need to know what to translate. from `STLC`, we expect the form to be wrapped in the @@ -235,12 +247,15 @@ 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. @@ -295,6 +310,7 @@ lambda term rather than a geb term. In time this will go away the trade offs and usage in the code-base read the section [Open Types versus Closed Types][a920]. + - [glossary-term] **open type** An open type is a type that can be extended by user code down the @@ -324,6 +340,7 @@ lambda term rather than a geb term. In time this will go away [Open Types versus Closed Types][a920]. + - [glossary-term] **Common Lisp Object System (CLOS)** The object system found in CL. Has great features like a [Meta Object @@ -331,6 +348,7 @@ lambda term rather than a geb term. In time this will go away helps it facilitate extensions. + ## 4 Original Efforts Originally GEB started off as an Idris codebase written by the @@ -340,6 +358,7 @@ 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 @@ -352,6 +371,7 @@ treasure trove of interesting information surrounding category theory. + ### 4.2 Geb's Agda Code The Agda folder can be found in the @@ -365,6 +385,7 @@ while [Geb's Agda Code][29b7] serves as the mathematical formalism proving vario conjectures about GEB + ## 5 Categorical Model Geb is organizing programming language concepts (and entities!) using @@ -384,7 +405,7 @@ $$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$, +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 @@ -434,14 +455,14 @@ 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}$. +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*](https://en.wikipedia.org/wiki/Currying) of functions, - $C^{(B^A)} \cong C^{(A × B)}$, + $C^\{(B^A)\} \cong C^\{(A × B)\}$, such that providing several arguments to a function can done either simultaneously, or in sequence. @@ -452,13 +473,13 @@ of functions, 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}.$$ +$$Ax^\{\sf 2\} +x^\{\sf 1\} - Dx^\{\sf 0\}.$$ (We need these later to define [“algebraic data types”](https://en.wikipedia.org/wiki/Polynomial_functor_(type_theory)).) 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$, +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 @@ -482,22 +503,27 @@ 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 @@ -514,6 +540,7 @@ 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\] @@ -546,6 +573,7 @@ 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][8932]'s and [open type][4a87]'s both have their perspective @@ -585,7 +613,7 @@ these methods, let us look at two other benefits given by [`GEB:`][fb7 great way to generically enhance the capabilities of the type without operating on it directly. -2. We can dispatch on `GEB:` since [`DEFMETHOD`][a981] only works on +2. We can dispatch on `GEB:` since [`DEFMETHOD`][6832] only works on [Common Lisp Object System (CLOS)][ecc6] types and not generic types in CL. #### Methods for closed and open types @@ -652,6 +680,7 @@ 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][4a87] variant to a [closed type][8932]. Thus when @@ -659,6 +688,7 @@ one sees a type like GEB: it is the open version of [`GEB:SUBSTOBJ`][3173]. Read [Open Types versus Closed Types][a920] for information on how to use them. + ## 7 The Geb Model ###### \[in package GEB\] @@ -666,6 +696,7 @@ 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\] @@ -673,28 +704,33 @@ 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`][74bd] + - [generic-function] **CODOM** *CAT-MORPH* Grabs the codomain of the morphism. Returns a [`CAT-OBJ`][74bd] + - [generic-function] **CURRY-PROD** *CAT-MORPH CAT-LEFT CAT-RIGHT* Curries the given product type given the @@ -706,6 +742,7 @@ contained in various data structures Use [`GEB.MAIN:CURRY`][2cbc] instead. + ### 7.2 Geneircs ###### \[in package GEB.GENERICS\] @@ -719,6 +756,7 @@ The main documentation for the functionality is given here, with examples often given in the specific methods + - [generic-function] **GAPPLY** *MORPHISM OBJECT* Applies a given Moprhism to a given object. @@ -745,6 +783,7 @@ examples often given in the specific methods + - [generic-function] **MAYBE** *OBJECT* Wraps the given `OBJECT` into a Maybe monad The Maybe monad in this @@ -761,27 +800,32 @@ examples often given in the specific methods + - [generic-function] **TO-CIRCUIT** *MORPHISM NAME* Turns a `MORPHISM` into a Vampir circuit. the `NAME` is the given name of the output circuit. + - [generic-function] **TO-BITC** *MORPHISM* Turns a given `MORPHISM` into a [`GEB.BITC.SPEC:BITC`][e017] + - [generic-function] **TO-POLY** *MORPHISM* Turns a given `MORPHISM` into a [`GEB.POLY.SPEC:POLY`][8bf3] + - [generic-function] **TO-CAT** *CONTEXT TERM* Turns a `MORPHISM` with a context into Geb's Core category + - [generic-function] **TO-VAMPIR** *MORPHISM VALUES CONSTRAINTS* Turns a `MORPHISM` into a Vampir circuit, with concrete values. @@ -795,12 +839,13 @@ examples often given in the specific methods The `CONSTRAINTS` represent constraints that get creating + ### 7.3 Core Category ###### \[in package GEB.SPEC\] The underlying category of GEB. With [Subst Obj][c1b3] covering the -shapes and forms ([Objects][dbe7]) of data while [Subst Morph][d2d1] -deals with concrete [Morphisms][ada9] within the category. +shapes and forms (GEB-DOCS/DOCS:@OBJECTS) of data while [Subst Morph][d2d1] +deals with concrete GEB-DOCS/DOCS:@MORPHISMS within the category. From this category, most abstractions will be made, with [`SUBSTOBJ`][3173] serving as a concrete type layout, with @@ -812,6 +857,7 @@ A good example of this category at work can be found within the [Booleans][399c] section. + #### 7.3.1 Subst Obj This section covers the objects of the [`SUBSTMORPH`][57dc] @@ -820,12 +866,14 @@ category. Note that [`SUBSTOBJ`][3173] refers to the to the [open type][4a87] that allows for user extension. + - [type] **SUBSTOBJ** + - [class] **\** *[\][db35] [DIRECT-POINTWISE-MIXIN][e2b0] [META-MIXIN][4529] [CAT-OBJ][74bd]* - the class corresponding to [`SUBSTOBJ`][3173]. See [Open Types versus Closed Types][a920] + the class corresponding to [`SUBSTOBJ`][3173]. See GEB-DOCS/DOCS:@OPEN-CLOSED [`SUBSTOBJ`][3173] type is not a constructor itself, instead it's best viewed as the sum type, with the types below forming the @@ -840,6 +888,7 @@ type substobj = so0 + - [class] **PROD** *[\][fb79]* The [PRODUCT][06c6] object. Takes two [`CAT-OBJ`][74bd] values that @@ -863,6 +912,7 @@ type substobj = so0 Here we create a product of two [`GEB-BOOL:BOOL`][0ad4] types. + - [class] **COPROD** *[\][fb79]* the [CO-PRODUCT][8be5] object. Takes [`CAT-OBJ`][74bd] values that @@ -874,7 +924,7 @@ type substobj = so0 (coprod mcar mcadr) ``` - Where [CORPOD][7e58] is the constructor, [`MCAR`][f1ce] is the left choice of + Where [CORPOD][1f37] is the constructor, [`MCAR`][f1ce] is the left choice of the sum, and [`MCADR`][cc87] is the right choice of the sum. Example: @@ -887,6 +937,7 @@ type substobj = so0 values. + - [class] **SO0** *[\][fb79]* The Initial Object. This is sometimes known as the @@ -898,7 +949,7 @@ type substobj = so0 so0 ``` - where [`SO0`][5c7c] is [`THE`][c767] initial object. + where [`SO0`][5c7c] is [`THE`][311a] initial object. Example @@ -906,6 +957,7 @@ type substobj = so0 ` + - [class] **SO1** *[\][fb79]* The Terminal Object. This is sometimes referred to as the @@ -917,7 +969,7 @@ type substobj = so0 so1 ``` - where [`SO1`][5cfe] is [`THE`][c767] terminal object + where [`SO1`][5cfe] is [`THE`][311a] terminal object Example @@ -941,18 +993,23 @@ type substobj = so0 The [Accessors][cc51] specific to [Subst Obj][c1b3] + - [method] **MCAR** *(PROD PROD)* + - [method] **MCADR** *(PROD PROD)* + - [method] **MCAR** *(COPROD COPROD)* + - [method] **MCADR** *(COPROD COPROD)* + #### 7.3.2 Subst Morph The overarching types that categorizes the [`SUBSTMORPH`][57dc] @@ -961,14 +1018,16 @@ category. Note that [`SUBSTMORPH`][57dc] refers to the to the [open type][4a87] that allows for user extension. + - [type] **SUBSTMORPH** The morphisms of the [`SUBSTMORPH`][57dc] category + - [class] **\** *[DIRECT-POINTWISE-MIXIN][e2b0] [META-MIXIN][4529] [CAT-MORPH][a7af]* - the class type corresponding to [`SUBSTMORPH`][57dc]. See [Open Types versus Closed Types][a920] + the class type corresponding to [`SUBSTMORPH`][57dc]. See GEB-DOCS/DOCS:@OPEN-CLOSED [`SUBSTMORPH`][57dc] type is not a constructor itself, instead it's best viewed as the sum type, with the types below forming the @@ -994,6 +1053,7 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a [`SUBSTMORPH`][57dc] + - [class] **COMP** *[\][db35]* The composition morphism. Takes two [`CAT-MORPH`][a7af] values that get @@ -1041,6 +1101,7 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a + - [class] **CASE** *[\][db35]* Eliminates coproducts. Namely Takes two [`CAT-MORPH`][a7af] values, one @@ -1069,10 +1130,11 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a In the second example, we inject a term with the shape [`GEB-BOOL:BOOL`][0ad4] into a pair with the shape ([`SO1`][5cfe] × [`GEB-BOOL:BOOL`][0ad4]), then we use - [`MCASE`][cd11] to denote a morphism saying. [`IF`][684b] the input is of the shape `SO1`([`0`][5cfe] [`1`][f4ba]), + [`MCASE`][cd11] to denote a morphism saying. [`IF`][02ad] the input is of the shape `SO1`([`0`][5cfe] [`1`][f4ba]), then give us True, otherwise flip the value of the boolean coming in. + - [class] **INIT** *[\][db35]* The [INITIAL][8e11] Morphism, takes any [`CAT-OBJ`][74bd] and @@ -1097,6 +1159,7 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a In this example we are creating a unit value out of void. + - [class] **TERMINAL** *[\][db35]* The [`TERMINAL`][874b] morphism, Takes any [`CAT-OBJ`][74bd] and creates a @@ -1134,6 +1197,7 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a The fourth example is taking a [`GEB-BOOL:BOOL`][0ad4] and returning [`GEB-BOOL:TRUE`][f022]. + - [class] **PAIR** *[\][db35]* Introduces products. Namely Takes two [`CAT-MORPH`][a7af] values. When @@ -1164,11 +1228,13 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a projects back the `GEB-BOOL:BOOL` field as the second values. + - [class] **DISTRIBUTE** *[\][db35]* The distributive law + - [class] **INJECT-LEFT** *[\][db35]* The left injection morphism. Takes two [`CAT-OBJ`][74bd] values. It is @@ -1198,10 +1264,11 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a In the second example, we inject a term with the shape `SO1`([`0`][5cfe] [`1`][f4ba]) into a pair with the shape ([`SO1`][5cfe] × [`GEB-BOOL:BOOL`][0ad4]), then we use [`MCASE`][cd11] to denote a - morphism saying. [`IF`][684b] the input is of the shape `SO1`([`0`][5cfe] [`1`][f4ba]), then give us True, + morphism saying. [`IF`][02ad] the input is of the shape `SO1`([`0`][5cfe] [`1`][f4ba]), then give us True, otherwise flip the value of the boolean coming in. + - [class] **INJECT-RIGHT** *[\][db35]* The right injection morphism. Takes two [`CAT-OBJ`][74bd] values. It is @@ -1231,10 +1298,11 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a In the second example, we inject a term with the shape [`GEB-BOOL:BOOL`][0ad4] into a pair with the shape ([`SO1`][5cfe] × [`GEB-BOOL:BOOL`][0ad4]), then we use - [`MCASE`][cd11] to denote a morphism saying. [`IF`][684b] the input is of the shape `SO1`([`0`][5cfe] [`1`][f4ba]), + [`MCASE`][cd11] to denote a morphism saying. [`IF`][02ad] the input is of the shape `SO1`([`0`][5cfe] [`1`][f4ba]), then give us True, otherwise flip the value of the boolean coming in. + - [class] **PROJECT-LEFT** *[\][db35]* The [`LEFT` PROJECTION][5ae3]. Takes two @@ -1249,7 +1317,7 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a ``` Where [`<-LEFT`][2882] is the constructor, [`MCAR`][f1ce] is the left type of the - [PRODUCT][7e58] and [`MCADR`][cc87] is the right type of the [PRODUCT][7e58]. + [PRODUCT][1f37] and [`MCADR`][cc87] is the right type of the [PRODUCT][1f37]. Example: @@ -1264,6 +1332,7 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a ([`GEB-BOOL:BOOL`][0ad4] [×][06c6] [`SO1`][5cfe] [×][06c6] [`GEB-BOOL:BOOL`][0ad4]) + - [class] **PROJECT-RIGHT** *[\][db35]* The [`RIGHT` PROJECTION][06e0]. Takes two @@ -1278,7 +1347,7 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a ``` Where [`<-RIGHT`][0dfe] is the constructor, [`MCAR`][f1ce] is the right type of the - [PRODUCT][7e58] and [`MCADR`][cc87] is the right type of the [PRODUCT][7e58]. + [PRODUCT][1f37] and [`MCADR`][cc87] is the right type of the [PRODUCT][1f37]. Example: @@ -1294,82 +1363,103 @@ we can view this as automatically lifting a [`SUBSTOBJ`][3173] into a ([`GEB-BOOL:BOOL`][0ad4] [×][06c6] [`SO1`][5cfe] [×][06c6] [`GEB-BOOL:BOOL`][0ad4]) + - [class] **FUNCTOR** *[\][db35]* The [Accessors][cc51] specific to [Subst Morph][d2d1] + - [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.3 Realized Subst Objs This section covers the [`REALIZED-OBJECT`][73be] type. This @@ -1394,6 +1484,7 @@ type realized-object = so0 + - [type] **REALIZED-OBJECT** A realized object that can be sent into. @@ -1405,18 +1496,23 @@ type realized-object = so0 Lastly [`SO1`][5cfe] and [`SO0`][5c7c] represent the proper class + - [class] **LEFT** *[DIRECT-POINTWISE-MIXIN][e2b0]* + - [class] **RIGHT** *[DIRECT-POINTWISE-MIXIN][e2b0]* + - [function] **LEFT** *OBJ* + - [function] **RIGHT** *OBJ* + ### 7.4 Accessors ###### \[in package GEB.UTILS\] @@ -1425,75 +1521,88 @@ 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`][8c99] on a generic CLOS + Can be seen as calling [`CAR`][d5a2] on a generic CLOS [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **MCADR** *OBJ* - like [`MCAR`][f1ce] but for the [`CADR`][74ab] + like [`MCAR`][f1ce] but for the [`CADR`][caea] + - [generic-function] **MCADDR** *OBJ* - like [`MCAR`][f1ce] but for the [`CADDR`][8bb8] + like [`MCAR`][f1ce] but for the [`CADDR`][57e1] + - [generic-function] **MCADDDR** *OBJ* - like [`MCAR`][f1ce] but for the [`CADDDR`][1791] + like [`MCAR`][f1ce] but for the [`CADDDR`][47d6] + - [generic-function] **MCDR** *OBJ* - Similar to [`MCAR`][f1ce], however acts like a [`CDR`][2570] for - [classes][7e58] that we wish to view as a [`SEQUENCE`][b9c1] + Similar to [`MCAR`][f1ce], however acts like a [`CDR`][e012] for + [classes][1f37] that we wish to view as a [`SEQUENCE`][ae23] + - [generic-function] **OBJ** *OBJ* Grabs the underlying [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **NAME** *OBJ* the name of the given [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **FUNC** *OBJ* the function of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **PREDICATE** *OBJ* the `PREDICATE` of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **THEN** *OBJ* the then branch of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **ELSE** *OBJ* the then branch of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **CODE** *OBJ* the code of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + ### 7.5 Constructors ###### \[in package GEB.SPEC\] @@ -1501,11 +1610,13 @@ 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 @@ -1513,57 +1624,70 @@ here relate to instantiating a term More Ergonomic API variants for [`*SO0*`][e982] and [`*SO1*`][b960] + - [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.6 API Various forms and structures built on-top of [Core Category][cb9e] + - [method] **GAPPLY** *(MORPH \) OBJECT* My main documentation can be found on [`GAPPLY`][bb34] - I am the [`GAPPLY`][bb34] for [][7e58], the + I am the [`GAPPLY`][bb34] for [][1f37], the OBJECT that I expect is of type [`REALIZED-OBJECT`][73be]. See the documentation for [`REALIZED-OBJECT`][73be] for the forms it can take. @@ -1602,11 +1726,12 @@ Various forms and structures built on-top of [Core Category][cb9e] + - [method] **GAPPLY** *(MORPH OPAQUE-MORPH) OBJECT* My main documentation can be found on [`GAPPLY`][bb34] - I am the [`GAPPLY`][bb34] for a generic [OPAQUE-MOPRH][7e58] + I am the [`GAPPLY`][bb34] for a generic [OPAQUE-MOPRH][1f37] I simply dispatch [`GAPPLY`][bb34] on my interior code `lisp GEB> (gapply (comp geb-list:*car* geb-list:*cons*) @@ -1615,6 +1740,7 @@ Various forms and structures built on-top of [Core Category][cb9e] ` + - [method] **GAPPLY** *(MORPH OPAQUE) OBJECT* My main documentation can be found on [`GAPPLY`][bb34] @@ -1624,6 +1750,7 @@ Various forms and structures built on-top of [Core Category][cb9e] is likely just an object + #### 7.6.1 Booleans ###### \[in package GEB-BOOL\] @@ -1646,24 +1773,29 @@ We likewise define it with coproducts 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 @@ -1674,23 +1806,27 @@ The functions given work on this. + - [symbol-macro] **NOT** Turns a [`TRUE`][f022] into a [`FALSE`][31c5] and vice versa + - [symbol-macro] **AND** + - [symbol-macro] **OR** + #### 7.6.2 Lists ###### \[in package GEB-LIST\] Here we define out the idea of a List. It comes naturally from the concept of coproducts. Since we lack polymorphism this list is -concrete over [`GEB-BOOL:@GEB-BOOL`][section] In ML syntax it looks like +concrete over `GEB-BOOL:@GEB-BOOL` In ML syntax it looks like ```haskell data List = Nil | Cons Bool List @@ -1714,33 +1850,43 @@ We likewise define it with coproducts, with the recursive type being opaque The functions given work on this. + - [variable] **\*NIL\*** *NIL* + - [variable] **\*CONS-TYPE\*** *CONS* + - [variable] **\*LIST\*** *LIST* + - [variable] **\*CAR\*** *CAR* + - [variable] **\*CONS\*** *CONS-Μ* + - [variable] **\*CDR\*** *CDR* + - [symbol-macro] **CONS-\>LIST** + - [symbol-macro] **NIL-\>LIST** + - [variable] **\*CANONICAL-CONS-TYPE\*** *CONS* + #### 7.6.3 Translation Functions ###### \[in package GEB.TRANS\] @@ -1748,41 +1894,50 @@ These cover various conversions from [Subst Morph][d2d1] and [Subst Obj][c1b3] into other categorical data structures. + - [method] **TO-POLY** *(OBJ \)* + - [method] **TO-POLY** *(OBJ \)* + - [method] **TO-CIRCUIT** *(OBJ \) NAME* Turns a [Subst Morph][d2d1] to a Vamp-IR Term + - [method] **TO-BITC** *(OBJ \)* + #### 7.6.4 Utility ###### \[in package GEB.MAIN\] Various utility functions ontop of [Core Category][cb9e] + - [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. @@ -1814,9 +1969,11 @@ Various utility functions ontop of [Core Category][cb9e] + - [function] **COMMUTES** *X Y* + - [function] **COMMUTES-LEFT** *MORPH* swap the input [domain][9728] of the given [cat-morph][a7af] @@ -1835,23 +1992,29 @@ Various utility functions ontop of [Core Category][cb9e] ` + - [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`][ceb9] + Gets the cardinality of the given object, returns a [`FIXNUM`][3cde] + - [method] **SO-CARD-ALG** *(OBJ \)* + - [function] **CURRY** *F* Curries the given object, returns a [cat-morph][a7af] @@ -1865,7 +2028,7 @@ Various utility functions ontop of [Core Category][cb9e] then: (curry f): a → c^b - where c^b means c to the exponent of b ([`EXPT`][9bcb2] c b) + where c^b means c to the exponent of b ([`EXPT`][f97d] c b) ``` Γ, f : a × b → c, @@ -1877,6 +2040,7 @@ Various utility functions ontop of [Core Category][cb9e] + - [function] **COPROD-MOR** *F G* Given f : A → B and g : C → D gives appropriate morphism between @@ -1884,6 +2048,7 @@ Various utility functions ontop of [Core Category][cb9e] That is, the morphism part of the coproduct functor Geb x Geb → Geb + - [function] **PROD-MOR** *F G* Given f : A → B and g : C → D gives appropriate morphism between @@ -1891,12 +2056,14 @@ Various utility functions ontop of [Core Category][cb9e] This is the morphism part of the product functor Geb x Geb → Geb + - [function] **UNCURRY** *Y Z F* Given a morphism f : x → z^y and explicitly given y and z variables produces an uncurried version f' : x × y → z of said morphism + - [generic-function] **TEXT-NAME** *MORPH* Gets the name of the moprhism @@ -1904,9 +2071,10 @@ Various utility functions ontop of [Core Category][cb9e] These utilities are ontop of [`CAT-OBJ`][74bd] + - [method] **MAYBE** *(OBJ \)* - I recursively add maybe terms to all [][7e58] terms, + I recursively add maybe terms to all [][1f37] terms, for what maybe means checkout [my generic function documentation][65a4]. turning [products][06c6] of A x B into Maybe (Maybe A x Maybe B), @@ -1918,6 +2086,7 @@ These utilities are ontop of [`CAT-OBJ`][74bd] and `SO0`([`0`][5c7c] [`1`][7088]) into Maybe `SO0`([`0`][5c7c] [`1`][7088]) + ### 7.7 Examples PLACEHOLDER: TO SHOW OTHERS HOW `EXAMPLE`s WORK @@ -1937,6 +2106,7 @@ with GEB: + ## 8 Extension Sets for Categories ###### \[in package GEB.EXTENSION.SPEC\] @@ -1950,18 +2120,20 @@ Common Sub expressions represent repeat logic that can be found throughout any piece of code + - [class] **COMMON-SUB-EXPRESSION** *[DIRECT-POINTWISE-MIXIN][e2b0] [META-MIXIN][4529] [CAT-MORPH][a7af]* I represent common sub-expressions found throughout the code. I implement a few categorical extensions. I am a valid [`CAT-MORPH`][a7af] along with fulling the interface for the - GEB.POLY.SPEC:([`0`][7058] [`1`][78ef]) category. + GEB.POLY.SPEC:([`0`][9990] [`1`][4df2]) category. The name should come from an algorithm that automatically fines common sub-expressions and places the appropriate names. + - [function] **MAKE-COMMON-SUB-EXPRESSION** *&KEY OBJ NAME* The Opaque extension lets users write categorical objects and @@ -1969,56 +2141,69 @@ morphisms where their implementation hide the specifics of what types they are operating over + - [class] **OPAQUE** *[CAT-OBJ][74bd] [META-MIXIN][4529]* I represent an object where we want to hide the implementation details of what kind of [`GEB:SUBSTOBJ`][3173] I am. + - [class] **REFERENCE** *[CAT-OBJ][74bd] [CAT-MORPH][a7af] [DIRECT-POINTWISE-MIXIN][e2b0] [META-MIXIN][4529]* I represent a reference to an [`OPAQUE`][2fc2] identifier. + - [class] **OPAQUE-MORPH** *[CAT-MORPH][a7af] [META-MIXIN][4529]* This represents a morphsim where we want to deal with an [`OPAQUE`][2fc2] that we know intimate details of + - [method] **CODE** *(OPAQUE-MORPH OPAQUE-MORPH)* the code that represents the underlying morphsism + - [method] **DOM** *(OPAQUE-MORPH OPAQUE-MORPH)* The dom of the opaque morph + - [method] **CODOM** *(OPAQUE-MORPH OPAQUE-MORPH)* The codom of the opaque morph + - [method] **CODE** *(OPAQUE OPAQUE)* + - [method] **NAME** *(OPAQUE OPAQUE)* + - [method] **NAME** *(REFERENCE REFERENCE)* + - [function] **REFERENCE** *NAME* + - [function] **OPAQUE-MORPH** *CODE &KEY (DOM (DOM CODE)) (CODOM (CODOM CODE))* + - [function] **OPAQUE** *NAME CODE* + ## 9 The GEB GUI ###### \[in package GEB-GUI\] @@ -2026,6 +2211,7 @@ This section covers the suite of tools that help visualize geb objects and make the system nice to work with + ### 9.1 Visualizer The GEB visualizer deals with visualizing any objects found in the [Core Category][cb9e] @@ -2037,30 +2223,58 @@ if the visualizer gets a [Subst Obj][c1b3], then it shows the data layout of the term, showing what kind of data + - [function] **VISUALIZE** *OBJECT &OPTIONAL (ASYNC T)* Visualizes both [Subst Obj][c1b3] and [Subst Morph][d2d1] objects + - [function] **KILL-RUNNING** Kills all threads and open gui objects created by [`VISUALIZE`][ada5] + #### 9.1.1 Aiding the Visualizer One can aid the visualization process a bit, this can be done by -simply placing ALIAS around the object, this will place it +simply placing `ALIAS` around the object, this will place it in a box with a name to better identify it in the graphing procedure. + + +### 9.2 Export Visualizer + +This works like the normal visualizer except it exports it to a +file to be used by other projects or perhaps in papers + + + +- [function] **SVG** *OBJECT PATH &KEY (DEFAULT-VIEW (MAKE-INSTANCE 'SHOW-VIEW))* + + Runs the visualizer, outputting a static `SVG` image at the directory of choice. + + You can customize the view. By default it uses the show-view, which is + the default of the visualizer. + + A good example usage is + + ```lisp + GEB-TEST> (geb-gui:svg (shallow-copy-object geb-bool:and) "/tmp/foo.svg") + ``` + + -### 9.2 The GEB Graphizer + +### 9.3 The GEB Graphizer ###### \[in package GEB-GUI.GRAPHING\] This section covers the GEB Graph representation -#### 9.2.1 The GEB Graphizer Core + +#### 9.3.1 The GEB Graphizer Core ###### \[in package GEB-GUI.CORE\] This section covers the graphing procedure in order to turn a GEB @@ -2069,6 +2283,7 @@ 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 @@ -2088,7 +2303,7 @@ The core types that facilittate the functionality Π₂ ``` - An example of a [MERGE-NOTE][7e58] + An example of a [MERGE-NOTE][1f37] ```lisp (Case f g) @@ -2106,10 +2321,11 @@ The core types that facilittate the functionality ``` 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][7e58] examples, the + place down, where as in both of the [MERGE-NOTE][1f37] examples, the Note at the end is not pre-pended by any special information + - [class] **NODE** *[META-MIXIN][4529]* I represent a graphical node structure. I contain my children and a @@ -2121,20 +2337,25 @@ The core types that facilittate the functionality that goes to it in the meta table and recovering the note. + - [class] **NODE-NOTE** + - [class] **SQUASH-NOTE** This note should be squashed into another note and or node. + - [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. @@ -2152,14 +2373,17 @@ The core types that facilittate the functionality 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`][ff98]. @@ -2172,17 +2396,21 @@ The core types that facilittate the functionality 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`][1fbc] of the `NODE`. @@ -2191,18 +2419,21 @@ The core types that facilittate the functionality child in the list + - [function] **NOTORIZE-CHILDREN-WITH-INDEX-SCHEMA** *PREFIX NODE* Notorizes the node with a prefix appended with the subscripted number -#### 9.2.2 The GEB Graphizer Passes + +#### 9.3.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. @@ -2210,6 +2441,7 @@ ways that are intuitive to the user only display it in a more bearable way + ## 10 Bits (Boolean Circuit) Specification ###### \[in package GEB.BITC\] @@ -2217,30 +2449,36 @@ This covers a GEB view of Boolean Circuits. In particular this type will be used in translating GEB's view of Boolean Circuits into Vampir + ### 10.1 Bits Types ###### \[in package GEB.BITC.SPEC\] -This section covers the types of things one can find in the `BIT`s([`0`][6a3c] [`1`][2410]) +This section covers the types of things one can find in the `BIT`s([`0`][01b6] [`1`][2282]) constructors + - [type] **BITC** + - [class] **\** *[DIRECT-POINTWISE-MIXIN][e2b0] [CAT-MORPH][a7af]* + - [class] **COMPOSE** *[\][26d4]* composes the [`MCAR`][f1ce] and the [`MCADR`][cc87] + - [class] **FORK** *[\][26d4]* Copies the [`MCAR`][f1ce] of length n onto length 2\*n by copying its inputs (`MCAR`). + - [class] **PARALLEL** *[\][26d4]* ```lisp @@ -2262,6 +2500,7 @@ constructors and d where the [`MCAR`][f1ce] and [`MCADR`][cc87] run on subvectors of the input. + - [class] **SWAP** *[\][26d4]* ```lisp @@ -2278,28 +2517,33 @@ constructors + - [class] **ONE** *[\][26d4]* [`ONE`][cf10] represents the map from 0 onto 1 producing a vector with only 1 in it. + - [class] **ZERO** *[\][26d4]* [`ZERO`][fa6c] map from 0 onto 1 producing a vector with only 0 in it. + - [class] **IDENT** *[\][26d4]* [`IDENT`][c417] represents the identity + - [class] **DROP** *[\][26d4]* [`DROP`][f130] represents the unique morphism from n to 0. + - [class] **BRANCH** *[\][26d4]* ```lisp @@ -2322,65 +2566,77 @@ constructors [`MCAR`][f1ce] is ran, however if the bit is `1`, then the [`MCADR`][cc87] is ran. + ### 10.2 Bits (Boolean Circuit) Constructors ###### \[in package GEB.BITC.SPEC\] -Every accessor for each of the [`CLASS`][7e58]'s found here are from [Accessors][cc51] +Every accessor for each of the [`CLASS`][1f37]'s found here are from [Accessors][cc51] + - [function] **COMPOSE** *MCAR MCADR &REST ARGS* Creates a multiway constructor for [`COMPOSE`][ecb2] + - [function] **FORK** *MCAR* `FORK` ARG1 + - [function] **PARALLEL** *MCAR MCADR &REST ARGS* Creates a multiway constructor for [`PARALLEL`][46bc] + - [function] **SWAP** *MCAR MCADR* swap ARG1 and ARG2 + - [symbol-macro] **ONE** + - [symbol-macro] **ZERO** + - [function] **IDENT** *MCAR* ident ARG1 + - [function] **DROP** *MCAR* drop ARG1 + - [function] **BRANCH** *MCAR MCADR* branch with ARG1 or ARG2 + ### 10.3 Bits (Boolean Circuit) API ###### \[in package GEB.BITC.MAIN\] This covers the Bits (Boolean Circuit) API + - [method] **GAPPLY** *(MORPHISM \) (OBJECT BIT-VECTOR)* My My main documentation can be found on [`GAPPLY`][bb34] I am the [`GAPPLY`][bb34] for [``][26d4], the - `OBJECT` that I expect is of type [`NUMBER`][7dbb]. [`GAPPLY`][bb34] + `OBJECT` that I expect is of type [`NUMBER`][4dee]. [`GAPPLY`][bb34] reduces down to ordinary common lisp expressions rather straight forwardly @@ -2400,10 +2656,11 @@ This covers the Bits (Boolean Circuit) API + - [method] **GAPPLY** *(MORPHISM \) (OBJECT LIST)* I am a helper gapply function, where the second argument for - [``][26d4] is a list. See the docs for the [`BIT-VECTOR`][46ed] version for + [``][26d4] is a list. See the docs for the [`BIT-VECTOR`][5f51] version for the proper one. We do allow sending in a list like so ```lisp @@ -2422,66 +2679,79 @@ This covers the Bits (Boolean Circuit) API + - [method] **DOM** *(X \)* Gives the length of the bit vector the [``][26d4] moprhism takes + - [method] **CODOM** *(X \)* Gives the length of the bit vector the [``][26d4] morphism returns + ### 10.4 Bits (Boolean Circuit) Transformations ###### \[in package GEB.BITC.TRANS\] This covers transformation functions from + - [method] **TO-CIRCUIT** *(MORPHISM \) NAME* Turns a [`BITC`][e017] term into a Vamp-IR Gate with the given name + - [method] **TO-VAMPIR** *(OBJ COMPOSE) VALUES CONSTRAINTS* + - [method] **TO-VAMPIR** *(OBJ FORK) VALUES CONSTRAINTS* Copy input n intput bits into 2\*n output bits + - [method] **TO-VAMPIR** *(OBJ PARALLEL) VALUES CONSTRAINTS* Take n + m bits, execute car the n bits and cadr on the m bits and concat the results from car and cadr + - [method] **TO-VAMPIR** *(OBJ SWAP) VALUES CONSTRAINTS* Turn n + m bits into m + n bits by swapping + - [method] **TO-VAMPIR** *(OBJ ONE) VALUES CONSTRAINTS* Produce a bitvector of length 1 containing 1 + - [method] **TO-VAMPIR** *(OBJ ZERO) VALUES CONSTRAINTS* Produce a bitvector of length 1 containing 0 + - [method] **TO-VAMPIR** *(OBJ IDENT) VALUES CONSTRAINTS* turn n bits into n bits by doing nothing + - [method] **TO-VAMPIR** *(OBJ DROP) VALUES CONSTRAINTS* turn n bits into an empty bitvector + - [method] **TO-VAMPIR** *(OBJ BRANCH) VALUES CONSTRAINTS* Look at the first bit. @@ -2491,6 +2761,7 @@ This covers transformation functions from If its 1, run g on the remaining bits. + ## 11 Polynomial Specification ###### \[in package GEB.POLY\] @@ -2498,6 +2769,7 @@ This covers a GEB view of Polynomials. In particular this type will be used in translating GEB's view of Polynomials into Vampir + ### 11.1 Polynomial Types ###### \[in package GEB.POLY.SPEC\] @@ -2505,59 +2777,72 @@ This section covers the types of things one can find in the [`POLY`][8bf3] constructors + - [type] **POLY** + - [class] **\** *[GEB.MIXINS:DIRECT-POINTWISE-MIXIN][e2b0]* - -- [type] **IDENT** + + +- [class] **IDENT** *[\][b4a6]* The Identity Element - -- [type] **+** + + +- [class] **+** *[\][b4a6]* + + + +- [class] **\*** *[\][b4a6]* + + - -- [type] **\*** +- [class] **/** *[\][b4a6]* - -- [type] **/** + - -- [type] **-** +- [class] **-** *[\][b4a6]* - -- [type] **MOD** + - -- [type] **COMPOSE** +- [class] **MOD** *[\][b4a6]* - -- [type] **IF-ZERO** + + +- [class] **COMPOSE** *[\][b4a6]* + + + +- [class] **IF-ZERO** *[\][b4a6]* compare with zero: equal takes first branch; not-equal takes second branch - -- [type] **IF-LT** + + +- [class] **IF-LT** *[\][b4a6]* If the [`MCAR`][f1ce] argument is strictly less than the [`MCADR`][cc87] then the [`THEN`][bfa9] branch is taken, otherwise the [`ELSE`][365a] branch is taken. + ### 11.2 Polynomial API ###### \[in package GEB.POLY.MAIN\] This covers the polynomial API + - [method] **GAPPLY** *(MORPHISM \) OBJECT* My main documentation can be found on [`GAPPLY`][bb34] I am the [`GAPPLY`][bb34] for [`POLY:`][b4a6], the - `OBJECT` that I expect is of type [`NUMBER`][7dbb]. [`GAPPLY`][bb34] reduces down to + `OBJECT` that I expect is of type [`NUMBER`][4dee]. [`GAPPLY`][bb34] reduces down to ordinary common lisp expressions rather straight forwardly Some examples of me are @@ -2577,12 +2862,13 @@ This covers the polynomial API + - [method] **GAPPLY** *(MORPHISM INTEGER) OBJECT* My main documentation can be found on [`GAPPLY`][bb34] - I am the [`GAPPLY`][bb34] for [`INTEGER`][ac8a]s, the - `OBJECT` that I expect is of type [`NUMBER`][7dbb]. I simply return myself. + I am the [`GAPPLY`][bb34] for [`INTEGER`][9b12]s, the + `OBJECT` that I expect is of type [`NUMBER`][4dee]. I simply return myself. Some examples of me are @@ -2595,109 +2881,132 @@ This covers the polynomial API + ### 11.3 Polynomial Constructors ###### \[in package GEB.POLY.SPEC\] -Every accessor for each of the [`CLASS`][7e58]'s found here are from [Accessors][cc51] +Every accessor for each of the [`CLASS`][1f37]'s found here are from [Accessors][cc51] + - [symbol-macro] **IDENT** + - [function] **+** *MCAR MCADR &REST ARGS* - Creates a multiway constructor for [+][c144] + Creates a multiway constructor for [+][109b] + - [function] **\*** *MCAR MCADR &REST ARGS* - Creates a multiway constructor for [\*][0ae3] + Creates a multiway constructor for [\*][86f1] + - [function] **/** *MCAR MCADR &REST ARGS* - Creates a multiway constructor for [/][c2f9] + Creates a multiway constructor for [/][938a] + - [function] **-** *MCAR MCADR &REST ARGS* - Creates a multiway constructor for [-][2c5e] + Creates a multiway constructor for [-][d4fe] + - [function] **MOD** *MCAR MCADR* `MOD` ARG1 by ARG2 + - [function] **COMPOSE** *MCAR MCADR &REST ARGS* - Creates a multiway constructor for [`COMPOSE`][9162] + Creates a multiway constructor for [`COMPOSE`][ed72] + - [function] **IF-ZERO** *PRED THEN ELSE* checks if [`PREDICATE`][8da6] is zero then take the [`THEN`][bfa9] branch otherwise the [`ELSE`][365a] branch + - [function] **IF-LT** *MCAR MCADR THEN ELSE* Checks if the [`MCAR`][f1ce] is less than the [`MCADR`][cc87] and chooses the appropriate branch + ### 11.4 Polynomial Transformations ###### \[in package GEB.POLY.TRANS\] This covers transformation functions from + - [method] **TO-CIRCUIT** *(MORPHISM \) NAME* Turns a [`POLY`][8bf3] term into a Vamp-IR Gate with the given name + - [method] **TO-VAMPIR** *(OBJ INTEGER) VALUE LET-VARS* Numbers act like a constant function, ignoring input + - [method] **TO-VAMPIR** *(OBJ IDENT) VALUE LET-VARS* Identity acts as the identity function + - [method] **TO-VAMPIR** *(OBJ +) VALUE LET-VARS* Propagates the value and adds them + - [method] **TO-VAMPIR** *(OBJ \*) VALUE LET-VARS* Propagates the value and times them + - [method] **TO-VAMPIR** *(OBJ -) VALUE LET-VARS* Propagates the value and subtracts them + - [method] **TO-VAMPIR** *(OBJ /) VALUE LET-VARS* + - [method] **TO-VAMPIR** *(OBJ COMPOSE) VALUE LET-VARS* + - [method] **TO-VAMPIR** *(OBJ IF-ZERO) VALUE LET-VARS* The [`PREDICATE`][8da6] that comes in must be 1 or 0 for the formula to work out. + - [method] **TO-VAMPIR** *(OBJ IF-LT) VALUE LET-VARS* + - [method] **TO-VAMPIR** *(OBJ MOD) VALUE LET-VARS* + ## 12 The Simply Typed Lambda Calculus model ###### \[in package GEB.LAMBDA\] @@ -2769,6 +3078,7 @@ MAIN> + ### 12.1 Lambda Specification ###### \[in package GEB.LAMBDA.SPEC\] @@ -2776,6 +3086,7 @@ This covers the various the abstract data type that is the simply typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] terms. + - [type] **STLC** Type of untyped terms of [`STLC`][e373]. Each class of a term has a slot for a type, @@ -2783,6 +3094,7 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term represented as [SUBSTOBJ][3173]. + - [class] **\** *[DIRECT-POINTWISE-MIXIN][e2b0] [META-MIXIN][4529] [CAT-OBJ][74bd]* Class of untyped terms of simply typed lambda claculus. Given our @@ -2790,6 +3102,7 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term unit types as well as coproduct, product, and function types. + - [class] **ABSURD** *[\][b36a]* The [`ABSURD`][4710] term provides an element of an arbitrary type @@ -2812,11 +3125,12 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term This corresponds to the elimination rule of the empty type. Namely, given - $$\Gamma \vdash \text{tcod : Type}$$ and - $$\Gamma \vdash \text{term : so0}$$ one deduces - $$\Gamma \vdash \text{(absurd tcod term) : tcod}$$ + $$\Gamma \vdash \text\{tcod : Type\}$$ and + $$\Gamma \vdash \text\{term : so0\}$$ one deduces + $$\Gamma \vdash \text\{(absurd tcod term) : tcod\}$$ + - [class] **UNIT** *[\][b36a]* The unique term of the unit type, the latter represented by @@ -2836,9 +3150,10 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term we provide all terms untyped. This grammar corresponds to the introduction rule of the unit type. Namely - $$\Gamma \dashv \text{(unit) : so1}$$ + $$\Gamma \dashv \text\{(unit) : so1\}$$ + - [class] **LEFT** *[\][b36a]* Term of a coproduct type gotten by injecting into the left type of the coproduct. The formal grammar of @@ -2861,13 +3176,14 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term is [`TERM`][0171]. This corresponds to the introduction rule of the coproduct type. Namely, given - $$\Gamma \dashv \text{(ttype term) : Type}$$ and - $$\Gamma \dashv \text{rty : Type}$$ + $$\Gamma \dashv \text\{(ttype term) : Type\}$$ and + $$\Gamma \dashv \text\{rty : Type\}$$ with - $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce - $$\Gamma \dashv \text{(left rty term) : (coprod (ttype term) rty)}$$ + $$\Gamma \dashv \text\{term : (ttype term)\}$$ we deduce + $$\Gamma \dashv \text\{(left rty term) : (coprod (ttype term) rty)\}$$ + - [class] **RIGHT** *[\][b36a]* Term of a coproduct type gotten by injecting into the right type of @@ -2889,13 +3205,14 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term hence an [`STLC`][e373]) we are injecting is [`TERM`][0171]. This corresponds to the introduction rule of the coproduct type. Namely, given - $$\Gamma \dashv \text{(ttype term) : Type}$$ and - $$\Gamma \dashv \text{lty : Type}$$ + $$\Gamma \dashv \text\{(ttype term) : Type\}$$ and + $$\Gamma \dashv \text\{lty : Type\}$$ with - $$\Gamma \dashv \text{term : (ttype term)}$$ we deduce - $$\Gamma \dashv \text{(right lty term) : (coprod lty (ttype term))}$$ + $$\Gamma \dashv \text\{term : (ttype term)\}$$ we deduce + $$\Gamma \dashv \text\{(right lty term) : (coprod lty (ttype term))\}$$ + - [class] **CASE-ON** *[\][b36a]* A term of an arbutrary type provided by casing on a coproduct term. The @@ -2917,17 +3234,18 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term - (mcar (ttype on)) and (mcadr (ttype on)). This corresponds to the elimination rule of the coprodut type. Namely, given - $$\Gamma \vdash \text{on : (coprod (mcar (ttype on)) (mcadr (ttype on)))}$$ + $$\Gamma \vdash \text\{on : (coprod (mcar (ttype on)) (mcadr (ttype on)))\}$$ and - $$\text{(mcar (ttype on))} , \Gamma \vdash \text{ltm : (ttype ltm)}$$ - , $$\text{(mcadr (ttype on))} , \Gamma \vdash \text{rtm : (ttype ltm)}$$ + $$\text\{(mcar (ttype on))\} , \Gamma \vdash \text\{ltm : (ttype ltm)\}$$ + , $$\text\{(mcadr (ttype on))\} , \Gamma \vdash \text\{rtm : (ttype ltm)\}$$ we get - $$\Gamma \vdash \text{(case-on on ltm rtm) : (ttype ltm)}$$ + $$\Gamma \vdash \text\{(case-on on ltm rtm) : (ttype ltm)\}$$ Note that in practice we append contexts on the left as computation of [`INDEX`][5b8b] is done from the left. Otherwise, the rules are the same as in usual type theory if context was read from right to left. + - [class] **PAIR** *[\][b36a]* A term of the product type gotten by pairing a terms of a left and right @@ -2949,11 +3267,12 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term of the product. The grammar corresponds to the introdcution rule of the pair type. Given - $$\Gamma \vdash \text{ltm : (mcar (ttype (pair ltm rtm)))}$$ and - $$\Gamma \vdash \text{rtm : (mcadr (ttype (pair ltm rtm)))}$$ we have - $$\Gamma \vdash \text{(pair ltm rtm) : (ttype (pair ltm rtm))}$$ + $$\Gamma \vdash \text\{ltm : (mcar (ttype (pair ltm rtm)))\}$$ and + $$\Gamma \vdash \text\{rtm : (mcadr (ttype (pair ltm rtm)))\}$$ we have + $$\Gamma \vdash \text\{(pair ltm rtm) : (ttype (pair ltm rtm))\}$$ + - [class] **FST** *[\][b36a]* The first projection of a term of a product type. @@ -2977,6 +3296,7 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term on a term of a product type. + - [class] **SND** *[\][b36a]* The second projection of a term of a product type. @@ -3000,12 +3320,13 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term on a term of a product type. + - [class] **LAMB** *[\][b36a]* A term of a function type gotten by providing a term in the codomain of the function type by assuming one is given variables in the specified list of types. [`LAMB`][8cde] takes in the [`TDOM`][2c8c] - accessor a list of types - and hence of [SUBSTOBJ][7e58] - and in the + accessor a list of types - and hence of [SUBSTOBJ][1f37] - and in the [`TERM`][0171] a term - and hence an [`STLC`][e373]. The formal grammar of [`LAMB`][8cde] is: @@ -3027,9 +3348,9 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term For a list of length 1, corresponds to the introduction rule of the function type. Namely, given - $$\Gamma \vdash \text{tdom : Type}$$ and - $$\Gamma, \text{tdom} \vdash \text{term : (ttype term)}$$ we have - $$\Gamma \vdash \text{(lamb tdom term) : (so-hom-obj tdom (ttype term))}$$ + $$\Gamma \vdash \text\{tdom : Type\}$$ and + $$\Gamma, \text\{tdom\} \vdash \text\{term : (ttype term)\}$$ we have + $$\Gamma \vdash \text\{(lamb tdom term) : (so-hom-obj tdom (ttype term))\}$$ For a list of length n, this coreesponds to the iterated lambda type, e.g. @@ -3051,7 +3372,7 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term due to Geb's computational definition of the function type. - Note that [`INDEX`][5b8b] 0 in the above code is of type [SO1][7e58]. + Note that [`INDEX`][5b8b] 0 in the above code is of type [SO1][1f37]. So that after annotating the term, one gets ```lisp @@ -3074,13 +3395,14 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term usual type theory if context was read from right to left. + - [class] **APP** *[\][b36a]* A term of an arbitrary type gotten by applying a function of an iterated function type with a corresponding codomain iteratively to terms in the domains. [`APP`][04f2] takes as argument for the [`FUN`][cccf] accessor a function - and hence an [`STLC`][e373] - whose function type has domain an - iterated [`GEB:PROD`][06c6] of [SUBSTOBJ][clas] and for the [`TERM`][0171] + iterated [`GEB:PROD`][06c6] of [SUBSTOBJ][1f37] and for the [`TERM`][0171] a list of terms - and hence of [`STLC`][e373] - matching the types of the product. The formal grammar of [`APP`][04f2] is @@ -3102,9 +3424,9 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term For a one-argument term list, this corresponds to the elimination rule of the function type. Given - $$\Gamma \vdash \text{fun : (so-hom-obj (ttype term) y)}$$ and - $$\Gamma \vdash \text{term : (ttype term)}$$ we get - $$\Gamma \vdash \text{(app fun term) : y}$$ + $$\Gamma \vdash \text\{fun : (so-hom-obj (ttype term) y)\}$$ and + $$\Gamma \vdash \text\{term : (ttype term)\}$$ we get + $$\Gamma \vdash \text\{(app fun term) : y\}$$ For several arguments, this corresponds to successive function application. Using currying, this corresponds to, given @@ -3125,6 +3447,7 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term in the codomain counted from the left. + - [class] **INDEX** *[\][b36a]* The variable term of an arbitrary type in a context. The formal @@ -3144,14 +3467,15 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term natural number indicating the position of a type in a context. This corresponds to the variable rule. Namely given a context - $$\Gamma\_1 , \ldots , \Gamma\_{pos} , \ldots , \Gamma\_k $$ we have + $$\Gamma\_1 , \ldots , \Gamma\_\{pos\} , \ldots , \Gamma\_k $$ we have - $$\Gamma\_1 , \ldots , \Gamma\_k \vdash \text{(index pos) :} \Gamma\_{pos}$$ + $$\Gamma\_1 , \ldots , \Gamma\_k \vdash \text\{(index pos) :\} \Gamma\_\{pos\}$$ Note that we add contexts on the left rather than on the right contra classical type-theoretic notation. + - [class] **ERR** *[\][b36a]* An error term of a type supplied by the user. The formal grammar of @@ -3165,231 +3489,286 @@ typed lambda calculus within GEB. The class presents untyped [`STLC`][e373] term have [`TTYPE`][134c] a possibly empty accessor. + - [function] **ABSURD** *TCOD TERM &KEY (TTYPE NIL)* + - [function] **UNIT** *&KEY (TTYPE NIL)* + - [function] **LEFT** *RTY TERM &KEY (TTYPE NIL)* + - [function] **RIGHT** *LTY TERM &KEY (TTYPE NIL)* + - [function] **CASE-ON** *ON LTM RTM &KEY (TTYPE NIL)* + - [function] **PAIR** *LTM RTM &KEY (TTYPE NIL)* + - [function] **FST** *TERM &KEY (TTYPE NIL)* + - [function] **SND** *TERM &KEY (TTYPE NIL)* + - [function] **LAMB** *TDOM TERM &KEY (TTYPE NIL)* + - [function] **APP** *FUN TERM &KEY (TTYPE NIL)* + - [function] **INDEX** *POS &KEY (TTYPE NIL)* + - [function] **ERR** *TTYPE* Accessors of [`ABSURD`][4710] + - [method] **TCOD** *(ABSURD ABSURD)* An arbitrary type + - [method] **TERM** *(ABSURD ABSURD)* A term of the empty type + - [method] **TTYPE** *(ABSURD ABSURD)* Accessors of [`UNIT`][0433] + - [method] **TTYPE** *(UNIT UNIT)* Accessors of [`LEFT`][56b3] + - [method] **RTY** *(LEFT LEFT)* Right argument of coproduct type + - [method] **TERM** *(LEFT LEFT)* Term of the left argument of coproduct type + - [method] **TTYPE** *(LEFT LEFT)* Accessors of [`RIGHT`][48fc] + - [method] **LTY** *(RIGHT RIGHT)* Left argument of coproduct type + - [method] **TERM** *(RIGHT RIGHT)* Term of the right argument of coproduct type + - [method] **TTYPE** *(RIGHT RIGHT)* Accessors of [`CASE-ON`][3f9d] + - [method] **ON** *(CASE-ON CASE-ON)* Term of coproduct type + - [method] **LTM** *(CASE-ON CASE-ON)* Term in context of left argument of coproduct type + - [method] **RTM** *(CASE-ON CASE-ON)* Term in context of right argument of coproduct type + - [method] **TTYPE** *(CASE-ON CASE-ON)* Accessors of [`PAIR`][5dae] + - [method] **LTM** *(PAIR PAIR)* Term of left argument of the product type + - [method] **RTM** *(PAIR PAIR)* Term of right argument of the product type + - [method] **TTYPE** *(PAIR PAIR)* Accessors of [`FST`][b4a5] + - [method] **TERM** *(FST FST)* Term of product type + - [method] **TTYPE** *(FST FST)* Accessors of [`SND`][0424] + - [method] **TERM** *(SND SND)* Term of product type + - [method] **TTYPE** *(SND SND)* Accessors of [`LAMB`][8cde] + - [method] **TDOM** *(LAMB LAMB)* Domain of the lambda term + - [method] **TERM** *(LAMB LAMB)* Term of the codomain mapped to given a variable of tdom + - [method] **TTYPE** *(LAMB LAMB)* Accessors of [`APP`][04f2] + - [method] **FUN** *(APP APP)* Term of exponential type + - [method] **TERM** *(APP APP)* List of Terms of the domain + - [method] **TTYPE** *(APP APP)* Accessors of [`INDEX`][5b8b] + - [method] **POS** *(INDEX INDEX)* Position of type + - [method] **TTYPE** *(INDEX INDEX)* Accessors of [`ERR`][3a9f] + - [method] **TTYPE** *(ERR ERR)* + - [generic-function] **TCOD** *OBJ* + - [generic-function] **TDOM** *OBJ* + - [generic-function] **TERM** *OBJ* + - [generic-function] **RTY** *OBJ* + - [generic-function] **LTY** *OBJ* + - [generic-function] **LTM** *OBJ* + - [generic-function] **RTM** *OBJ* + - [generic-function] **ON** *OBJ* + - [generic-function] **FUN** *OBJ* + - [generic-function] **POS** *OBJ* + - [generic-function] **TTYPE** *OBJ* + ### 12.2 Main functionality ###### \[in package GEB.LAMBDA.MAIN\] This covers the main API for the [`STLC`][e373] module + - [generic-function] **ANN-TERM1** *CTX TTERM* Given a list of [`SUBSTOBJ`][3173] objects with @@ -3411,7 +3790,7 @@ This covers the main API for the [`STLC`][e373] module (ann-term1 (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0)))) ``` - produces an error trying to use [`HOM-COD`][b324]. This warning applies to other + produces an error trying to use. This warning applies to other functions taking in context and terms below as well. Moreover, note that for terms whose typing needs addition of new context @@ -3427,15 +3806,8 @@ This covers the main API for the [`STLC`][e373] module as we count indeces from the left of the context while appending new types to the context on the left as well. For more info check [`LAMB`][8cde] - -- [function] **HOM-COD** *CTX F* - - Given a context of [`SUBSTOBJ`][3173] with occurences of - [`SO-HOM-OBJ`][07dd] replaced by [`FUN-TYPE`][8dcc], and similarly - an [`STLC`][e373] term of the stand-in for the hom object, produces the stand-in - to the codomain. - + - [function] **INDEX-CHECK** *I CTX* Given an natural number `I` and a context, checks that the context is of @@ -3443,6 +3815,7 @@ This covers the main API for the [`STLC`][e373] module from the left starting with 0. + - [function] **FUN-TO-HOM** *T1* Given a [`SUBSTOBJ`][3173] whose subobjects might have a @@ -3457,6 +3830,7 @@ This covers the main API for the [`STLC`][e373] module + - [function] **ANN-TERM2** *TTERM* Given an [`STLC`][e373] term with a [`TTYPE`][134c] accessor from @@ -3465,6 +3839,7 @@ This covers the main API for the [`STLC`][e373] module [`SUBSTOBJ`][3173] objects. + - [function] **ANNOTATED-TERM** *CTX TERM* Given a context consisting of a list of [`SUBSTOBJ`][3173] @@ -3475,6 +3850,7 @@ This covers the main API for the [`STLC`][e373] module which is a pure [`SUBSTOBJ`][3173] + - [function] **TYPE-OF-TERM-W-FUN** *CTX TTERM* Given a context consisting of a list of [`SUBSTOBJ`][3173] with @@ -3484,6 +3860,7 @@ This covers the main API for the [`STLC`][e373] module occurences of [`SO-HOM-OBJ`][07dd] replaced by [`FUN-TYPE`][8dcc]. + - [function] **TYPE-OF-TERM** *CTX TTERM* Given a context consisting of a list of [`SUBSTOBJ`][3173] with @@ -3493,6 +3870,7 @@ This covers the main API for the [`STLC`][e373] module which is a pure [`SUBSTOBJ`][3173]. + - [generic-function] **WELL-DEFP** *CTX TTERM* Given a context consisting of a list of [`SUBSTOBJ`][3173] @@ -3504,6 +3882,7 @@ This covers the main API for the [`STLC`][e373] module nil + - [class] **FUN-TYPE** *[DIRECT-POINTWISE-MIXIN][e2b0] [CAT-OBJ][74bd]* Stand-in for the [`SO-HOM-OBJ`][07dd] object. It does not have @@ -3514,20 +3893,25 @@ This covers the main API for the [`STLC`][e373] module pointwise. + - [function] **FUN-TYPE** *MCAR MCADR* + - [function] **ERRORP** *TTERM* Evaluates to true iff the term has an error subterm. + - [method] **MCAR** *(FUN-TYPE FUN-TYPE)* + - [method] **MCADR** *(FUN-TYPE FUN-TYPE)* + - [method] **MAYBE** *(OBJECT FUN-TYPE)* I recursively add maybe terms to my domain and codomain, and even @@ -3546,6 +3930,7 @@ This covers the main API for the [`STLC`][e373] module for what maybe means checkout [my generic function documentation][65a4]. + ### 12.3 Transition Functions ###### \[in package GEB.LAMBDA.TRANS\] @@ -3560,6 +3945,7 @@ Thus if the [``][b36a] term contains free variables, then call any other transition functions + - [method] **TO-CAT** *CONTEXT (TTERM \)* Compiles a checked term in said context to a Geb morphism. If the term has @@ -3567,6 +3953,7 @@ any other transition functions according to the term model interpretation of [`STLC`][e373] + - [method] **TO-POLY** *(OBJ \)* I convert a lambda term into a [`GEB.POLY.SPEC:POLY`][8bf3] term @@ -3578,6 +3965,7 @@ any other transition functions calling me + - [method] **TO-BITC** *(OBJ \)* I convert a lambda term into a [`GEB.BITC.SPEC:BITC`][e017] term @@ -3589,6 +3977,7 @@ any other transition functions calling me + - [method] **TO-CIRCUIT** *(OBJ \) NAME* I convert a lambda term into a vampir term @@ -3600,14 +3989,16 @@ any other transition functions calling me + #### 12.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 )][78ef] context into a + Converts a generic [(CODE )][4df2] context into a [`SUBSTMORPH`][57dc]. Note that usually contexts can be interpreted in a category as a $Sigma$-type$, which in a non-dependent setting gives us a usual [`PROD`][06c6] @@ -3621,11 +4012,13 @@ These are utility functions relating to translating lambda terms to other types + - [function] **SO-HOM** *DOM COD* Computes the hom-object of two [`SUBSTMORPH`][57dc]s + ## 13 Mixins ###### \[in package GEB.MIXINS\] @@ -3634,16 +4027,18 @@ project. Overall all these offer various services to the rest of the project + ### 13.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`][96d0]-able adhoc. The pointwise API, +checking if two objects are [`EQUAL`][3fb5]-able adhoc. The pointwise API, however, derives the behavior and naturally allows such idioms + - [class] **POINTWISE-MIXIN** Provides the service of giving point wise @@ -3654,6 +4049,7 @@ due to this we can instead compare only the slots defined directly in our class + - [class] **DIRECT-POINTWISE-MIXIN** *[POINTWISE-MIXIN][445d]* Works like [`POINTWISE-MIXIN`][445d], however functions on @@ -3663,6 +4059,7 @@ in our class Further all `DIRECT-POINTWISE-MIXIN`'s are [`POINTWISE-MIXIN`][445d]'s + ### 13.2 Pointwise API These are the general API functions on any class that have the @@ -3673,35 +4070,41 @@ be built off the key-value pair of the raw object form, while [`OBJ-EQUALP`][c111] 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`][592c] [`1`][98f9])'s are +traversal as `LIST`([`0`][79d8] [`1`][6d9f])'s are + - [generic-function] **TO-POINTWISE-LIST** *OBJ* - Turns a given object into a pointwise `LIST`([`0`][592c] [`1`][98f9]). listing - the [`KEYWORD`][4850] slot-name next to their value. + Turns a given object into a pointwise `LIST`([`0`][79d8] [`1`][6d9f]). listing + the [`KEYWORD`][077a] 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`][a802] [`EQUALP`][c721], which does the much + [`STANDARD-OBJECT`][a843] [`EQUALP`][2ff3], 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 + - [function] **MAP-POINTWISE** *FUNCTION OBJ* + - [function] **REDUCE-POINTWISE** *FUNCTION OBJ INITIAL* + ### 13.3 Mixins Examples Let's see some example uses of [`POINTWISE-MIXIN`][445d]: @@ -3717,6 +4120,7 @@ Let's see some example uses of [`POINTWISE-MIXIN`][445d]: + ### 13.4 Metadata Mixin Metadata is a form of meta information about a particular @@ -3729,6 +4133,7 @@ For this task we offer the [`META-MIXIN`][4529] 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 @@ -3739,6 +4144,7 @@ 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 @@ -3751,15 +4157,17 @@ it like an ordinary hashtable 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 + #### 13.4.1 Performance -The data stored is at the [`CLASS`][7e58] level. So having your type take the +The data stored is at the [`CLASS`][1f37] level. So having your type take the [`META-MIXIN`][4529] does interfere with the cache. Due to concerns about meta information being populated over time, the @@ -3801,6 +4209,7 @@ storage inside metadata be separated into volatile and stable storage. + ## 14 Geb Utilities ###### \[in package GEB.UTILS\] @@ -3808,6 +4217,7 @@ 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. @@ -3836,7 +4246,7 @@ used throughout the GEB codebase `(or wire constant)) ``` - Example usage of this can be used with [`typep`][d908] + Example usage of this can be used with [`typep`][0895] ```common-lisp (typep '(1 . 23) '(list-of fixnum)) @@ -3862,16 +4272,18 @@ used throughout the GEB codebase + - [function] **SYMBOL-TO-KEYWORD** *SYMBOL* - Turns a [symbol][7f9f] into a [keyword][4850] + Turns a [symbol][e5af] into a [keyword][077a] + - [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][bf07] instead of [`DEFPACKAGE`][42d7]. + to do the [export][0c4f] instead of [`DEFPACKAGE`][9b43]. This is more modular thank [MGL-PAX:DEFINE-PACKAGE](https://melisgl.Githubc.io/mgl-pax-world/mgl-pax-manual.html#MGL-PAX:DEFINE-PACKAGE%20MGL-PAX:MACRO) @@ -3890,27 +4302,31 @@ used throughout the GEB codebase + - [function] **SUBCLASS-RESPONSIBILITY** *OBJ* Denotes that the given method is the subclasses responsibility. Inspired from Smalltalk + - [function] **SHALLOW-COPY-OBJECT** *ORIGINAL* + - [generic-function] **COPY-INSTANCE** *OBJECT &REST INITARGS &KEY &ALLOW-OTHER-KEYS* Makes and returns a shallow copy of `OBJECT`. An uninitialized object of the same class as `OBJECT` is allocated by - calling [`ALLOCATE-INSTANCE`][a859]. For all slots returned by + calling [`ALLOCATE-INSTANCE`][868b]. For all slots returned by CLASS-SLOTS, the returned object has the same slot values and slot-unbound status as `OBJECT`. - [`REINITIALIZE-INSTANCE`][1456] is called to update the copy with `INITARGS`. + [`REINITIALIZE-INSTANCE`][1c95] is called to update the copy with `INITARGS`. + - [macro] **MAKE-PATTERN** *OBJECT-NAME &REST CONSTRUCTOR-NAMES* make pattern matching position style instead of record style. This @@ -3933,21 +4349,25 @@ used throughout the GEB codebase + - [function] **NUMBER-TO-DIGITS** *NUMBER &OPTIONAL REM* - turns an [`INTEGER`][ac8a] into a list of its digits + turns an [`INTEGER`][9b12] 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`][ac8a] into a subscripted [`STRING`][4267] + Turns an [`INTEGER`][9b12] into a subscripted [`STRING`][b93c] + - [function] **APPLY-N** *TIMES F INITIAL* Applies a function, f, n `TIMES` to the `INITIAL` values @@ -3959,6 +4379,7 @@ used throughout the GEB codebase + ### 14.1 Accessors These functions are generic lenses of the GEB codebase. If a class is @@ -3966,75 +4387,88 @@ 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`][8c99] on a generic CLOS + Can be seen as calling [`CAR`][d5a2] on a generic CLOS [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **MCADR** *OBJ* - like [`MCAR`][f1ce] but for the [`CADR`][74ab] + like [`MCAR`][f1ce] but for the [`CADR`][caea] + - [generic-function] **MCADDR** *OBJ* - like [`MCAR`][f1ce] but for the [`CADDR`][8bb8] + like [`MCAR`][f1ce] but for the [`CADDR`][57e1] + - [generic-function] **MCADDDR** *OBJ* - like [`MCAR`][f1ce] but for the [`CADDDR`][1791] + like [`MCAR`][f1ce] but for the [`CADDDR`][47d6] + - [generic-function] **MCDR** *OBJ* - Similar to [`MCAR`][f1ce], however acts like a [`CDR`][2570] for - [classes][7e58] that we wish to view as a [`SEQUENCE`][b9c1] + Similar to [`MCAR`][f1ce], however acts like a [`CDR`][e012] for + [classes][1f37] that we wish to view as a [`SEQUENCE`][ae23] + - [generic-function] **OBJ** *OBJ* Grabs the underlying [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **NAME** *OBJ* the name of the given [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **FUNC** *OBJ* the function of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **PREDICATE** *OBJ* the `PREDICATE` of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **THEN** *OBJ* the then branch of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **ELSE** *OBJ* the then branch of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + - [generic-function] **CODE** *OBJ* the code of the [object](http://www.lispworks.com/documentation/HyperSpec/Body/26_glo_o.htm#object) + ## 15 Testing ###### \[in package GEB-TEST\] @@ -4046,6 +4480,7 @@ Please read the 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 @@ -4063,9 +4498,11 @@ features and how to better lay out future tests + - [function] **RUN-TESTS-ERROR** + - [function] **CODE-COVERAGE** *&OPTIONAL (PATH NIL)* generates code coverage, for CCL the coverage can be found at @@ -4077,44 +4514,49 @@ features and how to better lay out future tests simply run this function to generate a fresh one [0171]: #x-28GEB-2ELAMBDA-2ESPEC-3ATERM-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:TERM GENERIC-FUNCTION" + [01b6]: http://www.lispworks.com/documentation/HyperSpec/Body/f_bt_sb.htm "BIT (MGL-PAX:CLHS FUNCTION)" [0251]: #x-28GEB-2EPOLY-2EMAIN-3A-40POLY-API-20MGL-PAX-3ASECTION-29 "Polynomial API" + [02ad]: http://www.lispworks.com/documentation/HyperSpec/Body/s_if.htm "IF (MGL-PAX:CLHS MGL-PAX:MACRO)" [0424]: #x-28GEB-2ELAMBDA-2ESPEC-3ASND-20CLASS-29 "GEB.LAMBDA.SPEC:SND CLASS" [0433]: #x-28GEB-2ELAMBDA-2ESPEC-3AUNIT-20CLASS-29 "GEB.LAMBDA.SPEC:UNIT CLASS" [04f2]: #x-28GEB-2ELAMBDA-2ESPEC-3AAPP-20CLASS-29 "GEB.LAMBDA.SPEC:APP CLASS" [0609]: #x-28GEB-2ELAMBDA-2ETRANS-3A-40UTILITY-20MGL-PAX-3ASECTION-29 "Utility Functionality" [06c6]: #x-28GEB-2ESPEC-3APROD-20CLASS-29 "GEB.SPEC:PROD CLASS" [06e0]: #x-28GEB-2ESPEC-3APROJECT-RIGHT-20CLASS-29 "GEB.SPEC:PROJECT-RIGHT CLASS" + [077a]: http://www.lispworks.com/documentation/HyperSpec/Body/t_kwd.htm "KEYWORD (MGL-PAX:CLHS TYPE)" [07dd]: #x-28GEB-2EMAIN-3ASO-HOM-OBJ-20FUNCTION-29 "GEB.MAIN:SO-HOM-OBJ FUNCTION" + [0895]: http://www.lispworks.com/documentation/HyperSpec/Body/f_typep.htm "TYPEP (MGL-PAX:CLHS FUNCTION)" [0ad4]: #x-28GEB-BOOL-3ABOOL-20MGL-PAX-3ASYMBOL-MACRO-29 "GEB-BOOL:BOOL MGL-PAX:SYMBOL-MACRO" - [0ae3]: #x-28GEB-2EPOLY-2ESPEC-3A-2A-20TYPE-29 "GEB.POLY.SPEC:* TYPE" + [0c4f]: http://www.lispworks.com/documentation/HyperSpec/Body/f_export.htm "EXPORT (MGL-PAX:CLHS FUNCTION)" [0dfe]: #x-28GEB-2ESPEC-3A-3C-RIGHT-20FUNCTION-29 "GEB.SPEC:<-RIGHT FUNCTION" [0e00]: #x-28GEB-DOCS-2FDOCS-3A-40YONEDA-LEMMA-20MGL-PAX-3ASECTION-29 "The Yoneda Lemma" [0efa]: #x-28GEB-2EEXTENSION-2ESPEC-3A-40GEB-EXTENSIONS-20MGL-PAX-3ASECTION-29 "Extension Sets for Categories" [0f3e]: #x-28GEB-2EPOLY-2ETRANS-3A-40POLY-TRANS-20MGL-PAX-3ASECTION-29 "Polynomial Transformations" + [109b]: #x-28GEB-2EPOLY-2ESPEC-3A-2B-20CLASS-29 "GEB.POLY.SPEC:+ CLASS" [134c]: #x-28GEB-2ELAMBDA-2ESPEC-3ATTYPE-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:TTYPE GENERIC-FUNCTION" - [1456]: http://www.lispworks.com/documentation/HyperSpec/Body/f_reinit.htm "REINITIALIZE-INSTANCE FUNCTION" [15a3]: #x-28GEB-2ELAMBDA-2ESPEC-3ALTY-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:LTY GENERIC-FUNCTION" [1774]: #x-28GEB-2EBITC-2ESPEC-3ABRANCH-20FUNCTION-29 "GEB.BITC.SPEC:BRANCH FUNCTION" - [1791]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CADDDR FUNCTION" [1b98]: #x-28GEB-GUI-2EGRAPHING-3A-40GRAPHING-MANUAL-20MGL-PAX-3ASECTION-29 "The GEB Graphizer" [1c91]: #x-28GEB-LIST-3A-40GEB-LIST-20MGL-PAX-3ASECTION-29 "Lists" + [1c95]: http://www.lispworks.com/documentation/HyperSpec/Body/f_reinit.htm "REINITIALIZE-INSTANCE (MGL-PAX:CLHS GENERIC-FUNCTION)" + [1f37]: http://www.lispworks.com/documentation/HyperSpec/Body/t_class.htm "CLASS (MGL-PAX:CLHS CLASS)" [1fbc]: #x-28GEB-GUI-2ECORE-3ACHILDREN-20GENERIC-FUNCTION-29 "GEB-GUI.CORE:CHILDREN GENERIC-FUNCTION" [2172]: #x-28GEB-2EBITC-2ESPEC-3A-40BITC-20MGL-PAX-3ASECTION-29 "Bits Types" [2276]: #x-28GEB-2EUTILS-3ASUBCLASS-RESPONSIBILITY-20FUNCTION-29 "GEB.UTILS:SUBCLASS-RESPONSIBILITY FUNCTION" - [2410]: http://www.lispworks.com/documentation/HyperSpec/Body/t_bit.htm "BIT TYPE" - [2570]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CDR FUNCTION" + [2282]: http://www.lispworks.com/documentation/HyperSpec/Body/t_bit.htm "BIT (MGL-PAX:CLHS TYPE)" [25f0]: #x-28GEB-DOCS-2FDOCS-3A-40GLOSSARY-20MGL-PAX-3ASECTION-29 "Glossary" [26d4]: #x-28GEB-2EBITC-2ESPEC-3A-3CBITC-3E-20CLASS-29 "GEB.BITC.SPEC: CLASS" [2882]: #x-28GEB-2ESPEC-3A-3C-LEFT-20FUNCTION-29 "GEB.SPEC:<-LEFT FUNCTION" [29b7]: #x-28GEB-DOCS-2FDOCS-3A-40AGDA-20MGL-PAX-3ASECTION-29 "Geb's Agda Code" [2ad4]: #x-28GEB-2ESPEC-3A-40GEB-CONSTRUCTORS-20MGL-PAX-3ASECTION-29 "Constructors" - [2c5e]: #x-28GEB-2EPOLY-2ESPEC-3A--20TYPE-29 "GEB.POLY.SPEC:- TYPE" [2c8c]: #x-28GEB-2ELAMBDA-2ESPEC-3ATDOM-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:TDOM GENERIC-FUNCTION" [2cbc]: #x-28GEB-2EMAIN-3ACURRY-20FUNCTION-29 "GEB.MAIN:CURRY FUNCTION" [2eb9]: #x-28GEB-2EGENERICS-3ATO-POLY-20GENERIC-FUNCTION-29 "GEB.GENERICS:TO-POLY GENERIC-FUNCTION" [2ebc]: #x-28GEB-2EBITC-2ETRANS-3A-40BITC-TRANS-20MGL-PAX-3ASECTION-29 "Bits (Boolean Circuit) Transformations" [2fc2]: #x-28GEB-2EEXTENSION-2ESPEC-3AOPAQUE-20CLASS-29 "GEB.EXTENSION.SPEC:OPAQUE CLASS" [2fcf]: #x-28GEB-2EMIXINS-3A-40POINTWISE-API-20MGL-PAX-3ASECTION-29 "Pointwise API" + [2ff3]: http://www.lispworks.com/documentation/HyperSpec/Body/f_equalp.htm "EQUALP (MGL-PAX:CLHS FUNCTION)" + [311a]: http://www.lispworks.com/documentation/HyperSpec/Body/s_the.htm "THE (MGL-PAX:CLHS MGL-PAX:MACRO)" [315f]: #x-28GEB-2ESPEC-3AALIAS-20MGL-PAX-3AMACRO-29 "GEB.SPEC:ALIAS MGL-PAX:MACRO" [3173]: #x-28GEB-2ESPEC-3ASUBSTOBJ-20TYPE-29 "GEB.SPEC:SUBSTOBJ TYPE" [31c5]: #x-28GEB-BOOL-3AFALSE-20MGL-PAX-3ASYMBOL-MACRO-29 "GEB-BOOL:FALSE MGL-PAX:SYMBOL-MACRO" @@ -4123,162 +4565,157 @@ features and how to better lay out future tests [3686]: #x-28GEB-DOCS-2FDOCS-3A-40ORIGINAL-EFFORTS-20MGL-PAX-3ASECTION-29 "Original Efforts" [399c]: #x-28GEB-BOOL-3A-40GEB-BOOL-20MGL-PAX-3ASECTION-29 "Booleans" [3a9f]: #x-28GEB-2ELAMBDA-2ESPEC-3AERR-20CLASS-29 "GEB.LAMBDA.SPEC:ERR CLASS" + [3cde]: http://www.lispworks.com/documentation/HyperSpec/Body/t_fixnum.htm "FIXNUM (MGL-PAX:CLHS TYPE)" [3d47]: #x-28GEB-DOCS-2FDOCS-3A-40GETTING-STARTED-20MGL-PAX-3ASECTION-29 "Getting Started" [3f85]: #x-28GEB-2ELAMBDA-2ESPEC-3APOS-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:POS GENERIC-FUNCTION" [3f9d]: #x-28GEB-2ELAMBDA-2ESPEC-3ACASE-ON-20CLASS-29 "GEB.LAMBDA.SPEC:CASE-ON CLASS" + [3fb5]: http://www.lispworks.com/documentation/HyperSpec/Body/f_equal.htm "EQUAL (MGL-PAX:CLHS FUNCTION)" [4044]: #x-28GEB-DOCS-2FDOCS-3A-40COVERAGE-20MGL-PAX-3ASECTION-29 "code coverage" [414c]: #x-28GEB-2EBITC-2ESPEC-3ABRANCH-20CLASS-29 "GEB.BITC.SPEC:BRANCH CLASS" [417f]: #x-28GEB-TEST-3ACODE-COVERAGE-20FUNCTION-29 "GEB-TEST:CODE-COVERAGE FUNCTION" - [4267]: http://www.lispworks.com/documentation/HyperSpec/Body/t_string.htm "STRING TYPE" - [42d7]: http://www.lispworks.com/documentation/HyperSpec/Body/m_defpkg.htm "DEFPACKAGE MGL-PAX:MACRO" [445d]: #x-28GEB-2EMIXINS-3APOINTWISE-MIXIN-20CLASS-29 "GEB.MIXINS:POINTWISE-MIXIN CLASS" [4529]: #x-28GEB-2EMIXINS-3AMETA-MIXIN-20CLASS-29 "GEB.MIXINS:META-MIXIN CLASS" [455b]: #x-28GEB-2EMIXINS-3A-40MIXIN-PERFORMANCE-20MGL-PAX-3ASECTION-29 "Performance" [4659]: #x-28GEB-2EBITC-2EMAIN-3A-40BITC-API-20MGL-PAX-3ASECTION-29 "Bits (Boolean Circuit) API" [46bc]: #x-28GEB-2EBITC-2ESPEC-3APARALLEL-20CLASS-29 "GEB.BITC.SPEC:PARALLEL CLASS" - [46ed]: http://www.lispworks.com/documentation/HyperSpec/Body/t_bt_vec.htm "BIT-VECTOR TYPE" [4710]: #x-28GEB-2ELAMBDA-2ESPEC-3AABSURD-20CLASS-29 "GEB.LAMBDA.SPEC:ABSURD CLASS" - [4850]: http://www.lispworks.com/documentation/HyperSpec/Body/t_kwd.htm "KEYWORD TYPE" + [47d6]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CADDDR (MGL-PAX:CLHS FUNCTION)" [48fc]: #x-28GEB-2ELAMBDA-2ESPEC-3ARIGHT-20CLASS-29 "GEB.LAMBDA.SPEC:RIGHT CLASS" [4938]: #x-28GEB-2EMIXINS-3A-40MIXIN-EXAMPLES-20MGL-PAX-3ASECTION-29 "Mixins Examples" [49d4]: #x-28GEB-2EMAIN-3A-40GEB-UTILITY-20MGL-PAX-3ASECTION-29 "Utility" [4a87]: #x-28GEB-DOCS-2FDOCS-3A-40OPEN-TYPE-20MGL-PAX-3AGLOSSARY-TERM-29 "GEB-DOCS/DOCS:@OPEN-TYPE MGL-PAX:GLOSSARY-TERM" + [4dee]: http://www.lispworks.com/documentation/HyperSpec/Body/t_number.htm "NUMBER (MGL-PAX:CLHS CLASS)" + [4df2]: http://www.lispworks.com/documentation/HyperSpec/Body/t_nil.htm "NIL (MGL-PAX:CLHS TYPE)" [4ffa]: #x-28GEB-2EUTILS-3A-40GEB-UTILS-MANUAL-20MGL-PAX-3ASECTION-29 "Geb Utilities" [56b3]: #x-28GEB-2ELAMBDA-2ESPEC-3ALEFT-20CLASS-29 "GEB.LAMBDA.SPEC:LEFT CLASS" [57dc]: #x-28GEB-2ESPEC-3ASUBSTMORPH-20TYPE-29 "GEB.SPEC:SUBSTMORPH TYPE" + [57e1]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CADDR (MGL-PAX:CLHS FUNCTION)" [58a9]: #x-28GEB-2EMIXINS-3ATO-POINTWISE-LIST-20GENERIC-FUNCTION-29 "GEB.MIXINS:TO-POINTWISE-LIST GENERIC-FUNCTION" - [592c]: http://www.lispworks.com/documentation/HyperSpec/Body/f_list_.htm "LIST FUNCTION" [5ae3]: #x-28GEB-2ESPEC-3APROJECT-LEFT-20CLASS-29 "GEB.SPEC:PROJECT-LEFT CLASS" [5b8b]: #x-28GEB-2ELAMBDA-2ESPEC-3AINDEX-20CLASS-29 "GEB.LAMBDA.SPEC:INDEX CLASS" [5c7c]: #x-28GEB-2ESPEC-3ASO0-20CLASS-29 "GEB.SPEC:SO0 CLASS" [5cfe]: #x-28GEB-2ESPEC-3ASO1-20CLASS-29 "GEB.SPEC:SO1 CLASS" [5d7c]: #x-28GEB-2ESPEC-3ACASE-20CLASS-29 "GEB.SPEC:CASE CLASS" [5dae]: #x-28GEB-2ELAMBDA-2ESPEC-3APAIR-20CLASS-29 "GEB.LAMBDA.SPEC:PAIR CLASS" + [5f51]: http://www.lispworks.com/documentation/HyperSpec/Body/t_bt_vec.htm "BIT-VECTOR (MGL-PAX:CLHS CLASS)" [603e]: #x-28GEB-GUI-3A-40VISAULIZER-AID-20MGL-PAX-3ASECTION-29 "Aiding the Visualizer" [6228]: #x-28GEB-3A-40GEB-API-20MGL-PAX-3ASECTION-29 "API" [6444]: #x-28GEB-2ESPEC-3ALEFT-20CLASS-29 "GEB.SPEC:LEFT CLASS" [65a4]: #x-28GEB-2EGENERICS-3AMAYBE-20GENERIC-FUNCTION-29 "GEB.GENERICS:MAYBE GENERIC-FUNCTION" - [684b]: http://www.lispworks.com/documentation/HyperSpec/Body/s_if.htm "IF MGL-PAX:MACRO" - [6a3c]: http://www.lispworks.com/documentation/HyperSpec/Body/f_bt_sb.htm "BIT FUNCTION" + [6832]: http://www.lispworks.com/documentation/HyperSpec/Body/m_defmet.htm "DEFMETHOD (MGL-PAX:CLHS MGL-PAX:MACRO)" [6b63]: #x-28GEB-2EBITC-3A-40BITC-MANUAL-20MGL-PAX-3ASECTION-29 "Bits (Boolean Circuit) Specification" + [6d9f]: http://www.lispworks.com/documentation/HyperSpec/Body/f_list_.htm "LIST (MGL-PAX:CLHS FUNCTION)" [6f67]: #x-28GEB-GUI-3A-40GEB-GUI-MANUAL-20MGL-PAX-3ASECTION-29 "The GEB GUI" - [7058]: http://www.lispworks.com/documentation/HyperSpec/Body/v_nil.htm "NIL MGL-PAX:CONSTANT" [7088]: #x-28GEB-2ESPEC-3ASO0-20MGL-PAX-3ASYMBOL-MACRO-29 "GEB.SPEC:SO0 MGL-PAX:SYMBOL-MACRO" [70c0]: #x-28GEB-2ELAMBDA-2ESPEC-3ATCOD-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:TCOD GENERIC-FUNCTION" [71e9]: #x-28GEB-GUI-2ECORE-3A-40GRAPHING-CORE-20MGL-PAX-3ASECTION-29 "The GEB Graphizer Core" [723a]: #x-28GEB-2EMIXINS-3A-40MIXINS-20MGL-PAX-3ASECTION-29 "Mixins" [73be]: #x-28GEB-2ESPEC-3AREALIZED-OBJECT-20TYPE-29 "GEB.SPEC:REALIZED-OBJECT TYPE" - [74ab]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CADR FUNCTION" [74bd]: #x-28GEB-2EMIXINS-3ACAT-OBJ-20CLASS-29 "GEB.MIXINS:CAT-OBJ CLASS" - [78ef]: http://www.lispworks.com/documentation/HyperSpec/Body/t_nil.htm "NIL TYPE" + [79d8]: http://www.lispworks.com/documentation/HyperSpec/Body/t_list.htm "LIST (MGL-PAX:CLHS CLASS)" [7c57]: #x-28GEB-2ELAMBDA-2ESPEC-3AON-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:ON GENERIC-FUNCTION" - [7dbb]: http://www.lispworks.com/documentation/HyperSpec/Body/t_number.htm "NUMBER TYPE" - [7e58]: http://www.lispworks.com/documentation/HyperSpec/Body/t_class.htm "CLASS CLASS" - [7f9f]: http://www.lispworks.com/documentation/HyperSpec/Body/t_symbol.htm "SYMBOL TYPE" [8311]: #x-28GEB-DOCS-2FDOCS-3A-40IDRIS-20MGL-PAX-3ASECTION-29 "Geb's Idris Code" [8387]: #x-28GEB-2ESPEC-3AINJECT-LEFT-20CLASS-29 "GEB.SPEC:INJECT-LEFT CLASS" + [868b]: http://www.lispworks.com/documentation/HyperSpec/Body/f_alloca.htm "ALLOCATE-INSTANCE (MGL-PAX:CLHS GENERIC-FUNCTION)" + [86f1]: #x-28GEB-2EPOLY-2ESPEC-3A-2A-20CLASS-29 "GEB.POLY.SPEC:* CLASS" [874b]: #x-28GEB-2ESPEC-3ATERMINAL-20CLASS-29 "GEB.SPEC:TERMINAL CLASS" [8932]: #x-28GEB-DOCS-2FDOCS-3A-40CLOSED-TYPE-20MGL-PAX-3AGLOSSARY-TERM-29 "GEB-DOCS/DOCS:@CLOSED-TYPE MGL-PAX:GLOSSARY-TERM" - [8bb8]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CADDR FUNCTION" [8be5]: #x-28GEB-2ESPEC-3ACOPROD-20CLASS-29 "GEB.SPEC:COPROD CLASS" [8bf3]: #x-28GEB-2EPOLY-2ESPEC-3APOLY-20TYPE-29 "GEB.POLY.SPEC:POLY TYPE" - [8c99]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CAR FUNCTION" [8cde]: #x-28GEB-2ELAMBDA-2ESPEC-3ALAMB-20CLASS-29 "GEB.LAMBDA.SPEC:LAMB CLASS" [8da6]: #x-28GEB-2EUTILS-3APREDICATE-20GENERIC-FUNCTION-29 "GEB.UTILS:PREDICATE GENERIC-FUNCTION" [8dcc]: #x-28GEB-2ELAMBDA-2EMAIN-3AFUN-TYPE-20CLASS-29 "GEB.LAMBDA.MAIN:FUN-TYPE CLASS" [8e11]: #x-28GEB-2ESPEC-3AINIT-20CLASS-29 "GEB.SPEC:INIT CLASS" [8eb0]: #x-28GEB-2EENTRY-3A-40GEB-ENTRY-20MGL-PAX-3ASECTION-29 "Geb as a binary" [8fa5]: #x-28GEB-DOCS-2FDOCS-3A-40INSTALLATION-20MGL-PAX-3ASECTION-29 "installation" - [9162]: #x-28GEB-2EPOLY-2ESPEC-3ACOMPOSE-20TYPE-29 "GEB.POLY.SPEC:COMPOSE TYPE" [925b]: #x-28GEB-DOCS-2FDOCS-3A-40POLY-SETS-20MGL-PAX-3ASECTION-29 "Poly in Sets" [9300]: #x-28GEB-2EMIXINS-3A-40METADATA-20MGL-PAX-3ASECTION-29 "Metadata Mixin" + [938a]: #x-28GEB-2EPOLY-2ESPEC-3A-2F-20CLASS-29 "GEB.POLY.SPEC:/ CLASS" [94a8]: #x-28GEB-2EPOLY-3A-40POLY-MANUAL-20MGL-PAX-3ASECTION-29 "Polynomial Specification" - [96d0]: http://www.lispworks.com/documentation/HyperSpec/Body/f_equal.htm "EQUAL FUNCTION" [9728]: #x-28GEB-2EMIXINS-3ADOM-20GENERIC-FUNCTION-29 "GEB.MIXINS:DOM GENERIC-FUNCTION" - [98f9]: http://www.lispworks.com/documentation/HyperSpec/Body/t_list.htm "LIST TYPE" + [9990]: http://www.lispworks.com/documentation/HyperSpec/Body/v_nil.htm "NIL (MGL-PAX:CLHS MGL-PAX:CONSTANT)" + [9b12]: http://www.lispworks.com/documentation/HyperSpec/Body/t_intege.htm "INTEGER (MGL-PAX:CLHS CLASS)" + [9b43]: http://www.lispworks.com/documentation/HyperSpec/Body/m_defpkg.htm "DEFPACKAGE (MGL-PAX:CLHS MGL-PAX:MACRO)" [9bc5]: #x-28GEB-DOCS-2FDOCS-3A-40LINKS-20MGL-PAX-3ASECTION-29 "Links" [9bcb]: #x-28GEB-TEST-3A-40GEB-TEST-MANUAL-20MGL-PAX-3ASECTION-29 "Testing" - [9bcb2]: http://www.lispworks.com/documentation/HyperSpec/Body/f_exp_e.htm "EXPT FUNCTION" [9f9c]: #x-28GEB-2ESPECS-3A-40GEB-SPECS-20MGL-PAX-3ASECTION-29 "Spec Files, Main Files and Project Layout" [a17b]: #x-28GEB-3A-40GEB-EXAMPLES-20MGL-PAX-3ASECTION-29 "Examples" [a300]: #x-28GEB-DOCS-2FDOCS-3A-40-3CTYPES-3E-20MGL-PAX-3ASECTION-29 "≺Types≻" [a7af]: #x-28GEB-2EMIXINS-3ACAT-MORPH-20CLASS-29 "GEB.MIXINS:CAT-MORPH CLASS" [a7d5]: #x-28GEB-DOCS-2FDOCS-3A-40LOADING-20MGL-PAX-3ASECTION-29 "loading" - [a802]: http://www.lispworks.com/documentation/HyperSpec/Body/t_std_ob.htm "STANDARD-OBJECT TYPE" + [a843]: http://www.lispworks.com/documentation/HyperSpec/Body/t_std_ob.htm "STANDARD-OBJECT (MGL-PAX:CLHS CLASS)" [a84b]: #x-28GEB-2EGENERICS-3A-40GENERICS-20MGL-PAX-3ASECTION-29 "Geneircs" - [a859]: http://www.lispworks.com/documentation/HyperSpec/Body/f_alloca.htm "ALLOCATE-INSTANCE FUNCTION" [a920]: #x-28GEB-DOCS-2FDOCS-3A-40OPEN-CLOSED-20MGL-PAX-3ASECTION-29 "Open Types versus Closed Types" - [a981]: http://www.lispworks.com/documentation/HyperSpec/Body/m_defmet.htm "DEFMETHOD MGL-PAX:MACRO" [abea]: #x-28GEB-2ELAMBDA-2ESPEC-3ARTY-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:RTY GENERIC-FUNCTION" [ac2d]: #x-28GEB-2ELAMBDA-2EMAIN-3AANN-TERM1-20GENERIC-FUNCTION-29 "GEB.LAMBDA.MAIN:ANN-TERM1 GENERIC-FUNCTION" - [ac8a]: http://www.lispworks.com/documentation/HyperSpec/Body/t_intege.htm "INTEGER TYPE" [ada5]: #x-28GEB-GUI-3AVISUALIZE-20FUNCTION-29 "GEB-GUI:VISUALIZE FUNCTION" [ada9]: #x-28GEB-DOCS-2FDOCS-3A-40MORPHISMS-20MGL-PAX-3ASECTION-29 "Morphisms" + [ae23]: http://www.lispworks.com/documentation/HyperSpec/Body/t_seq.htm "SEQUENCE (MGL-PAX:CLHS CLASS)" [af14]: #x-28GEB-2EUTILS-3AMCDR-20GENERIC-FUNCTION-29 "GEB.UTILS:MCDR GENERIC-FUNCTION" [b0d9]: #x-28GEB-2EGENERICS-3ATO-CIRCUIT-20GENERIC-FUNCTION-29 "GEB.GENERICS:TO-CIRCUIT GENERIC-FUNCTION" - [b324]: #x-28GEB-2ELAMBDA-2EMAIN-3AHOM-COD-20FUNCTION-29 "GEB.LAMBDA.MAIN:HOM-COD FUNCTION" [b36a]: #x-28GEB-2ELAMBDA-2ESPEC-3A-3CSTLC-3E-20CLASS-29 "GEB.LAMBDA.SPEC: CLASS" [b4a5]: #x-28GEB-2ELAMBDA-2ESPEC-3AFST-20CLASS-29 "GEB.LAMBDA.SPEC:FST CLASS" [b4a6]: #x-28GEB-2EPOLY-2ESPEC-3A-3CPOLY-3E-20CLASS-29 "GEB.POLY.SPEC: CLASS" + [b5ec]: http://www.lispworks.com/documentation/HyperSpec/Body/f_load.htm "LOAD (MGL-PAX:CLHS FUNCTION)" [b76d]: #x-28GEB-2EPOLY-2ESPEC-3A-40POLY-CONSTRUCTORS-20MGL-PAX-3ASECTION-29 "Polynomial Constructors" [b79a]: #x-28GEB-2ETRANS-3A-40GEB-TRANSLATION-20MGL-PAX-3ASECTION-29 "Translation Functions" + [b93c]: http://www.lispworks.com/documentation/HyperSpec/Body/t_string.htm "STRING (MGL-PAX:CLHS CLASS)" [b960]: #x-28GEB-2ESPEC-3A-2ASO1-2A-20VARIABLE-29 "GEB.SPEC:*SO1* VARIABLE" - [b9c1]: http://www.lispworks.com/documentation/HyperSpec/Body/t_seq.htm "SEQUENCE TYPE" [b9f3]: #x-28GEB-DOCS-2FDOCS-3A-40IDIOMS-20MGL-PAX-3ASECTION-29 "Project Idioms and Conventions" [ba44]: #x-28GEB-2ESPEC-3A--3ERIGHT-20FUNCTION-29 "GEB.SPEC:->RIGHT FUNCTION" [bb34]: #x-28GEB-2EGENERICS-3AGAPPLY-20GENERIC-FUNCTION-29 "GEB.GENERICS:GAPPLY GENERIC-FUNCTION" [bd81]: #x-28GEB-2EPOLY-2ESPEC-3A-40POLY-20MGL-PAX-3ASECTION-29 "Polynomial Types" - [bf07]: http://www.lispworks.com/documentation/HyperSpec/Body/f_export.htm "EXPORT FUNCTION" [bfa9]: #x-28GEB-2EUTILS-3ATHEN-20GENERIC-FUNCTION-29 "GEB.UTILS:THEN GENERIC-FUNCTION" [c111]: #x-28GEB-2EMIXINS-3AOBJ-EQUALP-20GENERIC-FUNCTION-29 "GEB.MIXINS:OBJ-EQUALP GENERIC-FUNCTION" - [c144]: #x-28GEB-2EPOLY-2ESPEC-3A-2B-20TYPE-29 "GEB.POLY.SPEC:+ TYPE" [c1b3]: #x-28GEB-2ESPEC-3A-40GEB-SUBSTMU-20MGL-PAX-3ASECTION-29 "Subst Obj" [c1fb]: #x-28GEB-3A-40GEB-20MGL-PAX-3ASECTION-29 "The Geb Model" [c275]: #x-28GEB-2ESPEC-3ARIGHT-20CLASS-29 "GEB.SPEC:RIGHT CLASS" [c2e9]: #x-28GEB-DOCS-2FDOCS-3A-40MODEL-20MGL-PAX-3ASECTION-29 "Categorical Model" - [c2f9]: #x-28GEB-2EPOLY-2ESPEC-3A-2F-20TYPE-29 "GEB.POLY.SPEC:/ TYPE" [c3e8]: #x-28GEB-GUI-2ECORE-3ANODE-NOTE-20CLASS-29 "GEB-GUI.CORE:NODE-NOTE CLASS" [c417]: #x-28GEB-2EBITC-2ESPEC-3AIDENT-20FUNCTION-29 "GEB.BITC.SPEC:IDENT FUNCTION" [c6cf]: #x-28GEB-GUI-3A-40GEB-VISUALIZER-20MGL-PAX-3ASECTION-29 "Visualizer" - [c721]: http://www.lispworks.com/documentation/HyperSpec/Body/f_equalp.htm "EQUALP FUNCTION" - [c767]: http://www.lispworks.com/documentation/HyperSpec/Body/s_the.htm "THE MGL-PAX:MACRO" + [caea]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CADR (MGL-PAX:CLHS FUNCTION)" [cb9e]: #x-28GEB-2ESPEC-3A-40GEB-CATEGORIES-20MGL-PAX-3ASECTION-29 "Core Category" [cc51]: #x-28GEB-2EUTILS-3A-40GEB-ACCESSORS-20MGL-PAX-3ASECTION-29 "Accessors" [cc87]: #x-28GEB-2EUTILS-3AMCADR-20GENERIC-FUNCTION-29 "GEB.UTILS:MCADR GENERIC-FUNCTION" [cccf]: #x-28GEB-2ELAMBDA-2ESPEC-3AFUN-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:FUN GENERIC-FUNCTION" [cd11]: #x-28GEB-2ESPEC-3AMCASE-20FUNCTION-29 "GEB.SPEC:MCASE FUNCTION" [ce5b]: #x-28GEB-2ESPEC-3ACOMP-20CLASS-29 "GEB.SPEC:COMP CLASS" - [ceb9]: http://www.lispworks.com/documentation/HyperSpec/Body/t_fixnum.htm "FIXNUM TYPE" [cf10]: #x-28GEB-2EBITC-2ESPEC-3AONE-20CLASS-29 "GEB.BITC.SPEC:ONE CLASS" [d243]: #x-28GEB-2EGENERICS-3ATO-CAT-20GENERIC-FUNCTION-29 "GEB.GENERICS:TO-CAT GENERIC-FUNCTION" [d2d1]: #x-28GEB-2ESPEC-3A-40GEB-SUBSTMORPH-20MGL-PAX-3ASECTION-29 "Subst Morph" [d2d5]: #x-28GEB-2ELAMBDA-2EMAIN-3A-40LAMBDA-API-20MGL-PAX-3ASECTION-29 "Main functionality" + [d4fe]: #x-28GEB-2EPOLY-2ESPEC-3A--20CLASS-29 "GEB.POLY.SPEC:- CLASS" + [d5a2]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CAR (MGL-PAX:CLHS FUNCTION)" [d5d3]: #x-28GEB-2EMIXINS-3A-40POINTWISE-20MGL-PAX-3ASECTION-29 "Pointwise Mixins" [d762]: #x-28GEB-2ELAMBDA-2ESPEC-3ARTM-20GENERIC-FUNCTION-29 "GEB.LAMBDA.SPEC:RTM GENERIC-FUNCTION" - [d908]: http://www.lispworks.com/documentation/HyperSpec/Body/f_typep.htm "TYPEP FUNCTION" [db35]: #x-28GEB-2ESPEC-3A-3CSUBSTMORPH-3E-20CLASS-29 "GEB.SPEC: CLASS" [db8f]: #x-28GEB-2ELAMBDA-3A-40STLC-20MGL-PAX-3ASECTION-29 "The Simply Typed Lambda Calculus model" [dbe7]: #x-28GEB-DOCS-2FDOCS-3A-40OBJECTS-20MGL-PAX-3ASECTION-29 "Objects" [dca9]: #x-28GEB-2ESPEC-3A-40GEB-REALIZED-20MGL-PAX-3ASECTION-29 "Realized Subst Objs" [dfa2]: #x-28GEB-2ESPEC-3APAIR-20CLASS-29 "GEB.SPEC:PAIR CLASS" + [e012]: http://www.lispworks.com/documentation/HyperSpec/Body/f_car_c.htm "CDR (MGL-PAX:CLHS FUNCTION)" [e017]: #x-28GEB-2EBITC-2ESPEC-3ABITC-20TYPE-29 "GEB.BITC.SPEC:BITC TYPE" [e2af]: #x-28GEB-2ESPEC-3A--3ELEFT-20FUNCTION-29 "GEB.SPEC:->LEFT FUNCTION" [e2b0]: #x-28GEB-2EMIXINS-3ADIRECT-POINTWISE-MIXIN-20CLASS-29 "GEB.MIXINS:DIRECT-POINTWISE-MIXIN CLASS" [e373]: #x-28GEB-2ELAMBDA-2ESPEC-3ASTLC-20TYPE-29 "GEB.LAMBDA.SPEC:STLC TYPE" [e3e4]: #x-28GEB-2ELAMBDA-2ETRANS-3A-40STLC-CONVERSION-20MGL-PAX-3ASECTION-29 "Transition Functions" [e429]: #x-28GEB-GUI-2EGRAPHING-2EPASSES-3A-40PASS-MANUAL-20MGL-PAX-3ASECTION-29 "The GEB Graphizer Passes" + [e5af]: http://www.lispworks.com/documentation/HyperSpec/Body/t_symbol.htm "SYMBOL (MGL-PAX:CLHS CLASS)" [e91b]: #x-28GEB-2EMIXINS-3A-40MIXINS-CAT-20MGL-PAX-3ASECTION-29 "The Categorical Interface" [e947]: #x-28GEB-2ESPEC-3AINJECT-RIGHT-20CLASS-29 "GEB.SPEC:INJECT-RIGHT CLASS" [e982]: #x-28GEB-2ESPEC-3A-2ASO0-2A-20VARIABLE-29 "GEB.SPEC:*SO0* VARIABLE" [ecb2]: #x-28GEB-2EBITC-2ESPEC-3ACOMPOSE-20CLASS-29 "GEB.BITC.SPEC:COMPOSE CLASS" [ecc6]: #x-28GEB-DOCS-2FDOCS-3A-40CLOS-20MGL-PAX-3AGLOSSARY-TERM-29 "GEB-DOCS/DOCS:@CLOS MGL-PAX:GLOSSARY-TERM" + [ed72]: #x-28GEB-2EPOLY-2ESPEC-3ACOMPOSE-20CLASS-29 "GEB.POLY.SPEC:COMPOSE CLASS" [ef6e]: #x-28GEB-GUI-2ECORE-3ANOTE-20TYPE-29 "GEB-GUI.CORE:NOTE TYPE" [f022]: #x-28GEB-BOOL-3ATRUE-20MGL-PAX-3ASYMBOL-MACRO-29 "GEB-BOOL:TRUE MGL-PAX:SYMBOL-MACRO" + [f0f8]: #x-28GEB-GUI-3A-40GEB-EXPORTER-20MGL-PAX-3ASECTION-29 "Export Visualizer" [f130]: #x-28GEB-2EBITC-2ESPEC-3ADROP-20FUNCTION-29 "GEB.BITC.SPEC:DROP FUNCTION" [f1ce]: #x-28GEB-2EUTILS-3AMCAR-20GENERIC-FUNCTION-29 "GEB.UTILS:MCAR GENERIC-FUNCTION" [f1e6]: #x-28GEB-2EUTILS-3AOBJ-20GENERIC-FUNCTION-29 "GEB.UTILS:OBJ GENERIC-FUNCTION" [f4ba]: #x-28GEB-2ESPEC-3ASO1-20MGL-PAX-3ASYMBOL-MACRO-29 "GEB.SPEC:SO1 MGL-PAX:SYMBOL-MACRO" - [f766]: http://www.lispworks.com/documentation/HyperSpec/Body/f_load.htm "LOAD FUNCTION" + [f97d]: http://www.lispworks.com/documentation/HyperSpec/Body/f_exp_e.htm "EXPT (MGL-PAX:CLHS FUNCTION)" [fa6c]: #x-28GEB-2EBITC-2ESPEC-3AZERO-20MGL-PAX-3ASYMBOL-MACRO-29 "GEB.BITC.SPEC:ZERO MGL-PAX:SYMBOL-MACRO" [fb79]: #x-28GEB-2ESPEC-3A-3CSUBSTOBJ-3E-20CLASS-29 "GEB.SPEC: CLASS" [fc10]: #x-28GEB-2EBITC-2ESPEC-3A-40BITC-CONSTRUCTORS-20MGL-PAX-3ASECTION-29 "Bits (Boolean Circuit) Constructors"