diff --git a/README.md b/README.md new file mode 100644 index 0000000..98b0b56 --- /dev/null +++ b/README.md @@ -0,0 +1,36 @@ +Lambda calc on CEK machine with call/cc +=== + +This is my term project for CSCI 8980: Programming Language Foundations in +Agda during the Fall 2021 semester. It follows a [textbook of the same +name][textbook]. + +[textbook]: https://plfa.github.io/ + +Assignment: + +> Your Agda project should be formalizing some language feature not detailed in +> the textbook and proving type safety of it. Your formalization should contain +> these three ingredients: +> +> 1. The statics: the type system. +> 2. The dynamics: a dynamic system that is different from the reduction system +> used in Part 2 of the textbook. +> 3. The theorems: progress and preservation as type safety. + +My project formalizes a lambda calculus with call/cc using a CEK interpreter +described by [Matt Might's blog post][might-cesk]. Slight modifications were +made to allow it to type correctly, but the semantics are very similar. + +Building +-------- + +If you already have Agda installed, compiling `src/Project/Cesk.agda` should +work. + +If not, this repository is a Nix flake; simply run `nix develop` and both neovim +with the Agda plugin and VSCode (FOSS edition) with its Agda extension are +available in the shell. + +[might-cesk]: https://matt.might.net/articles/cesk-machines/ + diff --git a/flake.lock b/flake.lock new file mode 100644 index 0000000..2e60b01 --- /dev/null +++ b/flake.lock @@ -0,0 +1,43 @@ +{ + "nodes": { + "flake-utils": { + "locked": { + "lastModified": 1638122382, + "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "74f7e4319258e287b0f9cb95426c9853b282730b", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1624913309, + "narHash": "sha256-HHZTzHgLuoOmTrHckl9eGG8UWTp32pYXmCoOjgQYIB4=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "860b56be91fb874d48e23a950815969a7b832fbc", + "type": "github" + }, + "original": { + "owner": "nixos", + "repo": "nixpkgs", + "rev": "860b56be91fb874d48e23a950815969a7b832fbc", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "nixpkgs": "nixpkgs" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..56a0808 --- /dev/null +++ b/flake.nix @@ -0,0 +1,52 @@ +{ + inputs = { + flake-utils.url = "github:numtide/flake-utils"; + nixpkgs.url = + "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc"; + }; + + outputs = { self, nixpkgs, flake-utils }: + flake-utils.lib.eachDefaultSystem (system: + let + pkgs = nixpkgs.legacyPackages.${system}; + + myPkgs = rec { + agda = pkgs.agda.withPackages (p: [ p.standard-library ]); + nvim-agda = import ./nix/nvim-agda { inherit nixpkgs system; }; + neovim = pkgs.callPackage ./nix/neovim.nix { inherit nvim-agda; }; + }; + + vscode-agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace { + name = "agda-mode"; + publisher = "banacorn"; + version = "0.2.19"; + sha256 = "2PFfFySOoxFEZdYb2BF6XQeYEygbTn/WJub/8IKfc1Y="; + }; + combinedExtensionsDrv = pkgs.buildEnv { + name = "vscodium-extensions"; + paths = [ vscode-agda-mode pkgs.vscode-extensions.vscodevim.vim ]; + }; + vscodium = pkgs.runCommand "vscodium-with-extensions" { + nativeBuildInputs = [ pkgs.makeWrapper ]; + buildInputs = [ pkgs.vscodium ]; + meta = pkgs.vscodium.meta; + } '' + mkdir -p $out/bin + makeWrapper "${pkgs.vscodium}/bin/codium" "$out/bin/codium" \ + --add-flags "--extensions-dir ${combinedExtensionsDrv}/share/vscode/extensions" + ''; + in { + packages = flake-utils.lib.flattenTree myPkgs; + + devShell = pkgs.mkShell { + buildInputs = with pkgs; + with myPkgs; [ + agda + vscodium + neovim + nvim-agda + lua51Packages.luautf8 + ]; + }; + }); +} diff --git a/main.tex b/main.tex index 47f7439..60e1185 100644 --- a/main.tex +++ b/main.tex @@ -49,6 +49,16 @@ \section{Background} +\begin{frame} + \frametitle{Overview} + + \begin{itemize} + \item Lambda calculus in A-normal form. + \item CESK machine is my dynamic system. + \item \texttt{call/cc} is my extra feature. + \end{itemize} +\end{frame} + \begin{frame} \frametitle{What is a CESK machine?} diff --git a/nix/agda.nix b/nix/agda.nix new file mode 100644 index 0000000..30cbe1e --- /dev/null +++ b/nix/agda.nix @@ -0,0 +1,4 @@ +{ nixpkgs, system, ... }: + +let pkgs = nixpkgs.legacyPackages.${system}; +in pkgs.agda.withPackages (p: [ p.standard-library ]) diff --git a/nix/neovim.nix b/nix/neovim.nix new file mode 100644 index 0000000..1b9d142 --- /dev/null +++ b/nix/neovim.nix @@ -0,0 +1,36 @@ +{ neovim, vimPlugins, luajitPackages, nvim-agda }: + +neovim.override { + configure = { + plug = { + plugins = with vimPlugins; [ + ctrlp-vim + nerdtree + nvim-agda + vim-code-dark + vim-polyglot + ]; + }; + + customRC = '' + lua << EOF + package.cpath = package.cpath .. ";${luajitPackages.luautf8}/lib/lua/5.1/lua-utf8.so" + EOF + + set hidden + set cursorline + set number + set splitright + set modeline + set expandtab + set colorcolumn=80 + syntax on + filetype on + filetype plugin indent on + colorscheme codedark + + nnoremap :NERDTreeToggle + imap kj + ''; + }; +} diff --git a/nix/nvim-agda/agda-vim-excerpts/LICENSE b/nix/nvim-agda/agda-vim-excerpts/LICENSE new file mode 100644 index 0000000..00257da --- /dev/null +++ b/nix/nvim-agda/agda-vim-excerpts/LICENSE @@ -0,0 +1,24 @@ +Copyright (c) 2013, Derek Elkins +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +Redistributions of source code must retain the above copyright notice, this +list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer in the +documentation and/or other materials provided with the distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/nix/nvim-agda/agda-vim-excerpts/README b/nix/nvim-agda/agda-vim-excerpts/README new file mode 100644 index 0000000..b96fc50 --- /dev/null +++ b/nix/nvim-agda/agda-vim-excerpts/README @@ -0,0 +1,2 @@ +autoload.vim and ftplugin.vim are mostly taken from +https://github.com/derekelkins/agda-vim, with slight modification. diff --git a/nix/nvim-agda/agda-vim-excerpts/autoload.vim b/nix/nvim-agda/agda-vim-excerpts/autoload.vim new file mode 100644 index 0000000..eaf8daf --- /dev/null +++ b/nix/nvim-agda/agda-vim-excerpts/autoload.vim @@ -0,0 +1,669 @@ +" Agda Input Abbreviations +" +let s:cpo_save = &cpo +set cpo&vim + +" Public to allow referencing in custom overrides. +if !exists('g:agda#default_glyphs') + let g:agda#default_glyphs = {} + + " Extra Shit + call extend(g:agda#default_glyphs, { + \ 'Gl-': 'ƛ', + \ '==': '≡', + \ '<': '⟨', + \ '>': '⟩', + \ 'em': '—', + \ '=>': '⇒', + \ '~-': '≃', + \ 'r': '→', + \ '0': '∅', + \ 'st': '★', + \}) + + " Combining marks + call extend(g:agda#default_glyphs, { + \ 'over`': ' ̀', + \ "over'": ' ́', + \ 'over^': ' ̂', + \ 'overv': ' ̌', + \ 'over~': ' ̃', + \ 'over-': ' ̄', + \ 'over_': ' ̅', + \ 'over–': ' ̅', + \ 'over—': ' ̅', + \ 'overcup': ' ̆', + \ 'overcap': ' ̑', + \ 'over.': ' ̇', + \ 'over..': ' ̈', + \ 'over"': ' ̈', + \ 'over...': ' ⃛', + \ 'overright.': ' ͘', + \ 'overo': ' ̊', + \ 'over``': ' ̏', + \ "over''": ' ̋', + \ 'overvec': ' ⃑', + \ 'vec': ' ⃑', + \ 'overlvec': ' ⃐', + \ 'lvec': ' ⃐', + \ 'overarc': ' ⃕', + \ 'overlarc': ' ⃔', + \ 'overto': ' ⃗', + \ 'overfrom': ' ⃖', + \ 'overfromto': ' ⃡', + \ 'over*': ' ⃰', + \ 'under`': ' ̖', + \ "under'": ' ̗', + \ 'under,': ' ̗', + \ 'under.': ' ̣', + \ 'under..': ' ̤', + \ 'under"': ' ̤', + \ 'undero': ' ̥', + \ 'under-': ' ̱', + \ 'under_': ' ̲', + \ 'under–': ' ̲', + \ 'under—': ' ̲', + \ 'through~': ' ̴', + \ 'through-': ' ̵', + \ 'through_': ' ̶', + \ 'through–': ' ̶', + \ 'through—': ' ̶', + \ 'through/': ' ̷', + \ 'not': ' ̷', + \ 'through?': ' ̸', + \ 'Not': ' ̸', + \ 'through\|': ' ⃒', + \ 'throughshortmid': ' ⃓', + \ 'througho': ' ⃘', + \}) + + " Math + " \ ':': '∶', + call extend(g:agda#default_glyphs, { + \ '{{': '⦃', + \ '}}': '⦄', + \ ':': '⦂', + \ '::': '∷', + \ ';': '﹔', + \ '..': '‥', + \ '=?': '≟', + \ 'all': '∀', + \ 'always': '□', + \ 'approx': '≈', + \ 'bot': '⊥', + \ 'box': '□', + \ 'boxdot': '⊡', + \ 'box.': '⊡', + \ 'boxminus': '⊟', + \ 'box-': '⊟', + \ 'boxplus': '⊞', + \ 'box+': '⊞', + \ 'boxtimes': '⊠', + \ 'box*': '⊠', + \ 'bul': '•', + \ 'C': 'ℂ', + \ 'cdot': '·', + \ '.': '∙', + \ 'cdots': '⋯', + \ 'check': '✓', + \ 'yes': '✓', + \ 'Check': '✔', + \ 'Yes': '✔', + \ 'circ': '∘', + \ 'clock': '↻', + \ 'cclock': '↺', + \ 'comp': '∘', + \ 'contra': '↯', + \ 'deg': '°', + \ 'den': '⟦⟧', + \ 'diamond': '◇', + \ 'dots': '…', + \ 'down': '↓', + \ 'downtri': '▼', + \ 'Down': '⇓', + \ 'dunion': '⊎', + \ 'du': '⊎', + \ 'ell': 'ℓ', + \ 'empty': '∅', + \ 'equiv': '≡', + \ 'eq': '≡', + \ 'eventually': '◇', + \ 'exists': '∃', + \ 'flat': '♭', + \ 'fold': '⦇⦈', + \ '(\|': '⦇', + \ '\|)': '⦈', + \ 'forall': '∀', + \ 'from': '←', + \ '<-': '←', + \ 'From': '⇐', + \ 'fromto': '↔', + \ 'Fromto': '⇔', + \ 'ge': '≥', + \ 'glub': '⊓', + \ 'iff': '⇔', + \ 'implies': '⇒', + \ 'impliedby': '⇐', + \ 'in': '∈', + \ 'infty': '∞', + \ 'inf': '∞', + \ 'int': '∫', + \ 'intersect': '∩', + \ 'iso': '≅', + \ 'join': '⋈', + \ 'land': '∧', + \ 'langle': '⟨', + \ 'lbrac': '⟦', + \ '[[': '⟦', + \ 'ldots': '…', + \ 'ldown': '⇃', + \ 'leadsto': '⇝', + \ '~>': '⇝', + \ 'le': '≤', + \ 'lift': '⌊⌋', + \ 'floor': '⌊⌋', + \ 'llangle': '⟪', + \ 'longto': '⟶ ', + \ '--': '⟶ ', + \ '–': '⟶ ', + \ 'lor': '∨', + \ 'lower': '⌈⌉', + \ 'ceil': '⌈⌉', + \ 'lub': '⊔', + \ 'lup': '↿', + \ 'mapsto': '↦', + \ 'map': '↦', + \ 'mid': '∣', + \ 'models': '⊨', + \ '\|=': '⊨', + \ 'N': 'ℕ', + \ 'ne': '≠', + \ 'nearrow': '↗', + \ 'Nearrow': '⇗', + \ 'neg': '¬', + \ '/=': '≠', + \ 'nequiv': '≢', + \ 'neq': '≢', + \ 'nexist': '∄', + \ 'none': '∄', + \ 'ni': '∋', + \ 'nin': '∉', + \ 'niso': '≇', + \ 'notin': '∉', + \ 'nwarrow': '↖', + \ 'Nwarrow': '⇖', + \ 'oast': '⊛', + \ 'odot': '⊙', + \ 'o.': '⊙', + \ 'of': '∘', + \ 'o': '∘', + \ 'ominus': '⊖', + \ 'o-': '⊖', + \ 'oplus': '⊕', + \ 'o+': '⊕', + \ 'oslash': '⊘', + \ 'o/': '⊘', + \ 'otimes': '⊗', + \ 'o*': '⊗', + \ 'par': '∂', + \ 'pge': '≽', + \ 'pgt': '≻', + \ 'ple': '≼', + \ 'plt': '≺', + \ 'p≥': '≽', + \ 'p>': '≻', + \ 'p≤': '≼', + \ 'p<': '≺', + \ 'pm': '±', + \ 'prec': '≼', + \ 'prod': '∏', + \ 'proves': '⊢', + \ '\|-': '⊢', + \ 'provedby': '⊣', + \ 'Q': 'ℚ', + \ 'qed': '∎', + \ 'R': 'ℝ', + \ 'rangle': '⟩', + \ 'rbrac': '⟧', + \ ']]': '⟧', + \ 'rdown': '⇂', + \ 'righttri': '▸', + \ 'rrangle': '⟫', + \ 'rup': '↾', + \ 'searrow': '↘', + \ 'Searrow': '⇘', + \ 'setminus': '∖', + \ 'sharp': '♯', + \ '#': '♯', + \ 'sim': '∼', + \ 'simeq': '≃', + \ 'some': '∃', + \ 'sqge': '⊒', + \ 'sqgt': '⊐', + \ 'sqle': '⊑', + \ 'sqlt': '⊏', + \ 's≥': '⊒', + \ 's>': '⊐', + \ 's≤': '⊑', + \ 's<': '⊏', + \ 'sqr': '²', + \ 'sqrt': '√', + \ 'star': '✭', + \ 'subset': '⊂', + \ 'sub': '⊂', + \ 'subseteq': '⊆', + \ 'subeq': '⊆', + \ 'subsetneq': '⊊', + \ 'subneq': '⊊', + \ 'sum': '∑', + \ 'supset': '⊃', + \ 'sup': '⊃', + \ 'supseteq': '⊇', + \ 'supeq': '⊇', + \ 'supsetneq': '⊋', + \ 'supneq': '⊋', + \ 'swarrow': '↙', + \ 'Swarrow': '⇙', + \ 'thus': '∴', + \ 'times': '×', + \ '*': '×', + \ 'to': '→', + \ '-': '→', + \ 'To': '⇒', + \ '=': '⇒', + \ 'top': '⊤', + \ 'tuple': '⟨⟩', + \ 'up': '↑', + \ 'updown': '↕', + \ 'ud': '↕', + \ 'unfold': '⦉⦊', + \ '<\|': '⦉', + \ '\|>': '⦊', + \ 'up;down': '⇅', + \ 'u;d': '⇅', + \ 'uptri': '▲', + \ 'Up': '⇑', + \ 'union': '∪', + \ 'vdots': '⋮', + \ 'voltage': '⚡', + \ 'xmark': '✗', + \ 'no': '✗', + \ 'Xmark': '✘', + \ 'No': '✘', + \ 'Z': 'ℤ', + \}) + + " Not math + call extend(g:agda#default_glyphs, { + \ 'sec': '§', + \}) + + " Superscripts + call extend(g:agda#default_glyphs, { + \ '^0': '⁰', + \ '^1': '¹', + \ '^2': '²', + \ '^3': '³', + \ '^4': '⁴', + \ '^5': '⁵', + \ '^6': '⁶', + \ '^7': '⁷', + \ '^8': '⁸', + \ '^9': '⁹', + \ '^A': 'ᴬ', + \ '^B': 'ᴮ', + \ '^D': 'ᴰ', + \ '^E': 'ᴱ', + \ '^G': 'ᴳ', + \ '^H': 'ᴴ', + \ '^I': 'ᴵ', + \ '^J': 'ᴶ', + \ '^K': 'ᴷ', + \ '^L': 'ᴸ', + \ '^M': 'ᴹ', + \ '^N': 'ᴺ', + \ '^O': 'ᴼ', + \ '^P': 'ᴾ', + \ '^R': 'ᴿ', + \ '^T': 'ᵀ', + \ '^U': 'ᵁ', + \ '^V': 'ⱽ', + \ '^W': 'ᵂ', + \ '^a': 'ᵃ', + \ '^b': 'ᵇ', + \ '^c': 'ᶜ', + \ '^d': 'ᵈ', + \ '^e': 'ᵉ', + \ '^f': 'ᶠ', + \ '^g': 'ᵍ', + \ '^h': 'ʰ', + \ '^i': 'ⁱ', + \ '^j': 'ʲ', + \ '^k': 'ᵏ', + \ '^l': 'ˡ', + \ '^m': 'ᵐ', + \ '^n': 'ⁿ', + \ '^o': 'ᵒ', + \ '^p': 'ᵖ', + \ '^r': 'ʳ', + \ '^s': 'ˢ', + \ '^t': 'ᵗ', + \ '^u': 'ᵘ', + \ '^v': 'ᵛ', + \ '^w': 'ʷ', + \ '^x': 'ˣ', + \ '^y': 'ʸ', + \ '^z': 'ᶻ', + \ '^+': '⁺', + \ '^-': '⁻', + \ '^=': '⁼', + \ '^(': '⁽', + \ '^)': '⁾', + \ "'": '′', + \ "''": '″', + \ "'''": '‴', + \ "''''": '⁗', + \ '"': '″', + \ '""': '⁗', + \ '`': '‵', + \ '``': '‶', + \ '```': '‷', + \}) + + " Subscripts + call extend(g:agda#default_glyphs, { + \ '_0': '₀', + \ '_1': '₁', + \ '_2': '₂', + \ '_3': '₃', + \ '_4': '₄', + \ '_5': '₅', + \ '_6': '₆', + \ '_7': '₇', + \ '_8': '₈', + \ '_9': '₉', + \ '_a': 'ₐ', + \ '_e': 'ₑ', + \ '_h': 'ₕ', + \ '_i': 'ᵢ', + \ '_j': 'ⱼ', + \ '_k': 'ₖ', + \ '_l': 'ₗ', + \ '_m': 'ₘ', + \ '_n': 'ₙ', + \ '_o': 'ₒ', + \ '_p': 'ₚ', + \ '_r': 'ᵣ', + \ '_s': 'ₛ', + \ '_t': 'ₜ', + \ '_u': 'ᵤ', + \ '_v': 'ᵥ', + \ '_x': 'ₓ', + \ '_+': '₊', + \ '_-': '₋', + \ '_=': '₌', + \ '_(': '₍', + \ '_)': '₎', + \ 'p0': 'π₀', + \ 'p1': 'π₁', + \ 'p2': 'π₂', + \ 'p3': 'π₃', + \ 'p4': 'π₄', + \ 'p5': 'π₅', + \ 'p6': 'π₆', + \ 'p7': 'π₇', + \ 'p8': 'π₈', + \ 'p9': 'π₉', + \ 'i0': 'ι₀', + \ 'i1': 'ι₁', + \ 'i2': 'ι₂', + \ 'i3': 'ι₃', + \ 'i4': 'ι₄', + \ 'i5': 'ι₅', + \ 'i6': 'ι₆', + \ 'i7': 'ι₇', + \ 'i8': 'ι₈', + \ 'i9': 'ι₉', + \}) + + " Greek (lower) + call extend(g:agda#default_glyphs, { + \ 'alpha': 'α', + \ 'a': 'α', + \ 'beta': 'β', + \ 'b': 'β', + \ 'gamma': 'γ', + \ 'g': 'γ', + \ 'delta': 'δ', + \ 'd': 'δ', + \ 'epsilon': 'ε', + \ 'e': 'ε', + \ 'zeta': 'ζ', + \ 'z': 'ζ', + \ 'eta': 'η', + \ 'h': 'η', + \ 'theta': 'θ', + \ 'iota': 'ι', + \ 'i': 'ι', + \ 'kappa': 'κ', + \ 'k': 'κ', + \ 'lambda': 'λ', + \ 'l': 'λ', + \ 'mu': 'μ', + \ 'm': 'μ', + \ 'nu': 'ν', + \ 'n': 'ν', + \ 'xi': 'ξ', + \ 'omicron': 'ο', + \ 'pi': 'π', + \ 'p': 'π', + \ 'rho': 'ρ', + \ 'sigma': 'σ', + \ 's': 'σ', + \ 'varsigma': 'ς', + \ 'vars': 'ς', + \ 'tau': 'τ', + \ 't': 'τ', + \ 'u': 'υ', + \ 'phi': 'φ', + \ 'f': 'φ', + \ 'chi': 'χ', + \ 'x': 'χ', + \ 'psi': 'ψ', + \ 'c': 'ψ', + \ 'omega': 'ω', + \ 'v': 'ω', + \}) + + " Greek (upper) + call extend(g:agda#default_glyphs, { + \ 'Alpha': 'Α', + \ 'Beta': 'Β', + \ 'Gamma': 'Γ', + \ 'G': 'Γ', + \ 'Delta': 'Δ', + \ 'D': 'Δ', + \ 'Epsilon': 'Ε', + \ 'Zeta': 'Ζ', + \ 'Eta': 'Η', + \ 'Theta': 'Θ', + \ 'Iota': 'Ι', + \ 'Kappa': 'Κ', + \ 'Lambda': 'Λ', + \ 'L': 'Λ', + \ 'Mu': 'Μ', + \ 'Nu': 'Ν', + \ 'Xi': 'Ξ', + \ 'Omicron': 'Ο', + \ 'Pi': 'Π', + \ 'P': 'Π', + \ 'Rho': 'Ρ', + \ 'Sigma': 'Σ', + \ 'S': 'Σ', + \ 'Tau': 'Τ', + \ 'Upsilon': 'Υ', + \ 'Phi': 'Φ', + \ 'F': 'Φ', + \ 'Chi': 'Χ', + \ 'Psi': 'Ψ', + \ 'Omega': 'Ω', + \ 'V': 'Ω', + \}) + + " Blackboard + call extend(g:agda#default_glyphs, { + \ 'bA': '𝔸', + \ 'bB': '𝔹', + \ 'bC': 'ℂ', + \ 'bD': '𝔻', + \ 'bE': '𝔼', + \ 'bF': '𝔽', + \ 'bG': '𝔾', + \ 'bH': 'ℍ', + \ 'bI': '𝕀', + \ 'bJ': '𝕁', + \ 'bK': '𝕂', + \ 'bL': '𝕃', + \ 'bM': '𝕄', + \ 'bN': 'ℕ', + \ 'bO': '𝕆', + \ 'bP': 'ℙ', + \ 'bQ': 'ℚ', + \ 'bR': 'ℝ', + \ 'bS': '𝕊', + \ 'bT': '𝕋', + \ 'bU': '𝕌', + \ 'bV': '𝕍', + \ 'bW': '𝕎', + \ 'bX': '𝕏', + \ 'bY': '𝕐', + \ 'bZ': 'ℤ', + \ 'b0': '𝟘', + \ 'b1': '𝟙', + \ 'b2': '𝟚', + \ 'b3': '𝟛', + \ 'b4': '𝟜', + \ 'b5': '𝟝', + \ 'b6': '𝟞', + \ 'b7': '𝟟', + \ 'b8': '𝟠', + \ 'b9': '𝟡', + \ 'bsum': '⅀', + \}) + + " Math chars + call extend(g:agda#default_glyphs, { + \ 'McA': '𝓐', + \ 'McB': '𝓑', + \ 'McC': '𝓒', + \ 'McD': '𝓓', + \ 'McE': '𝓔', + \ 'McF': '𝓕', + \ 'McG': '𝓖', + \ 'McH': '𝓗', + \ 'McI': '𝓘', + \ 'McJ': '𝓙', + \ 'McK': '𝓚', + \ 'McL': '𝓛', + \ 'McM': '𝓜', + \ 'McN': '𝓝', + \ 'McO': '𝓞', + \ 'McP': '𝓟', + \ 'McQ': '𝓠', + \ 'McR': '𝓡', + \ 'McS': '𝓢', + \ 'McT': '𝓣', + \ 'McU': '𝓤', + \ 'McV': '𝓥', + \ 'McW': '𝓦', + \ 'McX': '𝓧', + \ 'McY': '𝓨', + \ 'McZ': '𝓩', + \ 'Mca': '𝒶', + \ 'Mcb': '𝒷', + \ 'Mcc': '𝒸', + \ 'Mcd': '𝒹', + \ 'Mcf': '𝒻', + \ 'Mch': '𝒽', + \ 'Mci': '𝒾', + \ 'Mcj': '𝒿', + \ 'Mck': '𝓀', + \ 'Mcl': '𝓁', + \ 'Mcm': '𝓂', + \ 'Mcn': '𝓃', + \ 'Mcp': '𝓅', + \ 'Mcq': '𝓆', + \ 'Mcr': '𝓇', + \ 'Mcs': '𝓈', + \ 'Mct': '𝓉', + \ 'Mcu': '𝓊', + \ 'Mcv': '𝓋', + \ 'Mcw': '𝓌', + \ 'Mcx': '𝓍', + \ 'Mcy': '𝓎', + \ 'Mcz': '𝓏', + \ 'MfA': '𝔄', + \ 'MfB': '𝔅', + \ 'MfD': '𝔇', + \ 'MfE': '𝔈', + \ 'MfF': '𝔉', + \ 'MfG': '𝔊', + \ 'MfJ': '𝔍', + \ 'MfK': '𝔎', + \ 'MfL': '𝔏', + \ 'MfM': '𝔐', + \ 'MfN': '𝔑', + \ 'MfO': '𝔒', + \ 'MfP': '𝔓', + \ 'MfQ': '𝔔', + \ 'MfS': '𝔖', + \ 'MfT': '𝔗', + \ 'MfU': '𝔘', + \ 'MfV': '𝔙', + \ 'MfW': '𝔚', + \ 'MfX': '𝔛', + \ 'MfY': '𝔜', + \ 'Mfa': '𝔞', + \ 'Mfb': '𝔟', + \ 'Mfc': '𝔠', + \ 'Mfd': '𝔡', + \ 'Mfe': '𝔢', + \ 'Mff': '𝔣', + \ 'Mfg': '𝔤', + \ 'Mfh': '𝔥', + \ 'Mfi': '𝔦', + \ 'Mfj': '𝔧', + \ 'Mfk': '𝔨', + \ 'Mfl': '𝔩', + \ 'Mfm': '𝔪', + \ 'Mfn': '𝔫', + \ 'Mfo': '𝔬', + \ 'Mfp': '𝔭', + \ 'Mfq': '𝔮', + \ 'Mfr': '𝔯', + \ 'Mfs': '𝔰', + \ 'Mft': '𝔱', + \ 'Mfu': '𝔲', + \ 'Mfv': '𝔳', + \ 'Mfw': '𝔴', + \ 'Mfx': '𝔵', + \ 'Mfy': '𝔶', + \ 'Mfz': '𝔷', + \}) + + " From Favonia + call extend(g:agda#default_glyphs, { + \ 'breve': '˘', + \ 'monus': '∸', + \ '<>': '⟨⟩', + \ 'greekq': ';', + \}) + + lockvar g:agda#default_glyphs +endif + +if !exists('g:agda#glyphs') + let g:agda#glyphs = deepcopy(g:agda#default_glyphs) +endif + +let &cpo = s:cpo_save diff --git a/nix/nvim-agda/agda-vim-excerpts/ftplugin.vim b/nix/nvim-agda/agda-vim-excerpts/ftplugin.vim new file mode 100644 index 0000000..1cecb72 --- /dev/null +++ b/nix/nvim-agda/agda-vim-excerpts/ftplugin.vim @@ -0,0 +1,88 @@ +let s:cpo_save = &cpo +set cpo&vim + +let b:undo_ftplugin = '' + +for [sequence, symbol] in items(g:agda#glyphs) + execute printf('noremap! %s %s', sequence, symbol) +endfor + +setlocal matchpairs&vim +setlocal matchpairs+=(:) +setlocal matchpairs+=<:> +setlocal matchpairs+=[:] +setlocal matchpairs+={:} +setlocal matchpairs+=«:» +setlocal matchpairs+=‹:› +setlocal matchpairs+=⁅:⁆ +setlocal matchpairs+=⁽:⁾ +setlocal matchpairs+=₍:₎ +setlocal matchpairs+=⌈:⌉ +setlocal matchpairs+=⌊:⌋ +setlocal matchpairs+=〈:〉 +setlocal matchpairs+=⎛:⎞ +setlocal matchpairs+=⎝:⎠ +setlocal matchpairs+=⎡:⎤ +setlocal matchpairs+=⎣:⎦ +setlocal matchpairs+=⎧:⎫ +setlocal matchpairs+=⎨:⎬ +setlocal matchpairs+=⎩:⎭ +setlocal matchpairs+=⎴:⎵ +setlocal matchpairs+=❨:❩ +setlocal matchpairs+=❪:❫ +setlocal matchpairs+=❬:❭ +setlocal matchpairs+=❮:❯ +setlocal matchpairs+=❰:❱ +setlocal matchpairs+=❲:❳ +setlocal matchpairs+=❴:❵ +setlocal matchpairs+=⟅:⟆ +setlocal matchpairs+=⟦:⟧ +setlocal matchpairs+=⟨:⟩ +setlocal matchpairs+=⟪:⟫ +setlocal matchpairs+=⦃:⦄ +setlocal matchpairs+=⦅:⦆ +setlocal matchpairs+=⦇:⦈ +setlocal matchpairs+=⦉:⦊ +setlocal matchpairs+=⦋:⦌ +setlocal matchpairs+=⦍:⦎ +setlocal matchpairs+=⦏:⦐ +setlocal matchpairs+=⦑:⦒ +setlocal matchpairs+=⦓:⦔ +setlocal matchpairs+=⦕:⦖ +setlocal matchpairs+=⦗:⦘ +setlocal matchpairs+=⸠:⸡ +setlocal matchpairs+=⸢:⸣ +setlocal matchpairs+=⸤:⸥ +setlocal matchpairs+=⸦:⸧ +setlocal matchpairs+=⸨:⸩ +setlocal matchpairs+=〈:〉 +setlocal matchpairs+=《:》 +setlocal matchpairs+=「:」 +setlocal matchpairs+=『:』 +setlocal matchpairs+=【:】 +setlocal matchpairs+=〔:〕 +setlocal matchpairs+=〖:〗 +setlocal matchpairs+=〘:〙 +setlocal matchpairs+=〚:〛 +setlocal matchpairs+=︗:︘ +setlocal matchpairs+=︵:︶ +setlocal matchpairs+=︷:︸ +setlocal matchpairs+=︹:︺ +setlocal matchpairs+=︻:︼ +setlocal matchpairs+=︽:︾ +setlocal matchpairs+=︿:﹀ +setlocal matchpairs+=﹁:﹂ +setlocal matchpairs+=﹃:﹄ +setlocal matchpairs+=﹇:﹈ +setlocal matchpairs+=﹙:﹚ +setlocal matchpairs+=﹛:﹜ +setlocal matchpairs+=﹝:﹞ +setlocal matchpairs+=（:） +setlocal matchpairs+=＜:＞ +setlocal matchpairs+=［:］ +setlocal matchpairs+=｛:｝ +setlocal matchpairs+=｟:｠ +setlocal matchpairs+=｢:｣ +let b:undo_ftplugin .= ' | setlocal matchpairs<' + +let &cpo = s:cpo_save diff --git a/nix/nvim-agda/default.nix b/nix/nvim-agda/default.nix new file mode 100644 index 0000000..eee629e --- /dev/null +++ b/nix/nvim-agda/default.nix @@ -0,0 +1,26 @@ +{ nixpkgs, system, ... }: + +let + pkgs = nixpkgs.legacyPackages.${system}; +in +pkgs.vimUtils.buildVimPlugin rec { + pname = "nvim-agda"; + version = "2bed0b9a1d42f20438d22a3229c59faaf2b6a8df"; + src = pkgs.fetchFromGitHub { + owner = "ashinkarov"; + repo = pname; + rev = version; + hash = "sha256-cMEOSGMyFHp/iABjpbxb3GFi4lBFYOhIDcI/EwgVgdw="; + }; + buildPhase = '' + for patch in ${./patches}/*; do + echo Applying $patch... + patch -p1 --verbose < $patch + done + + mkdir autoload + cp ${agda-vim-excerpts/autoload.vim} autoload/agda.vim + cat ${agda-vim-excerpts/ftplugin.vim} >> ftplugin/agda.vim + cat ${./keybinds.vim} >> ftplugin/agda.vim + ''; +} diff --git a/nix/nvim-agda/keybinds.vim b/nix/nvim-agda/keybinds.vim new file mode 100644 index 0000000..7b95d35 --- /dev/null +++ b/nix/nvim-agda/keybinds.vim @@ -0,0 +1,11 @@ +nnoremap r :AgdaLoad +nnoremap t :AgdaInfer +nnoremap q :AgdaCloseMsg +nnoremap x :AgdaCompute +nnoremap a :AgdaRefine +nnoremap A :AgdaAuto +nnoremap c :AgdaMakeCase +nmap K :AgdaTypeContext +nnoremap [g :GoalPrev +nnoremap ]g :GoalNext +nnoremap gd :AgdaWhyInscope diff --git a/nix/nvim-agda/patches/0001-remove-default-keybinds.patch b/nix/nvim-agda/patches/0001-remove-default-keybinds.patch new file mode 100644 index 0000000..b6e8d2d --- /dev/null +++ b/nix/nvim-agda/patches/0001-remove-default-keybinds.patch @@ -0,0 +1,31 @@ +diff --git a/ftplugin/agda.vim b/ftplugin/agda.vim +index f3264b5..2585b54 100644 +--- a/ftplugin/agda.vim ++++ b/ftplugin/agda.vim +@@ -39,26 +39,3 @@ command! GoalPrev :call AgdaMod.agda_goal_prev(expand("%:p")) + command! AgdaCloseMsg :call AgdaMod.close_msg_win() + command! GoalContent :call AgdaMod.gc() + command! GetEvbuf :call AgdaMod.getevbuf() +- +- +-" Key mappings +-nm l :AgdaLoad +-nm q :AgdaCloseMsg +-nm , :AgdaTypeContext +-nm u, :AgdaTypeContextNorm +-nm d :AgdaInfer +-nm r :AgdaRefine +-nm c :AgdaMakeCase +-nm n :AgdaCompute +-nm a :AgdaAuto +-nm h :AgdaHelperFun +-nm o :AgdaModuleContents +-nm w :AgdaWhyInscope +-nm e :MkPrompt +-nm ? :PrintGoals +-nm f :GoalNext +-nm b :GoalPrev +- +- +-" mappings +-runtime agda-input.vim