diff --git a/coq-osiris/dune-project b/coq-osiris/dune-project
index 4daef42314c02b2906f51b97cf877fdb79b9ae0a..cff611792dc557808507478203d1197fef52f39f 100644
--- a/coq-osiris/dune-project
+++ b/coq-osiris/dune-project
@@ -54,6 +54,11 @@
; TODO
)
+(package
+ (name extracted)
+ ; TODO
+)
+
(package
(name osiris-interpreter)
; TODO
diff --git a/coq-osiris/extracted.opam b/coq-osiris/extracted.opam
new file mode 100644
index 0000000000000000000000000000000000000000..239eb58563e8edce9bd40754f96bb3dc27bae8aa
--- /dev/null
+++ b/coq-osiris/extracted.opam
@@ -0,0 +1,20 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+depends: [
+ "dune" {>= "3.8"}
+ "odoc" {with-doc}
+]
+build: [
+ ["dune" "subst"] {dev}
+ [
+ "dune"
+ "build"
+ "-p"
+ name
+ "-j"
+ jobs
+ "@install"
+ "@runtest" {with-test}
+ "@doc" {with-doc}
+ ]
+]
diff --git a/coq-osiris/interp/E2O.ml b/coq-osiris/interp/E2O.ml
index 0ca5d620a04874693ea2ccebbabd20e9e0f7e4bc..e4882010583f3874cd0421c6eda30e52e5174a03 100644
--- a/coq-osiris/interp/E2O.ml
+++ b/coq-osiris/interp/E2O.ml
@@ -1,8 +1,8 @@
(* Extracted modules *)
-open BinNums
-open Datatypes
-open String
-open Ascii
+open Extracted.BinNums
+open Extracted.Datatypes
+open Extracted.String
+open Extracted.Ascii
(* OCaml's standard library *)
open Stdlib
@@ -37,7 +37,7 @@ let string s =
(** Syntax types *)
module O = Translatorlib.Syntax
-module E = Syntax
+module E = Extracted.Syntax
let var = string
let name = string
diff --git a/coq-osiris/interp/E2O.mli b/coq-osiris/interp/E2O.mli
index 1a3a0083de40302a6ef98927eaeb6fa74d394815..ac0230d852af2b82fe4667810a494b7aaf057434 100644
--- a/coq-osiris/interp/E2O.mli
+++ b/coq-osiris/interp/E2O.mli
@@ -1,5 +1,5 @@
-open BinNums
-open Datatypes
+open Extracted.BinNums
+open Extracted.Datatypes
(** Conversions from extracted (E) to manually-defined-in-OCaml types (O) *)
@@ -16,10 +16,10 @@ val z : coq_Z -> int
val nat : nat -> int
val list : ('a -> 'b) -> 'a list -> 'b Stdlib.List.t
val prod : ('a1 -> 'b1) -> ('a2 -> 'b2) -> ('a1 * 'a2) -> ('b1 * 'b2)
-val string : String.string -> Stdlib.String.t
+val string : Extracted.String.string -> Stdlib.String.t
module O = Translatorlib.Syntax
-module E = Syntax (* from syntax.ml, extracted from syntax.v *)
+module E = Extracted.Syntax (* from syntax.ml, extracted from syntax.v *)
(* Enumeration of [val ty : E.ty -> O.ty] for each syntax type [ty] *)
diff --git a/coq-osiris/interp/O2E.ml b/coq-osiris/interp/O2E.ml
index 8e70f3ff24c07e08b745426a08c214922fa5e43d..1bf8bbec886e291d8fdcede0dca1793b2d58f34d 100644
--- a/coq-osiris/interp/O2E.ml
+++ b/coq-osiris/interp/O2E.ml
@@ -1,8 +1,8 @@
(* Extracted modules *)
-open BinNums
-open Datatypes
-open String
-open Ascii
+open Extracted.BinNums
+open Extracted.Datatypes
+open Extracted.String
+open Extracted.Ascii
(* OCaml's standard library *)
open Stdlib
@@ -35,7 +35,7 @@ let string s = String.fold_right (fun c a -> String (char c, a)) s EmptyString
(** Syntax types *)
module O = Translatorlib.Syntax
-module E = Syntax
+module E = Extracted.Syntax
let var = string
let name = string
@@ -142,7 +142,7 @@ and rec_binding : O.rec_binding -> E.rec_binding = function
and anonfun : O.anonfun -> E.anonfun = function
| AnonFun (v, e) -> AnonFun (var v, expr e)
- | AnonFunction bs -> Sugar.coq_AnonFunction (branches bs)
+ | AnonFunction bs -> Extracted.Sugar.coq_AnonFunction (branches bs)
and mexpr : O.mexpr -> E.mexpr = function
| MUnsupported -> MUnsupported
diff --git a/coq-osiris/interp/O2E.mli b/coq-osiris/interp/O2E.mli
index fc3b1981ad225b1be6df266540b1ae478293a91d..39be338956489d4875b571501d056e9cf1d271ca 100644
--- a/coq-osiris/interp/O2E.mli
+++ b/coq-osiris/interp/O2E.mli
@@ -1,5 +1,5 @@
-open BinNums
-open Datatypes
+open Extracted.BinNums
+open Extracted.Datatypes
(** Conversions from manually-defined-in-OCaml (O) to extracted types (E) *)
@@ -8,10 +8,10 @@ open Datatypes
val z : int -> coq_Z
val nat : int -> nat
val list : ('a -> 'b) -> 'a Stdlib.List.t -> 'b list
-val string : Stdlib.String.t -> String.string
+val string : Stdlib.String.t -> Extracted.String.string
module O = Translatorlib.Syntax
-module E = Syntax
+module E = Extracted.Syntax
(* [val ty : O.ty -> E.ty] *)
diff --git a/coq-osiris/interp/dune b/coq-osiris/interp/dune
index 0cc633647e1f640c5657be0929170cac6f9be426..69bda960af59c35589005b0e22c619c6e18bdff6 100644
--- a/coq-osiris/interp/dune
+++ b/coq-osiris/interp/dune
@@ -4,17 +4,5 @@
(name interp)
; TODO make flags more specific, e.g. to extracted code or conversion modules
(flags :standard "-w" "A-40-41-42-44-45")
- (libraries translatorlib)
-)
-
-(coq.extraction
- (prelude extract)
- (theories stdpp iris Ltac2 osiris Equations)
- (extracted_modules
- Datatypes Specif Decimal Basics Bool Orders List base BinNums BinPosDef
- BinPos BinNat Ascii BinInt ZArith_dec String Zpower option numbers list0
- countable void infinite fin_sets fin_maps mapset gmap locations PrimFloat
- Coqlib Zbits Integers int syntax sugar outcome code Mergesort options
- eval_strat eval step DecimalString Externals oStdlib run
- )
+ (libraries translatorlib extracted)
)
diff --git a/coq-osiris/interp/extracted/dune b/coq-osiris/interp/extracted/dune
new file mode 100644
index 0000000000000000000000000000000000000000..cb92c4ca2ab17919b798cad953092bc9175e77df
--- /dev/null
+++ b/coq-osiris/interp/extracted/dune
@@ -0,0 +1,17 @@
+(library
+ (package extracted)
+ (name extracted)
+ (flags :standard "-w" "A-40-41-42-44-45")
+)
+
+(coq.extraction
+ (prelude extract)
+ (theories stdpp iris Ltac2 osiris Equations)
+ (extracted_modules
+ Datatypes Specif Decimal Basics Bool Orders List base BinNums BinPosDef
+ BinPos BinNat Ascii BinInt ZArith_dec String Zpower option numbers list0
+ countable void infinite fin_sets fin_maps mapset gmap locations PrimFloat
+ Coqlib Zbits Integers int syntax sugar outcome code Mergesort options
+ eval_strat eval step DecimalString Externals oStdlib run
+ )
+)
diff --git a/coq-osiris/interp/extract.v b/coq-osiris/interp/extracted/extract.v
similarity index 100%
rename from coq-osiris/interp/extract.v
rename to coq-osiris/interp/extracted/extract.v
diff --git a/coq-osiris/interp/remove_generated_ml_files.sh b/coq-osiris/interp/extracted/remove_generated_ml_files.sh
similarity index 100%
rename from coq-osiris/interp/remove_generated_ml_files.sh
rename to coq-osiris/interp/extracted/remove_generated_ml_files.sh
diff --git a/coq-osiris/interp/interp.ml b/coq-osiris/interp/interp.ml
index 3c2452a309254ac510c5bde4a6d00d95d0d0f019..9b67eed8d6629cde2673eb816a445ecf5572003f 100644
--- a/coq-osiris/interp/interp.ml
+++ b/coq-osiris/interp/interp.ml
@@ -1,8 +1,8 @@
open Printf
(* Extracted modules *)
-open Syntax
-open Run
+open Extracted.Syntax
+open Extracted.Run
(* OCaml's stdlib; shadows some extracted modules such as List and String *)
open Stdlib
@@ -212,18 +212,18 @@ let () =
Translate.unit (Some filename) typedtree.structure in
if !show_ast then
fprintf stdout "Typed tree:\n%s\n\n" (Translatorlib.Syntax.show_mexpr mexpr);
- let mexpr : Syntax.mexpr = O2E.mexpr mexpr in
+ let mexpr : Extracted.Syntax.mexpr = O2E.mexpr mexpr in
flush_all ();
(* Choose evaluation options between "default" and "careful" *)
- let opt = if !noorder then Options.careful_eval_options
- else Options.default_eval_options in
+ let opt = if !noorder then Extracted.Options.careful_eval_options
+ else Extracted.Options.default_eval_options in
(* Make [mexpr] into a configuration (store, micro) *)
let env = io_env @ effect_stdlib_env in
let store = io_store in
- let config = (store, Eval_strat.eval_mexpr opt env mexpr) in
+ let config = (store, Extracted.Eval_strat.eval_mexpr opt env mexpr) in
if !detcheck then
match determinism_check opt config with
diff --git a/osiris/src/Dune.ml b/osiris/src/Dune.ml
index 98a9650493de43c4b9006250d7d6ad78c4d0cd65..a6ec8750cf04a8730d9f1984e3c49b633f0ae112 100644
--- a/osiris/src/Dune.ml
+++ b/osiris/src/Dune.ml
@@ -51,8 +51,8 @@ let rec extract_module_descriptions (e : Base.Sexp.t) accu =
| List (Atom "executables" :: [List (List (Atom "names" :: [List [Atom "interp"]]) :: _)]) ->
Printf.fprintf stderr "Warning: extract_module_descriptions: skipping S-expression (executables ((names (interp)) ...))\n";
accu
- | List [Atom "library"; List (List [Atom "name"; Atom "translatorlib"] :: _)] ->
- Printf.fprintf stderr "Warning: extract_module_descriptions: skipping S-expression (library ((name translatorlib) ...))\n";
+ | List [Atom "library"; List (List [Atom "name"; Atom ("translatorlib" | "extracted" as name)] :: _)] ->
+ Printf.fprintf stderr "Warning: extract_module_descriptions: skipping S-expression (library ((name %s) ...))\n" name;
accu
| _ ->
match [%of_sexp: module_description] e with