Coq Extaction to Emacs Lisp / Common Lisp

readme.md

Coq Extraction to Emacs Lisp/Common Lisp

Or Coq Extraction to Scheme also loadable as Emacs Lisp or Common Lisp programs.

Requirement

• Coq 8.4pl3
• Emacs 24 or later (for lexical-binding)
• An ANSI Common Lisp implementation.

How to use

Apply the patch to Coq-8.4pl3

% patch -p1 < coq-8.4pl3-elisp.diff

Build and install patched Coq.

Extract functions into Scheme.

Extraction Language Scheme.
Extraction ...

Load auxiliary definitions macros_extr.scm.el for emacs, or macros_extr.scm.lisp for common lisp, then your implementation is ready to load extracted files.

coq-8.4pl3-elisp.diff

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 7915bc8..ee2b3fb 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -23,14 +23,15 @@ open Common
 let keywords =
   List.fold_right (fun s -> Idset.add (id_of_string s))
     [ "define"; "let"; "lambda"; "lambdas"; "match";
-      "apply"; "car"; "cdr";
+      "apply"; "car"; "cdr"; "list"; "letrec";
       "error"; "delay"; "force"; "_"; "__"]
     Idset.empty
 
 let preamble _ _ usf =
+  str ";; -*- lexical-binding: t -*-\n" ++
   str ";; This extracted scheme code relies on some additional macros\n" ++
   str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
-  str "(load \"macros_extr.scm\")\n\n" ++
+  str ";; (load \"macros_extr.scm\")\n\n" ++
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id =
@@ -44,13 +45,11 @@ let paren = pp_par true
 
 let pp_abst st = function
   | [] -> assert false
-  | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
   | l -> paren
 	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
 
 let pp_apply st _ = function
   | [] -> st
-  | [a] -> hov 2 (paren (st ++ spc () ++ a))
   | args -> hov 2 (paren (str "@ " ++ st ++
 			  (prlist_strict (fun x -> spc () ++ x) args)))
 
@@ -88,8 +87,7 @@ let rec pp_expr env args =
     | MLcons (_,r,args') ->
 	assert (args=[]);
 	let st =
-	  str "`" ++
-	  paren (pp_global Cons r ++
+	  paren (str "list ':" ++ pp_global Cons r ++
 		 (if args' = [] then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
@@ -128,10 +126,10 @@ let rec pp_expr env args =
 
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->
-      paren (pp_global Cons r ++
+      paren (str ":" ++ pp_global Cons r ++
 	     (if args = [] then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
-  | e -> str "," ++ pp_expr env [] e
+  | e -> pp_expr env [] e
 
 and pp_one_pat env (ids,p,t) =
   let r = match p with
@@ -149,7 +147,7 @@ and pp_one_pat env (ids,p,t) =
 and pp_pat env pv =
   prvect_with_sep fnl
     (fun x -> let s1,s2 = pp_one_pat env x in
-     hov 2 (str "((" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv
+     hov 2 (str "((:" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)

macros_extr.scm.el

;; -*- lexical-binding: t -*-
(require 'cl-lib)

(defmacro define (v expr)
  `(progn
     (defvar ,v)
     (internal-make-var-non-special ',v)
     (setq ,v ,expr)))

(defmacro @ (f &rest args)
  "funcall for curried functions"
  (cl-reduce (lambda (acc x)
               `(funcall ,acc ,x))
             args
             :initial-value f))

(defmacro lambdas (args body)
  "curried lambda"
  (declare (indent 1))
  (cl-reduce (lambda (arg acc)
               `(lambda (,arg) ,acc))
             args
             :initial-value body
             :from-end t))

(cl-defstruct promise
  thunk evaluated-p value)

(defmacro delay (expr)
  `(make-promise :thunk (lambda () ,expr)))

(defun force (promise)
  (if (promise-evaluated-p promise)
      (promise-value promise)
    (let ((v (funcall (promise-thunk promise))))
      (setf (promise-value promise) v)
      (setf (promise-evaluated-p promise) t)
      v)))

(defmacro match (expr &rest clauses)
  (declare (indent 1))
  `(pcase ,expr
     ,@(cl-loop for (tag&args body) in clauses
                collect (let ((tag (car tag&args))
                              (args (cdr tag&args)))
                          `((,backquote-backquote-symbol
                             (,tag
                              ,@(mapcar (lambda (arg)
                                          `(,backquote-unquote-symbol ,arg))
                                        args)))
                            ,body)))))

macros_extr.scm.lisp

(defmacro define (v expr)
  (let ((backing-var (intern (format nil "*define-backing-var-for ~A*"
                                     (symbol-name v))
                             (symbol-package v))))
    `(progn
       (defvar ,backing-var)
       (define-symbol-macro ,v ,backing-var)
       (setq ,backing-var ,expr))))

(defmacro @ (f &rest args)
  "funcall for curried functions"
  (reduce (lambda (acc x)
            `(funcall ,acc ,x))
          args
          :initial-value f))

(defmacro lambdas (args body)
  "curried lambda"
  (reduce (lambda (arg acc)
               `(lambda (,arg) ,acc))
             args
             :initial-value body
             :from-end t))

(defstruct promise
  thunk
  evaluated-p
  value)

(defmacro delay (expr)
  `(make-promise :thunk (lambda () ,expr)))

(defun force (promise)
  (if (promise-evaluated-p promise)
      (promise-value promise)
      (let ((v (funcall (promise-thunk promise))))
        (setf (promise-value promise) v)
        (setf (promise-evaluated-p promise) t)
        v)))

(defmacro letrec (binds &rest body)
  `(let (,@(mapcar #'car binds))
     ,@(mapcar (lambda (bind) `(setq ,@bind)) binds)
     ,@body))

(defmacro match (expr &rest clauses)
  (let ((v (gensym)))
    `(let ((,v ,expr))
       (cond ,@(loop for ((c . args) . body) in clauses
                     collect `((eq (car ,v) ,c)
                               (destructuring-bind ,args (cdr ,v)
                                 ,@body)))))))