Commit b43e3c1d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove dead code.

parent 2b5ecd47
......@@ -107,8 +107,6 @@ let deref env t =
mk_term ~loc:t.term_loc (Tlet (id, tid, t)) in
Mstr.fold deref env.vars t
let stmt_of_decl = function Dstmt s -> s | _ -> invalid_arg "not a statement"
let rec has_stmt p = function
| Dstmt s -> p s || begin match s.stmt_desc with
| Sbreak | Sreturn _ | Sassign _ | Slabel _
......@@ -197,16 +195,6 @@ let rec expr env {Py_ast.expr_loc = loc; Py_ast.expr_desc = d } = match d with
| Py_ast.Eget (e1, e2) ->
mk_expr ~loc (Eidapp (get_op ~loc, [expr env e1; expr env e2]))
let post env (loc, l) =
loc, List.map (fun (pat, t) -> pat, deref env t) l
let spec env sp =
assert (sp.sp_xpost = [] && sp.sp_reads = [] && sp.sp_writes = []
&& sp.sp_variant = []);
{ sp with
sp_pre = List.map (deref env) sp.sp_pre;
sp_post = List.map (post env) sp.sp_post }
let no_params ~loc = [loc, None, false, Some (PTtuple [])]
let rec stmt env ({Py_ast.stmt_loc = loc; Py_ast.stmt_desc = d } as s) =
......
......@@ -101,7 +101,6 @@ let load_driver_absolute = let driver_tag = ref (-1) in fun env file extra_files
| ExitCodeValid s -> add_to_list exitcodes (s, Valid)
| ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
| ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
| ExitCodeOutOfMemory s -> add_to_list exitcodes (s, OutOfMemory)
| ExitCodeStepLimitExceeded s ->
add_to_list exitcodes (s, StepLimitExceeded)
| ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
......
......@@ -70,7 +70,6 @@ type global =
| ExitCodeValid of int
| ExitCodeInvalid of int
| ExitCodeTimeout of int
| ExitCodeOutOfMemory of int
| ExitCodeStepLimitExceeded of int
| ExitCodeUnknown of int * string
| ExitCodeFailure of int * string
......
......@@ -589,12 +589,8 @@ let get_obs (pa_st: pa_status) = match pa_st with
let get_proof_attempt (pa_st: pa_status) = match pa_st with
| pa, _, _ -> pa
let get_limit (pa_st: pa_status) = match pa_st with
| _, _, l -> l
let get_node_obs id = get_obs (get_node_id_pa id)
let get_node_proof_attempt id = get_proof_attempt (get_node_id_pa id)
let get_node_limit id = get_limit (get_node_id_pa id)
let get_node_id iter = goals_model#get ~row:iter ~column:node_id_column
......@@ -645,9 +641,9 @@ let notebook = GPack.notebook ~packing:vpan222#add ()
(********************************)
(* Task view (part of notebook) *)
(********************************)
let task_page,scrolled_task_view =
let scrolled_task_view =
let label = GMisc.label ~text:"Task" () in
0, GPack.vbox ~homogeneous:false ~packing:
GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(notebook#append_page ~tab_label:label#coerce w)) ()
let scrolled_task_view =
......@@ -767,15 +763,15 @@ let error_page,error_view =
0, GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()
let log_page,log_view =
let log_view =
let label = GMisc.label ~text:"Log" () in
1, GPack.vbox ~homogeneous:false ~packing:
GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()
(* tab 3: edited proof *)
let edited_page,edited_tab =
let edited_tab =
let label = GMisc.label ~text:"Edited proof" () in
2, GPack.vbox ~homogeneous:false ~packing:
GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()
let scrolled_edited_view =
......@@ -791,9 +787,9 @@ let edited_view =
()
(* tab 4: prover output *)
let output_page,output_tab =
let output_tab =
let label = GMisc.label ~text:"Prover output" () in
3, GPack.vbox ~homogeneous:false ~packing:
GPack.vbox ~homogeneous:false ~packing:
(fun w -> ignore(messages_notebook#append_page ~tab_label:label#coerce w)) ()
let scrolled_output_view =
......@@ -1011,22 +1007,6 @@ let reload_unsafe () =
let save_and_reload () = save_sources (); reload_unsafe ()
(* Same as reload_safe but propose to save edited sources before reload *)
let reload_safe () =
if files_need_saving () then
let answer =
GToolbox.question_box
~title:"Why3 saving source files"
~buttons:["Yes"; "No"; "Cancel"]
"Do you want to save modified source files before refresh?\nBeware that unsaved modifications will be discarded."
in
match answer with
| 1 -> save_and_reload ()
| 2 -> reload_unsafe ()
| _ -> ()
else
reload_unsafe ()
(****************************)
(* command entry completion *)
(****************************)
......@@ -1106,7 +1086,7 @@ let color_line ~color loc =
let f, l, _, _ = Loc.get loc in
try
let (_, v, _, _) = get_source_view_table f in
let v = get_source_view f in
let color = convert_color color in
color_line ~color v l
with
......@@ -1132,10 +1112,7 @@ let color_loc ?(ce=false) ~color loc =
let f, l, b, e = Loc.get loc in
try
let v = if ce then counterexample_view else
let (_, v, _, _) = get_source_view_table f in
v
in
let v = if ce then counterexample_view else get_source_view f in
let color = convert_color color in
color_loc ~color v l b e
with
......@@ -1551,35 +1528,6 @@ let treat_message_notification msg = match msg with
print_message ~kind:1 ~notif_kind:"General request failure" "%s" s
(***********************)
(* First Unproven goal *)
(***********************)
let is_goal node =
get_node_type node = NGoal
let proved node =
get_node_proved node
let children node =
let iter = (get_node_row node)#iter in
let n = goals_model#iter_n_children (Some iter) in
let acc = ref [] in
for i = 0 to (n-1) do
let new_iter = goals_model#iter_children ?nth:(Some i) (Some iter) in
let child_node = get_node_id new_iter in
if (get_node_type child_node != NProofAttempt) then
acc := child_node :: !acc
done;
!acc
let get_parent node =
let iter = (get_node_row node)#iter in
let parent_iter = goals_model#iter_parent iter in
match parent_iter with
| None -> None
| Some parent -> Some (get_node_id parent)
let is_selected_alone id =
match get_selected_row_references () with
| [r] -> let i = get_node_id r#iter in i = id
......
......@@ -16,8 +16,6 @@ let flag = Debug.register_flag "track_symbol_use"
let () = Debug.unset_flag flag (* make sure it is unset by default *)
let dummy_id = id_register (id_fresh "dummy")
type def_use = Def | Use
let glob = Hashtbl.create 5003
......
......@@ -13,8 +13,6 @@ open Ident
val flag: Debug.flag
val dummy_id: ident
val def: kind:string -> ident -> unit
(** [def id] registers that [id] is defined at position [id.id_loc] *)
......
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