diff --git a/src/driver/call_provers.mli b/src/driver/call_provers.mli index 1702139bd40db33899ad9d739503e9d947a592d3..6962b8e0972aa212dab7029550ea4a7cc110bdb8 100644 --- a/src/driver/call_provers.mli +++ b/src/driver/call_provers.mli @@ -17,22 +17,39 @@ (* *) (**************************************************************************) +(** Call provers and parse there outputs *) + type prover_answer = - | Valid - | Invalid - | Timeout - | Unknown of string + | Valid + (** The task is valid according to the prover *) + | Invalid + (** The task is invalid *) + | Timeout + (** the task timeout, ie it takes more time than specified*) + | Unknown of string + (** The prover can't determined the validity or not of the task *) | Failure of string - | HighFailure + (** The prover report a failure *) + | HighFailure + (** An error occured during the call to the prover or none of + the given regexp match the output of the prover *) type prover_result = { pr_answer : prover_answer; + (* The answer of the prover on the given task*) pr_output : string; + (* The output of the prover currently stderr and stdout *) pr_time : float; + (* The time taken by the prover *) } val print_prover_answer : Format.formatter -> prover_answer -> unit +(** Pretty-print a {! prover_answer} *) + val print_prover_result : Format.formatter -> prover_result -> unit +(** Pretty-print a prover_result. The answer and the time are output. + The output of the prover is printed if and only if the answer is an + [HighFailure] *) val call_on_buffer : ?debug : bool -> @@ -44,4 +61,6 @@ val call_on_buffer : filename : string -> Buffer.t -> unit -> prover_result - +(** Call a prover on the task printed in the {!type: Buffer.t} given. + @param debug : set the debug flag. + Print on stderr the commandline called and the output of the prover. *) diff --git a/src/driver/driver.mli b/src/driver/driver.mli index 0cfa01c7db94b71edd8fb33fa26dbb36220ae655..3df4a5775d108f5e24760ab17639bbc96cd825de 100644 --- a/src/driver/driver.mli +++ b/src/driver/driver.mli @@ -17,7 +17,7 @@ (* *) (**************************************************************************) -(** Drivers for calling external provers *) +(** Manage Why drivers *) open Format open Util diff --git a/src/driver/prover.mli b/src/driver/prover.mli index 1811aac11722ff7e5a6c34b0fc2218f292e6e3b2..d048a4bc4bff1295b4e01ef4d1106e241ef18eaf 100644 --- a/src/driver/prover.mli +++ b/src/driver/prover.mli @@ -17,6 +17,8 @@ (* *) (**************************************************************************) +(** Apply printers and registered transformations mentionned in drivers *) + val print_task : Driver.driver -> Format.formatter -> Task.task -> unit val prove_task : diff --git a/src/driver/register.mli b/src/driver/register.mli index bc2a4a43ec32a1b7cc39bba2a235179e154c4851..8fa0bb90aaaf9465e0bd52c57acc3a896bbda5ac 100644 --- a/src/driver/register.mli +++ b/src/driver/register.mli @@ -119,16 +119,17 @@ val catch_unsupportedtype : (Ty.ty -> 'a) -> (Ty.ty -> 'a) (** [catch_unsupportedtype f] return a function which applied on [arg] : - return [f arg] if [f arg] doesn't raise the {! Unsupported} exception. - - raise [unsupportedType (arg,s)] if [f arg] raises [Unsupported s]*) + - raise [Error (unsupportedType (arg,s))] if [f arg] + raises [Unsupported s]*) val catch_unsupportedterm : (Term.term -> 'a) -> (Term.term -> 'a) -(** same as {! catch_unsupportedtype} but raise {! -UnsupportedExpression} instead of {! UnsupportedType}*) + (** same as {! catch_unsupportedtype} but use [UnsupportedExpression] + instead of [UnsupportedType]*) val catch_unsupportedfmla : (Term.fmla -> 'a) -> (Term.fmla -> 'a) -(** same as {! catch_unsupportedtype} but raise {! -UnsupportedExpression} instead of {! UnsupportedType}*) + (** same as {! catch_unsupportedtype} but use [UnsupportedExpression] + instead of [UnsupportedType]*) val catch_unsupportedDeclaration : (Decl.decl -> 'a) -> (Decl.decl -> 'a) -(** same as {! catch_unsupportedtype} but raise {! -UnsupportedDeclaration} instead of {! UnsupportedType}*) +(** same as {! catch_unsupportedtype} but use + [UnsupportedDeclaration] instead of [UnsupportedType] *) diff --git a/src/driver/whyconf.mli b/src/driver/whyconf.mli index 998983835299d8101d3ce7c1f2178dd49dcf361e..e050e863e57ef5dc1642a71e3bf407a9249e5de5 100644 --- a/src/driver/whyconf.mli +++ b/src/driver/whyconf.mli @@ -17,6 +17,8 @@ (* *) (**************************************************************************) +(** Manage the config file of Why *) + open Util type config_prover = { diff --git a/src/transform/encoding_decorate.mli b/src/transform/encoding_decorate.mli index 81fccfe9c9422316b52813ab27a2d15c31f67db3..e6eb80d898fbfbcc45a2dbeeed202cc0857005d1 100644 --- a/src/transform/encoding_decorate.mli +++ b/src/transform/encoding_decorate.mli @@ -17,3 +17,7 @@ (* *) (**************************************************************************) +(** A transformation between polymorphic logic and multi-sorted logic*) +(** {{:http://www.lri.fr/~lescuyer/pdf/CADE-CL07.ps} + Handling Polymorphism in Automated Deduction}. + Jean-Francois Couchot et Stephane Lescuyer *) diff --git a/src/transform/split_conjunction.mli b/src/transform/split_conjunction.mli new file mode 100644 index 0000000000000000000000000000000000000000..4083feab4e4e886b27695e8b0e6cc9281fda7d65 --- /dev/null +++ b/src/transform/split_conjunction.mli @@ -0,0 +1,35 @@ +(**************************************************************************) +(* *) +(* Copyright (C) 2010- *) +(* Francois Bobot *) +(* Jean-Christophe Filliatre *) +(* Johannes Kanig *) +(* 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. *) +(* *) +(**************************************************************************) + +(** Move the conjunctions to top level and split the axiom or goal *) + + +val split_pos_goal : Task.task Register.tlist_reg +val split_pos_neg_goal : Task.task Register.tlist_reg +val split_pos_axiom : Task.task Register.tlist_reg +val split_pos_neg_axiom : Task.task Register.tlist_reg +val split_pos_all : Task.task Register.tlist_reg +val split_pos_neg_all : Task.task Register.tlist_reg + +(** naming convention : + - pos : move the conjuctions in positive sub-formula to top level + - pos : move the conjuctions in negative sub-formula to top level + - goal : apply the transformation only to goal + - axiom : apply the transformation only to axioms + - all : apply the transformation to goal and axioms *) diff --git a/src/util/hashcons.mli b/src/util/hashcons.mli index 009088c9b52724bc3044801e1c84333abe0dfc12..565d2e46125d5d4ce54325a7016ca3e776497836 100644 --- a/src/util/hashcons.mli +++ b/src/util/hashcons.mli @@ -17,6 +17,8 @@ (* *) (**************************************************************************) +(** Hash tables for hash consing *) + (*s Hash tables for hash consing. Hash consed values are of the diff --git a/src/util/hashweak.mli b/src/util/hashweak.mli index 87cd728335858a3eee291106b5b0196127743d7e..b0ff1a050500e21cfc3d0767eb655a6b2ffccc0e 100644 --- a/src/util/hashweak.mli +++ b/src/util/hashweak.mli @@ -17,6 +17,8 @@ (* *) (**************************************************************************) +(** Hashtable with weak key used for memoization *) + module type S = sig type key diff --git a/src/util/rc.mli b/src/util/rc.mli index 6924f501f8e084f3b28e54a8c96088766741d241..ca66c4daa0207c5c8ba0b2239f1592af7ce3d8e0 100644 --- a/src/util/rc.mli +++ b/src/util/rc.mli @@ -25,6 +25,7 @@ (* *) (**************************************************************************) +(** Parse rc files *) type rc_value = | RCint of int @@ -44,8 +45,8 @@ val string : rc_value -> string val from_file : string -> (string list * (string * rc_value) list) list (** returns the records of the file [f] - @raises Not_found is f does not exists - @raises Failure "lexing" in case of incorrect syntax *) + @raise Not_found is f does not exists + @raise Failure "lexing" in case of incorrect syntax *) val get_home_dir : unit -> string (** returns the home dir of the user *) diff --git a/src/util/util.mli b/src/util/util.mli index 40c67ec914f54115881535ea561cdd3b4778a0f6..93dfb3c8584259d18a5fca8d2fcee8da928d9926 100644 --- a/src/util/util.mli +++ b/src/util/util.mli @@ -17,6 +17,8 @@ (* *) (**************************************************************************) +(** Useful functions *) + (* useful option combinators *) val of_option : 'a option -> 'a