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
121
Issues
121
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
b48938dc
Commit
b48938dc
authored
Jun 10, 2016
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'bugfix/v0.87'
parents
bf3e01d6
669cb9f0
Changes
19
Hide whitespace changes
Inline
Side-by-side
Showing
19 changed files
with
66 additions
and
68 deletions
+66
-68
share/emacs/why3.el
share/emacs/why3.el
+1
-1
src/core/ident.mli
src/core/ident.mli
+11
-11
src/core/printer.mli
src/core/printer.mli
+4
-4
src/core/task.mli
src/core/task.mli
+13
-13
src/core/term.mli
src/core/term.mli
+1
-1
src/driver/driver.mli
src/driver/driver.mli
+2
-2
src/printer/cvc3.ml
src/printer/cvc3.ml
+1
-1
src/printer/smtv1.ml
src/printer/smtv1.ml
+1
-1
src/printer/smtv2.ml
src/printer/smtv2.ml
+1
-1
src/printer/yices.ml
src/printer/yices.ml
+1
-1
src/session/session.ml
src/session/session.ml
+8
-9
src/session/session.mli
src/session/session.mli
+3
-3
src/transform/prepare_for_counterexmp.ml
src/transform/prepare_for_counterexmp.ml
+1
-1
src/transform/prepare_for_counterexmp.mli
src/transform/prepare_for_counterexmp.mli
+1
-1
src/util/lists.mli
src/util/lists.mli
+1
-1
src/util/opt.mli
src/util/opt.mli
+1
-2
src/util/rc.mli
src/util/rc.mli
+2
-2
src/util/util.mli
src/util/util.mli
+12
-12
src/util/weakhtbl.mli
src/util/weakhtbl.mli
+1
-1
No files found.
share/emacs/why3.el
View file @
b48938dc
...
...
@@ -21,7 +21,7 @@
;; font-lock
(
defun
why3-regexp-opt
(
l
)
(
concat
"\\<"
(
concat
(
regexp-opt
l
t
)
"\\>"
)
))
(
regexp-opt
l
'words
))
(
defconst
why3-font-lock-keywords-1
(
list
...
...
src/core/ident.mli
View file @
b48938dc
...
...
@@ -63,10 +63,10 @@ val get_model_trace_label : labels : Slab.t -> Slab.elt
(** {2 Identifiers} *)
type
ident
=
private
{
id_string
:
string
;
(* non-unique name *)
id_label
:
Slab
.
t
;
(* identifier labels *)
id_loc
:
Loc
.
position
option
;
(* optional location *)
id_tag
:
Weakhtbl
.
tag
;
(* unique magical tag *)
id_string
:
string
;
(*
*
non-unique name *)
id_label
:
Slab
.
t
;
(*
*
identifier labels *)
id_loc
:
Loc
.
position
option
;
(*
*
optional location *)
id_tag
:
Weakhtbl
.
tag
;
(*
*
unique magical tag *)
}
module
Mid
:
Extmap
.
S
with
type
key
=
ident
...
...
@@ -78,29 +78,29 @@ val id_compare : ident -> ident -> int
val
id_equal
:
ident
->
ident
->
bool
val
id_hash
:
ident
->
int
(* a user-created type of unregistered identifiers *)
(*
*
a user-created type of unregistered identifiers *)
type
preid
=
{
pre_name
:
string
;
pre_label
:
Slab
.
t
;
pre_loc
:
Loc
.
position
option
;
}
(* register a pre-ident (you should never use this function) *)
(*
*
register a pre-ident (you should never use this function) *)
val
id_register
:
preid
->
ident
(* create a fresh pre-ident *)
(*
*
create a fresh pre-ident *)
val
id_fresh
:
?
label
:
Slab
.
t
->
?
loc
:
Loc
.
position
->
string
->
preid
(* create a localized pre-ident *)
(*
*
create a localized pre-ident *)
val
id_user
:
?
label
:
Slab
.
t
->
string
->
Loc
.
position
->
preid
(* create a duplicate pre-ident with given labels *)
(*
*
create a duplicate pre-ident with given labels *)
val
id_lab
:
Slab
.
t
->
ident
->
preid
(* create a duplicate pre-ident *)
(*
*
create a duplicate pre-ident *)
val
id_clone
:
?
label
:
Slab
.
t
->
ident
->
preid
(* create a derived pre-ident (inherit labels and location) *)
(*
*
create a derived pre-ident (inherit labels and location) *)
val
id_derive
:
?
label
:
Slab
.
t
->
string
->
ident
->
preid
(* DEPRECATED : retrieve preid name without registering *)
...
...
src/core/printer.mli
View file @
b48938dc
...
...
@@ -53,7 +53,7 @@ val lookup_printer : string -> printer
val
list_printers
:
unit
->
(
string
*
Pp
.
formatted
)
list
(** {2
u
se printers} *)
(** {2
U
se printers} *)
val
print_prelude
:
prelude
pp
val
print_th_prelude
:
task
->
prelude_map
pp
...
...
@@ -100,7 +100,7 @@ val syntax_arguments_typed :
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** {2
p
retty-printing transformations (useful for caching)} *)
(** {2
P
retty-printing transformations (useful for caching)} *)
val
on_syntax_map
:
(
syntax_map
->
'
a
Trans
.
trans
)
->
'
a
Trans
.
trans
...
...
@@ -114,7 +114,7 @@ val sprint_decl :
(
'
a
->
Format
.
formatter
->
Decl
.
decl
->
'
a
*
string
list
)
->
Theory
.
tdecl
->
'
a
*
string
list
->
'
a
*
string
list
(** {2
e
xceptions to use in transformations and printers} *)
(** {2
E
xceptions to use in transformations and printers} *)
exception
UnsupportedType
of
ty
*
string
exception
UnsupportedTerm
of
term
*
string
...
...
@@ -127,7 +127,7 @@ val unsupportedPattern : pattern -> string -> 'a
val
unsupportedDecl
:
decl
->
string
->
'
a
val
notImplemented
:
string
->
'
a
(** {3
f
unctions that catch inner error} *)
(** {3
F
unctions that catch inner error} *)
exception
Unsupported
of
string
(** This exception must be raised only inside a call
...
...
src/core/task.mli
View file @
b48938dc
...
...
@@ -37,12 +37,12 @@ type meta_map = tdecl_set Mmeta.t
type
task
=
task_hd
option
and
task_hd
=
private
{
task_decl
:
tdecl
;
(* last declaration *)
task_prev
:
task
;
(* context *)
task_known
:
known_map
;
(* known identifiers *)
task_clone
:
clone_map
;
(* cloning history *)
task_meta
:
meta_map
;
(* meta properties *)
task_tag
:
Weakhtbl
.
tag
;
(* unique magical tag *)
task_decl
:
tdecl
;
(*
*
last declaration *)
task_prev
:
task
;
(*
*
context *)
task_known
:
known_map
;
(*
*
known identifiers *)
task_clone
:
clone_map
;
(*
*
cloning history *)
task_meta
:
meta_map
;
(*
*
meta properties *)
task_tag
:
Weakhtbl
.
tag
;
(*
*
unique magical tag *)
}
val
task_equal
:
task
->
task
->
bool
...
...
@@ -58,7 +58,7 @@ val task_meta : task -> meta_map
val
find_clone_tds
:
task
->
theory
->
tdecl_set
val
find_meta_tds
:
task
->
meta
->
tdecl_set
(** {2
c
onstructors} *)
(** {2
C
onstructors} *)
val
add_decl
:
task
->
decl
->
task
val
add_tdecl
:
task
->
tdecl
->
task
...
...
@@ -67,7 +67,7 @@ val use_export : task -> theory -> task
val
clone_export
:
task
->
theory
->
th_inst
->
task
val
add_meta
:
task
->
meta
->
meta_arg
list
->
task
(** {2
d
eclaration constructors + add_decl} *)
(** {2
D
eclaration constructors + add_decl} *)
val
add_ty_decl
:
task
->
tysymbol
->
task
val
add_data_decl
:
task
->
data_decl
list
->
task
...
...
@@ -76,14 +76,14 @@ val add_logic_decl : task -> logic_decl list -> task
val
add_ind_decl
:
task
->
ind_sign
->
ind_decl
list
->
task
val
add_prop_decl
:
task
->
prop_kind
->
prsymbol
->
term
->
task
(** {2
u
tilities} *)
(** {2
U
tilities} *)
val
split_theory
:
theory
->
Spr
.
t
option
->
task
->
task
list
(** [split_theory th s t] returns the tasks of [th] added to [t]
that end by one of [s]. They are in the opposite order than
in the theory *)
(** {2
r
ealization utilities} *)
(** {2
R
ealization utilities} *)
val
used_theories
:
task
->
theory
Mid
.
t
(** returns a map from theory names to theories themselves *)
...
...
@@ -97,7 +97,7 @@ val local_decls : task -> theory Mid.t -> decl list
the list of declarations that are not imported
with those theories or derived thereof *)
(** {2
b
ottom-up, tail-recursive traversal functions} *)
(** {2
B
ottom-up, tail-recursive traversal functions} *)
val
task_fold
:
(
'
a
->
tdecl
->
'
a
)
->
'
a
->
task
->
'
a
val
task_iter
:
(
tdecl
->
unit
)
->
task
->
unit
...
...
@@ -113,7 +113,7 @@ val task_separate_goal : task -> tdecl * task
goal of the task [t] and [t'] is the rest. raises [GoalNotFound]
if task [t] has no goal *)
(** {2
s
electors} *)
(** {2
S
electors} *)
val
on_meta
:
meta
->
(
'
a
->
meta_arg
list
->
'
a
)
->
'
a
->
task
->
'
a
val
on_theory
:
theory
->
(
'
a
->
symbol_map
->
'
a
)
->
'
a
->
task
->
'
a
...
...
@@ -126,7 +126,7 @@ val on_tagged_ts : meta -> task -> Sts.t
val
on_tagged_ls
:
meta
->
task
->
Sls
.
t
val
on_tagged_pr
:
meta
->
task
->
Spr
.
t
(*
e
xceptions *)
(*
* E
xceptions *)
exception
NotTaggingMeta
of
meta
exception
NotExclusiveMeta
of
meta
...
...
src/core/term.mli
View file @
b48938dc
...
...
@@ -145,7 +145,7 @@ module Mterm : Extmap.S with type key = term
module
Sterm
:
Extset
.
S
with
module
M
=
Mterm
module
Hterm
:
Exthtbl
.
S
with
type
key
=
term
(** {2
t
erm equality modulo alpha-equivalence and location} *)
(** {2
T
erm equality modulo alpha-equivalence and location} *)
val
t_compare
:
term
->
term
->
int
val
t_equal
:
term
->
term
->
bool
...
...
src/driver/driver.mli
View file @
b48938dc
...
...
@@ -11,7 +11,7 @@
(** Managing the drivers for external provers *)
(** {2
c
reate a driver} *)
(** {2
C
reate a driver} *)
type
driver
...
...
@@ -22,7 +22,7 @@ val load_driver : Env.env -> string -> string list -> driver
@param string list additional driver files containing only theories
*)
(** {2
u
se a driver} *)
(** {2
U
se a driver} *)
val
file_of_task
:
driver
->
string
->
string
->
Task
.
task
->
string
(** [file_of_task d f th t] produces a filename
...
...
src/printer/cvc3.ml
View file @
b48938dc
...
...
@@ -23,7 +23,7 @@ let ident_printer =
let
bls
=
(*["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
"if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
"sat";"theory";"true";"unknown";"unsat";"xor";
"assumption";"axioms";"defintion";"extensions";"formula";
"assumption";"axioms";"defin
i
tion";"extensions";"formula";
"funs";"extrafuns";"extrasorts";"extrapreds";"language";
"notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
"Array";"U";"select";"store"]*)
...
...
src/printer/smtv1.ml
View file @
b48938dc
...
...
@@ -23,7 +23,7 @@ let ident_printer =
let
bls
=
[
"and"
;
"benchmark"
;
"distinct"
;
"exists"
;
"false"
;
"flet"
;
"forall"
;
"if then else"
;
"iff"
;
"implies"
;
"ite"
;
"let"
;
"logic"
;
"not"
;
"or"
;
"sat"
;
"theory"
;
"true"
;
"unknown"
;
"unsat"
;
"xor"
;
"assumption"
;
"axioms"
;
"defintion"
;
"extensions"
;
"formula"
;
"assumption"
;
"axioms"
;
"defin
i
tion"
;
"extensions"
;
"formula"
;
"funs"
;
"extrafuns"
;
"extrasorts"
;
"extrapreds"
;
"language"
;
"notes"
;
"preds"
;
"sorts"
;
"status"
;
"theory"
;
"Int"
;
"Real"
;
"Bool"
;
"Array"
;
"U"
;
"select"
;
"store"
]
in
...
...
src/printer/smtv2.ml
View file @
b48938dc
...
...
@@ -28,7 +28,7 @@ let ident_printer () =
let
bls
=
(*["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
"if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
"sat";"theory";"true";"unknown";"unsat";"xor";
"assumption";"axioms";"defintion";"extensions";"formula";
"assumption";"axioms";"defin
i
tion";"extensions";"formula";
"funs";"extrafuns";"extrasorts";"extrapreds";"language";
"notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
"Array";"U";"select";"store"]*)
...
...
src/printer/yices.ml
View file @
b48938dc
...
...
@@ -23,7 +23,7 @@ let ident_printer =
let
bls
=
(*["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
"if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
"sat";"theory";"true";"unknown";"unsat";"xor";
"assumption";"axioms";"defintion";"extensions";"formula";
"assumption";"axioms";"defin
i
tion";"extensions";"formula";
"funs";"extrafuns";"extrasorts";"extrapreds";"language";
"notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
"Array";"U";"select";"store"]*)
...
...
src/session/session.ml
View file @
b48938dc
...
...
@@ -2366,9 +2366,13 @@ exception OutdatedSession
let
merge_theory
~
ctxt
~
theories
env
from_th
to_th
=
found_missed_goals_in_theory
:=
false
;
set_theory_expanded
to_th
from_th
.
theory_expanded
;
let
get_goal_name
g
=
try
let
(
_
,_,
l
)
=
restore_path
g
.
goal_name
in
String
.
concat
"."
l
with
Not_found
->
g
.
goal_name
.
Ident
.
id_string
in
let
from_goals
=
List
.
fold_left
(
fun
from_goals
g
->
Mstr
.
add
g
.
goal_name
.
Ident
.
id_string
g
from_goals
)
(
fun
from_goals
g
->
Mstr
.
add
(
get_goal_name
g
)
g
from_goals
)
Mstr
.
empty
from_th
.
theory_goals
in
Debug
.
dprintf
debug
...
...
@@ -2379,16 +2383,11 @@ let merge_theory ~ctxt ~theories env from_th to_th =
List
.
iter
(
fun
to_goal
->
try
let
to_goal_name
=
try
let
(
_
,_,
l
)
=
restore_path
to_goal
.
goal_name
in
String
.
concat
"."
l
with
Not_found
->
to_goal
.
goal_name
.
Ident
.
id_string
in
let
to_goal_name
=
get_goal_name
to_goal
in
let
from_goal
=
Mstr
.
find
to_goal_name
from_goals
in
Debug
.
dprintf
debug
"[Goal checksum] goal %s: old sum = %a, new sum = %a@."
to_goal
.
goal_name
.
Ident
.
id_string
to_goal
_name
(
Pp
.
print_option
Tc
.
print_checksum
)
from_goal
.
goal_checksum
(
Pp
.
print_option
Tc
.
print_checksum
)
to_goal
.
goal_checksum
;
let
goal_obsolete
=
...
...
src/session/session.mli
View file @
b48938dc
...
...
@@ -77,7 +77,7 @@ type idpos = {
type
'
a
goal
=
private
{
mutable
goal_key
:
'
a
;
goal_name
:
Ident
.
ident
;
(**
The
ident of the task *)
goal_name
:
Ident
.
ident
;
(** ident of the task *)
goal_expl
:
expl
;
goal_parent
:
'
a
goal_parent
;
mutable
goal_checksum
:
Termcode
.
checksum
option
;
(** checksum of the task *)
...
...
@@ -486,7 +486,7 @@ val goal_task_or_recover: 'a env_session -> 'a goal -> Task.task
(** {2 Iterators} *)
(** {3
r
ecursive} *)
(** {3
R
ecursive} *)
val
goal_iter_proof_attempt
:
(
'
key
proof_attempt
->
unit
)
->
'
key
goal
->
unit
(* unused
...
...
@@ -511,7 +511,7 @@ val goal_iter_leaf_goal :
val
fold_all_sub_goals_of_theory
:
(
'
a
->
'
key
goal
->
'
a
)
->
'
a
->
'
key
theory
->
'
a
(** {3
n
ot recursive} *)
(** {3
N
ot recursive} *)
val
iter_goal
:
(
'
key
proof_attempt
->
unit
)
->
...
...
src/transform/prepare_for_counterexmp.ml
View file @
b48938dc
...
...
@@ -44,7 +44,7 @@ let prepare_for_counterexmp2 env task =
let
prepare_for_counterexmp
env
=
Trans
.
store
(
prepare_for_counterexmp2
env
)
let
()
=
Trans
.
register_env_transform
"prepare_for_counterexmp"
prepare_for_counterexmp
~
desc
:
"Transformation@ that@ prepares@ the@ task@ for@ quering@ for@ \
~
desc
:
"Transformation@ that@ prepares@ the@ task@ for@ quer
y
ing@ for@ \
the@ counter-example@ model.@ This@ transformation@ does@ so@ only@ \
when@ the@ solver@ will@ be@ asked@ for@ the@ counter-example."
...
...
src/transform/prepare_for_counterexmp.mli
View file @
b48938dc
...
...
@@ -16,7 +16,7 @@ val get_counterexmp : Task.task -> bool
val
prepare_for_counterexmp
:
Env
.
env
->
Task
.
task
Trans
.
trans
(**
Transformation that prepares the task for quering for
Transformation that prepares the task for quer
y
ing for
the counter-example model.
This transformation does so only when the solver will be asked
for the counter-example.
...
...
src/util/lists.mli
View file @
b48938dc
...
...
@@ -37,7 +37,7 @@ val fold_product : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
tail-recursive *)
val
fold_product_l
:
(
'
a
->
'
b
list
->
'
a
)
->
'
a
->
'
b
list
list
->
'
a
(** generalisation of {! Lists.fold_product} not tail-recursive *)
(** generalisation of {! Lists.fold_product}
;
not tail-recursive *)
val
flatten_rev
:
'
a
list
list
->
'
a
list
...
...
src/util/opt.mli
View file @
b48938dc
...
...
@@ -39,5 +39,4 @@ val equal : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool
val
compare
:
(
'
a
->
'
b
->
int
)
->
'
a
option
->
'
b
option
->
int
val
map_fold
:
(
'
a
->
'
b
->
'
a
*
'
b
)
->
'
a
->
'
b
option
->
'
a
*
'
b
option
val
map_fold
:
(
'
a
->
'
b
->
'
a
*
'
b
)
->
'
a
->
'
b
option
->
'
a
*
'
b
option
src/util/rc.mli
View file @
b48938dc
...
...
@@ -55,7 +55,7 @@ exception BoolExpected of string * rc_value
type
t
(** Rc parsed file *)
type
section
(**
s
ection in rc file *)
type
section
(**
S
ection in rc file *)
type
family
=
(
string
*
section
)
list
(** A family in rc files *)
type
simple_family
=
section
list
(** A family w/o arguments in rc files*)
...
...
@@ -199,7 +199,7 @@ val from_channel : in_channel -> t
val
from_file
:
string
->
t
(** [from_file filename] returns the Rc of the file [filename]
@raise CannotOpen i
s
[filename] does not exist
@raise CannotOpen i
f
[filename] does not exist
@raise SyntaxErrorFile in case of incorrect syntax
@raise ExtraParameters if a section header has more than one argument
*)
...
...
src/util/util.mli
View file @
b48938dc
...
...
@@ -26,28 +26,28 @@ val mapi : (int -> 'a) -> int -> int -> 'a list
val
iterf
:
(
float
->
unit
)
->
float
->
float
->
float
->
unit
(** [iterf f min max step] *)
(* Convert fold-like functions into [for_all] and [exists] functions.
Predicates passed to [all], [all2], and [alld] may raise FoldSkip to
signalize [false]. Predicates passed to [any], [any2], and [anyd] may
raise FoldSkip to signalize [true]. *)
(*
*
Convert fold-like functions into [for_all] and [exists] functions.
Predicates passed to [all], [all2], and [alld] may raise FoldSkip to
signalize [false]. Predicates passed to [any], [any2], and [anyd] may
raise FoldSkip to signalize [true]. *)
exception
FoldSkip
val
all_fn
:
(
'
a
->
bool
)
->
'
z
->
'
a
->
bool
(* [all_fn pr z a] return true if [pr a] is true,
otherwise raises
FoldSkip *)
(*
*
[all_fn pr z a] return true if [pr a] is true,
otherwise raise
FoldSkip *)
val
any_fn
:
(
'
a
->
bool
)
->
'
z
->
'
a
->
bool
(*
[all
_fn pr z a] return false if [pr a] is false,
otherwise raises
FoldSkip *)
(*
* [any
_fn pr z a] return false if [pr a] is false,
otherwise raise
FoldSkip *)
val
all2_fn
:
(
'
a
->
'
b
->
bool
)
->
'
z
->
'
a
->
'
b
->
bool
(*
[all
_fn pr z a b] return true if [pr a b] is true,
otherwise raises
FoldSkip *)
(*
* [all2
_fn pr z a b] return true if [pr a b] is true,
otherwise raise
FoldSkip *)
val
any2_fn
:
(
'
a
->
'
b
->
bool
)
->
'
z
->
'
a
->
'
b
->
bool
(*
[all
_fn pr z a b] return false if [pr a b] is false,
otherwise raises
FoldSkip *)
(*
* [any2
_fn pr z a b] return false if [pr a b] is false,
otherwise raise
FoldSkip *)
type
(
'
z
,
'
a
,
'
c
)
fold
=
(
'
z
->
'
a
->
'
z
)
->
'
z
->
'
c
->
'
z
...
...
src/util/weakhtbl.mli
View file @
b48938dc
...
...
@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
(** Hashtable with weak key used for memoization *)
(** Hashtable
s
with weak key used for memoization *)
type
tag
...
...
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