An Emacs editor tactic to produce Σ-types from Agda records (•̀ᴗ•́)و

example-usage.agda

-- Perform: M-x load-file RET to-Σ-editor-tactic.el
--
--------------------------------------------------------------------------------
-- Preamble
open import Data.Unit using (⊤; tt)
open import Data.Product public using (proj₁; proj₂; _,_)
open import Data.Product using (Σ)
open import Data.Nat
open import Relation.Binary.PropositionalEquality

Σ∶• : ∀ {a b} (A : Set a) (B : A → Set b) → Set _
Σ∶• = Σ

infix -666 Σ∶•
syntax Σ∶• A (λ x → B) = Σ x ∶ A • B

--------------------------------------------------------------------------------
{- Select the following record and press “C-x C-t” -}

record R (A : Set) (n : ℕ) : Set where

  Alias = A

  id : Set → Set
  id X = X

  field
    x : id Alias

  m : ℕ
  m = n

  field
    y : m ≡ n
    z : A

  more : Set → ℕ
  more = λ _ → n

--------------------------------------------------------------------------------
{- Now press “C-y” to paste in the derived Σ-version, as shown below -}


R′ : (A : Set) (n : ℕ) → Set
R′ = λ A n  → let  Alias = A ; id : Set → Set ; id X = X  in Σ x ∶ id Alias • let  m : ℕ ; m = n  in Σ y ∶ m ≡ n • Σ z ∶ A • let  more : Set → ℕ ; more = λ _ → n in ⊤

R-as-R′ : {A : Set} {n : ℕ} → R A n  → R′ A n
R-as-R′ = λ r → R.x r , R.y r , R.z r , tt

R′-as-R : {A : Set} {n : ℕ} → R′ A n  → R A n
R′-as-R = λ{ (x , y , z , tt) → record{x = x ; y = y ; z = z} }

R-Σ-to∘from≈id : {A : Set} {n : ℕ} → { r : R A n } → R′-as-R (R-as-R′ r) ≡ r
R-Σ-to∘from≈id {r = record{x = x ; y = y ; z = z}} = refl

R-Σ-from∘to≈id : {A : Set} {n : ℕ} → { σ : R A n } → R′-as-R (R-as-R′ σ) ≡ σ
R-Σ-from∘to≈id = refl

--------------------------------------------------------------------------------
{- Configuration

In the Lisp file, at the very top:

➬ Change the ‘Σ-naming-format’ string to alter how the Σ-variant should be named.

➬ Change the ‘record→Σ-coe-format’ string to alter how the record-to-Σ coercision
  should be named.

Likewise for the to-from bijection proofs.
-}

to-Σ-editor-tactic.el

;; Select an Agda record, then press C-x C-t to obtain a transformed
;; Σ-product form of the record; along with the expected bijection.
;; 
;; Musa Al-hassy ;; April 14 2020
;;
;; If this is useful to you, let me know and I'll happily extend it ^_^
;; 
;; Ensure the following lisp files are in your Emacs load path
;; https://github.com/magnars/dash.el
;; https://github.com/magnars/s.el

(require 's)
(require 'dash)
(require 'cl)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; User configurable settings

;; The new name of the Σ-variant: If R is the record name, then R′ is the
;; Σ-variant name. Change the syntax below for a different naming scheme.
(setq Σ-naming-format "%s′")
;; (setq Σ-naming-format "%s-Σ-variant") ;; For example.

;; The name of the “record to Σ-variant” coercion: The first ‘%s’ is the record
;; name and the second ‘%s’ is the Σ-variant name as determine by
;; ‘Σ-naming-format’.
(setq record→Σ-coe-format "%s-as-%s")
;; (setq record→Σ-coe-format "%s-as-iterated-Σ") ;; For example.

;; The name of the “Σ-variant to record” coercion: The first ‘%s’ is the
;; Σ-variant name as determine by ‘Σ-naming-format’ and the second ‘%s’ is the
;; record name.
(setq Σ→record-coe-format "%s-as-%s")
;; (setq Σ→record-coe-format "from-%s")  ;; For example.

;; The first and only ‘%s’ is the name of the record.
(setq to∘from≈id-format "%s-Σ-to∘from≈id")

;; The first and only ‘%s’ is the name of the record.
(setq from∘to≈id-format "%s-Σ-from∘to≈id")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun indent (s) 
  (length (car (s-match "\\( \\)+" s))))

(defun record-info (rrr)
  "Returns (name params level . body)  where ‘body’ is (qualifier . entry)*"
  (-let* ((((header . preamble) . rest)
             (--split-when (s-contains? "field" it) (s-lines (s-trim rrr))))
          ((_ lhs lvl)
             (s-match "record \\(.*\\) : Set\\(.*\\) where" header))
          ((nom . parms₀)
             (s-split " " lhs))
          (parms (s-join " " parms₀)))

    (-cons* nom parms lvl
    (apply #'-concat
    (cons (--map (cons 'let (s-trim it)) preamble)
    (loop for p in rest
          for indent = (indent (first p))
          collect (--map (cons (if (= indent (indent it)) 'field 'let) (s-trim it))
                         p)))))))

;; Override “transpose-lines” keybinding
;; to be “t”ransform to Σ-record
(global-set-key (kbd "C-x C-t")
(defun transform-to-Σ (beginning end)
  (interactive "r")
  (when (use-region-p)
    (kill-region beginning end)
    (-let* ((rrr (substring-no-properties (car kill-ring)))
           (_ (insert rrr))
           ((name params level . body) (record-info rrr))
           (args (s-collapse-whitespace (s-join " "
                     (--map (-let [(_ e τ r)
                                  (s-match "\\(.*\\):\\(.*\\)\\(}\\|)\\)" it)]
			      e)			    
                     (--map (s-join "" it)						 
                     (rest (--split-when (member it '("{" "(")) (s-split "" params))))))))
          (record{xᵢ=xᵢ}ᵢ
              (format "record{%s}"
              (s-join " ; "
                 (loop for (_ . e) in (--filter (equal 'field (car it)) body)
                       for field = (first (s-split " : " e))
                       collect (format "%s = %s" field field))))))
      (kill-new
  (s-concat
   ;; type declaration
   (format Σ-naming-format name)
   " : "
   (when params (concat params " → "))
   "Set " level "\n"
   ;; body
   (format Σ-naming-format name) " = "
   (if (s-blank? (s-trim args))
       ""
       (format "λ %s → " args))
   (s-replace "; in" " in"
   (s-replace "let ;" "let "
   (s-replace "; ;" ";"
   (s-replace "in let" ";"
   (s-collapse-whitespace
   (loop for (q . e) in body
         for e′ = (if (equal q 'field) (s-replace ":" "∶" e) e)
         concat (format (if (equal q 'field) "Σ %s • " "let %s in ") e′))))))) "⊤"

   "\n\n"

   ;; coercion
   (format record→Σ-coe-format name (format Σ-naming-format name))
   " : "
   (s-replace "(" "{" (s-replace ")" "}" params))
   (when params " → ")
   name " " args " → " (format Σ-naming-format name) " " args
   "\n"

   (format record→Σ-coe-format name (format Σ-naming-format name))
   " = λ r → "
   (loop for (_ . e) in (--filter (equal 'field (car it)) body)
         for field = (first (s-split " : " e))
         concat (format "%s.%s r , " name field))
   "tt"

   "\n\n"
   ;; coercion, the other way around
   (format Σ→record-coe-format (format Σ-naming-format name) name)
   " : "
   (s-replace "(" "{" (s-replace ")" "}" params))
   (when params " → ")
   (format Σ-naming-format name) " " args " → " name " " args
   "\n"

   (format Σ→record-coe-format (format Σ-naming-format name) name)
   " = λ{ ("
   (s-join " , "
   (loop for (_ . e) in (--filter (equal 'field (car it)) body)
         for field = (first (s-split " : " e))
         collect field))
   " , tt) → "
   record{xᵢ=xᵢ}ᵢ
   " }" ;; pattern matching λ

   "\n\n"
   ;; to∘from≈id
   (format to∘from≈id-format name)
   " : "
   (s-replace "(" "{" (s-replace ")" "}" params))
   (when params " → ")
   "{ r : " name " " args "} → "
   (format Σ→record-coe-format (format Σ-naming-format name) name)
   " (" (format record→Σ-coe-format name (format Σ-naming-format name))
   " r) ≡ r"
   "\n"
   (format to∘from≈id-format name)
   " {r = " record{xᵢ=xᵢ}ᵢ "} = refl"

   "\n\n"
   ;; from∘to≈id
   (format from∘to≈id-format name)
   " : "
   (s-replace "(" "{" (s-replace ")" "}" params))
   (when params " → ")
   "{ σ : " name " " args "} → "
   (format Σ→record-coe-format (format Σ-naming-format name) name)
   " (" (format record→Σ-coe-format name (format Σ-naming-format name))
   " σ) ≡ σ"
   "\n"
   (format from∘to≈id-format name)
   " = refl"   
   )) ;; kill-new
      (message "A Σ-variant is now in your clipboard -- press C-y to paste it (•̀ᴗ•́)و")))))

An Emacs editor tactic in the style of Agda's auto mechanism.
to transfomr the notationally conveneint Agda records into the more uniform
Sigma types.

0. Select, highlight, the record you are interested in;
1. Press C-x C-t to have a Sigma type and bijection to be created;
2. Paste in the Sigma type, and coercion, with C-y wherever you like.

This editor tactic lets you view a record as an iterated Sigma type.