Crate fungi_lang[][src]

Fungi language: reference implementation in Rust.

See also: example Fungi programs in this Rust implementation.

Syntax

Fungi's abstract syntax consists of Rust data types; we implement its concrete syntax with Rust macros:

  • ast --- Abstract syntax (Rust datatypes)
  • parse --- Concrete syntax (Rust macros)

(See examples)

Statics

Fungi's statics relate Fungi programs with their types and effects.

To accomplish this, Fungi gives a "type-level" semantics for relating types, and their index- and name terms. Specifically, this theory includes various supportive notions:

  • expand --- expand type-level definitions,
  • subst --- perform type-level variable substitution,
  • normal --- perform type-level term normalization,
  • decide --- decide relationships about types, and about type indices.
    • equiv -- decides term equivalence relationships
    • apart -- decides term apartness relationships
    • subset -- decide name subsets, and subtyping relationships
    • effect -- decide effect sequencing and subtracting relationships

These notions are each in support of

  • bitype --- bi-directional type checking for program terms (expressions and values).

In particular, the bitype module synthesizes and checks the types of Fungi program terms, and thus provides the most common "entry points" into the implementation of Fungi's statics.

Dynamics

Fungi's dynamics execute Fungi programs, under varying notions of execution.

Fungi's program executions use Adapton in Rust. We define two reference implementations for Fungi's dynamics: small-step reduction, and big-step evaluation:

  • reduce -- program dynamics as small-step reduction
  • eval -- program dynamics as big-step evaluation

These approaches have many common definitions:

  • dynamics -- common definitions: name term evaluation, run-time values, and environments.

Dynamics: practicum

Summary: Use program reduction (not evaluation) in all practical settings.

For the sake of completeness, we provide two execution definitions. However, the implementation of small-step reduction is significantly more practical than the version of big-step evaluation given here.

In particular, program reduction avoids using (Rust-level) stack space, whereas the simple evaluation definition here uses the (Rust-level) stack space in proportion to the depth of the full evaluation derivation. These derivations can be deep for recursive, looping programs, where their depth is often the same, asymptotically, as their running time. On the other hand, this definition of evaluation is simple, and easy to read and understand --- the goal of its reference implementation; readers are encouraged to read it, not run it (except for very small programs).

Modules

ast

Syntax: abstract (via Rust datatypes) and concrete (via Rust macros).

bitype

Bidirectional type system.

decide

Decision procedures for Fungi type and effect system.

dynamics

Syntax for dynamic, evaluation-time structures.

eval

Evaluation semantics.

examples

Examples of data structures and algorithms in Fungi.

expand

Expand static definitions (Ident cases of types, indices and effects).

html
normal

Static (typing-time) term reduction/normalization.

parse

Syntax: abstract (via Rust datatypes) and concrete (via Rust macros).

reduce

Reduction semantics.

serialize

Serialization for external data structures contained in Fungi's bundle format.

shared
subst

Static (typing-time) substitutions.

vis

Visualization of ASTs, typings, evaluation, etc.

Macros

fgi_bundle
fgi_ceffect

Parser for Computations with effects

fgi_ctype

Parser for computation types

fgi_decls

Parser for declaration lists

fgi_dynamic_trace
fgi_effect

Parser for Effects

fgi_exp

Parser for expressions

fgi_index

Parser for Index Terms

fgi_inner_mod

Declare an inner, named Fungi module, using an inner host (Rust) module.

fgi_kind

Parser for Kinds

fgi_listing_expect

Fungi program listing that we test.

fgi_listing_test
fgi_mod

Declare the Fungi module for current host (Rust) module.

fgi_module

Parser for modules, whose bodies consist of a declaration list.

fgi_name

Parser for Name Literals

fgi_nametm

Parser for Name Terms

fgi_prop

Parser for Propositions

fgi_sort

Parser for Sorts

fgi_val

Parser for values

fgi_vtype

Parser for value types

filename_of_module_path
parse_fgi_arrow

this macro is a helper for fgi_ctype, not for external use

parse_fgi_earrow

this macro is a helper for fgi_ceffect, not for external use

parse_fgi_eff

this macro is a helper for fgi_effect, not for external use

parse_fgi_name_bin

this macro is a helper for fgi_nametm, not for external use

parse_fgi_pack_multi

this macro is a helper for fgi_val, not for external use

parse_fgi_prod

this macro is a helper for fgi_vtype, not for external use

parse_fgi_split

this macro is a helper for fgi_exp, not for external use

parse_fgi_sum

this macro is a helper for fgi_vtype, not for external use

parse_fgi_tuple

this macro is a helper for fgi_val, not for external use

split_arrow

run a macro on a list of lists after splitting the input

split_comma

run a macro on a list of lists after splitting the input

split_cross

run a macro on a list of lists after splitting the input

split_plus

run a macro on a list of lists after splitting the input

split_semi

run a macro on a list of lists after splitting the input

split_star

run a macro on a list of lists after splitting the input