Commit e42b9985 authored by MARCHE Claude's avatar MARCHE Claude

bench: add defunctionalization in extraction bench

parent ba81184b
......@@ -224,6 +224,7 @@ echo "=== Extraction to Ocaml ==="
extract_and_run examples/euler001 euler001__*.ml 1000000
extract_and_run examples/vstte10_max_sum vstte10_max_sum__*.ml
extract_and_run examples/sudoku sudoku__*.ml 2,0,9,0,0,0,0,1,0,0,0,0,0,6,0,0,0,0,0,5,3,8,0,2,7,0,0,3,0,0,0,0,0,0,0,0,0,0,0,0,7,5,0,0,3,0,4,1,2,0,8,9,0,0,0,0,4,0,9,0,0,2,0,8,0,0,0,0,1,0,0,5,0,0,0,0,0,0,0,7,6
extract_and_run examples/defunctionalization defunctionalization__*.ml
echo ""
echo "=== Checking valid goals ==="
......
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3
WHY3SHARE=../../share
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
include $(WHY3SHARE)/Makefile.config
ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MAIN = main
OBJ = defunctionalization__Expr \
defunctionalization__DirectSem \
......@@ -12,36 +34,37 @@ CMX = $(addsuffix .cmx, $(OBJ))
ZARITH = $(shell ocamlfind query -i-format zarith)
NUMLIB = zarith
WHY3 = $(shell ocamlfind query -i-format why3)
OCAMLOPT = ocamlopt -noassert -inline 1000
all: $(MAIN).opt
extract: $(ML)
doc:
why3doc ../defunctionalization.mlw
why3session html ../defunctionalization.mlw
firefox defunctionalization.mlw.html defunctionalization.html &
$(WHY3) doc ../defunctionalization.mlw
$(WHY3) session html ../defunctionalization.mlw
@echo firefox ../defunctionalization.html why3session.html
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc -g $(ZARITH) $(WHY3) $(NUMLIB).cma why3extract.cma -o $@ $^
ocamlc -g $(ZARITH) $(INCLUDE) $(NUMLIB).cma why3extract.cma -o $@ $^
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(ZARITH) $(WHY3) $(NUMLIB).cmxa why3extract.cmxa -o $@ $^
$(OCAMLOPT) $(ZARITH) $(INCLUDE) $(NUMLIB).cmxa why3extract.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(ML): ../defunctionalization.mlw
why3 -E ocaml64 ../defunctionalization.mlw -o .
$(WHY3) extract -D ocaml64 ../defunctionalization.mlw -o .
%.cmx: %.ml
$(OCAMLOPT) $(WHY3) -annot -c $<
$(OCAMLOPT) $(INCLUDE) -annot -c $<
%.cmo: %.ml
ocamlc $(WHY3) -annot -g -c $<
ocamlc $(INCLUDE) -annot -g -c $<
%.cmi: %.mli
ocamlc $(WHY3) -annot -g -c $<
ocamlc $(INCLUDE) -annot -g -c $<
clean::
rm -f $(ML) *.cm[xio] $(MAIN).opt
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment