1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91
|
(******************************************************************************)
(* The Alt-Ergo theorem prover *)
(* Copyright (C) 2006-2013 *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* Sylvain Conchon *)
(* Evelyne Contejean *)
(* *)
(* Francois Bobot *)
(* Mohamed Iguernelala *)
(* Stephane Lescuyer *)
(* Alain Mebsout *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(******************************************************************************)
open Gui_session
open Why_annoted
open Why_connected
let replay_prune id env =
match findbyid id env.ast with
| AD (ad, _) -> prune ~register:false env ad
| AF (af, _) -> prune ~register:false env af
| AT at -> prune ~register:false env at
| QF aq -> prune ~register:false env aq
let replay_incorrect_prune id env =
match findbyid id env.ast with
| AD (ad, _) -> incorrect_prune ~register:false env ad
| AF (af, _) -> incorrect_prune ~register:false env af
| AT at -> incorrect_prune ~register:false env at
| QF aq -> incorrect_prune ~register:false env aq
let replay_unprune id env =
match findbyid id env.ast with
| AD (ad, _) -> unprune ~register:false env ad
| AF (af, _) -> unprune ~register:false env af
| AT at -> unprune ~register:false env at
| QF aq -> unprune ~register:false env aq
let replay_addinstance id aname entries env =
match findbyid id env.ast with
| AD (ad, _) ->
begin
match ad.c with
| AAxiom (_, aname, inv, af) ->
add_instance ~register:false env id af aname inv entries
| APredicate_def (_, aname,_ , af) ->
add_instance ~register:false env id af aname false entries
| _ -> assert false
end
| _ -> assert false
let replay_limitlemma id name nb env =
Hashtbl.add env.insts.h id (ref None, ref 0, name, ref nb)
let replay env = function
| Prune id -> replay_prune id env
| IncorrectPrune id -> replay_incorrect_prune id env
| Unprune id -> replay_unprune id env
| AddInstance (id, aname, entries) -> replay_addinstance id aname entries env
| AddTrigger (id, inst_buf, str) ->
readd_trigger ~register:false env id str inst_buf
| LimitLemma (id, name, nb) -> replay_limitlemma id name nb env
| UnlimitLemma (id, name) -> replay_limitlemma id name (-1) env
let replay_session env =
let l = ref [] in
Stack.iter (fun a -> l := a::!l) env.actions;
List.iter (replay env) !l
let undo_action env =
match Stack.pop env.actions with
| Prune id | IncorrectPrune id -> replay env (Unprune id)
| Unprune id -> replay env (Prune id)
| ((AddInstance _ | AddTrigger _ ) as ac) ->
replay env (Prune (Hashtbl.find resulting_ids ac))
| LimitLemma (id, name, _) | UnlimitLemma (id, name) ->
try
Stack.iter (function
| (LimitLemma (id', _, _) | UnlimitLemma (id', _) as ac)
when id = id' ->
replay env ac; raise Exit
| _ -> ()) env.actions;
replay env (LimitLemma (id, name, -1))
with Exit -> ()
|