Commit 93815f83 authored by MARCHE Claude's avatar MARCHE Claude

Fix ocaml extraction of "let rec ghost". Added Sudoku extraction + execution in bench

parent 6dae9d0e
......@@ -205,7 +205,7 @@ pvsbin/
/examples/use_api/runstrat/runstrat.opt
/examples/euler001/euler001__*.ml
/examples/euler001/Makefile
/examples/sudoku/euler001__*.ml
/examples/sudoku/sudoku__*.ml
/examples/in_progress/defunctionalization/defunctionalization__*.ml
# modules
......
......@@ -1199,10 +1199,16 @@ clean::
# Ocaml realizations
#######################
OCAMLLIBS_INT_THEORIES = Int Abs ComputerDivision Lex2 MinMax
OCAMLLIBS_MAP_THEORIES = Map
OCAMLLIBS_REF_MODULES = Ref Refint
OCAMLLIBS_ARRAY_MODULES = Array
OCAMLLIBS_FILES = why3__BigInt why3__BuiltIn why3__Prelude \
int__Int int__Abs int__ComputerDivision int__Lex2 int__MinMax \
ref__Refint ref__Ref \
map__Map array__Array
$(addprefix int__, $(OCAMLLIBS_INT_THEORIES)) \
$(addprefix map__, $(OCAMLLIBS_MAP_THEORIES)) \
$(addprefix ref__, $(OCAMLLIBS_REF_MODULES)) \
$(addprefix array__, $(OCAMLLIBS_ARRAY_MODULES))
OCAMLLIBS_MODULES := $(addprefix lib/ocaml/, $(OCAMLLIBS_FILES))
......@@ -1258,6 +1264,14 @@ install_no_local_lib::
$(OCAMLINSTALLLIB)/why3
update-ocaml: update-ocaml-int
update-ocaml-int: bin/why3 theories/int.why
# does not work: would erase existing realization :-(
# for f in $(OCAMLLIBS_INT_THEORIES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ -E ocaml -L modules -L theories -T int.$$f -o lib/ocaml; done
################
# Jessie3 plugin
################
......
......@@ -175,6 +175,7 @@ echo ""
echo "=== Extraction to Ocaml ==="
extract_and_run examples/euler001 euler001__Euler001.ml 1000000
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
echo ""
echo "=== Checking drivers ==="
......
......@@ -9,15 +9,15 @@ CMX = $(addsuffix .cmx, $(OBJ))
ZARITH = $(shell ocamlfind query -i-format zarith)
NUMLIB = zarith
WHY3 = $(shell ocamlfind query -i-format why3)
WHY3 = -I ../../lib/why3
OCAMLOPT = ocamlopt -noassert -inline 1000
all: $(MAIN).opt
doc:
why3doc ../sudoku.mlw
why3session html ../sudoku.mlw
../../bin/why3doc ../sudoku.mlw
../../bin/why3session html ../sudoku.mlw
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc -g $(ZARITH) $(WHY3) $(NUMLIB).cma why3extract.cma -o $@ $^
......@@ -28,7 +28,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(ML): ../sudoku.mlw
why3 -E ocaml ../sudoku.mlw -o .
../../bin/why3 -E ocaml ../sudoku.mlw -o .
%.cmx: %.ml
$(OCAMLOPT) $(WHY3) -annot -c $<
......
open Big_int_Z
type t = big_int
type t = Z.t
let compare = compare_big_int
let zero = zero_big_int
......
......@@ -790,7 +790,7 @@ let rec print_expr ?(paren=false) info fmt e =
and print_rec lr info fst fmt { fun_ps = ps ; fun_lambda = lam } =
if ps.ps_ghost then
fprintf fmt "@[<hov 2>%s %a = ()@]"
(if fst then if lr then "let rec" else "let" else "with")
(if fst then if lr then "let (*rec*)" else "let" else "with")
(print_ps info) ps
else
let print_arg fmt pv = fprintf fmt "@[%a@]" (print_pvty info) pv in
......
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