Commit 7f2a8aab authored by MARCHE Claude's avatar MARCHE Claude

implicit intros in display and anywhere in controller

parent 5f2e43ad
......@@ -78,6 +78,7 @@ type controller =
controller_env: Env.env;
controller_provers:
(Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_tasks_for_print : (bool * Task.task * Trans.naming_table) Hpn.t;
}
......@@ -88,6 +89,7 @@ let create_controller config env ses =
controller_config = config;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
controller_tasks_for_print = Hpn.create 7;
}
in
let provers = Whyconf.get_provers config in
......@@ -118,6 +120,30 @@ let get_undetached_children_no_pa s any : any list =
(* handling of task printing with intros *)
let goal_task_to_print ?do_intros c n =
try
let (b,t,ta) = Hpn.find c.controller_tasks_for_print n in
match do_intros with
| None -> t,ta
| Some b' -> if b <> b' then raise Not_found; t,ta
with Not_found ->
let t = get_task c.controller_session n in
let do_intros =
match do_intros with
| None -> false
| Some b -> b
in
let t =
if do_intros then Trans.apply Introduction.introduce_premises t else t
in
let ta = Args_wrapper.build_naming_tables t in
Hpn.add c.controller_tasks_for_print n (do_intros,t,ta);
t,ta
(* printing *)
module PSession = struct
......@@ -281,10 +307,10 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback =
config_pr
~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let task = Session_itp.get_task c.controller_session id in
let table = Session_itp.get_table c.controller_session id in
(* let table = Session_itp.get_table c.controller_session id in *)
let call =
Driver.prove_task ?old:proof_script ~cntexample:cntexample ~inplace:false ~command
~limit ?name_table:table driver task
~limit (*?name_table:table*) driver task
in
let pa = (c.controller_session,id,pr,proof_script,callback,false,call) in
Queue.push pa prover_tasks_in_progress
......@@ -537,10 +563,13 @@ let schedule_edition c id pr ~no_edit ~do_check_proof ?file ~callback ~notificat
let schedule_transformation_r c id name args ~callback =
let apply_trans () =
(*
let task = get_task c.controller_session id in
let table = match get_table c.controller_session id with
| None -> raise (Trans.Bad_name_table "Controller_itp.schedule_transformation_r")
| Some table -> table in
*)
let task,table = goal_task_to_print c id in
begin
try
let subtasks =
......
......@@ -78,6 +78,7 @@ type controller = private
controller_config : Whyconf.config;
controller_env : Env.env;
controller_provers : (Whyconf.config_prover * Driver.driver) Whyconf.Hprover.t;
controller_tasks_for_print : (bool * Task.task * Trans.naming_table) Hpn.t;
}
val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> controller
......@@ -87,6 +88,11 @@ val create_controller: Whyconf.config -> Env.env -> Session_itp.session -> contr
val print_session : Format.formatter -> controller -> unit
(* handling of task printing with intros *)
val goal_task_to_print :
?do_intros:bool -> controller -> proofNodeID -> Task.task * Trans.naming_table
(*
- TODO: the presence of obsolete goals should be returned somehow by
......
......@@ -83,9 +83,12 @@ let loaded_strategies = ref []
(****** Exception handling *********)
let p s id =
(*
let tables = match (Session_itp.get_table s id) with
| None -> Args_wrapper.build_naming_tables (Session_itp.get_task s id)
| Some tables -> tables in
*)
let _,tables = Controller_itp.goal_task_to_print s id in
let pr = tables.Trans.printer in
let apr = tables.Trans.aprinter in
(Pretty.create pr apr pr pr false)
......@@ -899,14 +902,17 @@ end
(* -- send the task -- *)
let task_of_id d id do_intros loc =
(*
let task = get_task d.cont.controller_session id in
let tables = get_table d.cont.controller_session id in
*)
let task,tables = goal_task_to_print ~do_intros d.cont id in
(* This function also send source locations associated to the task *)
let loc_color_list = if loc then get_locations task else [] in
let task_text =
match tables with
| None -> assert false
| Some t ->
(*| None -> assert false
| Some*) t ->
let pr = t.Trans.printer in
let apr = t.Trans.aprinter in
let module P = (val Pretty.create pr apr pr pr false) in
......@@ -1102,7 +1108,7 @@ end
let doc = try
Pp.sprintf "%s\n%a" tr Pp.formatted (Trans.lookup_trans_desc tr)
with | _ -> "" in
let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
let msg, loc, arg_opt = get_exception_message d.cont id e in
let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
P.notify (Message (Transf_error (node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
| _ -> ()
......
......@@ -409,9 +409,12 @@ let interp commands_table config cont id s =
| Qnotask f, _ -> Query (f cont args)
| Qtask _, None -> QError "please select a goal first"
| Qtask f, Some id ->
(*
let table = match Session_itp.get_table cont.Controller_itp.controller_session id with
| None -> raise (Trans.Bad_name_table "Server_utils.interp")
| Some table -> table in
*)
let _,table = Controller_itp.goal_task_to_print cont id in
let s = try Query (f cont table args) with
| Undefined_id s -> QError ("No existing id corresponding to " ^ s)
| Number_of_arguments -> QError "Bad number of arguments"
......
......@@ -210,10 +210,6 @@ let get_task (s:session) (id:proofNodeID) =
let node = get_proofNode s id in
node.proofn_task
let get_table (s: session) (id: proofNodeID) =
let node = get_proofNode s id in
node.proofn_table
let get_transfNode (s : session) (id : transID) =
try
Hint.find s.trans_table id
......
......@@ -85,7 +85,6 @@ val is_below: session -> any -> any -> bool
type proof_parent = Trans of transID | Theory of theory
val get_task : session -> proofNodeID -> Task.task
val get_table : session -> proofNodeID -> Trans.naming_table option
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempt_ids :
......
......@@ -2,9 +2,38 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.4.1" timelimit="5" steplimit="1" memlimit="0"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../demo-itp.mlw">
<theory name="TestAutoFocus" sum="b9c97d5c8e378bea09fece0986d55347">
<theory name="M" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestTaskPrinting" sum="01fbd777d08f356d2f390e335249eeb9">
<goal name="g1">
</goal>
<goal name="g2">
</goal>
<goal name="g3">
</goal>
<goal name="g4">
</goal>
<goal name="g5">
</goal>
<goal name="g6">
</goal>
<goal name="g7">
</goal>
<goal name="g8">
</goal>
</theory>
<theory name="TestAutomaticIntro" sum="6566463f1ee0314d808add53aa21307c">
<goal name="g">
</goal>
</theory>
<theory name="TestInfixSymbols" sum="1e2101112f2c37523da345d6bab356e6">
<goal name="g">
</goal>
</theory>
<theory name="TestAutoFocus" sum="bd282d677ea02bff5e05e03fd51a598a">
<goal name="g0">
</goal>
<goal name="g1">
......@@ -12,13 +41,20 @@
<goal name="g2">
</goal>
</theory>
<theory name="Power" sum="1c745a16ebe3e09577a4b58a87bd9d8b">
<theory name="Power" sum="4cc6d21f246903f98feda68da4e48c65">
<goal name="power_1">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="sqrt4_256">
</goal>
<goal name="power_sum">
<goal name="power_sum" proved="true">
<transf name="induction" proved="true"arg1="n" arg2="0">
<goal name="power_sum.0" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="power_sum.1" proved="true">
<proof prover="0"><result status="valid" time="0.16" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="power_0_left">
</goal>
......
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