Try Why3: inclusion of stdlib file at compile time + produce tasks for alt-ergo

Makefile.in

@@ -1430,14 +1430,14 @@ JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
            -syntax camlp4o -I src/trywhy3
 
 src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
-	js_of_ocaml +weak.js +nat.js $^
+	js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=why3.conf:/ \
+		--file=alt_ergo.drv:/ \
+		`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+		+weak.js +nat.js $^
 
-src/trywhy3/trywhy3.byte: lib/why3/why3.cma  src/trywhy3/theories.cmo src/trywhy3/trywhy3.cmo
+src/trywhy3/trywhy3.byte: lib/why3/why3.cma src/trywhy3/trywhy3.cmo
 	$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
 
-src/trywhy3/theories.ml: src/trywhy3/gen_theories.ml
-	ocaml -I src/util unix.cma sysutil.cmo src/trywhy3/gen_theories.ml
-
 src/trywhy3/%.cmo: src/trywhy3/%.ml
 	$(JSOCAMLC) $(BFLAGS) -c $<
 
@@ -1445,7 +1445,9 @@ src/trywhy3/%.cmi: src/trywhy3/%.mli
 	$(JSOCAMLC) $(BFLAGS) -c $<
 
 clean::
-	rm -f src/trywhy3/trywhy3.byte
+	rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte
+
+CLEANDIRS += src/trywhy3
 
 ########
 # bench

src/trywhy3/alt_ergo.drv

+(* Driver for Alt-Ergo version >= 0.95 *)
+
+prelude "(* this is the prelude for Alt-Ergo, any versions *)"
+
+printer "alt-ergo"
+filename "%f-%t-%g.why"
+
+valid "Valid"
+invalid "Invalid"
+unknown "I don't know" ""
+timeout "Timeout"
+steplimitexceeded "Steps limit reached"
+outofmemory "Fatal error: out of memory"
+outofmemory "Fatal error: exception Stack_overflow"
+fail "typing error:\\(.*\\)$" "Failure : File generation error : \\1"
+(*
+time "Valid (%s)"
+time "Valid (%s)"
+steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\))" 2
+steps "Valid (\\([0-9]+.?[0-9]*\\)) (\\([0-9]+.?[0-9]*\\) steps)" 2
+time "why3cpulimit time : %s s"
+*)
+
+(* À discuter *)
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_recursion"
+transformation "eliminate_inductive"
+transformation "eliminate_algebraic"
+transformation "eliminate_epsilon"
+transformation "eliminate_if"
+transformation "eliminate_let"
+
+transformation "split_premise_right"
+transformation "simplify_formula"
+(*transformation "simplify_trivial_quantification_in_goal"*)
+
+theory BuiltIn
+  syntax type int   "int"
+  syntax type real  "real"
+
+  syntax predicate (=)  "(%1 = %2)"
+end
+
+theory int.Int
+
+  prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
+
+  syntax function zero "0"
+  syntax function one  "1"
+
+  syntax function (+)  "(%1 + %2)"
+  syntax function (-)  "(%1 - %2)"
+  syntax function (*)  "(%1 * %2)"
+  syntax function (-_) "(-%1)"
+
+  meta "invalid trigger" predicate (<=)
+  meta "invalid trigger" predicate (<)
+  meta "invalid trigger" predicate (>=)
+  meta "invalid trigger" predicate (>)
+
+  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 Refl
+  remove prop Trans
+  remove prop Total
+  remove prop Antisymm
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop ZeroLessOne
+
+end
+
+
+theory real.Real
+
+  prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
+
+  syntax function zero "0.0"
+  syntax function one  "1.0"
+
+  syntax function (+)  "(%1 + %2)"
+  syntax function (-)  "(%1 - %2)"
+  syntax function (*)  "(%1 * %2)"
+  syntax function (/)  "(%1 / %2)"
+  syntax function (-_) "(-%1)"
+  syntax function inv  "(1.0 / %1)"
+
+  meta "invalid trigger" predicate (<=)
+  meta "invalid trigger" predicate (<)
+  meta "invalid trigger" predicate (>=)
+  meta "invalid trigger" predicate (>)
+
+  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 Refl
+  remove prop Trans
+  remove prop Total
+  remove prop Antisymm
+  remove prop Inverse
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop ZeroLessOne
+
+end
+
+theory real.RealInfix
+
+  syntax function (+.)  "(%1 + %2)"
+  syntax function (-.)  "(%1 - %2)"
+  syntax function ( *.) "(%1 * %2)"
+  syntax function (/.)  "(%1 / %2)"
+  syntax function (-._) "(-%1)"
+
+  meta "invalid trigger" predicate (<=.)
+  meta "invalid trigger" predicate (<.)
+  meta "invalid trigger" predicate (>=.)
+  meta "invalid trigger" predicate (>.)
+
+  syntax predicate (<=.) "(%1 <= %2)"
+  syntax predicate (<.)  "(%1 <  %2)"
+  syntax predicate (>=.) "(%1 >= %2)"
+  syntax predicate (>.)  "(%1 >  %2)"
+
+end
+
+theory Bool
+  syntax type     bool  "bool"
+  syntax function True  "true"
+  syntax function False "false"
+end
+
+theory Tuple0
+  syntax type     tuple0 "unit"
+  syntax function Tuple0 "void"
+end
+
+theory algebra.AC
+  meta AC function op
+  remove prop Comm.Comm
+  remove prop Assoc
+end
+
+theory map.Map
+  syntax type  map "(%1,%2) farray"
+
+  syntax function get "(%1[%2])"
+  syntax function set "(%1[%2 <- %3])"
+
+  remove prop Select_eq
+  remove prop Select_neq
+end
+
+
+theory BuiltIn
+
+  (* Alt-Ergo >= 0.95 supports enumerated datatypes and records *)
+
+  meta "eliminate_algebraic" "keep_enums"
+  meta "eliminate_algebraic" "keep_recs"
+
+end
+
+
+theory int.EuclideanDivision
+
+  (* protection against wrong semantics for negative arguments
+    last checked on 0.99.1: this is still needed
+  *)
+
+  prelude "logic safe_eucl_div: int, int -> int"
+  prelude "axiom safe_eucl_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_div(x,y) = x / y"
+
+  prelude "logic safe_eucl_mod: int, int -> int"
+  prelude "axiom safe_eucl_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_eucl_mod(x,y) = x % y"
+
+  syntax function div "safe_eucl_div(%1,%2)"
+  syntax function mod "safe_eucl_mod(%1,%2)"
+
+end
+
+theory int.ComputerDivision
+
+  (* protection against wrong semantics for negative arguments
+     last checked on 0.99.1: this is still needed
+  *)
+
+  prelude "logic safe_comp_div: int, int -> int"
+  prelude "axiom safe_comp_div_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_div(x,y) = x / y"
+
+  prelude "logic safe_comp_mod: int, int -> int"
+  prelude "axiom safe_comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> safe_comp_mod(x,y) = x % y"
+
+  syntax function div "safe_comp_div(%1,%2)"
+  syntax function mod "safe_comp_mod(%1,%2)"
+
+end
+
+
+(*
+Local Variables:
+mode: why
+compile-command: "make -C .. bench"
+End:
+*)

src/trywhy3/gen_theories.ml

-
-(*
-#load "unix.cma"
-#directory "../util"
-#load "sysutil.cmo"
-*)
-
-open Format
-
-let gen_dir fmt d suffix =
-  let dir = "." ^ d in
-  let t = Sys.readdir dir in
-  for i = 0 to Array.length t - 1 do
-    let file = t.(i) in
-    let f = Filename.concat dir file in
-    if Filename.check_suffix f suffix then
-      let c = String.escaped (Sysutil.file_contents f) in
-      fprintf fmt "\"%s/%s\",@\n\"%s@\n\";@\n" d file c
-  done
-
-let () =
-  let ch = open_out "src/trywhy3/theories.ml" in
-  let fmt = formatter_of_out_channel ch in
-  fprintf fmt "(* generated by gen_theories.ml *)@\n@\n";
-  fprintf fmt "let theories = [@\n";
-  gen_dir fmt "/theories" ".why";
-  gen_dir fmt "/modules" ".mlw";
-  gen_dir fmt "/modules/mach" ".mlw";
-  fprintf fmt "]@\n";
-  close_out ch

src/trywhy3/trywhy3.ml

@@ -58,11 +58,13 @@ end
 
 (** registering the std lib *)
 
+(*
 let () =
   List.iter
     (fun (name,content) ->
       Sys_js.register_file ~name ~content;
     ) Theories.theories
+*)
 
 
 (** Rendering in the browser *)
@@ -95,45 +97,52 @@ let ul nl =
 end
 
 let temp_file_name = "/input.mlw"
+let why3_conf_file = "/why3.conf"
 
 let () =
-  Sys_js.register_file ~name:temp_file_name ~content:"";
+  Sys_js.register_file ~name:temp_file_name ~content:""
 
 open Why3
-
-(* TODO: loading from standard library.
-
-   piste: utiliser Sys_js.register_autoload et
-   XmlHttpRequest.get
-
-*)
-let env = Env.create_env ["/theories" ; "/modules"]
-
-(*
-let bad_suffix path name =
-  match path with
-  | "/theories" -> not (Filename.check_suffix name ".why")
-  | "/modules" -> not (Filename.check_suffix name ".mlw")
-  | _ -> true
-
-let load_file_from_the_web (path,name) =
-  if bad_suffix path name then None else
-  let t = XmlHttpRequest.get
-    ("http://why3.lri.fr/try" ^ path ^ "/" ^ name)
-  in
-  let c = ref "" in
-  Lwt.on_success t
-    (fun frame ->
-      let content = frame. XmlHttpRequest.content in
-      (* useless ?
-         Sys_js.register_file ~name:(path ^ "/" ^ name) ~content; *)
-      c := content);
-  Some !c
-
-let () = Sys_js.register_autoload ~path:"/theories" load_file_from_the_web
-*)
-
-let split_trans = Why3.Trans.lookup_transform_l "split_goal_wp" env
+open Format
+
+(* reads the config file *)
+let config : Whyconf.config = Whyconf.read_config (Some why3_conf_file)
+(* the [main] section of the config file *)
+let main : Whyconf.main = Whyconf.get_main config
+(* all the provers detected, from the config file *)
+let provers : Whyconf.config_prover Whyconf.Mprover.t =
+  Whyconf.get_provers config
+
+(* One prover named Alt-Ergo in the config file *)
+let alt_ergo : Whyconf.config_prover =
+  if Whyconf.Mprover.is_empty provers then begin
+    eprintf "Prover Alt-Ergo not installed or not configured@.";
+    exit 0
+  end else snd (Whyconf.Mprover.choose provers)
+
+(* builds the environment from the [loadpath] *)
+let env : Env.env = Env.create_env (Whyconf.loadpath main)
+
+
+let alt_ergo_driver : Driver.driver =
+  try
+    Printexc.record_backtrace true;
+    Driver.load_driver env alt_ergo.Whyconf.driver []
+  with e ->
+    let s = Printexc.get_backtrace () in
+    eprintf "Failed to load driver for alt-ergo: %a@.%s@."
+      Exn_printer.exn_printer e s;
+  exit 1
+
+
+let run_alt_ergo_on_task t =
+  (* printing the task in a string *)
+  Driver.print_task alt_ergo_driver str_formatter t;
+  let text = flush_str_formatter () in
+  (* TODO ! *)
+  text
+
+let split_trans = Trans.lookup_transform_l "split_goal_wp" env
 
 let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
   let text = Js.to_string (textbox##value) in
@@ -142,6 +151,7 @@ let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
   close_out ch;
   let answer =
     try
+      (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
       let theories = Env.read_file Env.base_language env temp_file_name in
 (*
       Html.par
@@ -167,14 +177,15 @@ let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
                     | Some s -> s
                     | None -> id.Ident.id_string
                   in
-                  [Html.of_string ("Goal: " ^ expl)])
+                  let result = run_alt_ergo_on_task task in
+                  [Html.of_string (expl ^" : " ^ result)])
                 tasks
             in
             [ Html.of_string ("Theory " ^ thname); Html.ul tasks]
             :: acc)
           theories []
       in
-      Html.par [Html.ul theories]
+      Html.ul theories
 (*
       Stdlib.Mstr.iter
         (fun _thname th ->
@@ -236,7 +247,7 @@ let onload (_event : #Dom_html.event Js.t) : bool Js.t =
       b##onclick <-
         D.handler
         (fun (_ : D.mouseEvent Js.t) ->
-          textbox##textContent <- Js.some (Js.string text);
+          textbox##value <- Js.string text;
           Js._false))
     examples;
   Dom.appendChild output (D.createBr Html.d);

src/trywhy3/why3.conf

+[main]
+cntexample = false
+loadpath = "/theories"
+loadpath = "/modules"
+magic = 14
+memlimit = 1000
+running_provers_max = 2
+timelimit = 5
+
+[prover]
+command = "%l/why3-cpulimit %T %m -s alt-ergo-0.99.1 -timelimit %t %f"
+command_steps = "%l/why3-cpulimit %U %m -s alt-ergo-0.99.1 -steps-bound %S %f"
+driver = "/alt_ergo.drv"
+editor = "altgr-ergo"
+in_place = false
+interactive = false
+name = "Alt-Ergo"
+shortcut = "altergo"
+shortcut = "alt-ergo"
+version = "0.99.1"