Updated all descriptions

src/Analysis/TypeInferrer.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE TypeOperators #-}
 
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Analysis.TypeInferrer
   Description : Type inference algorithm for Contra.
@@ -14,32 +14,37 @@
   This type inference algorithm is based on De Bruijn indices and constraint
   solving.
 
-  We type-annotate the program by annotating each program statement, and in
-  turn, annotating each of their terms.
+  A constraint consists of two types that should be equal, and a string
+  with the source code position of the relevant term(s) for error messages.
 
-  Terms are annotated with a type, which is either a concrete type or
-  a unification variable denoted by an index.
-  Values (literals/canonical terms) are type-annotated directly with their
-  concrete type, while Patterns and general Terms are annotated indirectly.
+  Type-inference is done by annotating terms with concrete types or with
+  unification variables and then adding constraints to these types. When we are
+  done annotating, we solve the constraints and signal any errors.
+  
+  The Annotation monad is an instantiation of the ERWS monad and keeps track
+  of the following contexts:
+   * Environment: Type, which is the typed program text - including definitions
+     of algebraic data types
+   * Reader: Bindings, which is a mapping from variable names to types
+   * Writer: [Constraint], a list of type equality constraints
+   * State: Index, a fresh unification variable index
 
   Either a term's type judgement rule let us decide their type by the type of
   their subterms, or we generate fresh unification variables and add constraints
   to them according to the type judgement rules.
 
+  Values (literals/canonical terms) are type-annotated directly with their
+  concrete type, while Patterns and general Terms are annotated indirectly.
+
   Finally, we solve the constraints and replace each unification
   variable with a concrete type. If the constraints cannot be solved,
   we throw an error with a description of the unsatisfiable constraint.
 
-  The Annotation monad is an instantiation of the ERWS monad and keeps track
-  of the following contexts:
-   - Environment: Type, which is the typed program text - including definitions
-     of algebraic data types
-   - Reader: Bindings, which is a mapping from variable names to types
-   - Writer: [Constraint], a list of type equality constraints
-   - State: Index, a fresh unification variable index
+  When inferring a program, we add constraints to enforce accordance between
+  function/property signatures and their implementation. Additionally, we
+  require that properties *must* return a Boolean value.
 
--------------------------------------------------------------------------------}
--- TODO: Update TypeInferrer description
+-}
 
 module Analysis.TypeInferrer where
 

src/Analysis/Unifier.hs

@@ -1,4 +1,4 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Analysis.Unifier
   Description : Unification algorithm for Contra.
@@ -23,7 +23,7 @@
 
   If this Unifier exists, that constitutes our Transformation.
 
--------------------------------------------------------------------------------}
+-}
 
 
 module Analysis.Unifier where

src/Core/Parser.hs

@@ -1,4 +1,4 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Core.Parser
   Description : The parser for Contra.
@@ -15,9 +15,17 @@
   of Haskell.
 
   The parser is implemented with the monadic parser
-  combinator library Parsec. It is available on Hackage.
+  combinator library Parsec.
 
--------------------------------------------------------------------------------}
+  Besides strict parsing, the parser is responsible for "flattening" function
+  definitions s.t. functions defined over different pattern-match cases are
+  collapsed into a single function definition with a case statement representing
+  the different pattern-matches defined.
+
+  It also keeps track of the source position of each term so we can provide the
+  user with more helpful type error messages.
+
+-}
 
 module Core.Parser where
 
@@ -36,10 +44,10 @@ type Parser = Parsec Source ()
 type Info   = (SourcePos, SourcePos)
 
 data ParsingError =
-    MultipleSignatures           X
-  | MultipleADTs                 X
-  | MultipleProperties          (X, Info)
-  | ParsingFailed               ParseError
+    MultipleSignatures  X
+  | MultipleADTs        X
+  | MultipleProperties (X, Info)
+  | ParsingFailed      ParseError
   deriving Show
 
 

src/Core/Syntax.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE DeriveFunctor #-}
 
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Core.Syntax
   Description : Abstract syntax of Contra.
@@ -18,13 +18,13 @@
 
   Besides the abstract syntax, this file also contains functions and
   typeclass instances pertaining to:
-   - Term & program equality
-   - Term canonicity (literals)
-   - Term annotations
-   - Pretty printing
-   - Other utility functions
+   * Term & program equality
+   * Term canonicity (literals)
+   * Term annotations - used in program analysis
+   * Pretty printing
+   * Other utility functions
 
--------------------------------------------------------------------------------}
+-}
 
 module Core.Syntax where
 

src/Environment/ERSymbolic.hs

@@ -1,4 +1,4 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Environment.ERSymbolic
   Description : Environment Reader Symbolic monad.
@@ -9,9 +9,16 @@
   Stability   : experimental
   Portability : POSIX
 
-  -- TODO: Description of ERSymbolic monad
+  The ERSymbolic monad is reworked from Joachim Tilsted Kristensen's
+  implementation of the ERWS monad (found in Environment.ERWS). We use the same
+  approach used to create an Environment Reader Writer State monad, to make
+  an Environment Reader Symbolic monad.
 
--------------------------------------------------------------------------------}
+  Symbolic is the innermost monad. Besides it, we have access to a program
+  environment (i.e., the user's program text) and a Reader environment.
+  Through the Environment, we can access the user's ADT definitions.
+
+-}
 
 module Environment.ERSymbolic where
 

src/Environment/ERWS.hs

@@ -1,17 +1,22 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Environment.ERWS
   Description : Environment Reader Writer State monad.
-  Copyright   : (c) 2022 Joachim Tilsted Kristensen, 2024 Sophie Adeline Solheim Bosio
+  Copyright   : (c) 2022 Joachim Tilsted Kristensen
   License     : GLP-3.0
 
   Maintainer  : [email protected]
   Stability   : experimental
   Portability : POSIX
 
-  -- TODO: Description of ERWS monad
+  This implementation is by Joachim Tilsted Kristensen.
 
--------------------------------------------------------------------------------}
+  The Environment Reader Writer State monad transforms the usual RWS monad
+  and adds a program environment (Environment.Environment), which gives us
+  convenient access to parts of the user-written program text. Importantly,
+  we can access the user's ADT definitions.
+
+-}
 
 module Environment.ERWS where
 

src/Environment/Environment.hs

@@ -1,4 +1,4 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Environment.Environment
   Description : Program environment definition.
@@ -9,9 +9,17 @@
   Stability   : experimental
   Portability : POSIX
 
-  -- TODO: Description of Environment
+  This file contains the type `Mapping` and the type-level operator `MapsTo`,
+  which are used in:
+   * Analysis.TypeInferrer
+   * Environment.ERSymbolic
+   * Validation.Formula
 
--------------------------------------------------------------------------------}
+  It also contains the Program Environment, which is used in the monads in
+  Environment.ERWS and Environment.ERSymbolic for convenient access to parts of
+  the program text.
+
+-}
 
 module Environment.Environment where
 

src/Semantics/Interpreter.hs

@@ -1,4 +1,4 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Semantics.Interpreter
   Description : Interpreter for Contra.
@@ -11,16 +11,18 @@
 
   Interpreter for the functional language Contra.
 
-  Mostly, variables are bound directly, as in function application or
-  let-statements. Then, we can simply substitute the variable name(s) in the
-  relevant term with the terms they are bound to.
+  'evaluate' evaluates a term in the conventional way. It is either a value
+  and can be evaluated directly, or it can be evaluated by the evaluation of its
+  composite subterms.
 
-  However, we cannot do this directly for top-level bindings. That's why the
-  interpreter uses the Reader monad to access the program text.
-  With it, we can find the function/property definition bound by that name in
-  the program text and substitute the variable name for the definition.
+  Variables are mostly bound directly, as in function application or
+  let-statements, and we can simply substitute the variable name(s) for their
+  bound term in the relevant scope.
 
--------------------------------------------------------------------------------}
+  We use a Reader monad to access top-level bindings in the program text - i.e.,
+  function definitions outside the current program statement.
+
+-}
 
 module Semantics.Interpreter where
 

src/Semantics/PartialEvaluator.hs

@@ -1,4 +1,4 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Semantics.PartialEvaluator
   Description : Partial evaluator for Contra.
@@ -9,13 +9,14 @@
   Stability   : experimental
   Portability : POSIX
 
-  Partial evaluator for Contra, based on online partial evaluation.
+  Partial evaluator for Contra, based on online partial evaluation in the style
+  of the paper 'Tutorial on Online Partial Evaluation' by Cook & Lämmel (2011).
 
   The PartialState monad keeps track of the following contexts:
    - State  : Program a, which is keeps track of specialised functions
    - Reader : Program a, which is the original program text
 
--------------------------------------------------------------------------------}
+-}
 
 module Semantics.PartialEvaluator where
 

src/Semantics/REPL.hs

@@ -1,4 +1,4 @@
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Semantics.REPL
   Description : Rudimentary REPL for Contra.
@@ -15,7 +15,7 @@
   in a program text. Load a program in the terminal using the
   '--load <program-name>.con' option and call functions interactively.
 
--------------------------------------------------------------------------------}
+-}
 
 module Semantics.REPL where
 

src/Validation/Formula.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE FlexibleContexts, ScopedTypeVariables, TypeOperators #-}
 
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Validation.Formula
   Description : Formula monad and SValue definition.
@@ -11,21 +11,24 @@
   Stability   : experimental
   Portability : POSIX
 
+  The Formula file defines the abbreviations and the monad that is used in the
+  PropertyChecker, Translator, and SymUnifier.
+
   This file contains:
-   - Definition of SValue - middle layer between SBV and Contra values
-   - Bindings, which is a mapping from variable names to SValues
-   - The Formula monad
-   - Function 'bind' to create or update Bindings
-   - `Mergeable` instance for SValues
-   - Helper function 'sEqual' for comparing SValues
+   * Definition of SValue - middle layer between SBV and Contra values
+   * Bindings, which is a mapping from variable names to SValues
+   * The Formula monad
+   * Function 'bind' to create or update Bindings
+   * `Mergeable` instance for SValues
+   * Helper function 'sEqual' for comparing SValues
 
   The Formula monad is an instantiation of the ERSymbolic monad and keeps track
   of the following contexts:
-   - Environment : Type, which is the typed program text
-   - Reader      : Bindings, which are mappings from variable names to SValues
-   - Symbolic    : SBV's Symbolic monad, which keeps track of solver state
+   * Environment : Type, which is the typed program text
+   * Reader      : Bindings, which are mappings from variable names to SValues
+   * Symbolic    : SBV's Symbolic monad, which keeps track of solver state
 
--------------------------------------------------------------------------------}
+-}
 
 module Validation.Formula where
 

src/Validation/PropertyChecker.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE FlexibleContexts, ScopedTypeVariables, LambdaCase #-}
 
-{-------------------------------------------------------------------------------
+{-
 
   Module      : Validation.PropertyChecker
   Description : PropertyChecker for Contra.
@@ -11,9 +11,35 @@
   Stability   : experimental
   Portability : POSIX
 
-  -- TODO: Description of PropertyChecker
+  The PropertyChecker is the driver for the property-checking code, which is
+  primarily the Translator.
 
--------------------------------------------------------------------------------}
+  Its main functions are:
+   * 'check'
+   * 'checkProperty'
+   * 'generateFormula'
+   * 'realise'
+   * 'proveFormula'
+
+  'check' checks all the properties in a program by calling 'checkProperty'
+  on each property and collecting the residual (partially evaluated) program
+  for each call.
+
+  'checkProperty' checks a single property by partially evaluating the property
+  wrt. the program text, generating an SValue formula, converting it back to
+  an SBV formula, proving the formula, and returning the partially evaluated
+  program.
+
+  'generateFormula' calls 'translateToFormula' from Validation.Translator to
+  generate an SValue formula.
+
+  'realise' turns that SValue formula into an SBV formula.
+
+  'proveFormula' asks the SMT solver, via the SBV bindings, to prove the
+  generated formula, which succeeds, returns a counterexample, or produces
+  an unknown result.
+
+-}
 
 module Validation.PropertyChecker where