Extracting sequences from Coq to OCaml

Using Coq
1

I’m trying to write some verified code that I’ll later extract to ocaml:

Notation " x <- e1 ;; e2" := (match e1 with
                              | SomeE x => e2
                              | NoneE err => NoneE err
                              end)
         (right associativity, at level 60) : monad_scope.
Notation " 'return' e "
  := (SomeE e) (at level 60) : monad_scope.
Notation " 'fail' s "
  := (NoneE s) (at level 60) : monad_scope.

Definition keep {Y : Type} (x : unit) (y : Y) : Y :=
  let hello := x in y.
Notation " x #; y " := (keep x y) (at level 60) : monad_scope.

Definition func (_ : unit) : optionE unit :=
    print_endline "Please enter a username (length 1-32, no spaces)" #;
    (* actually do some real computations *)
    print_endline "more printing" #;
    return tt.

I’ve written the keep function in an attempt to fix the problem I’ve been having: whenever I write

let _ := func_that_returns_unit 5 in
tt

in Coq, it is extracted to just () in OCaml, as if the extractor is attempting to optimize out a function that it perceives as “not doing anything.”

My extraction setup:

Require Extraction.
Extraction Language OCaml.
Unset Extraction Optimize.

Extract Inlined Constant keep => "(fun x y -> let _ = x in y)".

Axiom print_endline : string -> unit.
Extract Inlined Constant print_endline => "print_endline".
Recursive Extraction func.

The keep function has been working for me, although there’s some strange stream-flushing behavior going on that somehow is not solved by explicit calls to flush.

Is it possible to extract to plain OCaml sequences?

2

Stumbled across the answer by investigating coqffi and related projects:

Notation " let* '_' <= e1 #; e2 " := (match e1 with
                                    | tt => e2 
                                    end)
         (right associativity, at level 60) : monad_scope.

This generates the slightly verbose, yet functional let _ = ... in form for all of my IO needs.