Commit 3e20cfe5 authored by François Bobot's avatar François Bobot

session: metas can be added

  - the symbols that appear in the metas are identified in the xml by
    their position in the task:
    - in which declaration
    - in which definition (if that apply otherwise -1)
    - in which constructor(or case in inductive predicate) (if that apply otherwise -1)
    - in which field (if that apply otherwise -1)

  - the md5sum of the prefix of the task that end with the declaration is used to know if the
    symbol have been changed, and if it is obsolete.

  - currently metas that contains obsolete symbol are removed.
parent 068ddc7b
......@@ -109,6 +109,8 @@ session
- the filenames in the location inside a session should be relative
to the session_dir.
- use the new restore_path for the metas in session?
tools
-----
......@@ -136,4 +138,3 @@ provers
- PVS: use a better name for PVS theory when printing a task, e.g.
file_theory_goal. Solution: do that when we have idents with origin
information (necessary for parsing a task).
......@@ -23,6 +23,8 @@ theory = "folder32"
goal = "file32"
prover = "wizard32"
transf = "configure32"
#TODO change metas
metas = "movefile32"
editor = "edit32"
replay = "refresh32"
cancel = "cut32"
......@@ -55,6 +57,8 @@ theory = "folder"
goal = "script"
prover = "magic_wand_2"
transf = "multitool"
#TODO change metas
metas = "ddr_memory"
editor = "pencil"
replay = "update"
cancel = "cancel"
......
......@@ -20,7 +20,7 @@
<!ATTLIST theory loccnumb CDATA #IMPLIED>
<!ATTLIST theory loccnume CDATA #IMPLIED>
<!ELEMENT goal (label*, proof*, transf*)>
<!ELEMENT goal (label*, proof*, transf*, metas*)>
<!ATTLIST goal name CDATA #REQUIRED>
<!ATTLIST goal expl CDATA #IMPLIED>
<!ATTLIST goal proved CDATA #REQUIRED>
......@@ -53,3 +53,61 @@
<!ELEMENT label EMPTY>
<!ATTLIST label name CDATA #REQUIRED>
<!ELEMENT metas (ts_pos*, ls_pos*, pr_pos*, meta_args*,goal)>
<!ATTLIST metas proved CDATA #REQUIRED>
<!ATTLIST metas expanded CDATA #IMPLIED>
<!ELEMENT ts_pos EMPTY>
<!ATTLIST ts_pos name CDATA #REQUIRED>
<!ATTLIST ts_pos arity CDATA #REQUIRED>
<!ATTLIST ts_pos id CDATA #REQUIRED>
<!ATTLIST ts_pos decl CDATA #REQUIRED>
<!ATTLIST ts_pos def CDATA #REQUIRED>
<!ATTLIST ts_pos const CDATA #REQUIRED>
<!ATTLIST ts_pos proj CDATA #REQUIRED>
<!ATTLIST ts_pos sum CDATA #REQUIRED>
<!ELEMENT ls_pos EMPTY>
<!ATTLIST ls_pos name CDATA #REQUIRED>
<!ATTLIST ls_pos id CDATA #REQUIRED>
<!ATTLIST ls_pos decl CDATA #REQUIRED>
<!ATTLIST ls_pos def CDATA #REQUIRED>
<!ATTLIST ls_pos const CDATA #REQUIRED>
<!ATTLIST ls_pos proj CDATA #REQUIRED>
<!ATTLIST ls_pos sum CDATA #REQUIRED>
<!ELEMENT pr_pos EMPTY>
<!ATTLIST pr_pos name CDATA #REQUIRED>
<!ATTLIST pr_pos id CDATA #REQUIRED>
<!ATTLIST pr_pos decl CDATA #REQUIRED>
<!ATTLIST pr_pos def CDATA #REQUIRED>
<!ATTLIST pr_pos const CDATA #REQUIRED>
<!ATTLIST pr_pos proj CDATA #REQUIRED>
<!ATTLIST pr_pos sum CDATA #REQUIRED>
<!ELEMENT meta (meta_arg_ty*, meta_arg_ts*, meta_arg_ls*, meta_arg_pr*, meta_arg_str*, meta_arg_int*)>
<!ATTLIST meta name CDATA #REQUIRED>
<!ELEMENT meta_args_ty (ty_var|ty_app)>
<!ELEMENT ty_var EMPTY>
<!ATTLIST ty_var id CDATA #REQUIRED>
<!ELEMENT ty_app (ty_var*,ty_app*)>
<!ATTLIST ty_app id CDATA #REQUIRED>
<!ELEMENT meta_args_ts EMPTY>
<!ATTLIST meta_args_ts id CDATA #REQUIRED>
<!ELEMENT meta_args_ls EMPTY>
<!ATTLIST meta_args_ls id CDATA #REQUIRED>
<!ELEMENT meta_args_pr EMPTY>
<!ATTLIST meta_args_pr id CDATA #REQUIRED>
<!ELEMENT meta_args_str EMPTY>
<!ATTLIST meta_args_str val CDATA #REQUIRED>
<!ELEMENT meta_args_int EMPTY>
<!ATTLIST meta_args_int val CDATA #REQUIRED>
......@@ -216,6 +216,12 @@ let meta_remove_prop = register_meta "remove_prop" [MTprsymbol]
~desc:"Specify@ the@ logical@ propositions@ to@ remove.@ \
Can@ be@ specified@ in@ the@ driver@ with@ the@ remove@ prop@ rule."
let meta_remove_type_symbol = register_meta "remove_type_symbol" [MTtysymbol]
~desc:"Specify@ the@ type@ symbol@ to@ remove."
let meta_remove_logic = register_meta "remove_logic" [MTlsymbol]
~desc:"Specify@ the@ logic@ symbol@ propositions@ to@ remove."
let meta_realized = register_meta "realized" [MTstring; MTstring]
~desc:"TODO??"
......
......@@ -50,6 +50,8 @@ val print_prelude_for_theory : theory -> prelude_map pp
val meta_syntax_type : meta
val meta_syntax_logic : meta
val meta_remove_prop : meta
val meta_remove_logic : meta
val meta_remove_type_symbol : meta
val meta_realized : meta
val syntax_type : tysymbol -> string -> tdecl
......
......@@ -51,6 +51,8 @@ let tds_singleton td = mk_tds (Stdecl.singleton td)
let tds_equal : tdecl_set -> tdecl_set -> bool = (==)
let tds_hash tds = Hashweak.tag_hash tds.tds_tag
let tds_compare tds1 tds2 = compare
(Hashweak.tag_hash tds1.tds_tag) (Hashweak.tag_hash tds2.tds_tag)
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
......@@ -141,6 +143,13 @@ let task_goal_fmla task = match find_goal task with
| Some (_,f) -> f
| None -> raise GoalNotFound
let task_separate_goal = function
| Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as goal;
task_prev = task} ->
goal,task
| _ -> raise GoalNotFound
let check_task task = match find_goal task with
| Some _ -> raise GoalFound
| None -> task
......@@ -369,6 +378,13 @@ let rec split i l acc = match i,l with
let merge task l = List.fold_left add_tdecl task l
type bisect_step =
| BSdone of task
| BSstep of task * (bool -> bisect_step)
(*
Simple version
let rec bisect_aux f task lt i lk =
if i < 2 then
if try f (merge task lk) with UnknownIdent _ -> false then [] else
......@@ -402,3 +418,55 @@ let bisect f task =
let task = merge None tacc in
let lt = bisect_aux f task lt i [goal] in
add_tdecl (merge task lt) goal
*)
let rec bisect_aux cont task lt i lk =
if i < 2 then
let res0 b =
if b then cont [] else
(assert (List.length lt = 1); cont lt) in
try BSstep (merge task lk, res0) with UnknownIdent _ -> res0 false
else
let i1 = i/2 in
let i2 = i/2 + i mod 2 in
let lt1,lt2 = split i1 lt [] in
let task1 = merge task lt1 in (** Can't fail *)
(** These "if then else" allow to remove big chunck with one call to f *)
let res1 b =
if b
then bisect_aux cont task lt1 i1 lk
else
let res2 b =
if b
then bisect_aux cont task lt2 i2 lk
else
let c1 lt2 =
let lk2 = List.append lt2 lk in
let c2 lt1 = cont (List.append lt1 lt2) in
bisect_aux c2 task lt1 i1 lk2 in
bisect_aux c1 task1 lt2 i2 lk in
try BSstep (merge (merge task lt2) lk, res2)
with UnknownIdent _ -> res2 false in
try BSstep (merge task1 lk,res1) with UnknownIdent _ -> res1 false
let bisect_step task =
let task,goal = match task with
| Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,_,_)}} as td;
task_prev = task} -> task,td
| _ -> raise GoalNotFound in
let lt,i,tacc = task_fold (fun (acc,i,tacc) td ->
match td.td_node with
| Decl _ -> (td::acc,succ i,tacc)
| _ -> (acc,i,td::tacc)) ([],0,[]) task in
let task = merge None tacc in
let c1 lt =
BSdone (add_tdecl (merge task lt) goal) in
bisect_aux c1 task lt i [goal]
let bisect f task =
let rec run = function
| BSdone r -> r
| BSstep (t,c) -> run (c (f t)) in
run (bisect_step task)
......@@ -34,8 +34,11 @@ type tdecl_set = private {
val tds_equal : tdecl_set -> tdecl_set -> bool
val tds_hash : tdecl_set -> int
val tds_compare : tdecl_set -> tdecl_set -> int
val tds_empty : tdecl_set
val mk_tds : Stdecl.t -> tdecl_set
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
......@@ -96,6 +99,13 @@ val bisect : (task -> bool) -> task -> task
included in [task] and if any declarations are removed from it the
task doesn't verify test anymore *)
type bisect_step =
| BSdone of task
| BSstep of task * (bool -> bisect_step)
val bisect_step : task -> bisect_step
(** Same as before but doing it step by step *)
(** {2 realization utilities} *)
val used_theories : task -> theory Mid.t
......@@ -120,6 +130,7 @@ val task_decls : task -> decl list
val task_goal : task -> prsymbol
val task_goal_fmla : task -> term
val task_separate_goal : task -> tdecl * task
(** {2 selectors} *)
......
......@@ -175,6 +175,8 @@ let loadpath m =
let timelimit m = m.timelimit
let memlimit m = m.memlimit
let running_provers_max m = m.running_provers_max
let get_complete_command pc =
String.concat " " (pc.command :: pc.extra_options)
let set_limits m time mem running =
{ m with timelimit = time; memlimit = mem; running_provers_max = running }
......
......@@ -119,6 +119,9 @@ type config_prover = {
extra_drivers : string list;
}
val get_complete_command : config_prover -> string
(** add the extra_options to the command *)
val get_provers : config -> config_prover Mprover.t
(** [get_provers config] get the prover family stored in the Rc file. The
keys are the unique ids of the prover (argument of the family) *)
......
......@@ -343,6 +343,7 @@ let image_theory = ref !image_default
let image_goal = ref !image_default
let image_prover = ref !image_default
let image_transf = ref !image_default
let image_metas = ref !image_default
let image_editor = ref !image_default
let image_replay = ref !image_default
let image_cancel = ref !image_default
......@@ -387,6 +388,7 @@ let iconname_theory = ref ""
let iconname_goal = ref ""
let iconname_prover = ref ""
let iconname_transf = ref ""
let iconname_metas = ref ""
let iconname_editor = ref ""
let iconname_replay = ref ""
let iconname_cancel = ref ""
......@@ -430,6 +432,7 @@ let load_icon_names () =
iconname_goal := get_icon_name "goal";
iconname_prover := get_icon_name "prover";
iconname_transf := get_icon_name "transf";
iconname_metas := get_icon_name "metas";
iconname_editor := get_icon_name "editor";
iconname_replay := get_icon_name "replay";
iconname_cancel := get_icon_name "cancel";
......@@ -462,6 +465,7 @@ let resize_images size =
image_goal := image ~size !iconname_goal;
image_prover := image ~size !iconname_prover;
image_transf := image ~size !iconname_transf;
image_metas := image ~size !iconname_metas;
image_editor := image ~size !iconname_editor;
image_replay := image ~size !iconname_replay;
image_cancel := image ~size !iconname_cancel;
......
......@@ -72,6 +72,7 @@ val image_theory : GdkPixbuf.pixbuf ref
val image_goal : GdkPixbuf.pixbuf ref
val image_prover : GdkPixbuf.pixbuf ref
val image_transf : GdkPixbuf.pixbuf ref
val image_metas : GdkPixbuf.pixbuf ref
val image_editor : GdkPixbuf.pixbuf ref
val image_replay : GdkPixbuf.pixbuf ref
val image_cancel : GdkPixbuf.pixbuf ref
......
This diff is collapsed.
This diff is collapsed.
......@@ -25,6 +25,8 @@
Use session_scheduler if you want to queue the operations
*)
open Stdlib
val debug : Debug.flag
(** The debug flag "session" *)
......@@ -58,6 +60,27 @@ type task_option
(** Currently just an option on a task, but later perhaps
we should be able to release a task and rebuild it when needed *)
type pos_task =
{ pos_decl : int; (* nth decl in the task from top *)
pos_def : int; (* nth def in the decl *)
pos_const : int; (* nth constructor in the type def *)
pos_proj : int; (* nth proj for the constructor (-1 for the constructor) *)
pos_checksum : Termcode.checksum;
(** the checksum of the prefix of the task starting at this decl *)
}
type meta_args = Theory.meta_arg list
module Mmeta_args : Map.S with type key = meta_args
module Smeta_args : Mmeta_args.Set
type metas_args = Smeta_args.t Util.Mstr.t
module Mmetas_args : Map.S with type key = metas_args
type idpos = {
idpos_ts : pos_task Ty.Mts.t;
idpos_ls : pos_task Term.Mls.t;
idpos_pr : pos_task Decl.Mpr.t;
}
(** {2 Session} *)
(** All the element of a session contain a key which can hold whatever
......@@ -76,6 +99,7 @@ type 'a goal = private
mutable goal_expanded : bool;
goal_external_proofs : 'a proof_attempt PHprover.t;
goal_transformations : 'a transf PHstr.t;
mutable goal_metas : 'a metas Mmetas_args.t;
}
and 'a proof_attempt = private
......@@ -93,6 +117,18 @@ and 'a proof_attempt = private
and 'a goal_parent = private
| Parent_theory of 'a theory
| Parent_transf of 'a transf
| Parent_metas of 'a metas
and 'a metas =
{ mutable metas_key : 'a;
metas_added : metas_args;
metas_idpos : idpos;
metas_parent : 'a goal;
mutable metas_verified : bool;
mutable metas_goal : 'a goal;
(** Not mutated after the creation *)
mutable metas_expanded : bool;
}
and 'a transf = private
{ mutable transf_key : 'a;
......@@ -236,9 +272,13 @@ val proof_verified : 'key proof_attempt -> bool
val get_used_provers : 'a session -> Whyconf.Sprover.t
(** Get the set of provers which appear in the session *)
(* val metas_of_virtuals : 'a metas -> Theory.Smeta.t *)
(* (\** Get the set of metas added (the parent goal must contain a task) *\) *)
(** {2 Modificator} *)
val set_transf_expanded : 'key transf -> bool -> unit
val set_metas_expanded : 'key metas -> bool -> unit
val set_goal_expanded : 'key goal -> bool -> unit
val set_theory_expanded : 'key theory -> bool -> unit
val set_file_expanded : 'key file -> bool -> unit
......@@ -252,6 +292,7 @@ type 'a any =
| Goal of 'a goal
| Proof_attempt of 'a proof_attempt
| Transf of 'a transf
| Metas of 'a metas
val print_any : Format.formatter -> 'a any -> unit
(** Print a subtree with a pstree format (cf Tree module) *)
......@@ -363,6 +404,18 @@ val add_registered_transformation :
val remove_transformation : ?notify:'key notify -> 'key transf -> unit
(** Remove a transformation *)
(** {2 Metas} *)
val add_registered_metas :
keygen:'key keygen ->
'key env_session ->
(string * Theory.meta_arg list) list ->
'key goal ->
'key metas
(** Add some metas to a task *)
val remove_metas : ?notify:'key notify -> 'key metas -> unit
(** Remove the addition of metas *)
(** {2 File} *)
val add_file :
......@@ -407,15 +460,21 @@ val goal_iter_leaf_goal :
(** {3 not recursive} *)
val iter_goal :
('key proof_attempt -> unit) -> ('key transf -> unit) -> 'key goal -> unit
('key proof_attempt -> unit) ->
('key transf -> unit) ->
('key metas -> unit) ->
'key goal -> unit
val iter_transf :
('key goal -> unit) -> 'key transf -> unit
val iter_metas :
('key goal -> unit) -> 'key metas -> unit
val goal_iter : ('key any -> unit) -> 'key goal -> unit
val transf_iter : ('key any -> unit) -> 'key transf -> unit
val theory_iter : ('key any -> unit) -> 'key theory -> unit
val transf_iter : ('key any -> unit) -> 'key transf -> unit
val metas_iter : ('key any -> unit) -> 'key metas -> unit
val file_iter : ('key any -> unit) -> 'key file -> unit
val session_iter : ('key any -> unit) -> 'key session -> unit
val iter : ('key any -> unit) -> 'key any -> unit
......
......@@ -318,6 +318,7 @@ let update_session ~allow_obsolete old_session env whyconf =
O.reset ();
let (env_session,_) as res =
update_session ~keygen:O.create ~allow_obsolete old_session env whyconf in
dprintf debug "Init_session@\n";
init_session env_session.session;
res
......@@ -485,9 +486,7 @@ let run_external_proof eS eT ?callback a =
end
in
let inplace = npc.prover_config.Whyconf.in_place in
let command =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
let command = Whyconf.get_complete_command npc.prover_config in
(* eprintf "scheduling it...@."; *)
schedule_proof_attempt
~timelimit ~memlimit
......@@ -545,6 +544,9 @@ let run_prover eS eT ~context_unproved_goals_only ~timelimit ~memlimit pr a =
(prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr)
tr.transf_goals
| Metas m ->
prover_on_goal_or_children eS eT
~context_unproved_goals_only ~timelimit ~memlimit pr m.metas_goal
(**********************************)
(* method: replay obsolete proofs *)
......@@ -558,19 +560,20 @@ let proof_successful_or_just_edited a =
let rec replay_on_goal_or_children eS eT
~obsolete_only ~context_unproved_goals_only g =
PHprover.iter
(fun _ a ->
iter_goal
(fun a ->
if not obsolete_only || a.proof_obsolete then
if not context_unproved_goals_only || proof_successful_or_just_edited a
then run_external_proof eS eT a)
g.goal_external_proofs;
PHstr.iter
(fun _ t ->
List.iter
(replay_on_goal_or_children eS eT
~obsolete_only ~context_unproved_goals_only)
t.transf_goals)
g.goal_transformations
(iter_transf
(replay_on_goal_or_children eS eT
~obsolete_only ~context_unproved_goals_only)
)
(iter_metas
(replay_on_goal_or_children eS eT
~obsolete_only ~context_unproved_goals_only)
)
g
let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
match a with
......@@ -598,6 +601,10 @@ let replay eS eT ~obsolete_only ~context_unproved_goals_only a =
(replay_on_goal_or_children eS eT
~obsolete_only ~context_unproved_goals_only)
tr.transf_goals
| Metas m ->
replay_on_goal_or_children eS eT
~obsolete_only ~context_unproved_goals_only m.metas_goal
(***********************************)
(* method: mark proofs as obsolete *)
......@@ -709,9 +716,7 @@ let check_external_proof eS eT todo a =
set_proof_state ~notify ~obsolete:false ~archived:false
result a
in
let command =
String.concat " " (npc.prover_config.Whyconf.command ::
npc.prover_config.Whyconf.extra_options) in
let command = Whyconf.get_complete_command npc.prover_config in
schedule_proof_attempt eT
~timelimit ~memlimit
?old ~inplace ~command
......@@ -758,12 +763,15 @@ let rec play_on_goal_and_children eS eT ~timelimit ~memlimit todo l g =
(* Whyconf.print_prover p g.goal_name.Ident.id_string; *)
prover_on_goal eS eT ~callback ~timelimit ~memlimit p g)
l;
PHstr.iter
(fun _ t ->
List.iter
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
t.transf_goals)
g.goal_transformations
iter_goal
(fun _ -> ())
(iter_transf
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
)
(iter_metas
(play_on_goal_and_children eS eT ~timelimit ~memlimit todo l)
)
g
let play_all eS eT ~callback ~timelimit ~memlimit l =
......@@ -929,6 +937,10 @@ let remove_transformation t =
O.remove t.transf_key;
remove_transformation ~notify t
let remove_metas t =
O.remove t.metas_key;
remove_metas ~notify t
let rec clean = function
| Goal g when g.goal_verified ->
iter_goal
......@@ -937,10 +949,22 @@ let rec clean = function
remove_proof_attempt a)
(fun t ->
if not t.transf_verified then remove_transformation t
else transf_iter clean t) g
else transf_iter clean t)
(fun m ->
if not m.metas_verified then remove_metas m
else metas_iter clean m)
g
| Goal g ->
(** iter only on transformations if the goal is not proved *)
PHstr.iter (fun _ t -> transf_iter clean t) g.goal_transformations
(** don't iter on proof_attempt if the goal is not proved *)
iter_goal
(fun _ -> ())
(fun t ->
if not t.transf_verified then remove_transformation t
else transf_iter clean t)
(fun m ->
if not m.metas_verified then remove_metas m
else metas_iter clean m)
g
| Proof_attempt a -> clean (Goal a.proof_parent)
| any -> iter clean any
......
......@@ -197,6 +197,8 @@ module Make(O: OBSERVER) : sig
val remove_transformation : O.key transf -> unit
val remove_metas : O.key metas -> unit
val set_archive : O.key proof_attempt -> bool -> unit
val clean : O.key any -> unit
......@@ -242,6 +244,15 @@ module Make(O: OBSERVER) : sig
Useful for benchmarking provers
*)
val schedule_proof_attempt:
timelimit:int ->
memlimit:int ->
?old:string ->
inplace:bool ->
command:string ->
driver:Driver.driver ->
callback:(Session.proof_attempt_status -> unit) -> t -> Task.task -> unit
val convert_unknown_prover : O.key env_session -> unit
(** Same as {!Session_tools.convert_unknown_prover} *)
......
......@@ -25,6 +25,8 @@ type checksum = string
let print_checksum = Format.pp_print_string
let string_of_checksum x = x
let checksum_of_string x = x
let equal_checksum x y = (x : checksum) = y
let dumb_checksum = ""
type shape = string
let print_shape = Format.pp_print_string
......
......@@ -24,6 +24,8 @@ type checksum
val print_checksum: Format.formatter -> checksum -> unit
val string_of_checksum: checksum -> string
val checksum_of_string: string -> checksum
val equal_checksum: checksum -> checksum -> bool
val dumb_checksum: checksum
type shape
val print_shape: Format.formatter -> shape -> unit
......
......@@ -20,29 +20,42 @@
open Util
open Ident
open Ty
open Term
open Decl
(** Discard definitions of built-in symbols *)
let add_id q (ls,ld) (abst,defn) = if Sls.mem ls q
let add_id undef_ls rem_ls (ls,ld) (abst,defn) =
if Sls.mem ls rem_ls then
abst,defn
else if Sls.mem ls undef_ls
then create_param_decl ls :: abst, defn
else abst, (ls,ld) :: defn
let elim q spr d = match d.d_node with
(** TODO: go further? such as constructor that are removed? *)
let elim undef_ls rem_pr rem_ls rem_ts d = match d.d_node with
| Dlogic l ->
let ld, id = List.fold_right (add_id q) l ([],[]) in