The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hi --

I'm wondering if anyone knows what could cause this bug when extracting the following code to Scheme:

Set Implicit Arguments.

Set Strict Implicit.

Record Monoid (S : Type) : Type :=

{ monoid_unit : S

}.

Class MonadWriter (T : Type) (M : Monoid T) (m : Type -> Type) : Type :=

{ tell : T -> m unit

; listen : forall {A}, m A -> m (A * T)%type

}.

Section ReaderType.

  Variable S : Type.

  Variable m : Type -> Type.

  Record readerT (t : Type) : Type := mkReaderT

  { runReaderT : S -> m t }.

  Global Instance MonadWriter_readerT T (Mon : Monoid T) (MW : MonadWriter Mon m) : MonadWriter Mon readerT :=

  { tell := fun v => mkReaderT (fun _ => tell v)

  ; listen := fun _ c => mkReaderT (fun s => listen (runReaderT c s))

  }.

End ReaderType.

Extraction Language Scheme.

Recursive Extraction MonadWriter_readerT.

Results in:

;; This extracted scheme code relies on some additional macros

;; available at http://www.pps.jussieu.fr/~letouzey/scheme

(load "macros_extr.scm")

(define __ (lambda (_) __))

(define tell (lambdas (m monadWriter)

  (match monadWriter

     ((Build_MonadWriter tell0 listen0) tell0))))

(define listen (lambdas (m monadWriter x)

  (match monadWriter

     ((Build_MonadWriter tell0 listen0) (@ listen0 __ x)))))

(define runReaderT (lambda (r) r))

(define monadWriter_readerT (lambdas (mon mW) `(Build_MonadWriter

  ,(lambdas (v x) (@ tell (error "Proj Args") mW v)) ,(lambdas (_ c s)

  (@ listen mon mW (@ runReaderT c s))))))

Note the "(error "Proj Args")" which corresponds to a bug. Does anyone know what would cause this or how to fix it?

Thank you.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/