diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index ad4e5416..bec6c1b4 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -9,7 +9,7 @@ on: branches: - "**" workflow_dispatch: - inputs: + inputs: {} jobs: build-matrix: @@ -19,24 +19,23 @@ jobs: opam_file: - 'coq-certicoq.opam' image: - - 'mattam82/coq:8.17--ocaml-4.13.1--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3' # comment back in if MetaCoq commit changes - # - 'yforster/coq:8.17.0--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3--elpi.1.17.1-metacoq-8.17.dev.e0794e3' + - 'yforster/coq:8.17.0--clang-11--compcert-3.12--extlib-0.11.8--equations-1.3--elpi.1.17.1-metacoq-v1.3-8.17' fail-fast: false # don't stop jobs if one fails steps: - - uses: actions/checkout@v2 - with: - submodules: true + - uses: actions/checkout@v3 + # with: + # submodules: true - uses: coq-community/docker-coq-action@v1 with: custom_image: ${{ matrix.image }} opam_file: ${{ matrix.opam_file }} - before_install: | # comment back in if MetaCoq commit changes - startGroup "fix permission issues" - sudo chown -R coq:coq . - endGroup - startGroup "opam pin" - opam pin -n -y submodules/metacoq - endGroup + # before_install: | # comment back in if MetaCoq commit changes + # startGroup "fix permission issues" + # sudo chown -R coq:coq . + # endGroup + # startGroup "opam pin" + # opam pin -n -y submodules/metacoq + # endGroup before_script: | startGroup "fix permission issues" sudo chown -R coq:coq . diff --git a/.gitignore b/.gitignore index 7f5b32f0..63904e4e 100644 --- a/.gitignore +++ b/.gitignore @@ -131,4 +131,9 @@ bootstrap/certicoqchk/META bootstrap/certicoqc*/glue.c bootstrap/certicoqc*/glue.h plugin/.merlin -_build \ No newline at end of file +_build +.vscode/CertiCoq.code-workspace +bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c +bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.h +bootstrap/certicoqc/tests/test.demo1.c +bootstrap/certicoqc/tests/test.demo1.h diff --git a/.vscode/CertiCoq.code-workspace b/.vscode/CertiCoq.code-workspace deleted file mode 100644 index b7134212..00000000 --- a/.vscode/CertiCoq.code-workspace +++ /dev/null @@ -1,7 +0,0 @@ -{ - "folders": [ - { - "path": ".." - } - ], -} diff --git a/.vscode/launch.json b/.vscode/launch.json index 5c00687d..ef97ee60 100644 --- a/.vscode/launch.json +++ b/.vscode/launch.json @@ -10,10 +10,7 @@ "request": "launch", "name": "Debug", "program": "${workspaceFolder}/_opam/bin/coqc", - "args": [ "-I", ".", "-Q", "../../theories/Codegen", "CertiCoq.Codegen", "-Q", "../../libraries", "CertiCoq.Libraries", "-Q", "../../theories/LambdaANF", - "CertiCoq.LambdaANF", "-Q", "../../theories/LambdaBoxLocal", "CertiCoq.LambdaBoxLocal", "-Q", "../../theories/Compiler", "CertiCoq.Compiler", "-Q", "../../theories/common", "CertiCoq.Common", - "-Q", "../../theories/Glue", "CertiCoq.Glue", "-Q", "../../theories/LambdaBoxMut", "CertiCoq.LambdaBoxMut", "-Q", "../../plugin", "CertiCoq.Plugin", "-I", "../../plugin", "-Q", - "../../cplugin", "CertiCoq.VanillaPlugin", "-I", "../../cplugin", "-Q", "theories", "CertiCoq.CertiCoqC", "test.v"], + "args": [ "test.v"], "cwd": "${workspaceFolder}/bootstrap/certicoqc" }, { diff --git a/Makefile b/Makefile index 07f7fcce..b7005fcc 100644 --- a/Makefile +++ b/Makefile @@ -2,8 +2,8 @@ all theories/Extraction/extraction.vo: theories/Makefile libraries/Makefile - $(MAKE) -C libraries -j`nproc` - $(MAKE) -C theories -j`nproc` + $(MAKE) -C libraries -j1 + $(MAKE) -C theories -j1 theories/Makefile: theories/_CoqProject cd theories;coq_makefile -f _CoqProject -o Makefile diff --git a/benchmarks/test_primitive.v b/benchmarks/test_primitive.v index 46b9085f..16675dd5 100644 --- a/benchmarks/test_primitive.v +++ b/benchmarks/test_primitive.v @@ -4,6 +4,8 @@ From CertiCoq.Plugin Require Import CertiCoq. From Coq Require Import Uint63 ZArith. Open Scope bs. +Set CertiCoq Build Directory "_build". + Definition cst := coq_msg_info (Primitive.string_of_prim_int ((1 << 63))%uint63). Set Warnings "-primitive-turned-into-axiom". CertiCoq Run cst. @@ -16,9 +18,13 @@ From MetaCoq.ErasurePlugin Require Import Loader. (* From MetaCoq.Erasure Require Import Loader. *) -(* Definition testd := diveucl_21 9305446873517 1793572051078448654 4930380657631323783. *) -(* Definition testmul := head0 3221225472. *) -(* Eval compute in testmul. *) +Definition testd := diveucl_21 9305446873517 1793572051078448654 4930380657631323783. +Definition testmul := head0 3221225472. +Eval compute in testmul. + +(* MetaCoq Erase -time -typed testmul. *) + +CertiCoq Eval -time -debug -typed-erasure testmul. (* Result: 549755813886, 0 Calling prim_int63_eqb on 0 and 0: 1, 1 @@ -27,7 +33,33 @@ Calling prim_int63_addmuldiv Calling addmuldiv with 1, 0 and 0: 0 *) (* Definition testd := diveucl_21 4 0 4611686018427387904. *) (* Eval compute in testd. *) -Definition cst_big : BigN.t * BigN.t := BigN.div_eucl (2 ^ 129 + (2 ^ 39 - 2)) 3. +Definition cst_small : BigN.t * BigN.t := BigN.div_eucl (6) 3. +Time Eval vm_compute in cst_small. +Time Eval compute in cst_small. +CertiCoq Eval -time -typed-erasure -unsafe-erasure cst_small. (* Execution: 0.001s *) +CertiCoq Show IR -time -typed-erasure -unsafe-erasure cst_small. (* Execution: 0.001s *) + +From Coq Require Import StreamMemo. + +CertiCoq Show IR -time -typed-erasure -unsafe-erasure memo_make. (* Execution: 0.001s *) + +Definition cst_big : bool := + let x := BigN.div_eucl (2 ^ 129 + (2 ^ 39 - 2)) 3 in + BigN.eqb (fst x) (fst x). + +Time Eval vm_compute in cst_big. (* 0s *) + +(*CertiCoq Eval -time -typed-erasure -unsafe-erasure cst_big.*) (* Execution: 0.001s, slow compilation *) +(* CertiCoq Eval -time -unsafe-erasure cst_big. *) + +Definition cst_big2 : bool := + let x := BigN.div_eucl (2 ^ 64500000 + (2 ^ 39 - 2)) 3 in + BigN.eqb (fst x) (fst x). + +(*Time Eval vm_compute in cst_big2. (* 14 s *) *) +(* Time CertiCoq Eval -debug -time -typed-erasure -unsafe-erasure cst_big2. *) + (* 69s *) + Require Import Cyclic63. Open Scope uint63_scope. Definition test := (addmuldiv 32 3 5629499534213120)%uint63. @@ -55,6 +87,6 @@ Definition string_of_primpair (x : int * int) := Definition result := coq_msg_info (Primitive.string_of_prim_int test). (* Definition result := ("(" ++ Primitive.string_of_prim_int (fst cst_big) ++ ", " ++ *) (* Primitive.string_of_prim_int (snd cst_big) ++ ")")%bs. *) -Time Eval native_compute in result. +Time Eval vm_compute in result. CertiCoq Run result. diff --git a/bootstrap/certicoqc/Makefile b/bootstrap/certicoqc/Makefile index 55958230..0e5d1c12 100644 --- a/bootstrap/certicoqc/Makefile +++ b/bootstrap/certicoqc/Makefile @@ -1,4 +1,15 @@ -CCOMPILER := $(shell { command -v clang-11 || command -v clang; } 2>/dev/null) +# clang compiler +CCOMPILER := $(shell { command -v clang-11 || command -v clang || command -v gcc; } 2>/dev/null) +# clang options +CCOMPILEROPTS = -fPIC -fomit-frame-pointer -g -c -I . -I $(RUNTIME_DIR) -I ${OCAMLLIB} -w -Wno-everything -O2 +SED=`which gsed || which sed` + +# CompCert compiler +CCOMPCOMPILER := $(CCOMPILER) +# $(shell { command -v ccomp; } 2>/dev/null) +# ccomp options +CCOMPCOMPILEROPTS = $(CCOMPILEROPTS) +# -g -c -I . -I $(RUNTIME_DIR) -I ${OCAMLLIB} -w -flongdouble -O2 -include ../../Makefile.conf @@ -34,69 +45,86 @@ COQLIBINSTALL = $(COQLIB)/user-contrib/CertiCoq/CertiCoqC OCAMLLIB = $(shell ocamlc -where) OCAMLOPTS = -package coq-metacoq-template-ocaml.plugin -open Metacoq_template_plugin -package coq-certicoq-vanilla.plugin -open Certicoq_vanilla_plugin \ -I . -thread -rectypes -w +a-4-9-27-41-42-44-45-48-58-67-68 -safe-string -strict-sequence -w -33 -w -34 -w -32 -w -39 -w -20 -w -60 -w -8 -GENCFILES = glue.c CertiCoq.CertiCoqC.compile.certicoqc.c -CFILES = certicoqc_wrapper.c ${GENCFILES} +GENCFILES = glue.c CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c +CFILES = certicoqc_wrapper.c $(GENCFILES) RUNTIME_DIR = ../../plugin/runtime -RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_c_ffi.o +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 -CCOMPILEROPTS = -fPIC -g -c -I . -I ${RUNTIME_DIR} -I ${OCAMLLIB} -w -Wno-everything -O2 -# ccomp CCOMPOPTS = -g -c -I . -I ${OCAMLLIB} -Wno-int-conversion -O2 +.PHONY: runtime certicoqc -.PHONY: certicoqc +all: plugin plugin: theories/compile.vo certicoqc +runtime: $(RUNTIME_FILES:.o=.c) + cd $(RUNTIME_DIR) && $(MAKE) + Makefile.certicoqc: _CoqProject coq_makefile -f _CoqProject -o Makefile.certicoqc -certicoqc: Makefile.certicoqc certicoqc_plugin.cmxs +certicoqc: runtime Makefile.certicoqc certicoqc_plugin.cmxs $(MAKE) -f Makefile.certicoqc test: test.vo test.vo: test.v mkdir -p tests - ulimit -Ss 65500 && coqc ${TESTCOQOPTS} test.v + ulimit -a + ulimit -H -a + ulimit -Ss 65500 && coqc $(TESTCOQOPTS) test.v clean: Makefile.certicoqc make -f Makefile.certicoqc clean - rm *.cm* *.o *.vo + rm -f *.cm* *.o *.vo theories/*.vo -theories/compile.vo ${GENCFILES} &: theories/compile.v - coqc ${COQOPTS} $< +theories/CertiCoqC.vo: theories/CertiCoqC.v + coqc $(COQOPTS) $< -%.o: %.c - $(CCOMPILER) $(CCOMPILEROPTS) -o $@ $< +theories/compile.v: theories/CertiCoqC.vo -certicoqc_plugin.cmxs: certicoqc_plugin.cmxa ${CFILES:.c=.o} ${RUNTIME_FILES} - ocamlfind ocamlopt ${OCAMLOPTS} -shared -o $@ $+ - -certicoqc_plugin.cmx: certicoqc_plugin_wrapper.cmx certicoqc.cmx g_certicoqc.cmx - ocamlfind opt ${OCAMLOPTS} -pack -o $@ $+ - -certicoqc_plugin.cmxa: certicoqc_plugin.cmx - ocamlfind opt -linkall ${OCAMLOPTS} -a -o $@ $< +theories/compile.vo CertiCoq.CertiCoqC.compile.certicoqc.c &: theories/compile.v + coqc $(COQOPTS) $< g_certicoqc.ml: g_certicoqc.mlg certicoqc.cmx certicoqc_plugin_wrapper.cmx coqpp $< -certicoqc_wrapper.c: theories/compile.vo - certicoqc.cmx: certicoqc_plugin_wrapper.cmx +.PRECIOUS: $(GENCFILES) + +$(GENCFILES:%.c=%.o): %.o: %.c + $(SED) -f unicode.sed -i $< + $(CCOMPCOMPILER) $(CCOMPCOMPILEROPTS) -o $@ $< + +certicoqc_wrapper.o: %.o: %.c + $(SED) -f unicode.sed -i $< + $(CCOMPILER) $(CCOMPILEROPTS) -o $@ $< + +certicoqc_plugin.cmx: certicoqc_plugin_wrapper.cmx certicoqc.cmx g_certicoqc.cmx + ocamlfind opt $(OCAMLOPTS) -pack -o $@ $+ + +certicoqc_plugin.cmxa: certicoqc_plugin.cmx + ocamlfind opt -linkall $(OCAMLOPTS) -a -o $@ $< + +certicoqc_plugin.cmxs: certicoqc_plugin.cmxa $(CFILES:.c=.o) $(RUNTIME_FILES) + ocamlfind ocamlopt $(OCAMLOPTS) -shared -o $@ $+ + +.PRECIOUS: %.cmi %.cmi: %.mli - ocamlfind opt ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin $< + ocamlfind opt $(PKGS) $(OCAMLOPTS) -for-pack Certicoqc_plugin $< %.cmx: %.ml %.cmi - ocamlfind opt -c ${PKGS} ${OCAMLOPTS} -for-pack Certicoqc_plugin -o $@ $< + ocamlfind opt -c $(PKGS) $(OCAMLOPTS) -for-pack Certicoqc_plugin -o $@ $< install: theories/compile.vo certicoqc_plugin.cmxs install -d "$(COQLIBINSTALL)" - install -m 0644 theories/compile.v theories/compile.vo certicoqc_plugin.cmx* "$(COQLIBINSTALL)" + install -m 0644 theories/CertiCoqC.v theories/CertiCoqC.vo theories/compile.v theories/compile.vo certicoqc_plugin.cmx* "$(COQLIBINSTALL)" make -f Makefile.certicoqc install ocamlfind install -add coq-certicoqc certicoqc_plugin.cmx* certicoqc_plugin.cmi .PHONY: plugin test + +.NOTPARALLEL: \ No newline at end of file diff --git a/bootstrap/certicoqc/_CoqProject b/bootstrap/certicoqc/_CoqProject index 139ce0ac..a9c3eab7 100644 --- a/bootstrap/certicoqc/_CoqProject +++ b/bootstrap/certicoqc/_CoqProject @@ -6,4 +6,3 @@ META.coq-certicoqc theories/Loader.v -theories/CertiCoqC.v diff --git a/bootstrap/certicoqc/certicoqc.ml b/bootstrap/certicoqc/certicoqc.ml index f48e86f8..9e909745 100644 --- a/bootstrap/certicoqc/certicoqc.ml +++ b/bootstrap/certicoqc/certicoqc.ml @@ -18,7 +18,7 @@ module MLCompiler : Certicoq.CompilerInterface with let printProg prog names (dest : string) (imports : import list) = let imports' = List.map (fun i -> match i with | FromRelativePath s -> "#include \"" ^ s ^ "\"" - | FromLibrary s -> "#include <" ^ s ^ ">" + | FromLibrary (s, _) -> "#include <" ^ s ^ ">" | FromAbsolutePath s -> failwith "Import with absolute path should have been filled") imports in PrintClight.print_dest_names_imports prog (Cps.M.elements names) dest imports' diff --git a/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml b/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml index f245c3b0..34039c2a 100644 --- a/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml +++ b/bootstrap/certicoqc/certicoqc_plugin_wrapper.ml @@ -146,6 +146,21 @@ let fix_quoted_program (p : Ast0.Env.program) = let declarations = fix_declarations declarations in { Ast0.Env.universes = universes; declarations; retroknowledge = retro }, term +let rec print_obj depth x = + if depth <= 0 then Printf.printf "_" + else + let x = Obj.magic x in + if Obj.is_block x then let size = Obj.size x in + if Obj.tag x = 247 then + Printf.printf "POINTER%!" + else + (Printf.printf ("(block[%i] (tag %i) %!") (Obj.size x) (Obj.tag x) ; + for i = 0 to size - 1 do + print_obj (pred depth) (Obj.field x i) + done; + Printf.printf ")") + else Printf.printf ("%i %!") x + let compile opts prog = info "Calling certicoq-compiled certicoq"; (* let pretty= Pretty.print_program false (Obj.magic (Caml_nat.nat_of_caml_int 100)) (Obj.magic prog) in *) @@ -155,4 +170,5 @@ let compile opts prog = (* time (str"Compilation with bootstrapped compiler") *) let res = certicoq_pipeline opts prog in info "Certicoq pipeline ran"; + (* print_obj 10 (Obj.repr (fst res)); *) res \ No newline at end of file diff --git a/bootstrap/certicoqc/certicoqc_wrapper.c b/bootstrap/certicoqc/certicoqc_wrapper.c index 9c35e3b4..7e700666 100644 --- a/bootstrap/certicoqc/certicoqc_wrapper.c +++ b/bootstrap/certicoqc/certicoqc_wrapper.c @@ -1,8 +1,9 @@ #include #include -#include "values.h" -#include "gc.h" +#include "gc_stack.h" +#include #include +#include #include #include @@ -10,11 +11,37 @@ extern value body(struct thread_info *); extern value *call(struct thread_info *, value, value); +value copy_value(value v) { + CAMLparam0(); + CAMLlocal1 (result); + + if (Is_long(v)) { + // printf ("Copying immediate int of value %i\n", Long_val(v)); + result = v; + } + else { + mlsize_t size = Wosize_val(v); + unsigned char tag = Tag_val(v); + + // printf ("Copying object of tag %i and size %i \n", tag, size); + + result = caml_alloc(size, tag); + int i; + for (i = 0; i < size; i++) { + // printf ("Copying field %i of block of tag %i\n", i, tag); + Store_field(result, i, copy_value (Field(v, i))); + } + } + + CAMLreturn (result); +} + // external certicoq_pipeline : (coq_Options × ExtractedASTBaseQuoter.quoted_program) -> coq_Cprogram error * Bytestring.String.t = "certicoq_pipeline" CAMLprim value certicoq_pipeline_wrapper(value opts, value prog) { CAMLparam2 (opts, prog); CAMLlocal1 (res); value closure; + value restemp; struct thread_info* tinfo; clock_t start, end; double msec, sec; @@ -25,7 +52,7 @@ CAMLprim value certicoq_pipeline_wrapper(value opts, value prog) { printf("about to call compiler\n"); closure = body(tinfo); closure = call(tinfo, closure, opts); - res = call(tinfo, closure, prog); + restemp = call(tinfo, closure, prog); printf("compiler returned a value\n"); end = clock(); @@ -33,5 +60,10 @@ CAMLprim value certicoq_pipeline_wrapper(value opts, value prog) { msec = 1000*sec; printf("Time taken %f seconds %f milliseconds\n", sec, msec); + printf("Copying value to OCaml heap\n"); + res = copy_value(restemp); + free_heap(tinfo->heap); + printf("Value copied to OCaml heap\n"); + CAMLreturn(res); } diff --git a/bootstrap/certicoqc/test.v b/bootstrap/certicoqc/test.v index b5665828..4ba1a014 100644 --- a/bootstrap/certicoqc/test.v +++ b/bootstrap/certicoqc/test.v @@ -28,13 +28,18 @@ Definition string_of_bool b := Require Import ZArith. From MetaCoq.ErasurePlugin Require Import Loader. -Fail From CertiCoq.CertiCoqC Require Import compile. -From CertiCoq.CertiCoqC Require Import compile. From CertiCoq.Common Require Import Pipeline_utils. +From CertiCoq.CertiCoqC Require Import CertiCoqC. +From CertiCoq.CertiCoqC Require Import Loader. Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) := let () := coq_msg_info "certicoqc called" in compile opts p. Set Warnings "-primitive-turned-into-axiom". + +Definition demo1 := [1; 0; 1]. + +(* Time CertiCoqC Compile -build_dir "tests" -time -O 1 demo1. *) + Time CertiCoqC Compile -build_dir "tests" -time -O 1 certicoqc. diff --git a/bootstrap/certicoqc/theories/CertiCoqC.v b/bootstrap/certicoqc/theories/CertiCoqC.v index 50d8eb26..cdcab9b7 100644 --- a/bootstrap/certicoqc/theories/CertiCoqC.v +++ b/bootstrap/certicoqc/theories/CertiCoqC.v @@ -1 +1,40 @@ -From CertiCoq.CertiCoqC Require Export Loader. +From MetaCoq.Utils Require Import utils. +Open Scope bs_scope. + +Require Import CertiCoq.Compiler.pipeline. +From CertiCoq.Common Require Import Pipeline_utils. +Require Import ExtLib.Structures.Monad. +Import Monads. +Import MonadNotation. +Import ListNotations. + +Section Pipeline. + Context (next_id : positive) + (prims : list (Kernames.kername * string * bool * nat * positive)) + (debug : bool). + + Definition CertiCoq_pipeline econf (p : Ast.Env.program) := + p <- compile_LambdaBoxMut econf 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 *) + compile_LambdaANF next_id p. +End Pipeline. + +(** * The main CertiCoq pipeline, with MetaCoq's erasure and C-code generation *) +Definition next_id := 100%positive. + +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 ;; + compile_Clight prs p'. + +Definition compile (opts : Options) (p : Template.Ast.Env.program) := + run_pipeline _ _ opts p pipeline. + +Transparent compile.compile. + +Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) := + compile opts p. diff --git a/bootstrap/certicoqc/theories/compile.v b/bootstrap/certicoqc/theories/compile.v index 187f2bb1..922e84c9 100644 --- a/bootstrap/certicoqc/theories/compile.v +++ b/bootstrap/certicoqc/theories/compile.v @@ -3,63 +3,10 @@ From MetaCoq.Utils Require Import utils. Open Scope bs_scope. Require Import CertiCoq.Compiler.pipeline. -From CertiCoq.Common Require Import Pipeline_utils. -Require Import ExtLib.Structures.Monad. -Import Monads. -Import MonadNotation. -Import ListNotations. - -Section Pipeline. - Context (next_id : positive) - (prims : list (Kernames.kername * string * bool * nat * positive)) - (debug : bool). - - Definition CertiCoq_pipeline (p : Ast.Env.program) := - p <- compile_LambdaBoxMut 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 *) - compile_LambdaANF next_id p. -End Pipeline. - -(** * The main CertiCoq pipeline, with MetaCoq's erasure and C-code generation *) -Definition next_id := 100%positive. - -Definition pipeline (p : Template.Ast.Env.program) := - let genv := fst p in - '(prs, next_id) <- register_prims next_id genv.(Ast.Env.declarations) ;; - p' <- CertiCoq_pipeline next_id prs p ;; - compile_Clight prs p'. - -Definition compile (opts : Options) (p : Template.Ast.Env.program) := - run_pipeline _ _ opts p pipeline. - -Transparent compile.compile. - -Definition cps_show (t : LambdaANF_FullTerm) := - let '(prims, primenv, ctorenv, ctortag, indtag, nameenv, funenv, evalenv, e) := t in - let s := cps_show.show_exp nameenv ctorenv false e in - coq_msg_info s. - -Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) := - let () := coq_msg_info "certicoqc called" in - compile opts p. +From CertiCoq.Plugin Require Import CertiCoq. +From CertiCoq.CertiCoqC Require Import CertiCoqC. Set Warnings "-primitive-turned-into-axiom". -(* -From MetaCoq Require Import Primitive Template.Ast. - -Definition certicoqc (opts : Options) (p : Template.Ast.Env.program) := - (* let () := coq_msg_info "certicoqc called" in *) - (* let () := coq_msg_info ("got program: " ++ Pretty.print_program false 100 p) in *) - match snd p with - | Template.Ast.tConst kn _ => - match Env.lookup_env (fst p) kn with - | Some (ConstantDecl {| cst_body := Some (tInt i) |}) => coq_msg_info (string_of_prim_int i) - | _ => tt - end - | _ => tt - end. *) CertiCoq Compile -time -O 1 certicoqc. CertiCoq Generate Glue -file "glue" [ ]. diff --git a/bootstrap/certicoqc/unicode.sed b/bootstrap/certicoqc/unicode.sed new file mode 100644 index 00000000..a331557b --- /dev/null +++ b/bootstrap/certicoqc/unicode.sed @@ -0,0 +1,6 @@ +s/Γ/Gamma/g +s/φ/phi/g +s/Δ/Delta/g +s/π/pi/g +s/ρ/rho/g +s/Σ/Sigma/g \ No newline at end of file diff --git a/bootstrap/certicoqchk/Makefile b/bootstrap/certicoqchk/Makefile index 2259e9e2..5bf14916 100644 --- a/bootstrap/certicoqchk/Makefile +++ b/bootstrap/certicoqchk/Makefile @@ -37,12 +37,13 @@ GENCFILES = glue.c CertiCoq.CertiCoqCheck.compile.certicoqchk.c CFILES = certicoqchk_wrapper.c ${GENCFILES} RUNTIME_DIR = ../../plugin/runtime -RUNTIME_FILES = ${RUNTIME_DIR}/gc_stack.o ${RUNTIME_DIR}/prim_floats.o ${RUNTIME_DIR}/prim_int63.o ${RUNTIME_DIR}/coq_c_ffi.o +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 # ccomp: CCOMPILEROPTS = -g -c -I . -I ${OCAMLLIB} -O2 -.PHONE: certicoqchk +.PHONY: certicoqchk +.PRECIOUS: $(GENCFILES) plugin: compile.vo certicoqchk @@ -53,7 +54,7 @@ test.vo: test.v clean: make -f Makefile.certicoqchk clean - rm *.cm* *.o *.vo + rm -f *.cm* *.o *.vo Makefile.certicoqchk: _CoqProject coq_makefile -f _CoqProject -o Makefile.certicoqchk @@ -101,3 +102,5 @@ install: Loader.vo certicoqchk_plugin.cmxs ocamlfind install -add coq-certicoqchk certicoqchk_plugin.cmx* certicoqchk_plugin.cmi .PHONY: plugin test + +.NOTPARALLEL: \ No newline at end of file diff --git a/bootstrap/certicoqchk/certicoqchk.ml b/bootstrap/certicoqchk/certicoqchk.ml index ca3a3e24..87cb51f4 100644 --- a/bootstrap/certicoqchk/certicoqchk.ml +++ b/bootstrap/certicoqchk/certicoqchk.ml @@ -10,22 +10,11 @@ open ExceptionMonad open AstCommon open Plugin_utils -let debug = true - -let debug_msg (flag : bool) (s : string) = - if flag then - Feedback.msg_debug (str s) - else () - let quote gr = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Evd.fresh_global env sigma gr in - debug_msg debug "Quoting"; - let time = Unix.gettimeofday() in let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass:true env sigma (EConstr.to_constr sigma c) in - let time = (Unix.gettimeofday() -. time) in - debug_msg debug (Printf.sprintf "Finished quoting in %f s.. checking." time); term let check gr = diff --git a/bootstrap/certicoqchk/compile.v b/bootstrap/certicoqchk/compile.v index eb56d14d..d5bc29e6 100644 --- a/bootstrap/certicoqchk/compile.v +++ b/bootstrap/certicoqchk/compile.v @@ -44,7 +44,7 @@ Definition certicoqchk (p : Template.Ast.Env.program) : bool := (guard := Erasure.fake_guard_impl) (nor := PCUICSN.default_normalizing) p Universes.Monomorphic_ctx with - | inl ty => let () := coq_msg_info ty in true + | inl ty => let () := coq_msg_notice ty in true | inr err => let () := coq_user_error err in false end. diff --git a/bootstrap/certicoqchk/test.v b/bootstrap/certicoqchk/test.v index e1719bec..5c20639c 100644 --- a/bootstrap/certicoqchk/test.v +++ b/bootstrap/certicoqchk/test.v @@ -1,5 +1,5 @@ From CertiCoq.CertiCoqCheck Require Import Loader. -Definition foo := (fun x : nat => x = 0). +Definition foo := (fun x : nat => x + 0 = 0). CertiCoqCheck foo. \ No newline at end of file diff --git a/cplugin/CoqMsgFFI.v b/cplugin/CoqMsgFFI.v index 57ccc599..3970c947 100644 --- a/cplugin/CoqMsgFFI.v +++ b/cplugin/CoqMsgFFI.v @@ -11,4 +11,4 @@ CertiCoq Register [ coq_msg_notice => "coq_msg_notice", coq_msg_debug => "coq_msg_debug", coq_user_error => "coq_user_error" ] -Include [ "coq_c_ffi.h" as library ]. +Include [ "coq_c_ffi.h" "coq_ffi.h" as library ]. diff --git a/cplugin/Makefile.local b/cplugin/Makefile.local index e24968a7..8bb44a1f 100644 --- a/cplugin/Makefile.local +++ b/cplugin/Makefile.local @@ -9,5 +9,12 @@ CAMLFLAGS+=-w -20 # Unused arguments CAMLFLAGS+=-w -60 # Unused functor arguments CAMLPKGS+=-package coq-metacoq-template-ocaml.plugin,stdlib-shims +CC=$(shell which gcc || which clang-11) + merlin-hook:: - $(HIDE)echo 'FLG $(OPENS)' >> .merlin \ No newline at end of file + $(HIDE)echo 'FLG $(OPENS)' >> .merlin + +get_ordinal.o: get_ordinal.c + $(CC) -c -o $@ -I runtime $< + +certicoq_plugin.cmxs: get_ordinal.o \ No newline at end of file diff --git a/cplugin/Makefile.local-late b/cplugin/Makefile.local-late new file mode 100644 index 00000000..da418b42 --- /dev/null +++ b/cplugin/Makefile.local-late @@ -0,0 +1,4 @@ +# 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 $@ $< diff --git a/cplugin/_CoqProject b/cplugin/_CoqProject index 382a2724..3277ed9a 100644 --- a/cplugin/_CoqProject +++ b/cplugin/_CoqProject @@ -63,8 +63,8 @@ extraction/pCUICWfEnvImpl.mli extraction/pCUICWfEnvImpl.ml extraction/typing0.mli extraction/typing0.ml -# extraction/environmentTyping.mli -# extraction/environmentTyping.ml +extraction/environmentTyping.mli +extraction/environmentTyping.ml extraction/astUtils.mli extraction/astUtils.ml extraction/etaExpand.mli @@ -115,8 +115,8 @@ extraction/classes1.ml extraction/classes1.mli extraction/classes2.ml extraction/classes2.mli -extraction/ctypesdefs.ml extraction/ctypesdefs.mli +extraction/ctypesdefs.ml extraction/clight.ml extraction/clight.mli extraction/closure_conversion.ml @@ -149,10 +149,6 @@ extraction/primInt63.mli extraction/primInt63.ml extraction/uint0.mli extraction/uint0.ml -extraction/decimalString.mli -extraction/decimalString.ml -extraction/hexadecimalString.mli -extraction/hexadecimalString.ml extraction/primitive.mli extraction/primitive.ml extraction/pCUICPrimitive.mli @@ -167,20 +163,38 @@ extraction/dead_param_elim.ml extraction/dead_param_elim.mli extraction/decimal.ml extraction/decimal.mli +extraction/show.mli +extraction/show.ml extraction/transform.mli extraction/transform.ml extraction/ePrimitive.mli extraction/ePrimitive.ml extraction/eAst.ml extraction/eAst.mli +extraction/eGlobalEnv.mli +extraction/eGlobalEnv.ml extraction/eAstUtils.ml extraction/eAstUtils.mli extraction/eEnvMap.mli extraction/eEnvMap.ml -extraction/eGlobalEnv.mli -extraction/eGlobalEnv.ml -# extraction/eLiftSubst.mli -# extraction/eLiftSubst.ml +extraction/eLiftSubst.ml +extraction/eLiftSubst.mli +extraction/ePretty.mli +extraction/ePretty.ml +extraction/resultMonad.mli +extraction/resultMonad.ml +extraction/exAst.mli +extraction/exAst.ml +extraction/fin.mli +extraction/fin.ml +extraction/vectorDef.mli +extraction/vectorDef.ml +extraction/vector.mli +extraction/vector.ml +extraction/optimize.mli +extraction/optimize.ml +extraction/optimizeCorrectness.mli +extraction/optimizeCorrectness.ml extraction/eCSubst.ml extraction/eCSubst.mli extraction/eWellformed.mli @@ -205,8 +219,16 @@ extraction/eInlineProjections.mli extraction/eInlineProjections.ml extraction/eConstructorsAsBlocks.mli extraction/eConstructorsAsBlocks.ml -# extraction/eCoInductiveToInductive.mli -# extraction/eCoInductiveToInductive.ml +extraction/eUnboxing.mli +extraction/eUnboxing.ml +extraction/eInlining.mli +extraction/eInlining.ml +extraction/eBeta.mli +extraction/eBeta.ml +extraction/eCoInductiveToInductive.mli +extraction/eCoInductiveToInductive.ml +extraction/eReorderCstrs.mli +extraction/eReorderCstrs.ml extraction/eTransform.mli extraction/eTransform.ml extraction/eqDecInstances.ml @@ -221,10 +243,14 @@ extraction/optimizePropDiscr.mli extraction/optimizePropDiscr.ml extraction/extractionCorrectness.mli extraction/extractionCorrectness.ml +extraction/erasure0.mli +extraction/erasure0.ml extraction/erasure.ml extraction/erasure.mli extraction/errors0.ml extraction/errors0.mli +extraction/cRelationClasses.mli +extraction/cRelationClasses.ml # extraction/eGlobalEnv.ml # extraction/eGlobalEnv.mli extraction/eval.ml @@ -273,6 +299,8 @@ extraction/lambdaBoxMut_to_LambdaBoxLocal.ml extraction/lambdaBoxMut_to_LambdaBoxLocal.mli extraction/lambdaBoxLocal_to_LambdaANF.ml extraction/lambdaBoxLocal_to_LambdaANF.mli +extraction/optionMonad.mli +extraction/optionMonad.ml extraction/lambdaANF_to_Clight.ml extraction/lambdaANF_to_Clight.mli extraction/lambdaANF_to_Clight_stack.ml @@ -287,12 +315,12 @@ extraction/logic0.ml extraction/logic0.mli extraction/maps.ml extraction/maps.mli +extraction/utils.mli +extraction/utils.ml extraction/maps_util.ml extraction/maps_util.mli extraction/map_util.ml extraction/map_util.mli -#extraction/decimalString.mli -#extraction/decimalString.ml extraction/reflectEq.mli extraction/reflectEq.ml extraction/mCString.mli @@ -301,12 +329,16 @@ extraction/mCCompare.ml extraction/mCCompare.mli extraction/mCList.ml extraction/mCList.mli +extraction/mCReflect.ml +extraction/mCReflect.mli extraction/mCOption.ml extraction/mCOption.mli extraction/mCPrelude.ml extraction/mCPrelude.mli extraction/mCProd.ml extraction/mCProd.mli +extraction/reflect.mli +extraction/reflect.ml extraction/memdata.ml extraction/memdata.mli extraction/memory.ml @@ -315,8 +347,6 @@ extraction/memtype.ml extraction/memtype.mli extraction/monad0.ml extraction/monad0.mli -extraction/optionMonad.mli -extraction/optionMonad.ml # extraction/monadExc.ml # extraction/monadExc.mli extraction/monadState.ml @@ -373,8 +403,6 @@ extraction/pCUICPosition.ml extraction/pCUICPosition.mli # extraction/pCUICPrimitive.ml # extraction/pCUICPrimitive.mli -extraction/cRelationClasses.mli -extraction/cRelationClasses.ml extraction/pCUICSafeReduce.ml extraction/pCUICSafeReduce.mli extraction/pCUICSafeRetyping.ml @@ -396,6 +424,8 @@ extraction/pOrderedType.ml extraction/pOrderedType.mli extraction/primFloat.ml extraction/primFloat.mli +# extraction/primInt63.ml +# extraction/primInt63.mli extraction/prototype.ml extraction/prototype.mli extraction/proto_util.ml @@ -442,8 +472,8 @@ extraction/toplevel1.ml extraction/toplevel1.mli extraction/toplevel2.ml extraction/toplevel2.mli -# extraction/toplevel3.ml -# extraction/toplevel3.mli +# extraction/topleveLambdaBoxMut.ml +# extraction/topleveLambdaBoxMut.mli extraction/toplevel.ml extraction/toplevel.mli extraction/uGraph0.ml diff --git a/cplugin/certicoq.ml b/cplugin/certicoq.ml index 859c5546..de1e74c5 100644 --- a/cplugin/certicoq.ml +++ b/cplugin/certicoq.ml @@ -3,7 +3,6 @@ (* Copyright (c) 2017 *) (**********************************************************************) -open Pp open Printer open Metacoq_template_plugin.Ast_quoter open ExceptionMonad @@ -136,9 +135,64 @@ let fix_quoted_program (p : Ast0.Env.program) = end +let get_stringopt_option key = + let open Goptions in + let tables = get_tables () in + try + let _ = OptionMap.find key tables in + fun () -> + let tables = get_tables () in + let opt = OptionMap.find key tables in + match opt.opt_value with + | StringOptValue b -> b + | _ -> assert false + with Not_found -> + declare_stringopt_option_and_ref ~depr:false ~key + +let get_build_dir_opt = + get_stringopt_option ["CertiCoq"; "Build"; "Directory"] + +let get_ocamlfind = + get_stringopt_option ["CertiCoq"; "ocamlfind"] + +let get_c_compiler = + get_stringopt_option ["CertiCoq"; "CC"] + +(* Taken from Coq's increment_subscript, but works on strings rather than idents *) +let increment_subscript id = + let len = String.length id in + let rec add carrypos = + let c = id.[carrypos] in + if Util.is_digit c then + if Int.equal (Char.code c) (Char.code '9') then begin + assert (carrypos>0); + add (carrypos-1) + end + else begin + let newid = Bytes.of_string id in + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid carrypos (Char.chr (Char.code c + 1)); + newid + end + else begin + let newid = Bytes.of_string (id^"0") in + if carrypos < len-1 then begin + Bytes.fill newid (carrypos+1) (len-1-carrypos) '0'; + Bytes.set newid (carrypos+1) '1' + end; + newid + end + in String.of_bytes (add (len-1)) + +let debug_reify = CDebug.create ~name:"certicoq-vanilla-reify" () + +external get_unboxed_ordinal : Obj.t -> int = "get_unboxed_ordinal" [@@noalloc] + +external get_boxed_ordinal : Obj.t -> (int [@untagged]) = "get_boxed_ordinal" "get_boxed_ordinal" [@@noalloc] + (** Various Utils *) -let pr_string s = str (Caml_bytestring.caml_string_of_bytestring s) +let pr_string s = Pp.str (Caml_bytestring.caml_string_of_bytestring s) (* remove duplicates but preserve order, keep the leftmost element *) let nub (xs : 'a list) : 'a list = @@ -151,14 +205,14 @@ let rec coq_nat_of_int x = let debug_msg (flag : bool) (s : string) = if flag then - Feedback.msg_debug (str s) + Feedback.msg_debug (Pp.str s) else () - + (* Separate registration of primitive extraction *) type prim = ((Kernames.kername * Kernames.ident) * Datatypes.bool) let global_registers = - Summary.ref (([], []) : prim list * import list) ~name:"Vanilla CertiCoq Registration" + Summary.ref (([], []) : prim list * import list) ~name:"CertiCoq Vanilla Registration" let global_registers_name = "certicoq-vanilla-registration" @@ -184,9 +238,73 @@ let register (prims : prim list) (imports : import list) : unit = let get_global_prims () = fst !global_registers let get_global_includes () = snd !global_registers +(* Support for dynamically-linked certicoq-compiled programs *) +type certicoq_run_function = unit -> Obj.t + +let certicoq_run_functions = + Summary.ref ~name:"CertiCoq Vanilla Run Functions Table" + (CString.Map.empty : certicoq_run_function CString.Map.t) + +let certicoq_run_functions_name = "certicoq-vanilla-run-functions-registration" + +let all_run_functions = ref CString.Set.empty + +let cache_certicoq_run_function (s, s', fn) = + let fns = !certicoq_run_functions in + all_run_functions := CString.Set.add s (CString.Set.add s' !all_run_functions); + certicoq_run_functions := CString.Map.add s fn fns + +let certicoq_run_function_input = + let open Libobject in + declare_object + (global_object_nodischarge certicoq_run_functions_name + ~cache:(fun r -> cache_certicoq_run_function r) + ~subst:None) + +let register_certicoq_run s s' fn = + Feedback.msg_debug Pp.(str"Registering function " ++ str s ++ str " in certicoq_run"); + Lib.add_leaf (certicoq_run_function_input (s, s', fn)) + +let exists_certicoq_run s = + Feedback.msg_debug Pp.(str"Looking up " ++ str s ++ str " in certicoq_run_functions"); + let res = CString.Map.find_opt s !certicoq_run_functions in + if Option.is_empty res then Feedback.msg_debug Pp.(str"Not found"); + res + +let run_certicoq_run s = + try CString.Map.find s !certicoq_run_functions + with Not_found -> CErrors.user_err Pp.(str"Could not find certicoq run function associated to " ++ str s) + +(** Coq FFI: message channels and raising user errors. *) + +let coq_msg_info s = + let s = Caml_bytestring.caml_string_of_bytestring s in + Feedback.msg_info (Pp.str s) + +let _ = Callback.register "coq_msg_info" coq_msg_info + +let coq_msg_debug s = + Feedback.msg_debug Pp.(str (Caml_bytestring.caml_string_of_bytestring s)) + +let _ = Callback.register "coq_msg_debug" coq_msg_debug + +let coq_msg_notice s = + Feedback.msg_notice Pp.(str (Caml_bytestring.caml_string_of_bytestring s)) + +let _ = Callback.register "coq_msg_notice" coq_msg_notice + +let coq_user_error s = + CErrors.user_err Pp.(str (Caml_bytestring.caml_string_of_bytestring s)) + +let _ = Callback.register "coq_user_error" coq_user_error + (** Compilation Command Arguments *) type command_args = + | TYPED_ERASURE + | FAST_ERASURE + | UNSAFE_ERASURE + | BYPASS_QED | CPS | TIME | TIMEANF @@ -198,10 +316,15 @@ type command_args = | EXT of string (* Filename extension to be appended to the file name *) | DEV of int (* For development purposes *) | PREFIX of string (* Prefix to add to the generated FFI fns, avoids clashes with C fns *) + | TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) | FILENAME of string (* Name of the generated file *) type options = - { cps : bool; + { typed_erasure : bool; + fast_erasure : bool; + unsafe_erasure : bool; + bypass_qed : bool; + cps : bool; time : bool; time_anf : bool; olevel : int; @@ -213,43 +336,50 @@ type options = ext : string; dev : int; prefix : string; + toplevel_name : string; prims : ((Kernames.kername * Kernames.ident) * Datatypes.bool) list; } -let default_options : options = - { cps = false; +let check_build_dir d = + if d = "" then "." else + let isdir = + try Unix.((stat d).st_kind = S_DIR) + with Unix.Unix_error (Unix.ENOENT, _, _) -> + CErrors.user_err Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.") + in + if not isdir then + CErrors.user_err Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.") + else d + +let default_options () : options = + { typed_erasure = false; + fast_erasure = false; + unsafe_erasure = false; + bypass_qed = false; + cps = false; time = false; time_anf = false; olevel = 1; debug = false; args = 5; anf_conf = 0; - build_dir = "."; + build_dir = (match get_build_dir_opt () with None -> "." | Some s -> check_build_dir s); filename = ""; ext = ""; dev = 0; prefix = ""; + toplevel_name = "body"; prims = []; } -let check_build_dir d = - if d = "" then "." else - let isdir = - try Unix.((stat d).st_kind = S_DIR) - with Unix.Unix_error (Unix.ENOENT, _, _) -> - CErrors.user_err ~hdr:"pipeline" - Pp.(str "Could not compile: build directory " ++ str d ++ str " not found.") - in - if not isdir then - CErrors.user_err ~hdr:"pipeline" - Pp.(str "Could not compile: " ++ str d ++ str " is not a directory.") - else d - - let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ident) * Datatypes.bool) list) (fname : string) : options = let rec aux (o : options) l = match l with | [] -> o + | TYPED_ERASURE :: xs -> aux {o with typed_erasure = true} xs + | FAST_ERASURE :: xs -> aux {o with fast_erasure = true} xs + | UNSAFE_ERASURE :: xs -> aux {o with unsafe_erasure = true} xs + | BYPASS_QED :: xs -> aux {o with bypass_qed = true} xs | CPS :: xs -> aux {o with cps = true} xs | TIME :: xs -> aux {o with time = true} xs | TIMEANF :: xs -> aux {o with time_anf = true} xs @@ -263,13 +393,37 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide | EXT s :: xs -> aux {o with ext = s} xs | DEV n :: xs -> aux {o with dev = n} xs | PREFIX s :: xs -> aux {o with prefix = s} xs + | TOPLEVEL_NAME s :: xs -> aux {o with toplevel_name = s} xs | FILENAME s :: xs -> aux {o with filename = s} xs in - let opts = { default_options with filename = fname } in + let opts = { (default_options ()) with filename = fname } in let o = aux opts l in {o with prims = pr} + +let make_unsafe_passes b = + let open Erasure0 in + let b = Caml_bool.to_coq b in + { cofix_to_lazy = b; + reorder_constructors = b; + inlining = b; + unboxing = b; + betared = b } +let all_unsafe_passes = make_unsafe_passes true +let no_unsafe_passes = make_unsafe_passes false + + let make_pipeline_options (opts : options) = + let erasure_config = + Erasure0.({ + enable_typed_erasure = Caml_bool.to_coq opts.typed_erasure; + enable_unsafe = if opts.unsafe_erasure then all_unsafe_passes else no_unsafe_passes; + enable_fast_remove_params = Caml_bool.to_coq opts.fast_erasure; + dearging_config = default_dearging_config; (* FIXME *) + inductives_mapping = []; + inlined_constants = Obj.magic (FixRepr.fix_set Kernames.KernameSet.empty) + }) + in let cps = Caml_bool.to_coq opts.cps in let args = coq_nat_of_int opts.args in let olevel = coq_nat_of_int opts.olevel in @@ -279,11 +433,10 @@ let make_pipeline_options (opts : options) = let anfc = coq_nat_of_int opts.anf_conf in let dev = coq_nat_of_int opts.dev in let prefix = bytestring_of_string opts.prefix in + let toplevel_name = bytestring_of_string opts.toplevel_name in let prims = get_global_prims () @ opts.prims in - let name = bytestring_of_string "body" in (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *) - Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix name prims - + Pipeline.make_opts erasure_config cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims (** Main Compilation Functions *) @@ -291,22 +444,26 @@ let make_pipeline_options (opts : options) = let get_name (gr : Names.GlobRef.t) : string = match gr with | Names.GlobRef.ConstRef c -> Names.KerName.to_string (Names.Constant.canonical c) - | _ -> CErrors.user_err ~hdr:"template-coq" (Printer.pr_global gr ++ str " is not a constant definition") + | _ -> CErrors.user_err Pp.(Printer.pr_global gr ++ str " is not a constant definition") (* Quote Coq term *) -let quote opts gr = +let quote_term opts env sigma c = let debug = opts.debug in - let env = Global.env () in - let sigma = Evd.from_env env in - let sigma, c = Evd.fresh_global env sigma gr in + let bypass = opts.bypass_qed in debug_msg debug "Quoting"; let time = Unix.gettimeofday() in - let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass:false env sigma (EConstr.to_constr sigma c) in + let term = Metacoq_template_plugin.Ast_quoter.quote_term_rec ~bypass env sigma (EConstr.to_constr sigma c) in let time = (Unix.gettimeofday() -. time) in - debug_msg debug (Printf.sprintf "Finished quoting in %f s.." time); + debug_msg debug (Printf.sprintf "Finished quoting in %f s.. compiling to L7." time); Obj.magic term +let quote opts gr = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + quote_term opts env sigma c + (* Compile Quoted term with CertiCoq *) module type CompilerInterface = sig @@ -330,7 +487,7 @@ module MLCompiler : CompilerInterface with let printProg prog names (dest : string) (imports : import list) = let imports' = List.map (fun i -> match i with | FromRelativePath s -> "#include \"" ^ s ^ "\"" - | FromLibrary s -> "#include <" ^ s ^ ">" + | FromLibrary (s, _) -> "#include <" ^ s ^ ">" | FromAbsolutePath s -> failwith "Import with absolute path should have been filled") imports in PrintClight.print_dest_names_imports prog (Cps.M.elements names) dest imports' @@ -341,25 +498,20 @@ end module CompileFunctor (CI : CompilerInterface) = struct + let make_fname opts str = Filename.concat opts.build_dir str let compile opts term imports = let debug = opts.debug in let options = make_pipeline_options opts in - let runtime_imports = [FromLibrary (if opts.cps then "gc.h" else "gc_stack.h")] in + let runtime_imports = [FromLibrary ((if opts.cps then "gc.h" else "gc_stack.h"), None)] in let curlib = Sys.getcwd () in let imports = List.map (fun i -> match i with | FromAbsolutePath s -> FromRelativePath (Filename.concat curlib s) | _ -> i) imports in let imports = runtime_imports @ get_global_includes () @ imports in - debug_msg debug (Printf.sprintf "Imports: %s" - (String.concat " " (List.map (fun i -> - match i with - | FromAbsolutePath s -> "#include \"" ^ s ^ "\"" - | FromRelativePath s -> "#include \"" ^ s ^ "\"" - | FromLibrary s -> "#include <" ^ s ^ ">") imports))); let p = CI.compile options term in match p with | (CompM.Ret ((nenv, header), prg), dbg) -> @@ -373,7 +525,6 @@ module CompileFunctor (CI : CompilerInterface) = struct let hstr' = make_fname opts hstr in CI.printProg prg nenv cstr' (imports @ [FromRelativePath hstr]); CI.printProg header nenv hstr' (runtime_imports); - (* (List.map Tm_util.string_to_list imports) *); (* let cstr = Metacoq_template_plugin.Tm_util.string_to_list (Names.KerName.to_string (Names.Constant.canonical const) ^ suff ^ ".c") in * let hstr = Metacoq_template_plugin.Tm_util.string_to_list (Names.KerName.to_string (Names.Constant.canonical const) ^ suff ^ ".h") in @@ -386,17 +537,18 @@ module CompileFunctor (CI : CompilerInterface) = struct | (CompM.Err s, dbg) -> debug_msg debug "Pipeline debug:"; debug_msg debug (string_of_bytestring dbg); - CErrors.user_err ~hdr:"pipeline" (str "Could not compile: " ++ (pr_string s) ++ str "\n") + CErrors.user_err Pp.(str "Could not compile: " ++ (pr_string s) ++ str "\n") + (* Generate glue code for the compiled program *) let generate_glue (standalone : bool) opts globs = if standalone && opts.filename = "" then - CErrors.user_err ~hdr:"glue-code" (str "You need to provide a file name with the -file option.") + CErrors.user_err Pp.(str "You need to provide a file name with the -file option.") else let debug = opts.debug in let options = make_pipeline_options opts in let runtime_imports = - [ FromLibrary (if opts.cps then "gc.h" else "gc_stack.h"); FromLibrary "stdio.h" ] in + [ FromLibrary ((if opts.cps then "gc.h" else "gc_stack.h"), None); FromLibrary ("stdio.h", None) ] in let time = Unix.gettimeofday() in (match CI.generate_glue options globs with | CompM.Ret (((nenv, header), prg), logs) -> @@ -415,9 +567,9 @@ module CompileFunctor (CI : CompilerInterface) = struct CI.printProg header nenv hstr' runtime_imports; let time = (Unix.gettimeofday() -. time) in - debug_msg debug (Printf.sprintf "Printed glue code to file in %f s.." time) + debug_msg debug (Printf.sprintf "Printed glue code to file %s in %f s.." cstr time) | CompM.Err s -> - CErrors.user_err ~hdr:"glue-code" (str "Could not generate glue code: " ++ pr_string s)) + CErrors.user_err Pp.(str "Could not generate glue code: " ++ pr_string s)) let compile_only (opts : options) (gr : Names.GlobRef.t) (imports : import list) : unit = let term = quote opts gr in @@ -426,9 +578,9 @@ module CompileFunctor (CI : CompilerInterface) = struct let generate_glue_only opts gr = let term = quote opts gr in generate_glue true opts (Ast0.Env.declarations (fst (Obj.magic term))) - - let compiler_executable debug = - let whichcmd = Unix.open_process_in "which gcc || which clang-11" in + + let find_executable debug cmd = + let whichcmd = Unix.open_process_in cmd in let result = try Stdlib.input_line whichcmd with End_of_file -> "" @@ -440,6 +592,16 @@ module CompileFunctor (CI : CompilerInterface) = struct result | _ -> failwith "Compiler not found" + let compiler_executable debug = + match get_c_compiler () with + | None -> find_executable debug "which gcc || which clang-11" + | Some s -> s + + let ocamlfind_executable debug = + match get_ocamlfind () with + | None -> find_executable debug "which ocamlfind" + | Some s -> s + type line = | EOF | Info of string @@ -461,7 +623,6 @@ module CompileFunctor (CI : CompilerInterface) = struct | Error s -> Feedback.msg_warning Pp.(str prog ++ str": " ++ str s) done - let runtime_dir () = let open Boot in let env = Env.init () in @@ -469,7 +630,7 @@ module CompileFunctor (CI : CompilerInterface) = struct let make_rt_file na = Boot.Env.Path.(to_string (relative (runtime_dir ()) na)) - + let compile_C opts gr imports = let () = compile_only opts gr imports in let imports = get_global_includes () @ imports in @@ -478,10 +639,10 @@ module CompileFunctor (CI : CompilerInterface) = struct let suff = opts.ext in let name = make_fname opts (fname ^ suff) in let compiler = compiler_executable debug in - let rt_dir = Boot.Env.Path.to_string (runtime_dir ()) in + let rt_dir = runtime_dir () in let cmd = - Printf.sprintf "%s -Wno-everything -g -I %s -I %s -c -o %s %s" - compiler opts.build_dir rt_dir (name ^ ".o") (name ^ ".c") + Printf.sprintf "%s -Wno-everything -O2 -fomit-frame-pointer -g -I %s -I %s -c -o %s %s" + compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (name ^ ".o") (name ^ ".c") in let importso = let oname s = @@ -490,10 +651,10 @@ module CompileFunctor (CI : CompilerInterface) = struct in let imports' = List.concat (List.map (fun i -> match i with - | FromAbsolutePath s -> [s] - | FromRelativePath s -> [s] - | _ -> []) imports) in - let l = make_rt_file "certicoq_run_main.o" :: List.map oname imports' in + | FromAbsolutePath s -> [oname s] + | FromRelativePath s -> [oname s] + | FromLibrary (s, _) -> [make_rt_file (oname s)]) imports) in + let l = make_rt_file "certicoq_run_main.o" :: imports' in String.concat " " l in let gc_stack_o = make_rt_file "gc_stack.o" in @@ -502,7 +663,7 @@ module CompileFunctor (CI : CompilerInterface) = struct | Unix.WEXITED 0 -> let linkcmd = Printf.sprintf "%s -Wno-everything -g -L %s -L %s -o %s %s %s %s" - compiler opts.build_dir rt_dir name gc_stack_o (name ^ ".o") importso + compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) name gc_stack_o (name ^ ".o") importso in debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd); (match Unix.system linkcmd with @@ -513,7 +674,277 @@ module CompileFunctor (CI : CompilerInterface) = struct | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n)) | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str cmd) | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n ++ str" while running " ++ str cmd) + + type reifyable_type = + | IsInductive of Names.inductive * Univ.Instance.t * Constr.t list + | IsPrimitive of Names.Constant.t * Univ.Instance.t * Constr.t list + + let type_of_reifyable_type = function + | IsInductive (hd, u, args) -> Term.applistc (Constr.mkIndU ((hd, u))) args + | IsPrimitive (c, u, args) -> Term.applistc (Constr.mkConstU ((c, u))) args + + let pr_reifyable_type env sigma ty = + Printer.pr_constr_env env sigma (type_of_reifyable_type ty) + + let find_nth_constant n ar = + let open Inductiveops in + let rec aux i const = + if Array.length ar <= i then raise Not_found + else if CList.is_empty ar.(i).cs_args then (* FIXME lets in constructors *) + if const = n then i + else aux (i + 1) (const + 1) + else aux (i + 1) const + in aux 0 0 + + let find_nth_non_constant n ar = + let open Inductiveops in + let rec aux i nconst = + if Array.length ar <= i then raise Not_found + else if not (CList.is_empty ar.(i).cs_args) then + if nconst = n then i + else aux (i + 1) (nconst + 1) + else aux (i + 1) nconst + in aux 0 0 + + let check_reifyable env sigma ty = + (* We might have bound universes though. It's fine! *) + try let (hd, u), args = Inductiveops.find_inductive env sigma ty in + IsInductive (hd, EConstr.EInstance.kind sigma u, args) + with Not_found -> + let hnf = Reductionops.whd_all env sigma ty in + let hd, args = EConstr.decompose_app sigma hnf in + match EConstr.kind sigma hd with + | Const (c, u) when Environ.is_primitive_type env c -> + IsPrimitive (c, EConstr.EInstance.kind sigma u, List.map EConstr.Unsafe.to_constr args) + | _ -> CErrors.user_err + Pp.(str"Cannot reify values of non-inductive or non-primitive type: " ++ + Printer.pr_econstr_env env sigma ty) + + let ill_formed env sigma ty = + match ty with + | IsInductive _ -> + CErrors.anomaly ~label:"certicoq-reify-ill-formed" + Pp.(str "Ill-formed inductive value representation in CertiCoq's reification for type " ++ + pr_reifyable_type env sigma ty) + | IsPrimitive _ -> + CErrors.anomaly ~label:"certicoq-reify-ill-formed" + Pp.(str "Ill-formed primitive value representation in CertiCoq's reification for type " ++ + pr_reifyable_type env sigma ty) + + (* let ocaml_get_boxed_ordinal v = + (* tag is the header of the object *) + let tag = Array.unsafe_get (Obj.magic v : Obj.t array) (-1) in + (* We turn it into an ocaml int usable for arithmetic operations *) + let tag_int = (Stdlib.Int.shift_left (Obj.magic (Obj.repr tag)) 1) + 1 in + Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml tag: %i" (Obj.tag tag))); + Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal int: %u" tag_int)); + Feedback.msg_debug (Pp.str (Printf.sprintf "Ocaml get_boxed_ordinal ordinal: %u" (tag_int land 255))); + tag_int land 255 *) + + + let time ~(msg:Pp.t) f = + let start = Unix.gettimeofday() in + let res = f () in + let time = Unix.gettimeofday () -. start in + Feedback.msg_notice Pp.(msg ++ str (Printf.sprintf " executed in %f sec" time)); + res + + let reify env sigma ty v : Constr.t = + let open Declarations in + let debug s = debug_reify Pp.(fun () -> str s) in + let rec aux ty v = + Control.check_for_interrupt (); + let () = debug_reify Pp.(fun () -> str "Reifying value of type " ++ pr_reifyable_type env sigma ty) in + match ty with + | IsInductive (hd, u, args) -> + let open Inductive in + let open Inductiveops in + let spec = lookup_mind_specif env hd in + let npars = inductive_params spec in + let params, _indices = CList.chop npars args in + let indfam = make_ind_family ((hd, u), params) in + let cstrs = get_constructors env indfam in + if Obj.is_block v then + let ord = get_boxed_ordinal v in + let () = debug (Printf.sprintf "Reifying constructor block of tag %i" ord) in + let coqidx = + try find_nth_non_constant ord cstrs + with Not_found -> ill_formed env sigma ty + in + let cstr = cstrs.(coqidx) in + let ctx = Vars.smash_rel_context cstr.cs_args in + let vargs = List.init (List.length ctx) (Obj.field v) in + let args' = List.map2 (fun decl v -> + let argty = check_reifyable env sigma + (EConstr.of_constr (Context.Rel.Declaration.get_type decl)) in + aux argty v) (List.rev ctx) vargs in + Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) (params @ args') + else (* Constant constructor *) + let ord = (Obj.magic v : int) in + let () = debug (Printf.sprintf "Reifying constant constructor: %i" ord) in + let coqidx = + try find_nth_constant ord cstrs + with Not_found -> ill_formed env sigma ty + in + let () = debug (Printf.sprintf "Reifying constant constructor: %i is %i in Coq" ord coqidx) in + Term.applistc (Constr.mkConstructU ((hd, coqidx + 1), u)) params + | IsPrimitive (c, u, _args) -> + if Environ.is_array_type env c then + CErrors.user_err Pp.(str "Primitive arrays are not supported yet in CertiCoq reification") + else if Environ.is_float64_type env c then + Constr.mkFloat (Obj.magic v) + else if Environ.is_int63_type env c then + Constr.mkInt (Obj.magic v) + else CErrors.user_err Pp.(str "Unsupported primitive type in CertiCoq reification") + in aux ty v + + let reify opts env sigma tyinfo result = + if opts.time then time ~msg:(Pp.str "Reification") (fun () -> reify env sigma tyinfo result) + else reify env sigma tyinfo result + + let template name = + Printf.sprintf "\nvalue %s ()\n { struct thread_info* tinfo = make_tinfo(); return %s_body(tinfo); }\n" name name + let template_header name = + Printf.sprintf "#include \nextern value %s ();\n" name + + let write_c_driver opts name = + let fname = make_fname opts (opts.filename ^ ".c") in + let fhname = make_fname opts (opts.filename ^ ".h") in + let fd = Unix.(openfile fname [O_CREAT; O_APPEND; O_WRONLY] 0o640) in + let chan = Unix.out_channel_of_descr fd in + output_string chan (template name); + flush chan; + close_out chan; + let chan = open_out fhname in + output_string chan (template_header name); + flush chan; close_out chan; + fname + + let template_ocaml id filename name = + Printf.sprintf "external %s : unit -> Obj.t = \"%s\"\nlet _ = Certicoq_vanilla_plugin.Certicoq.register_certicoq_run \"%s\" \"%s\" (Obj.magic %s)" name name id filename name + + let write_ocaml_driver id opts name = + let fname = make_fname opts (opts.filename ^ "_wrapper.ml") in + let chan = open_out fname in + output_string chan (template_ocaml id opts.filename name); + flush chan; close_out chan; fname + + let certicoq_eval_named opts env sigma c global_id imports = + let prog = quote_term opts env sigma c in + let tyinfo = + let ty = Retyping.get_type_of env sigma c in + (* assert (Evd.is_empty sigma); *) + check_reifyable env sigma ty + in + let id = opts.toplevel_name in + let () = compile { opts with toplevel_name = id ^ "_body" } (Obj.magic prog) imports in + (* Write wrapping code *) + let c_driver = write_c_driver opts id in + let ocaml_driver = write_ocaml_driver global_id opts id in + let imports = get_global_includes () @ imports in + let debug = opts.debug in + let suff = opts.ext in + let compiler = compiler_executable debug in + let ocamlfind = ocamlfind_executable debug in + let rt_dir = runtime_dir () in + let cmd = + Printf.sprintf "%s -Wno-everything -O2 -fomit-frame-pointer -g -I %s -I %s -c -o %s %s" + compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (Filename.remove_extension c_driver ^ ".o") c_driver + in + let importso = + let oname s = + assert (CString.is_suffix ".h" s); + String.sub s 0 (String.length s - 2) ^ ".o" + in + let imports' = List.concat (List.map (fun i -> + match i with + | FromAbsolutePath s -> [oname s] + | FromRelativePath s -> [oname s] + | FromLibrary (_, Some s) -> [make_rt_file (oname s)] + | FromLibrary (s, None) -> [make_rt_file (oname s)]) imports) in + let l = imports' in + String.concat " " l + in + let gc_stack_o = make_rt_file "gc_stack.o" in + debug_msg debug (Printf.sprintf "Executing command: %s" cmd); + let packages = ["coq-core"; "coq-core.plugins.ltac"; "coq-metacoq-template-ocaml"; + "coq-core.interp"; "coq-core.kernel"; "coq-core.library"] in + let pkgs = String.concat "," packages in + let dontlink = "str,unix,dynlink,threads,zarith,coq-core,coq-core.plugins.ltac,coq-core.interp" in + match Unix.system cmd with + | Unix.WEXITED 0 -> + let shared_lib = make_fname opts opts.filename ^ suff ^ ".cmxs" in + let linkcmd = + Printf.sprintf "%s ocamlopt -shared -linkpkg -dontlink %s -thread -rectypes -package %s \ + -I %s -I plugin -o %s %s %s %s %s" + ocamlfind dontlink pkgs opts.build_dir shared_lib ocaml_driver gc_stack_o + (make_fname opts opts.filename ^ ".o") importso + in + debug_msg debug (Printf.sprintf "Executing command: %s" linkcmd); + (match Unix.system linkcmd with + | Unix.WEXITED 0 -> + debug_msg debug (Printf.sprintf "Compilation ran fine, linking compiled code for %s" global_id); + Dynlink.loadfile_private shared_lib; + debug_msg debug (Printf.sprintf "Dynamic linking succeeded, retrieving function %s" global_id); + let result = + if opts.time then time ~msg:(Pp.str id) (run_certicoq_run global_id) + else run_certicoq_run global_id () + in + debug_msg debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); + reify opts env sigma tyinfo result + | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str linkcmd) + | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n)) + | Unix.WEXITED n -> CErrors.user_err Pp.(str"Compiler exited with code " ++ int n ++ str" while running " ++ str cmd) + | Unix.WSIGNALED n | Unix.WSTOPPED n -> CErrors.user_err Pp.(str"Compiler was signaled with code " ++ int n ++ str" while running " ++ str cmd) + + let next_string_away_from s bad = + let rec name_rec s = if bad s then name_rec (increment_subscript s) else s in + name_rec s + let find_fresh s map = + Feedback.msg_debug Pp.(str "Looking for fresh " ++ str s ++ str " in " ++ prlist_with_sep spc str (CString.Set.elements map)); + let freshs = next_string_away_from s (fun s -> CString.Set.mem s map) in + Feedback.msg_debug Pp.(str "Found " ++ str freshs); + freshs + + let toplevel_name_of_filename s = + let comps = CString.split_on_char '.' s in + CString.uncapitalize_ascii (CString.concat "_" comps) + + let certicoq_eval opts env sigma c imports = + let global_id = opts.filename in + let fresh_name = find_fresh global_id !all_run_functions in + let opts = { opts with toplevel_name = toplevel_name_of_filename fresh_name; filename = fresh_name } in + certicoq_eval_named opts env sigma c global_id imports + + let run_existing opts env sigma c id run = + let tyinfo = + let ty = Retyping.get_type_of env sigma c in + check_reifyable env sigma ty + in + let result = + if opts.time then time ~msg:Pp.(str"Running " ++ id) run + else run () + in + debug_msg opts.debug (Printf.sprintf "Running the dynamic linked program succeeded, reifying result"); + reify opts env sigma tyinfo result + + let eval opts env sigma c imports = + match exists_certicoq_run opts.filename with + | None -> certicoq_eval opts env sigma c imports + | Some run -> + debug_msg opts.debug (Printf.sprintf "Retrieved earlier compiled code for %s" opts.filename); + run_existing opts env sigma c (Pp.str opts.filename) run + + let eval_gr opts gr imports = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let filename = get_name gr in + let name = toplevel_name_of_filename filename in + let opts = { opts with toplevel_name = name; filename = filename } in + eval opts env sigma c imports + let print_to_file (s : string) (file : string) = let f = open_out file in Printf.fprintf f "%s\n" s; @@ -523,7 +954,6 @@ module CompileFunctor (CI : CompilerInterface) = struct let term = quote opts gr in let debug = opts.debug in let options = make_pipeline_options opts in - let term = FixRepr.fix_quoted_program term in let p = Pipeline.show_IR options (Obj.magic term) in match p with | (CompM.Ret prg, dbg) -> @@ -534,13 +964,13 @@ module CompileFunctor (CI : CompilerInterface) = struct let file = fname ^ suff ^ ".ir" in print_to_file (string_of_bytestring prg) file; let time = (Unix.gettimeofday() -. time) in - Feedback.msg_debug (str (Printf.sprintf "Printed to file in %f s.." time)); + debug_msg debug (Printf.sprintf "Printed to file %s in %f s.." file time); debug_msg debug "Pipeline debug:"; debug_msg debug (string_of_bytestring dbg) | (CompM.Err s, dbg) -> debug_msg debug "Pipeline debug:"; debug_msg debug (string_of_bytestring dbg); - CErrors.user_err ~hdr:"show-ir" (str "Could not compile: " ++ (pr_string s) ++ str "\n") + CErrors.user_err Pp.(str "Could not compile: " ++ (pr_string s) ++ str "\n") (* Quote Coq inductive type *) @@ -553,8 +983,8 @@ module CompileFunctor (CI : CompilerInterface) = struct | Names.GlobRef.IndRef i -> let (mut, _) = i in Names.KerName.to_string (Names.MutInd.canonical mut) - | _ -> CErrors.user_err ~hdr:"template-coq" - (Printer.pr_global gr ++ str " is not an inductive type") in + | _ -> CErrors.user_err + Pp.(Printer.pr_global gr ++ str " is not an inductive type") in debug_msg debug "Quoting"; let time = Unix.gettimeofday() in let term = quote_term_rec ~bypass:true env sigma (EConstr.to_constr sigma c) in @@ -584,11 +1014,11 @@ module CompileFunctor (CI : CompilerInterface) = struct let time = (Unix.gettimeofday() -. time) in debug_msg debug (Printf.sprintf "Printed FFI glue code to file in %f s.." time) | CompM.Err s -> - CErrors.user_err ~hdr:"ffi-glue-code" (str "Could not generate FFI glue code: " ++ pr_string s)) + CErrors.user_err Pp.(str "Could not generate FFI glue code: " ++ pr_string s)) let glue_command opts grs = let terms = grs |> List.rev - |> List.map (fun gr -> Ast0.Env.declarations (fst (quote opts gr))) + |> List.map (fun gr -> Metacoq_template_plugin.Ast0.Env.declarations (fst (quote opts gr))) |> List.concat |> nub in generate_glue true opts (Obj.magic terms) diff --git a/cplugin/certicoq.mli b/cplugin/certicoq.mli index 55a1b712..ae065027 100644 --- a/cplugin/certicoq.mli +++ b/cplugin/certicoq.mli @@ -1,6 +1,10 @@ open Plugin_utils type command_args = + | TYPED_ERASURE + | FAST_ERASURE + | UNSAFE_ERASURE + | BYPASS_QED | CPS | TIME | TIMEANF @@ -12,27 +16,33 @@ type command_args = | EXT of string (* Filename extension to be appended to the file name *) | DEV of int | PREFIX of string (* Prefix to add to the generated FFI fns, avoids clashes with C fns *) + | TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) | FILENAME of string (* Name of the generated file *) -type options = - { cps : bool; - time : bool; - time_anf : bool; - olevel : int; - debug : bool; - args : int; - anf_conf : int; - build_dir : string; - filename : string; - ext : string; - dev : int; - prefix : string; - prims : ((Kernames.kername * Kernames.ident) * Datatypes.bool) list; - } + type options = + { typed_erasure : bool; + fast_erasure : bool; + unsafe_erasure : bool; + bypass_qed : bool; + cps : bool; + time : bool; + time_anf : bool; + olevel : int; + debug : bool; + args : int; + anf_conf : int; + build_dir : string; + filename : string; + ext : string; + dev : int; + prefix : string; + toplevel_name : string; + prims : ((Kernames.kername * Kernames.ident) * Datatypes.bool) list; + } type prim = ((Kernames.kername * Kernames.ident) * Datatypes.bool) -val default_options : options +val default_options : unit -> options val make_options : command_args list -> prim list -> string -> options (* Register primitive operations and associated include file *) @@ -64,6 +74,17 @@ end val compile_only : options -> Names.GlobRef.t -> import list -> unit val generate_glue_only : options -> Names.GlobRef.t -> unit val compile_C : options -> Names.GlobRef.t -> import list -> unit +val eval_gr : options -> Names.GlobRef.t -> import list -> Constr.t val show_ir : options -> Names.GlobRef.t -> unit val ffi_command : options -> Names.GlobRef.t -> unit val glue_command : options -> Names.GlobRef.t list -> unit +val eval : options -> Environ.env -> Evd.evar_map -> EConstr.t -> import list -> Constr.t + +(* Support for running dynamically linked certicoq-compiled programs *) +type certicoq_run_function = unit -> Obj.t + +(* [register_certicoq_run global_id fresh_name function]. A same global_id + can be compiled multiple times with different definitions, fresh_name indicates + the version used this time *) +val register_certicoq_run : string -> string -> certicoq_run_function -> unit +val run_certicoq_run : string -> certicoq_run_function diff --git a/cplugin/certicoq_vanilla_plugin.mlpack b/cplugin/certicoq_vanilla_plugin.mlpack index ef260dd9..ab7d90fb 100644 --- a/cplugin/certicoq_vanilla_plugin.mlpack +++ b/cplugin/certicoq_vanilla_plugin.mlpack @@ -28,6 +28,9 @@ Byte Caml_byte Ascii String0 +Fin +VectorDef +Vector Orders OrdersTac OrdersFacts @@ -48,6 +51,7 @@ FMapFacts BinNums Classes1 EqDecInstances +MCReflect MCPrelude MCOption MCList @@ -58,6 +62,7 @@ Number0 Signature CRelationClasses +ResultMonad DecimalString Byte0 ByteCompare @@ -72,13 +77,13 @@ PrimFloat FloatOps Config0 Kernames +Reflect Transform Universes0 All_Forall BasicAst -DecimalString -HexadecimalString Primitive +Show Environment Ast0 Typing0 @@ -113,6 +118,7 @@ Init TemplateEnvMap TemplateProgram EtaExpand +EnvironmentTyping Ssrbool WGraph @@ -132,6 +138,8 @@ PCUICPosition PCUICChecker PCUICPretty PCUICReflect +PCUICSafeLemmata +PCUICCumulativity PCUICProgram PCUICExpandLets TemplateToPCUIC @@ -154,6 +162,7 @@ EAstUtils EInduction ECSubst EWellformed +ELiftSubst EEnvMap EGlobalEnv EWcbvEval @@ -163,15 +172,25 @@ Extract EEtaExpanded ErasureFunction ErasureFunctionProperties -OptimizePropDiscr -ExtractionCorrectness EProgram ERemoveParams -EOptimizePropDiscr EInlineProjections EConstructorsAsBlocks -ETransform +ExAst Erasure +Optimize +OptimizeCorrectness +EOptimizePropDiscr +OptimizePropDiscr +ExtractionCorrectness +EUnboxing +EInlining +EReorderCstrs +EBeta +ECoInductiveToInductive +ETransform +Erasure0 +ErasureCorrectness SafeTemplateErasure OptionMonad @@ -235,6 +254,7 @@ Zbits Integers Floats AST +Values Values0 LambdaBoxMut_to_LambdaBoxMut_eta LambdaBoxMut_to_LambdaBoxLocal @@ -266,5 +286,6 @@ Glue Ffi Pipeline Plugin_utils + Certicoq G_certicoq_vanilla \ No newline at end of file diff --git a/cplugin/g_certicoq_vanilla.mlg b/cplugin/g_certicoq_vanilla.mlg index 2476dc19..9cf0e539 100644 --- a/cplugin/g_certicoq_vanilla.mlg +++ b/cplugin/g_certicoq_vanilla.mlg @@ -9,10 +9,43 @@ open Ltac_plugin open Stdarg open Pcoq.Prim open Plugin_utils +open Tacexpr +open Tacinterp +open Stdarg +open Tacarg +open Genredexpr + +(** Calling Ltac **) + +let ltac_lcall tac args = + let (location, name) = Loc.tag (Names.Id.of_string tac) + (* Loc.tag @@ Names.Id.of_string tac *) + in + CAst.make ?loc:location (Tacexpr.TacArg(Tacexpr.TacCall + (CAst.make (Locus.ArgVar (CAst.make ?loc:location name),args)))) + + +let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = + let fold arg (i, vars, lfun) = + let id = Names.Id.of_string ("x" ^ string_of_int i) in + let (l,n) = (Loc.tag id) in + let x = Reference (Locus.ArgVar (CAst.make ?loc:l n)) in + (succ i, x :: vars, Names.Id.Map.add id arg lfun) + in + let (_, args, lfun) = List.fold_right fold args (0, [], Names.Id.Map.empty) in + let lfun = Names.Id.Map.add (Names.Id.of_string "F") f lfun in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in + Tacinterp.eval_tactic_ist ist (ltac_lcall "F" args) + +let to_ltac_val c = Tacinterp.Value.of_constr c } -VERNAC ARGUMENT EXTEND vanilla_cargs +ARGUMENT EXTEND vanilla_cargs +| [ "-typed-erasure" ] -> { TYPED_ERASURE } +| [ "-fast-erasure" ] -> { FAST_ERASURE } +| [ "-unsafe-erasure" ] -> { UNSAFE_ERASURE } +| [ "-bypass_qed" ] -> { BYPASS_QED } | [ "-cps" ] -> { CPS } | [ "-time" ] -> { TIME } | [ "-time_anf" ] -> { TIMEANF } @@ -25,6 +58,7 @@ VERNAC ARGUMENT EXTEND vanilla_cargs | [ "-dev" natural(n) ] -> { DEV(n) } | [ "-ext" string(s) ] -> { EXT(s) } | [ "-file" string(s) ] -> { FILENAME(s) } +| [ "-toplevel_name" string(s) ] -> { TOPLEVEL_NAME(s) } END @@ -49,7 +83,7 @@ END VERNAC ARGUMENT EXTEND vanilla_cinclude | [ string(str) ] -> { FromRelativePath str } | [ string(str) "as" "absolute" ] -> { FromAbsolutePath str } -| [ string(str) "as" "library" ] -> { FromLibrary str } +| [ string(str) string_opt(str') "as" "library" ] -> { FromLibrary (str, str') } END VERNAC COMMAND EXTEND CertiCoq_Register CLASSIFIED AS SIDEFF @@ -103,3 +137,31 @@ VERNAC COMMAND EXTEND CertiCoq_Compile CLASSIFIED AS QUERY Feedback.msg_info (str help_msg) } END + +VERNAC COMMAND EXTEND CertiCoq_Eval CLASSIFIED AS SIDEFF +| [ "CertiCoq" "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) + } +| [ "CertiCoq" "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 CertiCoq_eval +| [ "certicoq_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 diff --git a/cplugin/get_ordinal.c b/cplugin/get_ordinal.c new file mode 100644 index 00000000..b2cdfe5b --- /dev/null +++ b/cplugin/get_ordinal.c @@ -0,0 +1,12 @@ +#include "gc_stack.h" +#include + +value get_unboxed_ordinal(value $v) +{ + return Val_long($v); +} + +intnat get_boxed_ordinal(value $v) +{ + return *((unsigned long long *) $v + 18446744073709551615LLU) & 255LLU; +} diff --git a/cplugin/plugin_utils.ml b/cplugin/plugin_utils.ml index 48f4775c..07ee6c49 100644 --- a/cplugin/plugin_utils.ml +++ b/cplugin/plugin_utils.ml @@ -3,10 +3,31 @@ open Names open Pp open Caml_bytestring +let debug_opt = + let open Goptions in + let key = ["CertiCoq"; "Debug"] in + let tables = get_tables () in + try + let _ = OptionMap.find key tables in + fun () -> + let tables = get_tables () in + let opt = OptionMap.find key tables in + match opt.opt_value with + | BoolValue b -> b + | _ -> assert false + with Not_found -> + declare_bool_option_and_ref ~depr:false ~key ~value:false + + let debug (m : unit ->Pp.t) = + if debug_opt () then + Feedback.(msg_debug (m ())) + else + () + type import = FromRelativePath of string | FromAbsolutePath of string - | FromLibrary of string + | FromLibrary of string * string option let string_of_bytestring = caml_string_of_bytestring let bytestring_of_string = bytestring_of_caml_string @@ -16,9 +37,9 @@ let bytestring_of_string = bytestring_of_caml_string let extract_constant (g : Names.GlobRef.t) (s : string) : (Kernames.kername * Kernames.ident) = match g with | Names.GlobRef.ConstRef c -> (Obj.magic (quote_kn (Names.Constant.canonical c)), bytestring_of_caml_string s) - | Names.GlobRef.VarRef(v) -> CErrors.user_err ~hdr:"extract-constant" (str "Expected a constant but found a variable. Only constants can be realized in C.") - | Names.GlobRef.IndRef(i) -> CErrors.user_err ~hdr:"extract-constant" (str "Expected a constant but found an inductive type. Only constants can be realized in C.") - | Names.GlobRef.ConstructRef(c) -> CErrors.user_err ~hdr:"extract-constant" (str "Expected a constant but found a constructor. Only constants can be realized in C. ") + | Names.GlobRef.VarRef(v) -> CErrors.user_err (str "Expected a constant but found a variable. Only constants can be realized in C.") + | Names.GlobRef.IndRef(i) -> CErrors.user_err (str "Expected a constant but found an inductive type. Only constants can be realized in C.") + | Names.GlobRef.ConstructRef(c) -> CErrors.user_err (str "Expected a constant but found a constructor. Only constants can be realized in C. ") let rec debug_mappings (ms : (Kernames.kername * Kernames.ident) list) : unit = match ms with @@ -48,6 +69,9 @@ Valid options:\n\ -cps : Compile using continuation-passing style code (default: direct-style compilation)\n\ -time : Time each compilation phase\n\ -time_anf : Time λanf optimizations\n\ +-unsafe-erasure : Allow to use unsafe passes in the MetaCoq Erasure pipeline. This currently includes the cofixpoint-to-fixpoint translation.\n\ +-typed-erasure : Uses the typed erasure and de-arging phase of the MetaCoq Erasure pipeline.\n\ +-fast-erasure : Uses an alternative function to remove parameters of constructors in the MetaCoq Erasure pipeline.\n\ \n\n\ To compile Gallina constants to specific C functions use:\n\ CertiCoqC Compile Extract Constants [ constant1 => \"c_function1\", ... , constantN => \"c_functionN\" ] Include [ \"file1.h\", ... , \"fileM.h\" ]." diff --git a/cplugin/plugin_utils.mli b/cplugin/plugin_utils.mli index a51f2897..d7b30e25 100644 --- a/cplugin/plugin_utils.mli +++ b/cplugin/plugin_utils.mli @@ -1,7 +1,7 @@ type import = FromRelativePath of string | FromAbsolutePath of string - | FromLibrary of string + | FromLibrary of string * string option val string_of_bytestring : Bytestring.String.t -> string @@ -12,3 +12,6 @@ val extract_constant : Names.GlobRef.t -> string -> Kernames.kername * Kernames. val debug_mappings : (Kernames.kername * Kernames.ident) list -> unit val help_msg : string + +(** This is governed by the global CertiCoq Debug flag *) +val debug : (unit -> Pp.t) -> unit \ No newline at end of file diff --git a/cplugin/runtime/coq_c_ffi.c b/cplugin/runtime/coq_c_ffi.c index 554d6033..cb918770 100644 --- a/cplugin/runtime/coq_c_ffi.c +++ b/cplugin/runtime/coq_c_ffi.c @@ -44,7 +44,7 @@ value coq_user_error(value msg) { char *str = string_of_coq_string(msg); fputs(str, stderr); free(str); - return 1; + exit(1); } value coq_msg_debug(value msg) { @@ -53,3 +53,10 @@ value coq_msg_debug(value msg) { free(str); return 1; } + +value coq_msg_notice(value msg) { + char *str = string_of_coq_string(msg); + fputs(str, stdout); + free(str); + return 1; +} diff --git a/cplugin/runtime/coq_c_ffi.h b/cplugin/runtime/coq_c_ffi.h index d90386d0..895efe33 100644 --- a/cplugin/runtime/coq_c_ffi.h +++ b/cplugin/runtime/coq_c_ffi.h @@ -2,4 +2,5 @@ extern value coq_msg_debug(value msg); extern value coq_msg_info(value msg); +extern value coq_msg_notice(value msg); extern value coq_user_error(value msg); diff --git a/plugin/Makefile.local b/plugin/Makefile.local index 1b4fec03..f35e5adc 100644 --- a/plugin/Makefile.local +++ b/plugin/Makefile.local @@ -20,4 +20,4 @@ merlin-hook:: get_ordinal.o: get_ordinal.c $(CC) -c -o $@ -I runtime $< -certicoq_plugin.cmxs: get_ordinal.o \ No newline at end of file +certicoq_vanilla_plugin.cmxs: get_ordinal.o \ No newline at end of file diff --git a/plugin/Makefile.local-late b/plugin/Makefile.local-late index 6c6f7343..253507c5 100644 --- a/plugin/Makefile.local-late +++ b/plugin/Makefile.local-late @@ -1,4 +1,4 @@ # CAMLOPTLINK = "$(OCAMLFIND)" opt -linkall get_ordinal.o -certicoq_plugin.cmxa: certicoq_plugin.cmx +certicoq_plugin.cmxa: certicoq_plugin.cmx get_ordinal.o $(HIDE)$(TIMER) $(CAMLOPTLINK) get_ordinal.o $(CAMLDEBUG) $(CAMLFLAGS) $(FINDLIBPKGS) -a -o $@ $< diff --git a/plugin/PrimFloats.v b/plugin/PrimFloats.v index 45ae1814..0b61a2fb 100644 --- a/plugin/PrimFloats.v +++ b/plugin/PrimFloats.v @@ -2,6 +2,7 @@ From CertiCoq.Plugin Require Import Loader. From Coq Require Import PrimFloat. CertiCoq Register [ + Coq.Floats.PrimFloat.float => "erased", Coq.Floats.PrimFloat.compare => "prim_float_compare", Coq.Floats.PrimFloat.eqb => "prim_float_eqb", Coq.Floats.PrimFloat.ltb => "prim_float_ltb", diff --git a/plugin/PrimInt63.v b/plugin/PrimInt63.v index d11b3f88..d4e0a757 100644 --- a/plugin/PrimInt63.v +++ b/plugin/PrimInt63.v @@ -2,6 +2,7 @@ From CertiCoq.Plugin Require Import Loader. From Coq.Numbers.Cyclic.Int63 Require Import PrimInt63. CertiCoq Register [ + Coq.Numbers.Cyclic.Int63.PrimInt63.int => "erased", Coq.Numbers.Cyclic.Int63.PrimInt63.add => "prim_int63_add", Coq.Numbers.Cyclic.Int63.PrimInt63.eqb => "prim_int63_eqb", Coq.Numbers.Cyclic.Int63.PrimInt63.land => "prim_int63_land", @@ -9,7 +10,9 @@ CertiCoq Register [ Coq.Numbers.Cyclic.Int63.PrimInt63.lsl => "prim_int63_lsl", Coq.Numbers.Cyclic.Int63.PrimInt63.head0 => "prim_int63_head0", Coq.Numbers.Cyclic.Int63.PrimInt63.tail0 => "prim_int63_tail0", - Coq.Numbers.Cyclic.Int63.PrimInt63.compare => "prim_int63_compare", + Coq.Numbers.Cyclic.Int63.PrimInt63.compare => "prim_int63_compare", + Coq.Numbers.Cyclic.Int63.PrimInt63.asr => "prim_int63_asr", + Coq.Numbers.Cyclic.Int63.PrimInt63.divs => "prim_int63_divs", Coq.Numbers.Cyclic.Int63.PrimInt63.subc => "prim_int63_subc" with tinfo, Coq.Numbers.Cyclic.Int63.PrimInt63.sub => "prim_int63_sub", Coq.Numbers.Cyclic.Int63.PrimInt63.addc => "prim_int63_addc" with tinfo, diff --git a/plugin/_CoqProject b/plugin/_CoqProject index 454af828..722b3b76 100644 --- a/plugin/_CoqProject +++ b/plugin/_CoqProject @@ -56,8 +56,8 @@ extraction/pCUICWfEnvImpl.mli extraction/pCUICWfEnvImpl.ml extraction/typing0.mli extraction/typing0.ml -# extraction/environmentTyping.mli -# extraction/environmentTyping.ml +extraction/environmentTyping.mli +extraction/environmentTyping.ml extraction/astUtils.mli extraction/astUtils.ml extraction/etaExpand.mli @@ -142,10 +142,12 @@ extraction/primInt63.mli extraction/primInt63.ml extraction/uint0.mli extraction/uint0.ml -extraction/decimalString.mli -extraction/decimalString.ml -extraction/hexadecimalString.mli -extraction/hexadecimalString.ml +extraction/show.mli +extraction/show.ml +# extraction/decimalString.mli +# extraction/decimalString.ml +# extraction/hexadecimalString.mli +# extraction/hexadecimalString.ml extraction/primitive.mli extraction/primitive.ml extraction/pCUICPrimitive.mli @@ -172,8 +174,24 @@ extraction/eAstUtils.ml extraction/eAstUtils.mli extraction/eEnvMap.mli extraction/eEnvMap.ml -# extraction/eLiftSubst.ml -# extraction/eLiftSubst.mli +extraction/eLiftSubst.ml +extraction/eLiftSubst.mli +extraction/ePretty.mli +extraction/ePretty.ml +extraction/resultMonad.mli +extraction/resultMonad.ml +extraction/exAst.mli +extraction/exAst.ml +extraction/fin.mli +extraction/fin.ml +extraction/vectorDef.mli +extraction/vectorDef.ml +extraction/vector.mli +extraction/vector.ml +extraction/optimize.mli +extraction/optimize.ml +extraction/optimizeCorrectness.mli +extraction/optimizeCorrectness.ml extraction/eCSubst.ml extraction/eCSubst.mli extraction/eWellformed.mli @@ -198,8 +216,16 @@ extraction/eInlineProjections.mli extraction/eInlineProjections.ml extraction/eConstructorsAsBlocks.mli extraction/eConstructorsAsBlocks.ml -# extraction/eCoInductiveToInductive.mli -# extraction/eCoInductiveToInductive.ml +extraction/eUnboxing.mli +extraction/eUnboxing.ml +extraction/eInlining.mli +extraction/eInlining.ml +extraction/eBeta.mli +extraction/eBeta.ml +extraction/eCoInductiveToInductive.mli +extraction/eCoInductiveToInductive.ml +extraction/eReorderCstrs.mli +extraction/eReorderCstrs.ml extraction/eTransform.mli extraction/eTransform.ml extraction/eqDecInstances.ml @@ -214,6 +240,8 @@ extraction/optimizePropDiscr.mli extraction/optimizePropDiscr.ml extraction/extractionCorrectness.mli extraction/extractionCorrectness.ml +extraction/erasure0.mli +extraction/erasure0.ml extraction/erasure.ml extraction/erasure.mli extraction/errors0.ml @@ -284,6 +312,8 @@ extraction/logic0.ml extraction/logic0.mli extraction/maps.ml extraction/maps.mli +extraction/utils.mli +extraction/utils.ml extraction/maps_util.ml extraction/maps_util.mli extraction/map_util.ml @@ -298,12 +328,16 @@ extraction/mCCompare.ml extraction/mCCompare.mli extraction/mCList.ml extraction/mCList.mli +extraction/mCReflect.ml +extraction/mCReflect.mli extraction/mCOption.ml extraction/mCOption.mli extraction/mCPrelude.ml extraction/mCPrelude.mli extraction/mCProd.ml extraction/mCProd.mli +extraction/reflect.mli +extraction/reflect.ml extraction/memdata.ml extraction/memdata.mli extraction/memory.ml diff --git a/plugin/certicoq.ml b/plugin/certicoq.ml index 4a16cb2b..02ba971e 100644 --- a/plugin/certicoq.ml +++ b/plugin/certicoq.ml @@ -9,20 +9,28 @@ open ExceptionMonad open AstCommon open Plugin_utils +let get_stringopt_option key = + let open Goptions in + let tables = get_tables () in + try + let _ = OptionMap.find key tables in + fun () -> + let tables = get_tables () in + let opt = OptionMap.find key tables in + match opt.opt_value with + | StringOptValue b -> b + | _ -> assert false + with Not_found -> + declare_stringopt_option_and_ref ~depr:false ~key + let get_build_dir_opt = - Goptions.declare_stringopt_option_and_ref - ~key:["CertiCoq"; "Build"; "Directory"] - ~depr:false + get_stringopt_option ["CertiCoq"; "Build"; "Directory"] let get_ocamlfind = - Goptions.declare_stringopt_option_and_ref - ~key:["CertiCoq"; "ocamlfind"] - ~depr:false + get_stringopt_option ["CertiCoq"; "ocamlfind"] let get_c_compiler = - Goptions.declare_stringopt_option_and_ref - ~key:["CertiCoq"; "CC"] - ~depr:false + get_stringopt_option ["CertiCoq"; "CC"] (* Taken from Coq's increment_subscript, but works on strings rather than idents *) let increment_subscript id = @@ -167,6 +175,9 @@ let _ = Callback.register "coq_user_error" coq_user_error (** Compilation Command Arguments *) type command_args = + | TYPED_ERASURE + | FAST_ERASURE + | UNSAFE_ERASURE | BYPASS_QED | CPS | TIME @@ -183,7 +194,10 @@ type command_args = | FILENAME of string (* Name of the generated file *) type options = - { bypass_qed : bool; + { typed_erasure : bool; + fast_erasure : bool; + unsafe_erasure : bool; + bypass_qed : bool; cps : bool; time : bool; time_anf : bool; @@ -212,7 +226,10 @@ let check_build_dir d = else d let default_options () : options = - { bypass_qed = false; + { typed_erasure = false; + fast_erasure = false; + unsafe_erasure = false; + bypass_qed = false; cps = false; time = false; time_anf = false; @@ -233,6 +250,9 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide let rec aux (o : options) l = match l with | [] -> o + | TYPED_ERASURE :: xs -> aux {o with typed_erasure = true} xs + | FAST_ERASURE :: xs -> aux {o with fast_erasure = true} xs + | UNSAFE_ERASURE :: xs -> aux {o with unsafe_erasure = true} xs | BYPASS_QED :: xs -> aux {o with bypass_qed = true} xs | CPS :: xs -> aux {o with cps = true} xs | TIME :: xs -> aux {o with time = true} xs @@ -254,7 +274,28 @@ let make_options (l : command_args list) (pr : ((Kernames.kername * Kernames.ide let o = aux opts l in {o with prims = pr} +let make_unsafe_passes b = + let open Erasure0 in + { cofix_to_lazy = b; + reorder_constructors = b; + inlining = b; + unboxing = b; + betared = b } + +let all_unsafe_passes = make_unsafe_passes true +let no_unsafe_passes = make_unsafe_passes false + let make_pipeline_options (opts : options) = + let erasure_config = + Erasure0.({ + enable_typed_erasure = opts.typed_erasure; + enable_unsafe = if opts.unsafe_erasure then all_unsafe_passes else no_unsafe_passes; + enable_fast_remove_params = opts.fast_erasure; + dearging_config = default_dearging_config; + inductives_mapping = []; + inlined_constants = Kernames.KernameSet.empty + }) + in let cps = opts.cps in let args = coq_nat_of_int opts.args in let olevel = coq_nat_of_int opts.olevel in @@ -267,7 +308,7 @@ let make_pipeline_options (opts : options) = let toplevel_name = bytestring_of_string opts.toplevel_name in let prims = get_global_prims () @ opts.prims in (* Feedback.msg_debug Pp.(str"Prims: " ++ prlist_with_sep spc (fun ((x, y), wt) -> str (string_of_bytestring y)) prims); *) - Pipeline.make_opts cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims + Pipeline.make_opts erasure_config cps args anfc olevel timing timing_anf debug dev prefix toplevel_name prims (** Main Compilation Functions *) @@ -451,7 +492,8 @@ module CompileFunctor (CI : CompilerInterface) = struct | EOF -> debug_msg debug ("Program terminated"); continue := false | Info s -> Feedback.msg_notice Pp.(str prog ++ str": " ++ str s) | Error s -> Feedback.msg_warning Pp.(str prog ++ str": " ++ str s) - done + done; + ignore (Unix.close_process_full (stdout, stdin, stderr)) let runtime_dir () = let open Boot in @@ -677,9 +719,8 @@ module CompileFunctor (CI : CompilerInterface) = struct let compiler = compiler_executable debug in let ocamlfind = ocamlfind_executable debug in let rt_dir = runtime_dir () in - let cmd = - Printf.sprintf "%s -Wno-everything -g -I %s -I %s -c -o %s %s" + Printf.sprintf "%s -Wno-everything -O2 -fomit-frame-pointer -g -I %s -I %s -c -o %s %s" compiler opts.build_dir (Boot.Env.Path.to_string rt_dir) (Filename.remove_extension c_driver ^ ".o") c_driver in let importso = diff --git a/plugin/certicoq.mli b/plugin/certicoq.mli index 0e493721..f0115298 100644 --- a/plugin/certicoq.mli +++ b/plugin/certicoq.mli @@ -1,6 +1,9 @@ open Plugin_utils type command_args = + | TYPED_ERASURE + | FAST_ERASURE + | UNSAFE_ERASURE | BYPASS_QED | CPS | TIME @@ -13,11 +16,14 @@ type command_args = | EXT of string (* Filename extension to be appended to the file name *) | DEV of int | PREFIX of string (* Prefix to add to the generated FFI fns, avoids clashes with C fns *) -| TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) + | TOPLEVEL_NAME of string (* Name of the toplevel function ("body" by default) *) | FILENAME of string (* Name of the generated file *) type options = - { bypass_qed : bool; + { typed_erasure : bool; + fast_erasure : bool; + unsafe_erasure : bool; + bypass_qed : bool; cps : bool; time : bool; time_anf : bool; diff --git a/plugin/certicoq_plugin.mlpack b/plugin/certicoq_plugin.mlpack index aebaf145..eec0ffb0 100644 --- a/plugin/certicoq_plugin.mlpack +++ b/plugin/certicoq_plugin.mlpack @@ -25,6 +25,9 @@ Byte Caml_byte Ascii String0 +Fin +VectorDef +Vector Orders OrdersTac OrdersFacts @@ -45,6 +48,7 @@ FMapFacts BinNums Classes1 EqDecInstances +MCReflect MCPrelude MCOption MCList @@ -55,6 +59,7 @@ Number0 Signature CRelationClasses +ResultMonad DecimalString Byte0 ByteCompare @@ -68,12 +73,12 @@ PrimFloat FloatOps Config0 Kernames +Reflect Transform Universes0 All_Forall BasicAst -DecimalString -HexadecimalString +Show Primitive Environment Ast0 @@ -108,6 +113,7 @@ Init TemplateEnvMap TemplateProgram EtaExpand +EnvironmentTyping Ssrbool WGraph @@ -153,6 +159,7 @@ EInduction ECSubst EWellformed EEnvMap +ELiftSubst EGlobalEnv EWcbvEval ESpineView @@ -166,8 +173,19 @@ ERemoveParams EOptimizePropDiscr EInlineProjections EConstructorsAsBlocks -ETransform +ExAst Erasure +Optimize +OptimizeCorrectness +ExtractionCorrectness +OptimizePropDiscr +EUnboxing +EInlining +EReorderCstrs +EBeta +ECoInductiveToInductive +ETransform +Erasure0 OptimizePropDiscr ErasureCorrectness SafeTemplateErasure diff --git a/plugin/g_certicoq.mlg b/plugin/g_certicoq.mlg index 1a4c9d74..7c3d31ce 100644 --- a/plugin/g_certicoq.mlg +++ b/plugin/g_certicoq.mlg @@ -42,7 +42,10 @@ let to_ltac_val c = Tacinterp.Value.of_constr c } -ARGUMENT EXTEND cargs +ARGUMENT EXTEND cargs +| [ "-typed-erasure" ] -> { TYPED_ERASURE } +| [ "-fast-erasure" ] -> { FAST_ERASURE } +| [ "-unsafe-erasure" ] -> { UNSAFE_ERASURE } | [ "-bypass_qed" ] -> { BYPASS_QED } | [ "-cps" ] -> { CPS } | [ "-time" ] -> { TIME } @@ -60,8 +63,12 @@ ARGUMENT EXTEND cargs END VERNAC ARGUMENT EXTEND extract_cnst -| [ reference(gr) "=>" string(str) ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, false) } -| [ reference(gr) "=>" string(str) "with" "tinfo" ] -> { (extract_constant (Option.get (Constrintern.locate_reference gr)) str, true) } +| [ reference(gr) "=>" string(str) ] -> { + try (extract_constant (Option.get (Constrintern.locate_reference gr)) str, false) + with Not_found -> CErrors.user_err ~loc Pp.(str"Reference " ++ Libnames.pr_qualid gr ++ str" not found") } +| [ reference(gr) "=>" string(str) "with" "tinfo" ] -> { + try (extract_constant (Option.get (Constrintern.locate_reference gr)) str, true) + with Not_found -> CErrors.user_err ~loc Pp.(str"Reference " ++ Libnames.pr_qualid gr ++ str" not found") } END VERNAC ARGUMENT EXTEND ffiargs diff --git a/plugin/plugin_utils.ml b/plugin/plugin_utils.ml index ab87c355..f2e8008b 100644 --- a/plugin/plugin_utils.ml +++ b/plugin/plugin_utils.ml @@ -3,6 +3,27 @@ open Names open Pp open Caml_bytestring +let debug_opt = + let open Goptions in + let key = ["CertiCoq"; "Debug"] in + let tables = get_tables () in + try + let _ = OptionMap.find key tables in + fun () -> + let tables = get_tables () in + let opt = OptionMap.find key tables in + match opt.opt_value with + | BoolValue b -> b + | _ -> assert false + with Not_found -> + declare_bool_option_and_ref ~depr:false ~key ~value:false + + let debug (m : unit ->Pp.t) = + if debug_opt () then + Feedback.(msg_debug (m ())) + else + () + type import = FromRelativePath of string | FromAbsolutePath of string @@ -50,6 +71,9 @@ Valid options:\n\ -cps : Compile using continuation-passing style code (default: direct-style compilation)\n\ -time : Time each compilation phase\n\ -time_anf : Time λanf optimizations\n\ +-unsafe-erasure : Allow to use unsafe passes in the MetaCoq Erasure pipeline. This currently includes the cofixpoint-to-fixpoint translation.\n\ +-typed-erasure : Uses the typed erasure and de-arging phase of the MetaCoq Erasure pipeline.\n\ +-fast-erasure : Uses an alternative function to remove parameters of constructors in the MetaCoq Erasure pipeline.\n\ \n\n\ To compile Gallina constants to specific C functions use:\n\ CertiCoq Compile Extract Constants [ constant1 => \"c_function1\", ... , constantN => \"c_functionN\" ] Include [ \"file1.h\" as library, ... , \"fileM.h\" as library ].\n\ diff --git a/plugin/plugin_utils.mli b/plugin/plugin_utils.mli index 2efeb0ce..d7b30e25 100644 --- a/plugin/plugin_utils.mli +++ b/plugin/plugin_utils.mli @@ -12,3 +12,6 @@ val extract_constant : Names.GlobRef.t -> string -> Kernames.kername * Kernames. val debug_mappings : (Kernames.kername * Kernames.ident) list -> unit val help_msg : string + +(** This is governed by the global CertiCoq Debug flag *) +val debug : (unit -> Pp.t) -> unit \ No newline at end of file diff --git a/plugin/runtime/Makefile b/plugin/runtime/Makefile index f228779e..4a99d72a 100644 --- a/plugin/runtime/Makefile +++ b/plugin/runtime/Makefile @@ -9,7 +9,7 @@ DST = ${COQLIB}/user-contrib/CertiCoq/Plugin/runtime all: ${TARGETS} %.o: %.c - gcc -I . -I `ocamlc -where` -O2 -g -fomit-frame-pointer -c -o $@ $+ + gcc -I . -I `ocamlc -where` -fPIC -O2 -g -fomit-frame-pointer -c -o $@ $+ install: all install -d ${DST} diff --git a/plugin/runtime/coq_c_ffi.c b/plugin/runtime/coq_c_ffi.c index 298d3551..cb918770 100644 --- a/plugin/runtime/coq_c_ffi.c +++ b/plugin/runtime/coq_c_ffi.c @@ -53,3 +53,10 @@ value coq_msg_debug(value msg) { free(str); return 1; } + +value coq_msg_notice(value msg) { + char *str = string_of_coq_string(msg); + fputs(str, stdout); + free(str); + return 1; +} diff --git a/plugin/runtime/coq_c_ffi.h b/plugin/runtime/coq_c_ffi.h index d90386d0..895efe33 100644 --- a/plugin/runtime/coq_c_ffi.h +++ b/plugin/runtime/coq_c_ffi.h @@ -2,4 +2,5 @@ extern value coq_msg_debug(value msg); extern value coq_msg_info(value msg); +extern value coq_msg_notice(value msg); extern value coq_user_error(value msg); diff --git a/submodules/metacoq b/submodules/metacoq index 98b03601..60374183 160000 --- a/submodules/metacoq +++ b/submodules/metacoq @@ -1 +1 @@ -Subproject commit 98b0360169ba1dbc54f92ef50abd4c9dea7dfdc4 +Subproject commit 603741834df00f3dff90c308218eeeb044c241f8 diff --git a/theories/Compiler/pipeline.v b/theories/Compiler/pipeline.v index b877e2d3..788c3889 100644 --- a/theories/Compiler/pipeline.v +++ b/theories/Compiler/pipeline.v @@ -110,7 +110,7 @@ Section Pipeline. Definition CertiCoq_pipeline (p : Ast.Env.program) := o <- get_options ;; - p <- compile_LambdaBoxMut p ;; + p <- compile_LambdaBoxMut o.(erasure_config) p ;; check_axioms p ;; p <- compile_LambdaBoxLocal prims p ;; p <- (if direct o then compile_LambdaANF_ANF next_id prims p else compile_LambdaANF_CPS next_id prims p) ;; @@ -133,7 +133,8 @@ Definition pipeline (p : Template.Ast.Env.program) := Definition default_opts : Options := - {| direct := false; + {| erasure_config := Erasure.default_erasure_config; + direct := false; c_args := 5; anf_conf := 0; show_anf := false; @@ -148,6 +149,7 @@ Definition default_opts : Options := |}. Definition make_opts + (erasure_config : Erasure.erasure_configuration) (cps : bool) (* CPS or direct *) (args : nat) (* number of C args *) (conf : nat) (* λ_ANF configuration *) @@ -159,7 +161,8 @@ Definition make_opts (toplevel_name : string) (* Name of the toplevel function ("body" by default) *) (prims : list (kername * string * bool)) (* list of extracted constants *) : Options := - {| direct := negb cps; + {| erasure_config := erasure_config; + direct := negb cps; c_args := args; anf_conf := conf; show_anf := false; diff --git a/theories/Extraction/extraction.v b/theories/Extraction/extraction.v index 432d61c6..3f885b69 100644 --- a/theories/Extraction/extraction.v +++ b/theories/Extraction/extraction.v @@ -14,6 +14,7 @@ Require compcert.common.AST Require Glue.glue Compiler.pipeline. +From MetaCoq.ErasurePlugin Require Import Erasure. (* Standard lib *) Require Import ExtrOcamlBasic ExtrOCamlFloats ExtrOCamlInt63. Require Import Coq.extraction.Extraction. @@ -101,6 +102,7 @@ Separate Extraction String.length Compiler.pipeline.make_opts Compiler.pipeline.compile + Erasure.default_dearging_config Glue.glue.generate_glue Glue.ffi.generate_ffi cps.M.elements diff --git a/theories/ExtractionVanilla/extraction.v b/theories/ExtractionVanilla/extraction.v index 76935234..a2ac40ee 100644 --- a/theories/ExtractionVanilla/extraction.v +++ b/theories/ExtractionVanilla/extraction.v @@ -115,6 +115,7 @@ Separate Extraction String.length Compiler.pipeline.make_opts Compiler.pipeline.compile + Erasure.default_dearging_config Glue.glue.generate_glue Glue.ffi.generate_ffi cps.M.elements diff --git a/theories/LambdaANF/PrototypeGenFrame.v b/theories/LambdaANF/PrototypeGenFrame.v index d15ecff4..e537c55b 100644 --- a/theories/LambdaANF/PrototypeGenFrame.v +++ b/theories/LambdaANF/PrototypeGenFrame.v @@ -321,9 +321,9 @@ Definition string_of_N n := | N0 => "0" | Npos n => string_of_positive n end. -Compute (string_of_N 100). -Compute (string_of_N 200). -Compute (string_of_N 350). +(* Compute (string_of_N 100). *) +(* Compute (string_of_N 200). *) +(* Compute (string_of_N 350). *) Notation "'GM'" := (stateT N (sum string)). diff --git a/theories/LambdaANF/cps_show.v b/theories/LambdaANF/cps_show.v index 68842c56..5e0acfe4 100644 --- a/theories/LambdaANF/cps_show.v +++ b/theories/LambdaANF/cps_show.v @@ -108,8 +108,8 @@ Definition newline : M unit := emit (String.String chr_newline String.EmptyStrin Definition emit_prim (p : primitive) : M unit := match projT1 p as tag return prim_value tag -> M unit with - | primInt => fun f => emit "(int: " ;; emit (string_of_prim_int f) ;; emit ")" - | primFloat => fun f => emit "(float: " ;; emit (string_of_float f) ;; emit ")" + | primInt => fun f => emit "(int: " ;; emit (Show.string_of_prim_int f) ;; emit ")" + | primFloat => fun f => emit "(float: " ;; emit (AstCommon.string_of_float f) ;; emit ")" end%bs (projT2 p). diff --git a/theories/LambdaANF/inline_correct.v b/theories/LambdaANF/inline_correct.v index fc3a444b..7914c88c 100644 --- a/theories/LambdaANF/inline_correct.v +++ b/theories/LambdaANF/inline_correct.v @@ -2475,7 +2475,7 @@ Section Inline_correct. destruct p. destruct i. do 3 eexists. split; [| split; [| split; [| split; [| split ]]]]. - - setoid_rewrite Hstate. (* why? *) reflexivity. + - reflexivity. - eassumption. - eapply Included_trans. eassumption. rewrite apply_r_empty_f_eq. rewrite image_id, occurs_free_fun_map_empty. sets. diff --git a/theories/LambdaANF/proto_util.v b/theories/LambdaANF/proto_util.v index ee96edd8..d85aede2 100644 --- a/theories/LambdaANF/proto_util.v +++ b/theories/LambdaANF/proto_util.v @@ -57,7 +57,8 @@ Lemma gensyms_len' {A} : forall x (xs : list A) x' xs', (x', xs') = gensyms x xs Proof. intros x xs; revert x; induction xs as [|x xs IHxs]; intros x0 x' xs' Hgen; [simpl in Hgen; now inv Hgen|]. unfold gensyms in Hgen; fold @gensyms in Hgen. - destruct (gensyms (x0 + 1)%positive xs) as [x'' xs''] eqn:Hx0; inv Hgen; now simpl. + destruct (gensyms (x0 + 1)%positive xs) as [x'' xs''] eqn:Hx0. inv Hgen; simpl. f_equal. + eapply IHxs. now symmetry. Qed. Lemma gensyms_increasing' {A} : diff --git a/theories/LambdaBoxMut/compile.v b/theories/LambdaBoxMut/compile.v index 69335d4d..c4110df0 100644 --- a/theories/LambdaBoxMut/compile.v +++ b/theories/LambdaBoxMut/compile.v @@ -4,6 +4,7 @@ recursion on the size of terms, see [compile]). *) Require Import Coq.Lists.List. +From Coq Require Import PrimInt63. Require Import Coq.Arith.Arith. Require Import Common.Common. Require Import Coq.micromega.Lia. @@ -349,6 +350,9 @@ Section Compile. destruct x; cbn; auto with arith. Qed. + Local Open Scope uint63_scope. + Import PrimInt63Notations. + Equations? compile (t: term) : Term by wf t (fun x y : EAst.term => size x < size y) := | e with TermSpineView.view e := { @@ -370,6 +374,10 @@ Section Compile. | tPrim p with trans_prim_val p := { | None => TWrong "unsupported primtive type" | Some pv => TPrim pv } + | tLazy t => TWrong "Lazy" (* TLambda nAnon (lift 1 (compile t)) *) + | tForce t => TWrong "Force" + (* TmkApps (compile t) + (tcons (TPrim (@existT _ (fun tag => prim_value tag) AstCommon.primInt 0)) tnil) *) | tVar _ => TWrong "Var" | tEvar _ _ => TWrong "Evar" }. Proof. @@ -411,8 +419,8 @@ Fixpoint compile_ctx (t : global_context) := (n, compile_global_decl decl) :: compile_ctx rest end. -Program Definition compile_program (p : Ast.Env.program) : Program Term := - let p := run_erase_program p _ in +Program Definition compile_program econf (p : Ast.Env.program) : Program Term := + let p := run_erase_program econf p _ in {| main := compile (snd p) ; env := compile_ctx (fst p) |}. Next Obligation. split. @@ -422,5 +430,5 @@ Next Obligation. split; typeclasses eauto. Qed. -Definition program_Program (p: Ast.Env.program) : Program Term := - compile_program p. +Definition program_Program econf (p: Ast.Env.program) : Program Term := + compile_program econf p. diff --git a/theories/LambdaBoxMut/stripEvalCommute.v b/theories/LambdaBoxMut/stripEvalCommute.v index fa81ed65..7179ca90 100644 --- a/theories/LambdaBoxMut/stripEvalCommute.v +++ b/theories/LambdaBoxMut/stripEvalCommute.v @@ -54,6 +54,7 @@ Definition term_flags := has_tFix := true; has_tCoFix := false; has_tPrim := prim_flags; + has_tLazy_Force := false; |}. Definition env_flags := diff --git a/theories/LambdaBoxMut/toplevel.v b/theories/LambdaBoxMut/toplevel.v index c22a0bee..36b16552 100644 --- a/theories/LambdaBoxMut/toplevel.v +++ b/theories/LambdaBoxMut/toplevel.v @@ -29,8 +29,8 @@ Import MonadNotation. BigStep := fun s sv => WcbvEval (env s) (main s) sv }. -Definition compile_LambdaBoxMut +Definition compile_LambdaBoxMut econf : CertiCoqTrans (Ast.Env.program) (Program LambdaBoxMut.compile.Term) := fun src => debug_msg "Translating from L1g to L1k" ;; - (LiftCertiCoqTrans "LambdaBoxMut" compile_program src). + (LiftCertiCoqTrans "LambdaBoxMut" (compile_program econf) src). diff --git a/theories/common/AstCommon.v b/theories/common/AstCommon.v index d08b2988..032ae0e7 100644 --- a/theories/common/AstCommon.v +++ b/theories/common/AstCommon.v @@ -572,10 +572,24 @@ Definition prim_value (p : prim_tag) : Set := Definition primitive : Set := { tag : prim_tag & prim_value tag }. +Import SpecFloat. + +(* C version using macros for INFINITY and NAN *) +Definition string_of_specfloat (f : SpecFloat.spec_float) := + match f with + | S754_zero sign => if sign then "-0" else "0" + | S754_infinity sign => if sign then "-INFINITY" else "INFINITY" + | S754_nan => "NAN" + | S754_finite sign p z => + let num := MCString.string_of_positive p ++ "p" ++ string_of_Z z in + if sign then "-" ++ num else num + end%bs. + +Definition string_of_float f := string_of_specfloat (FloatOps.Prim2SF f). Definition string_of_prim (p : primitive) := match projT1 p as tag return prim_value tag -> string with - | primInt => Primitive.string_of_prim_int - | primFloat => Primitive.string_of_float + | primInt => Show.string_of_prim_int + | primFloat => string_of_float end (projT2 p). Equations eqb_prim (p q : primitive) : bool := diff --git a/theories/common/Pipeline_utils.v b/theories/common/Pipeline_utils.v index da7a69a6..8b708e2d 100644 --- a/theories/common/Pipeline_utils.v +++ b/theories/common/Pipeline_utils.v @@ -3,7 +3,8 @@ From Coq Require Import PArith. From ExtLib Require Import Monads. Require Import MetaCoq.Utils.bytestring. Require Import Common.AstCommon Common.compM. - +From MetaCoq.ErasurePlugin Require Import Erasure. +#[global] Hint Resolve Bool.absurd_eq_true Bool.trans_eq_bool f_equal2_nat f_equal_nat : core. Import MonadNotation ListNotations. Notation ret := (ExtLib.Structures.Monad.ret). @@ -17,7 +18,8 @@ Open Scope bs_scope. (* Compiler options *) Record Options := - { direct : bool; (* direct or CPS code *) + { erasure_config : erasure_configuration; + direct : bool; (* direct or CPS code *) c_args : nat; (* numbers of C arguments *) anf_conf : nat; (* for different ANF pipeline configs. For development purposes *)