Reorder cstrs and unique ffi (#30)

* Adapt to latest MetaCoq erasure integrating reordering of constructors

* Simplify build, removing malfunction_ffi

* Use MetaCoq's git version for testing for now

* Ensure that mapping of bool is done by extractions and update README to document Extract Inductive command

* Fix test-suite

* Fix PrintMli metaprogram to not print type declarations for bool and unit

* Fix test output

.github/workflows/main.yml

@@ -33,6 +33,7 @@ jobs:
               sudo chown -R coq:coq .
             endGroup
             startGroup "opam pin"
+              opam pin -n -y "https://github.com/MetaCoq/metacoq.git#coq-8.19"
               opam pin -n -y "https://github.com/stedolan/malfunction.git#master"
             endGroup
             startGroup "install dependencies for benchmarks"

Makefile

@@ -1,7 +1,4 @@
-all: coq extraction_plugin extraction_ocaml_ffi extraction_malfunction_ffi plugin bootstrap
-
-extraction_malfunction_ffi:
-	cd lib/coq_verified_extraction_malfunction_ffi && dune build
+all: coq extraction_plugin extraction_ocaml_ffi plugin bootstrap
 
 extraction_ocaml_ffi:
 	cd lib/coq_verified_extraction_ocaml_ffi && dune build
@@ -19,7 +16,6 @@ install: install-coq plugin
 
 install-coq: Makefile.coq coq
 	+make -f Makefile.coq install
-	cd lib/coq_verified_extraction_malfunction_ffi && dune install
 	cd lib/coq_verified_extraction_ocaml_ffi && dune install
 	cd lib/coq_verified_extraction_plugin && dune install
 	cd plugin/plugin && make -f Makefile.coq install
@@ -29,7 +25,6 @@ clean: Makefile.coq plugin/plugin/Makefile.coq plugin/plugin-bootstrap/Makefile.
 	+make -f Makefile.coq clean
 	rm -f Makefile.coq
 	rm -f Makefile.coq.conf
-	cd lib/coq_verified_extraction_malfunction_ffi && dune clean
 	cd lib/coq_verified_extraction_ocaml_ffi && dune clean
 	cd lib/coq_verified_extraction_plugin && dune clean
 	cd plugin/plugin && make clean
@@ -51,7 +46,7 @@ Makefile.coq: _CoqProject
 plugin/plugin-bootstrap/Makefile.coq: plugin/plugin-bootstrap/_CoqProject
 	cd plugin/plugin-bootstrap && make Makefile.coq
 
-bootstrap: coq plugin extraction_plugin extraction_malfunction_ffi
+bootstrap: coq plugin extraction_plugin extraction_ocaml_ffi
 	+make -C plugin/plugin-bootstrap -j 1
 
-.PHONY: extraction_plugin extraction_ocaml_ffi extraction_malfunction_ffi
+.PHONY: extraction_plugin extraction_ocaml_ffi

README.md

@@ -29,6 +29,8 @@ After `From VerifiedExtraction Require Import Extraction.`
 the commands `Verified Extraction <definition>` and `Verified Extraction <definition> "<file>.mlf"` can be used to run the new extraction process.
 Multiple functions can be extracted at the same time with `Verified Extraction (<d1>,<d2>,...)`.
 To add an `mli` file one can add the output of the (unverified) generator `MetaCoq Run Print mli <definition>.` to a `.mli` file.
+Note that this metaprogram does not (yet) take into account the reordering of constructors, besides the one for booleans (see `Extract Inductives` below).
+It won't output declarations for `unit`, `bool`, `list`, `option` and `prod` that have matching representations in OCaml. 
 
 `Verified Extraction` supports the following options:
 
@@ -49,12 +51,19 @@ To add an `mli` file one can add the output of the (unverified) generator `MetaC
 - `-fmt`: Use malfunctions automatic formatting to produce the .mlf file (for more readable generated code)
 - `-unsafe`: Use unsafe optimizations (all of them, or a subset by listing some of the following flags separated by spaces):
     + `cofix-to-lazy`: unverified cofixpoints to lazy/force translation
-    + `reorder-constructors`: honor `Verified Extract Inductive` directives to reorder constructors
     + `inlining`: honor `Verified Extract Inline` directives.
     + `unboxing`: perform unboxing of types having a single constructor with a single computational argument 
       This is run after typed erasure for more opportunities to unbox.
     + `betared`: perform apparent beta reductions (useful when combined with inlining)
 
+`Verified Extraction` also supports the directives:
+  + `Verified Extract Inductives [ ind [ name [ tags ] ], .. ]`: this declares a reordering of constructors 
+    to match existing ocaml datatype representations (tags are natural numbers). This reordering phase is 
+    verified. By default, Coq's booleans `Inductive bool := true | false` are mapped to OCaml's 
+    `type bool = false | true` by swapping their constructor tags.
+  + `Verified Extract Inline cst`: declares `cst` to be inlined (expanded everywhere) during extraction.
+    This phase is NOT verified at the moment.
+
 ## Structure
 
 - the [`theories`](theories) directory contains the Coq files with implementation and verification of the plugin

coq-verified-extraction.opam

@@ -17,7 +17,7 @@ install: [
 depends: [
   "coq" { >= "8.19" & < "8.20~" }
   "coq-ceres" {= "0.4.1"}
-  "coq-metacoq-erasure-plugin"
+  "coq-metacoq-erasure-plugin" { = "8.19.dev" }
   # "malfunction" {= "0.6" }
 ]
 

examples/arity_function/test.v

@@ -14,7 +14,6 @@ Definition function := function_or_nat true.
 Verified Extraction
   function.
 MetaCoq Run Print mli function.
-(* type bool = True  | False  *)
 (* val function : bool -> bool *)
 
 Extraction function_or_nat.
@@ -29,6 +28,4 @@ Require Import Extraction.
 Recursive Extraction assumes_purity.
 
 MetaCoq Run Print mli assumes_purity.
-(* type unit = Tt  *)
-(* type bool = True  | False  *)
 (* val assumes_purity : (unit -> bool) (* higher-order functions are not safe to extract *)  -> bool *)

examples/prim-integers/Makefile

@@ -1,4 +1,4 @@
-CAMLPKGS = coq-core.kernel,coq_verified_extraction.plugin,coq_verified_extraction_malfunction_ffi
+CAMLPKGS = coq-core.kernel,coq_verified_extraction.plugin,coq_verified_extraction_ocaml_ffi
 
 test: append.vo
 

examples/simple/Tests.v

@@ -20,13 +20,13 @@ Local Existing Instance SemanticsSpec.CanonicalHeap.
 
 Definition eval_malfunction (cf := config.extraction_checker_flags) (p : Ast.Env.program)
   : string :=
-  let p' := run (malfunction_pipeline Pipeline.default_malfunction_config) p (MCUtils.todo "wf_env and welltyped term"%bs) in
+  let p' := run (malfunction_pipeline Pipeline.default_malfunction_config) (nil, p) (MCUtils.todo "wf_env and welltyped term"%bs) in
   let t := Mlet_ (MCList.rev_map Malfunction.Named (List.flat_map (fun '(x, d) => match d with Some b => cons (x,b) nil | None => nil end) (fst p')), snd p') in
   time "Pretty printing"%bs (@to_string _ Serialize_t) t.
 
 Definition eval_malfunction_sexp (cf := config.extraction_checker_flags) (p : Ast.Env.program)
   : Malfunction.t :=
-  let p' := run (malfunction_pipeline default_malfunction_config) p (MCUtils.todo "wf_env and welltyped term"%bs) in
+  let p' := run (malfunction_pipeline default_malfunction_config) (nil,p) (MCUtils.todo "wf_env and welltyped term"%bs) in
   let t := Mlet_ (MCList.rev_map Malfunction.Named (List.flat_map (fun '(x, d) => match d with Some b => cons (x,b) nil | None => nil end) (fst p')), snd p') in
   time "Pretty printing"%bs id t.
 

examples/simple/test_extract.v

@@ -8,7 +8,7 @@ From Coq Require Import String.
 From Coq Require Vector.
 
 (* Set Verified Extraction Build Directory "_build". *)
-(* Set MetaCoq Opam Path "/usr/local/bin/opam". *)
+(* Set Verified Extraction Opam Path "/usr/local/bin/opam". *)
 
 From Coq Require Import PrimInt63 Sint63.
 Definition test_primint := 

examples/simple/test_extract_inductive.v

@@ -11,19 +11,15 @@ Verified Extract Inductives [
 Definition coq_true := true.
 Definition coq_false := false.
 (* Set Debug "verified-extraction". *)
-Verified Extraction -time -verbose coq_true.
-Verified Extraction -unsafe coq_true.
+Verified Extraction coq_true.
 Verified Extraction coq_false.
-Verified Extraction -unsafe coq_false.
-
 Verified Extraction andb.
-Verified Extraction -unsafe andb.
 
 Verified Extract Inductives [
   option => "option" [ 1 0 ] (* This makes switches look at none cases before some *)
 ].
 
 Definition test_get := (@option_get nat 0%nat None).
-Verified Extraction -unsafe test_get.
+Verified Extraction test_get.