# Extracting sequences from Coq to OCaml

**URL:** https://discourse.rocq-prover.org/t/extracting-sequences-from-coq-to-ocaml/2431
**Category:** Using Rocq
**Created:** [September 20, 2024, 9:54pm UTC](https://discourse.rocq-prover.org/t/extracting-sequences-from-coq-to-ocaml/2431 "2024-09-20T21:54:00Z")
**Posts on this page:** 2
**Page:** 1

<div class="post-metadata">

### Author: ![caverill](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/caverill/32/832_2.png) [@caverill](https://discourse.rocq-prover.org/u/caverill)
#### Post date: [September 20, 2024, 9:54pm UTC](https://discourse.rocq-prover.org/t/extracting-sequences-from-coq-to-ocaml/2431/1 "2024-09-20T21:54:00Z")

</div>

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

```auto
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

```auto
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:

```auto
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?

---

<div class="post-metadata">

### Author: ![caverill](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/caverill/32/832_2.png) [@caverill](https://discourse.rocq-prover.org/u/caverill)
#### Post date: [September 21, 2024, 6:14am UTC](https://discourse.rocq-prover.org/t/extracting-sequences-from-coq-to-ocaml/2431/2 "2024-09-21T06:14:04Z")

</div>

Stumbled across the answer by investigating [coqffi](https://github.com/coq-community/coqffi/blob/main/examples/bin/extract.v) and related projects:

```auto
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.