1 files changed, 52 insertions, 0 deletions

diff --git a/lib/extraction/prelude.v b/lib/extraction/prelude.v
new file mode 100644
index 0000000..ef35bcb
--- /dev/null
+++ b/lib/extraction/prelude.v
@@ -0,0 +1,52 @@
+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.