Commit 3cd2c274 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Adding a test file.

Struggling with names. Removed the print_task which looked at the driver
before printing for uniformity. If I dont do that the printing function
I use to have a safe naming environnment inside tasks are not the same
as the printing function we use for display. So hypothesis displayed dont
actually exists and other bugs.

I will try to see if my changes (in particular clean_environnment and
gen_ident) are necessary.

Modifications in Pretty to get real unique names for hypothesis.
parent c69805dd
......@@ -613,3 +613,6 @@ let () = Exn_printer.register
fprintf fmt "Cannot prove the termination of %a" print_ls ls
| _ -> raise exn
end
(* TODO To remove *)
let ppunique = Ident.string_unique pprinter
......@@ -64,3 +64,6 @@ val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit
val print_namespace : formatter -> string -> theory -> unit
(* TODO dont use this and remove it *)
val ppunique : string -> string
......@@ -8,19 +8,29 @@ open Args_wrapper
let rec dup n x = if n = 0 then [] else x::(dup (n-1) x)
(* TODO ugly ! Solve it an other way *)
let clean_environment task =
let _ = Pretty.forget_all in
let _ = Pretty.print_task Format.str_formatter task in
()
let gen_ident s = Ident.id_fresh (Pretty.ppunique s)
(* From task [delta |- G] and term t, build the tasks:
[delta, t] |- G] and [delta, not t | - G] *)
let case t task =
let h = Decl.create_prsymbol (Ident.id_fresh "h") in
let hnot = Decl.create_prsymbol (Ident.id_fresh "hnot") in
clean_environment task;
let h = Decl.create_prsymbol (gen_ident "h") in
let hnot = Decl.create_prsymbol (gen_ident "hnot") in
let t_not_decl = Decl.create_prop_decl Decl.Paxiom hnot (Term.t_not t) in
let t_decl = Decl.create_prop_decl Decl.Paxiom h t in
List.map (fun f -> Trans.apply f task) [Trans.add_decls [t_decl]; Trans.add_decls [t_not_decl]]
(* From task [delta |- G] , build the tasks [delta, t | - G] and [delta] |- t] *)
let cut t task =
clean_environment task;
let g, task = Task.task_separate_goal task in
let h = Decl.create_prsymbol (Ident.id_fresh "h") in
let h = Decl.create_prsymbol (gen_ident "h") in
let g_t = Decl.create_prop_decl Decl.Pgoal h t in
let h_t = Decl.create_prop_decl Decl.Paxiom h t in
let goal_cut = Task.add_decl task g_t in
......@@ -56,11 +66,12 @@ let subst_forall t x =
(* From task [delta |- exists x. G] and term t, build the task [delta] |- G[x -> t]]
Return an error if x and t are not unifiable. *)
let exists x task =
clean_environment task;
let g, task = Task.task_separate_goal task in
match g.td_node with
| Decl {d_node = Dprop (_, _, t)} ->
let t = subst_exist t x in
let pr_goal = create_prsymbol (Ident.id_fresh "G") in
let pr_goal = create_prsymbol (gen_ident "G") in
let new_goal = Decl.create_prop_decl Decl.Pgoal pr_goal t in
[Task.add_decl task new_goal]
| _ -> failwith "No goal"
......@@ -92,9 +103,7 @@ let rec remove_task_decl task (name: string) : task_hd option =
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
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]
......@@ -115,10 +124,8 @@ let find_hypothesis name task =
(* from task [delta, name:forall x.A |- G,
build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
let simple_apply name t task =
(* Force setting of pprinter *)
let _ = Pretty.print_task Format.str_formatter task in
let _ = ignore (Format.flush_str_formatter ()) in
let instantiate name t task =
clean_environment task;
let g, task = Task.task_separate_goal task in
let ndecl = find_hypothesis name task in
match ndecl with
......@@ -126,7 +133,7 @@ let simple_apply name t task =
| Some decl -> (match decl.td_node with
| Decl {d_node = Dprop (pk, _pr, ht)} ->
let t_subst = subst_forall ht t in
let new_pr = create_prsymbol (Ident.id_fresh name) in
let new_pr = create_prsymbol (gen_ident name) in
let new_decl = create_prop_decl pk new_pr t_subst in
let task = add_decl task new_decl in
[Task.add_tdecl task g]
......@@ -188,9 +195,7 @@ let term_decl d =
(* from task [delta, name:forall x.A->B |- G,
build the task [delta,name:forall x.A->B] |- A[x -> t]] ou t est tel que B[x->t] = G *)
let apply name task =
(* Force setting of pprinter *)
let _ = Pretty.print_task Format.str_formatter task in
let _ = ignore (Format.flush_str_formatter ()) in
clean_environment task;
let g, task = Task.task_separate_goal task in
let tg = term_decl g in
let d = find_hypothesis name task in
......@@ -214,7 +219,7 @@ let apply name task =
(* TODO t_equal is probably too strong *)
if (Term.t_equal new_tb tg) then
[Task.add_decl task (create_prop_decl Pgoal
(create_prsymbol (Ident.id_fresh "G")) new_goal)]
(create_prsymbol (gen_ident "G")) new_goal)]
else
(Format.printf "Term substituted was %a. Should be goal was %a. Goal was %a @." Pretty.print_term x Pretty.print_term new_tb Pretty.print_term tg;
failwith "After substitution, terms are not exactly identical")
......@@ -228,7 +233,7 @@ let () = register_transform_with_args ~desc:"test case" "case" (wrap (Tformula T
let () = register_transform_with_args ~desc:"test cut" "cut" (wrap (Tformula Ttrans) cut)
let () = register_transform_with_args ~desc:"test exists" "exists" (wrap (Tterm Ttrans) exists)
let () = register_transform_with_args ~desc:"test remove" "remove" (wrap (Tstring Ttrans) remove)
let () = register_transform_with_args ~desc:"test simple_apply" "simple_apply"
(wrap (Tstring (Tterm Ttrans)) simple_apply)
let () = register_transform_with_args ~desc:"test instantiate" "instantiate"
(wrap (Tstring (Tterm Ttrans)) instantiate)
let () = register_transform_with_args ~desc:"test apply" "apply" (wrap (Tstring Ttrans) apply)
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" (wrap (Tint Ttrans) dup)
......@@ -452,7 +452,8 @@ 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@]@."
(Driver.print_task ~cntexample:false task_driver) task
(*(fprintf fmt "@[%a@]@?" Pretty.print_task task)*) Pretty.print_task
(*Driver.print_task ~cntexample:false task_driver)*) task
let test_save_session _fmt args =
match args with
......@@ -467,11 +468,28 @@ let test_reload fmt _args =
C.reload_files cont;
fprintf fmt "done @."
let test_transform_and_display fmt args =
match args with
| tr :: tl ->
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status;
match status with
| TSdone -> (ignore (move_to_goal_ret next_node);
test_print_goal fmt [])
| _ -> ()
in
C.schedule_transformation cont id tr tl ~callback
| _ -> printf "Error: Give the name of the transformation@."
(*******)
let commands =
[
"list-provers", "list available provers", list_provers;
"list-transforms", "list available transformations", list_transforms;
"a", "<transname> <args>: apply the transformation <transname> with arguments <args>", apply_transform;
"b", "<transname> <args>: behave like a then wait 0.2sec and display goal", test_transform_and_display;
"p", "print the session in raw form", dump_session_raw;
"t", "test schedule_proof_attempt with alt-ergo on the first goal", test_schedule_proof_attempt;
"g", "prints the first goal", test_print_goal;
......
theory Test
use import int.Int
goal G: forall x. exists y. x = 2 * y
(*
ng
b introduce_premises
>> print goal with primitives introduced
b cut "exists x: int. x = x"
>> print goal with h in context
b exists "5"
>> print new goal G1 with (x = (2 * 5))
p
>> print the proof tree with ** where we are
b case "exists x. exists y. x + y = y - x"
>> print the goal with the hypothesis in context
ng
g
>> print the goal with the contrary hypothesis
pg
>> return to context with positive exists
g
>> print it
b cut "exists x. exists y. x + y = 0"
ng
g
>> Have to prove h2 with 2 exists
b exists "4"
>> Instantiate x1
b cut "forall x. forall y. x + y = 0"
>> print with h2 in context
b instantiate "h2" "4"
>> create h21 which is correct
*)
end
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