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
f5b0fbd2
Commit
f5b0fbd2
authored
May 19, 2010
by
Simon Cruanes
Browse files
small changes
parent
aef6cb4c
Changes
2
Hide whitespace changes
Inline
Sidebyside
src/manager/db.mli
View file @
f5b0fbd2
...
...
@@ 114,12 +114,12 @@ val transformations : goal > transf list
val
goal_proved
:
goal
>
bool
(** tells if the goal is proved valid or not.
It returns true iff either
<
li
>
exists proof p in [external_proofs g] s.t.
proof_obsolete p == false and status p = Valid
{ul {
li
exists proof p in [external_proofs g] s.t.
proof_obsolete p == false and status p = Valid
}}
or
<
li
>
exists transf t in [transformations g] s.t.
{ul {
li
exists transf t in [transformations g] s.t.
transf_obsolete t == false and
forall g in [subgoals t], [goal_proved g]
forall g in [subgoals t], [goal_proved g]
}}
*)
...
...
src/transform/explicit_polymorphism.ml
View file @
f5b0fbd2
...
...
@@ 29,42 +29,50 @@ open Term
open
Decl
open
Task
(** parenthesing operator *)
let
(
$
)
f
x
=
f
x
(** type representing types *)
let
t
=
Ty
.
create_tysymbol
(
id_fresh
"t"
)
[]
None
let
t_decl
=
Decl
.
create_ty_decl
[(
t
,
Tabstract
)]
(*s module to separate utilities from important functions *)
(** {2 module to separate utilities from important functions} *)
module
Prelude
=
struct
(** [find construct tbl id] searches for the
iden
t associated with
(** [find construct tbl id] searches for the
objec
t associated with
[id] in [tbl]. It creates it with [construct id] if it cannot find it. *)
let
find_generic
construct
tbl
id
=
try
Hashtbl
.
find
tbl
id
try
(
Hashtbl
.
find
tbl
id
,
[]
)
with
Not_found
>
let
new_image
=
construct
id
in
let
(
new_image
,
preliminary_decls
)
=
construct
id
in
Hashtbl
.
add
tbl
id
new_image
;
new_image
print_endline
"... done"
;
(
new_image
,
preliminary_decls
)
(** creates a new logic symbol, with a different type if the
given symbol was polymorphic *)
let
logic_to_logic
lsymbol
=
print_string
$
"logic_to_logic "
^
lsymbol
.
ls_name
.
id_string
;
let
replace
ty
=
match
ty
.
ty_node
with

Tyvar
_
>
ty_app
t
[]

_
>
ty
in
let
new_ty
=
List
.
map
replace
lsymbol
.
ls_args
in
Term
.
create
_lsymbol
(
id_clone
lsymbol
.
ls_name
)
new_ty
lsymbol
.
ls_value
let
new
_lsymbol
=
Term
.
create_lsymbol
(
id_clone
lsymbol
.
ls_name
)
new_ty
lsymbol
.
ls_value
in
(
new_
lsymbol
,
[
Decl
.
create_logic_decl
[
new_lsymbol
,
None
]])
(** creates a lsymbol associated with the given type *)
let
type_to_logic
ty
=
print_string
$
"type_to_logic "
^
ty
.
ts_name
.
id_string
;
let
my_t
=
ty_app
t
[]
in
let
name
=
"t"
in
let
name
=
id_clone
ty
.
ts_name
in
let
args
=
(
List
.
map
(
fun
_
>
my_t
)
ty
.
ts_args
)
in
let
lsymbol
=
Term
.
create
_lsymbol
(
id_fresh
name
)
args
(
Some
my_t
)
in
(
lsymbol
,
None
)
let
new
_lsymbol
=
Term
.
create_lsymbol
name
args
(
Some
my_t
)
in
(
new_lsymbol
,
[
Decl
.
create_logic_decl
[
new_
lsymbol
,
None
]]
)
(** different finders *)
...
...
@@ 76,7 +84,7 @@ module Prelude = struct
let
logic_transform
tbl
decls
=
let
helper
=
function

(
lsymbol
,
Some
ldef
)
>
let
new_lsymbol
=
findL
tbl
lsymbol
in
(* new lsymbol *)
let
(
new_lsymbol
,
more_decls
)
=
findL
tbl
lsymbol
in
(* new lsymbol *)
let
polymorphic_vars
=
List
.
filter
(
fun
ty
>
match
ty
.
ty_node
with
Tyvar
_
>
true
_>
false
)
lsymbol
.
ls_args
in
(* get polymorphic vars *)
...
...
@@ 85,39 +93,47 @@ module Prelude = struct
(
fun
_
>
Term
.
create_vsymbol
(
id_fresh
"t"
)
(
ty_app
t
[]
))
polymorphic_vars
in
(* new vars for polymorphism *)
let
vars
=
List
.
append
new_vars
vars
in
(* add new vars in signature *)
(
match
expr
with
(
(
match
expr
with

Term
t
>
Decl
.
make_fs_defn
new_lsymbol
vars
t

Fmla
f
>
Decl
.
make_ps_defn
new_lsymbol
vars
(
f_forall
new_vars
[]
f
))
,
more_decls
)
(* FIXME : is it useful / meaningful ? *)

(
lsymbol
,
None
)
>
let
new_lsymbol
=
findL
tbl
lsymbol
in
(
new_lsymbol
,
None
)
in
[
Decl
.
create_logic_decl
(
List
.
map
helper
decls
)]
let
(
new_lsymbol
,
more_decls
)
=
findL
tbl
lsymbol
in
((
new_lsymbol
,
None
)
,
more_decls
)
in
let
(
cur_decl
,
more_decls
)
=
List
.
split
(
List
.
map
helper
decls
)
in
(
List
.
concat
more_decls
)
@
[
Decl
.
create_logic_decl
cur_decl
]
(** transforms a list of type declarations *)
let
type_transform
tbl
tys
=
let
helper
=
function

(
ty_symbol
,
Tabstract
)
>
findT
tbl
ty_symbol

_
>
failwith
"type_transform : no algebraic type should remain !"
in
[
Decl
.
create_logic_decl
(
List
.
map
helper
tys
)]

(
ty_symbol
,
Tabstract
)
>
let
(
new_lsymbol
,
more_decls
)
=
findT
tbl
ty_symbol
in
((
new_lsymbol
,
None
)
,
more_decls
)

_
>
failwith
"type_transform : no algebraic type should remain !"
in
let
(
cur_decl
,
more_decls
)
=
List
.
split
(
List
.
map
helper
tys
)
in
Decl
.
create_ty_decl
tys
::
(
List
.
concat
more_decls
)
@
[
Decl
.
create_logic_decl
cur_decl
]
(** transforms a proposition into another (mostly a substitution) *)
let
prop_transform
_tblT
_tblL
fmla
=
failwith
"prop_transform : not implemented"
let
prop_transform
_tblT
_tblL
(
prop_kind
,
prop_name
,
fmla
)
=
[
Decl
.
create_prop_decl
prop_kind
prop_name
fmla
]
(* TODO : currently this is identity *)
end
(** {2 main part} *)
(** 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
=
match
d
.
d_node
with

Dind
_inds
>
failwith
"Dind : should not be here !"

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_kind
,
prop_name
,
fmla
)
>
[
Decl
.
create_prop_decl
prop_kind
prop_name
(
Prelude
.
prop_transform
tblT
tblL
fmla
)]

Dprop
prop
>
Prelude
.
prop_transform
tblT
tblL
prop
(** the transformation to be registered. *)
...
...
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