Skip to content

GitLab

why3
why3
Commit c5e93f64 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

cleaning up sources: no more tabulation and headers

parent 5fabaead
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 2774 additions and 2448 deletions
Makefile.in
View file @ c5e93f64
##########################################################################
# #
# Copyright (C) 2010- #
# Copyright (C) 2010-2011 #
# François Bobot #
# Jean-Christophe Filliâtre #
# Claude Marché #
......
configure.in
View file @ c5e93f64
##########################################################################
# #
# Copyright (C) 2010- #
# Copyright (C) 2010-2011 #
# François Bobot #
# Jean-Christophe Filliâtre #
# Claude Marché #
......
src/bench/bench.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/bench/bench.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/bench/benchdb.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** run benchs from the database *)
open Format
......
src/bench/benchdb.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** run benchs from the database *)
open Why
......
src/bench/benchrc.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
......
src/bench/benchrc.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(**
......
src/bench/whybench.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/config/whyconfig.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/coq-plugin/g_whytac.ml4
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/coq-plugin/whytac.ml
View file @ c5e93f64
This diff is collapsed.
src/core/decl.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/decl.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/env.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/env.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/ident.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/ident.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/pattern.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/pattern.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/pretty.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/pretty.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/printer.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......@@ -147,8 +147,8 @@ let print_prelude fmt pl =
let print_prelude_of_theories th_used fmt pm =
List.iter (fun th ->
let prel = Mid.find_default th.th_name [] pm in
print_prelude fmt prel) th_used
let prel = Mid.find_default th.th_name [] pm in
print_prelude fmt prel) th_used
let print_th_prelude task fmt pm =
let th_used = task_fold (fun acc -> function
......
src/core/printer.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/task.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/task.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/term.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/term.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/theory.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......@@ -728,8 +728,8 @@ let on_meta _meta fn acc theory =
List.fold_left
(fun acc td ->
match td.td_node with
| Meta (_,ma) -> fn acc ma
| _ -> acc)
| Meta (_,ma) -> fn acc ma
| _ -> acc)
acc tdecls
......
src/core/theory.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/trans.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/trans.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/ty.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/core/ty.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/autodetection.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......@@ -129,7 +129,7 @@ let detect_exec main data com =
let ch = open_in out in
let c = Sysutil.channel_contents ch in
close_in ch;
Sys.remove out;
Sys.remove out;
c
with Not_found | End_of_file -> ""
in
......@@ -142,7 +142,7 @@ let detect_exec main data com =
None
else begin
if List.mem ver data.versions_ok then
eprintf "Found prover %s version %s, OK.@." nam ver
eprintf "Found prover %s version %s, OK.@." nam ver
else
begin
prover_tips_info := true;
......@@ -164,11 +164,11 @@ let detect_exec main data com =
with Not_found ->
begin
prover_tips_info := true;
eprintf "Warning: found prover %s but name/version not \
eprintf "Warning: found prover %s but name/version not \
recognized by regexp `%s'@."
data.prover_name data.version_regexp;
eprintf "Answer was `%s'@." s;
None
eprintf "Answer was `%s'@." s;
None
end
let detect_prover main acc l =
......
src/driver/autodetection.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/call_provers.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/call_provers.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/driver.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/driver.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/driver_ast.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/driver_lexer.mll
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......@@ -34,19 +34,19 @@
List.iter
(fun (x,y) -> Hashtbl.add keywords x y)
[ "theory", THEORY;
"end", END;
"syntax", SYNTAX;
"remove", REMOVE;
"meta", META;
"cloned", CLONED;
"prelude", PRELUDE;
"printer", PRINTER;
"valid", VALID;
"invalid", INVALID;
"end", END;
"syntax", SYNTAX;
"remove", REMOVE;
"meta", META;
"cloned", CLONED;
"prelude", PRELUDE;
"printer", PRINTER;
"valid", VALID;
"invalid", INVALID;
"timeout", TIMEOUT;
"time", TIME;
"unknown", UNKNOWN;
"fail", FAIL;
"unknown", UNKNOWN;
"fail", FAIL;
"logic", LOGIC;
"type", TYPE;
"prop", PROP;
......
src/driver/driver_parser.mly
View file @ c5e93f64
/**************************************************************************/
/* */
/* Copyright (C) 2010- */
/* Copyright (C) 2010-2011 */
/* François Bobot */
/* Jean-Christophe Filliâtre */
/* Claude Marché */
......
src/driver/whyconf.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/driver/whyconf.mli
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......
src/ide/db.ml
View file @ c5e93f64
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Copyright (C) 2010-2011 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
......@@ -296,7 +296,7 @@ module ProverId = struct
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
{ prover_id = new_id ;
prover_name = name }
prover_name = name }
)
let from_name db name =
......@@ -308,7 +308,7 @@ module ProverId = struct
(* convert statement into record *)
let of_stmt stmt =
{ prover_id = stmt_column_INT stmt 0 "ProverId.get: bad prover id";
prover_name = name;
prover_name = name;
}
in
(* execute the SQL query *)
......@@ -326,7 +326,7 @@ module ProverId = struct
(* convert statement into record *)
let of_stmt stmt =
{ prover_id = id ;
prover_name = stmt_column_string stmt 0
prover_name = stmt_column_string stmt 0
"ProverId.from_id: bad prover_name";
}
in
......@@ -406,7 +406,7 @@ module TransfId = struct
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
{ transformation_id = new_id ;
transformation_name = name }
transformation_name = name }
)
let from_name db name =
......@@ -418,7 +418,7 @@ module TransfId = struct
(* convert statement into record *)
let of_stmt stmt =
{ transformation_id = stmt_column_INT stmt 0 "TransfId.from_name: bad transformation id";
transformation_name = name;
transformation_name = name;
}
in
(* execute the SQL query *)
......@@ -436,7 +436,7 @@ module TransfId = struct
(* convert statement into record *)
let of_stmt stmt =
{ transformation_id = id ;
transformation_name = stmt_column_string stmt 0
transformation_name = stmt_column_string stmt 0
"TransfId.from_id: bad transformation name";
}
in
......@@ -516,8 +516,8 @@ module External_proof = struct
let add db (g : goal) (p: prover_id) =
transaction db
(fun () ->
let sql = "INSERT INTO external_proofs VALUES(NULL,?,?,0,0,0.0,\"\")" in
let stmt = bind db sql [
let sql = "INSERT INTO external_proofs VALUES(NULL,?,?,0,0,0.0,\"\")" in
let stmt = bind db sql [
Sqlite3.Data.INT g;
Sqlite3.Data.INT p.prover_id;
(*
......@@ -534,47 +534,47 @@ module External_proof = struct
*)
]
in
db_must_done db (fun () -> Sqlite3.step stmt);
Sqlite3.last_insert_rowid db.raw_db)
db_must_done db (fun () -> Sqlite3.step stmt);
Sqlite3.last_insert_rowid db.raw_db)
let set_status db e stat time =
transaction db
(fun () ->
let sql =
"UPDATE external_proofs SET status=?,obsolete=0,time=? WHERE external_proof_id=?"
in
let stmt = bind db sql [
let sql =