Commit 8f3b82bd authored by François Bobot's avatar François Bobot

session: add_registered_* add only when not already existing

parent 3e20cfe5
......@@ -1555,19 +1555,22 @@ let remove_transformation ?(notify=notify) t =
let add_registered_transformation ~keygen env_session tr_name g =
let task = goal_task g in
let gname = g.goal_name in
let subgoals = Trans.apply_transform tr_name env_session.env task in
let i = ref 1 in
let goal task =
let gid = (Task.task_goal task).Decl.pr_name in
let expl = get_explanation gid task in
let goal_name = gname.Ident.id_string ^ "." ^ (string_of_int (!i)) in
incr i;
let goal_name = Ident.id_register (Ident.id_derive goal_name gid) in
goal_name, expl, task
in
add_transformation ~keygen ~goal env_session tr_name g subgoals
try
Hstr.find g.goal_transformations tr_name
with Not_found ->
let task = goal_task g in
let gname = g.goal_name in
let subgoals = Trans.apply_transform tr_name env_session.env task in
let i = ref 1 in
let goal task =
let gid = (Task.task_goal task).Decl.pr_name in
let expl = get_explanation gid task in
let goal_name = gname.Ident.id_string ^ "." ^ (string_of_int (!i)) in
incr i;
let goal_name = Ident.id_register (Ident.id_derive goal_name gid) in
goal_name, expl, task
in
add_transformation ~keygen ~goal env_session tr_name g subgoals
(****************)
(** metas *)
......@@ -1699,26 +1702,29 @@ let pos_of_metas ?version_shape lms task =
in
idpos
let add_registered_metas ~keygen env added g =
let goal,task0 = Task.task_separate_goal (goal_task g) in
let add_meta task (s,l) =
let m = Theory.lookup_meta s in
Task.add_meta task m l in
(** add before the goal *)
let task = List.fold_left add_meta task0 added in
let task = add_tdecl task goal in
let idpos = pos_of_metas added task in
let add_registered_metas ~keygen env added0 g =
let added = List.fold_left (fun ma (s,l) ->
Mstr.change (function
| None -> Some (Smeta_args.singleton l)
| Some std ->
Some (Smeta_args.add l std)) s ma) Mstr.empty added in
let metas = raw_add_metas ~keygen g added idpos false in
let goal = raw_add_task ~version:env.session.session_shape_version
~keygen (Parent_metas metas)
g.goal_name g.goal_expl task false in
metas.metas_goal <- goal;
metas
Some (Smeta_args.add l std)) s ma) Mstr.empty added0 in
match Mmetas_args.find_opt added g.goal_metas with
| Some metas -> metas
| None ->
let goal,task0 = Task.task_separate_goal (goal_task g) in
let add_meta task (s,l) =
let m = Theory.lookup_meta s in
Task.add_meta task m l in
(** add before the goal *)
let task = List.fold_left add_meta task0 added0 in
let task = add_tdecl task goal in
let idpos = pos_of_metas added0 task in
let metas = raw_add_metas ~keygen g added idpos false in
let goal = raw_add_task ~version:env.session.session_shape_version
~keygen (Parent_metas metas)
g.goal_name g.goal_expl task false in
metas.metas_goal <- goal;
metas
let remove_metas ?(notify=notify) m =
let g = m.metas_parent in
......
......@@ -399,7 +399,9 @@ val add_registered_transformation :
'key goal ->
'key transf
(** Apply a real transformation by its why3 name,
raise NoTask if the goal doesn't contain a task *)
raise NoTask if the goal doesn't contain a task.
If the goal already has a transformation with this name,
it is returned. *)
val remove_transformation : ?notify:'key notify -> 'key transf -> unit
(** Remove a transformation *)
......@@ -411,10 +413,12 @@ val add_registered_metas :
(string * Theory.meta_arg list) list ->
'key goal ->
'key metas
(** Add some metas to a task *)
(** Add some metas to a task. If the goal already contain a {!metas}
with same metas, the old one is returned.
*)
val remove_metas : ?notify:'key notify -> 'key metas -> unit
(** Remove the addition of metas *)
(** Remove the addition of metas *)
(** {2 File} *)
......
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