Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
fe31fcaf
Commit
fe31fcaf
authored
May 20, 2011
by
Andrei Paskevich
Browse files
introduce ls_defn_open_cb + some term+fmla fusion
parent
c5343cc8
Changes
8
Hide whitespace changes
Inline
Side-by-side
src/core/decl.ml
View file @
fe31fcaf
...
...
@@ -64,6 +64,15 @@ let open_ls_defn (_,f) =
|
Tbinop
(
_
,
_
,
f
)
->
vl
,
f
|
_
->
assert
false
let
open_ls_defn_cb
ld
=
let
ls
,_
=
ld
in
let
vl
,
t
=
open_ls_defn
ld
in
let
close
ls'
vl'
t'
=
if
t_equal
t
t'
&&
list_all2
vs_equal
vl
vl'
&&
ls_equal
ls
ls'
then
ls
,
Some
ld
else
make_ls_defn
ls'
vl'
t'
in
vl
,
t
,
close
let
ls_defn_axiom
(
_
,
f
)
=
f
(** Termination checking for mutually recursive logic declarations *)
...
...
@@ -481,8 +490,8 @@ let decl_map fn d = match d.d_node with
|
Dlogic
l
->
let
fn
=
function
|
ls
,
Some
ld
->
let
vl
,
e
=
open_ls_defn
ld
in
make_ls_defn
ls
vl
(
fn
e
)
let
vl
,
e
,
close
=
open_ls_defn
_cb
ld
in
close
ls
vl
(
fn
e
)
|
ld
->
ld
in
create_logic_decl
(
List
.
map
fn
l
)
...
...
@@ -510,25 +519,28 @@ let decl_fold fn acc d = match d.d_node with
|
Dprop
(
_
,_,
f
)
->
fn
acc
f
let
rpair_map_fold
f
acc
(
x1
,
x2
)
=
let
acc
,
x2
=
f
acc
x2
i
n
acc
,
(
x1
,
x2
)
let
list_rpair_map_fold
f
=
Util
.
map_fold_left
(
rpair_map_fold
f
)
let
list_
rpair_map_fold
f
n
=
let
f
n
acc
(
x1
,
x2
)
=
let
acc
,
x2
=
fn
acc
x2
in
acc
,
(
x1
,
x2
)
in
Util
.
map_fold_left
fn
let
decl_map_fold
fn
acc
d
=
match
d
.
d_node
with
|
Dtype
_
->
acc
,
d
|
Dlogic
l
->
let
acc
,
l
=
list_rpair_map_fold
(
option_map_fold
(
rpair_map_fold
(
t_map_fold
fn
)))
acc
l
in
let
fn
acc
=
function
|
ls
,
Some
ld
->
let
vl
,
e
,
close
=
open_ls_defn_cb
ld
in
let
acc
,
e
=
fn
acc
e
in
acc
,
close
ls
vl
e
|
ld
->
acc
,
ld
in
let
acc
,
l
=
Util
.
map_fold_left
fn
acc
l
in
acc
,
create_logic_decl
l
|
Dind
l
->
let
acc
,
l
=
list_rpair_map_fold
(
list_rpair_map_fold
(
t_map_fold
fn
))
acc
l
in
let
acc
,
l
=
list_rpair_map_fold
(
list_rpair_map_fold
fn
)
acc
l
in
acc
,
create_ind_decl
l
|
Dprop
(
k
,
pr
,
f
)
->
let
acc
,
f
=
t_map_fold
fn
acc
f
in
let
acc
,
f
=
fn
acc
f
in
acc
,
create_prop_decl
k
pr
f
module
DeclTF
=
struct
...
...
src/core/decl.mli
View file @
fe31fcaf
...
...
@@ -43,6 +43,9 @@ val make_ls_defn : lsymbol -> vsymbol list -> term -> logic_decl
val
open_ls_defn
:
ls_defn
->
vsymbol
list
*
term
val
open_ls_defn_cb
:
ls_defn
->
vsymbol
list
*
term
*
(
lsymbol
->
vsymbol
list
->
term
->
logic_decl
)
val
ls_defn_axiom
:
ls_defn
->
term
val
check_termination
:
logic_decl
list
->
(
int
list
)
Mls
.
t
...
...
src/printer/why3.ml
View file @
fe31fcaf
...
...
@@ -128,7 +128,7 @@ let unambig_fs fs =
|
Tyvar
u
when
not
(
lookup
u
)
->
false
|
_
->
ty_all
inspect
ty
in
inspect
(
of_option
fs
.
ls_value
)
option_apply
true
inspect
fs
.
ls_value
(** Patterns, terms, and formulas *)
...
...
@@ -170,18 +170,12 @@ let prio_binop = function
let
print_label
=
Pretty
.
print_label
let
rec
print_term
fmt
t
=
print_lterm
0
fmt
t
and
print_fmla
fmt
f
=
print_lfmla
0
fmt
f
and
print_lterm
pri
fmt
t
=
match
t
.
t_label
with
|
[]
->
print_tnode
pri
fmt
t
|
ll
->
fprintf
fmt
(
protect_on
(
pri
>
0
)
"%a %a"
)
(
print_list
space
print_label
)
ll
(
print_tnode
0
)
t
and
print_lfmla
pri
fmt
f
=
match
f
.
t_label
with
|
[]
->
print_fnode
pri
fmt
f
|
ll
->
fprintf
fmt
(
protect_on
(
pri
>
0
)
"%a %a"
)
(
print_list
space
print_label
)
ll
(
print_fnode
0
)
f
and
print_tapp
pri
fs
fmt
tl
=
match
query_syntax
fs
.
ls_name
with
|
Some
s
->
syntax_arguments
s
print_term
fmt
tl
...
...
@@ -203,7 +197,7 @@ and print_tnode pri fmt t = match t.t_node with
(
print_tapp
0
fs
)
tl
print_ty
(
t_type
t
)
|
Tif
(
f
,
t1
,
t2
)
->
fprintf
fmt
(
protect_on
(
pri
>
0
)
"if @[%a@] then %a@ else %a"
)
print_
fmla
f
print_term
t1
print_term
t2
print_
term
f
print_term
t1
print_term
t2
|
Tlet
(
t1
,
tb
)
->
let
v
,
t2
=
t_open_bound
tb
in
fprintf
fmt
(
protect_on
(
pri
>
0
)
"let %a = @[%a@] in@ %a"
)
...
...
@@ -215,63 +209,32 @@ and print_tnode pri fmt t = match t.t_node with
|
Teps
fb
->
let
v
,
f
=
t_open_bound
fb
in
fprintf
fmt
(
protect_on
(
pri
>
0
)
"epsilon %a.@ %a"
)
print_vsty
v
print_
fmla
f
;
print_vsty
v
print_
term
f
;
forget_var
v
|
Tquant
_
|
Tbinop
_
|
Tnot
_
|
Ttrue
|
Tfalse
->
raise
(
TermExpected
t
)
and
print_fnode
pri
fmt
f
=
match
f
.
t_node
with
|
Tapp
(
ps
,
tl
)
->
begin
match
query_syntax
ps
.
ls_name
with
|
Some
s
->
syntax_arguments
s
print_term
fmt
tl
|
None
->
begin
match
tl
with
|
[]
->
print_ls
fmt
ps
|
tl
->
fprintf
fmt
(
protect_on
(
pri
>
4
)
"%a@ %a"
)
print_ls
ps
(
print_list
space
(
print_lterm
5
))
tl
end
end
|
Tquant
(
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_
fmla
f
;
(
print_list
comma
print_vsty
)
vl
print_tl
tl
print_
term
f
;
List
.
iter
forget_var
vl
|
Ttrue
->
fprintf
fmt
"true"
|
Tfalse
->
fprintf
fmt
"false"
|
Tbinop
(
b
,
f1
,
f2
)
->
let
p
=
prio_binop
b
in
fprintf
fmt
(
protect_on
(
pri
>
p
)
"%a %a@ %a"
)
(
print_l
fmla
(
p
+
1
))
f1
print_binop
b
(
print_l
fmla
p
)
f2
(
print_l
term
(
p
+
1
))
f1
print_binop
b
(
print_l
term
p
)
f2
|
Tnot
f
->
fprintf
fmt
(
protect_on
(
pri
>
4
)
"not %a"
)
(
print_lfmla
4
)
f
|
Tif
(
f1
,
f2
,
f3
)
->
fprintf
fmt
(
protect_on
(
pri
>
0
)
"if @[%a@] then %a@ else %a"
)
print_fmla
f1
print_fmla
f2
print_fmla
f3
|
Tlet
(
t
,
f
)
->
let
v
,
f
=
t_open_bound
f
in
fprintf
fmt
(
protect_on
(
pri
>
0
)
"let %a = @[%a@] in@ %a"
)
print_vs
v
(
print_lterm
4
)
t
print_fmla
f
;
forget_var
v
|
Tcase
(
t
,
bl
)
->
fprintf
fmt
"match @[%a@] with@
\n
@[<hov>%a@]@
\n
end"
print_term
t
(
print_list
newline
print_fbranch
)
bl
|
Tvar
_
|
Tconst
_
|
Teps
_
->
raise
(
FmlaExpected
f
)
fprintf
fmt
(
protect_on
(
pri
>
4
)
"not %a"
)
(
print_lterm
4
)
f
|
Ttrue
->
fprintf
fmt
"true"
|
Tfalse
->
fprintf
fmt
"false"
and
print_tbranch
fmt
br
=
let
p
,
t
=
t_open_branch
br
in
fprintf
fmt
"@[<hov 4>| %a ->@ %a@]"
print_pat
p
print_term
t
;
Svs
.
iter
forget_var
p
.
pat_vars
and
print_fbranch
fmt
br
=
let
p
,
f
=
t_open_branch
br
in
fprintf
fmt
"@[<hov 4>| %a ->@ %a@]"
print_pat
p
print_fmla
f
;
Svs
.
iter
forget_var
p
.
pat_vars
and
print_tl
fmt
tl
=
if
tl
=
[]
then
()
else
fprintf
fmt
"@ [%a]"
(
print_list
alt
(
print_list
comma
print_expr
))
tl
and
print_expr
fmt
=
TermTF
.
t_select
(
print_term
fmt
)
(
print_fmla
fmt
)
(
print_list
alt
(
print_list
comma
print_term
))
tl
(** Declarations *)
...
...
@@ -320,7 +283,7 @@ let print_logic_decl fst fmt (ls,ld) = match ld with
fprintf
fmt
"@[<hov 2>%s %a%a%a =@ %a@]@
\n
@
\n
"
(
if
fst
then
"logic"
else
"with"
)
print_ls
ls
(
print_list
nothing
print_vs_arg
)
vl
(
print_option
print_ls_type
)
ls
.
ls_value
print_
expr
e
;
(
print_option
print_ls_type
)
ls
.
ls_value
print_
term
e
;
List
.
iter
forget_var
vl
|
None
->
fprintf
fmt
"@[<hov 2>%s %a%a%a@]@
\n
@
\n
"
...
...
@@ -333,7 +296,7 @@ let print_logic_decl first fmt d =
(
print_logic_decl
first
fmt
d
;
forget_tvs
()
)
let
print_ind
fmt
(
pr
,
f
)
=
fprintf
fmt
"@[<hov 4>| %a : %a@]"
print_pr
pr
print_
fmla
f
fprintf
fmt
"@[<hov 4>| %a : %a@]"
print_pr
pr
print_
term
f
let
print_ind_decl
fst
fmt
(
ps
,
bl
)
=
fprintf
fmt
"@[<hov 2>%s %a%a =@ @[<hov>%a@]@]@
\n
@
\n
"
...
...
@@ -349,7 +312,7 @@ let print_pkind = Pretty.print_pkind
let
print_prop_decl
fmt
(
k
,
pr
,
f
)
=
fprintf
fmt
"@[<hov 2>%a %a : %a@]@
\n
@
\n
"
print_pkind
k
print_pr
pr
print_
fmla
f
print_pr
pr
print_
term
f
let
print_prop_decl
fmt
(
k
,
pr
,
f
)
=
match
k
with
|
Paxiom
when
query_remove
pr
.
pr_name
->
()
...
...
src/transform/eliminate_definition.ml
View file @
fe31fcaf
...
...
@@ -62,46 +62,22 @@ let rec t_insert hd t = match t.t_node with
t_close_branch
pl
(
t_insert
hd
t1
)
in
t_case
tl
(
List
.
map
br
bl
)
|
_
->
t_equ_simp
hd
t
let
rec
f_insert
hd
f
=
match
f
.
t_node
with
|
Tif
(
f1
,
f2
,
f3
)
->
t_if
f1
(
f_insert
hd
f2
)
(
f_insert
hd
f3
)
|
Tlet
(
t1
,
bf
)
->
let
v
,
f2
=
t_open_bound
bf
in
t_let_close
v
t1
(
f_insert
hd
f2
)
|
Tcase
(
tl
,
bl
)
->
let
br
b
=
let
pl
,
f1
=
t_open_branch
b
in
t_close_branch
pl
(
f_insert
hd
f1
)
in
t_case
tl
(
List
.
map
br
bl
)
|
_
->
t_iff_simp
hd
f
let
add_ld
func
pred
axl
d
=
match
d
with
|
_
,
None
->
|
_
->
TermTF
.
t_selecti
t_equ_simp
t_iff_simp
hd
t
let
add_ld
func
pred
axl
=
function
|
ls
,
Some
ld
when
(
if
ls
.
ls_value
=
None
then
pred
else
func
)
->
let
vl
,
e
=
open_ls_defn
ld
in
let
nm
=
ls
.
ls_name
.
id_string
^
"_def"
in
let
hd
=
t_app
ls
(
List
.
map
t_var
vl
)
e
.
t_ty
in
let
ax
=
t_forall_close
vl
[]
(
t_insert
hd
e
)
in
let
pr
=
create_prsymbol
(
id_derive
nm
ls
.
ls_name
)
in
create_prop_decl
Paxiom
pr
ax
::
axl
,
(
ls
,
None
)
|
d
->
axl
,
d
|
ls
,
Some
ld
->
let
vl
,
e
=
open_ls_defn
ld
in
begin
match
e
.
t_ty
with
|
Some
_
when
func
->
let
nm
=
ls
.
ls_name
.
id_string
^
"_def"
in
let
hd
=
t_app
ls
(
List
.
map
t_var
vl
)
e
.
t_ty
in
let
ax
=
t_forall_close
vl
[]
(
t_insert
hd
e
)
in
let
pr
=
create_prsymbol
(
id_derive
nm
ls
.
ls_name
)
in
create_prop_decl
Paxiom
pr
ax
::
axl
,
(
ls
,
None
)
|
None
when
pred
->
let
nm
=
ls
.
ls_name
.
id_string
^
"_def"
in
let
hd
=
ps_app
ls
(
List
.
map
t_var
vl
)
in
let
ax
=
t_forall_close
vl
[]
(
f_insert
hd
e
)
in
let
pr
=
create_prsymbol
(
id_derive
nm
ls
.
ls_name
)
in
create_prop_decl
Paxiom
pr
ax
::
axl
,
(
ls
,
None
)
|
_
->
axl
,
d
end
let
elim_decl
func
pred
l
=
let
axl
,
l
=
map_fold_left
(
add_ld
func
pred
)
[]
l
in
let
d
=
create_logic_decl
l
in
d
::
List
.
rev
axl
create_logic_decl
l
::
List
.
rev
axl
let
elim
func
pred
d
=
match
d
.
d_node
with
|
Dlogic
l
->
elim_decl
func
pred
l
...
...
@@ -112,10 +88,7 @@ let is_rec = function
|
[
_
,
None
]
->
false
|
[
ls
,
Some
ld
]
->
let
_
,
e
=
open_ls_defn
ld
in
begin
match
e
.
t_ty
with
|
Some
_
->
t_s_any
(
const
false
)
(
ls_equal
ls
)
e
|
None
->
t_s_any
(
const
false
)
(
ls_equal
ls
)
e
end
t_s_any
Util
.
ffalse
(
ls_equal
ls
)
e
|
_
->
true
let
elim_recursion
d
=
match
d
.
d_node
with
...
...
@@ -144,4 +117,3 @@ let () =
Trans
.
register_transform
"eliminate_mutual_recursion"
eliminate_mutual_recursion
src/transform/eliminate_if.ml
View file @
fe31fcaf
...
...
@@ -71,7 +71,7 @@ let rec elim_t t = TermTF.t_map elim_t elim_f t
let
add_ld
axl
d
=
match
d
with
|
_
,
None
->
axl
,
d
|
ls
,
Some
ld
->
let
vl
,
e
=
open_ls_defn
ld
in
let
vl
,
e
,
close
=
open_ls_defn
_cb
ld
in
begin
match
e
.
t_ty
with
|
Some
_
when
has_if
e
->
let
nm
=
ls
.
ls_name
.
id_string
^
"_def"
in
...
...
@@ -80,7 +80,7 @@ let add_ld axl d = match d with
let
f
=
t_forall_close
vl
[]
(
elim_f
(
t_equ
hd
e
))
in
create_prop_decl
Paxiom
pr
f
::
axl
,
(
ls
,
None
)
|
_
->
axl
,
make_ls_defn
ls
vl
(
TermTF
.
t_select
elim_t
elim_f
e
)
axl
,
close
ls
vl
(
TermTF
.
t_select
elim_t
elim_f
e
)
end
let
elim_d
d
=
match
d
.
d_node
with
...
...
src/transform/encoding_explicit.ml
View file @
fe31fcaf
...
...
@@ -67,20 +67,12 @@ module Transform = struct
(** translation of terms *)
let
rec
term_transform
varM
t
=
match
t
.
t_node
with
|
Tapp
(
f
,
terms
)
->
(* first case : predicate (not =), we must translate it and its args *)
|
Tapp
(
f
,
terms
)
when
not
(
ls_equal
f
ps_equ
)
->
let
terms
=
args_transform
varM
f
terms
t
.
t_ty
in
t_app
(
findL
f
)
terms
t
.
t_ty
|
_
->
(* default case : traverse *)
TermTF
.
t_map
(
term_transform
varM
)
(
fmla_transform
varM
)
t
(** translation of formulae *)
and
fmla_transform
varM
f
=
match
f
.
t_node
with
(* first case : predicate (not =), we must translate it and its args *)
|
Tapp
(
p
,
terms
)
when
not
(
ls_equal
p
ps_equ
)
->
let
terms
=
args_transform
varM
p
terms
None
in
ps_app
(
findL
p
)
terms
|
_
->
(* otherwise : just traverse and translate *)
TermTF
.
t_map
(
term_transform
varM
)
(
fmla_transform
varM
)
f
t_map
(
term_transform
varM
)
t
and
args_transform
varM
ls
args
ty
=
(* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
...
...
@@ -98,19 +90,14 @@ module Transform = struct
let
helper
=
function
|
(
lsymbol
,
Some
ldef
)
->
let
new_lsymbol
=
findL
lsymbol
in
(* new lsymbol *)
let
vars
,
expr
=
open_ls_defn
ldef
in
let
vars
,
expr
,
close
=
open_ls_defn
_cb
ldef
in
let
add
v
(
vl
,
vm
)
=
let
vs
=
Term
.
create_vsymbol
(
id_fresh
"t"
)
ty_type
in
vs
::
vl
,
Mtv
.
add
v
(
t_var
vs
)
vm
in
let
vars
,
varM
=
Stv
.
fold
add
(
ls_ty_freevars
lsymbol
)
(
vars
,
Mtv
.
empty
)
in
(
match
expr
.
t_ty
with
|
Some
_
->
let
t
=
term_transform
varM
expr
in
Decl
.
make_ls_defn
new_lsymbol
vars
t
|
None
->
let
f
=
fmla_transform
varM
expr
in
Decl
.
make_ls_defn
new_lsymbol
vars
f
)
let
t
=
term_transform
varM
expr
in
close
new_lsymbol
vars
t
|
(
lsymbol
,
None
)
->
(
findL
lsymbol
,
None
)
in
...
...
@@ -118,13 +105,13 @@ module Transform = struct
(** transform an inductive declaration *)
let
ind_transform
idl
=
let
iconv
(
pr
,
f
)
=
pr
,
Libencoding
.
t_type_close
fmla
_transform
f
in
let
iconv
(
pr
,
f
)
=
pr
,
Libencoding
.
t_type_close
term
_transform
f
in
let
conv
(
ls
,
il
)
=
findL
ls
,
List
.
map
iconv
il
in
[
Decl
.
create_ind_decl
(
List
.
map
conv
idl
)]
(** transforms a proposition into another (mostly a substitution) *)
let
prop_transform
(
prop_kind
,
prop_name
,
f
)
=
let
quantified_fmla
=
Libencoding
.
t_type_close
fmla
_transform
f
in
let
quantified_fmla
=
Libencoding
.
t_type_close
term
_transform
f
in
[
Decl
.
create_prop_decl
prop_kind
prop_name
quantified_fmla
]
end
...
...
src/transform/encoding_guard.ml
View file @
fe31fcaf
...
...
@@ -87,7 +87,7 @@ module Transform = struct
(** creates a new logic symbol, with a different type if the
given symbol was polymorphic *)
let
findL
=
Wls
.
memoize
63
(
fun
lsymbol
->
if
ls_equal
lsymbol
ps_equ
||
lsymbol
.
ls_value
=
None
then
lsymbol
else
if
lsymbol
.
ls_value
=
None
then
lsymbol
else
let
new_ty
=
type_variable_only_in_value
lsymbol
in
(* as many t as type vars *)
if
Stv
.
is_empty
new_ty
then
lsymbol
(* same type *)
else
...
...
@@ -113,30 +113,22 @@ module Transform = struct
(** translation of terms *)
let
rec
term_transform
kept
varM
t
=
match
t
.
t_node
with
|
Tapp
(
f
,
terms
)
->
let
terms
=
args_transform
kept
varM
f
terms
(
t_type
t
)
in
t_app
(
findL
f
)
terms
t
.
t_ty
|
_
->
(* default case : traverse *)
TermTF
.
t_map
(
term_transform
kept
varM
)
(
fmla_transform
kept
varM
)
t
(** translation of formulae *)
and
fmla_transform
kept
varM
f
=
match
f
.
t_node
with
(* first case : predicate are not translated *)
|
Tapp
(
p
,
terms
)
->
|
Tapp
(
p
,
terms
)
when
t
.
t_ty
=
None
->
let
terms
=
List
.
map
(
term_transform
kept
varM
)
terms
in
ps_app
(
findL
p
)
terms
|
Tapp
(
f
,
terms
)
->
let
terms
=
args_transform
kept
varM
f
terms
(
t_type
t
)
in
t_app
(
findL
f
)
terms
t
.
t_ty
|
Tquant
(
q
,_
)
->
let
vsl
,
trl
,
fmla
=
f_open_all_quant
q
f
in
let
fmla
=
fmla
_transform
kept
varM
fmla
in
let
vsl
,
trl
,
fmla
=
f_open_all_quant
q
t
in
let
fmla
=
term
_transform
kept
varM
fmla
in
let
fmla2
=
guard
q
kept
varM
fmla
vsl
in
(* TODO : how to modify the triggers? *)
let
trl
=
TermTF
.
tr_map
(
term_transform
kept
varM
)
(
fmla_transform
kept
varM
)
trl
in
let
trl
=
tr_map
(
term_transform
kept
varM
)
trl
in
t_quant
q
(
t_close_quant
vsl
trl
fmla2
)
|
_
->
(* otherwise : just traverse and translate *)
TermTF
.
t_map
(
term_transform
kept
varM
)
(
fmla_transform
kept
varM
)
f
(* in *)
(* Format.eprintf "fmla_to : %a@." Pretty.print_fmla f;f *)
|
_
->
(* default case : traverse *)
t_map
(
term_transform
kept
varM
)
t
and
guard
q
kept
varM
fmla
vsl
=
let
aux
fmla
vs
=
...
...
@@ -168,14 +160,13 @@ module Transform = struct
let
fn
varM
f
=
let
fmla2
=
guard
q
kept
varM
f
vsl
in
(* TODO : how to modify the triggers? *)
let
trl
=
TermTF
.
tr_map
(
term_transform
kept
varM
)
(
fmla_transform
kept
varM
)
trl
in
let
trl
=
tr_map
(
term_transform
kept
varM
)
trl
in
fn
varM
(
t_quant
q
(
t_close_quant
vsl
trl
fmla2
))
in
let
fn
varM
f
=
fn
varM
(
fmla
_transform
kept
varM
f
)
in
let
fn
varM
f
=
fn
varM
(
term
_transform
kept
varM
f
)
in
type_close_select
tvs
acc
fn
fmla
|
_
->
let
fn
varM
f
=
fn
varM
(
fmla
_transform
kept
varM
f
)
in
let
fn
varM
f
=
fn
varM
(
term
_transform
kept
varM
f
)
in
type_close_select
tvs
acc
fn
f
in
trans
(
fun
_
f
->
f
)
[]
f'
...
...
@@ -214,7 +205,7 @@ module Transform = struct
let
helper
=
function
|
(
lsymbol
,
Some
ldef
)
->
let
new_lsymbol
=
findL
lsymbol
in
(* new lsymbol *)
let
vars
,
expr
=
open_ls_defn
ldef
in
let
vars
,
expr
,
close
=
open_ls_defn
_cb
ldef
in
let
add
v
(
vl
,
vm
)
=
let
vs
=
Term
.
create_vsymbol
(
id_fresh
"t"
)
ty_type
in
vs
::
vl
,
Mtv
.
add
v
(
t_var
vs
)
vm
...
...
@@ -225,13 +216,8 @@ module Transform = struct
|
Some
ty_value
->
let
new_ty
=
ty_freevars
Stv
.
empty
ty_value
in
Stv
.
fold
add
new_ty
(
vars
,
Mtv
.
empty
)
in
(
match
expr
.
t_ty
with
|
Some
_
->
let
t
=
term_transform
kept
varM
expr
in
Decl
.
make_ls_defn
new_lsymbol
vars
t
|
None
->
let
f
=
fmla_transform
kept
varM
expr
in
Decl
.
make_ls_defn
new_lsymbol
vars
f
)
let
t
=
term_transform
kept
varM
expr
in
close
new_lsymbol
vars
t
|
(
lsymbol
,
None
)
->
(
findL
lsymbol
,
None
)
in
...
...
src/transform/libencoding.ml
View file @
fe31fcaf
...
...
@@ -153,7 +153,6 @@ let vs_monomorph ty_base kept vs =
let
rec
t_monomorph
ty_base
kept
lsmap
consts
vmap
t
=
let
t_mono
=
t_monomorph
ty_base
kept
lsmap
consts
in
let
f_mono
=
f_monomorph
ty_base
kept
lsmap
consts
in
t_label_copy
t
(
match
t
.
t_node
with
|
Tvar
v
->
Mvs
.
find
v
vmap
...
...
@@ -163,12 +162,13 @@ let rec t_monomorph ty_base kept lsmap consts vmap t =
let
ls
=
ls_of_const
ty_base
t
in
consts
:=
Sls
.
add
ls
!
consts
;
fs_app
ls
[]
ty_base
|
Tapp
(
fs
,
tl
)
->
let
fs
=
lsmap
fs
in
let
ty
=
of_option
fs
.
ls_value
in
fs_app
fs
(
List
.
map
(
t_mono
vmap
)
tl
)
ty
|
Tapp
(
ps
,
[
t1
;
t2
])
when
ls_equal
ps
ps_equ
->
t_equ
(
t_mono
vmap
t1
)
(
t_mono
vmap
t2
)
|
Tapp
(
ls
,
tl
)
->
let
ls
=
lsmap
ls
in
t_app
ls
(
List
.
map
(
t_mono
vmap
)
tl
)
ls
.
ls_value
|
Tif
(
f
,
t1
,
t2
)
->
t_if
(
f
_mono
vmap
f
)
(
t_mono
vmap
t1
)
(
t_mono
vmap
t2
)
t_if
(
t
_mono
vmap
f
)
(
t_mono
vmap
t1
)
(
t_mono
vmap
t2
)
|
Tlet
(
t1
,
b
)
->
let
u
,
t2
,
close
=
t_open_bound_cb
b
in
let
v
=
vs_monomorph
ty_base
kept
u
in
...
...
@@ -179,47 +179,26 @@ let rec t_monomorph ty_base kept lsmap consts vmap t =
|
Teps
b
->
let
u
,
f
,
close
=
t_open_bound_cb
b
in
let
v
=
vs_monomorph
ty_base
kept
u
in
let
f
=
f
_mono
(
Mvs
.
add
u
(
t_var
v
)
vmap
)
f
in
let
f
=
t
_mono
(
Mvs
.
add
u
(
t_var
v
)
vmap
)
f
in
t_eps
(
close
v
f
)
|
Tquant
_
|
Tbinop
_
|
Tnot
_
|
Ttrue
|
Tfalse
->
raise
(
TermExpected
t
))
and
f_monomorph
ty_base
kept
lsmap
consts
vmap
f
=
let
t_mono
=
t_monomorph
ty_base
kept
lsmap
consts
in
let
f_mono
=
f_monomorph
ty_base
kept
lsmap
consts
in
t_label_copy
f
(
match
f
.
t_node
with
|
Tapp
(
ps
,
[
t1
;
t2
])
when
ls_equal
ps
ps_equ
->
t_equ
(
t_mono
vmap
t1
)
(
t_mono
vmap
t2
)
|
Tapp
(
ps
,
tl
)
->
ps_app
(
lsmap
ps
)
(
List
.
map
(
t_mono
vmap
)
tl
)
|
Tquant
(
q
,
b
)
->
let
ul
,
tl
,
f1
,
close
=
t_open_quant_cb
b
in
let
vl
=
List
.
map
(
vs_monomorph
ty_base
kept
)
ul
in
let
add
acc
u
v
=
Mvs
.
add
u
(
t_var
v
)
acc
in
let
vmap
=
List
.
fold_left2
add
vmap
ul
vl
in
let
tl
=
TermTF
.
tr_map
(
t_mono
vmap
)
(
f_mono
vmap
)
tl
in
t_quant
q
(
close
vl
tl
(
f
_mono
vmap
f1
))
let
tl
=
tr_map
(
t_mono
vmap
)
tl
in
t_quant
q
(
close
vl
tl
(
t
_mono
vmap
f1
))
|
Tbinop
(
op
,
f1
,
f2
)
->
t_binary
op
(
f
_mono
vmap
f1
)
(
f
_mono
vmap
f2
)
t_binary
op
(
t
_mono
vmap
f1
)
(
t
_mono
vmap
f2
)
|
Tnot
f1
->
t_not
(
f
_mono
vmap
f1
)
t_not
(
t
_mono
vmap
f1
)
|
Ttrue
|
Tfalse
->
f
|
Tif
(
f1
,
f2
,
f3
)
->
t_if
(
f_mono
vmap
f1
)
(
f_mono
vmap
f2
)
(
f_mono
vmap
f3
)
|
Tlet
(
t
,
b
)
->
let
u
,
f1
,
close
=
t_open_bound_cb
b
in
let
v
=
vs_monomorph
ty_base
kept
u
in
let
f1
=
f_mono
(
Mvs
.
add
u
(
t_var
v
)
vmap
)
f1
in
t_let
(
t_mono
vmap
t
)
(
close
v
f1
)
|
Tcase
_
->
Printer
.
unsupportedTerm
f
"no match expressions at this point"
|
Tvar
_
|
Tconst
_
|
Teps
_
->
raise
(
FmlaExpected
f
))
t
)
let
d_monomorph
ty_base
kept
lsmap
d
=
let
kept
=
Sty
.
add
ty_base
kept
in
let
consts
=
ref
Sls
.
empty
in
let
t_mono
=
t_monomorph
ty_base
kept
lsmap
consts
in
let
f_mono
=
f_monomorph
ty_base
kept
lsmap
consts
in
let
dl
=
match
d
.
d_node
with
|
Dtype
tdl
->
let
add
td
acc
=
match
td
with
...
...
@@ -237,22 +216,21 @@ let d_monomorph ty_base kept lsmap d =
in
match
ld
with
|
Some
ld
->
let
ul
,
e
=
open_ls_defn
ld
in
let
ul
,
e
,
close
=
open_ls_defn
_cb
ld
in
let
vl
=
List
.
map
(
vs_monomorph
ty_base
kept
)
ul
in
let
add
acc
u
v
=
Mvs
.
add
u
(
t_var
v
)
acc
in
let
vmap
=
List
.
fold_left2
add
Mvs
.
empty
ul
vl
in
let
e
=
TermTF
.
t_selecti
t_mono
f_mono
vmap
e
in
make_ls_defn
ls
vl
e
close
ls
vl
(
t_mono
vmap
e
)
|
None
->
ls
,
None
in
[
create_logic_decl
(
List
.
map
conv
ldl
)]
|
Dind
idl
->
let
iconv
(
pr
,
f
)
=
pr
,
f
_mono
Mvs
.
empty
f
in
let
iconv
(
pr
,
f
)
=
pr
,
t
_mono
Mvs
.
empty
f
in
let
conv
(
ls
,
il
)
=
lsmap
ls
,
List
.
map
iconv
il
in
[
create_ind_decl
(
List
.
map
conv
idl
)]
|
Dprop
(
k
,
pr
,
f
)
->
[
create_prop_decl
k
pr
(
f
_mono
Mvs
.
empty
f
)]
[
create_prop_decl
k
pr
(
t
_mono
Mvs
.
empty
f
)]
in
let
add
ls
acc
=
create_logic_decl
[
ls
,
None
]
::
acc
in
Sls
.
fold
add
!
consts
dl
...
...
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