Commit 7db57db6 authored by David Hauzar's avatar David Hauzar

Merge branch 'counter-examples' of...

Merge branch 'counter-examples' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3 into counter-examples
parents 6b21ff73 69de5f30
...@@ -31,21 +31,27 @@ let concat_expls = function ...@@ -31,21 +31,27 @@ let concat_expls = function
| [l] -> Some l | [l] -> Some l
| l :: ls -> Some (l ^ " (" ^ String.concat ". " ls ^ ")") | l :: ls -> Some (l ^ " (" ^ String.concat ". " ls ^ ")")
let rec get_expls_fmla acc f =
let search_labels callback =
let rec aux acc f =
if f.t_ty <> None then acc if f.t_ty <> None then acc
else if Ident.Slab.mem Split_goal.stop_split f.Term.t_label then acc else if Ident.Slab.mem Split_goal.stop_split f.Term.t_label then acc
else else
let res = collect_expls f.Term.t_label in let res = callback f.Term.t_label in
if res = [] then match f.t_node with if res = [] then match f.t_node with
| Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc | Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc
| Term.Tbinop (Term.Timplies, _, f) -> get_expls_fmla acc f | Term.Tbinop (Term.Timplies, _, f) -> aux acc f
| Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) -> | Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) ->
Term.t_fold get_expls_fmla acc f Term.t_fold aux acc f
| _ -> raise Exit | _ -> raise Exit
else if acc = [] then res else if acc = [] then res
else raise Exit else raise Exit
in
aux []
let get_expls_fmla f = try get_expls_fmla [] f with Exit -> [] let get_expls_fmla =
let search = search_labels collect_expls in
fun f -> try search f with Exit -> []
let goal_expl_task ~root task = let goal_expl_task ~root task =
let gid = (Task.task_goal task).Decl.pr_name in let gid = (Task.task_goal task).Decl.pr_name in
......
...@@ -14,6 +14,14 @@ ...@@ -14,6 +14,14 @@
val goal_expl_task: val goal_expl_task:
root:bool -> Task.task -> Ident.ident * string option * Task.task root:bool -> Task.task -> Ident.ident * string option * Task.task
val search_labels :
(Ident.Slab.t -> 'a list) -> Term.term -> 'a list
(* [search_labels callback f] traverses [f] in a top-down manner and calls the
[callback] on the label set of all encountered nodes. As soon as the
callback returns a non-empty list, the traversal is stopped and that list
is returned. Raises exception Exit if the entire term has been traversed.
*)
(** Shapes *) (** Shapes *)
val reset_dict : unit -> unit val reset_dict : unit -> unit
......
...@@ -194,12 +194,6 @@ let () = Trans.register_transform "intro_vc_vars_counterexmp" ...@@ -194,12 +194,6 @@ let () = Trans.register_transform "intro_vc_vars_counterexmp"
intro_vc_vars_counterexmp intro_vc_vars_counterexmp
~desc:"Introduce." ~desc:"Introduce."
let rec string_join sep l =
match l with
| [] -> ""
| [x] -> x
| x :: rest -> x ^ sep ^ string_join sep rest
let get_location_of_vc task = let get_location_of_vc task =
let meta_args = Task.on_meta_excl meta_vc_location task in let meta_args = Task.on_meta_excl meta_vc_location task in
match meta_args with match meta_args with
...@@ -214,7 +208,7 @@ let get_location_of_vc task = ...@@ -214,7 +208,7 @@ let get_location_of_vc task =
let line = int_of_string line in let line = int_of_string line in
let col1 = int_of_string col1 in let col1 = int_of_string col1 in
let col2 = int_of_string col2 in let col2 = int_of_string col2 in
let filename = string_join ":" (List.rev rest) in let filename = Strings.join ":" (List.rev rest) in
Some (Loc.user_position filename line col1 col2) Some (Loc.user_position filename line col1 col2)
| _ -> None in | _ -> None in
loc loc
......
...@@ -39,6 +39,12 @@ let rev_bounded_split c s n = ...@@ -39,6 +39,12 @@ let rev_bounded_split c s n =
let bounded_split c s n = List.rev (rev_bounded_split c s n) let bounded_split c s n = List.rev (rev_bounded_split c s n)
let rec join sep l =
match l with
| [] -> ""
| [x] -> x
| x :: rest -> x ^ sep ^ join sep rest
let ends_with s suf = let ends_with s suf =
let rec aux s suf suflen offset i = let rec aux s suf suflen offset i =
i >= suflen || (s.[i + offset] = suf.[i] i >= suflen || (s.[i + offset] = suf.[i]
......
...@@ -32,6 +32,10 @@ val bounded_split : char -> string -> int -> string list ...@@ -32,6 +32,10 @@ val bounded_split : char -> string -> int -> string list
[n] substring at most. [n] substring at most.
The concatenation of returned substrings is equal to the string s.*) The concatenation of returned substrings is equal to the string s.*)
val join : string -> string list -> string
(** [join sep l] joins all the strings in [l] together, in the same
order, separating them by [sep] *)
val ends_with : string -> string -> bool val ends_with : string -> string -> bool
(** test if a string ends with another *) (** test if a string ends with another *)
......
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