Merge branch 'master' into claude

Conflicts:
	examples/bts/execute.mlw

.gitignore

@@ -238,6 +238,8 @@ pvsbin/
 /examples/euler001/*__*.ml
 /examples/sudoku/*__*.ml
 /examples/sudoku/jsmain.js
+/examples/in_progress/sudoku_reloaded/*__*.ml
+/examples/in_progress/sudoku_reloaded/jsmain.js
 /examples/gcd/*__*.ml
 /examples/gcd/jsmain.js
 /examples/defunctionalization/*__*.ml

configure.in

@@ -292,11 +292,21 @@ if test "$USEOCAMLFIND" = yes; then
    fi
 fi
 
-#if ocamlfind is used it gives the install path for ocaml library
-if test "$USEOCAMLFIND" = yes; then
-   OCAMLINSTALLLIB=$(ocamlfind printconf destdir)
+if test "$enable_local" = no; then
+   LOCALDIR=''
 else
-   OCAMLINSTALLLIB=$OCAMLLIB
+   LOCALDIR="${PWD}"
+fi
+
+if test "$enable_local" = yes ; then
+   OCAMLINSTALLLIB=$LOCALDIR/lib
+else
+   #if ocamlfind is used it gives the install path for ocaml library
+   if test "$USEOCAMLFIND" = yes; then
+      OCAMLINSTALLLIB=$(ocamlfind printconf destdir)
+   else
+      OCAMLINSTALLLIB=$OCAMLLIB
+   fi
 fi
 
 # bin-annot
@@ -672,12 +682,6 @@ if test "$enable_frama_c" = yes ; then
    fi
 fi
 
-if test "$enable_local" = no; then
-   LOCALDIR=''
-else
-   LOCALDIR="${PWD}"
-fi
-
 #For the META
 if test "$enable_hypothesis_selection" = yes; then
    META_OCAMLGRAPH="ocamlgraph"

drivers/cvc4_bare.drv

@@ -8,6 +8,14 @@ prelude "(set-logic AUFNIRA)"   (* how come bv is supported by cvc4 in this logi
 
 import "smt-libv2.drv"
 
+(* regexp for steps should match things like
+
+smt::SmtEngine::resourceUnitsUsed, 1041
+
+but not in the same line as the "valid" answer
+
+*)
+
 (* CVC4 division seems to be neither the Euclidean one, nor the Computer one *)
 (*
 theory int.EuclideanDivision

drivers/psyche.drv

+(* Why driver for Psyche *)
+
+prelude "(set-logic FO)"
+
+printer "smtv2"
+filename "%f-%t-%g.smt2"
+
+valid "^PROVABLE"
+invalid "^NOT PROVABLE"
+timeout "interrupted by timeout"
+time "why3cpulimit time : %s s"
+
+(* À discuter *)
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_definition"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification"*)
+
+transformation "discriminate"
+transformation "encoding_smt"
+
+theory BuiltIn
+  syntax type real  "Real"
+  syntax predicate (=)  "(= %1 %2)"
+  meta "eliminate_algebraic" "no_index"
+end
+
+theory real.Real
+
+  prelude ";;; this is a prelude for smt-lib v2 real arithmetic"
+
+  syntax function zero "0"
+  syntax function one  "1"
+
+  syntax function (+)  "(+ %1 %2)"
+  syntax function (-)  "(- %1 %2)"
+  syntax function ( * )  "(* %1 %2)"
+  syntax function (/)  "(/ %1 %2)"
+  syntax function (-_) "(- %1)"
+  syntax function inv  "(/ 1 %1)"
+
+  syntax predicate (<=) "(<= %1 %2)"
+  syntax predicate (<)  "(< %1 %2)"
+  syntax predicate (>=) "(>= %1 %2)"
+  syntax predicate (>)  "(> %1 %2)"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc
+  remove prop CommutativeGroup.Unit_def_l
+  remove prop CommutativeGroup.Unit_def_r
+  remove prop CommutativeGroup.Inv_def_l
+  remove prop CommutativeGroup.Inv_def_r
+  remove prop Assoc.Assoc
+  remove prop Mul_distr_l
+  remove prop Mul_distr_r
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Inverse
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop ZeroLessOne
+
+  meta "encoding : kept" type real
+
+end
+
+(*
+theory Bool
+   syntax type     bool  "Bool"
+   syntax function True  "true"
+   syntax function False "false"
+   meta "encoding : kept" type bool
+end
+
+theory bool.Bool
+   syntax function andb  "(and %1 %2)"
+   syntax function orb   "(or %1 %2)"
+   syntax function xorb  "(xor %1 %2)"
+   syntax function notb  "(not %1)"
+   syntax function implb "(=> %1 %2)"
+end
+
+theory bool.Ite
+  syntax function ite "(ite %1 %2 %3)"
+  meta "encoding : lskept" function ite
+end
+*)
+
+import "discrimination.gen"

drivers/smt-libv2.drv

@@ -200,6 +200,7 @@ theory bv.BV32
   (* syntax function nth "(= ((_ extract 0 0) (bvlshr %1 ((_ int2bv 32) %2))) #b1)" *)
   (* syntax function nth_bv "(= ((_ extract 0 0) (bvlshr %1 %2)) #b1)" *)
   syntax predicate eq "(= %1 %2)"
+  remove prop Extensionality
 
   syntax predicate slt "(bvslt %1 %2)"
   syntax predicate sle "(bvsle %1 %2)"

examples/in_progress/mp/Makefile

@@ -20,7 +20,7 @@ ifeq ($(BENCH),yes)
 endif
 
 MAIN=main
-GEN=map__Map mp__N
+GEN=map__Map mach__int__UInt32 mp__N
 OBJ=$(GEN) parse
 
 GENML = $(addsuffix .ml, $(GEN))
@@ -46,7 +46,7 @@ $(MAIN).opt: $(CMX)  $(MAIN).cmx
 $(MAIN).cmx: $(CMX)
 
 $(GENML): ../mp.mlw
-	$(WHY3) -E ocaml32 $< -o .
+	$(WHY3) extract -D ocaml32 $< -o .
 
 %.cmx: %.ml
 	$(OCAMLOPT) $(INCLUDE) -annot -c $<
@@ -70,12 +70,12 @@ JSMAIN=jsmain
 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
+$(JSMAIN).js: $(JSMAIN).byte
+	js_of_ocaml +nat.js $(JSMAIN).byte
 
 
 $(JSMAIN).byte: $(CMO) jsmain.ml
-	$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
+	$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg nums.cma why3extract.cma $^
 
 
 %.cmo: %.ml

examples/in_progress/sudoku_reloaded/Makefile

+
+BENCH ?= no
+
+ifeq ($(BENCH),yes)
+  WHY3=../../bin/why3.opt
+  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
+GEN = map__Map sudoku_reloaded__Grid sudoku_reloaded__TheClassicalSudokuGrid sudoku_reloaded__Solver
+OBJ=$(GEN)
+
+GENML = $(addsuffix .ml, $(GEN))
+ML = $(addsuffix .ml, $(OBJ))
+CMO = $(addsuffix .cmo, $(OBJ))
+CMX = $(addsuffix .cmx, $(OBJ))
+
+OCAMLOPT = ocamlopt -noassert -inline 1000
+
+all: $(MAIN).opt
+
+extract: $(GENML)
+
+doc:
+	$(WHY3) doc ../sudoku_reloaded.mlw
+	$(WHY3) session html .
+
+$(MAIN).byte: $(CMO) $(MAIN).cmo
+	ocamlc -g $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ $^
+
+$(MAIN).opt: $(CMX) $(MAIN).cmx
+	$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
+
+$(MAIN).cmx: $(CMX)
+
+$(GENML): ../sudoku_reloaded.mlw
+	$(WHY3) extract -D ocaml32 ../sudoku_reloaded.mlw -o .
+
+# javascript
+
+
+JSMAIN=jsmain
+
+JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
+          -syntax camlp4o
+
+$(JSMAIN).js: $(JSMAIN).byte
+	js_of_ocaml $(JSMAIN).byte
+
+$(JSMAIN).byte: $(CMO) $(JSMAIN).cmo
+	$(JSOCAMLC) $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -o $@ -linkpkg $^
+
+%.cmo: %.ml
+	$(JSOCAMLC) $(INCLUDE) -annot -c $<
+
+%.cmi: %.mli
+	$(JSOCAMLC) $(INCLUDE) -annot -c $<
+
+%.cmx: %.ml
+	$(OCAMLOPT) $(INCLUDE) -annot -c $<
+
+clean::
+	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

examples/in_progress/sudoku_reloaded/index.html

+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
+        "http://www.w3.org/TR/html4/strict.dtd">
+<html>
+  <head>
+    <title>Sudoku Solver using Why3</title>
+    <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
+  </head>
+  <body id="body" style="background-color:#e0e0a0">
+    <h1>Sudoku Solver</h1>
+        <p>This solver was developed and formally proved correct using
+        <a href="http://why3.lri.fr/">Why3</a>, extracted to OCaml and
+        then compiled to JavaScript
+        using <a href="http://ocsigen.org/js_of_ocaml/">Js_of_ocaml</a></p>
+
+    <div id="board"></div>
+    <p>
+      <button id="solve">Solve</button>
+      <button id="reset">Reset</button>
+    </p>
+    <p>
+      <button id="sample1">Example 1</button>
+      <button id="sample2">Example 2</button>
+      <button id="sample3">Example 3 (hard)</button>
+    </p>
+    <script type="text/javascript" src="jsmain.js"></script>
+        <p>See also
+          <ul>
+            <li> The <a href="http://toccata.lri.fr/gallery/sudoku.en.html">Why3 source of this solver</a>
+            <li> A <a href="http://www-sop.inria.fr/marelle/Laurent.Thery/Sudoku/Sudoku.html">Sudoku Solver formally proved using Coq</a>
+          </ul>
+        </p>
+  </body>
+</html>

examples/in_progress/sudoku_reloaded/jsmain.ml

+
+
+module D = Dom_html
+
+let d = D.document
+
+(* Grid Layout *)
+
+let make_board () =
+  let make_input () =
+    let input =
+      D.createInput ~_type:(Js.string "text") ~name:(Js.string "input") d
+    in
+    input##size <- 1;
+    input##maxLength <- 1;
+    input##align <- Js.string "center";
+    let style = input##style in
+    style##border <- Js.string "none";
+    style##fontFamily <- Js.string "monospace";
+    style##fontSize <- Js.string "20px";
+    style##fontWeight <- Js.string "bold";
+    style##paddingBottom <- Js.string "5px";
+    style##paddingTop <- Js.string "5px";
+    style##paddingLeft <- Js.string "10px";
+    style##paddingRight <- Js.string "10px";
+    let enforce_digit _ =
+      begin
+        match Js.to_string input##value with
+        | "1" | "2" | "3" | "4" | "5"
+        | "6" | "7" | "8" | "9" -> ()
+        | _ -> input##value <- Js.string ""
+      end;
+      Js._false
+    in
+    input##onchange <- Dom_html.handler enforce_digit;
+    input
+  in
+  let make_td i j input =
+    let td = D.createTd d in
+    td##align <- Js.string "center";
+    let style = td##style in
+    style##borderStyle <- Js.string "solid";
+    style##borderColor <- Js.string "#000000";
+    let widths = function
+      | 0 -> 3, 0 | 2 -> 1, 1 | 3 -> 1, 0
+      | 5 -> 1, 1 | 6 -> 1, 0 | 8 -> 1, 3
+      | _ -> 1, 0 in
+    let (top, bottom) = widths i in
+    let (left, right) = widths j in
+    let px k = Js.string (string_of_int k ^ "px") in
+    style##borderTopWidth <- px top;
+    style##borderBottomWidth <- px bottom;
+    style##borderLeftWidth <- px left;
+    style##borderRightWidth <- px right;
+    Dom.appendChild td input;
+    td
+  in
+  let rows = Array.init 9 (fun i -> Array.init 9 (fun j -> make_input ())) in
+  let table = D.createTable d in
+  table##cellPadding <- Js.string "0px";
+  table##cellSpacing <- Js.string "0px";
+  let tbody = D.createTbody d in
+  Dom.appendChild table tbody;
+  ArrayLabels.iteri rows ~f:(fun i row ->
+    let tr = D.createTr d in
+    ArrayLabels.iteri row ~f:(fun j cell ->
+      let td = make_td i j cell in
+      ignore (Dom.appendChild tr td));
+    ignore (Dom.appendChild tbody tr));
+  (rows, table)
+
+
+(* Solver *)
+
+open Why3extract
+
+let display_sol rows a =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      cell##value <- Js.string (string_of_int a.(9*i+j));
+      cell##style##backgroundColor <- Js.string "#ffffff"
+    done
+  done
+
+let no_sol rows =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      cell##style##backgroundColor <- Js.string "#ff0000"
+    done
+  done
+
+let solve_board rows _ =
+  let sudoku = Sudoku_reloaded__TheClassicalSudokuGrid.classical_sudoku () in
+  let input_grid = Array.make 81 0 in
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      let v =
+        match Js.to_string cell##value with
+        | "" -> 0
+        | s -> Char.code s.[0] - Char.code '0'
+      in
+      input_grid.(9*i+j) <- v
+    done
+  done;
+  begin
+    try
+      let a = Sudoku_reloaded__Solver.check_then_solve sudoku input_grid in
+      display_sol rows a
+    with Sudoku_reloaded__Solver.NoSolution -> no_sol rows
+  end;
+  Js._false
+
+(* reset board to empty cells *)
+
+let reset_board rows _ =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      cell##value <- Js.string "";
+      cell##style##backgroundColor <- Js.string "#ffffff";
+    done
+  done;
+  Js._false
+
+(* load examples *)
+
+let load_board rows test _ =
+  for i=0 to 8 do
+    for j=0 to 8 do
+      let cell = rows.(i).(j) in
+      let v = test.(9*i+j) in
+      let v = if v = 0 then "" else string_of_int v in
+      cell##value <- Js.string v;
+      cell##style##backgroundColor <- Js.string "#ffffff";
+    done
+  done;
+  Js._false
+
+let test1 =
+[| 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 |]
+
+let test2 =
+[| 7;0;0;0;0;0;0;0;8;
+   0;9;0;7;0;6;0;3;0;
+   0;0;1;0;0;0;9;0;0;
+   0;7;0;1;0;4;0;5;0;
+   0;0;0;0;6;0;0;0;0;
+   0;5;0;3;0;7;0;1;0;
+   0;0;2;0;0;0;1;0;0;
+   0;1;0;9;0;8;0;7;0;
+   8;0;0;0;0;0;0;0;6 |]
+
+let test3 =
+[| 0;0;0;0;0;0;0;0;0;
+   0;0;0;0;0;3;0;8;5;
+   0;0;1;0;2;0;0;0;0;
+   0;0;0;5;0;7;0;0;0;
+   0;0;4;0;0;0;1;0;0;
+   0;9;0;0;0;0;0;0;0;
+   5;0;0;0;0;0;0;7;3;
+   0;0;2;0;1;0;0;0;0;
+   0;0;0;0;4;0;0;0;9 |]
+
+let onload (_event : #Dom_html.event Js.t) : bool Js.t =
+  let (rows, table) = make_board () in
+  let solve = Js.Opt.get (d##getElementById (Js.string "solve"))
+    (fun () -> assert false) in
+  solve##onclick <- Dom_html.handler (solve_board rows);
+  let reset = Js.Opt.get (d##getElementById (Js.string "reset"))
+    (fun () -> assert false) in
+  reset##onclick <- Dom_html.handler (reset_board rows);
+  let sample1 = Js.Opt.get (d##getElementById (Js.string "sample1"))
+    (fun () -> assert false) in
+  sample1##onclick <- Dom_html.handler (load_board rows test1);
+  let sample2 = Js.Opt.get (d##getElementById (Js.string "sample2"))
+    (fun () -> assert false) in
+  sample2##onclick <- Dom_html.handler (load_board rows test2);
+  let sample3= Js.Opt.get (d##getElementById (Js.string "sample3"))
+    (fun () -> assert false) in
+  sample3##onclick <- Dom_html.handler (load_board rows test3);
+  let board = Js.Opt.get (d##getElementById (Js.string "board"))
+    (fun () -> assert false) in
+  Dom.appendChild board table;
+  board##style##padding <- Js.string "40px";
+  Js._false
+
+let _ = Dom_html.window##onload <- Dom_html.handler onload

examples/in_progress/sudoku_reloaded/main.ml

+
+open Why3extract
+open Format
+
+let usage () =
+  eprintf "Sudoku: solve a Sudoku puzzle@.";
+  eprintf "Usage: %s <comma separated sequence of 81 non-zero digits>@." Sys.argv.(0);
+  exit 2
+
+let input =
+  if Array.length Sys.argv <> 2 then usage ();
+  Sys.argv.(1)
+
+let input_grid =
+  if String.length input <> 161 then usage ();
+  for i=0 to 79 do
+    if input.[i+i+1] <> ',' then usage ();
+  done;
+  let a = Array.make 81 0 in
+  for i=0 to 80 do
+    match input.[i+i] with
+      | '0'..'9' as c -> a.(i) <- Char.code c - Char.code '0'
+      | _ -> usage ()
+  done;
+  a
+
+let print_grid fmt a =
+  fprintf fmt "@[";
+  for i=0 to 80 do
+    if i mod 9 = 8
+    then fprintf fmt "%d@\n" a.(i)
+    else fprintf fmt "%d " a.(i)
+  done;
+  fprintf fmt "@]"
+
+let () =
+  let sudoku = Sudoku_reloaded__TheClassicalSudokuGrid.classical_sudoku () in
+  printf "Problem: %a@." print_grid input_grid;
+  let a = Sudoku_reloaded__Solver.solve sudoku input_grid
+  in
+  printf "Solution: %a@." print_grid a
+
+(*
+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
+1 8 7 9 6 4 5 3 2
+4 5 3 8 1 2 7 6 9
+3 7 5 6 4 9 2 8 1
+9 2 8 1 7 5 6 4 3
+6 4 1 2 3 8 9 5 7
+7 1 4 5 9 6 3 2 8
+8 3 6 7 2 1 4 9 5
+5 9 2 4 8 3 1 7 6
+
+Other tests:
+
+0,0,0,0,0,0,0,0,0,0,0,0,0,0,3,0,8,5,0,0,1,0,2,0,0,0,0,0,0,0,5,0,7,0,0,0,0,0,4,0,0,0,1,0,0,0,9,0,0,0,0,0,0,0,5,0,0,0,0,0,0,7,3,0,0,2,0,1,0,0,0,0,0,0,0,0,4,0,0,0,9
+
+*)

examples/linked_list_rev.mlw

 
-(*
 
-In-place linked list reversal.
+(**
+
+{1 In-place linked list reversal }
 
-Version designed for the MPRI lecture http://www.lri.fr/~marche/MPRI-2-36-1/
+Version designed for the {h <a href="http://www.lri.fr/~marche/MPRI-2-36-1/">MPRI lecture ``Proof of Programs''</a>}
+
+This is an improved version of {h <a href="linked_list_rev.html">this
+one</a>}: it does not use any Coq proofs, but lemma functions instead.
 
 *)
 
-theory ListReverse
+
+module Disjoint