File: gui_session.ml

package info (click to toggle)
alt-ergo 0.95.2-3
  • links: PTS, VCS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 1,528 kB
  • ctags: 3,449
  • sloc: ml: 19,645; makefile: 354
file content (107 lines) | stat: -rw-r--r-- 4,112 bytes parent folder | download
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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
(******************************************************************************)
(*     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         *)
(******************************************************************************)

type action =
  | Prune of int
  | IncorrectPrune of int
  | Unprune of int
  | AddInstance of int * string * string list
  | AddTrigger of int * bool * string
  | LimitLemma of int * string * int
  | UnlimitLemma of int * string

let resulting_ids = Hashtbl.create 17

let save actions ac = 
  (* (match ac with *)
  (*   | Prune id -> Format.eprintf "Prune %d@." id *)
  (*   | IncorrectPrune id -> Format.eprintf "Incorrectprune %d@." id *)
  (*   | Unprune id -> Format.eprintf "Unrune %d@." id *)
  (*   | AddInstance (id, name, vars) -> *)
  (*     Format.eprintf "AddInstance %d %s@." id name *)
  (*   | AddTrigger (id, inst_buf, trs) -> *)
  (*     Format.eprintf "AddTriger %d %b %s@." id inst_buf trs *)
  (*   | LimitLemma (id, name, nb) -> *)
  (*     Format.eprintf "LimitLemma %d-%s %d@." id name nb *)
  (* ); *)
  Stack.push ac actions

let compute_ids_offsets old_res res =
  List.fold_left (fun acc (name1, id1) ->
    try let id2 = List.assoc name1 res in 
	(* if id1 = id2 then acc else *) (id1, id2 - id1)::acc
    with Not_found -> acc) [] old_res

let offset_id id offsets =
  let nid = ref id in
  try 
    List.iter 
      (fun (i, off) ->
	if id <= i then (nid := id + off; raise Exit))
      offsets;
    id
  with Exit -> !nid


let offset_stack st offsets =
  let l = ref [] in
  while not (Stack.is_empty st) do
    let ac = match Stack.pop st with
      | Prune id -> Prune (offset_id id offsets)
      | IncorrectPrune id -> IncorrectPrune (offset_id id offsets)
      | Unprune id -> Unprune (offset_id id offsets)
      | AddInstance (id, name, vars) ->
	AddInstance ((offset_id id offsets), name, vars)
      | AddTrigger (id, inst_buf, trs) ->
	AddTrigger ((offset_id id offsets), inst_buf, trs)
      | LimitLemma (id, name, nb) ->
	LimitLemma ((offset_id id offsets), name, nb)
      | UnlimitLemma (id, name) ->
	UnlimitLemma ((offset_id id offsets), name)
    in
    l := ac :: !l
  done;
  List.iter (fun ac -> Stack.push ac st) !l

let read_actions res = function
  | Some cin -> 
    begin
      try 
	let old_res = (input_value cin: (string * int) list) in
	let st = (input_value cin: action Stack.t) in
	let offsets = compute_ids_offsets old_res res in
	offset_stack st offsets;
	st
      with End_of_file -> Stack.create ()
    end
  | None -> Stack.create ()


module SI = Set.Make (struct type t = int let compare = compare end)

let safe_session actions =
  let l = ref [] in
  Stack.iter (fun a -> l := a::!l) actions;
  let list_actions = !l in
  let _, incorrect_prunes = 
    List.fold_left (fun (prunes, incorrect_prunes) -> function
      | Prune id -> SI.add id prunes, incorrect_prunes
      | IncorrectPrune id -> prunes, SI.add id incorrect_prunes
      | Unprune id -> SI.remove id prunes, SI.remove id incorrect_prunes
      | _ -> prunes, incorrect_prunes)
      (SI.empty, SI.empty) list_actions
  in
  SI.is_empty incorrect_prunes