Cogent Reference Manual

This part of the manual is not intended as a tutorial for programming in Cogent, or to introduce proving properties of Cogent programs. The examples are not chosen to be realistic; they are only used for illustrating the syntax. Much of the manual describes the Cogent “surface syntax”, which is the interface for the programmer; most formal publications about Cogent refer to the more concise “core syntax”, which is created from the surface syntax by applying the “desugaring rules”.

• Surface Syntax
  • Lexical Syntax
    • Comments
    • Identifiers
    • Literals
      • Boolean Literals
      • Integer Literals
      • Character Literals
      • String Literals
• Core Syntax
• Types
  • Type Basics
    • Primitive Types
      • Bitstring Types
      • Other Primitive Types
    • Composite Types
      • Tuple Types
      • Record Types
      • Variant Types
      • Function Types
    • Type Definitions
      • Generic Types
      • Expanding Type Expressions
      • Abstract Types
  • Restricted Types
    • Linear Types
    • Boxed and Unboxed Types
    • Partial Record Types
    • Readonly Types
      • The bang Operator
      • Escape-restricted Types
• Working with Values
  • Patterns
    • Simple Patterns
      • Irrefutable Simple Patterns
      • Refutable Simple Patterns
    • Composite Patterns
      • Tuple Patterns
      • Record Patterns
      • Variant Patterns
  • Expressions
    • Terms
      • Literal Terms
      • Terms for Tuple Values
      • Terms for Record Values
      • Terms for Values of Variant Types
      • Terms for Values of Function Types
    • Basic Expressions
      • Plain Function Application
      • Operator Application
      • Put Expressions
      • Member Access
    • General Expressions
      • Matching Expressions
      • Binding Variables
      • Conditional Expressions
      • Observing Variables
  • Expression Usage Rules
    • Using Values of Linear Types
      • Sharing a Value
      • Discarding a Value
      • The Result of Using a Value
    • Using Values of Readonly Types
      • Modifying a Value
      • Creating readonly Values
      • Preventing Values from Escaping
• Programs
  • Including Files
  • Toplevel Definitions
    • Value Definitions
    • Function Definitions
    • Abstract Definitions
    • Polymorphic Definitions
• Antiquoted C
  • Antiquotes
    • $id: Introducing Identifiers
    • $ty: Talking Types
    • $exp: Embedding Expressions
    • $spec: Specifying Casts
    • $esc and $escstm: No Escape In Sight
• Antiquoted C
  • Cheatsheet
  • Overview
  • Modes in the compiler
  • Function definitions
  • Type declarations / Typedef’s
  • Escape sequences
  • Expressions
• Using the Cogent Compiler
  • Commands
  • All Flags
• Installation Guide
  • In a Nutshell
  • Detailed Instructions
    • Dependencies
    • Install Cogent dependencies
      • The GHC compiler and Cabal
      • alex and happy
      • z3 SMT-solver
    • Install Cogent
      • Optional features
      • Build with Makefile (simple, but can be fragile)
      • Build with Cabal (more advanced)
      • Build with Stack (simple, more robust)
    • Test your installation
      • Testing on macOS
  • Common Issues and Troubleshooting
    • Cabal Version
    • Missing Dependencies
    • Could not resolve dependency isa-parser
• Verification
  • Dependencies
  • Generated Theory Files
  • Building/Running The Generated Files
    • In Jedit
    • On the command line
  • Examples
    • A Simple Example
    • A More Involved Example
  • Common Errors
    • ACInstall