3 files changed, 126 insertions, 0 deletions

diff --git a/lib/extraction/dune b/lib/extraction/dune
new file mode 100644
index 0000000..b56caf9
--- /dev/null
+++ b/lib/extraction/dune
@@ -0,0 +1,56 @@
+(coq.extraction
+ (prelude prelude)
+ (extracted_modules
+  Ascii
+  BinInt
+  Bits
+  Decimal
+  prelude
+  gmap
+  Nat
+  PeanoNat
+  SpecFloat
+  ZArith_dec
+  base
+  BinNat
+  Bool
+  DecimalString
+  interp
+  numbers
+  pretty
+  Specif
+  Zbool
+  Basics
+  BinNums
+  countable
+  list0
+  operational
+  res
+  String
+  Zpower
+  Binary
+  BinPosDef
+  Datatypes
+  fin_maps
+  List
+  option
+  Round
+  strings
+  BinarySingleNaN
+  BinPos
+  decidable
+  floats
+  mapset
+  orders
+  sorting
+  utils)
+ (flags
+  (-output-directory "."))
+ (theories Flocq stdpp mininix))
+
+(library
+ (name extraction)
+ (flags
+  (:standard -w -33))
+ (instrumentation
+  (backend bisect_ppx)))
diff --git a/lib/extraction/extraction.ml b/lib/extraction/extraction.ml
new file mode 100644
index 0000000..a737700
--- /dev/null
+++ b/lib/extraction/extraction.ml
@@ -0,0 +1,18 @@
+include Prelude
+include Interp
+include Operational
+include Res
+
+(* Stuff that's not part of the paper. Still exposed because we sometimes want
+   to be able to create a natural number, float, process a list etc. *)
+module Internal = struct
+  module BinNums = BinNums
+  module Datatypes = Datatypes
+  module List = List
+
+  module Floats = struct
+    include Floats
+    include Binary
+    include SpecFloat
+  end
+end
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.