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
/*! **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). */ #![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;