Skip to content
GitLab
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
3b0a2723
Commit
3b0a2723
authored
May 25, 2010
by
Simon Cruanes
Browse files
bugs tracking in progress in explicit_polymorphism
parent
55f3ee72
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/transform/explicit_polymorphism.ml
View file @
3b0a2723
...
...
@@ -29,8 +29,26 @@ open Term
open
Decl
open
Task
(** module with printing functions *)
module
Debug
=
struct
let
print_mtv
vprinter
fmter
m
=
Mtv
.
iter
(
fun
key
value
->
Format
.
fprintf
fmter
"@[%a@] -> @[%a@]@."
Pretty
.
print_tv
key
vprinter
value
)
m
let
print_mty
vprinter
fmter
m
=
Mty
.
iter
(
fun
key
value
->
Format
.
fprintf
fmter
"@[%a@] -> @[%a@]@."
Pretty
.
print_ty
key
vprinter
value
)
m
(** utility to print a list of items *)
let
rec
print_list
printer
fmter
=
function
|
[]
->
Format
.
fprintf
fmter
""
|
e
::
es
->
if
es
=
[]
then
Format
.
fprintf
fmter
"@[%a@] %a"
printer
e
(
print_list
printer
)
es
else
Format
.
fprintf
fmter
"@[%a@], %a"
printer
e
(
print_list
printer
)
es
let
debug
x
=
Format
.
eprintf
"%s@."
x
end
(** {2 small functions} *)
...
...
@@ -39,29 +57,68 @@ module Utils = struct
(** parenthesing operator *)
let
(
$
)
f
x
=
f
x
let
const
x
_
=
x
let
map_keys
m
=
Mty
.
fold
(
fun
key
_
acc
->
key
::
acc
)
m
[]
let
map_values
m
=
Mty
.
fold
(
fun
_
value
acc
->
value
::
acc
)
m
[]
(** type representing types *)
let
t
=
Ty
.
create_tysymbol
(
id_fresh
"t"
)
[]
None
let
my_t
=
ty_app
t
[]
let
t_decl
=
Decl
.
create_ty_decl
[(
t
,
Tabstract
)]
let
has_type_t
=
ty_equal
(
ty_app
t
[]
)
let
has_type_t
=
ty_equal
my_t
let
is_tyvar
=
function
|
Tyvar
_
->
true
|
_
->
false
and
from_tyvar
=
function
let
from_tyvar
=
function
|
Tyvar
x
->
x
|
_
->
failwith
"from_tyvar called on non-tyvar"
let
isSome
=
function
|
Some
_
->
true
|
_
->
false
let
fromSome
=
function
|
Some
x
->
x
|
None
->
failwith
"fromSome called on None"
(** returns all type vars (free) in given fmla_node *)
let
rec
find_type_vars
acc
f
=
match
f
.
f_node
with
(** list from 1 to n *)
let
range
n
=
let
rec
helper
acc
=
function
|
0
->
acc
|
n
->
helper
(
n
::
acc
)
(
n
-
1
)
in
helper
[]
n
(** [drop n l] is [l], without its [n] first elements *)
let
rec
drop
n
l
=
match
(
n
,
l
)
with
|
(
0
,
_
)
->
l
|
(
n
,
[]
)
->
failwith
"dropping items from empty list"
|
(
_
,
x
::
xs
)
->
drop
(
n
-
1
)
xs
(** explore a type to seek all type vars *)
let
rec
find_tyvars
tyvars
ty
=
match
ty
.
ty_node
with
|
Tyvar
_
->
(* test if ty has already been found *)
(
try
ignore
$
List
.
find
(
fun
x
->
x
.
ty_tag
=
ty
.
ty_tag
)
tyvars
;
tyvars
with
Not_found
->
ty
::
tyvars
)
|
Tyapp
(
_
,
tys
)
->
List
.
fold_left
find_tyvars
tyvars
tys
(** predicate to check whether a type has type vars *)
and
has_tyvars
ty
=
match
ty
.
ty_node
with
|
Tyvar
_
->
true
|
Tyapp
(
_
,
tys
)
->
List
.
exists
has_tyvars
tys
(** returns all type vars (free) in given fmla [f] *)
let
rec
f_find_type_vars
acc
f
=
match
f
.
f_node
with
|
Fapp
(
p
,
terms
)
->
let
new_acc
=
List
.
filter
(
fun
x
->
is_tyvar
x
.
ty_node
)
p
.
ls_args
in
List
.
fold_left
term_analyse
(
new_acc
@
acc
)
terms
|
_
->
f_fold
term_analyse
find_type_vars
acc
f
and
term_analyse
acc
t
=
match
t
.
t_node
with
|
Tvar
x
when
is_tyvar
(
x
.
vs_ty
.
ty_node
)
->
x
.
vs_ty
::
acc
|
_
->
t_fold
term_analyse
find_type_vars
acc
t
List
.
fold_left
t_find_type_vars
acc
terms
|
_
->
f_fold
t_find_type_vars
f_find_type_vars
acc
f
(** returns all type vars in given term *)
and
t_find_type_vars
acc
t
=
match
t
.
t_node
with
|
Tvar
x
->
find_tyvars
acc
x
.
vs_ty
|
_
->
t_fold
t_find_type_vars
f_find_type_vars
acc
t
(** returns all type vars in given lsymbol *)
and
l_find_type_vars
l
=
let
acc
=
match
l
.
ls_value
with
|
None
->
[]
|
Some
ty
->
find_tyvars
[]
ty
in
List
.
fold_left
find_tyvars
acc
l
.
ls_args
(** kind of composition of filter and map *)
...
...
@@ -71,20 +128,33 @@ module Utils = struct
|
None
->
mapSome
f
es
)
|
[]
->
[]
let
from_ty_node
=
function
|
Tyvar
_
->
assert
false
|
Tyapp
(
ty_symb
,
vars
)
->
(
ty_symb
,
vars
)
(** to get unique elements in list (inefficient) *)
let
list_unique
l
=
let
remember
memory
x
=
if
List
.
mem
x
memory
then
memory
else
x
::
memory
in
List
.
fold_left
remember
[]
l
(* FIXME : make it efficient *)
let
const
x
_
=
x
(** [find_matching_vars tv_to_ty left right] matches [left]
against [right] to deduce a mapping from type vars in [left]
to types in [right]. [tv_to_ty] is a mapping given in argument.
It must be compliant with the unification between [left] and [right] *)
let
rec
find_matching_vars
tv_to_ty
left
right
=
assert
(
List
.
length
left
=
List
.
length
right
);
Format
.
eprintf
"matching @[%a@] with @[%a@]@."
(
Debug
.
print_list
Pretty
.
print_ty
)
left
(
Debug
.
print_list
Pretty
.
print_ty
)
right
;
let
tv_to_ty
=
List
.
fold_left2
ty_match
tv_to_ty
left
right
in
Format
.
eprintf
"gives @[%a@]@."
(
Debug
.
print_mtv
Pretty
.
print_ty
)
tv_to_ty
;
flush
stderr
;
tv_to_ty
module
Mint
=
Map
.
Make
(
struct
type
t
=
int
let
compare
=
Pervasives
.
compare
end
);;
(** [bind_nums_to_type_vars l] takes a lsymbol [l], and binds 1..n (where
n is the number of type vars in [l]) to type vars of [l] *)
let
bind_nums_to_type_vars
l
=
let
type_vars
=
l_find_type_vars
l
in
let
n
=
List
.
length
type_vars
in
List
.
fold_left2
(
fun
acc
key
value
->
Mint
.
add
key
value
acc
)
Mint
.
empty
(
range
n
)
type_vars
let
map_keys
m
=
Mty
.
fold
(
fun
key
_value
acc
->
key
::
acc
)
m
[]
let
map_values
m
=
Mty
.
fold
(
fun
_key
value
acc
->
value
::
acc
)
m
[]
end
...
...
@@ -93,7 +163,9 @@ open Utils
(** {2 module to separate utilities from important functions} *)
module
Prelude
=
struct
module
Transform
=
struct
(** {1 memoization facilities} *)
(** [find construct tbl id] searches for the object associated with
[id] in [tbl]. It creates it with [construct id] if it cannot find it. *)
...
...
@@ -109,36 +181,23 @@ module Prelude = struct
given symbol was polymorphic *)
let
logic_to_logic
lsymbol
=
if
ls_equal
lsymbol
ps_equ
||
ls_equal
lsymbol
ps_neq
then
lsymbol
else
let
new_ty
=
list_unique
$
List
.
filter
(
fun
x
->
is_tyvar
x
.
ty_node
)
lsymbol
.
ls_args
in
let
ty_vars
=
match
lsymbol
.
ls_value
with
(* do not forget result type *)
|
Some
t
->
t
::
lsymbol
.
ls_args
|
None
->
lsymbol
.
ls_args
in
let
new_ty
=
(
List
.
fold_left
find_tyvars
[]
ty_vars
)
in
(* as many t as type vars *)
if
new_ty
=
[]
then
lsymbol
(* same type *)
else
let
new_ty
=
List
.
map
(
fun
_
->
ty_app
t
[]
)
new_ty
in
let
new_ty
=
List
.
map
(
const
my_t
)
new_ty
in
let
all_new_ty
=
new_ty
@
lsymbol
.
ls_args
in
let
new_lsymbol
=
Term
.
create_lsymbol
(
id_clone
lsymbol
.
ls_name
)
all_new_ty
lsymbol
.
ls_value
in
new_lsymbol
Term
.
create_lsymbol
(
id_clone
lsymbol
.
ls_name
)
all_new_ty
lsymbol
.
ls_value
in
new_lsymbol
(** creates a lsymbol associated with the given ty
pe
*)
(** creates a lsymbol associated with the given ty
symbol
*)
let
type_to_logic
ty
=
let
my_t
=
ty_app
t
[]
in
let
name
=
id_clone
ty
.
ts_name
in
let
args
=
(
List
.
map
(
fun
_
->
my_t
)
ty
.
ts_args
)
in
let
new_lsymbol
=
Term
.
create_lsymbol
name
args
(
Some
my_t
)
in
new_lsymbol
(** [find_matching_vars tblT varM args_ty args_vars] matches [args_ty]
against [args_vars] to deduce a mapping from [args_vars] to lsymbols
through [tblT] and [varM] *)
let
find_matching_vars
_tblT
varM
args_ty
args_vars
=
let
tv_to_ty
=
Mtv
.
empty
in
let
mapping
=
List
.
fold_left2
ty_match
tv_to_ty
args_ty
args_vars
in
let
tv_to_lsymbol
=
Mtv
.
empty
in
(* result mapping *)
Mtv
.
fold
(
fun
key
value
acc
->
Mtv
.
add
key
(
Mty
.
find
value
varM
)
acc
)
mapping
tv_to_lsymbol
let
args
=
(
List
.
map
(
const
my_t
)
ty
.
ts_args
)
in
Term
.
create_lsymbol
name
args
(
Some
my_t
)
(** different finders *)
...
...
@@ -146,38 +205,77 @@ module Prelude = struct
let
findL
tbl
x
=
find_generic
logic_to_logic
tbl
x
let
findT
tbl
x
=
find_generic
type_to_logic
tbl
x
(** substitutions in formulae and terms *)
let
rec
term_transform
tblT
tblL
varM
t
=
match
t
.
t_node
with
(** {1 transformations} *)
(** transforms a type into another *)
let
rec
ty_to_ty
tv_to_ty
ty
=
match
ty
.
ty_node
with
|
Tyvar
x
->
(
try
Mtv
.
find
x
tv_to_ty
with
Not_found
->
ty
)
|
Tyapp
(
typ
,
tys
)
->
ty_app
typ
(
List
.
map
(
ty_to_ty
tv_to_ty
)
tys
)
(** transforms a type into a term (new args of polymorphic symbols) *)
let
rec
ty_to_term
tblT
varM
tv_to_ty
ty
=
match
ty
.
ty_node
with
|
Tyvar
x
->
let
new_ty
=
ty_to_ty
tv_to_ty
ty
in
begin
match
new_ty
.
ty_node
with
|
Tyvar
_
->
(* var -> var, stop there *)
assert
(
Mty
.
mem
new_ty
varM
);
t_var
(
Mty
.
find
new_ty
varM
)
|
Tyapp
_
->
(* recur *)
ty_to_term
tblT
varM
tv_to_ty
new_ty
end
|
Tyapp
(
typ
,
tys
)
->
assert
(
Hashtbl
.
mem
tblT
typ
);
(* nonsense otherwise *)
let
lsymbol
=
Hashtbl
.
find
tblT
typ
in
let
terms
=
List
.
map
(
ty_to_term
tblT
varM
tv_to_ty
)
tys
in
t_app
lsymbol
terms
my_t
(** translation of terms *)
let
rec
term_transform
tblT
tblL
varM
tv_to_ty
t
=
match
t
.
t_node
with
|
Tapp
(
f
,
terms
)
->
let
result_ty
=
fromSome
f
.
ls_value
in
let
new_f
=
(
findL
tblL
f
)
in
let
args_ty
=
List
.
map
(
fun
x
->
x
.
t_ty
)
terms
in
let
matched_terms
=
find_matching_vars
tblT
varM
args_ty
new_f
.
ls_args
in
let
new_terms
=
List
.
filter
(
fun
x
->
is_tyvar
x
.
ty_node
)
f
.
ls_args
in
let
new_terms
=
List
.
map
(
fun
x
->
match
x
.
ty_node
with
|
Tyvar
v
->
t_var
(
Mtv
.
find
v
matched_terms
)
|
_
->
failwith
"should find a mapping for this var"
)
new_terms
in
let
transformed_terms
=
List
.
map
(
term_transform
tblT
tblL
varM
)
terms
in
t_app
new_f
(
new_terms
@
transformed_terms
)
result_ty
let
new_f
=
findL
tblL
f
in
(* first, remember an order for type vars of new_f *)
let
type_vars
=
l_find_type_vars
new_f
in
Debug
.
print_list
Pretty
.
print_ty
Format
.
std_formatter
type_vars
;
let
int_to_tyvars
=
bind_nums_to_type_vars
new_f
in
(* match types *)
let
result_to_match
=
fromSome
new_f
.
ls_value
in
let
args_to_match
=
drop
(
List
.
length
type_vars
)
new_f
.
ls_args
in
let
concrete_ty
=
List
.
map
(
fun
x
->
x
.
t_ty
)
terms
in
let
tv_to_ty
=
find_matching_vars
tv_to_ty
(
result_to_match
::
args_to_match
)
(
t
.
t_ty
::
concrete_ty
)
in
Debug
.
print_mtv
Pretty
.
print_ty
Format
.
err_formatter
tv_to_ty
;
(* fresh terms to be added at the beginning of the list of arguments *)
let
new_ty_int
=
range
(
List
.
length
type_vars
)
in
let
new_ty
=
List
.
map
(
fun
x
->
Mint
.
find
x
int_to_tyvars
)
new_ty_int
in
let
new_terms
=
List
.
map
(
ty_to_term
tblT
varM
tv_to_ty
)
new_ty
in
let
transformed_terms
=
List
.
map
(
term_transform
tblT
tblL
varM
tv_to_ty
)
terms
in
let
transformed_result
=
ty_to_ty
tv_to_ty
(
fromSome
new_f
.
ls_value
)
in
t_app
new_f
(
new_terms
@
transformed_terms
)
transformed_result
|
_
->
(* default case : traverse *)
t_map
(
term_transform
tblT
tblL
varM
)
(
fmla_transform
tblT
tblL
varM
)
t
and
fmla_transform
tblT
tblL
varM
f
=
f_map
(
term_transform
tblT
tblL
varM
)
(
fmla_transform
tblT
tblL
varM
)
f
t_map
(
term_transform
tblT
tblL
varM
tv_to_ty
)
(
fmla_transform
tblT
tblL
varM
tv_to_ty
)
t
(** (trivial) translation of formulae *)
and
fmla_transform
tblT
tblL
varM
tv_to_ty
f
=
f_map
(
term_transform
tblT
tblL
varM
tv_to_ty
)
(
fmla_transform
tblT
tblL
varM
tv_to_ty
)
f
(** transforms a list of logic declarations into another
(** transforms a list of logic declarations into another.
Declares new lsymbols with explicit polymorphic signatures.
@param tbl hashtable used to memoize new lsymbols *)
let
logic_transform
tbl
decls
=
let
helper
=
function
|
(
lsymbol
,
Some
ldef
)
->
let
new_lsymbol
=
findL
tbl
lsymbol
in
(* new lsymbol *)
let
polymorphic_vars
=
list_unique
$
List
.
filter
(
fun
ty
->
match
ty
.
ty_node
with
Tyvar
_
->
true
|_->
false
)
lsymbol
.
ls_args
in
(* get unique type vars *)
let
polymorphic_vars
=
List
.
fold_left
find_tyvars
[]
lsymbol
.
ls_args
in
(* get unique type vars *)
let
vars
,
expr
=
open_ls_defn
ldef
in
let
new_vars
=
List
.
map
(
fun
_
->
Term
.
create_vsymbol
(
id_fresh
"t"
)
(
ty_app
t
[]
)
)
(
fun
_
->
Term
.
create_vsymbol
(
id_fresh
"t"
)
my_t
)
polymorphic_vars
in
(* new vars for polymorphism *)
let
vars
=
List
.
append
new_vars
vars
in
(* add new vars in signature *)
(
match
expr
with
...
...
@@ -193,56 +291,52 @@ module Prelude = struct
(** transforms a list of type declarations *)
let
type_transform
tbl
tys
=
let
helper
=
function
|
(
ty_symbol
,
Tabstract
)
->
let
new_lsymbol
=
findT
tbl
ty_symbol
in
(
new_lsymbol
,
None
)
|
_
->
failwith
"type_transform : no algebraic type should remain !"
in
let
cur_decl
=
List
.
map
helper
tys
in
[
Decl
.
create_ty_decl
tys
;
Decl
.
create_logic_decl
cur_decl
]
|
(
ty_symbol
,
Tabstract
)
->
(
findT
tbl
ty_symbol
,
None
)
|
_
->
failwith
"type_transform : no algebraic type should remain !"
in
let
cur_decl
=
List
.
map
helper
tys
in
[
Decl
.
create_ty_decl
tys
;
Decl
.
create_logic_decl
cur_decl
]
(** transforms a proposition into another (mostly a substitution) *)
let
prop_transform
tblT
tblL
(
prop_kind
,
prop_name
,
fmla
)
=
let
type_vars
=
list_unique
$
find_type_vars
[]
fmla
in
let
varM
=
List
.
fold_left
(
fun
m
x
->
Mty
.
add
x
(
create_vsymbol
(
id_fresh
"t"
)
(
ty_app
t
[]
))
m
)
Mty
.
empty
type_vars
in
[
Decl
.
create_prop_decl
prop_kind
prop_name
(
f_forall
(
map_values
varM
)
[]
(*universal quantification over ty vars*)
(
fmla_transform
tblT
tblL
varM
fmla
))]
let
type_vars
=
(
f_find_type_vars
[]
fmla
)
in
let
varM
=
List
.
fold_left
(* create a vsymbol for each type var *)
(
fun
m
x
->
Mty
.
add
x
(
create_vsymbol
(
id_fresh
"v"
)
my_t
)
m
)
Mty
.
empty
type_vars
in
Debug
.
print_mty
Pretty
.
print_vs
Format
.
err_formatter
varM
;
Format
.
eprintf
"-----------@."
;
(*universal quantification over ty vars*)
let
new_fmla
=
(
fmla_transform
tblT
tblL
varM
Mtv
.
empty
fmla
)
in
let
quantified_fmla
=
f_forall
(
map_values
varM
)
[]
new_fmla
in
[
Decl
.
create_prop_decl
prop_kind
prop_name
quantified_fmla
]
end
(** {2 main part} *)
(** utility to print a list of items *)
let
rec
print_list
printer
fmter
=
function
|
[]
->
()
|
e
::
es
->
Format
.
fprintf
fmter
"%a,@ %a"
printer
e
(
print_list
printer
)
es
(** main function, takes hashtables (for memoization of types and logic
symbols) and a declaration, and returns the corresponding declaration in
explicit polymorphism logic. *)
let
decl_transform
tblT
tblL
d
=
(*
Format.eprintf "%a@
" Pretty.print_decl d;
*)
Format
.
eprintf
"%a@
.
"
Pretty
.
print_decl
d
;
let
result
=
match
d
.
d_node
with
|
Dind
_inds
->
failwith
"Dind : should not have inductives declarations at this point !"
|
Dtype
tys
->
Prelude
.
type_transform
tblT
tys
|
Dlogic
decls
->
Prelude
.
logic_transform
tblL
decls
|
Dprop
prop
->
Prelude
.
prop_transform
tblT
tblL
prop
in
(*
Format.eprintf "
===
>
%a@." (print_list Pretty.print_decl) result;
*)
|
Dtype
tys
->
Transform
.
type_transform
tblT
tys
|
Dlogic
decls
->
Transform
.
logic_transform
tblL
decls
|
Dprop
prop
->
Transform
.
prop_transform
tblT
tblL
prop
in
Format
.
eprintf
"===
@.
%a@.
@.
"
(
Debug
.
print_list
Pretty
.
print_decl
)
result
;
result
(** the transformation to be registered. *)
(** the transformation to be registered.
It creates two new hashtables, used everywhere, which updates are
shared by side effects. *)
let
explicit_polymorphism
=
let
prelude_task
=
Task
.
add_decl
None
t_decl
in
(* declare t first *)
Register
.
store
(
fun
()
->
Trans
.
decl
(
decl_transform
(
Hashtbl
.
create
4
2
)
(
Hashtbl
.
create
42
))
prelude_task
)
(
decl_transform
(
Hashtbl
.
create
2
1
)
(
Hashtbl
.
create
42
))
prelude_task
)
let
()
=
Register
.
register_transform
"explicit_polymorphism"
explicit_polymorphism
"explicit_polymorphism"
explicit_polymorphism
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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