diff --git a/Makefile.in b/Makefile.in index fca262487e3b9329f488774ce910d05279a2255c..4f3801376ac250e8010d1c273982e9327b19be2d 100644 --- a/Makefile.in +++ b/Makefile.in @@ -59,8 +59,8 @@ OCAMLVERSION = @OCAMLVERSION@ #PSVIEWER = @PSVIEWER@ #PDFVIEWER = @PDFVIEWER@ -BFLAGS = -w Ae -warn-error Z -dtypes -g -I src $(INCLUDES) -OFLAGS = -w Ae -warn-error Z -dtypes -I src $(INCLUDES) +BFLAGS = -w Ae -dtypes -g -I src $(INCLUDES) +OFLAGS = -w Ae -dtypes -I src $(INCLUDES) # external libraries common to all binaries diff --git a/src/coq-plugin/whytac.ml b/src/coq-plugin/whytac.ml index 7311b3b046c01855aa8b5a05003a0c6499fbf3d6..ee5788ab2d8579324c8e2ee6329a84833ab7cb80 100644 --- a/src/coq-plugin/whytac.ml +++ b/src/coq-plugin/whytac.ml @@ -271,7 +271,7 @@ and tr_global_ts env r = with Not_found -> add_global global_ts r None; match r with - | VarRef id -> + | VarRef _id -> assert false (*TODO*) | ConstructRef _ -> assert false diff --git a/src/core/decl.ml b/src/core/decl.ml index aa95ecc15792462825611f048c78664e93795d81..2a93b1425ae4ffa7287c84c857fc0b3bf403d70b 100644 --- a/src/core/decl.ml +++ b/src/core/decl.ml @@ -58,16 +58,8 @@ let make_ls_defn ls vl = e_apply (make_fs_defn ls vl) (make_ps_defn ls vl) let open_ls_defn (_,f) = let vl, ef = f_open_forall f in match ef.f_node with - | Fapp (s, [t1; t2]) when s == ps_equ -> - begin match t1.t_node with - | Tapp (fs, _) -> vl, Term t2 - | _ -> assert false - end - | Fbinop (Fiff, f1, f2) -> - begin match f1.f_node with - | Fapp (ps, _) -> vl, Fmla f2 - | _ -> assert false - end + | Fapp (_, [_; t2]) -> vl, Term t2 + | Fbinop (_, _, f2) -> vl, Fmla f2 | _ -> assert false let open_fs_defn ld = let vl,e = open_ls_defn ld in @@ -137,7 +129,7 @@ module Hsdecl = Hashcons.Make (struct | None, None -> true | _ -> false - let eq_iax (pr1,fr1) (pr2,fr2) = pr1 == pr1 && fr1 == fr2 + let eq_iax (pr1,fr1) (pr2,fr2) = pr1 == pr2 && fr1 == fr2 let eq_ind (ps1,al1) (ps2,al2) = ps1 == ps2 && list_all2 eq_iax al1 al2 @@ -507,7 +499,7 @@ let find_prop kn pr = | Dind dl -> let test (_,l) = List.mem_assq pr l in List.assq pr (snd (List.find test dl)) - | Dprop (_,pr,f) -> f + | Dprop (_,_,f) -> f | _ -> assert false exception NonExhaustiveExpr of (pattern list * expr) diff --git a/src/core/term.ml b/src/core/term.ml index 7fb5684e4f9330340dd40e51723377b74a68642b..98e81809648f8efdb80e1d67a67e9bd2b8ba12fb 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -294,10 +294,7 @@ module Hsterm = Hashcons.Make (struct | Tvar v1, Tvar v2 -> v1 == v2 | Tconst c1, Tconst c2 -> c1 = c2 | Tapp (s1, l1), Tapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2 - (* Claude: en voila un beau bug - j'espere que cela convaincra les developpeurs - de Why3 de compiler avec l'option -w Z !!! *) - | Tif (f1, t1, e1), Tif (f2, t2, e2) -> f1 == f2 && t1 == t2 && e2 == e2 + | Tif (f1, t1, e1), Tif (f2, t2, e2) -> f1 == f2 && t1 == t2 && e1 == e2 | Tlet (t1, b1), Tlet (t2, b2) -> t1 == t2 && t_eq_bound b1 b2 | Tcase (tl1, bl1), Tcase (tl2, bl2) -> list_all2 (==) tl1 tl2 && list_all2 t_eq_branch bl1 bl2 @@ -536,22 +533,22 @@ let brlvl fn lvl acc (_, nv, t) = fn (lvl + nv) acc t let t_fold_unsafe fnT fnF lvl acc t = match t.t_node with | Tbvar n when n >= lvl -> raise UnboundIndex | Tbvar _ | Tvar _ | Tconst _ -> acc - | Tapp (f, tl) -> List.fold_left (fnT lvl) acc tl + | Tapp (_, tl) -> List.fold_left (fnT lvl) acc tl | Tif (f, t1, t2) -> fnT lvl (fnT lvl (fnF lvl acc f) t1) t2 - | Tlet (t1, (u, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2 + | Tlet (t1, (_, t2)) -> fnT (lvl + 1) (fnT lvl acc t1) t2 | Tcase (tl, bl) -> List.fold_left (brlvl fnT lvl) (List.fold_left (fnT lvl) acc tl) bl - | Teps (u, f) -> fnF (lvl + 1) acc f + | Teps (_, f) -> fnF (lvl + 1) acc f let f_fold_unsafe fnT fnF lvl acc f = match f.f_node with - | Fapp (p, tl) -> List.fold_left (fnT lvl) acc tl - | Fquant (q, (vl, nv, tl, f1)) -> let lvl = lvl + nv in + | Fapp (_, tl) -> List.fold_left (fnT lvl) acc tl + | Fquant (_, (_, nv, tl, f1)) -> let lvl = lvl + nv in tr_fold (fnT lvl) (fnF lvl) (fnF lvl acc f1) tl - | Fbinop (op, f1, f2) -> fnF lvl (fnF lvl acc f1) f2 + | Fbinop (_, f1, f2) -> fnF lvl (fnF lvl acc f1) f2 | Fnot f1 -> fnF lvl acc f1 | Ftrue | Ffalse -> acc | Fif (f1, f2, f3) -> fnF lvl (fnF lvl (fnF lvl acc f1) f2) f3 - | Flet (t, (u, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1 + | Flet (t, (_, f1)) -> fnF (lvl + 1) (fnT lvl acc t) f1 | Fcase (tl, bl) -> List.fold_left (brlvl fnF lvl) (List.fold_left (fnT lvl) acc tl) bl @@ -732,10 +729,10 @@ and f_s_fold fnT fnL acc f = let fn_v acc u = ty_s_fold fnT acc u.vs_ty in match f.f_node with | Fapp (p, tl) -> List.fold_left fn_t (fnL acc p) tl - | Fquant (q, (vl,_,tl,f1)) -> + | Fquant (_, (vl,_,tl,f1)) -> let acc = List.fold_left fn_v acc vl in fn_f (tr_fold fn_t fn_f acc tl) f1 - | Fbinop (op, f1, f2) -> fn_f (fn_f acc f1) f2 + | Fbinop (_, f1, f2) -> fn_f (fn_f acc f1) f2 | Fnot f1 -> fn_f acc f1 | Ftrue | Ffalse -> acc | Fif (f1, f2, f3) -> fn_f (fn_f (fn_f acc f1) f2) f3 @@ -964,7 +961,7 @@ let f_branch fn acc b = let _,f = f_open_branch b in fn acc f let t_fold fnT fnF acc t = match t.t_node with | Tbvar _ -> raise UnboundIndex | Tvar _ | Tconst _ -> acc - | Tapp (f, tl) -> List.fold_left fnT acc tl + | Tapp (_, tl) -> List.fold_left fnT acc tl | Tif (f, t1, t2) -> fnT (fnT (fnF acc f) t1) t2 | Tlet (t1, b) -> let _,t2 = t_open_bound b in fnT (fnT acc t1) t2 | Tcase (tl, bl) -> @@ -972,10 +969,10 @@ let t_fold fnT fnF acc t = match t.t_node with | Teps b -> let _,f = f_open_bound b in fnF acc f let f_fold fnT fnF acc f = match f.f_node with - | Fapp (p, tl) -> List.fold_left fnT acc tl - | Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in + | Fapp (_, tl) -> List.fold_left fnT acc tl + | Fquant (_, b) -> let _, tl, f1 = f_open_quant b in tr_fold fnT fnF (fnF acc f1) tl - | Fbinop (op, f1, f2) -> fnF (fnF acc f1) f2 + | Fbinop (_, f1, f2) -> fnF (fnF acc f1) f2 | Fnot f1 -> fnF acc f1 | Ftrue | Ffalse -> acc | Fif (f1, f2, f3) -> fnF (fnF (fnF acc f1) f2) f3 @@ -1043,8 +1040,8 @@ let f_subst_single v t1 f = f_v_map (eq_vs v t1) f (* set of free variables *) -let t_freevars s t = t_v_fold (fun s u -> Svs.add u s) Svs.empty t -let f_freevars s f = f_v_fold (fun s u -> Svs.add u s) Svs.empty f +let t_freevars s t = t_v_fold (fun s u -> Svs.add u s) s t +let f_freevars s f = f_v_fold (fun s u -> Svs.add u s) s f (* equality modulo alpha *) @@ -1063,15 +1060,15 @@ let rec t_equal_alpha t1 t2 = | Tif (f1, t1, e1), Tif (f2, t2, e2) -> f_equal_alpha f1 f2 && t_equal_alpha t1 t2 && t_equal_alpha e1 e2 | Tlet (t1, tb1), Tlet (t2, tb2) -> - let v1, b1 = tb1 in - let v2, b2 = tb2 in + let _, b1 = tb1 in + let _, b2 = tb2 in t_equal_alpha t1 t2 && t_equal_alpha b1 b2 | Tcase (tl1, bl1), Tcase (tl2, bl2) -> list_all2 t_equal_alpha tl1 tl2 && list_all2 t_equal_branch_alpha bl1 bl2 | Teps fb1, Teps fb2 -> - let v1, f1 = fb1 in - let v2, f2 = fb2 in + let _, f1 = fb1 in + let _, f2 = fb2 in f_equal_alpha f1 f2 | _ -> false @@ -1092,8 +1089,8 @@ and f_equal_alpha f1 f2 = | Fif (f1, g1, h1), Fif (f2, g2, h2) -> f_equal_alpha f1 f2 && f_equal_alpha g1 g2 && f_equal_alpha h1 h2 | Flet (t1, fb1), Flet (t2, fb2) -> - let v1, f1 = fb1 in - let v2, f2 = fb2 in + let _, f1 = fb1 in + let _, f2 = fb2 in t_equal_alpha t1 t2 && f_equal_alpha f1 f2 | Fcase (tl1, bl1), Fcase (tl2, bl2) -> list_all2 t_equal_alpha tl1 tl2 && @@ -1145,16 +1142,16 @@ let rec t_match s t1 t2 = | Tif (f1, t1, e1), Tif (f2, t2, e2) -> t_match (t_match (f_match s f1 f2) t1 t2) e1 e2 | Tlet (t1, tb1), Tlet (t2, tb2) -> - let v1, b1 = tb1 in - let v2, b2 = tb2 in + let _, b1 = tb1 in + let _, b2 = tb2 in t_match (t_match s t1 t2) b1 b2 | Tcase (tl1, bl1), Tcase (tl2, bl2) -> (try List.fold_left2 t_match_branch (List.fold_left2 t_match s tl1 tl2) bl1 bl2 with Invalid_argument _ -> raise NoMatch) | Teps fb1, Teps fb2 -> - let v1, f1 = fb1 in - let v2, f2 = fb2 in + let _, f1 = fb1 in + let _, f2 = fb2 in f_match s f1 f2 | _ -> raise NoMatch @@ -1175,8 +1172,8 @@ and f_match s f1 f2 = | Fif (f1, g1, h1), Fif (f2, g2, h2) -> f_match (f_match (f_match s f1 f2) g1 g2) h1 h2 | Flet (t1, fb1), Flet (t2, fb2) -> - let v1, f1 = fb1 in - let v2, f2 = fb2 in + let _, f1 = fb1 in + let _, f2 = fb2 in f_match (t_match s t1 t2) f1 f2 | Fcase (tl1, bl1), Fcase (tl2, bl2) -> (try List.fold_left2 f_match_branch diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml index 198cd8b1c06c6235d3b041a3eadacf8c6535473f..d5b2f1a6f6c914c135806a13d0102ba4df8fc08c 100644 --- a/src/driver/call_provers.ml +++ b/src/driver/call_provers.ml @@ -171,7 +171,7 @@ let treat_result pr (t,c,outerr) = here or in the use of why_cpulimit *) Timeout | Unix.WSTOPPED _ | Unix.WSIGNALED _ -> HighFailure - | Unix.WEXITED c -> + | Unix.WEXITED _ -> let rec greps res = function | [] -> HighFailure | (r,pa)::l -> diff --git a/src/driver/driver.ml b/src/driver/driver.ml index 25e48d77d741f72bd7a5995acefd9608d7964830..a446a4bd8aab5e5acc9e14f7945f685f577aeabc 100644 --- a/src/driver/driver.ml +++ b/src/driver/driver.ml @@ -289,7 +289,7 @@ let load_rules env (premap,tmap) {thr_name = loc,qualid; thr_rules = trl} = with Not_found -> errorm ~loc "Unknown proposition %s" (string_of_qualid qualid q) end - | Rprelude (loc,s) -> + | Rprelude (_loc,s) -> let l = try Mid.find th.th_name premap with Not_found -> [] @@ -435,7 +435,7 @@ let file_printer = [] let call_prover_on_file ?debug ?timeout drv filename = - Call_provers.on_file drv.drv_prover filename + Call_provers.on_file ?debug ?timeout drv.drv_prover filename let call_prover_on_formatter ?debug ?timeout ?filename drv ib = Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_prover ib let call_prover_on_buffer ?debug ?timeout ?filename drv ib = diff --git a/src/main.ml b/src/main.ml index af8693633696afea391c557dd9919a08f154cb7e..9197df6502a7013a1dab1b4284ce31c98125addf 100644 --- a/src/main.ml +++ b/src/main.ml @@ -197,7 +197,7 @@ let print_th_namespace fmt th = let fname_printer = ref (Ident.create_ident_printer []) -let do_task env drv fname tname (th : Why.Theory.theory) (task : Task.task) = +let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) = if !opt_prove then begin let res = Driver.call_prover ~debug:!opt_debug ?timeout drv task in printf "%s %s %s : %a@." fname tname diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 55f5c8f00aa9e61101d8b0fbaf5089eb4b9e6302..5ecefdeebeef48675441dfe0899f76a4f176710c 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -217,7 +217,7 @@ let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc) let specialize_lsymbol p uc = let s = find_lsymbol p uc in - s, specialize_lsymbol (qloc p) s + s, specialize_lsymbol ~loc:(qloc p) s let specialize_fsymbol p uc = let s, (tl, ty) = specialize_lsymbol p uc in diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml index 68b62f81b167b22a87fc1e6aa96fc68a0917d8a6..c44a821fc9c17e47ed0eb4530b137b007bcfccda 100644 --- a/src/printer/alt_ergo.ml +++ b/src/printer/alt_ergo.ml @@ -171,7 +171,7 @@ let print_type_decl drv fmt = function let ac_th = ["algebra";"AC"] -let print_logic_decl drv task fmt (ls,ld) = +let print_logic_decl drv _task fmt (ls,ld) = match drv ls.ls_name with | Driver.Remove | Driver.Syntax _ -> false | Driver.Tag s -> diff --git a/src/printer/smt.ml b/src/printer/smt.ml index e3c803aa4b47833009e584c7b9f059d17b6802e1..4541bef85af5306855808da1e28a96febe3cc940 100644 --- a/src/printer/smt.ml +++ b/src/printer/smt.ml @@ -39,7 +39,7 @@ let ident_printer = let print_ident fmt id = fprintf fmt "%s" (id_unique ident_printer id) -let print_tvsymbols fmt id = assert false +let print_tvsymbols _fmt _id = assert false let forget_var v = forget_id ident_printer v.vs_name @@ -117,7 +117,7 @@ let rec print_fmla drv fmt f = match f.f_node with end | Fquant (q, fq) -> let q = match q with Fforall -> "forall" | Fexists -> "exists" in - let vl, tl, f = f_open_quant fq in + let vl, _tl, f = f_open_quant fq in (* TODO trigger *) let rec forall fmt = function | [] -> print_fmla drv fmt f @@ -172,10 +172,10 @@ let print_type_decl drv fmt = function | _, Talgebraic _ -> assert false -let print_logic_decl drv task fmt (ls,ld) = +let print_logic_decl drv _task fmt (ls,ld) = match drv ls.ls_name with | Driver.Remove | Driver.Syntax _ -> false - | Driver.Tag s -> + | Driver.Tag _s -> begin match ld with | None -> begin match ls.ls_value with @@ -189,7 +189,7 @@ let print_logic_decl drv task fmt (ls,ld) = (print_list space (print_type drv)) ls.ls_args (print_type drv) value end - | Some ld -> assert false (* Dealt in Encoding *) + | Some _ -> assert false (* Dealt in Encoding *) end; true @@ -201,7 +201,7 @@ let print_decl drv task fmt d = match d.d_node with | Dind _ -> assert false (* TODO *) | Dprop (Paxiom, pr, _) when drv pr.pr_name = Driver.Remove -> false - | Dprop (Paxiom, pr, f) -> + | Dprop (Paxiom, _pr, f) -> fprintf fmt "@[:assumption@ %a@]@\n" (print_fmla drv) f; true | Dprop (Pgoal, pr, f) -> diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml index 708a28a6108961b1bc359e4b116585ad31099418..dfad8586948547a4f0e46d8a8410298283821b5d 100644 --- a/src/programs/pgm_typing.ml +++ b/src/programs/pgm_typing.ml @@ -151,7 +151,7 @@ and expr_desc env loc = function let e2 = dexpr env e2 in expected_type e2 env.ty_bool; DElazy (op, e1, e2), env.ty_bool - | Pgm_ptree.Ematch (el, bl) -> + | Pgm_ptree.Ematch (_el, _bl) -> assert false (*TODO*) | Pgm_ptree.Eskip -> DEskip, env.ty_unit @@ -222,7 +222,7 @@ and expr_desc env denv = function | DElabel (s, e1) -> Elabel (s, expr env e1) -let code uc id e = +let code uc _id e = let env = create_denv uc in let e = dexpr env e in ignore (expr Mstr.empty e) diff --git a/src/transform/encoding_decorate.ml b/src/transform/encoding_decorate.ml index aa71f140b2ffda9f8e14f9e19e46dbdf346c8428..96fa4dcc314c417971517abb7d0c320f0940d746 100644 --- a/src/transform/encoding_decorate.ml +++ b/src/transform/encoding_decorate.ml @@ -230,7 +230,7 @@ and rewrite_fmla tenv tvar vsvar f = let p = Hls.find tenv.trans_lsymbol p in let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in f_app p tl - | Fquant (q, b) -> let vl, tl, f1 = f_open_quant b in + | Fquant (q, b) -> let vl, _tl, f1 = f_open_quant b in let conv_vs (vsvar,acc) vs = let tres,vsres = let ty_res = conv_ty_pos tenv vs.vs_ty in @@ -268,7 +268,7 @@ let decl (tenv:tenv) d = type which are not in recursive bloc") | Dlogic l -> let fn = function - | ls, Some _ -> assert false (* TODO or not + | _ls, Some _ -> assert false (* TODO or not (remove_logic_definition*) | ls, None -> try @@ -279,7 +279,7 @@ let decl (tenv:tenv) d = Hls.add tenv.trans_lsymbol ls ls_conv; ls_conv,None in [create_logic_decl (List.map fn l)] - | Dind l -> failwith ("Encoding_decorate : I can't work on inductive") + | Dind _ -> failwith ("Encoding_decorate : I can't work on inductive") (* let fn (pr,f) = pr, fnF f in *) (* let fn (ps,l) = ps, List.map fn l in *) (* [create_ind_decl (List.map fn l)] *) diff --git a/src/transform/inlining.ml b/src/transform/inlining.ml index 2a9822e70005ee99dd5986d4f8f9df83152b6591..966a4923a0c48ce48f9dbae199aff5fd5193b8b1 100644 --- a/src/transform/inlining.ml +++ b/src/transform/inlining.ml @@ -56,7 +56,7 @@ and replacep env f = match f.f_node with | Fapp (ps,tl) -> begin try - let (vs,t) = Mls.find ps env.ps in + let (vs,f) = Mls.find ps env.ps in let m = List.fold_left2 (fun acc x y -> Mvs.add x y acc) Mvs.empty vs tl in f_subst m f @@ -101,7 +101,7 @@ let fold isnotinlinedt isnotinlinedf d (env, task) = let vs,e = open_ls_defn ld in let e = e_map (replacet env) (replacep env) e in make_ls_defn ls vs e) dl)) - | Dtype dl -> env,add_decl task d + | Dtype _ -> env,add_decl task d | Dprop (k,pr,f) -> env,add_decl task (create_prop_decl k pr (replacep env f)) @@ -121,14 +121,14 @@ let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false) let trivial = t ~isnotinlinedt:(fun m -> match m.t_node with | Tconst _ | Tvar _ -> false - | Tapp (ls,tl) when List.for_all + | Tapp (_,tl) when List.for_all (fun m -> match m.t_node with | Tvar _ -> true | _ -> false) tl -> false | _ -> true ) ~isnotinlinedf:(fun m -> match m.f_node with | Ftrue | Ffalse -> false - | Fapp (ls,tl) when List.for_all + | Fapp (_,tl) when List.for_all (fun m -> match m.t_node with | Tvar _ -> true | _ -> false) tl -> false