{-# OPTIONS --safe --experimental-lossy-unification #-}

module README where

-- This file contains an index for the code snippets referenced in the paper,
-- pointing to their definitions in the agda formalisation.
-- You can read it alongside the paper, and click on the relevant defs to
-- get to the code for each.

--==============================================================================
-- Section 1: Introduction
--==============================================================================

-- Hoare logic

import Hoare.Definition
  using
  ( hoare-def-explicit -- Encoding displayed in paper
  ; Hoare              -- Actual encoding, equivalent
  ; module DisplayGlobal
  )
 
-- The signature of nondeterminism

import Effects.NonDet
  using
  ( NonDet
  ; ℕ𝔻
  )

-- The signature of state

import Effects.State
  using
  ( module StateFunctor -- In the paper, the S is an argument to Op; here, it is
                        -- paramaterised over the whole module.
  ; 𝕊
  )

-- Associativity of <|>

import Effects.NonDet
  using
  ( module AssocLaw
  )

-- put-put law

import Effects.State
  using
  ( module PutPutLawDisplay
  )

-- Finiteness condition

import Finite
  using
  ( ℰ
  )

-- Parsing equality

import Effects.Parser.HElim
  using
  ( push-print-parse
  )

-- Parsing Hoare triple

import Effects.Parser.TreeParser
  using
  ( round-trip
  )

-- Tree Parsing, Fig. 2

import Effects.Parser
  using
  ( any-char
  ; char
  )

import Data.Tree
  using
  ( Tree
  )

import Effects.Parser.TreeParser
  using
  ( parse-tree
  )

--==============================================================================
-- Section 2: Algebraic Signatures and Algebras
--==============================================================================

--------------------------------------------------------------------------------
-- 2.1 Algebraic Signatures
--------------------------------------------------------------------------------

-- Signature

import Signatures
  using
  ( Signature
  )

-- Fin

import Data.Fin
  using
  ( module DisplayDef
  )

--------------------------------------------------------------------------------
-- 2.2 Algebras of Signatures
--------------------------------------------------------------------------------

-- Interpreting a Signatures

import Signatures
  using
  ( ⟦_⟧
  )

-- F-alg

import Signatures
  using
  ( _-Alg[_]
  )

-- Interpretations for nondeterminism

import Effects.NonDet
  using
  ( list-int
  ; all-int
  ; any-int
  )

-- Interpretation for State

import Effects.State
  using
  ( state-alg
  )

--------------------------------------------------------------------------------
-- 2.3 Term Algebras
--------------------------------------------------------------------------------

-- Syntax type

import FreeMonad.Syntax
  using
  ( Syntax
  )

-- Odds example

import Effects.NonDet
  using
  ( module OddsExample
  ; module Synt
  )

open Effects.NonDet.OddsExample
  using
  ( guard
  ; up-to
  ; odds
  )

open Effects.NonDet.Synt
  using
  ( _<|>_
  ; fail
  ; module BindParameterised
  )

open BindParameterised
  using
  ( return
  ; _>>=_
  )

--------------------------------------------------------------------------------
-- 2.4 Interpreting the Syntax Tree
--------------------------------------------------------------------------------

-- interp function

import FreeMonad.Syntax
  using
  ( interp
  ; module SyntaxBind
  )

-- >>= using interp

open FreeMonad.Syntax.SyntaxBind
  using
  ( _>>=_
  )

-- syntax-alg

import FreeMonad.Syntax
  using
  ( syntax-alg
  )

-- interp-id

import FreeMonad.Syntax
  using
  ( interp-id
  )

-- interp comp

import FreeMonad.Syntax
  using
  ( interp-comp
  )

--------------------------------------------------------------------------------
-- 2.5 Freeness of Syntax
--------------------------------------------------------------------------------

-- Homomorphisms

import Signatures
  using
  ( _⟶_
  ; cmap
  )


-- Theorem 2.1: Syntax is free

import FreeMonad.Syntax
  using
  ( syntax-is-free
  )

--==============================================================================
-- Section 3: Algebraic Theories and Models
--==============================================================================

--------------------------------------------------------------------------------
-- Equations
--------------------------------------------------------------------------------

import FreeMonad.Theory
  using 
  ( Equation
  )

open Effects.NonDet.AssocLaw
  using
  ( module Literals
  )

-- Assoc law

open Literals
  using
  ( assoc
  )

-- Assoc law with syntactic sugar

open Effects.NonDet.AssocLaw
  using
  ( assoc
  )

--------------------------------------------------------------------------------
-- Contexts
--------------------------------------------------------------------------------

-- Law

import FreeMonad.Theory
  using
  ( Law
  )

-- Put-put law
import Effects.State
  using
  ( module PutPutLawDisplay
  )

--------------------------------------------------------------------------------
-- Theories
--------------------------------------------------------------------------------

import FreeMonad.Theory
  using
  ( Theory
  )

-- State laws

import Effects.State
  using
  ( module Synt
  )

open Effects.State.Synt
  using
  ( Laws
  ; Eqns
  )

--------------------------------------------------------------------------------
-- Models
--------------------------------------------------------------------------------

-- Respects, models

import FreeMonad.Theory
  using
  ( _Respects_
  ; _Models_
  ; _-Model[_]
  )

--==============================================================================
-- Section 4: Free Models of Algebraic Theories
--==============================================================================

--------------------------------------------------------------------------------
-- 4.1 Quotient Types
--------------------------------------------------------------------------------

-- Set quotient

import Examples.Quotients
  using
  ( [_]
  ; isSet
  ; isProp
  ; rec/
  )

-- Bag example

import Examples.Bag
  using
  ( _↺_
  ; size
  )

--------------------------------------------------------------------------------
-- 4.2 Program Equivalence
--------------------------------------------------------------------------------

import FreeMonad.Relation
  using
  ( _~ₜ_
  )

--------------------------------------------------------------------------------
-- 4.3 Terms up to Program Equivalence
--------------------------------------------------------------------------------

-- Term type

import FreeMonad.Quotiented
  using
  ( Term
  ; [_]ₜ
  )

-- interpₜ

import FreeMonad.Quotiented
  using
  ( interpₜ
  )

-- Lemma 4.1: interpₜ-cong

import FreeMonad.Quotiented
  using
  ( interpₜ-cong
  )

--------------------------------------------------------------------------------
-- 4.4 Term Models
--------------------------------------------------------------------------------

-- opₜ

import FreeMonad.Quotiented
  using
  ( opₜ
  )

-- Quotient Preserving

import FinitenessConditions
  using
  ( dist
  ; Pointwise
  ; quot-pre
  )

-- Bind on Term

import FreeMonad.Quotiented
  using
  ( _>>=_
  )

-- Theorem 4.3: Term is free

import FreeMonad.IsFree
  using
  ( ⟦f⟧-hom
  ; uniq
  )

-- Corollary 4.4: Birkhoff's completeness theorem

import FreeMonad.IsFree
  using
  ( ≈⇒∼
  )

--==============================================================================
-- Section 5: Programming with Effects
--==============================================================================

-- print

import Effects.Parser.TreeParser
  using
  ( print
  )

--------------------------------------------------------------------------------
-- Combining Signatures
--------------------------------------------------------------------------------

import Signatures
  using
  ( _⊞_
  )

-- Operations on parser

import Effects.Parser
  using
  ( module SyntaxExamples
  )

open Effects.Parser.SyntaxExamples
  using
  ( fail
  ; put
  ; get
  ; eof
  ; any-char
  ; char
  )

import Effects.Parser
  using
  ( put
  ; _<|>_
  )

--------------------------------------------------------------------------------
-- Combining Laws
--------------------------------------------------------------------------------

-- NonDet Laws

open Effects.NonDet.Synt
  using
  ( Eqns
  )

-- <|>-assoc

import Effects.NonDet
  using
  ( <|>-assoc
  )

-- Commutativity Law

import FreeMonad.Combinations.LiftLess.Tensor
  using
  ( commutative
  )

-- Op constructor

import FreeMonad.Syntax
  using
  ( Op⟦_⟧
  )

--------------------------------------------------------------------------------
-- Interpreting into Models
--------------------------------------------------------------------------------

-- toState, runState

import Effects.State
  using
  ( toState
  ; runState
  )

-- State Transformer Iso

import Effects.State.Tensor
  using
  ( stateT-iso
  )

--==============================================================================
-- Section 6: An Effect-Generic Hoare Logic
--==============================================================================

--------------------------------------------------------------------------------
-- Truth Values
--------------------------------------------------------------------------------

-- Ω

import Truth
  using
  ( Ω
  ; module LevelZero
  )

-- 3 is even

open Truth.LevelZero
  using
  ( 3-is-even
  ; 3-is-not-even
  ; 1≢0
  )

-- Truth Combinators

import Truth
  using
  ( _iff_
  ; False
  ; True
  ; _|∧|_
  ; _|→|_
  ; _|∨|_
  )

-- Propositional Truncation

import Examples.Quotients
  using
  ( ∥_∥
  )

-- Truth Equality

import Truth
  using
  ( _|≡|_
  )

--------------------------------------------------------------------------------
-- Assertions
--------------------------------------------------------------------------------

-- no-input encodings

import Effects.Parser
  using
  ( module NoInpAssertion
  ; module NoInpG
  )

open Hoare.Definition.DisplayGlobal
  using
  ( 𝒢
  )

--------------------------------------------------------------------------------
-- Pure Assertions
--------------------------------------------------------------------------------

import Hoare.Definition
  using
  ( SEF
  ; DET
  )

--------------------------------------------------------------------------------
-- Hoare Triples
--------------------------------------------------------------------------------

import Hoare.Definition
  using
  ( hoare-def-explicit -- Encoding displayed in paper
  ; Hoare              -- Actual encoding, equivalent
  )

-- Remaining and no-input

import Effects.Parser
  using
  ( remaining
  ; no-input
  )

--------------------------------------------------------------------------------
-- Connectives on Assertions
--------------------------------------------------------------------------------

import Hoare.Calculus
  using
  ( conj
  )

--------------------------------------------------------------------------------
-- Using Hoare Logic
--------------------------------------------------------------------------------

-- Hoare valued predicate on parser

import Effects.Parser
  using
  ( _∈_↦_
  )

-- round-trip

import Effects.Parser.TreeParser
  using
  ( round-trip
  )

-- lemmas used to prove

import Effects.Parser
  using
  ( fail-anything
  ; _⟨<|>⟩_
  ; parse-char
  )

-- Using H-Elim on the Parser

import Effects.Parser.HElim
  using
  ( Total
  ; parse-equality
  ; push-print-parse
  )

--==============================================================================
-- Section 7: Relating Hoare-Style and Equational Reasoning
--==============================================================================

import Hoare.Definition
  using
  ( hoare-def-explicit
  )

-- Theorem 7.1 (H-Elim)

import Hoare.HElim
  using
  ( H-elim
  )

-- Classical proof of H-elim

import Hoare.Boolean
  using
  ( ℋ-elim
  )

-- Provenance

import FreeMonad.HElim
  using
  ( Provenance
  )

-- Lemma 7.2

import FreeMonad.HElim
  using
  ( derive
  )

-- Pushouts

import Examples.Pushout
   using
   ( Pushout
   )

-- Lemma 7.3

import HITs.Pushout.Properties
  using
  ( fin-disc-pushout
  ; _≈*_
  ; Loopless
  ; deloop
  )

-- Proof Sketch

import FreeMonad.HElim
  using
  ( 𝒢-elim
  )