Commit 6e1ab42d authored by MARCHE Claude's avatar MARCHE Claude

Extraction: all examples ported

parent cae5a087
......@@ -272,17 +272,17 @@ pvsbin/
/examples/*/*/*/*.tex
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
/examples/vstte10_max_sum/*__*.ml
/examples/euler001/*__*.ml
/examples/sudoku/*__*.ml
/examples/vstte10_max_sum/vstte10_max_sum.ml
/examples/euler001/euler001.ml
/examples/sudoku/sudoku.ml
/examples/sudoku/jsmain.js
/examples/in_progress/sudoku_reloaded/*__*.ml
/examples/in_progress/sudoku_reloaded/jsmain.js
/examples/gcd/*__*.ml
/examples/gcd/euclideanAlgorithm63.ml
/examples/gcd/jsmain.js
/examples/defunctionalization/*__*.ml
/examples/defunctionalization/defunctionalization.ml
/examples/vstte12_combinators/jsmain.js
/examples/vstte12_combinators/*__*.ml
/examples/vstte12_combinators/vstte12_combinators.ml
/examples/in_progress/bigInt/jsmain.js
/examples/in_progress/bigInt/*__*.ml
/examples/in_progress/mp/jsmain.js
......
......@@ -231,8 +231,7 @@ extract_and_run examples/gcd gcd.ml 6 15
extract_and_run examples/vstte10_max_sum vstte10_max_sum.ml
extract_and_run examples/vstte12_combinators vstte12_combinators.ml "((((K K) K) K) K)"
extract_and_run examples/defunctionalization defunctionalization.ml
echo "TODO: update 1 more extraction example"
# 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/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 ""
......
......@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
endif
MAIN=main
GEN = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
GEN =sudoku
OBJ=$(GEN)
GENML = $(addsuffix .ml, $(GEN))
......@@ -47,7 +47,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(GENML): ../sudoku.mlw
$(WHY3) extract -D ocaml32 ../sudoku.mlw -o .
$(WHY3) extract -D ocaml64 --recursive -o $@ -L .. sudoku.Test
# javascript
......
......@@ -35,9 +35,9 @@ let print_grid fmt a =
fprintf fmt "@]"
let () =
let sudoku = Sudoku__TheClassicalSudokuGrid.classical_sudoku () in
let sudoku = Sudoku.classical_sudoku () in
printf "Problem: %a@." print_grid input_grid;
let a = Sudoku__Solver.solve sudoku input_grid
let a = Sudoku.solve sudoku input_grid
in
printf "Solution: %a@." print_grid a
......
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