\begin{code}
{-# OPTIONS --safe --experimental-lossy-unification #-}

open import Prelude renaming (tt to ⟨⟩)
open import Signatures
open import FinitenessConditions
open import FreeMonad.PackagedTheory

-- This could all be redefined to work over a generic monad (instead of Term),
-- but unfortunately that takes extremely long to typecheck. I'm going to
-- proceed with this slightly specialised version, and maybe switch out the
-- definitions later.
--
-- Also: the universe polymorphism here is making things crazy slow. If
-- you miss a single application it can blow up the typechecking time to several
-- hours (rather then ~10 seconds). I plan to remove it in some principled way
-- (i.e. replace all the levels with one)

module Hoare.Definition {β„“} (𝒯 : FullTheory β„“) where

open import FreeMonad.Quotiented 𝒯

open import Truth hiding (Ξ©; True)

[_/⟨⟩] : Term A β†’ Term ⊀
[_/⟨⟩] = _>> return ⟨⟩

module DisplayConditions where
  module _ {A : Type a} where
    SEF : Term A β†’ Type _
    DET : Term A β†’ Type _
\end{code}
%<*sef-dsef>
\begin{code}[number=sef-dsef]
    SEF t = (do t; return ⟨⟩) ≑ return ⟨⟩
    DET t = (do x ← t; y ← t; return (x , y)) ≑ (do x ← t; t; return (x , x))
\end{code}
%</sef-dsef>
\begin{code}


module _ (p : Level) where
  module _ {A : Type a} where
    SEF : Term A β†’ Type _
    SEF t = βˆ€ {R : Type p} (k : Term R) β†’ (do t ; k) ≑ k

    DET : Term A β†’ Type _
    DET t = βˆ€ {R : Type p} (k : A β†’ A β†’ Term R) β†’ (do x ← t ; y ← t ; k x y) ≑ (do x ← t ; t ; k x x)


module _ (p : Level) where
  open import Truth.MonoLevel p

  Assertion : Type (β„“ β„“βŠ” β„“suc (β„“suc p))
  Assertion = Ξ£[ Ο• ⦂ Term Ξ© ] Γ— SEF (β„“suc p) Ο• Γ— DET (β„“suc p) Ο•

module _ {p : Level} where
  open import Truth.MonoLevel p
  module DisplayGlobal {a} {A : Type a} where
    open import Truth.MonoLevel (β„“ β„“βŠ” β„“suc p β„“βŠ” a) using () renaming (Ξ© to Ω₁)
    open import Truth.MonoLevel using () renaming (Ξ© to Ξ©β€²)
\end{code}
%<*global>
\begin{code}
    𝒒 : Term (A Γ— Ξ©) β†’ Type _
    𝒒 t = t ≑ (do x , _ ← t; return (x , True))
\end{code}
%</global>
\begin{code}
    𝒒-Ξ© : Term (A Γ— Ξ©) β†’ Ω₁
    ProofOf  (𝒒-Ξ© t) = 𝒒 t
    IsProp   (𝒒-Ξ© t) = squash/ _ _

    Hoare : Term Ξ© β†’ Term A β†’ (A β†’ Term Ξ©) β†’ Type _
\end{code}
%<*hoare-def>
\begin{code}
    Hoare Ο• t ψ = 𝒒 do p ← Ο•; x ← t; q ← ψ x; return (x , p |β†’| q)
\end{code}
%</hoare-def>

\begin{code}
    hoare-def-explicit : Term Ξ© β†’ Term A β†’ (A β†’ Term Ξ©) β†’ Type _
    hoare-def-explicit = Ξ» Ο• t ψ β†’
\end{code}
%<*hoare-def-explicit-unnumbered>
\begin{code}
         (do p ← Ο•; x ← t; q ← ψ x; return (x , p |β†’| q))
      ≑  (do p ← Ο•; x ← t; q ← ψ x; return (x , True))
\end{code}
%</hoare-def-explicit-unnumbered>
\begin{code}
    _ : Term Ξ© β†’ Term A β†’ (A β†’ Term Ξ©) β†’ Type _
    _ = Ξ» Ο• t ψ β†’
\end{code}
%<*hoare-def-explicit>
\begin{code}[number=hoare-eq]
         (do p ← Ο•; x ← t; q ← ψ x; return (x , p |β†’| q))
      ≑  (do p ← Ο•; x ← t; q ← ψ x; return (x , True))
\end{code}
%</hoare-def-explicit>

\begin{code}
    HoareNoAssume : Term A β†’ (A β†’ Term Ξ©) β†’ Type _
    HoareNoAssume t ψ = Hoare (return True) t ψ

    syntax Hoare Ο• p (Ξ» x β†’ ψ) = βŸ… Ο• βŸ† x ← p βŸ… ψ βŸ†

    syntax HoareNoAssume p (Ξ» x β†’ ψ) = βŸ…βŸ† x ← p βŸ… ψ βŸ†

  open DisplayGlobal using (hoare-def-explicit) public

-- We need to keep the variables in the expression. This is a difference from
-- HasCasl.

-- However, we won't use this much type elsewhere, since we often also need the
-- variables in the expression as well.
-- Instead, we'll specialise it to each use case, like the following:

open Truth

module _ {A : Type a} {b c : Level} where
  record Hoare (Ο• : Term (Ξ© b)) (t : Term A) (ψ : A β†’ Term (Ξ© c)) : Type (β„“ β„“βŠ” β„“suc (a β„“βŠ” β„“suc (b β„“βŠ” c))) where
    no-eta-equality
    field
      proof : βˆ€ {R : Type (a β„“βŠ” β„“suc (b β„“βŠ” c))} β†’ (k : A β†’ Ξ© (b β„“βŠ” c) β†’ Term R) β†’
        (do a ← Ο•
            x ← t
            b ← ψ x
            k x (a |β†’| b)) ≑

        (do a ← Ο•
            x ← t
            b ← ψ x
            k x True)

    on-pair : 
        (do a ← Ο•
            x ← t
            b ← ψ x
            return (x , a |β†’| b)) ≑
        (do a ← Ο•
            x ← t
            b ← ψ x
            return (x , True))
    on-pair = proof Ξ» x p β†’ return (x , p)
  open Hoare public

  syntax Hoare Ο• p (Ξ» x β†’ ψ) = βŸ… Ο• βŸ† x ← p βŸ… ψ βŸ†

Hoare-NoVar : Term (Ξ© b) β†’ Term A β†’ Term (Ξ© c) β†’ Type _
Hoare-NoVar Ο• p ψ = Hoare Ο• p (const ψ)

syntax Hoare-NoVar Ο• p ψ = βŸ… Ο• βŸ† p βŸ… ψ βŸ†

Hoare-NoAssume : {A : Type a} β†’ Term A β†’ (A β†’ Term (Ξ© b)) β†’ Type _
Hoare-NoAssume p ψ = Hoare (return (True {β„“zero})) p ψ

syntax Hoare-NoAssume p (Ξ» x β†’ ψ) = βŸ…βŸ† x ← p βŸ… ψ βŸ†

Hoare-NoAssumeNoVar : Term ⊀ β†’ Term (Ξ© b) β†’ Type _
Hoare-NoAssumeNoVar = Hoare-NoVar (return (True {β„“zero}))

syntax Hoare-NoAssumeNoVar p ψ = βŸ…βŸ† p βŸ… ψ βŸ†
\end{code}