1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166

/*! **Fungi language:** *reference implementation in Rust.*
 
See also:
[example Fungi programs](https://docs.rs/fungi-lang/0/fungi_lang/examples/index.html)
in this Rust implementation.

# Syntax

Fungi's 
[abstract syntax](https://docs.rs/fungi-lang/0/fungi_lang/ast/index.html) 
consists of Rust data types; we implement
its 
[concrete syntax](https://docs.rs/fungi-lang/0/fungi_lang/parse/index.html) 
with Rust macros:

 - [`ast`](https://docs.rs/fungi-lang/0/fungi_lang/ast/index.html)
--- Abstract syntax (Rust datatypes)
 - [`parse`](https://docs.rs/fungi-lang/0/fungi_lang/parse/index.html)
--- Concrete syntax (Rust macros)

(See [examples](https://docs.rs/fungi-lang/0/fungi_lang/examples/index.html))

# 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`](https://docs.rs/fungi-lang/0/fungi_lang/expand/index.html)
--- expand type-level definitions,
 - [`subst`](https://docs.rs/fungi-lang/0/fungi_lang/subst/index.html)
--- perform type-level variable substitution, 
 - [`normal`](https://docs.rs/fungi-lang/0/fungi_lang/normal/index.html)
--- perform type-level term normalization,
 - [`decide`](https://docs.rs/fungi-lang/0/fungi_lang/decide/index.html)
--- decide relationships about types, and about type indices.
   - [`equiv`](https://docs.rs/fungi-lang/0/fungi_lang/decide/equiv/index.html) -- decides term _equivalence_ relationships
   - [`apart`](https://docs.rs/fungi-lang/0/fungi_lang/decide/apart/index.html) -- decides term _apartness_ relationships
   - [`subset`](https://docs.rs/fungi-lang/0/fungi_lang/decide/subset/index.html) -- decide name _subsets_, and _subtyping_ relationships
   - [`effect`](https://docs.rs/fungi-lang/0/fungi_lang/decide/effect/index.html) -- decide _effect sequencing_ and _subtracting_ relationships
  
These notions are each in support of  
 - [`bitype`](https://docs.rs/fungi-lang/0/fungi_lang/bitype/index.html)
--- 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](http://github.com/Adapton/adapton.rust). 
We define two 
reference implementations for Fungi's dynamics: 
[_small-step reduction_](https://docs.rs/fungi-lang/0/fungi_lang/reduce/index.html),
and 
[_big-step evaluation_](https://docs.rs/fungi-lang/0/fungi_lang/eval/index.html):

- [`reduce`](https://docs.rs/fungi-lang/0/fungi_lang/reduce/index.html)
-- program dynamics as _small-step reduction_
- [`eval`](https://docs.rs/fungi-lang/0/fungi_lang/eval/index.html)
-- program dynamics as _big-step evaluation_

These approaches have many [_common definitions_](https://docs.rs/fungi-lang/0/fungi_lang/dynamics/index.html):

- [`dynamics`](https://docs.rs/fungi-lang/0/fungi_lang/dynamics/index.html)
-- 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](https://docs.rs/fungi-lang/0/fungi_lang/reduce/index.html)
is _significantly_ more practical than the version of [big-step
evaluation](https://docs.rs/fungi-lang/0/fungi_lang/eval/index.html) 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](https://docs.rs/fungi-lang/0/fungi_lang/eval/index.html), _not_ run it (except for very small programs).

*/
#![feature(crate_in_paths)]
#![recursion_limit="512"]
#![doc(html_logo_url = "http://adapton.org/fungi-lang-logo/Fungi-lang-logo.png",
       html_root_url = "https://docs.rs/fungi-lang/")]

//#![feature(rc_downcast)]

#[macro_use] extern crate adapton;

extern crate core;
extern crate regex;
extern crate serde;
extern crate serde_json;
#[macro_use] extern crate serde_derive;
//#[macro_use] extern crate nom;

// // Source language (IODyn)
// // ------------------------
// #[macro_use] pub mod ast;
// pub mod bitype;
// pub mod prims;
// pub mod eval;

// Utilities that are common across various test harnesses
#[macro_use]
#[doc(hidden)] pub mod util; 

#[macro_use]
#[doc(hidden)] pub mod db;
#[doc(hidden)] pub mod vt100;
#[doc(hidden)] pub mod display;

pub mod shared;

// === Syntax ===
//
pub mod ast;
//#[doc(hidden)]
#[macro_use]
pub mod parse;

// == Statics ===
//
pub mod subst;
pub mod expand;
pub mod normal;
pub mod decide;
pub mod bitype;

// === Dynamics ====
//
pub mod dynamics;
pub mod hostobj;
pub mod eval;
pub mod reduce;

// === Debugging/Instrumentation/Visualization ====
// 
#[macro_use]
pub mod vis;
pub mod html;
pub mod serialize;

// Note to readers: The standard library is a stale "sketch" of Fungi
// code; see `examples` modules for up-to-date examples.
#[doc(hidden)] pub mod stdlib;

pub mod examples;

// Translation
// ------------------
// pub mod translate;