Commit d9a3aab4 authored by Johannes Kanig's avatar Johannes Kanig Committed by David Hauzar

O225-030 render traversal function more generic

So that it can be used to search for other labels.

* termcode.ml
(search_labels): basically a copy of get_expls_fmla with extra argument
for the callback
(get_expls_fmla): rewritten to use search_labels
parent c249ccb9
......@@ -42,21 +42,27 @@ let concat_expls = function
| [l] -> Some l
| l :: ls -> Some (l ^ " (" ^ String.concat ". " ls ^ ")")
let rec get_expls_fmla acc f =
if f.t_ty <> None then acc
else if Ident.Slab.mem Split_goal.stop_split f.Term.t_label then acc
else
let res = collect_expls f.Term.t_label in
if res = [] then match f.t_node with
| Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc
| Term.Tbinop (Term.Timplies, _, f) -> get_expls_fmla acc f
| Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) ->
Term.t_fold get_expls_fmla acc f
| _ -> raise Exit
else if acc = [] then res
else raise Exit
let get_expls_fmla f = try get_expls_fmla [] f with Exit -> []
let search_labels callback =
let rec aux acc f =
if f.t_ty <> None then acc
else if Ident.Slab.mem Split_goal.stop_split f.Term.t_label then acc
else
let res = callback f.Term.t_label in
if res = [] then match f.t_node with
| Term.Ttrue | Term.Tfalse | Term.Tapp _ -> acc
| Term.Tbinop (Term.Timplies, _, f) -> aux acc f
| Term.Tlet _ | Term.Tcase _ | Term.Tquant (Term.Tforall, _) ->
Term.t_fold aux acc f
| _ -> raise Exit
else if acc = [] then res
else raise Exit
in
aux []
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 gid = (Task.task_goal task).Decl.pr_name in
......
......@@ -16,6 +16,14 @@ val arg_extra_expl_prefix : string * Arg.spec * string
val goal_expl_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 *)
val reset_dict : unit -> unit
......
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