    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- An example of how to use `Wrap` to help term inference.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module README.Data.Wrap where

    open import Data.Wrap

    open import Algebra
    open import Data.Nat
    open import Data.Nat.Properties
    open import Data.Product.Base using (_,_; ∃; ∃₂; _×_)
    open import Level using (Level)

    private
      variable
        c ℓ : Level
        A : Set c
        m n : ℕ

    ------------------------------------------------------------------------
    -- `Wrap` for remembering instances
    ------------------------------------------------------------------------

    module Instances where

      -- `Monoid.Carrier` gets the carrier set from a monoid, and thus has
      -- type `Monoid c ℓ → Set c`.
      -- Using `Wrap`, we can convert `Monoid.Carrier` into an equivalent
      -- “wrapped” version: `MonoidEl`.
      MonoidEl : Monoid c ℓ → Set c
      MonoidEl = Wrap Monoid.Carrier

      -- We can turn any monoid into the equivalent monoid where the elements
      -- and equations have been wrapped.
      -- The translation mainly consists of wrapping and unwrapping everything
      -- via the `Wrap` constructor, `[_]`.
      -- Notice that the equality field is wrapping the binary relation
      -- `_≈_ : (x y : Carrier) → Set ℓ`, giving an example of how `Wrap` works
      -- for arbitrary n-ary relations.
      Wrap-monoid : Monoid c ℓ → Monoid c ℓ
      Wrap-monoid M = record
        { Carrier = MonoidEl M
        ; _≈_ = λ ([ x ]) ([ y ]) → Wrap _≈_ x y
        ; _∙_ = λ ([ x ]) ([ y ]) → [ x ∙ y ]
        ; ε = [ ε ]
        ; isMonoid = record
          { isSemigroup = record
            { isMagma = record
              { isEquivalence = record
                { refl = [ refl ]
                ; sym = λ ([ xy ]) → [ sym xy ]
                ; trans = λ ([ xy ]) ([ yz ]) → [ trans xy yz ]
                }
              ; ∙-cong = λ ([ xx ]) ([ yy ]) → [ ∙-cong xx yy ]
              }
            ; assoc = λ ([ x ]) ([ y ]) ([ z ]) → [ assoc x y z ]
            }
          ; identity = (λ ([ x ]) → [ identityˡ x ])
                     , (λ ([ x ]) → [ identityʳ x ])
          }
        }
        where open Monoid M

      -- Usually, we would only open one monoid at a time.
      -- If we were to open two monoids `M` and `N` simultaneously, Agda would
      -- get confused whenever it came across, for example, `_∙_`, not knowing
      -- whether it came from `M` or `N`.
      -- This is true whether or not `M` and `N` can be disambiguated by some
      -- other means (such as by their `Carrier`s).

      -- However, with wrapped monoids, we are going to remember the monoid
      -- while checking any monoid expressions, so we can afford to have just
      -- one, polymorphic, version of `_∙_` visible globally.
      open module Wrap-monoid {c ℓ} {M : Monoid c ℓ} = Monoid (Wrap-monoid M)

      -- Now we can test out this construct on some existing monoids.

      open import Data.Nat.Properties

      -- Notice that, while the following two definitions appear to be defined
      -- by the same expression, their types are genuinely different.
      -- Whereas `Carrier +-0-monoid = ℕ = Carrier *-1-monoid`, `MonoidEl M`
      -- does not compute, and thus
      -- `MonoidEl +-0-monoid ≠ MonoidEl *-1-monoid` definitionally.
      -- This lets us use the respective monoids when checking the respective
      -- definitions.

      test-+ : MonoidEl +-0-monoid
      test-+ = ([ 3 ] ∙ ε) ∙ [ 2 ]

      test-* : MonoidEl *-1-monoid
      test-* = ([ 3 ] ∙ ε) ∙ [ 2 ]

      -- The reader is invited to normalise these two definitions
      -- (`C-c C-n`, then type in the name).
      -- `test-+` is interpreted using (ℕ, +, 0), and thus computes to `[ 5 ]`.
      -- Meanwhile, `test-*` is interpreted using (ℕ, *, 1), and thus computes
      -- to `[ 6 ]`.

    ------------------------------------------------------------------------
    -- `Wrap` for dealing with functions spoiling unification
    ------------------------------------------------------------------------

    module Unification where

      open import Relation.Binary.PropositionalEquality

      module Naïve where

        -- We want to work with factorisations of natural numbers in a
        -- “proof-relevant” style. We could draw out `Factor m n o` as
        --   m
        --  /*\
        -- n   o.

        Factor : (m n o : ℕ) → Set
        Factor m n o = m ≡ n * o

        -- We can prove a basic lemma about `Factor`: the following tree rotation
        -- can be done, due to associativity of `_*_`.
        --      m             m
        --     /*\           /*\
        --   no   p  ---->  n   op
        --  /*\                 /*\
        -- n   o               o   p

        assoc-→ : ∀ {m n o p} →
                  (∃ λ no → Factor m no p × Factor no n o) →
                  (∃ λ op → Factor m n op × Factor op o p)
        assoc-→ {m} {n} {o} {p} (._ , refl , refl) = _ , *-assoc n o p , refl

        -- We must give at least some arguments to `*-assoc`, as Agda is unable to
        -- unify `? * ? * ?` with `n * o * p`, as `_*_` is a function and not
        -- necessarily injective (and indeed not injective when one of its
        -- arguments is 0).

        -- We now want to use this lemma in a more complex proof:
        --         m            m
        --        /*\          /*\
        --     nop   q        n   opq
        --     /*\      ---->     /*\
        --   no   p              o   pq
        --  /*\                      /*\
        -- n   o                    p   q

        test : ∀ {m n o p q} →
               (∃₂ λ no nop → Factor m nop q × Factor nop no p × Factor no n o) →
               (∃₂ λ pq opq → Factor m n opq × Factor opq o pq × Factor pq p q)
        test {n = n} (no , nop , fm , fnop , fno) =
          let _ , fm , fpq = assoc-→ {n = no} (_ , fm , fnop) in
          let _ , fm , fopq = assoc-→ {n = n} (_ , fm , fno) in
          _ , _ , fm , fopq , fpq

        -- This works okay, but where we have written `{n = no}` and similar, we
        -- are being forced to deal with details we don't really care about. Agda
        -- should be able to fill in the vertices given part of a tree, but can't
        -- due to similar reasons as before: `Factor ? ? ?` doesn't unify against
        -- `Factor m no p`, because both instances of `Factor` compute and we're
        -- left trying to unify `? * ?` against `no * p`.

      module Wrapped where

        -- We can use `Wrap` to stop the computation of `Factor`.

        Factor : (m n o : ℕ) → Set
        Factor = Wrap λ m n o → m ≡ n * o

        -- Because `assoc-→` needs access to the implementation of `Factor`, the
        -- proof is exactly as before except for using `[_]` to wrap and unwrap.

        assoc-→ : ∀ {m n o p} →
                  (∃ λ no → Factor m no p × Factor no n o) →
                  (∃ λ op → Factor m n op × Factor op o p)
        assoc-→ {m} {n} {o} {p} (._ , [ refl ] , [ refl ]) =
          _ , [ *-assoc n o p ] , [ refl ]

        -- The difference is that now we have our basic lemma, the complex proof
        -- can work purely in terms of `Factor` trees. In particular,
        -- `Factor ? ? ?` now does unify with `Factor m no p`, so we don't have to
        -- give `no` explicitly again.

        test : ∀ {m n o p q} →
               (∃₂ λ no nop → Factor m nop q × Factor nop no p × Factor no n o) →
               (∃₂ λ pq opq → Factor m n opq × Factor opq o pq × Factor pq p q)
        test (_ , _ , fm , fnop , fno) =
          let _ , fm , fpq = assoc-→ (_ , fm , fnop) in
          let _ , fm , fopq = assoc-→ (_ , fm , fno) in
          _ , _ , fm , fopq , fpq