Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
125
Issues
125
List
Boards
Labels
Service Desk
Milestones
Merge Requests
15
Merge Requests
15
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
e9a5d7d4
Commit
e9a5d7d4
authored
Sep 06, 2010
by
Francois Bobot
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
docapi : whyconf rc
parent
03adebf0
Changes
11
Hide whitespace changes
Inline
Side-by-side
Showing
11 changed files
with
144 additions
and
55 deletions
+144
-55
src/core/env.mli
src/core/env.mli
+1
-1
src/driver/whyconf.mli
src/driver/whyconf.mli
+37
-6
src/printer/alt_ergo.ml
src/printer/alt_ergo.ml
+2
-0
src/printer/coq.ml
src/printer/coq.ml
+2
-0
src/printer/gappa.ml
src/printer/gappa.ml
+2
-0
src/printer/simplify.ml
src/printer/simplify.ml
+2
-0
src/printer/smt.ml
src/printer/smt.ml
+2
-0
src/printer/why3.ml
src/printer/why3.ml
+2
-0
src/transform/encoding_explicit.ml
src/transform/encoding_explicit.ml
+1
-1
src/util/rc.mli
src/util/rc.mli
+93
-44
src/util/rc.mll
src/util/rc.mll
+0
-3
No files found.
src/core/env.mli
View file @
e9a5d7d4
...
...
@@ -33,7 +33,7 @@ exception TheoryNotFound of string list * string
val
find_theory
:
env
->
string
list
->
string
->
theory
(** [find_theory e p n] finds the theory named [p.n] in environment [e]
@raise
s [TheoryNotFound p n]
if theory not present in env [e] *)
@raise
TheoryNotFound
if theory not present in env [e] *)
(** Parsers *)
...
...
src/driver/whyconf.mli
View file @
e9a5d7d4
...
...
@@ -42,29 +42,60 @@ type main = {
}
type
config
(** A configuration linked to an rc file. Whyconf gives access to
every sections of the rc file ({!Whyconf.get_section},
{!Whyconf.set_section}, {!Whyconf.get_family},
{!Whyconf.set_family}) but the section main and the family prover
which are dealt by it ({!Whyconf.get_main}, {!Whyconf.set_main},
{!Whyconf.get_provers}, {!Whyconf.set_provers} *)
(** - If conf_file is given and the file doesn't exists Not_found is
val
read_config
:
string
option
->
config
(** [read_config conf_file] :
- If conf_file is given and the file doesn't exists Not_found is
raised.
- If "$WHY_CONFIG" is given and the file doesn't exists Not_found is raised
- otherwise tries the following:
- otherwise tries the following
, Not_found is never raised
:
"./why.conf"; "./.why.conf"; "$HOME/.why.conf";
"$USERPROFILE/.why.conf"; the built-in default_config *)
val
read_config
:
string
option
->
config
"$USERPROFILE/.why.conf"; the built-in default_config with default
configuration filename*)
val
save_config
:
config
->
unit
(** [save_config config] save the configuration *)
val
default_config
:
string
->
config
(** [ default_config filename ] create a default configuration which is going
to be saved in [ filename ]*)
val
get_main
:
config
->
main
(** [get_main config] get the main section stored in the Rc file *)
val
get_provers
:
config
->
config_prover
Mstr
.
t
(** [get_main config] get the prover family stored in the Rc file. The
keys are the unique ids of the prover (argument of the family) *)
val
set_main
:
config
->
main
->
config
(** [set_main config main] replace the main section by the given one *)
val
set_provers
:
config
->
config_prover
Mstr
.
t
->
config
(** [set_provers config provers] replace all the family prover by the
one given *)
val
set_conf_file
:
config
->
string
->
config
val
get_conf_file
:
config
->
string
(** [get_conf_file config] get the rc file corresponding to this
configuration *)
(* val set_conf_file : config -> string -> config *)
(* (\** [set_conf_file config] set the rc file corresponding to this *)
(* configuration *\) *)
(** Access to the Rc.t *)
val
get_section
:
config
->
string
->
Rc
.
section
option
(** [get_section config name] Same as {!Rc.get_section} except name
must not be "main" *)
val
get_family
:
config
->
string
->
Rc
.
family
(** [get_family config name] Same as {!Rc.get_family} except name
must not be prover *)
val
set_section
:
config
->
string
->
Rc
.
section
->
config
(** [set_section config name] Same as {!Rc.set_section} except name
must not be "main" *)
val
set_family
:
config
->
string
->
Rc
.
family
->
config
(** [set_family config name] Same as {!Rc.set_family} except name
must not be prover *)
src/printer/alt_ergo.ml
View file @
e9a5d7d4
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Alt-ergo printer *)
open
Format
open
Pp
open
Ident
...
...
src/printer/coq.ml
View file @
e9a5d7d4
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Coq printer *)
open
Format
open
Pp
open
Util
...
...
src/printer/gappa.ml
View file @
e9a5d7d4
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Gappa printer *)
(*
open Register
open Format
...
...
src/printer/simplify.ml
View file @
e9a5d7d4
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Simplify printer *)
open
Format
open
Pp
open
Ident
...
...
src/printer/smt.ml
View file @
e9a5d7d4
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** SMT v1 printer with some extensions *)
open
Format
open
Pp
open
Ident
...
...
src/printer/why3.ml
View file @
e9a5d7d4
...
...
@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
(** Why3 printer *)
open
Format
open
Pp
open
Util
...
...
src/transform/encoding_explicit.ml
View file @
e9a5d7d4
...
...
@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
(**
s
transformation from polymorphic logic to untyped logic. The polymorphic
(** transformation from polymorphic logic to untyped logic. The polymorphic
logic must not have finite support types. *)
...
...
src/util/rc.mli
View file @
e9a5d7d4
...
...
@@ -17,8 +17,9 @@
(* *)
(**************************************************************************)
(** Rc file management *)
(*
Exception
*)
(*
* {2 Exception}
*)
type
rc_value
=
|
RCint
of
int
...
...
@@ -29,84 +30,125 @@ type rc_value =
(* exception SyntaxError *)
exception
ExtraParameters
of
string
(** [ExtraParameters name] One section of name [name] has two many
parameters : more than one if [name] is a family, more than none
if [name] is a section *)
exception
MissingParameters
of
string
(** [MissingParameters name] One section of a family [name] has no
parameters *)
(* exception UnknownSection of string *)
exception
UnknownField
of
string
(** [UnknownField key] The key [key] appeared in a section but is not
expected there *)
(* exception MissingSection of string *)
exception
MissingField
of
string
(** [MissingField key] The field [key] is required but not given *)
exception
DuplicateSection
of
string
(** [DuplicateSection name] section [name] appears more than once *)
exception
DuplicateField
of
string
*
rc_value
*
rc_value
(** [DuplicateField key] key [key] appears more than once *)
exception
StringExpected
of
string
*
rc_value
exception
IdentExpected
of
string
*
rc_value
(** [StringExpected key value] string expected *)
(* exception IdentExpected of string * rc_value *)
(* (\** [IdentExpected key value] string expected *\) *)
exception
IntExpected
of
string
*
rc_value
(** [IntExpected key value] int expected *)
exception
BoolExpected
of
string
*
rc_value
exception
DuplicateProver
of
string
(** [BoolExpected key value] bool expected *)
(** {2 RC API} *)
(* RC API *)
type
t
type
section
type
family
=
(
string
*
section
)
list
val
empty
:
t
val
empty_section
:
section
type
t
(** Rc parsed file *)
type
section
(** section in rc file *)
type
family
=
(
string
*
section
)
list
(** A family in rc files *)
val
empty
:
t
(** An empty Rc *)
val
empty_section
:
section
(** An empty section *)
val
get_section
:
t
->
string
->
section
option
(** return None if the section is not in the rc file *)
(** [get_section rc name]
@return None if the section is not in the rc file
@raise DuplicateSection if multiple section has the name [name]
@raise ExtraParameters if [name] is a family in [rc] instead of a section
*)
val
get_family
:
t
->
string
->
family
(** [get_family rc name] return all the sections of the family [name]
in [rc]
@raise MissingParameters if [name] correspond also too a section in [rc]
*)
val
set_section
:
t
->
string
->
section
->
t
(** [set_section rc name section] add a section [section] with name [name] in
[rc]. Remove former section [name] if present in [rc] *)
val
set_family
:
t
->
string
->
family
->
t
(** [set_family rc name family] add all the section in [family] using
the associated [string] as argument of the family [name] in the rc
file [rc]. Remove all the former sections of family [name] if
present in [rc] *)
val
get_int
:
?
default
:
int
->
section
->
string
->
int
(** raise Bad_value_type
raise Key_not_found
raise Multiple_value
*)
(** [get_int ~default section key] one key to one value
@raise Bad_value_type if the value associated to [key] is not of type
{!int}
@raise Key_not_found if default is not given and no value is
associated to [key]
@raise Multiple_value if the key appears multiple time.
*)
val
get_intl
:
?
default
:
int
list
->
section
->
string
->
int
list
(** raise Bad_value_type
raise Key_not_found *)
(** [get_intl ~default section key] one key to many value
@raise Bad_value_type if the value associated to [key] is not of
type {!int}
@raise Key_not_found if default is not given and no values are
associated to [key]
*)
val
set_int
:
section
->
string
->
int
->
section
(** raise Yet_defined_key *)
(** [set_int section key value] add the association [key] to [value]
in the section. Remove all former associations with this [key]
*)
val
set_intl
:
section
->
string
->
int
list
->
section
(** raise Yet_defined_key *)
(** [set_int section key lvalue] add the associations [key] to all the
[lvalue] in the section. Remove all former associations with this
[key]
*)
val
get_bool
:
?
default
:
bool
->
section
->
string
->
bool
(** raise Bad_value_type
raise Key_not_found
raise Multiple_value
*)
(** Same as {!get_int} but on bool *)
val
get_booll
:
?
default
:
bool
list
->
section
->
string
->
bool
list
(** raise Bad_value_type
raise Key_not_found *)
(** Same as {!get_intl} but on bool *)
val
set_bool
:
section
->
string
->
bool
->
section
(** raise Yet_defined_key
*)
(** Same as {!set_int} but on bool
*)
val
set_booll
:
section
->
string
->
bool
list
->
section
(** raise Yet_defined_key
*)
(** Same as {!set_intl} but on bool
*)
val
get_string
:
?
default
:
string
->
section
->
string
->
string
(** raise Bad_value_type
raise Key_not_found
raise Multiple_value
*)
val
get_string
:
?
default
:
string
->
section
->
string
->
string
(** Same as {!get_int} but on string *)
val
get_stringl
:
?
default
:
string
list
->
section
->
string
->
string
list
(** raise Bad_value_type
raise Key_not_found *)
val
get_stringl
:
?
default
:
string
list
->
section
->
string
->
string
list
(** Same as {!get_intl} but on string *)
val
set_string
:
section
->
string
->
string
->
section
(** raise Yet_defined_key
*)
(** Same as {!set_int} but on string
*)
val
set_stringl
:
section
->
string
->
string
list
->
section
(** raise Yet_defined_key *)
(** Same as {!set_intl} but on string *)
(* val ident : ?default:string -> section -> string -> string *)
(* (\** raise Bad_value_type *)
...
...
@@ -129,17 +171,24 @@ val set_stringl : section -> string -> string list -> section
(* *\) *)
val
check_exhaustive
:
section
->
Util
.
Sstr
.
t
->
unit
(** raise Not_exhaustive of string *)
(** [check_exhaustive section keys] check that only the keys in [keys]
appear inside the section [section]
@raise UnknownField if it is not the case
*)
val
from_file
:
string
->
t
(** returns the records of the file [f]
@raise Not_found is f does not exists
@raise Failure "lexing" in case of incorrect syntax *)
(** [from_file filename] returns the Rc of the file [filename]
@raise Not_found is [filename] does not exists
@raise Failure "lexing" in case of incorrect syntax
@raise ExtraParameters if a section header has more than one argument
*)
val
to_file
:
string
->
t
->
unit
(** [to_file f
t] save the records [t] in the file [f
] *)
(** [to_file f
ilename rc] save the Rc [rc] in the file [filename
] *)
val
get_home_dir
:
unit
->
string
(** returns the home dir of the user *)
(**
[get_home_dir ()]
returns the home dir of the user *)
src/util/rc.mll
View file @
e9a5d7d4
...
...
@@ -55,7 +55,6 @@ exception StringExpected of string * rc_value
exception
IdentExpected
of
string
*
rc_value
exception
IntExpected
of
string
*
rc_value
exception
BoolExpected
of
string
*
rc_value
exception
DuplicateProver
of
string
let
error
?
loc
e
=
match
loc
with
|
None
->
raise
e
...
...
@@ -99,8 +98,6 @@ let () = Exn_printer.register (fun fmt e -> match e with
|
IntExpected
(
s
,
v
)
->
fprintf
fmt
"cannot set field '%s' to %a: an integer is expected"
s
print_rc_value
v
|
DuplicateProver
s
->
fprintf
fmt
"prover %s is already listed"
s
|
e
->
raise
e
)
type
section
=
rc_value
list
Mstr
.
t
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment