Commit a1c7f4da authored by MARCHE Claude's avatar MARCHE Claude

Replacing some use of Str library by handwritten code

Incidentally, Try Why3 is now able to produce Alt-Ergo goals
parent 5459a06b
......@@ -74,82 +74,141 @@ let () = register_printer
(** Syntax substitutions *)
(*
let opt_search_forward re s pos =
try Some (Str.search_forward re s pos) with Not_found -> None
*)
let global_substitute_fmt expr repl_fun text fmt =
let rec replace start last_was_empty =
let startpos = if last_was_empty then start + 1 else start in
if startpos > String.length text then
pp_print_string fmt (Str.string_after text start)
else
match opt_search_forward expr text startpos with
| None ->
pp_print_string fmt (Str.string_after text start)
| Some pos ->
let end_pos = Str.match_end () in
pp_print_string fmt (String.sub text start (pos - start));
repl_fun text fmt;
replace end_pos (end_pos = pos)
(* specialized version of opt_search_forward, searching for strings
matching '%' [tv]? [0-9]+ [search_forward s pos] search from
starting position [pos], in the string [s], and returns either None
if no substrings match, or [Some(b,e)] if the substring between
positions [b] included and [e] excluded matches (without the leading '%').
*)
let is_digit ch = match ch with '0'..'9' -> true | _ -> false
let opt_search_forward s pos =
let l = String.length s in
let b = ref pos in
let i = ref pos in
try
while !i < l-1 do
if s.[!i] = '%' then begin
incr i;
b := !i;
begin match s.[!i] with
| 't' | 'v' -> incr i
| _ -> ()
end;
let e = !i in
while !i < l && is_digit s.[!i] do incr i done;
if !i > e then raise Exit
end;
incr i
done;
None
with Exit -> Some(!b,!i)
(*
let _ = opt_search_forward "%1 + %2" 0
let _ = opt_search_forward "%1 + %2" 2
let _ = opt_search_forward "%1 + %2" 7
let _ = opt_search_forward "%t1 + %v42" 0
let _ = opt_search_forward "%t1 + %v42" 2
let s = "<app><const name=\"HOL.eq\"/>%1%2</app>"
let Some(b,e) = opt_search_forward s 0
let t = String.sub s b (e-b)
open Format
*)
let global_substitute_fmt repl_fun text fmt =
let len = String.length text in
let rec replace start =
match opt_search_forward text start with
| None ->
pp_print_string fmt (String.sub text start (len - start))
| Some(pos,end_pos) ->
pp_print_string fmt (String.sub text start (pos - start - 1));
repl_fun text pos end_pos fmt;
replace end_pos
in
replace 0 false
replace 0
(*
let repl s e b fmt = fprintf fmt "A"
let iter_group expr iter_fun text =
let () =
global_substitute_fmt repl "(LAMBDA (x:%v0): %1)" std_formatter;
fprintf std_formatter "@."
*)
let iter_group iter_fun text =
let rec iter start last_was_empty =
let startpos = if last_was_empty then start + 1 else start in
if startpos < String.length text then
match opt_search_forward expr text startpos with
match opt_search_forward text startpos with
| None -> ()
| Some pos ->
let end_pos = Str.match_end () in
iter_fun text;
| Some (pos,end_pos) ->
iter_fun text pos end_pos;
iter end_pos (end_pos = pos)
in
iter 0 false
(*
let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"
let regexp_arg_pos_typed = Str.regexp "%\\([tv]?[0-9]+\\)"
*)
exception BadSyntaxIndex of int
exception BadSyntaxArity of int * int
let int_of_string s =
try int_of_string s
with _ ->
Format.eprintf "bad argument for int_of_string : %s@." s;
assert false
let check_syntax s len =
let arg s =
let i = int_of_string (Str.matched_group 1 s) in
let arg s b e =
let i = int_of_string (String.sub s b (e-b)) in
if i <= 0 then raise (BadSyntaxIndex i);
if i > len then raise (BadSyntaxArity (len,i));
()
in
iter_group regexp_arg_pos arg s
iter_group (*regexp_arg_pos*) arg s
let check_syntax_logic ls s =
let len = List.length ls.ls_args in
let ret = ls.ls_value <> None in
let nfv = Stv.cardinal (ls_ty_freevars ls) in
let arg s =
let grp = (Str.matched_group 1 s) in
if grp.[0] = 't' then begin
let grp = String.sub grp 1 (String.length grp - 1) in
let arg s b e =
if s.[b] = 't' then begin
let grp = String.sub s (b+1) (e-b-1) in
let i = int_of_string grp in
if i < 0 || (not ret && i = 0) then raise (BadSyntaxIndex i);
if i > len then raise (BadSyntaxArity (len,i))
end else if grp.[0] = 'v' then begin
let grp = String.sub grp 1 (String.length grp - 1) in
end else if s.[b] = 'v' then begin
let grp = String.sub s (b+1) (e-b-1) in
let i = int_of_string grp in
if i < 0 || i >= nfv then raise (BadSyntaxIndex i)
end else begin
let grp = String.sub s b (e-b) in
let i = int_of_string grp in
if i <= 0 then raise (BadSyntaxIndex i);
if i > len then raise (BadSyntaxArity (len,i));
end
in
iter_group regexp_arg_pos_typed arg s
iter_group (*regexp_arg_pos_typed*) arg s
let syntax_arguments s print fmt l =
let args = Array.of_list l in
let repl_fun s fmt =
let i = int_of_string (Str.matched_group 1 s) in
let repl_fun s b e fmt =
let i = int_of_string (String.sub s b (e-b)) in
print fmt args.(i-1) in
global_substitute_fmt regexp_arg_pos repl_fun s fmt
global_substitute_fmt (*regexp_arg_pos*) repl_fun s fmt
(* return the type arguments of a symbol application, sorted according
to their (formal) names *)
......@@ -166,22 +225,22 @@ let get_type_arguments t = match t.t_node with
let gen_syntax_arguments_typed ty_of tys_of s print_arg print_type t fmt l =
let args = Array.of_list l in
let repl_fun s fmt =
let grp = (Str.matched_group 1 s) in
if grp.[0] = 't' then
let grp = String.sub grp 1 (String.length grp - 1) in
let repl_fun s b e fmt =
if s.[b] = 't' then
let grp = String.sub s (b+1) (e-b-1) in
let i = int_of_string grp in
if i = 0
then print_type fmt (ty_of t)
else print_type fmt (ty_of args.(i-1))
else if grp.[0] = 'v' then
let grp = String.sub grp 1 (String.length grp - 1) in
else if s.[b] = 'v' then
let grp = String.sub s (b+1) (e-b-1) in
let m = tys_of t in
print_type fmt m.(int_of_string grp)
else
let grp = String.sub s b (e-b) in
let i = int_of_string grp in
print_arg fmt args.(i-1) in
global_substitute_fmt regexp_arg_pos_typed repl_fun s fmt
global_substitute_fmt (*regexp_arg_pos_typed*) repl_fun s fmt
let syntax_arguments_typed =
gen_syntax_arguments_typed t_type get_type_arguments
......
......@@ -316,7 +316,7 @@ let rec print_term info fmt t =
ls.ls_name.id_label
| Some _ ->
model_trace_for_postcondition ~labels:ls.ls_name.id_label info in
let t_check_pos = t_label ~loc labels t in
let _t_check_pos = t_label ~loc labels t in
(* TODO: temporarily disable collecting variables inside the term triggering VC *)
(*info.info_model <- S.add t_check_pos info.info_model;*)
()
......
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