diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml index accb469a9f6152e0db8d3e466a3f78266d2f65c5..a7f1fdccd6e034bc974e2793cc951ea756046136 100644 --- a/src/session/session_itp.ml +++ b/src/session/session_itp.ml @@ -165,7 +165,10 @@ let get_proof_attempts (s : session) (id : proofNodeID) = let get_sub_tasks (s : session) (id : transID) = (get_transfNode s id).transf_subtasks -let get_transformation_name (s : session) (id : transID) = +let get_transf_args (s : session) (id : transID) = + (get_transfNode s id).transf_args + +let get_transf_name (s : session) (id : transID) = (get_transfNode s id).transf_name let get_proof_name (s : session) (id : proofNodeID) = @@ -218,10 +221,11 @@ let rec print_proof_node s (fmt: Format.formatter) p = and print_trans_node s fmt id = let tn = get_transfNode s id in + let args = get_transf_args s id in let name = tn.transf_name in let l = tn.transf_subtasks in let parent = (get_proofNode s tn.transf_parent).proofn_name.id_string in - fprintf fmt "@[<hv 2> Trans %s;@ parent %s;@ [%a]@]" name parent + fprintf fmt "@[<hv 2> Trans %s; args %a; parent %s;@ [%a]@]" name (Pp.print_list Pp.colon pp_print_string) args parent (Pp.print_list Pp.semi (print_proof_node s)) l @@ -523,25 +527,31 @@ and load_proof_or_transf session old_provers pid a = raise (LoadError (a,"prover not listing in header")) end | "transf" -> - let trname = string_attribute "name" a in - let tid = gen_transID session in - let subtasks_ids = - List.rev (List.fold_left - (fun goals th -> + let trname = string_attribute "name" a in + let rec get_args id = + match string_attribute_opt ("arg"^(string_of_int id)) a with + | Some arg -> arg :: (get_args (id+1)) + | None -> [] + in + let args = get_args 1 in + let tid = gen_transID session in + let subtasks_ids = + List.rev (List.fold_left + (fun goals th -> match th.Xml.name with | "goal" -> (gen_proofNodeID session) :: goals | _ -> goals) [] a.Xml.elements) - in - mk_transf_node session pid tid trname [] subtasks_ids; - List.iter2 - (load_goal session old_provers (Trans tid)) - a.Xml.elements subtasks_ids; + in + mk_transf_node session pid tid trname args subtasks_ids; + List.iter2 + (load_goal session old_provers (Trans tid)) + a.Xml.elements subtasks_ids; | "metas" -> () | "label" -> () | s -> - Warning.emit - "[Warning] Session.load_proof_or_transf: unexpected element '%s'@." - s + Warning.emit + "[Warning] Session.load_proof_or_transf: unexpected element '%s'@." + s let load_theory session old_provers acc th = match th.Xml.name with @@ -866,8 +876,13 @@ let rec save_goal s ctxt fmt pnid = fprintf fmt "@]@\n</goal>" and save_trans s ctxt fmt t = - fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\">@]" - save_string t.transf_name; + let arg_id = ref 0 in + let save_arg fmt s = + arg_id := !arg_id + 1; + fprintf fmt "arg%i=\"%a\"" !arg_id save_string s + in + fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\" %a>@]" + save_string t.transf_name (Pp.print_list Pp.space save_arg) t.transf_args; List.iter (save_goal s ctxt fmt) t.transf_subtasks; fprintf fmt "@]@\n</transf>" diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli index 0a020f2fe34605f10da2efeb49c2003c483e29a1..25b698cd5a4fffd9d8c7fecfa1c7e676bacc621d 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -101,7 +101,9 @@ val get_transformations : session -> proofNodeID -> transID list val get_proof_attempts : session -> proofNodeID -> proof_attempt list val get_sub_tasks : session -> transID -> proofNodeID list -val get_transformation_name : session -> transID -> string +val get_transf_args : session -> transID -> string list +val get_transf_name : session -> transID -> string + val get_proof_name : session -> proofNodeID -> Ident.ident val get_proof_parent : session -> proofNodeID -> proof_parent diff --git a/src/why3shell/why3shell.ml b/src/why3shell/why3shell.ml index 47570f23e370aa7f6bf418503f82817a859410f7..dca6fdfe6aee05f606442bd9bad80759ef5271b0 100644 --- a/src/why3shell/why3shell.ml +++ b/src/why3shell/why3shell.ml @@ -358,7 +358,7 @@ let print_proof_attempt fmt pa = let rec print_proof_node s (fmt: Format.formatter) p = let parent = match get_proof_parent s p with | Theory t -> (theory_name t).Ident.id_string - | Trans id -> get_transformation_name s id + | Trans id -> get_transf_name s id in let current_goal = match is_goal_cursor () with @@ -369,20 +369,21 @@ let rec print_proof_node s (fmt: Format.formatter) p = fprintf fmt "**"; fprintf fmt - "@[<hv 2> Goal %s;@ parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]" + "@[<hv 2> Goal %s; parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%a]@]@]" (get_proof_name s p).Ident.id_string parent (Pp.print_list Pp.semi print_proof_attempt) (get_proof_attempts s p) (Pp.print_list Pp.semi (print_trans_node s)) (get_transformations s p); if current_goal then - fprintf fmt "**" + fprintf fmt " **" and print_trans_node s fmt id = - let name = get_transformation_name s id in + let name = get_transf_name s id in + let args = get_transf_args s id in let l = get_sub_tasks s id in let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in - fprintf fmt "@[<hv 2> Trans %s;@ parent %s;@ [%a]@]" name parent + fprintf fmt "@[<hv 2> Trans %s; args %a; parent %s;@ [%a]@]" name (Pp.print_list Pp.semi pp_print_string) args parent (Pp.print_list Pp.semi (print_proof_node s)) l let print_theory s fmt th : unit =