Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
3047a120
Commit
3047a120
authored
May 16, 2011
by
Andrei Paskevich
Browse files
finally rename everything to term, t_, T* etc
parent
fa6d7f41
Changes
65
Expand all
Hide whitespace changes
Inline
Side-by-side
examples/use_api.ml
View file @
3047a120
...
...
@@ -28,9 +28,9 @@ the alt-ergo prover to check them
open
Why
(* a ground propositional goal: true or false *)
let
fmla_true
:
Term
.
fmla
=
Term
.
f
_true
let
fmla_false
:
Term
.
fmla
=
Term
.
f
_false
let
fmla1
:
Term
.
fmla
=
Term
.
f
_or
fmla_true
fmla_false
let
fmla_true
:
Term
.
term
=
Term
.
t
_true
let
fmla_false
:
Term
.
term
=
Term
.
t
_false
let
fmla1
:
Term
.
term
=
Term
.
t
_or
fmla_true
fmla_false
(* printing it *)
open
Format
...
...
@@ -41,9 +41,9 @@ let () = printf "@[formula 1 is:@ %a@]@." Pretty.print_term fmla1
let
prop_var_A
:
Term
.
lsymbol
=
Term
.
create_psymbol
(
Ident
.
id_fresh
"A"
)
[]
let
prop_var_B
:
Term
.
lsymbol
=
Term
.
create_psymbol
(
Ident
.
id_fresh
"B"
)
[]
let
atom_A
:
Term
.
fmla
=
Term
.
ps_app
prop_var_A
[]
let
atom_B
:
Term
.
fmla
=
Term
.
ps_app
prop_var_B
[]
let
fmla2
:
Term
.
fmla
=
Term
.
f
_implies
(
Term
.
f
_and
atom_A
atom_B
)
atom_A
let
atom_A
:
Term
.
term
=
Term
.
ps_app
prop_var_A
[]
let
atom_B
:
Term
.
term
=
Term
.
ps_app
prop_var_B
[]
let
fmla2
:
Term
.
term
=
Term
.
t
_implies
(
Term
.
t
_and
atom_A
atom_B
)
atom_A
let
()
=
printf
"@[formula 2 is:@ %a@]@."
Pretty
.
print_term
fmla2
...
...
@@ -124,7 +124,7 @@ let plus_symbol : Term.lsymbol =
Theory
.
ns_find_ls
int_theory
.
Theory
.
th_export
[
"infix +"
]
let
two_plus_two
:
Term
.
term
=
Term
.
fs_app
plus_symbol
[
two
;
two
]
Ty
.
ty_int
let
two_plus_two
:
Term
.
term
=
Term
.
t_app_infer
plus_symbol
[
two
;
two
]
let
fmla3
:
Term
.
fmla
=
Term
.
f
_equ
two_plus_two
four
let
fmla3
:
Term
.
term
=
Term
.
t
_equ
two_plus_two
four
let
task3
=
None
let
task3
=
Task
.
use_export
task3
int_theory
...
...
@@ -156,12 +156,12 @@ let var_x : Term.vsymbol =
let
x
:
Term
.
term
=
Term
.
t_var
var_x
let
x_times_x
:
Term
.
term
=
Term
.
t_app_infer
mult_symbol
[
x
;
x
]
let
fmla4_aux
:
Term
.
fmla
=
let
fmla4_aux
:
Term
.
term
=
Term
.
ps_app
ge_symbol
[
x_times_x
;
zero
]
let
fmla4_quant
:
Term
.
fmla
_quant
=
Term
.
f
_close_quant
[
var_x
]
[]
fmla4_aux
let
fmla4
:
Term
.
fmla
=
Term
.
f
_forall
fmla4_quant
let
fmla4_quant
:
Term
.
term
_quant
=
Term
.
t
_close_quant
[
var_x
]
[]
fmla4_aux
let
fmla4
:
Term
.
term
=
Term
.
t
_forall
fmla4_quant
let
task4
=
None
let
task4
=
Task
.
use_export
task4
int_theory
...
...
src/coq-plugin/whytac.ml
View file @
3047a120
...
...
@@ -747,7 +747,7 @@ and tr_formula dep tvm bv env f =
let
ty
=
type_of
env
Evd
.
empty
t
in
if
is_Set
ty
||
is_Type
ty
then
let
_
=
tr_type
dep
tvm
env
t
in
Term
.
f
_equ
(
tr_term
dep
tvm
bv
env
a
)
(
tr_term
dep
tvm
bv
env
b
)
Term
.
t
_equ
(
tr_term
dep
tvm
bv
env
a
)
(
tr_term
dep
tvm
bv
env
b
)
else
raise
NotFO
(* comparisons on integers *)
...
...
@@ -778,29 +778,29 @@ and tr_formula dep tvm bv env f =
Term
.
f_app
ls
[
tr_term
dep
tvm
bv
env
a
;
tr_term
dep
tvm
bv
env
b
]
(* propositional logic *)
|
_
,
[]
when
c
=
build_coq_False
()
->
Term
.
f
_false
Term
.
t
_false
|
_
,
[]
when
c
=
build_coq_True
()
->
Term
.
f
_true
Term
.
t
_true
|
_
,
[
a
]
when
c
=
build_coq_not
()
->
Term
.
f
_not
(
tr_formula
dep
tvm
bv
env
a
)
Term
.
t
_not
(
tr_formula
dep
tvm
bv
env
a
)
|
_
,
[
a
;
b
]
when
c
=
build_coq_and
()
->
Term
.
f
_and
(
tr_formula
dep
tvm
bv
env
a
)
(
tr_formula
dep
tvm
bv
env
b
)
Term
.
t
_and
(
tr_formula
dep
tvm
bv
env
a
)
(
tr_formula
dep
tvm
bv
env
b
)
|
_
,
[
a
;
b
]
when
c
=
build_coq_or
()
->
Term
.
f
_or
(
tr_formula
dep
tvm
bv
env
a
)
(
tr_formula
dep
tvm
bv
env
b
)
Term
.
t
_or
(
tr_formula
dep
tvm
bv
env
a
)
(
tr_formula
dep
tvm
bv
env
b
)
|
_
,
[
a
;
b
]
when
c
=
Lazy
.
force
coq_iff
->
Term
.
f
_iff
(
tr_formula
dep
tvm
bv
env
a
)
(
tr_formula
dep
tvm
bv
env
b
)
Term
.
t
_iff
(
tr_formula
dep
tvm
bv
env
a
)
(
tr_formula
dep
tvm
bv
env
b
)
|
Prod
(
n
,
a
,
b
)
,
_
->
if
is_imp_term
f
&&
is_Prop
(
type_of
env
Evd
.
empty
a
)
then
Term
.
f
_implies
Term
.
t
_implies
(
tr_formula
dep
tvm
bv
env
a
)
(
tr_formula
dep
tvm
bv
env
b
)
else
let
vs
,
_t
,
bv
,
env
,
b
=
quantifiers
n
a
b
dep
tvm
bv
env
in
Term
.
f
_forall_close
[
vs
]
[]
(
tr_formula
dep
tvm
bv
env
b
)
Term
.
t
_forall_close
[
vs
]
[]
(
tr_formula
dep
tvm
bv
env
b
)
|
_
,
[
_
;
a
]
when
c
=
build_coq_ex
()
->
begin
match
kind_of_term
a
with
|
Lambda
(
n
,
a
,
b
)
->
let
vs
,
_t
,
bv
,
env
,
b
=
quantifiers
n
a
b
dep
tvm
bv
env
in
Term
.
f
_exists_close
[
vs
]
[]
(
tr_formula
dep
tvm
bv
env
b
)
Term
.
t
_exists_close
[
vs
]
[]
(
tr_formula
dep
tvm
bv
env
b
)
|
_
->
(* unusual case of the shape (ex p) *)
(* TODO: we could eta-expanse *)
...
...
@@ -856,10 +856,10 @@ let tr_goal gl =
let
ty
=
tr_type
dep
tvm
env
ty
in
(* DO NOT INLINE! *)
let
vs
=
Term
.
create_vsymbol
(
preid_of_id
id
)
ty
in
let
bv
=
Idmap
.
add
id
vs
bv
in
Term
.
f
_forall_close
[
vs
]
[]
(
tr_ctxt
tvm
bv
ctxt
)
Term
.
t
_forall_close
[
vs
]
[]
(
tr_ctxt
tvm
bv
ctxt
)
else
if
is_Prop
t
then
let
h
=
tr_formula
dep
tvm
bv
env
ty
in
(* DO NOT INLINE! *)
Term
.
f
_implies
h
(
tr_ctxt
tvm
bv
ctxt
)
Term
.
t
_implies
h
(
tr_ctxt
tvm
bv
ctxt
)
else
raise
NotFO
with
NotFO
->
...
...
src/core/decl.ml
View file @
3047a120
...
...
@@ -33,7 +33,7 @@ type ty_decl = tysymbol * ty_def
(** Logic declaration *)
type
ls_defn
=
lsymbol
*
fmla
type
ls_defn
=
lsymbol
*
term
type
logic_decl
=
lsymbol
*
ls_defn
option
...
...
@@ -49,19 +49,19 @@ let check_tl ty t = ty_equal_check ty (t_type t)
let
make_ls_defn
ls
vl
t
=
let
hd
=
t_app
ls
(
List
.
map
t_var
vl
)
t
.
t_ty
in
let
hd
=
e_fold
f
_equ
f
_iff
hd
t
in
let
fd
=
f
_forall_close
vl
[]
hd
in
let
hd
=
TermTF
.
t_selecti
t
_equ
t
_iff
hd
t
in
let
fd
=
t
_forall_close
vl
[]
hd
in
List
.
iter2
check_vl
ls
.
ls_args
vl
;
t_ty_check
t
ls
.
ls_value
;
ls
,
Some
(
ls
,
check_fvs
fd
)
let
open_ls_defn
(
_
,
f
)
=
let
vl
,_,
f
=
match
f
.
t_node
with
|
F
quant
(
F
forall
,
b
)
->
f
_open_quant
b
|
T
quant
(
T
forall
,
b
)
->
t
_open_quant
b
|
_
->
[]
,
[]
,
f
in
match
f
.
t_node
with
|
Tapp
(
_
,
[
_
;
f
])
|
F
binop
(
_
,
_
,
f
)
->
vl
,
f
|
T
binop
(
_
,
_
,
f
)
->
vl
,
f
|
_
->
assert
false
let
ls_defn_axiom
(
_
,
f
)
=
f
...
...
@@ -124,8 +124,8 @@ let build_call_graph cgr syms ls =
let
p
,
t
=
t_open_branch
b
in
let
vml
=
match_term
vm
e
[
vm
]
p
in
List
.
iter
(
fun
vm
->
term
vm
()
t
)
vml
)
bl
|
F
quant
(
_
,
b
)
->
let
_
,_,
f
=
f
_open_quant
b
in
term
vm
()
f
|
T
quant
(
_
,
b
)
->
let
_
,_,
f
=
t
_open_quant
b
in
term
vm
()
f
|
_
->
t_fold
(
term
vm
)
()
t
in
fun
(
vl
,
e
)
->
...
...
@@ -245,7 +245,7 @@ let pr_hash pr = id_hash pr.pr_name
let
create_prsymbol
n
=
{
pr_name
=
id_register
n
}
type
ind_decl
=
lsymbol
*
(
prsymbol
*
fmla
)
list
type
ind_decl
=
lsymbol
*
(
prsymbol
*
term
)
list
(** Proposition declaration *)
...
...
@@ -255,7 +255,7 @@ type prop_kind =
|
Pgoal
(* prove, do not use as a premise *)
|
Pskip
(* do not prove, do not use as a premise *)
type
prop_decl
=
prop_kind
*
prsymbol
*
fmla
type
prop_decl
=
prop_kind
*
prsymbol
*
term
(** Declaration type *)
...
...
@@ -431,11 +431,11 @@ let t_pos_ps sps = t_s_all (fun _ -> true) (fun s -> not (ls_mem s sps))
let
rec
f_pos_ps
sps
pol
f
=
match
f
.
t_node
,
pol
with
|
Tapp
(
s
,
_
)
,
Some
false
when
ls_mem
s
sps
->
false
|
Tapp
(
s
,
_
)
,
None
when
ls_mem
s
sps
->
false
|
F
binop
(
F
iff
,
f
,
g
)
,
_
->
|
T
binop
(
T
iff
,
f
,
g
)
,
_
->
f_pos_ps
sps
None
f
&&
f_pos_ps
sps
None
g
|
F
binop
(
F
implies
,
f
,
g
)
,
_
->
|
T
binop
(
T
implies
,
f
,
g
)
,
_
->
f_pos_ps
sps
(
option_map
not
pol
)
f
&&
f_pos_ps
sps
pol
g
|
F
not
f
,
_
->
|
T
not
f
,
_
->
f_pos_ps
sps
(
option_map
not
pol
)
f
|
Tif
(
f
,
g
,
h
)
,
_
->
f_pos_ps
sps
None
f
&&
f_pos_ps
sps
pol
g
&&
f_pos_ps
sps
pol
h
...
...
@@ -447,9 +447,9 @@ let create_ind_decl idl =
let
sps
=
List
.
fold_left
add
Sls
.
empty
idl
in
let
check_ax
ps
(
syms
,
news
)
(
pr
,
f
)
=
let
rec
clause
acc
f
=
match
f
.
t_node
with
|
F
quant
(
F
forall
,
f
)
->
let
_
,_,
f
=
f
_open_quant
f
in
clause
acc
f
|
F
binop
(
F
implies
,
g
,
f
)
->
clause
(
g
::
acc
)
f
|
T
quant
(
T
forall
,
f
)
->
let
_
,_,
f
=
t
_open_quant
f
in
clause
acc
f
|
T
binop
(
T
implies
,
g
,
f
)
->
clause
(
g
::
acc
)
f
|
_
->
(
acc
,
f
)
in
let
cls
,
f
=
clause
[]
(
check_fvs
f
)
in
...
...
@@ -532,9 +532,9 @@ let decl_map_fold fn acc d = match d.d_node with
acc
,
create_prop_decl
k
pr
f
module
DeclTF
=
struct
let
decl_map
fnT
fnF
=
decl_map
(
e_map
fnT
fnF
)
let
decl_fold
fnT
fnF
=
decl_fold
(
e_fold
fnT
fnF
)
let
decl_map_fold
fnT
fnF
=
decl_map_fold
(
e_fold
fnT
fnF
)
let
decl_map
fnT
fnF
=
decl_map
(
TermTF
.
t_select
fnT
fnF
)
let
decl_fold
fnT
fnF
=
decl_fold
(
TermTF
.
t_selecti
fnT
fnF
)
let
decl_map_fold
fnT
fnF
=
decl_map_fold
(
TermTF
.
t_selecti
fnT
fnF
)
end
(** Known identifiers *)
...
...
src/core/decl.mli
View file @
3047a120
...
...
@@ -43,7 +43,7 @@ val make_ls_defn : lsymbol -> vsymbol list -> term -> logic_decl
val
open_ls_defn
:
ls_defn
->
vsymbol
list
*
term
val
ls_defn_axiom
:
ls_defn
->
fmla
val
ls_defn_axiom
:
ls_defn
->
term
val
check_termination
:
logic_decl
list
->
(
int
list
)
Mls
.
t
(** [check_termination ldl] returns a mapping of every logical
...
...
@@ -69,7 +69,7 @@ val pr_equal : prsymbol -> prsymbol -> bool
val
pr_hash
:
prsymbol
->
int
type
ind_decl
=
lsymbol
*
(
prsymbol
*
fmla
)
list
type
ind_decl
=
lsymbol
*
(
prsymbol
*
term
)
list
(* Proposition declaration *)
...
...
@@ -79,7 +79,7 @@ type prop_kind =
|
Pgoal
(* prove, do not use as a premise *)
|
Pskip
(* do not prove, do not use as a premise *)
type
prop_decl
=
prop_kind
*
prsymbol
*
fmla
type
prop_decl
=
prop_kind
*
prsymbol
*
term
(** {2 Declaration type} *)
...
...
@@ -108,7 +108,7 @@ val d_hash : decl -> int
val
create_ty_decl
:
ty_decl
list
->
decl
val
create_logic_decl
:
logic_decl
list
->
decl
val
create_ind_decl
:
ind_decl
list
->
decl
val
create_prop_decl
:
prop_kind
->
prsymbol
->
fmla
->
decl
val
create_prop_decl
:
prop_kind
->
prsymbol
->
term
->
decl
(* exceptions *)
...
...
@@ -137,12 +137,12 @@ val decl_map_fold : ('a -> term -> 'a * term) -> 'a -> decl -> 'a * decl
module
DeclTF
:
sig
val
decl_map
:
(
term
->
term
)
->
(
fmla
->
fmla
)
->
decl
->
decl
val
decl_map
:
(
term
->
term
)
->
(
term
->
term
)
->
decl
->
decl
val
decl_fold
:
(
'
a
->
term
->
'
a
)
->
(
'
a
->
fmla
->
'
a
)
->
'
a
->
decl
->
'
a
val
decl_fold
:
(
'
a
->
term
->
'
a
)
->
(
'
a
->
term
->
'
a
)
->
'
a
->
decl
->
'
a
val
decl_map_fold
:
(
'
a
->
term
->
'
a
*
term
)
->
(
'
a
->
fmla
->
'
a
*
fmla
)
->
'
a
->
decl
->
'
a
*
decl
val
decl_map_fold
:
(
'
a
->
term
->
'
a
*
term
)
->
(
'
a
->
term
->
'
a
*
term
)
->
'
a
->
decl
->
'
a
*
decl
end
(** {2 Known identifiers} *)
...
...
@@ -160,8 +160,8 @@ exception NonExhaustiveCase of pattern list * term
exception
NonFoundedTypeDecl
of
tysymbol
val
find_constructors
:
known_map
->
tysymbol
->
lsymbol
list
val
find_inductive_cases
:
known_map
->
lsymbol
->
(
prsymbol
*
fmla
)
list
val
find_inductive_cases
:
known_map
->
lsymbol
->
(
prsymbol
*
term
)
list
val
find_logic_definition
:
known_map
->
lsymbol
->
ls_defn
option
val
find_prop
:
known_map
->
prsymbol
->
fmla
val
find_prop_decl
:
known_map
->
prsymbol
->
prop_kind
*
fmla
val
find_prop
:
known_map
->
prsymbol
->
term
val
find_prop_decl
:
known_map
->
prsymbol
->
prop_kind
*
term
src/core/pretty.ml
View file @
3047a120
...
...
@@ -166,20 +166,20 @@ let print_vsty fmt v =
fprintf
fmt
"%a:@,%a"
print_vs
v
print_ty
v
.
vs_ty
let
print_quant
fmt
=
function
|
F
forall
->
fprintf
fmt
"forall"
|
F
exists
->
fprintf
fmt
"exists"
|
T
forall
->
fprintf
fmt
"forall"
|
T
exists
->
fprintf
fmt
"exists"
let
print_binop
fmt
=
function
|
F
and
->
fprintf
fmt
"and"
|
F
or
->
fprintf
fmt
"or"
|
F
implies
->
fprintf
fmt
"->"
|
F
iff
->
fprintf
fmt
"<->"
|
T
and
->
fprintf
fmt
"and"
|
T
or
->
fprintf
fmt
"or"
|
T
implies
->
fprintf
fmt
"->"
|
T
iff
->
fprintf
fmt
"<->"
let
prio_binop
=
function
|
F
and
->
3
|
F
or
->
2
|
F
implies
->
1
|
F
iff
->
1
|
T
and
->
3
|
T
or
->
2
|
T
implies
->
1
|
T
iff
->
1
let
print_label
fmt
l
=
if
l
=
""
then
()
else
fprintf
fmt
"
\"
%s
\"
"
l
...
...
@@ -242,20 +242,20 @@ and print_tnode pri fmt t = match t.t_node with
fprintf
fmt
(
protect_on
(
pri
>
0
)
"epsilon %a.@ %a"
)
print_vsty
v
print_term
f
;
forget_var
v
|
F
quant
(
q
,
fq
)
->
let
vl
,
tl
,
f
=
f
_open_quant
fq
in
|
T
quant
(
q
,
fq
)
->
let
vl
,
tl
,
f
=
t
_open_quant
fq
in
fprintf
fmt
(
protect_on
(
pri
>
0
)
"%a %a%a.@ %a"
)
print_quant
q
(
print_list
comma
print_vsty
)
vl
print_tl
tl
print_term
f
;
List
.
iter
forget_var
vl
|
F
true
->
|
T
true
->
fprintf
fmt
"true"
|
F
false
->
|
T
false
->
fprintf
fmt
"false"
|
F
binop
(
b
,
f1
,
f2
)
->
|
T
binop
(
b
,
f1
,
f2
)
->
let
p
=
prio_binop
b
in
fprintf
fmt
(
protect_on
(
pri
>
p
)
"%a %a@ %a"
)
(
print_lterm
(
p
+
1
))
f1
print_binop
b
(
print_lterm
p
)
f2
|
F
not
f
->
|
T
not
f
->
fprintf
fmt
(
protect_on
(
pri
>
4
)
"not %a"
)
(
print_lterm
4
)
f
and
print_tbranch
fmt
br
=
...
...
src/core/printer.ml
View file @
3047a120
...
...
@@ -228,7 +228,6 @@ let query_syntax sm id = Mid.find_option id sm
(** {2 exceptions to use in transformations and printers} *)
exception
UnsupportedTysymbol
of
tysymbol
*
string
exception
UnsupportedType
of
ty
*
string
exception
UnsupportedTerm
of
term
*
string
exception
UnsupportedDecl
of
decl
*
string
...
...
@@ -237,10 +236,8 @@ exception Unsupported of string
(** {3 functions that catch inner error} *)
let
unsupportedTysymbol
e
s
=
raise
(
UnsupportedTysymbol
(
e
,
s
))
let
unsupportedType
e
s
=
raise
(
UnsupportedType
(
e
,
s
))
let
unsupportedTerm
e
s
=
raise
(
UnsupportedTerm
(
e
,
s
))
let
unsupportedFmla
e
s
=
raise
(
UnsupportedTerm
(
e
,
s
))
let
unsupportedDecl
e
s
=
raise
(
UnsupportedDecl
(
e
,
s
))
let
notImplemented
s
=
raise
(
NotImplemented
s
)
let
unsupported
s
=
raise
(
Unsupported
s
)
...
...
@@ -248,9 +245,6 @@ let unsupported s = raise (Unsupported s)
let
catch_unsupportedType
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedType
e
s
let
catch_unsupportedTysymbol
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedTysymbol
e
s
let
catch_unsupportedTerm
f
e
=
try
f
e
with
Unsupported
s
->
unsupportedTerm
e
s
...
...
@@ -277,9 +271,6 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
|
UnsupportedType
(
e
,
s
)
->
fprintf
fmt
"@[<hov 3> This type isn't supported:@
\n
%a@
\n
%s@]"
Pretty
.
print_ty
e
s
|
UnsupportedTysymbol
(
e
,
s
)
->
fprintf
fmt
"@[<hov 3> This type isn't supported:@
\n
%a@
\n
%s@]"
Pretty
.
print_ts
e
s
|
UnsupportedTerm
(
e
,
s
)
->
fprintf
fmt
"@[<hov 3> This expression isn't supported:@
\n
%a@
\n
%s@]"
Pretty
.
print_term
e
s
...
...
src/core/printer.mli
View file @
3047a120
...
...
@@ -72,16 +72,13 @@ val syntax_arguments_typed : string -> term pp -> ty pp ->
(** {2 exceptions to use in transformations and printers} *)
exception
UnsupportedTysymbol
of
tysymbol
*
string
exception
UnsupportedType
of
ty
*
string
exception
UnsupportedTerm
of
term
*
string
exception
UnsupportedDecl
of
decl
*
string
exception
NotImplemented
of
string
val
unsupportedTysymbol
:
tysymbol
->
string
->
'
a
val
unsupportedType
:
ty
->
string
->
'
a
val
unsupportedTerm
:
term
->
string
->
'
a
val
unsupportedFmla
:
fmla
->
string
->
'
a
val
unsupportedDecl
:
decl
->
string
->
'
a
val
notImplemented
:
string
->
'
a
...
...
@@ -98,10 +95,6 @@ val catch_unsupportedType : (ty -> 'a) -> (ty -> 'a)
- return [f arg] if [f arg] does not raise {!Unsupported} exception
- raise [UnsupportedType (arg,s)] if [f arg] raises [Unsupported s]*)
val
catch_unsupportedTysymbol
:
(
tysymbol
->
'
a
)
->
(
tysymbol
->
'
a
)
(** same as {! catch_unsupportedType} but use [UnsupportedTysymbol]
instead of [UnsupportedType]*)
val
catch_unsupportedTerm
:
(
term
->
'
a
)
->
(
term
->
'
a
)
(** same as {! catch_unsupportedType} but use [UnsupportedExpr]
instead of [UnsupportedType]*)
...
...
src/core/task.mli
View file @
3047a120
...
...
@@ -78,7 +78,7 @@ val add_meta : task -> meta -> meta_arg list -> task
val
add_ty_decl
:
task
->
ty_decl
list
->
task
val
add_logic_decl
:
task
->
logic_decl
list
->
task
val
add_ind_decl
:
task
->
ind_decl
list
->
task
val
add_prop_decl
:
task
->
prop_kind
->
prsymbol
->
fmla
->
task
val
add_prop_decl
:
task
->
prop_kind
->
prsymbol
->
term
->
task
(** {2 utilities} *)
...
...
@@ -95,7 +95,7 @@ val task_tdecls : task -> tdecl list
val
task_decls
:
task
->
decl
list
val
task_goal
:
task
->
prsymbol
val
task_goal_fmla
:
task
->
fmla
val
task_goal_fmla
:
task
->
term
(** {2 selectors} *)
...
...
src/core/term.ml
View file @
3047a120
This diff is collapsed.
Click to expand it.
src/core/term.mli
View file @
3047a120
...
...
@@ -53,7 +53,6 @@ module Hls : Hashtbl.S with type key = lsymbol
module
Wls
:
Hashweak
.
S
with
type
key
=
lsymbol
val
ls_equal
:
lsymbol
->
lsymbol
->
bool
(** equality of function and predicate symbols *)
val
ls_hash
:
lsymbol
->
int
val
create_lsymbol
:
preid
->
ty
list
->
ty
option
->
lsymbol
...
...
@@ -108,14 +107,14 @@ val pat_any : (pattern -> bool) -> pattern -> bool
(** {2 Terms and Formulas} *)
type
quant
=
|
F
forall
|
F
exists
|
T
forall
|
T
exists
type
binop
=
|
F
and
|
F
or
|
F
implies
|
F
iff
|
T
and
|
T
or
|
T
implies
|
T
iff
type
real_constant
=
|
RConstDecimal
of
string
*
string
*
string
option
(* int / frac / exp *)
...
...
@@ -138,21 +137,19 @@ and term_node = private
|
Tvar
of
vsymbol
|
Tconst
of
constant
|
Tapp
of
lsymbol
*
term
list
|
Tif
of
fmla
*
term
*
term
|
Tif
of
term
*
term
*
term
|
Tlet
of
term
*
term_bound
|
Tcase
of
term
*
term_branch
list
|
Teps
of
fmla_bound
|
Fquant
of
quant
*
fmla_quant
|
Fbinop
of
binop
*
fmla
*
fmla
|
Fnot
of
fmla
|
Ftrue
|
Ffalse
and
fmla
=
term
|
Teps
of
term_bound
|
Tquant
of
quant
*
term_quant
|
Tbinop
of
binop
*
term
*
term
|
Tnot
of
term
|
Ttrue
|
Tfalse
and
term_bound
and
fmla_bound
=
term_bound
and
term_branch
and
fmla
_quant
and
term
_quant
and
trigger
=
term
list
list
...
...
@@ -169,13 +166,13 @@ val t_hash : term -> int
val
t_close_bound
:
vsymbol
->
term
->
term_bound
val
t_close_branch
:
pattern
->
term
->
term_branch
val
f
_close_quant
:
vsymbol
list
->
trigger
->
fmla
->
fmla
_quant
val
t
_close_quant
:
vsymbol
list
->
trigger
->
term
->
term
_quant
(** open bindings *)
val
t_open_bound
:
term_bound
->
vsymbol
*
term
val
t_open_branch
:
term_branch
->
pattern
*
term
val
f
_open_quant
:
fmla
_quant
->
vsymbol
list
*
trigger
*
fmla
val
t
_open_quant
:
term
_quant
->
vsymbol
list
*
trigger
*
term
(** open bindings with optimized closing callbacks *)
...
...
@@ -185,9 +182,9 @@ val t_open_bound_cb :
val
t_open_branch_cb
:
term_branch
->
pattern
*
term
*
(
pattern
->
term
->
term_branch
)
val
f
_open_quant_cb
:
fmla
_quant
->
vsymbol
list
*
trigger
*
fmla
*
(
vsymbol
list
->
trigger
->
fmla
->
fmla
_quant
)
val
t
_open_quant_cb
:
term
_quant
->
vsymbol
list
*
trigger
*
term
*
(
vsymbol
list
->
trigger
->
term
->
term
_quant
)
(** Type checking *)
...
...
@@ -203,15 +200,11 @@ val t_prop : term -> term
val
t_ty_check
:
term
->
ty
option
->
unit
(** [t_ty_check t ty] checks that the type of [t] is [ty] *)
(** [e_map fnT fnF t] is [fnT t] if [t] is value-typed, [fnF t] otherwise *)
val
e_map
:
(
term
->
'
a
)
->
(
fmla
->
'
a
)
->
term
->
'
a
val
e_fold
:
(
'
a
->
term
->
'
b
)
->
(
'
a
->
fmla
->
'
b
)
->
'
a
->
term
->
'
b
(** Smart constructors for terms and formulas *)
val
t_app
:
lsymbol
->
term
list
->
ty
option
->
term
val
fs_app
:
lsymbol
->
term
list
->
ty
->
term
val
ps_app
:
lsymbol
->
term
list
->
fmla
val
ps_app
:
lsymbol
->
term
list
->
term
val
t_app_infer
:
lsymbol
->
term
list
->
term
val
ls_arg_inst
:
lsymbol
->
term
list
->
ty
Mtv
.
t
...
...
@@ -221,27 +214,27 @@ val t_var : vsymbol -> term
val
t_const
:
constant
->
term
val
t_int_const
:
string
->
term
val
t_real_const
:
real_constant
->
term
val
t_if
:
fmla
->
term
->
term
->
term
val
t_if
:
term
->
term
->
term
->
term
val
t_let
:
term
->
term_bound
->
term
val
t_case
:
term
->
term_branch
list
->
term
val
t_eps
:
fmla
_bound
->
term
val
f
_quant
:
quant
->
fmla
_quant
->
fmla
val
f
_forall
:
fmla
_quant
->
fmla
val
f
_exists
:
fmla
_quant
->
fmla
val
f
_binary
:
binop
->
fmla
->
fmla
->
fmla
val
f
_and
:
fmla
->
fmla
->
fmla
val
f
_or
:
fmla
->
fmla
->
fmla
val
f
_implies
:
fmla
->
fmla
->
fmla
val
f
_iff
:
fmla
->
fmla
->
fmla
val
f
_not
:
fmla
->
fmla
val
f
_true
:
fmla
val
f
_false
:
fmla
val
t_eps
:
term
_bound
->
term
val
t
_quant
:
quant
->
term
_quant
->
term
val
t
_forall
:
term
_quant
->
term
val
t
_exists
:
term
_quant
->
term
val
t
_binary
:
binop
->
term
->
term
->
term
val
t
_and
:
term
->
term
->
term
val
t
_or
:
term
->
term
->
term
val
t
_implies
:
term
->
term
->
term
val
t
_iff
:
term
->
term
->
term
val
t
_not
:
term
->
term
val
t
_true
:
term
val
t
_false
:
term
val
t_let_close
:
vsymbol
->
term
->
term
->
term
val
t_eps_close
:
vsymbol
->
fmla
->
term
val
f
_quant_close
:
quant
->
vsymbol
list
->
trigger
->
fmla
->
fmla
val
f
_forall_close
:
vsymbol
list
->
trigger
->
fmla
->
fmla
val
f
_exists_close
:
vsymbol
list
->
trigger
->
fmla
->
fmla
val
t_eps_close
:
vsymbol
->
term
->
term
val
t
_quant_close
:
quant
->
vsymbol
list
->
trigger
->
term
->
term
val
t
_forall_close
:
vsymbol
list
->
trigger
->
term
->
term
val
t
_exists_close
:
vsymbol
list
->
trigger
->
term
->
term
val
t_label
:
?
loc
:
Loc
.
position
->
label
list
->
term
->
term
val
t_label_add
:
label
->
term
->
term
...
...
@@ -249,26 +242,26 @@ val t_label_copy : term -> term -> term
(** Constructors with propositional simplification *)
val
t_if_simp
:
fmla
->
term
->
term
->
term
val
t_if_simp
:
term
->
term
->
term
->
term
val
t_let_simp
:
term
->
term_bound
->
term
val
f
_quant_simp
:
quant
->
fmla
_quant
->
fmla
val
f
_forall_simp
:
fmla
_quant
->
fmla
val
f
_exists_simp
:
fmla
_quant
->
fmla
val
f
_binary_simp
:
binop
->
fmla
->
fmla
->
fmla
val
f
_and_simp
:
fmla
->
fmla
->
fmla
val
f
_and_simp_l
:
fmla
list
->
fmla
val
f
_or_simp
:
fmla
->
fmla
->
fmla
val
f
_or_simp_l
:
fmla
list
->
fmla
val
f
_implies_simp
:
fmla
->
fmla
->
fmla
val
f
_iff_simp
:
fmla
->
fmla
->
fmla
val
f
_not_simp
:
fmla
->
fmla
val
t
_quant_simp
:
quant
->
term
_quant
->
term
val
t
_forall_simp
:
term
_quant
->
term
val
t
_exists_simp
:
term
_quant
->
term
val
t
_binary_simp
:
binop
->
term
->
term
->
term
val
t
_and_simp
:
term
->
term
->
term
val
t
_and_simp_l
:
term
list
->
term
val
t
_or_simp
:
term
->
term
->
term
val
t
_or_simp_l
:
term
list
->
term