-- This file:
--   http://angg.twu.net/AGDA/Postulate1.agda.html
--   http://angg.twu.net/AGDA/Postulate1.agda
--           (find-angg "AGDA/Postulate1.agda")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
-- Version: 2021dec28 (with tiny changes later)
-- Public domain.
--
-- Long story short: if we want to build telescopes for tests the
-- right tool to use is "postulate", not "variable". See:
--   https://lists.chalmers.se/pipermail/agda/2021/012832.html my question
--   https://lists.chalmers.se/pipermail/agda/2021/012834.html Jesper's answer =)
-- My failed attempt to use "variable"s is here:
--   (find-angg "AGDA/Variable1.agda")
--
-- This file takes some examples of the old RecordsTutorial and makes
-- them more concrete by specializing the "n" and the "m" in the
-- length of its telescopes to 2 and 2.
--
-- The sexp hyperlinks with `page' and `text' are explained here:
-- (find-pdf-like-intro "7. Shorter hyperlinks to PDF files")
--
-- ;; (find-eev "eev-pdflike.el" "change-default-viewer")
-- ;; (defalias 'find-pdf-page 'find-pdftools-page)
-- ;; (defalias 'find-pdf-page 'find-xpdf-page)
--
-- https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening
-- (find-recordstutorialpage 13 "Opening a record")
-- (find-recordstutorialtext 13 "Opening a record")
--
-- ;; (find-angg "AGDA/find-agdatype.el" "video-0")
-- ;; (find-angg "AGDA/find-agdatype.el")
-- (load       "~/AGDA/find-agdatype.el")

module Postulate1 where

-- From:
-- https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#syntax
-- (find-recordstutorialpage 12 "General Syntax and Meaning")
-- (find-recordstutorialtext 12 "General Syntax and Meaning")
--
--   General Syntax and Meaning
--   A record type in general is declared in the following way.
--   
--     record R Δ : Set where
--       field
--         x₁ : A₁[y₁, ..., yₘ₋₁]
--         x₂ : A₁[y₁, ..., yₘ₋₁, x₁]
--         ...
--         xₙ : A₁[y₁, ..., yₘ₋₁, x₁, ..., xₙ₋₁]
--   
--   Here, Δ represents a 'telescope', which is of the following form
--   
--     (y₁ : B₁) (y₂ : B₂[y₁]) ... (yₘ : Bₘ[y₁, ..., yₘ₋₁])
--
-- Let's make m:=2 and n:=2.
-- Then...

postulate B₁ :                                              Set
postulate B₂ : (y₁ : B₁) →                                  Set
postulate A₁ : (y₁ : B₁) → (y₂ : B₂ y₁) →                   Set
postulate A₂ : (y₁ : B₁) → (y₂ : B₂ y₁) → (x₁ : A₁ y₁ y₂) → Set
-- (find-agdatype " B₁   ")
-- (find-agdatype " B₂   ")
-- (find-agdatype " A₁   ")
-- (find-agdatype " A₂   ")

-- postulate y₁ : B₁
-- postulate y₂ : B₂ y₁
-- postulate x₁ : A₁ y₁ y₂
-- postulate x₂ : A₂ y₁ y₂ x₁

---- ^ These postulates were useful in my first tests, but their names
---- started to collide with other things and I had to comment them
---- out...
---- (find-agdatype " y₁   ")
---- (find-agdatype " y₂   ")
---- (find-agdatype " x₁   ")
---- (find-agdatype " x₂   ")
---- (find-agdatype " B₁          ")
---- (find-agdatype " B₂ y₁       ")
---- (find-agdatype " A₁ y₁ y₂    ")
---- (find-agdatype " A₂ y₁ y₂ x₁ ")


record R (y₁ : B₁) (y₂ : B₂ y₁) : Set1 where
  field
    x₁ : A₁ y₁ y₂
    x₂ : A₂ y₁ y₂ x₁

postulate ay₁ : B₁
postulate ay₂ : B₂ ay₁
postulate ax₁ : A₁ ay₁ ay₂
postulate ax₂ : A₂ ay₁ ay₂ ax₁
postulate ar  : R  ay₁ ay₂

-- (find-recordstutorialpage 13 "This declaration introduces")
-- (find-recordstutorialtext 13 "This declaration introduces")
-- (find-agdatype " R         ")
-- (find-agdatype " R.x₁      ")
-- (find-agdatype " R.x₂      ")

-- (find-agdatype "      ar   ")
-- (find-agdatype " R.x₁ ar   ")
-- (find-agdatype " R.x₂ ar   ")

-- (find-agdatype " R ay₁     ")
-- (find-agdatype " R ay₁ ay₂ ")

-- From:
-- https://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.RecordsTutorial#opening
-- (find-recordstutorialpage 13 "Opening a record")
-- (find-recordstutorialtext 13 "Opening a record")
-- (...) For the record R above, we generate a parametrised module R:
--
--   module R {Δ} (r : R Δ) where
--       x₁ : A₁[y₁, ..., yₘ₋₁]
--       x₁ = ...
--       x₂ : A₂[y₁, ..., yₘ₋₁, x₁]
--       x₂ = ...
--       ...
--       xₙ : Aₙ[y₁, ..., yₘ₋₁, x₁, ..., xₙ₋₁]
--       xₙ = ...

module MR {y₁ : B₁} {y₂ : B₂ y₁} (r : R y₁ y₂) where
    x₁ : A₁ y₁ y₂
    x₁ = {!!}
    x₂ : A₂ y₁ y₂ x₁
    x₂ = {!!}

-- (find-recordstutorialpage 14 "Record opening example")
-- (find-recordstutorialtext 14 "Record opening example")
-- (find-agdatype " MR.x₁    ")
-- (find-agdatype " MR.x₂    ")
-- (find-agdatype " MR.x₁ ar ")
-- (find-agdatype " MR.x₂ ar ")

module TestOpen where
  open MR ar
  goal : {!!}
  goal = {!!}
  -- (find-agdatype  " x₁    ")
  -- (find-agdatypep " x₁    ")
  -- ^ Note that here `find-agdatype' doesn't work,
  --   but `find-agdatypep' does...



-- Local Variables:
-- coding:  utf-8-unix
-- End: