Library heap

From FreeSpec.Core Require Import Core Extraction.
From FreeSpec.FFI Require Import FFI Refs.
From FreeSpec.Exec Require Import Exec.

From Coq Require Import String.

Open Scope nat_scope.

Definition with_heap `{Monad m, MonadRefs m} : m string :=
  let× ptr := make_ref 2 in
  assign ptr 3;;
  let× x := deref ptr in
  if Nat.eqb x 2
  then pure "yes!"
  else pure "no!".

Definition with_heap_impure `{Provide ix REFS} : impure ix string :=
  with_heap.

Exec with_heap_impure.