Commit 824a5cfb authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Transformation remove implemented using Trans.decl

parent 5e5163b6
......@@ -126,9 +126,6 @@ val on_tagged_ts : meta -> task -> Sts.t
val on_tagged_ls : meta -> task -> Sls.t
val on_tagged_pr : meta -> task -> Spr.t
val mk_task: Theory.tdecl -> task -> Decl.known_map -> clone_map -> meta_map -> task
(** Exceptions *)
exception NotTaggingMeta of meta
......
......@@ -48,6 +48,10 @@ val fold_map : (task_hd -> 'a * 'b -> ('a * 'b) ) -> 'a -> 'b -> 'b trans
val fold_map_l : (task_hd -> 'a * 'b -> ('a * 'b) list) -> 'a -> 'b -> 'b tlist
val decl : (decl -> decl list ) -> task -> task trans
(** [decl f t1 t2] adds to task [t1] the declarations [f d] for each
declaration [d] of task [t2]. (similar to a "flat_map"
operation) *)
val decl_l : (decl -> decl list list) -> task -> task tlist
val tdecl : (decl -> tdecl list ) -> task -> task trans
......
......@@ -83,20 +83,14 @@ let string_pr pr =
Format.flush_str_formatter()
(* Return a new task with hypothesis name removed *)
let rec remove_task_decl task (name: string) : task_hd option =
match task with
| Some {task_decl = {td_node = Decl {d_node = Dprop (Paxiom, pr, _)}};
task_prev = task} when (string_pr pr = name) ->
task
| Some {task_decl = decl;
task_prev = task;
task_known = known;
task_clone = clone;
task_meta = meta;
task_tag = _} ->
(* Should create a new unique tag each time *)
Task.mk_task decl (remove_task_decl task name) known clone meta
| None -> None
let remove_task_decl (name: string) : task trans =
Trans.decl
(fun d ->
match d.d_node with
| Dprop (Paxiom, pr, _) when (string_pr pr = name) ->
[]
| _ -> [d])
None
(* TODO check if this works in particular when hypothesis names
are extracted from same name. Seemed not to work before
......@@ -104,9 +98,8 @@ let rec remove_task_decl task (name: string) : task_hd option =
(* from task [delta, name:A |- G] build the task [delta |- G] *)
let remove name task =
clean_environment task;
let g, task = Task.task_separate_goal task in
let task = remove_task_decl task name in
[Task.add_tdecl task g]
[Trans.apply (remove_task_decl name) task]
let pr_prsymbol pr =
match pr with
......
......@@ -452,8 +452,9 @@ let test_print_goal fmt _args =
let id = nearest_goal () in
let task = Session_itp.get_task cont.Controller_itp.controller_session id in
fprintf fmt "@[====================== Task =====================@\n%a@]@."
(* (fprintf fmt "@[%a@]@?" Pretty.print_task task) Pretty.print_task *)
(Driver.print_task ~cntexample:false task_driver) task
Pretty.print_task
(* (Driver.print_task ~cntexample:false task_driver) *)
task
let test_save_session _fmt args =
match args with
......
......@@ -7,7 +7,7 @@ theory Test
(*
ng
b introduce_premises
>> print goal with primitives introduced
>> print goal with premisses introduced
b cut "exists x: int. x = x"
>> print goal with h in context
b exists "5"
......
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