Verified reordering cleanup (#100)

* Adapt to latest metacoq with verified reordering of constructors

* A single implementation of primitives for all plugins, thanks to constructor reordering being built-in now

* Fix install instructions

.vscode/settings.json

@@ -2,5 +2,18 @@
     "lldb.displayFormat": "auto",
     "lldb.showDisassembly": "auto",
     "lldb.dereferencePointers": false,
-    "lldb.consoleMode": "commands"
+    "lldb.consoleMode": "commands",
+    "files.exclude": {
+        "**/*.vo": true,
+        "**/*.vok": true,
+        "**/*.vos": true,
+        "**/*.aux": true,
+        "**/*.glob": true,
+        "**/.git": true,
+        "**/.svn": true,
+        "**/.hg": true,
+        "**/CVS": true,
+        "**/.DS_Store": true,
+        "**/Thumbs.db": true
+    }
 }

Makefile

@@ -1,4 +1,4 @@
-.PHONY: all submodules plugin cplugin install clean bootstrap
+.PHONY: all submodules runtime plugin cplugin install clean bootstrap
 
 
 all theories/Extraction/extraction.vo: theories/Makefile libraries/Makefile
@@ -11,14 +11,13 @@ theories/Makefile: theories/_CoqProject
 libraries/Makefile: libraries/_CoqProject
 	cd libraries;coq_makefile -f _CoqProject -o Makefile
 
-
 submodules:
 	git submodule update
 	./make_submodules.sh
 
 plugins: plugin cplugin
 
-plugin: all plugin/CertiCoq.vo
+plugin: all runtime plugin/CertiCoq.vo
 
 plugin/Makefile: plugin/_CoqProject
 	cd plugin ; coq_makefile -f _CoqProject -o Makefile
@@ -27,7 +26,7 @@ plugin/CertiCoq.vo: all plugin/Makefile theories/Extraction/extraction.vo
 	bash ./make_plugin.sh plugin
 
 
-cplugin: all cplugin/CertiCoq.vo
+cplugin: all runtime cplugin/CertiCoq.vo
 
 cplugin/Makefile: cplugin/_CoqProject
 	cd cplugin ; coq_makefile -f _CoqProject -o Makefile
@@ -41,6 +40,7 @@ bootstrap: plugin cplugin
 install: plugin cplugin bootstrap
 	$(MAKE) -C libraries install
 	$(MAKE) -C theories install
+	$(MAKE) -C runtime install
 	$(MAKE) -C plugin install
 	$(MAKE) -C cplugin install
 	$(MAKE) -C bootstrap install
@@ -55,10 +55,14 @@ mrproper: theories/Makefile libraries/Makefile plugin/Makefile cplugin/Makefile
 clean: theories/Makefile libraries/Makefile plugin/Makefile cplugin/Makefile
 	$(MAKE) -C libraries clean
 	$(MAKE) -C theories clean
+	$(MAKE) -C runtime clean
 	$(MAKE) -C plugin clean
 	$(MAKE) -C cplugin clean
 	$(MAKE) -C bootstrap clean
 	rm -f `find theories -name "*.ml*"`
 	rm -rf plugin/extraction
 	rm -rf cplugin/extraction
-	$(MAKE) mrproper
+	$(MAKE) mrproper
+
+runtime: runtime/Makefile
+	$(MAKE) -C runtime

benchmarks/Makefile

@@ -7,7 +7,7 @@ TESTS=$(shell cat TESTS)
 CFILES=$(patsubst %, CertiCoq.Benchmarks.tests.%_cps.c, $(TESTS)) $(patsubst %, CertiCoq.Benchmarks.tests.%.c, $(TESTS))
 # Names of the generated executables
 EXEC=$(TESTS) $(patsubst %, %_cps, $(TESTS)) $(patsubst %, %_cps_opt, $(TESTS)) $(patsubst %, %_opt, $(TESTS))
-INCLUDE=../plugin/runtime
+INCLUDE=../runtime
 
 all: lib tests exec run
 default: exec run

benchmarks/metacoq_erasure/Makefile

@@ -11,7 +11,7 @@ COQOPTS = -Q ../../theories/Codegen CertiCoq.Codegen -Q ../../libraries CertiCoq
 	-Q ../../theories/Compiler CertiCoq.Compiler -Q ../../theories/common CertiCoq.Common \
 	-Q ../../theories/LambdaBoxMut CertiCoq.LambdaBoxMut -Q .. CertiCoq.Benchmarks
 
-RUNTIME_DIR = ../../plugin/runtime
+RUNTIME_DIR = ../../runtime
 RUNTIME_FILES = ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o
 
 plugin: metacoq_erasure.vo Loader.vo

bootstrap/certicoqc/Makefile

@@ -60,7 +60,7 @@ OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_pl
 GENCFILES = glue.c CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
 CFILES = certicoqc_wrapper.c $(GENCFILES)
 
-RUNTIME_DIR = ../../plugin/runtime
+RUNTIME_DIR = ../../runtime
 RUNTIME_FILES = $(RUNTIME_DIR)/gc_stack.o $(RUNTIME_DIR)/prim_floats.o $(RUNTIME_DIR)/prim_int63.o $(RUNTIME_DIR)/coq_c_ffi.o
 
 VFILES = theories/Loader.v theories/PrimInt63.v theories/PrimFloats.v theories/CertiCoqC.v

bootstrap/certicoqc/g_certicoqc.mlg

@@ -10,6 +10,7 @@ open Stdarg
 open Pcoq.Prim
 open Plugin_utils
 open Certicoq
+open Tacarg
 open G_certicoq_vanilla
 }
 
@@ -58,3 +59,32 @@ VERNAC COMMAND EXTEND CertiCoqCCompile CLASSIFIED AS QUERY
     Feedback.msg_info (str help_msg)
   }
 END
+
+
+VERNAC COMMAND EXTEND CertiCoqC_Eval CLASSIFIED AS SIDEFF
+| [ "CertiCoqC" "Eval" vanilla_cargs_list(l) global(gr) "Extract" "Constants" "[" vanilla_extract_cnst_list_sep(cs, ",") "]" "Include" "[" vanilla_cinclude_list_sep(imps, ",") "]" ] -> {
+  let gr = Nametab.global gr in
+  let opts = Certicoq.make_options l cs (get_name gr) in
+  let result = Certicoq.eval_gr opts gr imps in 
+  Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result)
+  }
+| [ "CertiCoqC" "Eval" vanilla_cargs_list(l) global(gr) ] -> {
+  let gr = Nametab.global gr in
+  let opts = Certicoq.make_options l [] (get_name gr) in
+  let result = Certicoq.eval_gr opts gr [] in
+  Feedback.msg_notice Pp.(str" = " ++ Printer.pr_constr_env (Global.env ()) Evd.empty result)
+  }
+END
+
+TACTIC EXTEND CertiCoqc_eval
+| [ "certicoqc_eval" vanilla_cargs_list(l) constr(c) tactic(tac) ] ->
+  { (* quote and evaluate the given term, unquote, pass the result to t *)
+    Proofview.Goal.enter begin fun gl ->
+      let env = Proofview.Goal.env gl in
+      let sigma = Proofview.Goal.sigma gl in
+      let opts = Certicoq.make_options l [] "goal" in
+      let opts = Certicoq.{ opts with toplevel_name = "goal" } in
+      let c' = Certicoq.eval opts env sigma c [] in 
+      ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c'])
+  end }
+END

bootstrap/certicoqc/test.v

@@ -38,7 +38,12 @@ Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) :=
 
 Set Warnings "-primitive-turned-into-axiom".
 
-Definition demo1 := [1; 0; 1].
+(* Definition demo1 := show [1; 0; 1].
+
+CertiCoqC Eval demo1.
+
+Definition demo2 := if false then false else true.
+CertiCoqC Eval demo2. *)
 
 (* Time CertiCoqC Compile -build_dir "tests" -time -O 1 demo1. *)
 

bootstrap/certicoqc/theories/CertiCoqC.v

@@ -13,8 +13,8 @@ Section Pipeline.
     (prims : list (Kernames.kername * string * bool * nat * positive))
     (debug : bool).
 
-  Definition CertiCoq_pipeline econf (p : Ast.Env.program) :=
-    p <- compile_LambdaBoxMut econf p ;;
+  Definition CertiCoq_pipeline econf im (p : Ast.Env.program) :=
+    p <- compile_LambdaBoxMut econf im p ;;
     p <- compile_LambdaBoxLocal prims p ;;
     p <- compile_LambdaANF_ANF next_id prims p ;;
     (* if debug then compile_LambdaANF_debug next_id p  For debugging intermediate states of the λanf pipeline else *)
@@ -28,7 +28,7 @@ Definition pipeline (p : Template.Ast.Env.program) :=
   let genv := fst p in
   o <- get_options ;;
   '(prs, next_id) <- register_prims next_id genv.(Ast.Env.declarations) ;;
-  p' <- CertiCoq_pipeline next_id prs o.(erasure_config) p ;;
+  p' <- CertiCoq_pipeline next_id prs o.(erasure_config) o.(inductives_mapping) p ;;
   compile_Clight prs p'.
 
 Definition compile (opts : Options) (p : Template.Ast.Env.program) :=

bootstrap/certicoqchk/Makefile

@@ -36,7 +36,7 @@ OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_pl
 GENCFILES = glue.c CertiCoq.CertiCoqCheck.compile.certicoqchk.c
 CFILES = certicoqchk_wrapper.c ${GENCFILES}
 
-RUNTIME_DIR = ../../plugin/runtime
+RUNTIME_DIR = ../../runtime
 RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_ffi.o
 
 CCOMPILEROPTS = -fPIC -g -c -I . -I ${RUNTIME_DIR} -I ${OCAMLLIB} -w -Wno-everything -O2

bootstrap/certicoqchk/certicoqchk.ml

@@ -21,6 +21,4 @@ let check gr =
   (* Quote Coq term *)
   let p = quote gr in
   let b = Certicoqchk_plugin_wrapper.check (Obj.magic p) (* Go through a type equality *) in
-  match b with
-  | Datatypes.Coq_true -> () 
-  | Datatypes.Coq_false -> CErrors.user_err Pp.(str"The program does not typecheck")
+  if b then () else CErrors.user_err Pp.(str"The program does not typecheck")

bootstrap/certicoqchk/certicoqchk_plugin_wrapper.ml

@@ -6,7 +6,7 @@ open Ast0
 open Toplevel2
 open Pipeline_utils
 
-external certicoqchk_wrapper : Ast0.Env.program -> Datatypes.bool = "certicoqchk_wrapper"
+external certicoqchk_wrapper : Ast0.Env.program -> bool = "certicoqchk_wrapper"
 let info s = Feedback.msg_info (Pp.str s)
 
 let msg_info s =

bootstrap/certicoqchk/certicoqchk_plugin_wrapper.mli

@@ -1 +1 @@
-val check : Ast0.Env.program -> Datatypes.bool
+val check : Ast0.Env.program -> bool

cplugin/Loader.v

@@ -1 +1,3 @@
-Declare ML Module "coq-certicoq-vanilla.plugin".
+Declare ML Module "coq-certicoq-vanilla.plugin".
+
+CertiCoq Extract Inductives [ bool => "bool" [ 1 0 ]].

cplugin/Makefile.local

@@ -15,7 +15,4 @@ merlin-hook::
 		$(HIDE)echo 'PKG coq-metacoq-template-ocaml.plugin' >> .merlin
 		$(HIDE)echo 'PKG stdlib-shims' >> .merlin
 
-get_ordinal.o: get_ordinal.c
-	$(CC) -c -o $@ -I runtime $<
-
-certicoq_plugin.cmxs: get_ordinal.o
+certicoq_plugin.cmxs: ../runtime/get_ordinal.o

cplugin/Makefile.local-late

@@ -1,4 +1,2 @@
-# CAMLOPTLINK = "$(OCAMLFIND)" opt      -linkall get_ordinal.o
-
-certicoq_vanilla_plugin.cmxa: certicoq_vanilla_plugin.cmx get_ordinal.o
-	$(HIDE)$(TIMER) $(CAMLOPTLINK) get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $<
+certicoq_vanilla_plugin.cmxa: certicoq_vanilla_plugin.cmx ../runtime/get_ordinal.o
+	$(HIDE)$(TIMER) $(CAMLOPTLINK) ../runtime/get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $<

cplugin/_CoqProject

@@ -21,8 +21,6 @@ PrimInt63.v
 PrimFloats.v
 CertiCoqVanilla.v
 
-static/caml_bool.mli
-static/caml_bool.ml
 static/caml_option.mli
 static/caml_option.ml
 static/caml_nat.mli