Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit a3e4a012 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Try Why3: working around some simple uses of Str

parent c1eae8fa
......@@ -1435,8 +1435,8 @@ src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
src/trywhy3/trywhy3.byte: lib/why3/why3.cma src/trywhy3/theories.cmo src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/theories.ml: src/trywhy3/gentheories.ml
ocaml src/trywhy3/gen_theories.ml
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 $<
......
......@@ -15,15 +15,23 @@ open Term
(* explanations *)
(*******************************)
(*
let expl_regexp = Str.regexp "expl:\\(.*\\)"
*)
let collect_expls lab =
Ident.Slab.fold
(fun lab acc ->
let lab = lab.Ident.lab_string in
(*
if Str.string_match expl_regexp lab 0
then Str.matched_group 1 lab :: acc
else acc)
else acc
*)
try
let s = Lexlib.remove_prefix "expl:" lab in s :: acc
with Not_found -> acc)
lab
[]
......
(*
#load "unix.cma"
#directory "../util"
#load "sysutil.cmo"
*)
open Format
let gen_dir fmt d suffix =
let dir = "../.." ^ d in
let dir = "." ^ d in
let t = Sys.readdir dir in
for i = 0 to Array.length t - 1 do
let file = t.(i) in
......
......@@ -50,9 +50,8 @@ let html_of_string (s:string) =
d##createElement (Js.string "p") <|
[node (d##createTextNode (Js.string s))]
let replace_child p n =
Js.Opt.iter (p##firstChild) (fun c -> Dom.removeChild p c);
Dom.appendChild p n
let rec removeChildren p =
Js.Opt.iter (p##lastChild) (fun c -> Dom.removeChild p c; removeChildren p)
let temp_file_name = "/input.mlw"
......@@ -67,7 +66,7 @@ open Why3
XmlHttpRequest.get
*)
let env = Env.create_env ["/theories" (*; "/modules"*)]
let env = Env.create_env ["/theories" ; "/modules"]
(*
let bad_suffix path name =
......@@ -98,25 +97,47 @@ let run textbox preview (_ : D.mouseEvent Js.t) : bool Js.t =
let ch = open_out temp_file_name in
output_string ch text;
close_out ch;
let answer =
let answer = ref [] in
let push_answer s = answer := s :: !answer in
begin
try
let x = Env.read_file Env.base_language env temp_file_name in
Pp.sprintf "parsing and typing OK, %d theories"
(Stdlib.Mstr.cardinal x)
push_answer
(Pp.sprintf "parsing and typing OK, %d theories"
(Stdlib.Mstr.cardinal x));
Stdlib.Mstr.iter
(fun _thname th ->
let tasks = Task.split_theory th None None in
List.iter
(fun task ->
let (id,expl,_) = Termcode.goal_expl_task ~root:true task in
let expl = match expl with
| Some s -> s
| None -> id.Ident.id_string
in
push_answer
(Pp.sprintf "Goal: %s@\n" expl))
tasks)
x
with
| Loc.Located(loc,Parser.Error) ->
let (_,l,b,e) = Loc.get loc in
Pp.sprintf "syntax error line %d, columns %d-%d" l b e
push_answer
(Pp.sprintf "syntax error line %d, columns %d-%d" l b e)
| Loc.Located(loc,e') ->
let (_,l,b,e) = Loc.get loc in
Pp.sprintf
"error line %d, columns %d-%d: %a" l b e Exn_printer.exn_printer e'
push_answer
(Pp.sprintf
"error line %d, columns %d-%d: %a" l b e Exn_printer.exn_printer e')
| e ->
Pp.sprintf
"unexpected exception: %a (%s)" Exn_printer.exn_printer e
(Printexc.to_string e)
in
replace_child preview (html_of_string answer);
push_answer
(Pp.sprintf
"unexpected exception: %a (%s)" Exn_printer.exn_printer e
(Printexc.to_string e))
end;
removeChildren preview;
List.iter
(fun s -> Dom.appendChild preview (html_of_string s)) (List.rev !answer);
Js._false
let onload (_event : #Dom_html.event Js.t) : bool Js.t =
......
......@@ -22,3 +22,10 @@ val update_loc : Lexing.lexbuf -> string option -> int -> int -> unit
val remove_leading_plus : string -> string
val remove_underscores : string -> string
val has_prefix : string -> string -> bool
(** [has_prefix pref s] returns true if s [s] starts with prefix [pref] *)
val remove_prefix : string -> string -> string
(** [remove_prefix pref s] removes the prefix [pref] from [s]. Raises
[Not_found if [s] does not start with [pref] *)
......@@ -103,4 +103,19 @@ and string = parse
String.iter (fun c -> if c <> '_' then (Strings.set t !i c; incr i)) s;
t
end else s
let has_prefix pref s =
let l = String.length pref in
if String.length s < l then false else
try
for i = 0 to l - 1 do if s.[i] <> pref.[i] then raise Exit done;
true
with Exit -> false
let remove_prefix pref s =
let l = String.length pref in
if String.length s < l then raise Not_found else
for i = 0 to l - 1 do if s.[i] <> pref.[i] then raise Not_found done;
String.sub s l (String.length s - l)
}
......@@ -138,10 +138,14 @@ let expl_loopvar = Ident.create_label "expl:loop variant decrease"
let expl_variant = Ident.create_label "expl:variant decrease"
let lab_has_expl =
(*
let expl_regexp = Str.regexp "expl:\\(.*\\)" in
*)
Slab.exists
(fun l ->
(fun l -> Lexlib.has_prefix "expl:" l.lab_string)
(*
Str.string_match expl_regexp l.lab_string 0)
*)
let rec wp_expl l f =
if lab_has_expl f.t_label then f
......
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