From 895066fe3c7af3100bb43c02575d3db3bd480b57 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 14:00:50 -0300 Subject: [PATCH 01/15] add: doc and update readme --- README.md | 71 ++++++++++++++++++++++++----- docs/code/CHANGELOG.md | 16 +++++++ docs/code/app.md | 28 ++++++++++++ docs/code/app/Main.md | 27 +++++++++++ docs/code/cabal.md | 28 ++++++++++++ docs/code/introduction.md | 43 ++++++++++++++++++ docs/code/kind-lang.md | 56 +++++++++++++++++++++++ docs/code/main.md | 84 +++++++++++++++++++++++++++++++++++ docs/code/src.md | 26 +++++++++++ docs/code/src/Kind.md | 24 ++++++++++ docs/code/src/Kind/API.md | 60 +++++++++++++++++++++++++ docs/code/src/Kind/Check.md | 54 ++++++++++++++++++++++ docs/code/src/Kind/Compile.md | 39 ++++++++++++++++ docs/code/src/Kind/Env.md | 42 ++++++++++++++++++ docs/code/src/Kind/Equal.md | 50 +++++++++++++++++++++ docs/code/src/Kind/Parse.md | 47 ++++++++++++++++++++ docs/code/src/Kind/Reduce.md | 70 +++++++++++++++++++++++++++++ docs/code/src/Kind/Show.md | 53 ++++++++++++++++++++++ docs/code/src/Kind/Type.md | 55 +++++++++++++++++++++++ 19 files changed, 862 insertions(+), 11 deletions(-) create mode 100644 docs/code/CHANGELOG.md create mode 100644 docs/code/app.md create mode 100644 docs/code/app/Main.md create mode 100644 docs/code/cabal.md create mode 100644 docs/code/introduction.md create mode 100644 docs/code/kind-lang.md create mode 100644 docs/code/main.md create mode 100644 docs/code/src.md create mode 100644 docs/code/src/Kind.md create mode 100644 docs/code/src/Kind/API.md create mode 100644 docs/code/src/Kind/Check.md create mode 100644 docs/code/src/Kind/Compile.md create mode 100644 docs/code/src/Kind/Env.md create mode 100644 docs/code/src/Kind/Equal.md create mode 100644 docs/code/src/Kind/Parse.md create mode 100644 docs/code/src/Kind/Reduce.md create mode 100644 docs/code/src/Kind/Show.md create mode 100644 docs/code/src/Kind/Type.md diff --git a/README.md b/README.md index 95604a66a..639854f4c 100644 --- a/README.md +++ b/README.md @@ -1,23 +1,69 @@ -# Kind-Core +# Kind -Kind is a minimal Proof Checker. +Kind is a minimalist proof checker. -Examples on [MonoBook](https://github.com/HigherOrderCO/MonoBook) (search for `.kind` files) +Examples can be found in the [MonoBook](https://github.com/HigherOrderCO/MonoBook) (look for `.kind` files). -# Usage +## Usage -1. Clone and install this project +### Installation with Haskell and Cabal -2. Use the `kind` command to check/run terms +To install Kind using Haskell and Cabal, follow these steps: -## Grammar: +1. Clone the repository: + ``` + git clone https://github.com/HigherOrderCO/Kind-Core.git + ``` + +2. Navigate to the project directory: + ``` + cd Kind-Core + ``` + +3. Update Cabal's package list: + ``` + cabal update + ``` + +4. Build the project: + ``` + cabal build + ``` + +5. Install the Kind executable: + ``` + cabal install + ``` + +6. Verify the installation: + ``` + kind --version + ``` + +Note: Ensure that Haskell and Cabal are installed on your system and that Cabal's binary directory is in your PATH. + +### Usage + +Kind can be used with the following commands: + +- `kind check`: Checks all .kind files in the current directory and subdirectories +- `kind check `: Type-checks all definitions in the specified file +- `kind run `: Normalizes the specified definition +- `kind show `: Stringifies the specified definition +- `kind to-js `: Compiles the specified definition to JavaScript +- `kind deps `: Shows immediate dependencies of the specified definition +- `kind rdeps `: Shows all dependencies of the specified definition recursively +- `kind help`: Shows the help message + + +## Grammar + +The grammar of Kind is defined as follows: ``` - ::= - + ::= - ::= - + ::= ::= | ALL: "∀(" ":" ")" @@ -51,3 +97,6 @@ Examples on [MonoBook](https://github.com/HigherOrderCO/MonoBook) (search for `. | ">" | "==" | "!=" | "&" | "|" | "^" | "<<" | ">>" ``` + +This grammar defines the syntactic structure of the Kind language, including terms, constructors, operators, and other fundamental elements. + diff --git a/docs/code/CHANGELOG.md b/docs/code/CHANGELOG.md new file mode 100644 index 000000000..d62889e1c --- /dev/null +++ b/docs/code/CHANGELOG.md @@ -0,0 +1,16 @@ +--- +title: CHANGELOG +description: 'Revision history for the kind2hs project' +--- + +# Revision History + +This document records the changes and updates made to the kind2hs project over time. + +## 0.1.0.0 + +- Release date: YYYY-mm-dd +- First version of the project +- Initial public release + +Note: The specific release date has not been defined yet and is represented as YYYY-mm-dd in the record. diff --git a/docs/code/app.md b/docs/code/app.md new file mode 100644 index 000000000..295f9d3f5 --- /dev/null +++ b/docs/code/app.md @@ -0,0 +1,28 @@ +--- +title: App +description: 'Directory containing the entry point of the Kind application' +--- + +# App + +The `app` directory is an essential part of the Kind project structure. It contains the main entry point of the application, typically a `Main.hs` file. + +## Structure + +The `app` directory usually includes: + +- `Main.hs`: The main file containing the `main` function, which is the entry point of the Kind application. + +## Purpose + +The purpose of the `app` directory is to: + +1. Separate the main application code from the library code. +2. Contain the initialization and configuration logic of the application. +3. Provide a clear entry point for program execution. + +## Usage + +The code in the `app` directory typically imports and utilizes the functionalities defined in the `src` directory, combining them to create the complete application. + +For more details on the specific content and implementation, refer to the `Main.hs` file within this directory. diff --git a/docs/code/app/Main.md b/docs/code/app/Main.md new file mode 100644 index 000000000..fbc1da09e --- /dev/null +++ b/docs/code/app/Main.md @@ -0,0 +1,27 @@ +--- +title: Main +description: 'Main module that initiates the execution of the Kind compiler' +--- + +# Main + +This module is the entry point for the Kind compiler. It imports and executes the `main` function from the `Kind` module. + +## Structure + +The `Main` module consists of: + +1. A module declaration +2. An import of the `Kind` module +3. A definition of the `main` function + +## Main function + +```haskell +main :: IO () +main = Kind.main +``` + +The `main` function is defined with the type `IO ()`, indicating that it performs input/output operations. It simply calls the `main` function from the `Kind` module, delegating all the compiler's execution logic to that module. + +This structure allows for a clear separation between the program's entry point and the main logic of the compiler, which is contained in the `Kind` module. diff --git a/docs/code/cabal.md b/docs/code/cabal.md new file mode 100644 index 000000000..e52b63de1 --- /dev/null +++ b/docs/code/cabal.md @@ -0,0 +1,28 @@ +--- +title: cabal.project +description: 'Cabal project configuration for the Kind compiler' +--- + +# cabal.project + +This file contains the Cabal project configuration for the Kind compiler. + +## Content + +``` +packages: . + +-- Enable -O2 optimization for all packages +package * + optimization: 2 +``` + +## Details + +1. `packages: .`: Indicates that the package is located in the current directory. + +2. `package *`: This line starts a configuration section that applies to all packages. + +3. `optimization: 2`: Sets the optimization level to 2 (equivalent to -O2) for all packages. This instructs the compiler to perform more aggressive optimizations during compilation, potentially improving the performance of the generated code. + +This configuration ensures that all packages in the project are compiled with level 2 optimizations, which can result in more efficient code, although it may increase compilation time. diff --git a/docs/code/introduction.md b/docs/code/introduction.md new file mode 100644 index 000000000..adf5c0a57 --- /dev/null +++ b/docs/code/introduction.md @@ -0,0 +1,43 @@ +--- +title: Introduction to Kind-Core +description: 'A guide to get started with Kind, a minimalist proof checker' +--- + +# Introduction to Kind-Core + +Kind-Core is a minimalist proof checker. This project provides a powerful tool for verifying and executing terms in a dependent type system. + +## Overview + +Kind-Core is designed to be a lean and efficient implementation of a proof checker. It supports a rich grammar that allows the expression of complex concepts in type theory, including universal quantification, lambda abstraction, function application, type annotations, recursive types, and much more. + +## About the Project + +The project is structured into several main parts: + +- `src/Kind`: Contains the main modules of the proof checker. +- `app`: Contains the application entry point. +- `cabal.project` and `kind-lang.cabal`: Haskell project configuration files. + +## How to Run + +To start using Kind-Core: + +1. Clone this repository. +2. Install the project following the Haskell setup instructions. +3. Use the `kind` command to verify or execute terms. + +## Requirements + +- GHC (Glasgow Haskell Compiler) +- Cabal or Stack for Haskell package management + +## Examples + +Examples of Kind usage can be found in the [MonoBook](https://github.com/HigherOrderCO/MonoBook) repository. Look for files with the `.kind` extension. + +## Grammar + +Kind-Core uses a specific grammar to define terms. The complete grammar can be found in the project's README, including constructions for universal quantifiers, lambda abstractions, applications, type annotations, recursive types, data constructors, and more. + +For more details on the grammar and advanced usage, refer to the project's full documentation. diff --git a/docs/code/kind-lang.md b/docs/code/kind-lang.md new file mode 100644 index 000000000..826d9c8c6 --- /dev/null +++ b/docs/code/kind-lang.md @@ -0,0 +1,56 @@ +--- +title: kind-lang.cabal +description: 'Cabal configuration file for the kind-lang project' +--- + +# kind-lang.cabal + +This file is the Cabal configuration file for the kind-lang project. It defines the package specifications, dependencies, and project structure. + +## Package Details + +- **Name**: kind-lang +- **Version**: 0.1.0.0 +- **License**: MIT +- **Author**: Victor Taelin +- **Maintainer**: victor.taelin@gmail.com +- **Category**: Language + +## Library + +The library exposes the following modules: + +- Kind +- Kind.API +- Kind.Check +- Kind.Compile +- Kind.Env +- Kind.Equal +- Kind.Parse +- Kind.Reduce +- Kind.Show +- Kind.Type + +Main dependencies: + +- base ^>=4.20.0.0 +- containers ==0.7 +- parsec ==3.1.17.0 +- ansi-terminal==1.1.1 +- directory==1.3.8.3 +- hs-highlight == 1.0.3 +- filepath==1.5.2.0 + +## Executable + +The project also defines an executable called "kind" with the following characteristics: + +- **Main file**: Main.hs +- **Dependencies**: Includes the kind-lang library itself and other dependencies shared with the library. + +## Common Settings + +- The project uses GHC2024 as the default language. +- Warnings are enabled for both the library and executable. + +This Cabal file provides a clear overview of the kind-lang project's structure and dependencies, facilitating its compilation and distribution. diff --git a/docs/code/main.md b/docs/code/main.md new file mode 100644 index 000000000..4b9e41d93 --- /dev/null +++ b/docs/code/main.md @@ -0,0 +1,84 @@ +--- +title: main.kindc +description: 'Type and function definitions in Kind, including Bool, Nat, IsTrue, Equal and rewrite' +--- + +# main.kindc + +This file contains fundamental type and function definitions in Kind, a functional programming language with a dependent type system. + +## Basic Types + +### Bool + +Defines the boolean type with two constructors: + +```kind +Bool : * = #[]{ + #true{} : Bool + #false{} : Bool +}; +``` + +### Nat + +Defines the natural numbers type with two constructors: + +```kind +Nat : * = #[]{ + #zero{} : Nat + #succ{ pred: Nat } : Nat +}; +``` + +## Predicates and Equality + +### IsTrue + +A predicate that checks if a boolean is true: + +```kind +IsTrue : ∀(b: Bool) * = λb #[b]{ + #indeed{} : (IsTrue #true{}) +}; +``` + +### Equal + +Defines propositional equality between two values of the same type: + +```kind +Equal : ∀(T: *) ∀(a: T) ∀(b: T) * = λT λa λb #[a b]{ + #refl{} : (Equal T a a) +}; +``` + +## Functions + +### rewrite + +A function that allows rewriting an equality proof: + +```kind +rewrite +: ∀(T: *) + ∀(a: T) + ∀(b: T) + ∀(e: (Equal T a b)) + ∀(P: ∀(x: A) *) + ∀(x: (P a)) + (P b) += λT λa λb λ{ + #refl: λP λx x +}; +``` + +## Entry Point + +The program's entry point is defined as: + +```kind +MAIN = rewrite; +``` + +This file serves as a foundation for fundamental definitions in Kind, including basic types, predicates, and equality manipulation functions. diff --git a/docs/code/src.md b/docs/code/src.md new file mode 100644 index 000000000..203a2ae47 --- /dev/null +++ b/docs/code/src.md @@ -0,0 +1,26 @@ +--- +title: src +description: 'Main directory containing the source code of the Kind project' +--- + +# src + +This directory contains the main source code of the Kind project. Here you will find the essential modules that make up the core of the Kind language and compiler. + +## Structure + +The `src` directory is organized as follows: + +- `Kind.hs`: Main module that likely exports the core functionalities of the Kind language. +- `Kind/`: Subdirectory containing specific modules: + - `API.hs`: Application programming interface. + - `Check.hs`: Type checker implementation. + - `Compile.hs`: Compilation logic. + - `Env.hs`: Environment management. + - `Equal.hs`: Equality implementation. + - `Parse.hs`: Syntactic analyzer. + - `Reduce.hs`: Reduction mechanism. + - `Show.hs`: Display and formatting functions. + - `Type.hs`: Type definitions. + +Each of these files plays a crucial role in the functioning of the Kind compiler and language. To fully understand the project, it is recommended to examine each of these modules individually. diff --git a/docs/code/src/Kind.md b/docs/code/src/Kind.md new file mode 100644 index 000000000..6744cf407 --- /dev/null +++ b/docs/code/src/Kind.md @@ -0,0 +1,24 @@ +--- +title: Kind +description: 'Main module of the Kind language, containing essential subcomponents for analysis, verification, and compilation' +--- + +# Kind + +The `Kind` directory is the core of the Kind language implementation. It contains several Haskell modules that together form the main structure of the language's compiler and type system. + +## Structure + +The `Kind` directory includes the following files: + +- `API.hs`: Defines the programming interface of the Kind language. +- `Check.hs`: Implements type checking. +- `Compile.hs`: Contains the compilation logic of the language. +- `Env.hs`: Manages the execution environment and context. +- `Equal.hs`: Implements the logic for equality between types and terms. +- `Parse.hs`: Responsible for syntactic analysis of the source code. +- `Reduce.hs`: Implements reduction and evaluation of expressions. +- `Show.hs`: Provides functionalities for displaying and formatting language structures. +- `Type.hs`: Defines the fundamental types and data structures of the Kind language. + +Each of these modules plays a crucial role in the functioning of the Kind language's compiler and type system, working together to analyze, verify, and compile programs written in this language. diff --git a/docs/code/src/Kind/API.md b/docs/code/src/Kind/API.md new file mode 100644 index 000000000..2a34cd9f7 --- /dev/null +++ b/docs/code/src/Kind/API.md @@ -0,0 +1,60 @@ +--- +title: API +description: 'Main module that defines the API and core functions of Kind Language' +--- + +# API + +This module contains the main API functions of Kind Language, including file loading, type checking, normalization, compilation to JavaScript, and other utilities. + +## Main Functions + +### `findBookDir` + +Finds the directory called "book" or "monobook" starting from the current directory. + +### `extractName` + +Extracts the definition name from a file path or name. + +### `apiLoad` + +Loads a Kind file and returns the book, a map of file paths to top-level definitions, and a dependency map. + +### `apiNormal` + +Normalizes a term and displays the result. + +### `apiCheckFile` + +Type checks all terms in a file. + +### `apiCheckAll` + +Type checks all Kind files in the base directory and its subdirectories. + +### `apiShow` + +Displays a term. + +### `apiToJS` + +Compiles the entire book to JavaScript. + +### `getDeps` and `getAllDeps` + +Gets the direct and indirect dependencies of a term, respectively. + +## Main Function + +The `main` function processes command-line arguments and executes the corresponding operation: + +- `check`: Checks all Kind files or a specific file +- `run`: Normalizes a specific definition +- `show`: Displays a specific definition +- `to-js`: Compiles a specific definition to JavaScript +- `deps`: Shows the immediate dependencies of a definition +- `rdeps`: Shows all dependencies of a definition recursively +- `help`: Displays the help message + +This module provides the main interface for interacting with Kind Language, allowing loading, checking, normalizing, and compiling Kind definitions. diff --git a/docs/code/src/Kind/Check.md b/docs/code/src/Kind/Check.md new file mode 100644 index 000000000..4599c6e33 --- /dev/null +++ b/docs/code/src/Kind/Check.md @@ -0,0 +1,54 @@ +--- +title: Check +description: 'Module responsible for type checking in the Kind compiler' +--- + +# Check + +The `Check` module is responsible for type checking in the Kind compiler. It implements the main functions for type inference and checking, as well as auxiliary functions for handling telescopes. + +## Main Functions + +### infer + +```haskell +infer :: Term -> Int -> Env Term +``` + +Infers the type of a given term. It takes a term and a depth as arguments and returns the inferred type within the `Env` environment. + +### check + +```haskell +check :: Maybe Cod -> Term -> Term -> Int -> Env () +``` + +Checks if a term has the expected type. It takes an optional source code, the term to be checked, the expected type, and the depth. + +### doCheck + +```haskell +doCheck :: Term -> Env () +``` + +High-level function to initiate type checking of a term. + +## Auxiliary Functions + +- `checkTele`: Checks types for telescopes. +- `checkConAgainstTele`: Checks constructors against telescopes. +- `teleToType`: Converts a telescope to a type. +- `teleToTerm`: Converts a telescope to a term. +- `extractEqualities`: Extracts equalities from data types. + +## Implementation Details + +The module uses various techniques to handle different language constructs, including: + +- Type checking for functions (lambdas) +- Handling of dependent types +- Checking of data constructors +- Type inference for pattern matching expressions +- Manipulation of references and definitions + +The module also includes error handling and logging to assist in diagnosing problems during type checking. diff --git a/docs/code/src/Kind/Compile.md b/docs/code/src/Kind/Compile.md new file mode 100644 index 000000000..18a6a0ec6 --- /dev/null +++ b/docs/code/src/Kind/Compile.md @@ -0,0 +1,39 @@ +--- +title: Compile +description: 'Module responsible for compiling terms and books to JavaScript' +--- + +# Compile + +This module contains functions to compile terms and books from the Kind language to JavaScript. + +## Main Functions + +### `nameToJS` + +Converts Kind language names to valid JavaScript names. + +### `termToJS` + +Converts a Kind language term to its JavaScript representation. + +### `operToJS` + +Maps Kind language operators to their JavaScript equivalents. + +### `bookToJS` + +Converts a book (set of definitions) from the Kind language to JavaScript. + +### `compileJS` + +Main compilation function that generates the complete JavaScript code, including a preamble with helper functions. + +## Implementation Details + +- The `termToJS` function handles different Kind language constructs, such as lambdas, applications, annotations, constructors, etc. +- `operToJS` maps arithmetic and logical operators to their JavaScript equivalents. +- `bookToJS` converts each book definition into a JavaScript assignment. +- `compileJS` includes a preamble with the `APPLY` function, which handles the application of functions to multiple arguments. + +This module is essential for generating executable JavaScript code from programs written in the Kind language. diff --git a/docs/code/src/Kind/Env.md b/docs/code/src/Kind/Env.md new file mode 100644 index 000000000..5b004938e --- /dev/null +++ b/docs/code/src/Kind/Env.md @@ -0,0 +1,42 @@ +--- +title: Env +description: 'Module that defines the environment and related operations for the Kind system' +--- + +# Env + +This module defines the environment (`Env`) and various related operations for the Kind system. The environment is used to manage the state during term checking and compilation. + +## Main Structure + +- `Env`: Represents the execution environment. +- `State`: Contains the current state, including the book (`Book`), fillings (`Fill`), suspensions (`Susp`), and logs. + +## Main Functions + +### Environment Operations + +- `envBind`: Binds an environment to a function that produces another environment. +- `envPure`: Creates a pure environment with a value. +- `envFail`: Creates a failing environment. +- `envRun`: Runs an environment with a given book. + +### State Manipulation + +- `envLog`: Adds information to the log. +- `envSnapshot`: Captures the current state. +- `envRewind`: Returns to the previous state. +- `envSusp`: Adds a check to the list of suspensions. +- `envFill`: Inserts a term into the fillings map. + +### Accessors + +- `envGetFill`: Gets the current fillings map. +- `envGetBook`: Gets the current book. +- `envTakeSusp`: Gets and clears the list of suspensions. + +## Instances + +The module also provides instances of `Functor`, `Applicative`, and `Monad` for `Env`, allowing the use of monadic operations with the environment. + +This module is fundamental to the internal workings of the Kind system, managing the state and operations during the verification and compilation process. diff --git a/docs/code/src/Kind/Equal.md b/docs/code/src/Kind/Equal.md new file mode 100644 index 000000000..c44e7ccd4 --- /dev/null +++ b/docs/code/src/Kind/Equal.md @@ -0,0 +1,50 @@ +--- +title: Equal +description: 'Module responsible for checking equality between terms and performing pattern unification' +--- + +# Equal + +The `Equal` module provides functionalities to check equality between terms and perform pattern unification in the context of a dependent type system. + +## Main Functions + +### equal + +Checks if two terms are equal after reduction steps. + +```haskell +equal :: Term -> Term -> Int -> Env Bool +``` + +### identical + +Checks if two terms are syntactically identical. + +```haskell +identical :: Term -> Term -> Int -> Env Bool +``` + +### similar + +Checks if two terms are equal component by component. + +```haskell +similar :: Term -> Term -> Int -> Env Bool +``` + +### unify + +Attempts to solve a pattern unification problem, generating a substitution if possible. + +```haskell +unify :: Int -> [Term] -> Term -> Int -> Env Bool +``` + +## Auxiliary Functions + +- `valid`: Checks if a problem is solvable by pattern unification. +- `solve`: Generates the solution for a unification problem, adding bindings and renaming variables. +- `occur`: Checks if a metavariable occurs recursively within a term. + +This module is fundamental for implementing type checking and inference in dependent type systems, providing the basic operations necessary to compare and unify terms. diff --git a/docs/code/src/Kind/Parse.md b/docs/code/src/Kind/Parse.md new file mode 100644 index 000000000..9aee3fb1c --- /dev/null +++ b/docs/code/src/Kind/Parse.md @@ -0,0 +1,47 @@ +--- +title: Parse +description: 'Module responsible for the syntactic analysis of the Kind language' +--- + +# Parse + +The `Kind.Parse` module is responsible for the syntactic analysis of the Kind language. It defines the structures and functions necessary to convert the source code into an abstract representation that can be processed by the compiler. + +## Main structures + +- `Uses`: List of tuples representing name aliases. +- `PState`: Parser state, containing the file name and the list of Uses. +- `Parser`: Custom type for the parser, based on Parsec. + +## Main functions + +### Term parsing + +- `doParseTerm`: Parses a complete term from an input string. +- `parseTerm`: Main parser for Kind language terms. + +### Parsing uses and books + +- `doParseUses`: Parses the use declarations (aliases) at the beginning of the file. +- `doParseBook`: Parses a complete book, including uses and definitions. + +### Error handling + +- `showParseError`: Displays parsing errors in a user-friendly way, highlighting the error position. + +### Specific parsers + +The module includes parsers for various language constructs, such as: + +- `parseAll`: For universal quantifiers. +- `parseLam`: For lambda expressions. +- `parseApp`: For function applications. +- `parseAnn`: For type annotations. +- `parseDat`: For data type definitions. +- `parseCon`: For data type constructors. +- `parseSwi`: For switch expressions. +- `parseMat`: For pattern matching expressions. + +## Usage + +This module is used internally by the Kind compiler to transform the source code into a data structure that can be processed by subsequent compilation stages, such as type checking and code generation. diff --git a/docs/code/src/Kind/Reduce.md b/docs/code/src/Kind/Reduce.md new file mode 100644 index 000000000..80f883fe0 --- /dev/null +++ b/docs/code/src/Kind/Reduce.md @@ -0,0 +1,70 @@ +--- +title: Reduce +description: 'Module responsible for reduction and normalization of terms in Kind' +--- + +# Reduce + +This module implements the functionalities for reduction and normalization of terms in the Kind language. + +## Main Functions + +### reduce + +```haskell +reduce :: Book -> Fill -> Int -> Term -> Term +``` + +Evaluates a term to its weak normal form. The `lv` parameter defines when to expand references: +- 0 = never +- 1 = in redexes + +### normal + +```haskell +normal :: Book -> Fill -> Int -> Term -> Int -> Term +``` + +Evaluates a term to its complete normal form. + +### bind + +```haskell +bind :: Term -> [(String,Term)] -> Term +``` + +Binds quoted variables to bound HOAS variables. + +### genMetas + +```haskell +genMetas :: Term -> Term +``` + +Generates metavariables for a term. + +### subst + +```haskell +subst :: Int -> Term -> Term -> Term +``` + +Substitutes a Bruijn level variable with a new value in a term. + +## Data Structures + +The module uses the following main structures: + +- `Term`: Represents terms in the Kind language +- `Book`: Map of definitions +- `Fill`: Map of fillings for metavariables + +## Implementation Details + +- The `reduce` function implements the lazy reduction strategy, evaluating only when necessary. +- `normal` performs a complete normalization, including subterms. +- `bind` is used to bind variables in lambda abstractions and universal quantifiers. +- `genMetas` is used to generate unique metavariables in a term. +- `subst` implements variable substitution, respecting the term structure. + +This module is fundamental for the type system and evaluation of the Kind language, providing the basic reduction and normalization operations necessary for term processing. diff --git a/docs/code/src/Kind/Show.md b/docs/code/src/Kind/Show.md new file mode 100644 index 000000000..6e424fed6 --- /dev/null +++ b/docs/code/src/Kind/Show.md @@ -0,0 +1,53 @@ +--- +title: Show +description: 'Module responsible for displaying and formatting terms and information in the Kind compiler' +--- + +# Show + +The `Kind.Show` module is responsible for providing functions to display and format terms, contexts, and information in the Kind compiler. It defines various helper functions to convert internal data structures into readable string representations. + +## Main Functions + +### termShower + +```haskell +termShower :: Bool -> Term -> Int -> String +``` + +This function is the core of term display. It takes a boolean to control the level of detail, a term, and a depth, and returns a string representation of the term. + +### contextShow + +```haskell +contextShow :: Book -> Fill -> [Term] -> Int -> String +``` + +Displays a context (list of terms) with annotations. + +### infoShow + +```haskell +infoShow :: Book -> Fill -> Info -> IO String +``` + +Formats different types of information (such as goals, errors, solutions) for display. + +## Helper Functions + +- `unwrapApp`: Unpacks nested function applications. +- `termShow`: Simplified version of `termShower`. +- `operShow`: Converts operators to their string representations. +- `teleShower`: Displays telescopes (data structures for dependent parameters). + +## Error Handling + +The module includes functions for reading source files and resolving absolute paths, which are used to display error information with source code context. + +## Notes + +- The module makes extensive use of string concatenation to build representations. +- It uses ANSI codes to color the output in the terminal. +- Integrates with a syntax highlighting module (`Highlight`) to improve error display. + +This module is crucial for providing readable and useful feedback during compilation and type checking in the Kind compiler. diff --git a/docs/code/src/Kind/Type.md b/docs/code/src/Kind/Type.md new file mode 100644 index 000000000..5d89b5730 --- /dev/null +++ b/docs/code/src/Kind/Type.md @@ -0,0 +1,55 @@ +--- +title: Type +description: 'Type definitions and data structures for the Kind compiler' +--- + +# Type + +This module defines the fundamental data structures used in the Kind compiler. + +## Main Structures + +### Term + +Represents the abstract syntax tree (AST) of Kind. Includes constructions such as: + +- `All`: Dependent product (∀) +- `Lam`: Lambda abstraction +- `App`: Function application +- `Ann`: Type annotation +- `Slf`: Recursive type +- `Ins`: Recursive type instantiation +- `Dat`: Data type definition +- `Con`: Data constructor +- `Mat`: Pattern matching +- `Ref`: Top-level reference +- `Let`: Local definition +- `Use`: Use of local definition +- `Set`: Type of types +- `U32`: 32-bit integer type +- `Num`: Integer value +- `Op2`: Binary operation +- `Swi`: U32 elimination +- `Hol`: Inspection hole +- `Met`: Unification metavariable +- `Var`: Variable +- `Src`: Source code location +- `Txt`: Text literal +- `Nat`: Natural literal + +### Other Structures + +- `Loc`: Source code location (name, line, column) +- `Cod`: Code range +- `Oper`: Numeric operators +- `Tele`: Telescope (sequence of typed arguments) +- `Ctr`: Data type constructor +- `Book`: Map of definitions +- `Info`: Type checker outputs +- `Fill`: Unification solutions +- `Check`: Type checker state +- `State`: Global compiler state +- `Res`: Checking result +- `Env`: Type checker monadic environment + +This module provides the essential data structures for representing and manipulating Kind programs during the compilation process. From 2d03f8545668e5d5473ee6935677ba0208f616e6 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 14:03:12 -0300 Subject: [PATCH 02/15] fix: dir docs/code --- docs/{code => }/CHANGELOG.md | 0 docs/{code => }/app.md | 0 docs/{code => }/app/Main.md | 0 docs/{code => }/cabal.md | 0 docs/{code => }/introduction.md | 0 docs/{code => }/kind-lang.md | 0 docs/{code => }/main.md | 0 docs/{code => }/src.md | 0 docs/{code => }/src/Kind.md | 0 docs/{code => }/src/Kind/API.md | 0 docs/{code => }/src/Kind/Check.md | 0 docs/{code => }/src/Kind/Compile.md | 0 docs/{code => }/src/Kind/Env.md | 0 docs/{code => }/src/Kind/Equal.md | 0 docs/{code => }/src/Kind/Parse.md | 0 docs/{code => }/src/Kind/Reduce.md | 0 docs/{code => }/src/Kind/Show.md | 0 docs/{code => }/src/Kind/Type.md | 0 18 files changed, 0 insertions(+), 0 deletions(-) rename docs/{code => }/CHANGELOG.md (100%) rename docs/{code => }/app.md (100%) rename docs/{code => }/app/Main.md (100%) rename docs/{code => }/cabal.md (100%) rename docs/{code => }/introduction.md (100%) rename docs/{code => }/kind-lang.md (100%) rename docs/{code => }/main.md (100%) rename docs/{code => }/src.md (100%) rename docs/{code => }/src/Kind.md (100%) rename docs/{code => }/src/Kind/API.md (100%) rename docs/{code => }/src/Kind/Check.md (100%) rename docs/{code => }/src/Kind/Compile.md (100%) rename docs/{code => }/src/Kind/Env.md (100%) rename docs/{code => }/src/Kind/Equal.md (100%) rename docs/{code => }/src/Kind/Parse.md (100%) rename docs/{code => }/src/Kind/Reduce.md (100%) rename docs/{code => }/src/Kind/Show.md (100%) rename docs/{code => }/src/Kind/Type.md (100%) diff --git a/docs/code/CHANGELOG.md b/docs/CHANGELOG.md similarity index 100% rename from docs/code/CHANGELOG.md rename to docs/CHANGELOG.md diff --git a/docs/code/app.md b/docs/app.md similarity index 100% rename from docs/code/app.md rename to docs/app.md diff --git a/docs/code/app/Main.md b/docs/app/Main.md similarity index 100% rename from docs/code/app/Main.md rename to docs/app/Main.md diff --git a/docs/code/cabal.md b/docs/cabal.md similarity index 100% rename from docs/code/cabal.md rename to docs/cabal.md diff --git a/docs/code/introduction.md b/docs/introduction.md similarity index 100% rename from docs/code/introduction.md rename to docs/introduction.md diff --git a/docs/code/kind-lang.md b/docs/kind-lang.md similarity index 100% rename from docs/code/kind-lang.md rename to docs/kind-lang.md diff --git a/docs/code/main.md b/docs/main.md similarity index 100% rename from docs/code/main.md rename to docs/main.md diff --git a/docs/code/src.md b/docs/src.md similarity index 100% rename from docs/code/src.md rename to docs/src.md diff --git a/docs/code/src/Kind.md b/docs/src/Kind.md similarity index 100% rename from docs/code/src/Kind.md rename to docs/src/Kind.md diff --git a/docs/code/src/Kind/API.md b/docs/src/Kind/API.md similarity index 100% rename from docs/code/src/Kind/API.md rename to docs/src/Kind/API.md diff --git a/docs/code/src/Kind/Check.md b/docs/src/Kind/Check.md similarity index 100% rename from docs/code/src/Kind/Check.md rename to docs/src/Kind/Check.md diff --git a/docs/code/src/Kind/Compile.md b/docs/src/Kind/Compile.md similarity index 100% rename from docs/code/src/Kind/Compile.md rename to docs/src/Kind/Compile.md diff --git a/docs/code/src/Kind/Env.md b/docs/src/Kind/Env.md similarity index 100% rename from docs/code/src/Kind/Env.md rename to docs/src/Kind/Env.md diff --git a/docs/code/src/Kind/Equal.md b/docs/src/Kind/Equal.md similarity index 100% rename from docs/code/src/Kind/Equal.md rename to docs/src/Kind/Equal.md diff --git a/docs/code/src/Kind/Parse.md b/docs/src/Kind/Parse.md similarity index 100% rename from docs/code/src/Kind/Parse.md rename to docs/src/Kind/Parse.md diff --git a/docs/code/src/Kind/Reduce.md b/docs/src/Kind/Reduce.md similarity index 100% rename from docs/code/src/Kind/Reduce.md rename to docs/src/Kind/Reduce.md diff --git a/docs/code/src/Kind/Show.md b/docs/src/Kind/Show.md similarity index 100% rename from docs/code/src/Kind/Show.md rename to docs/src/Kind/Show.md diff --git a/docs/code/src/Kind/Type.md b/docs/src/Kind/Type.md similarity index 100% rename from docs/code/src/Kind/Type.md rename to docs/src/Kind/Type.md From 18637bbba9273e44d2819d0cb8d9bb295580fc12 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 14:04:28 -0300 Subject: [PATCH 03/15] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 639854f4c..53cc98e26 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ To install Kind using Haskell and Cabal, follow these steps: 2. Navigate to the project directory: ``` - cd Kind-Core + cd Kind ``` 3. Update Cabal's package list: From 5717c319300f485d30c9a45f9c5f0ab0b4ce1ab9 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 14:05:24 -0300 Subject: [PATCH 04/15] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 53cc98e26..0e87796d4 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ To install Kind using Haskell and Cabal, follow these steps: 2. Navigate to the project directory: ``` - cd Kind + cd Kind-core ``` 3. Update Cabal's package list: From b1b8f35c58dc8a4973e28b41e3b1e6fe54c60309 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 14:16:44 -0300 Subject: [PATCH 05/15] Update README.md rm -core from name --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 0e87796d4..0eaf41a41 100644 --- a/README.md +++ b/README.md @@ -12,12 +12,12 @@ To install Kind using Haskell and Cabal, follow these steps: 1. Clone the repository: ``` - git clone https://github.com/HigherOrderCO/Kind-Core.git + git clone https://github.com/HigherOrderCO/Kind.git ``` 2. Navigate to the project directory: ``` - cd Kind-core + cd Kind ``` 3. Update Cabal's package list: From 48a1e12f3112fb203df3b98941c96d8063661b7b Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:28:27 -0300 Subject: [PATCH 06/15] Delete docs/src directory --- docs/src/Kind.md | 24 -------------- docs/src/Kind/API.md | 60 ---------------------------------- docs/src/Kind/Check.md | 54 ------------------------------- docs/src/Kind/Compile.md | 39 ---------------------- docs/src/Kind/Env.md | 42 ------------------------ docs/src/Kind/Equal.md | 50 ---------------------------- docs/src/Kind/Parse.md | 47 --------------------------- docs/src/Kind/Reduce.md | 70 ---------------------------------------- docs/src/Kind/Show.md | 53 ------------------------------ docs/src/Kind/Type.md | 55 ------------------------------- 10 files changed, 494 deletions(-) delete mode 100644 docs/src/Kind.md delete mode 100644 docs/src/Kind/API.md delete mode 100644 docs/src/Kind/Check.md delete mode 100644 docs/src/Kind/Compile.md delete mode 100644 docs/src/Kind/Env.md delete mode 100644 docs/src/Kind/Equal.md delete mode 100644 docs/src/Kind/Parse.md delete mode 100644 docs/src/Kind/Reduce.md delete mode 100644 docs/src/Kind/Show.md delete mode 100644 docs/src/Kind/Type.md diff --git a/docs/src/Kind.md b/docs/src/Kind.md deleted file mode 100644 index 6744cf407..000000000 --- a/docs/src/Kind.md +++ /dev/null @@ -1,24 +0,0 @@ ---- -title: Kind -description: 'Main module of the Kind language, containing essential subcomponents for analysis, verification, and compilation' ---- - -# Kind - -The `Kind` directory is the core of the Kind language implementation. It contains several Haskell modules that together form the main structure of the language's compiler and type system. - -## Structure - -The `Kind` directory includes the following files: - -- `API.hs`: Defines the programming interface of the Kind language. -- `Check.hs`: Implements type checking. -- `Compile.hs`: Contains the compilation logic of the language. -- `Env.hs`: Manages the execution environment and context. -- `Equal.hs`: Implements the logic for equality between types and terms. -- `Parse.hs`: Responsible for syntactic analysis of the source code. -- `Reduce.hs`: Implements reduction and evaluation of expressions. -- `Show.hs`: Provides functionalities for displaying and formatting language structures. -- `Type.hs`: Defines the fundamental types and data structures of the Kind language. - -Each of these modules plays a crucial role in the functioning of the Kind language's compiler and type system, working together to analyze, verify, and compile programs written in this language. diff --git a/docs/src/Kind/API.md b/docs/src/Kind/API.md deleted file mode 100644 index 2a34cd9f7..000000000 --- a/docs/src/Kind/API.md +++ /dev/null @@ -1,60 +0,0 @@ ---- -title: API -description: 'Main module that defines the API and core functions of Kind Language' ---- - -# API - -This module contains the main API functions of Kind Language, including file loading, type checking, normalization, compilation to JavaScript, and other utilities. - -## Main Functions - -### `findBookDir` - -Finds the directory called "book" or "monobook" starting from the current directory. - -### `extractName` - -Extracts the definition name from a file path or name. - -### `apiLoad` - -Loads a Kind file and returns the book, a map of file paths to top-level definitions, and a dependency map. - -### `apiNormal` - -Normalizes a term and displays the result. - -### `apiCheckFile` - -Type checks all terms in a file. - -### `apiCheckAll` - -Type checks all Kind files in the base directory and its subdirectories. - -### `apiShow` - -Displays a term. - -### `apiToJS` - -Compiles the entire book to JavaScript. - -### `getDeps` and `getAllDeps` - -Gets the direct and indirect dependencies of a term, respectively. - -## Main Function - -The `main` function processes command-line arguments and executes the corresponding operation: - -- `check`: Checks all Kind files or a specific file -- `run`: Normalizes a specific definition -- `show`: Displays a specific definition -- `to-js`: Compiles a specific definition to JavaScript -- `deps`: Shows the immediate dependencies of a definition -- `rdeps`: Shows all dependencies of a definition recursively -- `help`: Displays the help message - -This module provides the main interface for interacting with Kind Language, allowing loading, checking, normalizing, and compiling Kind definitions. diff --git a/docs/src/Kind/Check.md b/docs/src/Kind/Check.md deleted file mode 100644 index 4599c6e33..000000000 --- a/docs/src/Kind/Check.md +++ /dev/null @@ -1,54 +0,0 @@ ---- -title: Check -description: 'Module responsible for type checking in the Kind compiler' ---- - -# Check - -The `Check` module is responsible for type checking in the Kind compiler. It implements the main functions for type inference and checking, as well as auxiliary functions for handling telescopes. - -## Main Functions - -### infer - -```haskell -infer :: Term -> Int -> Env Term -``` - -Infers the type of a given term. It takes a term and a depth as arguments and returns the inferred type within the `Env` environment. - -### check - -```haskell -check :: Maybe Cod -> Term -> Term -> Int -> Env () -``` - -Checks if a term has the expected type. It takes an optional source code, the term to be checked, the expected type, and the depth. - -### doCheck - -```haskell -doCheck :: Term -> Env () -``` - -High-level function to initiate type checking of a term. - -## Auxiliary Functions - -- `checkTele`: Checks types for telescopes. -- `checkConAgainstTele`: Checks constructors against telescopes. -- `teleToType`: Converts a telescope to a type. -- `teleToTerm`: Converts a telescope to a term. -- `extractEqualities`: Extracts equalities from data types. - -## Implementation Details - -The module uses various techniques to handle different language constructs, including: - -- Type checking for functions (lambdas) -- Handling of dependent types -- Checking of data constructors -- Type inference for pattern matching expressions -- Manipulation of references and definitions - -The module also includes error handling and logging to assist in diagnosing problems during type checking. diff --git a/docs/src/Kind/Compile.md b/docs/src/Kind/Compile.md deleted file mode 100644 index 18a6a0ec6..000000000 --- a/docs/src/Kind/Compile.md +++ /dev/null @@ -1,39 +0,0 @@ ---- -title: Compile -description: 'Module responsible for compiling terms and books to JavaScript' ---- - -# Compile - -This module contains functions to compile terms and books from the Kind language to JavaScript. - -## Main Functions - -### `nameToJS` - -Converts Kind language names to valid JavaScript names. - -### `termToJS` - -Converts a Kind language term to its JavaScript representation. - -### `operToJS` - -Maps Kind language operators to their JavaScript equivalents. - -### `bookToJS` - -Converts a book (set of definitions) from the Kind language to JavaScript. - -### `compileJS` - -Main compilation function that generates the complete JavaScript code, including a preamble with helper functions. - -## Implementation Details - -- The `termToJS` function handles different Kind language constructs, such as lambdas, applications, annotations, constructors, etc. -- `operToJS` maps arithmetic and logical operators to their JavaScript equivalents. -- `bookToJS` converts each book definition into a JavaScript assignment. -- `compileJS` includes a preamble with the `APPLY` function, which handles the application of functions to multiple arguments. - -This module is essential for generating executable JavaScript code from programs written in the Kind language. diff --git a/docs/src/Kind/Env.md b/docs/src/Kind/Env.md deleted file mode 100644 index 5b004938e..000000000 --- a/docs/src/Kind/Env.md +++ /dev/null @@ -1,42 +0,0 @@ ---- -title: Env -description: 'Module that defines the environment and related operations for the Kind system' ---- - -# Env - -This module defines the environment (`Env`) and various related operations for the Kind system. The environment is used to manage the state during term checking and compilation. - -## Main Structure - -- `Env`: Represents the execution environment. -- `State`: Contains the current state, including the book (`Book`), fillings (`Fill`), suspensions (`Susp`), and logs. - -## Main Functions - -### Environment Operations - -- `envBind`: Binds an environment to a function that produces another environment. -- `envPure`: Creates a pure environment with a value. -- `envFail`: Creates a failing environment. -- `envRun`: Runs an environment with a given book. - -### State Manipulation - -- `envLog`: Adds information to the log. -- `envSnapshot`: Captures the current state. -- `envRewind`: Returns to the previous state. -- `envSusp`: Adds a check to the list of suspensions. -- `envFill`: Inserts a term into the fillings map. - -### Accessors - -- `envGetFill`: Gets the current fillings map. -- `envGetBook`: Gets the current book. -- `envTakeSusp`: Gets and clears the list of suspensions. - -## Instances - -The module also provides instances of `Functor`, `Applicative`, and `Monad` for `Env`, allowing the use of monadic operations with the environment. - -This module is fundamental to the internal workings of the Kind system, managing the state and operations during the verification and compilation process. diff --git a/docs/src/Kind/Equal.md b/docs/src/Kind/Equal.md deleted file mode 100644 index c44e7ccd4..000000000 --- a/docs/src/Kind/Equal.md +++ /dev/null @@ -1,50 +0,0 @@ ---- -title: Equal -description: 'Module responsible for checking equality between terms and performing pattern unification' ---- - -# Equal - -The `Equal` module provides functionalities to check equality between terms and perform pattern unification in the context of a dependent type system. - -## Main Functions - -### equal - -Checks if two terms are equal after reduction steps. - -```haskell -equal :: Term -> Term -> Int -> Env Bool -``` - -### identical - -Checks if two terms are syntactically identical. - -```haskell -identical :: Term -> Term -> Int -> Env Bool -``` - -### similar - -Checks if two terms are equal component by component. - -```haskell -similar :: Term -> Term -> Int -> Env Bool -``` - -### unify - -Attempts to solve a pattern unification problem, generating a substitution if possible. - -```haskell -unify :: Int -> [Term] -> Term -> Int -> Env Bool -``` - -## Auxiliary Functions - -- `valid`: Checks if a problem is solvable by pattern unification. -- `solve`: Generates the solution for a unification problem, adding bindings and renaming variables. -- `occur`: Checks if a metavariable occurs recursively within a term. - -This module is fundamental for implementing type checking and inference in dependent type systems, providing the basic operations necessary to compare and unify terms. diff --git a/docs/src/Kind/Parse.md b/docs/src/Kind/Parse.md deleted file mode 100644 index 9aee3fb1c..000000000 --- a/docs/src/Kind/Parse.md +++ /dev/null @@ -1,47 +0,0 @@ ---- -title: Parse -description: 'Module responsible for the syntactic analysis of the Kind language' ---- - -# Parse - -The `Kind.Parse` module is responsible for the syntactic analysis of the Kind language. It defines the structures and functions necessary to convert the source code into an abstract representation that can be processed by the compiler. - -## Main structures - -- `Uses`: List of tuples representing name aliases. -- `PState`: Parser state, containing the file name and the list of Uses. -- `Parser`: Custom type for the parser, based on Parsec. - -## Main functions - -### Term parsing - -- `doParseTerm`: Parses a complete term from an input string. -- `parseTerm`: Main parser for Kind language terms. - -### Parsing uses and books - -- `doParseUses`: Parses the use declarations (aliases) at the beginning of the file. -- `doParseBook`: Parses a complete book, including uses and definitions. - -### Error handling - -- `showParseError`: Displays parsing errors in a user-friendly way, highlighting the error position. - -### Specific parsers - -The module includes parsers for various language constructs, such as: - -- `parseAll`: For universal quantifiers. -- `parseLam`: For lambda expressions. -- `parseApp`: For function applications. -- `parseAnn`: For type annotations. -- `parseDat`: For data type definitions. -- `parseCon`: For data type constructors. -- `parseSwi`: For switch expressions. -- `parseMat`: For pattern matching expressions. - -## Usage - -This module is used internally by the Kind compiler to transform the source code into a data structure that can be processed by subsequent compilation stages, such as type checking and code generation. diff --git a/docs/src/Kind/Reduce.md b/docs/src/Kind/Reduce.md deleted file mode 100644 index 80f883fe0..000000000 --- a/docs/src/Kind/Reduce.md +++ /dev/null @@ -1,70 +0,0 @@ ---- -title: Reduce -description: 'Module responsible for reduction and normalization of terms in Kind' ---- - -# Reduce - -This module implements the functionalities for reduction and normalization of terms in the Kind language. - -## Main Functions - -### reduce - -```haskell -reduce :: Book -> Fill -> Int -> Term -> Term -``` - -Evaluates a term to its weak normal form. The `lv` parameter defines when to expand references: -- 0 = never -- 1 = in redexes - -### normal - -```haskell -normal :: Book -> Fill -> Int -> Term -> Int -> Term -``` - -Evaluates a term to its complete normal form. - -### bind - -```haskell -bind :: Term -> [(String,Term)] -> Term -``` - -Binds quoted variables to bound HOAS variables. - -### genMetas - -```haskell -genMetas :: Term -> Term -``` - -Generates metavariables for a term. - -### subst - -```haskell -subst :: Int -> Term -> Term -> Term -``` - -Substitutes a Bruijn level variable with a new value in a term. - -## Data Structures - -The module uses the following main structures: - -- `Term`: Represents terms in the Kind language -- `Book`: Map of definitions -- `Fill`: Map of fillings for metavariables - -## Implementation Details - -- The `reduce` function implements the lazy reduction strategy, evaluating only when necessary. -- `normal` performs a complete normalization, including subterms. -- `bind` is used to bind variables in lambda abstractions and universal quantifiers. -- `genMetas` is used to generate unique metavariables in a term. -- `subst` implements variable substitution, respecting the term structure. - -This module is fundamental for the type system and evaluation of the Kind language, providing the basic reduction and normalization operations necessary for term processing. diff --git a/docs/src/Kind/Show.md b/docs/src/Kind/Show.md deleted file mode 100644 index 6e424fed6..000000000 --- a/docs/src/Kind/Show.md +++ /dev/null @@ -1,53 +0,0 @@ ---- -title: Show -description: 'Module responsible for displaying and formatting terms and information in the Kind compiler' ---- - -# Show - -The `Kind.Show` module is responsible for providing functions to display and format terms, contexts, and information in the Kind compiler. It defines various helper functions to convert internal data structures into readable string representations. - -## Main Functions - -### termShower - -```haskell -termShower :: Bool -> Term -> Int -> String -``` - -This function is the core of term display. It takes a boolean to control the level of detail, a term, and a depth, and returns a string representation of the term. - -### contextShow - -```haskell -contextShow :: Book -> Fill -> [Term] -> Int -> String -``` - -Displays a context (list of terms) with annotations. - -### infoShow - -```haskell -infoShow :: Book -> Fill -> Info -> IO String -``` - -Formats different types of information (such as goals, errors, solutions) for display. - -## Helper Functions - -- `unwrapApp`: Unpacks nested function applications. -- `termShow`: Simplified version of `termShower`. -- `operShow`: Converts operators to their string representations. -- `teleShower`: Displays telescopes (data structures for dependent parameters). - -## Error Handling - -The module includes functions for reading source files and resolving absolute paths, which are used to display error information with source code context. - -## Notes - -- The module makes extensive use of string concatenation to build representations. -- It uses ANSI codes to color the output in the terminal. -- Integrates with a syntax highlighting module (`Highlight`) to improve error display. - -This module is crucial for providing readable and useful feedback during compilation and type checking in the Kind compiler. diff --git a/docs/src/Kind/Type.md b/docs/src/Kind/Type.md deleted file mode 100644 index 5d89b5730..000000000 --- a/docs/src/Kind/Type.md +++ /dev/null @@ -1,55 +0,0 @@ ---- -title: Type -description: 'Type definitions and data structures for the Kind compiler' ---- - -# Type - -This module defines the fundamental data structures used in the Kind compiler. - -## Main Structures - -### Term - -Represents the abstract syntax tree (AST) of Kind. Includes constructions such as: - -- `All`: Dependent product (∀) -- `Lam`: Lambda abstraction -- `App`: Function application -- `Ann`: Type annotation -- `Slf`: Recursive type -- `Ins`: Recursive type instantiation -- `Dat`: Data type definition -- `Con`: Data constructor -- `Mat`: Pattern matching -- `Ref`: Top-level reference -- `Let`: Local definition -- `Use`: Use of local definition -- `Set`: Type of types -- `U32`: 32-bit integer type -- `Num`: Integer value -- `Op2`: Binary operation -- `Swi`: U32 elimination -- `Hol`: Inspection hole -- `Met`: Unification metavariable -- `Var`: Variable -- `Src`: Source code location -- `Txt`: Text literal -- `Nat`: Natural literal - -### Other Structures - -- `Loc`: Source code location (name, line, column) -- `Cod`: Code range -- `Oper`: Numeric operators -- `Tele`: Telescope (sequence of typed arguments) -- `Ctr`: Data type constructor -- `Book`: Map of definitions -- `Info`: Type checker outputs -- `Fill`: Unification solutions -- `Check`: Type checker state -- `State`: Global compiler state -- `Res`: Checking result -- `Env`: Type checker monadic environment - -This module provides the essential data structures for representing and manipulating Kind programs during the compilation process. From 769ae06e6fe18895a5e7c36872ff73e7886652d7 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:28:51 -0300 Subject: [PATCH 07/15] Delete docs/app/Main.md --- docs/app/Main.md | 27 --------------------------- 1 file changed, 27 deletions(-) delete mode 100644 docs/app/Main.md diff --git a/docs/app/Main.md b/docs/app/Main.md deleted file mode 100644 index fbc1da09e..000000000 --- a/docs/app/Main.md +++ /dev/null @@ -1,27 +0,0 @@ ---- -title: Main -description: 'Main module that initiates the execution of the Kind compiler' ---- - -# Main - -This module is the entry point for the Kind compiler. It imports and executes the `main` function from the `Kind` module. - -## Structure - -The `Main` module consists of: - -1. A module declaration -2. An import of the `Kind` module -3. A definition of the `main` function - -## Main function - -```haskell -main :: IO () -main = Kind.main -``` - -The `main` function is defined with the type `IO ()`, indicating that it performs input/output operations. It simply calls the `main` function from the `Kind` module, delegating all the compiler's execution logic to that module. - -This structure allows for a clear separation between the program's entry point and the main logic of the compiler, which is contained in the `Kind` module. From cbee50aed9fa930c3ff10a9c17a9fe4626d7e84c Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:28:59 -0300 Subject: [PATCH 08/15] Delete docs/CHANGELOG.md --- docs/CHANGELOG.md | 16 ---------------- 1 file changed, 16 deletions(-) delete mode 100644 docs/CHANGELOG.md diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md deleted file mode 100644 index d62889e1c..000000000 --- a/docs/CHANGELOG.md +++ /dev/null @@ -1,16 +0,0 @@ ---- -title: CHANGELOG -description: 'Revision history for the kind2hs project' ---- - -# Revision History - -This document records the changes and updates made to the kind2hs project over time. - -## 0.1.0.0 - -- Release date: YYYY-mm-dd -- First version of the project -- Initial public release - -Note: The specific release date has not been defined yet and is represented as YYYY-mm-dd in the record. From 6f1374d23101aceef0c1cea16d487e67cd4dbf49 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:29:13 -0300 Subject: [PATCH 09/15] Delete docs/app.md --- docs/app.md | 28 ---------------------------- 1 file changed, 28 deletions(-) delete mode 100644 docs/app.md diff --git a/docs/app.md b/docs/app.md deleted file mode 100644 index 295f9d3f5..000000000 --- a/docs/app.md +++ /dev/null @@ -1,28 +0,0 @@ ---- -title: App -description: 'Directory containing the entry point of the Kind application' ---- - -# App - -The `app` directory is an essential part of the Kind project structure. It contains the main entry point of the application, typically a `Main.hs` file. - -## Structure - -The `app` directory usually includes: - -- `Main.hs`: The main file containing the `main` function, which is the entry point of the Kind application. - -## Purpose - -The purpose of the `app` directory is to: - -1. Separate the main application code from the library code. -2. Contain the initialization and configuration logic of the application. -3. Provide a clear entry point for program execution. - -## Usage - -The code in the `app` directory typically imports and utilizes the functionalities defined in the `src` directory, combining them to create the complete application. - -For more details on the specific content and implementation, refer to the `Main.hs` file within this directory. From 4fb6633f1effb4627d3323d6461453b5444ac351 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:29:21 -0300 Subject: [PATCH 10/15] Delete docs/cabal.md --- docs/cabal.md | 28 ---------------------------- 1 file changed, 28 deletions(-) delete mode 100644 docs/cabal.md diff --git a/docs/cabal.md b/docs/cabal.md deleted file mode 100644 index e52b63de1..000000000 --- a/docs/cabal.md +++ /dev/null @@ -1,28 +0,0 @@ ---- -title: cabal.project -description: 'Cabal project configuration for the Kind compiler' ---- - -# cabal.project - -This file contains the Cabal project configuration for the Kind compiler. - -## Content - -``` -packages: . - --- Enable -O2 optimization for all packages -package * - optimization: 2 -``` - -## Details - -1. `packages: .`: Indicates that the package is located in the current directory. - -2. `package *`: This line starts a configuration section that applies to all packages. - -3. `optimization: 2`: Sets the optimization level to 2 (equivalent to -O2) for all packages. This instructs the compiler to perform more aggressive optimizations during compilation, potentially improving the performance of the generated code. - -This configuration ensures that all packages in the project are compiled with level 2 optimizations, which can result in more efficient code, although it may increase compilation time. From 24fb1cdb982fec094b47b52224f936ccc74a28f5 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:29:35 -0300 Subject: [PATCH 11/15] Delete docs/introduction.md --- docs/introduction.md | 43 ------------------------------------------- 1 file changed, 43 deletions(-) delete mode 100644 docs/introduction.md diff --git a/docs/introduction.md b/docs/introduction.md deleted file mode 100644 index adf5c0a57..000000000 --- a/docs/introduction.md +++ /dev/null @@ -1,43 +0,0 @@ ---- -title: Introduction to Kind-Core -description: 'A guide to get started with Kind, a minimalist proof checker' ---- - -# Introduction to Kind-Core - -Kind-Core is a minimalist proof checker. This project provides a powerful tool for verifying and executing terms in a dependent type system. - -## Overview - -Kind-Core is designed to be a lean and efficient implementation of a proof checker. It supports a rich grammar that allows the expression of complex concepts in type theory, including universal quantification, lambda abstraction, function application, type annotations, recursive types, and much more. - -## About the Project - -The project is structured into several main parts: - -- `src/Kind`: Contains the main modules of the proof checker. -- `app`: Contains the application entry point. -- `cabal.project` and `kind-lang.cabal`: Haskell project configuration files. - -## How to Run - -To start using Kind-Core: - -1. Clone this repository. -2. Install the project following the Haskell setup instructions. -3. Use the `kind` command to verify or execute terms. - -## Requirements - -- GHC (Glasgow Haskell Compiler) -- Cabal or Stack for Haskell package management - -## Examples - -Examples of Kind usage can be found in the [MonoBook](https://github.com/HigherOrderCO/MonoBook) repository. Look for files with the `.kind` extension. - -## Grammar - -Kind-Core uses a specific grammar to define terms. The complete grammar can be found in the project's README, including constructions for universal quantifiers, lambda abstractions, applications, type annotations, recursive types, data constructors, and more. - -For more details on the grammar and advanced usage, refer to the project's full documentation. From 55fa0fdfc1c740e11d4541849c608cbc88c4cff5 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:29:45 -0300 Subject: [PATCH 12/15] Delete docs/kind-lang.md --- docs/kind-lang.md | 56 ----------------------------------------------- 1 file changed, 56 deletions(-) delete mode 100644 docs/kind-lang.md diff --git a/docs/kind-lang.md b/docs/kind-lang.md deleted file mode 100644 index 826d9c8c6..000000000 --- a/docs/kind-lang.md +++ /dev/null @@ -1,56 +0,0 @@ ---- -title: kind-lang.cabal -description: 'Cabal configuration file for the kind-lang project' ---- - -# kind-lang.cabal - -This file is the Cabal configuration file for the kind-lang project. It defines the package specifications, dependencies, and project structure. - -## Package Details - -- **Name**: kind-lang -- **Version**: 0.1.0.0 -- **License**: MIT -- **Author**: Victor Taelin -- **Maintainer**: victor.taelin@gmail.com -- **Category**: Language - -## Library - -The library exposes the following modules: - -- Kind -- Kind.API -- Kind.Check -- Kind.Compile -- Kind.Env -- Kind.Equal -- Kind.Parse -- Kind.Reduce -- Kind.Show -- Kind.Type - -Main dependencies: - -- base ^>=4.20.0.0 -- containers ==0.7 -- parsec ==3.1.17.0 -- ansi-terminal==1.1.1 -- directory==1.3.8.3 -- hs-highlight == 1.0.3 -- filepath==1.5.2.0 - -## Executable - -The project also defines an executable called "kind" with the following characteristics: - -- **Main file**: Main.hs -- **Dependencies**: Includes the kind-lang library itself and other dependencies shared with the library. - -## Common Settings - -- The project uses GHC2024 as the default language. -- Warnings are enabled for both the library and executable. - -This Cabal file provides a clear overview of the kind-lang project's structure and dependencies, facilitating its compilation and distribution. From 8fb1638991d2eb65c4d27e5039edd13a3795a0c6 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:29:59 -0300 Subject: [PATCH 13/15] Delete docs/src.md --- docs/src.md | 26 -------------------------- 1 file changed, 26 deletions(-) delete mode 100644 docs/src.md diff --git a/docs/src.md b/docs/src.md deleted file mode 100644 index 203a2ae47..000000000 --- a/docs/src.md +++ /dev/null @@ -1,26 +0,0 @@ ---- -title: src -description: 'Main directory containing the source code of the Kind project' ---- - -# src - -This directory contains the main source code of the Kind project. Here you will find the essential modules that make up the core of the Kind language and compiler. - -## Structure - -The `src` directory is organized as follows: - -- `Kind.hs`: Main module that likely exports the core functionalities of the Kind language. -- `Kind/`: Subdirectory containing specific modules: - - `API.hs`: Application programming interface. - - `Check.hs`: Type checker implementation. - - `Compile.hs`: Compilation logic. - - `Env.hs`: Environment management. - - `Equal.hs`: Equality implementation. - - `Parse.hs`: Syntactic analyzer. - - `Reduce.hs`: Reduction mechanism. - - `Show.hs`: Display and formatting functions. - - `Type.hs`: Type definitions. - -Each of these files plays a crucial role in the functioning of the Kind compiler and language. To fully understand the project, it is recommended to examine each of these modules individually. From 4eaeff104b9ad9388145fed6718f842b05092c68 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 15:32:20 -0300 Subject: [PATCH 14/15] Update and rename docs/main.md to example.md --- docs/main.md => example.md | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) rename docs/main.md => example.md (87%) diff --git a/docs/main.md b/example.md similarity index 87% rename from docs/main.md rename to example.md index 4b9e41d93..ab1f119ad 100644 --- a/docs/main.md +++ b/example.md @@ -1,7 +1,3 @@ ---- -title: main.kindc -description: 'Type and function definitions in Kind, including Bool, Nat, IsTrue, Equal and rewrite' ---- # main.kindc @@ -13,7 +9,7 @@ This file contains fundamental type and function definitions in Kind, a function Defines the boolean type with two constructors: -```kind +```hs Bool : * = #[]{ #true{} : Bool #false{} : Bool @@ -24,7 +20,7 @@ Bool : * = #[]{ Defines the natural numbers type with two constructors: -```kind +```hs Nat : * = #[]{ #zero{} : Nat #succ{ pred: Nat } : Nat @@ -37,7 +33,7 @@ Nat : * = #[]{ A predicate that checks if a boolean is true: -```kind +```hs IsTrue : ∀(b: Bool) * = λb #[b]{ #indeed{} : (IsTrue #true{}) }; @@ -47,7 +43,7 @@ IsTrue : ∀(b: Bool) * = λb #[b]{ Defines propositional equality between two values of the same type: -```kind +```hs Equal : ∀(T: *) ∀(a: T) ∀(b: T) * = λT λa λb #[a b]{ #refl{} : (Equal T a a) }; @@ -59,7 +55,7 @@ Equal : ∀(T: *) ∀(a: T) ∀(b: T) * = λT λa λb #[a b]{ A function that allows rewriting an equality proof: -```kind +```hs rewrite : ∀(T: *) ∀(a: T) @@ -77,7 +73,7 @@ rewrite The program's entry point is defined as: -```kind +```hs MAIN = rewrite; ``` From e07ba00264cd1b39e2ef1a7eb78c3c17faf86e93 Mon Sep 17 00:00:00 2001 From: Sergio Bonatto <52257001+SergioBonatto@users.noreply.github.com> Date: Tue, 1 Oct 2024 16:06:12 -0300 Subject: [PATCH 15/15] add: Prerequisites --- README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/README.md b/README.md index 0eaf41a41..1dc56a700 100644 --- a/README.md +++ b/README.md @@ -100,3 +100,14 @@ The grammar of Kind is defined as follows: This grammar defines the syntactic structure of the Kind language, including terms, constructors, operators, and other fundamental elements. + +### Prerequisites + +Before installing Kind, ensure that you have GHC (Glasgow Haskell Compiler) version 9.10.1 installed on your system. You can check your GHC version by running: + +``` +ghc --version +``` + +If you don't have GHC 9.10.1 installed, please visit the official Haskell website (https://www.haskell.org/ghc/) for installation instructions specific to your operating system. +