max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: lean4-mode: avoid cl

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-10 18:10:06 +01:00
parent 31d5f9fa51
commit 64bfd803fe
1 changed files with 21 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
lean4-mode/lean4-input.el
View file

@ -1,3 +1,4 @@
;;; -*- lexical-binding: t -*-
;;; lean4-input.el --- The Lean input method (based/copied from Agda)
;;;
;;; DISCLAIMER: This file is based on agda-input.el provided with the Agda language.
@ -22,6 +23,7 @@
;;; Code:
(require 'quail)
(require 'cl-lib)
;; Quail is quite stateful, so be careful when editing this code. Note
;; that with-temp-buffer is used below whenever buffer-local state is
@ -53,17 +55,13 @@ removing all space and newline characters."
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Functions used to tweak translation pairs
;; lexical-let is used since Elisp lacks lexical scoping.
(defun lean4-input-compose (f g)
"\x -> concatMap F (G x)"
(lexical-let ((f1 f) (g1 g))
(lambda (x) (lean4-input-concat-map f1 (funcall g1 x)))))
(lambda (x) (lean4-input-concat-map f (funcall g x))))
(defun lean4-input-or (f g)
"\x -> F x ++ G x"
(lexical-let ((f1 f) (g1 g))
(lambda (x) (append (funcall f1 x) (funcall g1 x)))))
(lambda (x) (append (funcall f x) (funcall g x))))
(defun lean4-input-nonempty ()
"Only keep pairs with a non-empty first component."
@ -71,42 +69,36 @@ removing all space and newline characters."
(defun lean4-input-prepend (prefix)
"Prepend PREFIX to all key sequences."
(lexical-let ((prefix1 prefix))
(lambda (x) `((,(concat prefix1 (car x)) . ,(cdr x))))))
(lambda (x) `((,(concat prefix (car x)) . ,(cdr x)))))
(defun lean4-input-prefix (prefix)
"Only keep pairs whose key sequence starts with PREFIX."
(lexical-let ((prefix1 prefix))
(lambda (x)
(if (equal (substring (car x) 0 (length prefix1)) prefix1)
(list x)))))
(lambda (x)
(if (equal (substring (car x) 0 (length prefix)) prefix)
(list x))))
(defun lean4-input-suffix (suffix)
"Only keep pairs whose key sequence ends with SUFFIX."
(lexical-let ((suffix1 suffix))
(lambda (x)
(if (equal (substring (car x)
(- (length (car x)) (length suffix1)))
suffix1)
(list x)))))
(lambda (x)
(if (equal (substring (car x)
(- (length (car x)) (length suffix)))
suffix)
(list x))))
(defun lean4-input-drop (ss)
"Drop pairs matching one of the given key sequences.
SS should be a list of strings."
(lexical-let ((ss1 ss))
(lambda (x) (unless (member (car x) ss1) (list x)))))
(lambda (x) (unless (member (car x) ss) (list x))))
(defun lean4-input-drop-beginning (n)
"Drop N characters from the beginning of each key sequence."
(lexical-let ((n1 n))
(lambda (x) `((,(substring (car x) n1) . ,(cdr x))))))
(lambda (x) `((,(substring (car x) n) . ,(cdr x)))))
(defun lean4-input-drop-end (n)
"Drop N characters from the end of each key sequence."
(lexical-let ((n1 n))
(lambda (x)
`((,(substring (car x) 0 (- (length (car x)) n1)) .
,(cdr x))))))
(lambda (x)
`((,(substring (car x) 0 (- (length (car x)) n)) .
,(cdr x)))))
(defun lean4-input-drop-prefix (prefix)
"Only keep pairs whose key sequence starts with PREFIX.
@ -118,10 +110,9 @@ This prefix is dropped."
(defun lean4-input-drop-suffix (suffix)
"Only keep pairs whose key sequence ends with SUFFIX.
This suffix is dropped."
(lexical-let ((suffix1 suffix))
(lean4-input-compose
(lean4-input-drop-end (length suffix1))
(lean4-input-suffix suffix1))))
(lean4-input-compose
(lean4-input-drop-end (length suffix))
(lean4-input-suffix suffix)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Customization