Require Import Coq.Numbers.DecimalString ExtrOcamlBasic ExtrOcamlString.
From stdpp Require Import strings stringmap gmap.
From mininix Require Import nix.interp.

Definition attr_set_insert (x : string) (α : attr) (αs : gmap string attr) : gmap string attr :=
  <[x:=α]> αs.

Definition attr_set_contains (x : string) (αs : gmap string attr) : bool :=
  bool_decide (x ∈ dom αs).

Definition attr_set_fold {A} (f : string → attr → A → A) (init : A) (αs : gmap string attr) : A :=
  map_fold f init αs.

Definition attr_set_empty : gmap string attr := ∅.

Definition env_fold {A} (f : string → (kind * thunk) → A → A) (init : A) (E : env) : A :=
  map_fold f init E.

Definition env_insert_abs (x : string) (t : thunk) (E : env) : env :=
  <[x:=(ABS,t)]> E.

Definition thunk_map_fold {A} (f : string → thunk → A → A) (init : A) (bs : gmap string thunk) : A :=
  map_fold f init bs.

Definition thunk_map_insert (x : string) (t : thunk) (bs : gmap string thunk) : gmap string thunk :=
  <[x:=t]> bs.

Definition thunk_map_empty : gmap string thunk := ∅.

Definition matcher := gmap string (option expr).

Definition matcher_empty : matcher := ∅.

Definition matcher_insert (x : string) (me : option expr) (ms : matcher) : matcher :=
  <[x:=me]> ms.

Definition matcher_fold {A} (f : string → option expr → A → A) (init : A) (ms : matcher) : A :=
  map_fold f init ms.

Definition env_empty : env := ∅.

Definition string_of_Z (x : Z) : string :=
  NilZero.string_of_int (Z.to_int x).

Definition string_to_Z (s : string) : option Z :=
  Z.of_int <$> NilZero.int_of_string s.

Separate Extraction
  attr_set_insert env_insert_abs matcher_insert thunk_map_insert
  attr_set_contains attr_set_fold env_fold matcher_fold thunk_map_fold
  env_empty attr_set_empty matcher_empty thunk_map_empty string_of_Z
  string_to_Z interp' forallb.