------------------------------------------------------------------------ -- INCREMENTAL λ-CALCULUS -- -- All modules of the formalization. -- -- This file is automatically generated by GenerateEverythingIlc.hs. ------------------------------------------------------------------------ module Everything where -- Change Structures. -- -- This module defines the notion of change structures, -- as well as change structures for groups, functions and lists. -- -- This module corresponds to Section 2 of the PLDI paper. ------------------------------------------------------------------------ import Base.Change.Algebra -- Change contexts -- -- This module specifies how a context of values is merged -- together with the corresponding context of changes. -- -- In the PLDI paper, instead of merging the contexts together, we just -- concatenate them. For example, in the "typing rule" for Derive -- in Sec. 3.2 of the paper, we write in the conclusion of the rule: -- "Γ, ΔΓ ⊢ Derive(t) : Δτ". Simple concatenation is possible because -- the paper uses named variables and assumes that no user variables -- start with "d". In this formalization, we use de Bruijn indices, so -- it is easier to alternate values and their changes in the context. ------------------------------------------------------------------------ import Base.Change.Context -- Reexport Data.List.All from the standard library. -- -- At one point, we reinvented Data.List.All from the Agda -- standard library, under the name dependent list. We later -- replaced our reinvention by this adapter module that just -- exports the standard library's version with partly different -- names. ------------------------------------------------------------------------ import Base.Data.DependentList -- Environments -- -- This module defines the meaning of contexts, that is, -- the type of environments that fit a context, together -- with operations and properties of these operations. -- -- This module is parametric in the syntax and semantics -- of types, so it can be reused for different calculi -- and models. ------------------------------------------------------------------------ import Base.Denotation.Environment -- Overloading ⟦_⟧ notation -- -- This module defines a general mechanism for overloading the -- ⟦_⟧ notation, using Agda’s instance arguments. ------------------------------------------------------------------------ import Base.Denotation.Notation -- Variables and contexts -- -- This module defines the syntax of contexts, prefixes of -- contexts and variables and properties of these notions. -- -- This module is parametric in the syntax of types, so it -- can be reused for different calculi. ------------------------------------------------------------------------ import Base.Syntax.Context -- Sets of variables ------------------------------------------------------------------------ import Base.Syntax.Vars -- Correctness of differentiation with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Change.Correctness -- Incrementalization as term-to-term transformation with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Change.Derive -- Connecting Nehemiah.Change.Term and Nehemiah.Change.Value. ------------------------------------------------------------------------ import Nehemiah.Change.Evaluation -- Logical relation for erasure with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Change.Implementation -- Change evaluation with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Change.Specification -- Terms that operate on changes with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Change.Term -- Simply-typed changes with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Change.Type -- Dependently typed changes with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Change.Validity -- The values of terms in Nehemiah.Change.Term. ------------------------------------------------------------------------ import Nehemiah.Change.Value -- Standard evaluation with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Denotation.Evaluation -- Values for standard evaluation with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Denotation.Value -- The syntax of terms with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Syntax.Term -- The syntax of types with the Nehemiah plugin. ------------------------------------------------------------------------ import Nehemiah.Syntax.Type import PLDI14-List-of-Theorems -- Correctness of differentiation (Lemma 3.10 and Theorem 3.11). ------------------------------------------------------------------------ import Parametric.Change.Correctness -- Incrementalization as term-to-term transformation (Fig. 4g). ------------------------------------------------------------------------ import Parametric.Change.Derive -- Connecting Parametric.Change.Term and Parametric.Change.Value. ------------------------------------------------------------------------ import Parametric.Change.Evaluation -- Logical relation for erasure (Def. 3.8 and Lemma 3.9) ------------------------------------------------------------------------ import Parametric.Change.Implementation -- Change evaluation (Def 3.6 and Fig. 4h). ------------------------------------------------------------------------ import Parametric.Change.Specification -- Terms that operate on changes (Fig. 3). ------------------------------------------------------------------------ import Parametric.Change.Term -- Simply-typed changes (Fig. 3 and Fig. 4d) ------------------------------------------------------------------------ import Parametric.Change.Type -- Dependently typed changes (Def 3.4 and 3.5, Fig. 4b and 4e) ------------------------------------------------------------------------ import Parametric.Change.Validity -- The values of terms in Parametric.Change.Term. ------------------------------------------------------------------------ import Parametric.Change.Value -- Standard evaluation (Def. 3.3 and Fig. 4i) ------------------------------------------------------------------------ import Parametric.Denotation.Evaluation -- Values for standard evaluation (Def. 3.1 and 3.2, Fig. 4c and 4f). ------------------------------------------------------------------------ import Parametric.Denotation.Value -- The syntax of terms (Fig. 1a and 1b). ------------------------------------------------------------------------ import Parametric.Syntax.Term -- The syntax of function types (Fig. 1a). ------------------------------------------------------------------------ import Parametric.Syntax.Type import Postulate.Bag-Nehemiah -- Postulate extensionality of functions. -- -- Justification on Agda mailing list: -- http://permalink.gmane.org/gmane.comp.lang.agda/2343 ------------------------------------------------------------------------ import Postulate.Extensionality -- Bags of integers, for Nehemiah plugin. -- -- This module imports postulates about bags of integers -- with negative multiplicities as a group under additive union. ------------------------------------------------------------------------ import Structure.Bag.Nehemiah -- Congruence of application. -- -- If f ≡ g and x ≡ y, then (f x) ≡ (g y). ------------------------------------------------------------------------ import Theorem.CongApp -- About the group structure of integers and bags for Nehemiah plugin. ------------------------------------------------------------------------ import Theorem.Groups-Nehemiah