The type-i Reference Manual

Table of Contents

Next: , Previous: , Up: (dir)   [Contents][Index]

The type-i Reference Manual

This is the type-i Reference Manual, version 0.1, generated automatically by Declt version 2.3 "Robert April" on Tue Jan 09 15:57:22 2018 GMT+0.


Next: , Previous: , Up: Top   [Contents][Index]

1 Introduction


* Type-I : type-inference from a predicate

This library tries to provide a way to detect what kind of type the given
predicate is trying to check. *This is different from inferring the return
type of a function.* For example,

#+BEGIN_SRC lisp

(eq 'null (test-type '(eql nil ?)))

(eq 'string (test-type '(stringp ?)))

#+END_SRC

The inference is done on form basis, and the equivalence of predicates are
determined by =#'equal=. To simplify the design, the argument to check
should be a symbol =?=, exported in package =type-i=.

Function =test-type= returns the inferred type. In contrast, =type-tests=
returns a list of all possible test predicates that returns true when =?=
is bound to the object of interest.

#+BEGIN_SRC lisp
  (is (subset '((TYPEP ? 'integer)
                (integerp ?))
              (type-tests 'integer)))

  ;; more inference on integers, e.g., (< 0 ? 4), should be added
  (is (subset '((TYPEP ? '(mod 5))
                (TYPEP ? '(integer 0 4)))
              (type-tests '(mod 5))))

#+END_SRC

This library is extensible. with =define-inference-rule= macro, you can add
more inferers to improve this library. Each inference rule is a unary
function that takes a predicate form, then returns a list of more
forms.

The =test-type= searches in the form space, adding the results of each
inference rule, until a form =(typep ? X)= is found (where X is
unknown). If it fails to find such a form even if the maximal set
is obtained, then the =test-type= returns nil. =type-tests= just returns
the maximal set.

I currently implemented the following inference rules:

- typep -- =(typep ? 'array)= -> =(arrayp ?)= etc.
- unary -- =(arrayp ?)= -> =(typep ? 'array) (typep ? '(array)) (typep ?
  '(array *))= ...
- null -- =(null ?) (typep ? null) (eql ? nil) (eql nil ?) (eq ? nil)= ...
- derived -- call =typexpand=

Inference on exhaustive partitions, e.g., =(typep ? 'list)= -> =(typep ?
'(or cons null))= is planned.

** Dependencies

This library is at least tested on implementation listed below:

+ SBCL 1.2.8 on X86-64 Linux  3.13.0-46-generic (author's environment)

Also, it depends on the following libraries:

+ Trivia by Masataro Asai ::
     NON-Optimized Pattern Matching Library

+ alexandria by  ::
    Alexandria is a collection of portable public domain utilities.

+ iterate by  ::
    Jonathan Amsterdam's iterator/gatherer/accumulator facility

+ introspect-environment by Bike  ::
    Small interface to portable but nonstandard introspection of CL environments.



** Author

+ Masataro Asai (guicho2.71828@gmail.com)

* Copyright

Copyright (c) 2015 Masataro Asai (guicho2.71828@gmail.com)


* License

Licensed under the LLGPL License.





Next: , Previous: , Up: Top   [Contents][Index]

2 Systems

The main system appears first, followed by any subsystem dependency.


Previous: , Up: Systems   [Contents][Index]

2.1 type-i

Author

Masataro Asai

Contact

guicho2.71828@gmail.com

License

LLGPL

Description

Type Inference Utility on Fundamentally 1-arg Predicates

Version

0.1

Dependencies
Source

type-i.asd (file)

Components

Next: , Previous: , Up: Top   [Contents][Index]

3 Files

Files are sorted by type and then listed depth-first from the systems components trees.


Previous: , Up: Files   [Contents][Index]

3.1 Lisp


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.1 type-i.asd

Location

/home/quickbuilder/quicklisp/dists/quicklisp/software/type-i-20150608-git/type-i.asd

Systems

type-i (system)

Packages

type-i-asd


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.2 type-i/package.lisp

Parent

type-i (system)

Location

package.lisp

Packages

type-i

Exported Definitions
Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.3 type-i/infer-typep.lisp

Dependency

package.lisp (file)

Parent

type-i (system)

Location

infer-typep.lisp

Internal Definitions

Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.4 type-i/infer-unary.lisp

Dependency

infer-typep.lisp (file)

Parent

type-i (system)

Location

infer-unary.lisp

Internal Definitions

typep-form (function)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.5 type-i/infer-derived.lisp

Dependency

infer-unary.lisp (file)

Parent

type-i (system)

Location

infer-derived.lisp


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.6 type-i/infer-constants.lisp

Dependency

infer-derived.lisp (file)

Parent

type-i (system)

Location

infer-constants.lisp

Internal Definitions

+null-tests+ (special variable)


Next: , Previous: , Up: Lisp files   [Contents][Index]

3.1.7 type-i/infer-compound.lisp

Dependency

infer-constants.lisp (file)

Parent

type-i (system)

Location

infer-compound.lisp


Previous: , Up: Lisp files   [Contents][Index]

3.1.8 type-i/infer-numbers.lisp

Dependency

infer-compound.lisp (file)

Parent

type-i (system)

Location

infer-numbers.lisp


Next: , Previous: , Up: Top   [Contents][Index]

4 Packages

Packages are listed by definition order.


Next: , Previous: , Up: Packages   [Contents][Index]

4.1 type-i-asd

Source

/home/quickbuilder/quicklisp/dists/quicklisp/software/type-i-20150608-git/type-i.asd

Use List

Previous: , Up: Packages   [Contents][Index]

4.2 type-i

Source

package.lisp (file)

Use List
Exported Definitions
Internal Definitions

Next: , Previous: , Up: Top   [Contents][Index]

5 Definitions

Definitions are sorted by export status, category, package, and then by lexicographic order.


Next: , Previous: , Up: Definitions   [Contents][Index]

5.1 Exported definitions


Next: , Previous: , Up: Exported definitions   [Contents][Index]

5.1.1 Macros

Macro: define-inference-rule NAME ARGS &body BODY
Package

type-i

Source

package.lisp (file)


Previous: , Up: Exported definitions   [Contents][Index]

5.1.2 Functions

Function: ? SYMBOL TEST

substitute symbol with ’?, canonicalizing the test form amenable for comparison

Package

type-i

Source

package.lisp (file)

Function: test-type TEST &optional VERBOSE

infer the type which the given test form is trying to test against.
If the values are NIL,T , it means the type is definitely NIL.
If the values are NIL,NIL , it means the type is not successfully inferred.

Package

type-i

Source

package.lisp (file)

Function: type-tests TYPE &optional VERBOSE
Package

type-i

Source

package.lisp (file)


Previous: , Up: Definitions   [Contents][Index]

5.2 Internal definitions


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.1 Special variables

Special Variable: *compound-infer-level*
Package

type-i

Source

infer-typep.lisp (file)

Special Variable: *inference-rules-doc-table*
Package

type-i

Source

package.lisp (file)

Special Variable: *inference-rules-table*
Package

type-i

Source

package.lisp (file)

Special Variable: *max-compound-type-arguments*
Package

type-i

Source

infer-typep.lisp (file)

Special Variable: +null-tests+
Package

type-i

Source

infer-constants.lisp (file)


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.2 Macros

Macro: inference-rules-let BINDINGS &body BODY
Package

type-i

Source

package.lisp (file)


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.3 Functions

Function: all-compound-types COMPOUND &optional *COMPOUND-INFER-LEVEL*
Package

type-i

Source

infer-typep.lisp (file)

Function: inference-rules-boundp SYMBOL

Automatically defined boolean function.

Package

type-i

Source

package.lisp (file)

Function: predicate-p TYPE
Package

type-i

Source

infer-typep.lisp (file)

Function: predicate-p-function TYPE
Package

type-i

Source

infer-typep.lisp (file)

Function: predicatep TYPE
Package

type-i

Source

infer-typep.lisp (file)

Function: predicatep-function TYPE
Package

type-i

Source

infer-typep.lisp (file)

Function: symbol-inference-rules SYMBOL &optional DEFAULT

Automatically defined getter function. When DEFAULT is supplied, the value is set automatically.

Package

type-i

Source

package.lisp (file)

Writer

(setf symbol-inference-rules) (function)

Function: (setf symbol-inference-rules) NEW-VALUE SYMBOL

Automatically defined setter function.

Package

type-i

Source

package.lisp (file)

Reader

symbol-inference-rules (function)

Function: typep-form TYPESYM
Package

type-i

Source

infer-unary.lisp (file)


Next: , Previous: , Up: Internal definitions   [Contents][Index]

5.2.4 Conditions

Condition: unbound-inference-rules ()
Package

type-i

Source

package.lisp (file)

Direct superclasses

unbound-variable (condition)


Previous: , Up: Internal definitions   [Contents][Index]

5.2.5 Types

Type: inference-rules-type ()
Package

type-i

Source

package.lisp (file)


Previous: , Up: Top   [Contents][Index]

Appendix A Indexes


Next: , Previous: , Up: Indexes   [Contents][Index]

A.1 Concepts

Jump to:   F   L   T  
Index Entry  Section

F
File, Lisp, type-i.asd: The type-i<dot>asd file
File, Lisp, type-i/infer-compound.lisp: The type-i/infer-compound<dot>lisp file
File, Lisp, type-i/infer-constants.lisp: The type-i/infer-constants<dot>lisp file
File, Lisp, type-i/infer-derived.lisp: The type-i/infer-derived<dot>lisp file
File, Lisp, type-i/infer-numbers.lisp: The type-i/infer-numbers<dot>lisp file
File, Lisp, type-i/infer-typep.lisp: The type-i/infer-typep<dot>lisp file
File, Lisp, type-i/infer-unary.lisp: The type-i/infer-unary<dot>lisp file
File, Lisp, type-i/package.lisp: The type-i/package<dot>lisp file

L
Lisp File, type-i.asd: The type-i<dot>asd file
Lisp File, type-i/infer-compound.lisp: The type-i/infer-compound<dot>lisp file
Lisp File, type-i/infer-constants.lisp: The type-i/infer-constants<dot>lisp file
Lisp File, type-i/infer-derived.lisp: The type-i/infer-derived<dot>lisp file
Lisp File, type-i/infer-numbers.lisp: The type-i/infer-numbers<dot>lisp file
Lisp File, type-i/infer-typep.lisp: The type-i/infer-typep<dot>lisp file
Lisp File, type-i/infer-unary.lisp: The type-i/infer-unary<dot>lisp file
Lisp File, type-i/package.lisp: The type-i/package<dot>lisp file

T
type-i.asd: The type-i<dot>asd file
type-i/infer-compound.lisp: The type-i/infer-compound<dot>lisp file
type-i/infer-constants.lisp: The type-i/infer-constants<dot>lisp file
type-i/infer-derived.lisp: The type-i/infer-derived<dot>lisp file
type-i/infer-numbers.lisp: The type-i/infer-numbers<dot>lisp file
type-i/infer-typep.lisp: The type-i/infer-typep<dot>lisp file
type-i/infer-unary.lisp: The type-i/infer-unary<dot>lisp file
type-i/package.lisp: The type-i/package<dot>lisp file

Jump to:   F   L   T  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.2 Functions

Jump to:   (   ?  
A   D   F   I   M   P   S   T  
Index Entry  Section

(
(setf symbol-inference-rules): Internal functions

?
?: Exported functions

A
all-compound-types: Internal functions

D
define-inference-rule: Exported macros

F
Function, (setf symbol-inference-rules): Internal functions
Function, ?: Exported functions
Function, all-compound-types: Internal functions
Function, inference-rules-boundp: Internal functions
Function, predicate-p: Internal functions
Function, predicate-p-function: Internal functions
Function, predicatep: Internal functions
Function, predicatep-function: Internal functions
Function, symbol-inference-rules: Internal functions
Function, test-type: Exported functions
Function, type-tests: Exported functions
Function, typep-form: Internal functions

I
inference-rules-boundp: Internal functions
inference-rules-let: Internal macros

M
Macro, define-inference-rule: Exported macros
Macro, inference-rules-let: Internal macros

P
predicate-p: Internal functions
predicate-p-function: Internal functions
predicatep: Internal functions
predicatep-function: Internal functions

S
symbol-inference-rules: Internal functions

T
test-type: Exported functions
type-tests: Exported functions
typep-form: Internal functions

Jump to:   (   ?  
A   D   F   I   M   P   S   T  

Next: , Previous: , Up: Indexes   [Contents][Index]

A.3 Variables

Jump to:   *   +  
S  
Index Entry  Section

*
*compound-infer-level*: Internal special variables
*inference-rules-doc-table*: Internal special variables
*inference-rules-table*: Internal special variables
*max-compound-type-arguments*: Internal special variables

+
+null-tests+: Internal special variables

S
Special Variable, *compound-infer-level*: Internal special variables
Special Variable, *inference-rules-doc-table*: Internal special variables
Special Variable, *inference-rules-table*: Internal special variables
Special Variable, *max-compound-type-arguments*: Internal special variables
Special Variable, +null-tests+: Internal special variables

Jump to:   *   +  
S  

Previous: , Up: Indexes   [Contents][Index]

A.4 Data types

Jump to:   C   I   P   S   T   U  
Index Entry  Section

C
Condition, unbound-inference-rules: Internal conditions

I
inference-rules-type: Internal types

P
Package, type-i: The type-i package
Package, type-i-asd: The type-i-asd package

S
System, type-i: The type-i system

T
Type, inference-rules-type: Internal types
type-i: The type-i system
type-i: The type-i package
type-i-asd: The type-i-asd package

U
unbound-inference-rules: Internal conditions

Jump to:   C   I   P   S   T   U