Commit d896d490 authored by Sylvain Dailler's avatar Sylvain Dailler

Adding remove transformation. I had to add functions from Task and I would

like to add more from Ident and Pretty but keeped minimal changes in those
files.
TODOs to be discussed.
parent 35ef6310
......@@ -126,6 +126,9 @@ 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
......
......@@ -3,6 +3,7 @@ open Trans
open Term
open Decl
open Theory
open Task
let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
......@@ -57,9 +58,38 @@ let exists x task =
[Task.add_decl task new_goal]
| _ -> failwith "No goal"
let remove _name task =
[task;task]
(* TODO :from task [delta, name:A |- G] build the task [delta |- G] *)
(* TODO ask to have functions in ident and Pretty that do something like that *)
let string_pr pr =
ignore (Format.flush_str_formatter ());
Pretty.print_pr Format.str_formatter pr;
Format.flush_str_formatter()
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
(* TODO check this works in particular when hypothesis names
are extracted from same name. Seemed not to work before
adding "print_task". To be resolved in a better way. *)
(* from task [delta, name:A |- G] build the task [delta |- G] *)
let remove name task =
(* Force setting of pprinter *)
let _ = Pretty.print_task Format.str_formatter task in
let _ = ignore (Format.flush_str_formatter ()) in
let g, task = Task.task_separate_goal task in
let task = remove_task_decl task name in
[Task.add_tdecl task g]
let simple_apply _name _t task = (* ? *)
[task;task]
......@@ -86,7 +116,13 @@ let exists' args task =
| [TAterm t] -> exists t task
| _ -> failwith "wrong arguments for exists"
let remove' args task =
match args with
| [TAstring name] -> remove name task
| _ -> failwith "wrong argument for remove"
let () = register_transform_with_args ~desc:"test case" "case" case'
let () = register_transform_with_args ~desc:"test cut" "cut" cut'
let () = register_transform_with_args ~desc:"test exists" "exists" exists'
let () = register_transform_with_args ~desc:"test remove" "remove" remove'
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" duplicate
......@@ -425,6 +425,33 @@ let parse_transformation_arg args : Term.term option =
end
| _ -> let _ = printf "term argument expected@." in None
let parse_transformation_string args : string option =
(* temporary : parses a string *)
match args with
| [s] ->
let s =
let l = String.length s in
if l >= 2 && s.[0] = '"' && s.[l - 1] = '"' then
String.sub s 1 (l - 2)
else s
in
printf "parsing string \"%s\"@." s;
Some s
| _ -> let _ = printf "term argument expected@." in None
let test_remove_with_string_args fmt args =
match (parse_transformation_string args) with
| None -> ()
| Some s ->
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "remove" [Trans.TAstring s] ~callback
(* Only parses arguments and print debugging information *)
let test_transformation_with_term_arg _fmt args =
let _ = parse_transformation_arg args in ()
......@@ -495,6 +522,7 @@ let commands =
"c", "case on next goal", test_case_with_term_args;
"g", "prints the first goal", test_print_goal;
"r", "reload the session (test only)", test_reload;
"rem", "test remove transformation. Take one string argument", test_remove_with_string_args;
"s", "[s my_session] save the current session in my_session.xml", test_save_session;
"tr", "test schedule_transformation with split_goal on the current or next right goal (or on the top goal if there is none", test_transformation;
"ttr", "takes 2 arguments. Name of the transformation (with one term argument) and a term" , test_transformation_one_arg_term;
......
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