Add Nix files + README
This commit is contained in:
parent
c06439c971
commit
b2e58c1704
GPG Key ID:
BDA47A31A3C8EE6B
|
|
@ -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/
|
||||
|
||||
|
|
@ -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
|
||||
}
|
||||
|
|
@ -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
|
||||
];
|
||||
};
|
||||
});
|
||||
}
|
||||
10
main.tex
10
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?}
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,4 @@
|
|||
{ nixpkgs, system, ... }:
|
||||
|
||||
let pkgs = nixpkgs.legacyPackages.${system};
|
||||
in pkgs.agda.withPackages (p: [ p.standard-library ])
|
||||
|
|
@ -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 <C-n> :NERDTreeToggle<CR>
|
||||
imap kj <Esc>
|
||||
'';
|
||||
};
|
||||
}
|
||||
|
|
@ -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.
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
autoload.vim and ftplugin.vim are mostly taken from
|
||||
https://github.com/derekelkins/agda-vim, with slight modification.
|
||||
|
|
@ -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': '⟦⟧<left>',
|
||||
\ 'diamond': '◇',
|
||||
\ 'dots': '…',
|
||||
\ 'down': '↓',
|
||||
\ 'downtri': '▼',
|
||||
\ 'Down': '⇓',
|
||||
\ 'dunion': '⊎',
|
||||
\ 'du': '⊎',
|
||||
\ 'ell': 'ℓ',
|
||||
\ 'empty': '∅',
|
||||
\ 'equiv': '≡',
|
||||
\ 'eq': '≡',
|
||||
\ 'eventually': '◇',
|
||||
\ 'exists': '∃',
|
||||
\ 'flat': '♭',
|
||||
\ 'fold': '⦇⦈<left>',
|
||||
\ '(\|': '⦇',
|
||||
\ '\|)': '⦈',
|
||||
\ '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': '⌊⌋<left>',
|
||||
\ 'floor': '⌊⌋<left>',
|
||||
\ 'llangle': '⟪',
|
||||
\ 'longto': '⟶ ',
|
||||
\ '--': '⟶ ',
|
||||
\ '–': '⟶ ',
|
||||
\ 'lor': '∨',
|
||||
\ 'lower': '⌈⌉<left>',
|
||||
\ 'ceil': '⌈⌉<left>',
|
||||
\ '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': '⟨⟩<left>',
|
||||
\ 'up': '↑',
|
||||
\ 'updown': '↕',
|
||||
\ 'ud': '↕',
|
||||
\ 'unfold': '⦉⦊<left>',
|
||||
\ '<\|': '⦉',
|
||||
\ '\|>': '⦊',
|
||||
\ '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': '∸',
|
||||
\ '<>': '⟨⟩<left>',
|
||||
\ '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
|
||||
|
|
@ -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! <buffer> <LocalLeader>%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
|
||||
|
|
@ -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
|
||||
'';
|
||||
}
|
||||
|
|
@ -0,0 +1,11 @@
|
|||
nnoremap <buffer> <LocalLeader>r :<c-u>AgdaLoad<cr>
|
||||
nnoremap <buffer> <LocalLeader>t :<c-u>AgdaInfer<cr>
|
||||
nnoremap <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
|
||||
nnoremap <buffer> <LocalLeader>x :<c-u>AgdaCompute<cr>
|
||||
nnoremap <buffer> <LocalLeader>a :<c-u>AgdaRefine<cr>
|
||||
nnoremap <buffer> <LocalLeader>A :<c-u>AgdaAuto<cr>
|
||||
nnoremap <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
|
||||
nmap <buffer> K :<c-u>AgdaTypeContext<cr>
|
||||
nnoremap <buffer> [g :<c-u>GoalPrev<cr>
|
||||
nnoremap <buffer> ]g :<c-u>GoalNext<cr>
|
||||
nnoremap <buffer> gd :<c-u>AgdaWhyInscope<cr>
|
||||
|
|
@ -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 <buffer> <LocalLeader>l :<c-u>AgdaLoad<cr>
|
||||
-nm <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
|
||||
-nm <buffer> <LocalLeader>, :<c-u>AgdaTypeContext<cr>
|
||||
-nm <buffer> <LocalLeader>u, :<c-u>AgdaTypeContextNorm<cr>
|
||||
-nm <buffer> <LocalLeader>d :<c-u>AgdaInfer<cr>
|
||||
-nm <buffer> <LocalLeader>r :<c-u>AgdaRefine<cr>
|
||||
-nm <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
|
||||
-nm <buffer> <LocalLeader>n :<c-u>AgdaCompute<cr>
|
||||
-nm <buffer> <LocalLeader>a :<c-u>AgdaAuto<cr>
|
||||
-nm <buffer> <LocalLeader>h :<c-u>AgdaHelperFun<cr>
|
||||
-nm <buffer> <LocalLeader>o :<c-u>AgdaModuleContents<cr>
|
||||
-nm <buffer> <LocalLeader>w :<c-u>AgdaWhyInscope<cr>
|
||||
-nm <buffer> <LocalLeader>e :<c-u>MkPrompt<cr>
|
||||
-nm <buffer> <LocalLeader>? :<c-u>PrintGoals<cr>
|
||||
-nm <buffer> <LocalLeader>f :<c-u>GoalNext<cr>
|
||||
-nm <buffer> <LocalLeader>b :<c-u>GoalPrev<cr>
|
||||
-
|
||||
-
|
||||
-" mappings
|
||||
-runtime agda-input.vim
|
||||
Loading…
Reference in New Issue