Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Coq Extaction to Emacs Lisp / Common Lisp

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.

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. *)
;; -*- 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)))))
(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)))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment