Commit 4d2d92ca authored by Claude Marche's avatar Claude Marche

Removed (or commented out) some dead code, thanks to OCaml 4.00

parent 30884114
......@@ -23,7 +23,6 @@
open Why3
open Format
(**************)
(*
......
......@@ -23,22 +23,25 @@
open Lexing
open Tptp_ast
open Tptp_parser
open Tptp_typing
open Why3
(* lexical errors *)
exception IllegalCharacter of char
exception UnterminatedComment
(* dead code
exception UnterminatedString
*)
exception UnknownDDW of string
exception UnknownDW of string
let () = Exn_printer.register (fun fmt e -> match e with
| IllegalCharacter c -> fprintf fmt "illegal character %c" c
| UnterminatedComment -> fprintf fmt "unterminated comment"
(* dead code
| UnterminatedString -> fprintf fmt "unterminated string"
*)
| UnknownDDW s -> fprintf fmt "unknown system_word %s" s
| UnknownDW s -> fprintf fmt "unknown defined_word %s" s
| _ -> raise e)
......@@ -243,6 +246,7 @@ and comment_line = parse
{ comment_line lexbuf }
{
(* dead code
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
......@@ -257,6 +261,7 @@ and comment_line = parse
let library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel
~desc:"TPTP format (CNF FOF FOFX TFF)"
*)
}
(*
......
......@@ -19,16 +19,18 @@
/**************************************************************************/
%{
open Parsing
open Tptp_ast
let loc () = (symbol_start_pos (), symbol_end_pos ())
let floc () = Why3.Loc.extract (loc ())
(* dead code
let loc_i i = (rhs_start_pos i, rhs_end_pos i)
let floc_i i = Why3.Loc.extract (loc_i i)
let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
let floc_ij i j = Why3.Loc.extract (loc_ij i j)
*)
let mk_e n = { e_node = n ; e_loc = floc () }
......
......@@ -26,7 +26,6 @@ open Ident
open Ty
open Term
open Decl
open Task
open Printer
let ident_printer =
......
......@@ -66,9 +66,11 @@ type symbol =
| Sdobj of lsymbol
| Suse of theory
(* dead code
type env = symbol Mstr.t
type implicit = (string,symbol) Hashtbl.t
*)
(** Defined symbols : arithmetic etc... *)
......
......@@ -20,7 +20,6 @@
open Format
open Why3
open Util
open Whyconf
let usage_msg =
......
......@@ -18,7 +18,6 @@
(* *)
(**************************************************************************)
open Format
open Util
open Ident
open Ty
......
......@@ -1243,6 +1243,7 @@ let t_equal_alpha = t_equal_alpha (ref (-1)) (ref (-1)) Mvs.empty Mvs.empty
(* hash modulo alpha *)
(* dead code
let rec pat_hash_alpha p =
match p.pat_node with
| Pwild -> 0
......@@ -1254,6 +1255,7 @@ let rec pat_hash_alpha p =
| Por (p, q) ->
Hashcons.combine
(Hashcons.combine 4 (pat_hash_alpha p)) (pat_hash_alpha q)
*)
let rec t_hash_alpha c m t =
let fn = t_hash_alpha c m in
......
......@@ -242,7 +242,7 @@ let ts_tuple_ids = Hid.create 17
let ts_tuple = Util.Hint.memo 17 (fun n ->
let vl = ref [] in
for i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
for _i = 1 to n do vl := create_tvsymbol (id_fresh "a") :: !vl done;
let ts = create_tysymbol (id_fresh ("tuple" ^ string_of_int n)) !vl None in
Hid.add ts_tuple_ids ts.ts_name n;
ts)
......
......@@ -50,7 +50,6 @@ The regexp must start with ^.
open Format
open Util
open Ident
open Whyconf
open Stdlib
module Wc = Whyconf
......@@ -112,10 +111,12 @@ let load_prover kind (id,section) =
(sprintf "In section prover %s command specified without driver" id);
prover
(* dead code
let editor_keys =
let add acc k = Sstr.add k acc in
List.fold_left add Sstr.empty
["command"]
*)
let load_editor section =
check_exhaustive section prover_keys;
......@@ -187,7 +188,9 @@ let read_auto_detection_data main =
| Not_found ->
Loc.errorm "provers-detection-data.conf not found at %s@." filename
(* dead code
let provers_found = ref 0
*)
let read_editors main =
let filename = Filename.concat (Whyconf.datadir main)
......@@ -212,6 +215,7 @@ let make_command =
in
Str.global_substitute cmd_regexp replace com
(* dead code
let sanitize_exec =
let first c = match c with
| '_' | ' ' -> "_"
......@@ -222,6 +226,7 @@ let sanitize_exec =
| _ -> char_to_alnumus c
in
sanitizer first rest
*)
let ask_prover_version exec_name version_switch =
let out = Filename.temp_file "out" "" in
......
......@@ -19,7 +19,6 @@
(**************************************************************************)
open Format
open Sysutil
(** time regexp "%h:%m:%s" *)
type timeunit =
......
......@@ -21,7 +21,6 @@
open Format
open Util
open Ident
open Ty
open Term
open Decl
open Theory
......
......@@ -20,7 +20,7 @@
%{
open Driver_ast
open Parsing
let loc () = Loc.extract (symbol_start_pos (), symbol_end_pos ())
let loc_i i = Loc.extract (rhs_start_pos i, rhs_end_pos i)
let infix s = "infix " ^ s
......
......@@ -683,7 +683,9 @@ let set_policies config policies =
(*******)
(* dead code
let set_conf_file config conf_file = {config with conf_file = conf_file}
*)
let get_conf_file config = config.conf_file
(*******)
......
......@@ -20,7 +20,6 @@
open Format
open Why3
open Util
open Rc
open Whyconf
......@@ -170,6 +169,7 @@ let set_locs_flag =
fun b ->
(if b then Debug.set_flag else Debug.unset_flag) fl
(* dead code
let load_altern alterns (_,section) =
let unknown =
{prover_name = get_string section "unknown_name";
......@@ -186,6 +186,7 @@ let load_altern alterns (_,section) =
prover_altern = get_string ~default:"" section "known_alternative";
} in
Mprover.add unknown known alterns
*)
let load_config config original_config =
(* let main = get_main config in *)
......
......@@ -1078,7 +1078,7 @@ let paste_on_selection () =
match a with
| S.Goal g ->
let keygen = MA.keygen in
let rec paste = function
let paste = function
| S.Transf f ->
MA.init_any
(S.Transf (S.add_transf_to_goal ~keygen (env_session()) g f))
......
......@@ -25,7 +25,6 @@ open Whyconf
open Theory
open Task
open Driver
open Trans
let usage_msg = sprintf
"Usage: %s [options] [[file|-] [-T <theory> [-G <goal>]...]...]..."
......
......@@ -25,7 +25,6 @@ open Ident
open Ptree
open Ty
open Term
open Theory
(** types with destructive type variables *)
......
......@@ -30,10 +30,12 @@ let dummy_id = id_register (id_fresh "dummy")
let glob = Hashtbl.create 5003
(* could be improved with nested hash tables *)
(* dead code
let with_loc f = function
| None -> ()
| Some loc when loc = Loc.dummy_position -> ()
| Some loc -> f loc
*)
let use loc id =
let f, l, c, _ = Loc.get loc in
......
......@@ -22,8 +22,7 @@
open Format
open Lexing
open Term
open Ptree
open Parser
open Parser
(* lexical errors *)
......
......@@ -36,20 +36,22 @@ module Incremental = struct
end
open Ptree
open Parsing
let loc () = (symbol_start_pos (), symbol_end_pos ())
let floc () = Loc.extract (loc ())
let loc_i i = (rhs_start_pos i, rhs_end_pos i)
let floc_i i = Loc.extract (loc_i i)
(* dead code
let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
let floc_ij i j = Loc.extract (loc_ij i j)
*)
let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
let mk_pp d = mk_ppl (floc ()) d
(* dead code
let mk_pp_i i d = mk_ppl (floc_i i) d
*)
let mk_pat p = { pat_loc = floc (); pat_desc = p }
let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
......@@ -132,7 +134,9 @@ end
let id_anonymous () = mk_id "_" (floc ())
let ty_unit () = PPTtuple []
(* dead code
let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
*)
let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }
......@@ -149,9 +153,11 @@ end
pc_pre = p;
pc_post = q; }
(* dead code
let add_init_mark e =
let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
{ e with expr_desc = Emark (init, e) }
*)
let small_integer i =
try
......
......@@ -39,7 +39,9 @@ exception TermExpected
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
exception ClashTheory of string
(* dead code
exception UnboundTheory of qualid
*)
exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
......@@ -67,8 +69,10 @@ let () = Exn_printer.register (fun fmt e -> match e with
fprintf fmt "%a is not a predicate symbol" Pretty.print_ls ls
| ClashTheory s ->
fprintf fmt "Clash with previous theory %s" s
(* dead code
| UnboundTheory q ->
fprintf fmt "unbound theory %a" print_qualid q
*)
| UnboundTypeVar s ->
fprintf fmt "unbound type variable '%s" s
| UnboundType sl ->
......@@ -203,7 +207,9 @@ let find_psymbol q uc = find_psymbol_ns q (get_namespace uc)
let get_dummy_id _ = Glob.dummy_id
let find_namespace_ns = find_ns get_dummy_id ns_find_ns
(* dead code
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
*)
let specialize_lsymbol p uc =
let s = find_lsymbol p uc in
......
......@@ -23,8 +23,6 @@
open Format
open Why3
open Util
open Ident
open Theory
open Typing
open Ptree
open Pgm_module
......
......@@ -22,7 +22,6 @@ open Why3
open Util
open Ident
open Ty
open Decl
open Theory
open Term
......@@ -64,7 +63,9 @@ let ns_add eq chk x v m = Mstr.change (function
| Some vo -> Some (ns_replace eq chk x vo v)) x m
let ex_add = ns_add ls_equal
(* dead code
let mt_add = ns_add mt_equal
*)
let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
......@@ -95,6 +96,7 @@ let impure_uc uc = uc.uc_impure
let effect_uc uc = uc.uc_effect
let pure_uc uc = uc.uc_pure
(* dead code
let add_pervasives uc =
(* type unit = () *)
let ts =
......@@ -102,6 +104,7 @@ let add_pervasives uc =
(id_fresh "unit") [] (Some (Ty.ty_app (Ty.ts_tuple 0) []))
in
add_ty_decl uc ts
*)
let open_namespace uc s = match uc.uc_import with
| ns :: _ -> { uc with
......
......@@ -21,7 +21,6 @@
open Format
open Why3
open Pp
open Ident
open Term
open Pretty
open Pgm_types.T
......
......@@ -19,7 +19,7 @@
(**************************************************************************)
open Why3
open Ident
(*open Ident*)
open Denv
open Ty
open Pgm_types
......
......@@ -19,12 +19,9 @@
(**************************************************************************)
open Why3
open Util
open Ident
open Ty
open Theory
open Term
open Decl
(* model type symbols *)
......@@ -314,8 +311,10 @@ end = struct
let compare_pvsymbol v1 v2 =
compare (id_hash v1.pv_name) (id_hash v2.pv_name)
(* dead code
let equal_pvsymbol v1 v2 =
compare_pvsymbol v1 v2 = 0
*)
(* purify: turns program types into logic types *)
......@@ -699,7 +698,9 @@ end = struct
let print_rset fmt s = print_list comma R.print fmt (Sreg.elements s)
let print_eset fmt s = print_list comma print_ls fmt (Sexn.elements s)
(* dead code
let print_pvset fmt s = print_list comma T.print_pvsymbol fmt (Spv.elements s)
*)
let print fmt e =
if not (Sreg.is_empty e.reads) then
......
......@@ -38,7 +38,9 @@ let debug = Debug.register_info_flag "whyml_typing"
~desc:"Print@ details@ of@ program@ typechecking."
let is_debug () = Debug.test_flag debug
(* dead code
let error = Loc.error
*)
let errorm = Loc.errorm
let id_result = "result"
......@@ -59,8 +61,10 @@ let declare_mutable_field ts i j =
let mutable_field ts i =
Hashtbl.find (Hts.find mutable_fields ts) i
(* dead code
let is_mutable_field ts i =
Hashtbl.mem (Hts.find mutable_fields ts) i
*)
(* phase 1: typing programs (using destructive type inference) **************)
......@@ -91,7 +95,9 @@ let create_denv uc =
let loc_of_id id = Util.of_option id.Ident.id_loc
(* dead code
let loc_of_ls ls = ls.ls_name.Ident.id_loc
*)
let dcurrying tyl ty =
let make_arrow_type ty1 ty2 = tyapp ts_arrow [ty1; ty2] in
......@@ -230,6 +236,7 @@ let expected_type e ty =
"@[this expression has type %a,@ but is expected to have type %a@]"
print_dty e.dexpr_type print_dty ty
(* dead code
let check_mutable_type loc dty = match view_dty dty with
| Denv.Tyapp (ts, _) when is_mutable_ts ts ->
()
......@@ -237,6 +244,7 @@ let check_mutable_type loc dty = match view_dty dty with
errorm ~loc
"@[this expression has type %a,@ but is expected to have a mutable type@]"
print_dty dty
*)
let dexception uc qid =
let sl = Typing.string_list_of_qualid [] qid in
......@@ -850,7 +858,7 @@ let iadd_local env x ty =
in
env, v
let rec type_effect_term env t =
let type_effect_term env t =
let loc = t.pp_loc in
match t.pp_desc with
| PPvar (Qident x) when Mstr.mem x.id env.i_effects ->
......@@ -928,6 +936,7 @@ let iueffect env e = {
ie_raises = e.du_raises;
}
(* dead code
let pre env = Denv.fmla env.i_pures
let post env ((ty, f), ql) =
......@@ -948,6 +957,8 @@ let post env ((ty, f), ql) =
let env = Mstr.add id_result v_result env in
(v_result, Denv.fmla env f), List.map exn ql
*)
let iterm env l =
let t = dterm (pure_uc env.i_uc) env.i_denv l in
let t = Denv.term env.i_pures t in
......@@ -1159,9 +1170,9 @@ let ipattern env p =
(* pretty-printing (for debugging) *)
open Pp
open Pretty
(* dead code
let print_iregion = R.print
let rec print_iexpr fmt e = match e.iexpr_desc with
......@@ -1190,6 +1201,8 @@ let rec print_iexpr fmt e = match e.iexpr_desc with
| _ ->
fprintf fmt "<other>"
*)
let mtv_of_htv htv =
Htv.fold
(fun tv tvar m ->
......@@ -1560,6 +1573,7 @@ let make_apply loc e1 ty c =
Elet (x, e1, any_c), v, ef
let exn_check = ref true
(* dead code
let without_exn_check f x =
if !exn_check then begin
exn_check := false;
......@@ -1567,6 +1581,7 @@ let without_exn_check f x =
with e -> exn_check := true; raise e
end else
f x
*)
(*s Pure expressions. Used in [Slazy_and] and [Slazy_or] to decide
whether to use [strict_bool_and_] and [strict_bool_or_] or not. *)
......@@ -2026,6 +2041,7 @@ let cannot_be_generalized = function
| Tpure ty -> let _, m = cannot_be_generalized_ty ty in m
| Tarrow _ -> false
(* dead code
let check_type_vars ~loc vars ty =
let h = Htv.create 17 in
List.iter (fun v -> Htv.add h v ()) vars;
......@@ -2038,6 +2054,7 @@ let check_type_vars ~loc vars ty =
List.iter check tyl
in
check ty
*)
let make_immutable_type td =
if td.td_vis = Private then errorm ~loc:td.td_loc
......@@ -2152,7 +2169,7 @@ let add_types loc uc dl =
| PPTtyapp (tyl, q) ->
let n = nregions_of_qualid q in
let reg = ref [] in
for i = 1 to n do reg := PPTtyvar (snd (region ())) :: !reg done;
for _i = 1 to n do reg := PPTtyvar (snd (region ())) :: !reg done;
PPTtyapp (List.rev !reg @ List.map add_regions_to_type tyl, q)
| PPTtuple tyl ->
PPTtuple (List.map add_regions_to_type tyl)
......@@ -2205,7 +2222,7 @@ let add_types loc uc dl =
let visited = Hashtbl.create 17 in
let th = effect_uc uc in
let km = get_known th in
let rec visit x =
let visit x =
if not (Hashtbl.mem visited x) then begin
Hashtbl.add visited x ();
if is_debug () then
......@@ -2277,7 +2294,7 @@ let add_logics loc uc d =
let ts = ns_find_ts (get_namespace (impure_uc uc)) p in
let n = (get_mtsymbol ts).mt_regions in
let reg = ref [] in
for i = 1 to n do reg := PPTtyvar (region loc) :: !reg done;
for _i = 1 to n do reg := PPTtyvar (region loc) :: !reg done;
PPTtyapp (List.rev !reg @ List.map add_regions_to_type tyl, q)
| PPTtuple tyl ->
PPTtuple (List.map add_regions_to_type tyl)
......
......@@ -27,7 +27,6 @@ open Term
open Decl
open Theory
open Eval_match
open Pretty
open Pgm_ttree
open Pgm_types
open Pgm_types.T
......@@ -151,11 +150,13 @@ let rec unref ~now s t = match t.t_node with
| _ ->
t_map (unref ~now s) t
(* dead code
let find_constructor env ts =
let km = get_known (pure_uc env) in
match find_constructors km ts with
| [ls] -> ls
| _ -> assert false
*)
let get_ty_subst ty = match ty.ty_node with
| Tyapp (ts, tyl) ->
......
......@@ -133,6 +133,7 @@ let empty_idpos =
idpos_pr = Mpr.empty;
}
(* dead code
let posid_of_idpos idpos =
let posid = Mpos.empty in
let posid = Mts.fold (fun ts pos ->
......@@ -142,6 +143,7 @@ let posid_of_idpos idpos =
let posid = Mpr.fold (fun pr pos ->
Mpos.add pos (MApr pr)) idpos.idpos_pr posid in
posid
*)
type 'a goal =
{ mutable goal_key : 'a;
......@@ -271,7 +273,7 @@ let file_iter_proof_attempt f t =
let session_iter_proof_attempt f s =
PHstr.iter (fun _ file -> file_iter_proof_attempt f file) s.session_files
let rec iter_proof_attempt f = function
let iter_proof_attempt f = function
| Goal g -> goal_iter_proof_attempt f g
| Theory th -> theory_iter_proof_attempt f th
| File file -> file_iter_proof_attempt f file
......@@ -407,6 +409,7 @@ let create_session ?shape_version project_dir =
empty_session ?shape_version project_dir
(* dead code
let load_env_session ?(includes=[]) session conf_path_opt =
let config = Whyconf.read_config conf_path_opt in
let loadpath = (Whyconf.loadpath (Whyconf.get_main config)) @ includes in
......@@ -416,6 +419,7 @@ let load_env_session ?(includes=[]) session conf_path_opt =
whyconf = config;
loaded_provers = PHprover.create 5;
}
*)
(************************)
(* session accessor *)
......@@ -423,19 +427,24 @@ let load_env_session ?(includes=[]) session conf_path_opt =
let get_session_file file = file.file_parent
(* dead code
let get_session_theory th = get_session_file th.theory_parent
*)
(* dead code
let rec get_session_goal goal =
match goal.goal_parent with
| Parent_transf trans -> get_session_trans trans
| Parent_theory th -> get_session_theory th
| Parent_metas metas -> get_session_metas metas
and get_session_trans transf = get_session_goal transf.transf_parent
and get_session_metas metas = get_session_goal metas.metas_parent
let get_session_proof_attempt pa = get_session_goal pa.proof_parent
*)
let get_used_provers session =
let sprover = ref Sprover.empty in
......@@ -1289,7 +1298,9 @@ let load_file session old_provers f =
old_provers
let old_provers = ref Util.Mstr.empty
(* dead code
let get_old_provers () = !old_provers
*)
let load_session session xml =
match xml.Xml.name with
......@@ -1542,10 +1553,12 @@ let add_registered_transformation ~keygen env_session tr_name g =
(** metas *)
(****************)
(* dead code
let task_nb_decl task =
Task.task_fold
(fun n tdecl -> match tdecl.td_node with Decl _ -> n+1 | _ -> n)
0 task
*)
let pos_of_metas lms =
let restore_path id =
......@@ -1833,7 +1846,9 @@ let merge_proof ~keygen obsolete to_goal _ from_proof =
from_proof.proof_prover
from_proof.proof_state)
(* dead code
exception MalformedMetas of ident_path
*)
(** ~theories is the current theory library path empty : [] *)
let rec merge_any_goal ~keygen ~theories env obsolete from_goal to_goal =
......
......@@ -79,11 +79,13 @@ let init_session session = session_iter init_any session
(* | Detected_prover p -> p.prover_id *)
(* | Undetected_prover s -> s *)
(* dead code
let theory_name t = t.theory_name
let theory_key t = t.theory_key
let verified t = t.theory_verified
let goals t = t.theory_goals
let theory_expanded t = t.theory_expanded
*)
let running a = match a.proof_state with
| Undone (Scheduled | Running) -> true
......@@ -208,10 +210,12 @@ let schedule_any_timeout t callback =
t.running_proofs <- (Any_timeout callback) :: t.running_proofs;
run_timeout_handler t
(* dead code