Commit e1568dd2 authored by MARCHE Claude's avatar MARCHE Claude

Sudoku in Javascript: it works !

But: requires to configure why3 with --disable-zarith
parent c3ea4b0f
......@@ -19,10 +19,12 @@ ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MAIN = main
OBJ = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
MAIN=main
GEN = map__Map sudoku__Grid sudoku__TheClassicalSudokuGrid sudoku__Solver
OBJ=$(GEN)
ML = $(addsuffix .ml, $(OBJ))
GENML = $(addsuffix .ml, $(GEN))
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
......@@ -30,7 +32,7 @@ OCAMLOPT = ocamlopt -noassert -inline 1000
all: $(MAIN).opt
extract: $(ML)
extract: $(GENML)
doc:
$(WHY3) doc ../sudoku.mlw
......@@ -44,7 +46,7 @@ $(MAIN).opt: $(CMX) $(MAIN).cmx
$(MAIN).cmx: $(CMX)
$(ML): ../sudoku.mlw
$(GENML): ../sudoku.mlw
$(WHY3) extract -D ocaml32 ../sudoku.mlw -o .
# javascript
......@@ -56,10 +58,10 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o
$(JSMAIN).js: $(JSMAIN).byte
js_of_ocaml -pretty -noinline $(JSMAIN).byte
js_of_ocaml -pretty -noinline +nat.js $(JSMAIN).byte
$(JSMAIN).byte: $(ML) $(JSMAIN).cmo
$(JSOCAMLC) -g -o $@ -linkpkg $^
$(JSMAIN).byte: $(CMO) $(JSMAIN).cmo
$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
%.cmo: %.ml
$(JSOCAMLC) $(INCLUDE) -annot -c $<
......@@ -71,6 +73,6 @@ $(JSMAIN).byte: $(ML) $(JSMAIN).cmo
$(OCAMLOPT) $(INCLUDE) -annot -c $<
clean::
rm -f $(ML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte
rm -f $(GENML) *.annot *.o *.cm[xio] $(MAIN).opt $(MAIN).byte
rm -f sudoku__*.ml why3__*.ml
rm -f int__Int.ml map__Map.ml array__Array.ml
let () = Firebug.console##info (Js.string "debut de jsmain.ml")
module D = Dom_html
let d = D.document
......@@ -201,10 +204,10 @@ let onload (_event : #Dom_html.event Js.t) : bool Js.t =
(fun () -> assert false) in
Dom.appendChild board table;
board##style##backgroundColor <- Js.string "#00ff00";
board##style##paddingLeft <- Js.string "100px";
board##style##paddingRight <- Js.string "100px";
board##style##paddingBottom <- Js.string "100px";
board##style##paddingTop <- Js.string "100px";
board##style##paddingLeft <- Js.string "40px";
board##style##paddingRight <- Js.string "40px";
board##style##paddingBottom <- Js.string "40px";
board##style##paddingTop <- Js.string "40px";
Js._false
let _ = Dom_html.window##onload <- Dom_html.handler onload
......
......@@ -37,7 +37,7 @@ let print_grid fmt a =
let () =
let sudoku = Sudoku__TheClassicalSudokuGrid.classical_sudoku () in
printf "Problem: %a@." print_grid input_grid;
let a = Sudoku__Solver.solve sudoku input_grid
let a = Sudoku__Solver.solve sudoku input_grid
in
printf "Solution: %a@." print_grid a
......@@ -46,6 +46,18 @@ test:
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
that is
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
should give:
2 6 9 3 5 7 8 1 4
......
......@@ -62,12 +62,12 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o
$(JSMAIN).js: $(JSMAIN).byte
js_of_ocaml -pretty -noinline $(JSMAIN).byte
js_of_ocaml -pretty -noinline +nat.js $(JSMAIN).byte
$(JSMAIN).byte: $(ML) jsmain.ml
$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
# $(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
$(JSMAIN).byte: $(CMO) jsmain.ml
# $(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
%.cmo: %.ml
......
let () = Firebug.console##info (Js.string "debut de jsmain.ml")
(* computation part *)
let compute_result text =
......
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