This file is to be placed alongside the extracted file, or at least somewhere your Scheme will look into when doing a (load ...). It only includes R5RS-style macros, so it should be compatible with any decent Scheme implementation. Tested so far: bigloo, mzscheme, petite, scheme48, guile.
Nota: In the case of bigloo, you could use instead: macros_extr_bigloo.scm.
This version is much faster, since it takes advantage of bigloo's native pattern matching
construct. Just rename this file into macros_extr.scm.
Nota2: In the case of guile, you should first force the support of R5RS macros via
(use-modules (ice-9 syncase))
Nota3: In the case of scheme48, you should provide an error function, even a dummy one, for instance via (define error). Moreover, it seems that you should load every file explicitely, instead of expecting your extracted file to load macros_extr.scm.
Because of Scheme fixed arity, we should always use unary lambda in order to allow partial application. This can easily be done using a lambdas macro:
(lambdas (a b) c) ==> (lambda (a) (lambda (b) c))
Conversely, all applications should be unary: ((f x) y). To remove some parenthesis, we introduce another macro:
(@ f x y) ==> ((f x) y)
The last needed feature is inductive objects and pattern matching. We encode inductive objects as lists whose first element is the constructor, followed by the remaining arguments. For instance, Coq notation for three in unary numbers translates to:
'(S (S (O)))
Concerning pattern matching, the ones produced by the extraction are really basic: one branch per constructor, and all patterns are made of a constructor followed by variables. We reuse a syntax inspired from Bigloo match-case construct, but without ? in the patterns, in order to have an easy R5RS-style macro for this.
For example, the predecessor should be written:
(define (pred n)
(match n
((O) '(O))
((S n) n)))