The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

Dear Yevgeniy,

Extraction from classical proofs is currently not a feature of the Coq
extraction, unlike for example in Minlog (www.minlog-system.de). An
obvious reason for this is that Coq extraction only consider objects in
Set (or more recently Type) universes, and adding any form of classical
axioms in Set was immediatly leading to inconsistency before Coq 8.0, as
explained by Hugo in his mail.

Nonetheless, as Hugo explained in his mail, it is now possible to play
with classical axioms + call/cc + extraction in Scheme.

But please keep in mind that the extraction to Scheme is higly experimental
and not as finished and tested as the extraction to Ocaml:

* In particular I've fixed last november in Coq CVS a bug about some
arguments of function being lost during printing of the extracted terms.
The last stable Coq version (8.0..) still suffer from this problem.

* Today, when tring Hugo's example, I've discovered that the Extract
Constant mechanism (replacing an axiom by some manually given code) is
currently broken for the extraction to Scheme. I will fix that, but in the
meantime, you need to do the substitution manually in the extracted file.

* The Extraction to Scheme may produce illegal names (like n') because I
haven't fully implemented yet the scheme syntactic convention for names.
Lowercase and uppercase clashes (n and N) will also raise difficulties.


On Mon, 21 Feb 2005, Hugo Herbelin wrote:

>
>   Extraction to Scheme uses non-standard macros such as "match-case"
> (reminiscent of bigloo?) and many others strange things. I couldn't
> find a scheme dialect that can interpret the extracted files as such.
>

Indeed, the extraction needs a "match" operator. My advise is to use the
one coming natively with bigloo. Otherwise, I've got some macros
implementing this match-case for other dialects. But then you should
remove manually all the "?" characters in the extracted files.

Please recontact me if you have question concerning this (tricky)
extraction to Scheme...

Pierre Letouzey



Macros for running extracted scheme code with bigloo:
---------------------------------------------------------------------------
;;;;;; Extraction from Coq to Bigloo: Init file

;; because of fixed arity, we always use unary lambda
;; (lambdas (a b) c) ==> (lambda (a) (lambda (b) c))

(define-macro (lambdas a c)
  (if (null? a)
      c
      `(lambda (,(car a)) (lambdas ,(cdr a) ,c))))

;; hence all applications should be unary: ((f x) y)
;; to remove some parenthesis, we introduce a macro: (@ f x y) = ((f x) y)

(define-syntax @
   (syntax-rules  ()
      ((@ f) (f))
      ((@ f x) (f x))
      ((@ f x . l) (@ (f x) . l))))

;; we can see absurd cases as errors:

(define (absurd) (error "extraction" "absurd case occurred..." ""))
---------------------------------------------------------------------------



Macros for r5rs-compliant dialect of scheme:
--------------------------------------------------------------------------
;;;;;; Extraction from Coq to regular (R5RS) scheme: Init file

;; because of fixed arity, we always use unary lambda
;; (lambdas (a b) c) ==> (lambda (a) (lambda (b) c))

(define-syntax lambdas (syntax-rules ()
        ((lambdas () c) c)
        ((lambdas (a b ...) c) (lambda (a) (lambdas (b ...) c)))))

;; hence all applications should be unary: ((f x) y)
;; to remove some parenthesis, we introduce a macro: (@ f x y) = ((f x) y)

(define-syntax @
   (syntax-rules  ()
      ((@ f) (f))
      ((@ f x) (f x))
      ((@ f x . l) (@ (f x) . l))))

;; (limited) encoding of pattern matching in the bigloo style
;; but without ? in the patterns:
;; Example: predecessor should be written
;;    (define (pred n)
;;       (match-case n
;;          ((O) '(O))
;;          ((S n) n)))

(define-syntax !match-aux (syntax-rules ()
        ((match-aux c a ((constr . args) u))
         (if (eq? c 'constr)
             (apply (lambda args u) a)))
        ((match-aux c a ((constr . args) u) clauses ...)
         (if (eq? c 'constr)
             (apply (lambda args u) a)
             (!match-aux c a clauses ...)))))

(define-syntax match-case (syntax-rules ()
        ((match c clauses ...)
         (let* ((val c)
               (hd (car val))
               (tl (cdr val)))
           (!match-aux hd tl clauses ...)))))

;; we can see absurd cases as errors:

(define escape "undefined")
(call-with-current-continuation (lambda (c) (set! escape c)))

(define (absurd)
  (escape (begin
            (display "Error: absurd case occurred...")
            (newline))))

;; or just simply ignore them...

;(define (absurd) (begin))

;;;;;;;;; end of macros;;;;;;;
--------------------------------------------------------------------------