Set Implicit Arguments.
Unset Strict Implicit.
Set Contextual Implicit.
Generalizable All Variables.

From CoqFFI Require Export Extraction.
From SimpleIO Require Import IO_Monad.
From CoqFFI Require Import Interface.

Axiom (reference : ∀ (a : Type), Type).

Extract Constant reference "'a" ⇒ "'a FreeSpecFFI.Refs.reference".

Class MonadRefs (m : Type → Type) : Type :=
  { make_ref : ∀ (a : Type), a → m (reference a)
  ; deref : ∀ (a : Type), reference a → m a
  ; assign : ∀ (a : Type), reference a → a → m unit
  }.

Axiom (io_make_ref : ∀ (a : Type), a → IO (reference a)).
Axiom (io_deref : ∀ (a : Type), reference a → IO a).
Axiom (io_assign : ∀ (a : Type), reference a → a → IO unit).

Extract Constant io_make_ref ⇒
  "(fun x0 k__ -> k__ (FreeSpecFFI.Refs.make_ref x0))".
Extract Constant io_deref ⇒
  "(fun x0 k__ -> k__ (FreeSpecFFI.Refs.deref x0))".
Extract Constant io_assign ⇒
  "(fun x0 x1 k__ -> k__ (FreeSpecFFI.Refs.assign x0 x1))".

Instance MonadRefs_IO : MonadRefs IO :=
  { make_ref := io_make_ref
  ; deref := io_deref
  ; assign := io_assign
  }.

Inductive REFS : Type → Type :=
| Make_ref : ∀ (a : Type), a → REFS (reference a)
| Deref : ∀ (a : Type), reference a → REFS a
| Assign : ∀ (a : Type), reference a → a → REFS unit.

Definition inj_make_ref `{Inject REFS m} (a : Type) (x0 : a)
  : m (reference a) :=
  inject (Make_ref x0).

Definition inj_deref `{Inject REFS m} (a : Type) (x0 : reference a) : m a :=
  inject (Deref x0).

Definition inj_assign `{Inject REFS m} (a : Type) (x0 : reference a) (x1 : a)
  : m unit :=
  inject (Assign x0 x1).

Instance MonadRefs_Inject `(Inject REFS m) : MonadRefs m :=
  { make_ref := inj_make_ref
  ; deref := inj_deref
  ; assign := inj_assign
  }.