diff --git a/examples/use_api/create_session.ml b/examples/use_api/create_session.ml index 186d3af5bf9ba933325a5fac27c6f336ec8d0d43..70870b23d6a48dc21e0104e68702a01d91843e85 100644 --- a/examples/use_api/create_session.ml +++ b/examples/use_api/create_session.ml @@ -53,21 +53,27 @@ let provers = provers [] +let dummy_keygen ?parent () = () (* a dummy keygen function for sessions *) -let keygen ?parent () = () - (* create an empty session in the current directory *) let env_session,_,_ = let dummy_session : unit Session.session = Session.create_session "." in - Session.update_session ~use_shapes:false ~keygen ~allow_obsolete:true - dummy_session env config + let ctxt = { + Session.allow_obsolete_goals = true; + Session.release_tasks = false; + Session.use_shapes_for_pairing_sub_goals = false; + Session.theory_is_fully_up_to_date = false; + Session.keygen = dummy_keygen; + } + in + Session.update_session ~ctxt dummy_session env config (* adds a file in the new session *) let file : unit Session.file = let file_name = "examples/logic/hello_proof.why" in try - Session.add_file keygen env_session file_name + Session.add_file ~keygen:dummy_keygen env_session file_name with e -> eprintf "@[Error while reading file@ '%s':@ %a@.@]" file_name Exn_printer.exn_printer e; @@ -84,7 +90,7 @@ let add_proofs_attempts g = (fun (p,d) -> let _pa : unit Session.proof_attempt = Session.add_external_proof - ~keygen + ~keygen:dummy_keygen ~obsolete:true ~archived:false ~timelimit:5 diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index ad0bd670ffe529b32e6343c4686625bf7682c7a4..c6214b5826b4c233ef96548270e2e75ae33f663a 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -810,14 +810,8 @@ let sched = S.create_session project_dir, false in let env,(_:bool),(_:bool) = - let ctxt = { - S.allow_obsolete_goals = true; - S.release_tasks = false; - S.use_shapes_for_pairing_sub_goals = use_shapes; - S.theory_is_fully_up_to_date = false; - } - in - M.update_session ~ctxt session gconfig.env gconfig.Gconfig.config + M.update_session ~allow_obsolete:true ~release:false ~use_shapes + session gconfig.env gconfig.Gconfig.config in Debug.dprintf debug "@]@\n[GUI session] Opening session: update done@. @["; let sched = M.init (gconfig.session_nb_processes) @@ -1964,14 +1958,8 @@ let reload () = let old_session = (env_session()).S.session in let new_env_session,(_:bool),(_:bool) = (* use_shapes is true since session is in memory *) - let ctxt = { - S.allow_obsolete_goals = true; - S.release_tasks = false; - S.use_shapes_for_pairing_sub_goals = true; - S.theory_is_fully_up_to_date = false; - } - in - M.update_session ~ctxt old_session gconfig.env gconfig.Gconfig.config + M.update_session ~allow_obsolete:true ~release:false ~use_shapes:true + old_session gconfig.env gconfig.Gconfig.config in current_env_session := Some new_env_session with diff --git a/src/session/session.ml b/src/session/session.ml index 03fa140250f7676751378a2fcf0fdb34fb719a88..2018bfc8d368ed3e464b000195afa2181d0ecdd1 100644 --- a/src/session/session.ml +++ b/src/session/session.ml @@ -1107,7 +1107,7 @@ let string_attribute field r = field r.Xml.name; assert false -let keygen ?parent:_ () = () +let dummy_keygen ?parent:_ () = () let load_result r = match r.Xml.name with @@ -1199,7 +1199,7 @@ let rec load_goal ctxt parent acc g = in let expanded = bool_attribute "expanded" g false in let mg = - raw_add_no_task ~keygen ~expanded parent gname expl sum shape + raw_add_no_task ~keygen:dummy_keygen ~expanded parent gname expl sum shape in List.iter (load_proof_or_transf ctxt mg) g.Xml.elements; mg.goal_verified <- goal_verified mg; @@ -1239,7 +1239,7 @@ and load_proof_or_transf ctxt mg a = end; *) let (_ : 'a proof_attempt) = - add_external_proof ~keygen ~archived ~obsolete + add_external_proof ~keygen:dummy_keygen ~archived ~obsolete ~timelimit ~memlimit ~edit mg p res in () @@ -1250,7 +1250,7 @@ and load_proof_or_transf ctxt mg a = | "transf" -> let trname = string_attribute "name" a in let expanded = bool_attribute "expanded" a false in - let mtr = raw_add_transformation ~keygen ~expanded mg trname in + let mtr = raw_add_transformation ~keygen:dummy_keygen ~expanded mg trname in mtr.transf_goals <- List.rev (List.fold_left @@ -1368,7 +1368,7 @@ and load_metas ctxt mg a = let metas_args = List.fold_left load_meta Mstr.empty metas_args in let expanded = bool_attribute "expanded" a false in - let metas = raw_add_metas ~keygen ~expanded mg metas_args idpos in + let metas = raw_add_metas ~keygen:dummy_keygen ~expanded mg metas_args idpos in let goal = match goal with | [] -> raise (LoadError (a,"No subgoal for this metas")) | [goal] -> goal @@ -1390,7 +1390,7 @@ let load_theory ctxt mf acc th = let expanded = bool_attribute "expanded" th false in let csum = string_attribute_opt "sum" th in let checksum = Opt.map Tc.checksum_of_string csum in - let mth = raw_add_theory ~keygen ~expanded ~checksum mf thname in + let mth = raw_add_theory ~keygen:dummy_keygen ~expanded ~checksum mf thname in mth.theory_goals <- List.rev (List.fold_left @@ -1408,7 +1408,7 @@ let load_file session old_provers f = let fn = string_attribute "name" f in let fmt = load_option "format" f in let expanded = bool_attribute "expanded" f false in - let mf = raw_add_file ~keygen ~expanded session fn fmt in + let mf = raw_add_file ~keygen:dummy_keygen ~expanded session fn fmt in mf.file_theories <- List.rev (List.fold_left @@ -2215,11 +2215,12 @@ let rec release_sub_tasks g = exception UnrecoverableTask of Ident.ident -type update_context = +type 'key update_context = { allow_obsolete_goals : bool; release_tasks : bool; use_shapes_for_pairing_sub_goals : bool; theory_is_fully_up_to_date : bool; + keygen : 'key keygen; } let rec recover_sub_tasks ~theories env_session task g = @@ -2272,17 +2273,17 @@ let goal_task_or_recover env_session g = (** merge session *) (** ~theories is the current theory library path empty : [] *) -let rec merge_any_goal ~ctxt ~keygen ~theories env obsolete from_goal to_goal = +let rec merge_any_goal ~ctxt ~theories env obsolete from_goal to_goal = set_goal_expanded to_goal from_goal.goal_expanded; - PHprover.iter (merge_proof ~keygen obsolete to_goal) + PHprover.iter (merge_proof ~keygen:ctxt.keygen obsolete to_goal) from_goal.goal_external_proofs; - PHstr.iter (merge_trans ~ctxt ~keygen ~theories env to_goal) + PHstr.iter (merge_trans ~ctxt ~theories env to_goal) from_goal.goal_transformations; - Mmetas_args.iter (merge_metas ~ctxt ~keygen ~theories env to_goal) + Mmetas_args.iter (merge_metas ~ctxt ~theories env to_goal) from_goal.goal_metas -and merge_trans ~ctxt ~keygen ~theories env to_goal _ from_transf = +and merge_trans ~ctxt ~theories env to_goal _ from_transf = try let from_transf_name = from_transf.transf_name in let to_goal_name = to_goal.goal_name in @@ -2291,7 +2292,7 @@ and merge_trans ~ctxt ~keygen ~theories env to_goal _ from_transf = let to_transf = try add_registered_transformation - ~keygen env from_transf_name to_goal + ~keygen:ctxt.keygen env from_transf_name to_goal with exn when not (Debug.test_flag Debug.stack_trace) -> Debug.dprintf debug "[Reload] transformation %s produce an error:%a" from_transf_name Exn_printer.exn_printer exn; @@ -2307,7 +2308,7 @@ and merge_trans ~ctxt ~keygen ~theories env to_goal _ from_transf = in List.iter (function | (to_goal, Some (from_goal, obsolete)) -> - merge_any_goal ~ctxt ~keygen ~theories env obsolete from_goal to_goal + merge_any_goal ~ctxt ~theories env obsolete from_goal to_goal | (_, None) -> found_missed_goals := true) associated @@ -2315,7 +2316,7 @@ and merge_trans ~ctxt ~keygen ~theories env to_goal _ from_transf = (** convert the ident from the old task to the ident at the same position in the new task *) -and merge_metas_aux ~ctxt ~keygen ~theories env to_goal _ from_metas = +and merge_metas_aux ~ctxt ~theories env to_goal _ from_metas = Debug.dprintf debug "[Reload] metas for goal %s@\n" to_goal.goal_name.Ident.id_string; @@ -2323,28 +2324,28 @@ and merge_metas_aux ~ctxt ~keygen ~theories env to_goal _ from_metas = merge_metas_in_task ~theories env (goal_task to_goal) from_metas in let to_metas = - raw_add_metas ~keygen ~expanded:from_metas.metas_expanded + raw_add_metas ~keygen:ctxt.keygen ~expanded:from_metas.metas_expanded to_goal metas to_idpos in let to_goal = raw_add_task ~version:env.session.session_shape_version - ~keygen (Parent_metas to_metas) ~expanded:true + ~keygen:ctxt.keygen (Parent_metas to_metas) ~expanded:true to_goal.goal_name to_goal.goal_expl task in to_metas.metas_goal <- to_goal; Debug.dprintf debug "[Reload] metas done@\n"; - merge_any_goal ~ctxt ~keygen ~theories env obsolete from_metas.metas_goal to_goal + merge_any_goal ~ctxt ~theories env obsolete from_metas.metas_goal to_goal -and merge_metas ~ctxt ~keygen ~theories env to_goal s from_metas = +and merge_metas ~ctxt ~theories env to_goal s from_metas = try - merge_metas_aux ~ctxt ~keygen ~theories env to_goal s from_metas + merge_metas_aux ~ctxt ~theories env to_goal s from_metas with exn -> Debug.dprintf debug "[merge metas] error %a during merge, metas removed@\n" Exn_printer.exn_printer exn exception OutdatedSession -let merge_theory ~ctxt ~keygen ~theories env from_th to_th = +let merge_theory ~ctxt ~theories env from_th to_th = set_theory_expanded to_th from_th.theory_expanded; let from_goals = List.fold_left (fun from_goals g -> @@ -2382,8 +2383,7 @@ let merge_theory ~ctxt ~keygen ~theories env from_th to_th = if not ctxt.allow_obsolete_goals then raise OutdatedSession; found_obsolete := true; end; - merge_any_goal ~ctxt ~keygen ~theories env goal_obsolete - from_goal to_goal; + merge_any_goal ~ctxt ~theories env goal_obsolete from_goal to_goal; if ctxt.release_tasks then release_sub_tasks to_goal with | Not_found when ctxt.allow_obsolete_goals -> @@ -2392,7 +2392,7 @@ let merge_theory ~ctxt ~keygen ~theories env from_th to_th = | Not_found -> raise OutdatedSession ) to_th.theory_goals -let merge_file ~ctxt ~keygen ~theories env from_f to_f = +let merge_file ~ctxt ~theories env from_f to_f = Debug.dprintf debug "[Info] merge_file, shape_version = %d@\n" env.session.session_shape_version; set_file_expanded to_f from_f.file_expanded; @@ -2409,7 +2409,7 @@ let merge_file ~ctxt ~keygen ~theories env from_f to_f = (* TODO: remove this later when all sessions are updated *) with Not_found -> Mstr.find ("WP "^name) from_theories in - merge_theory ~ctxt ~keygen ~theories env from_th to_th + merge_theory ~ctxt ~theories env from_th to_th with | Not_found when ctxt.allow_obsolete_goals -> () | Not_found -> raise OutdatedSession @@ -2438,9 +2438,7 @@ let recompute_all_shapes ~release session = session.session_shape_version <- Termcode.current_shape_version; iter_session (recompute_all_shapes_file ~release) session -let update_session ~ctxt - (* ?(release=false) *) ~keygen (* ~allow_obsolete *) old_session - env whyconf = +let update_session ~ctxt old_session env whyconf = Debug.dprintf debug "[Info] update_session: shape_version = %d@\n" old_session.session_shape_version; AssoGoals.set_use_shapes ctxt.use_shapes_for_pairing_sub_goals; @@ -2464,7 +2462,7 @@ let update_session ~ctxt PHstr.fold (fun _ old_file acc -> Debug.dprintf debug "[Load] file '%s'@\n" old_file.file_name; let new_file = add_file - ~keygen new_env_session + ~keygen:ctxt.keygen new_env_session ?format:old_file.file_format old_file.file_name in let theories = Opt.get new_file.file_for_recovery in @@ -2472,7 +2470,7 @@ let update_session ~ctxt let ctxt = { ctxt with release_tasks = ctxt.release_tasks && (not will_recompute_shape) } in - merge_file ~ctxt ~keygen ~theories new_env_session old_file new_file; + merge_file ~ctxt ~theories new_env_session old_file new_file; let fname = Filename.basename (Filename.chop_extension old_file.file_name) in diff --git a/src/session/session.mli b/src/session/session.mli index 199213eea6855c08624e258c7f58c965d8ee0948..d2c5a022fca989ef08fbf6bb262838605d616fac 100644 --- a/src/session/session.mli +++ b/src/session/session.mli @@ -239,24 +239,16 @@ exception OutdatedSession exception ShapesFileError of string exception SessionFileError of string -type update_context = +type 'key update_context = { allow_obsolete_goals : bool; release_tasks : bool; use_shapes_for_pairing_sub_goals : bool; theory_is_fully_up_to_date : bool; + keygen : 'key keygen; } -val update_session : ctxt:update_context -> -(* - use_shapes:bool -> - ?release:bool (* default false *) -> -*) - keygen:'a keygen -> -(* - allow_obsolete:bool -> -*) -'b session -> - Env.env -> Whyconf.config -> 'a env_session * bool * bool +val update_session : ctxt:'key update_context -> 'a session -> + Env.env -> Whyconf.config -> 'key env_session * bool * bool (** reload the given session with the given environnement : - the files are reloaded - apply again the transformation diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index 3ebf3c9fabc0ad9b0c37c78cbb7789494066ba74..2e2ce4ed7862ff27d9194d3585cedf8909bed3e9 100644 --- a/src/session/session_scheduler.ml +++ b/src/session/session_scheduler.ml @@ -312,10 +312,19 @@ let rec init_any any = O.init (key_any any) any; iter init_any any let init_session session = session_iter init_any session -let update_session ~ctxt old_session env whyconf = +let update_session ~allow_obsolete ~release ~use_shapes + old_session env whyconf = O.reset (); + let ctxt = { + allow_obsolete_goals = allow_obsolete; + release_tasks = release; + use_shapes_for_pairing_sub_goals = use_shapes; + theory_is_fully_up_to_date = false; (* dummy initialisation *) + keygen = O.create; + } + in let (env_session,_,_) as res = - update_session ~ctxt ~keygen:O.create old_session env whyconf + update_session ~ctxt old_session env whyconf in Debug.dprintf debug "Init_session@\n"; init_session env_session.session; diff --git a/src/session/session_scheduler.mli b/src/session/session_scheduler.mli index 1e9516a9a8bfe903024448f0c7aee1a6290ec5a9..5141d5cc7c61d5f9dede4fab64b154d6c7a90d24 100644 --- a/src/session/session_scheduler.mli +++ b/src/session/session_scheduler.mli @@ -110,11 +110,9 @@ module Make(O: OBSERVER) : sig (** {2 Save and load a state} *) val update_session : - ctxt:update_context -> -(* - ?release:bool -> allow_obsolete:bool -> -*) + release:bool -> + use_shapes:bool -> 'key session -> Env.env -> Whyconf.config -> O.key env_session * bool * bool diff --git a/src/tools/why3replay.ml b/src/tools/why3replay.ml index a2b157cdba1bb48279942f2de8996af3be4d66dc..b85776975dbb959e7a7bb24232291ec3a1bc6d30 100644 --- a/src/tools/why3replay.ml +++ b/src/tools/why3replay.ml @@ -400,14 +400,8 @@ let () = O.verbose := Debug.test_flag debug; let env_session,found_obs,some_merge_miss = let session, use_shapes = S.read_session project_dir in - let ctxt = { - S.allow_obsolete_goals = true; - S.release_tasks = false; - S.use_shapes_for_pairing_sub_goals = use_shapes; - S.theory_is_fully_up_to_date = false; - } - in - M.update_session ~ctxt session env config + M.update_session ~allow_obsolete:true ~release:false ~use_shapes + session env config in Debug.dprintf debug " done.@."; if !opt_obsolete_only && not found_obs diff --git a/src/why3session/why3session_lib.ml b/src/why3session/why3session_lib.ml index e5e41080c27a138de020df7b15432077206bc9de..be95bb775c2683e3d01ebcdff10261984bfeb857 100644 --- a/src/why3session/why3session_lib.ml +++ b/src/why3session/why3session_lib.ml @@ -80,9 +80,9 @@ let read_update_session ~allow_obsolete env config fname = S.release_tasks = false; S.use_shapes_for_pairing_sub_goals = use_shapes; S.theory_is_fully_up_to_date = false; - } + S.keygen = fun ?parent:_ _ -> (); + } in - let keygen ?parent:_ _ = () in Session.update_session ~ctxt ~keygen session env config (** filter *)