From 0d0a403db7c336aae587a7675748dfa6bb6e1696 Mon Sep 17 00:00:00 2001 From: Francois Bobot Date: Mon, 26 Apr 2010 12:36:33 +0000 Subject: [PATCH] Un peu de documentation --- src/driver/call_provers.mli | 31 ++++++++++++++++++++----- src/driver/driver.mli | 2 +- src/driver/prover.mli | 2 ++ src/driver/register.mli | 15 +++++++------ src/driver/whyconf.mli | 2 ++ src/transform/encoding_decorate.mli | 4 ++++ src/transform/split_conjunction.mli | 35 +++++++++++++++++++++++++++++ src/util/hashcons.mli | 2 ++ src/util/hashweak.mli | 2 ++ src/util/rc.mli | 5 +++-- src/util/util.mli | 2 ++ 11 files changed, 86 insertions(+), 16 deletions(-) create mode 100644 src/transform/split_conjunction.mli diff --git a/src/driver/call_provers.mli b/src/driver/call_provers.mli index 1702139bd..6962b8e09 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 0cfa01c7d..3df4a5775 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 1811aac11..d048a4bc4 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 bc2a4a43e..8fa0bb90a 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 998983835..e050e863e 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 81fccfe9c..e6eb80d89 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 000000000..4083feab4 --- /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 009088c9b..565d2e461 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 87cd72833..b0ff1a050 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 6924f501f..ca66c4daa 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 40c67ec91..93dfb3c85 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 -- GitLab