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
8d22557f
Commit
8d22557f
authored
Mar 18, 2010
by
Jean-Christophe Filliâtre
Browse files
menage dans Denv et Typing (les fonctions find sont maintenant celles de Theory)
parent
02b4a09b
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/parser/denv.ml
View file @
8d22557f
...
...
@@ -9,11 +9,7 @@ open Term
open
Theory
type
error
=
|
UnboundNamespace
of
string
|
UnboundType
of
string
|
UnboundSymbol
of
string
|
AnyMessage
of
string
|
TypeArity
of
qualid
*
int
*
int
exception
Error
of
error
...
...
@@ -21,33 +17,13 @@ let error ?loc e = match loc with
|
None
->
raise
(
Error
e
)
|
Some
loc
->
raise
(
Loc
.
Located
(
loc
,
Error
e
))
let
errorm
?
loc
f
=
let
buf
=
Buffer
.
create
512
in
let
fmt
=
Format
.
formatter_of_buffer
buf
in
Format
.
kfprintf
(
fun
_
->
Format
.
pp_print_flush
fmt
()
;
let
s
=
Buffer
.
contents
buf
in
Buffer
.
clear
buf
;
error
?
loc
(
AnyMessage
s
))
fmt
f
let
rec
print_qualid
fmt
=
function
|
Qident
s
->
fprintf
fmt
"%s"
s
.
id
|
Qdot
(
m
,
s
)
->
fprintf
fmt
"%a.%s"
print_qualid
m
s
.
id
let
report
fmt
=
function
|
UnboundNamespace
s
->
fprintf
fmt
"unbound namespace %s"
s
|
UnboundType
s
->
fprintf
fmt
"Unbound type '%s'"
s
|
UnboundSymbol
s
->
fprintf
fmt
"Unbound symbol '%s'"
s
|
AnyMessage
s
->
fprintf
fmt
"%s"
s
|
TypeArity
(
id
,
a
,
n
)
->
fprintf
fmt
"@[The type %a expects %d argument(s),@ "
print_qualid
id
a
;
fprintf
fmt
"but is applied to %d argument(s)@]"
n
(** types with destructive type variables *)
...
...
@@ -116,39 +92,13 @@ let rec ty_of_dty = function
|
Tyvar
{
type_val
=
Some
t
}
->
ty_of_dty
t
|
Tyvar
{
type_val
=
None
;
user
=
false
;
type_var_loc
=
loc
}
->
error
m
?
loc
"undefined type variable"
error
?
loc
(
AnyMessage
"undefined type variable"
)
|
Tyvar
{
tvsymbol
=
tv
}
->
Ty
.
ty_var
tv
|
Tyapp
(
s
,
tl
)
->
Ty
.
ty_app
s
(
List
.
map
ty_of_dty
tl
)
(** Destructive typing environment, that is
environment + local variables.
It is only local to this module and created with [create_denv] below. *)
type
denv
=
{
th
:
theory_uc
;
(* the theory under construction *)
utyvars
:
(
string
,
type_var
)
Hashtbl
.
t
;
(* user type variables *)
dvars
:
dty
Mstr
.
t
;
(* local variables, to be bound later *)
}
let
create_denv
th
=
{
th
=
th
;
utyvars
=
Hashtbl
.
create
17
;
dvars
=
Mstr
.
empty
;
}
let
find_user_type_var
x
env
=
try
Hashtbl
.
find
env
.
utyvars
x
with
Not_found
->
(* TODO: shouldn't we localize this ident? *)
let
v
=
create_tvsymbol
(
id_fresh
x
)
in
let
v
=
create_ty_decl_var
~
user
:
true
v
in
Hashtbl
.
add
env
.
utyvars
x
v
;
v
(* Specialize *)
let
find_type_var
~
loc
env
tv
=
...
...
@@ -165,90 +115,13 @@ let rec specialize ~loc env t = match t.ty_node with
|
Ty
.
Tyapp
(
s
,
tl
)
->
Tyapp
(
s
,
List
.
map
(
specialize
~
loc
env
)
tl
)
(** generic find function using a path *)
let
find_local_namespace
{
id
=
x
;
id_loc
=
loc
}
ns
=
try
Mnm
.
find
x
ns
.
ns_ns
with
Not_found
->
error
~
loc
(
UnboundNamespace
x
)
let
rec
find_namespace
q
ns
=
match
q
with
|
Qident
t
->
find_local_namespace
t
ns
|
Qdot
(
q
,
t
)
->
let
ns
=
find_namespace
q
ns
in
find_local_namespace
t
ns
let
rec
find
f
q
ns
=
match
q
with
|
Qident
x
->
f
x
ns
|
Qdot
(
m
,
x
)
->
let
ns
=
find_namespace
m
ns
in
f
x
ns
(** specific find functions using a path *)
let
find_local_tysymbol
{
id
=
x
;
id_loc
=
loc
}
ns
=
try
Mnm
.
find
x
ns
.
ns_ts
with
Not_found
->
error
~
loc
(
UnboundType
x
)
let
find_tysymbol_ns
p
ns
=
find
find_local_tysymbol
p
ns
let
find_tysymbol
p
th
=
find_tysymbol_ns
p
(
get_namespace
th
)
let
find_lsymbol
{
id
=
x
;
id_loc
=
loc
}
ns
=
try
Mnm
.
find
x
ns
.
ns_ls
with
Not_found
->
error
~
loc
(
UnboundSymbol
x
)
let
find_lsymbol_ns
p
ns
=
find
find_lsymbol
p
ns
let
find_lsymbol
p
th
=
find_lsymbol_ns
p
(
get_namespace
th
)
let
find_prop
{
id
=
x
;
id_loc
=
loc
}
ns
=
try
Mnm
.
find
x
ns
.
ns_pr
with
Not_found
->
errorm
~
loc
"unbound formula %s"
x
let
find_prop_ns
p
ns
=
find
find_prop
p
ns
let
find_prop
p
th
=
find_prop_ns
p
(
get_namespace
th
)
(** specialize functions *)
let
specialize_tysymbol
~
loc
x
env
=
let
s
=
find_tysymbol
x
env
.
th
in
let
specialize_tysymbol
~
loc
s
=
let
env
=
Htv
.
create
17
in
s
,
List
.
map
(
find_type_var
~
loc
env
)
s
.
ts_args
List
.
map
(
find_type_var
~
loc
env
)
s
.
ts_args
let
specialize_lsymbol
~
loc
s
=
let
tl
=
s
.
ls_args
in
let
t
=
s
.
ls_value
in
let
env
=
Htv
.
create
17
in
s
,
List
.
map
(
specialize
~
loc
env
)
tl
,
option_map
(
specialize
~
loc
env
)
t
(* parsed types -> intermediate types *)
let
rec
qloc
=
function
|
Qident
x
->
x
.
id_loc
|
Qdot
(
m
,
x
)
->
Loc
.
join
(
qloc
m
)
x
.
id_loc
let
rec
type_inst
s
ty
=
match
ty
.
ty_node
with
|
Ty
.
Tyvar
n
->
Mtv
.
find
n
s
|
Ty
.
Tyapp
(
ts
,
tyl
)
->
Tyapp
(
ts
,
List
.
map
(
type_inst
s
)
tyl
)
let
rec
dty
env
=
function
|
PPTtyvar
{
id
=
x
}
->
Tyvar
(
find_user_type_var
x
env
)
|
PPTtyapp
(
p
,
x
)
->
let
loc
=
qloc
x
in
let
ts
,
tv
=
specialize_tysymbol
~
loc
x
env
in
let
np
=
List
.
length
p
in
let
a
=
List
.
length
tv
in
if
np
<>
a
then
error
~
loc
(
TypeArity
(
x
,
a
,
np
));
let
tyl
=
List
.
map
(
dty
env
)
p
in
match
ts
.
ts_def
with
|
None
->
Tyapp
(
ts
,
tyl
)
|
Some
ty
->
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
let
s
=
List
.
fold_left2
add
Mtv
.
empty
ts
.
ts_args
tyl
in
type_inst
s
ty
List
.
map
(
specialize
~
loc
env
)
tl
,
option_map
(
specialize
~
loc
env
)
t
src/parser/denv.mli
View file @
8d22557f
...
...
@@ -18,40 +18,15 @@ val unify : dty -> dty -> bool
val
print_dty
:
Format
.
formatter
->
dty
->
unit
(** Destructive environments *)
type
denv
=
{
th
:
theory_uc
;
(* the theory under construction *)
utyvars
:
(
string
,
type_var
)
Hashtbl
.
t
;
(* user type variables *)
dvars
:
dty
Mstr
.
t
;
(* local variables, to be bound later *)
}
val
create_denv
:
theory_uc
->
denv
val
dty
:
denv
->
Ptree
.
pty
->
dty
val
ty_of_dty
:
dty
->
ty
(** Lookup *)
val
find_tysymbol_ns
:
Ptree
.
qualid
->
namespace
->
tysymbol
val
find_lsymbol_ns
:
Ptree
.
qualid
->
namespace
->
lsymbol
val
find_prop_ns
:
Ptree
.
qualid
->
namespace
->
Decl
.
prop
val
find_tysymbol
:
Ptree
.
qualid
->
theory_uc
->
tysymbol
val
find_lsymbol
:
Ptree
.
qualid
->
theory_uc
->
lsymbol
val
find_prop
:
Ptree
.
qualid
->
theory_uc
->
Decl
.
prop
(** Specialization *)
val
specialize_tysymbol
:
loc
:
Ptree
.
loc
->
Ptree
.
qualid
->
denv
->
Ty
.
tysymbol
*
type_var
list
loc
:
Ptree
.
loc
->
tysymbol
->
type_var
list
val
specialize_lsymbol
:
loc
:
Ptree
.
loc
->
lsymbol
->
lsymbol
*
dty
list
*
dty
option
loc
:
Ptree
.
loc
->
lsymbol
->
dty
list
*
dty
option
(** Error reporting *)
...
...
src/parser/typing.ml
View file @
8d22557f
...
...
@@ -50,6 +50,8 @@ type error =
|
NotInLoadpath
of
string
|
CyclicTypeDef
|
UnboundTypeVar
of
string
|
UnboundType
of
string
list
|
UnboundSymbol
of
string
list
|
AnyMessage
of
string
exception
Error
of
error
...
...
@@ -112,6 +114,10 @@ let report fmt = function
fprintf
fmt
"cyclic type definition"
|
UnboundTypeVar
s
->
fprintf
fmt
"unbound type variable '%s"
s
|
UnboundType
sl
->
fprintf
fmt
"Unbound type '%a'"
(
print_list
dot
pp_print_string
)
sl
|
UnboundSymbol
sl
->
fprintf
fmt
"Unbound symbol '%a'"
(
print_list
dot
pp_print_string
)
sl
|
AnyMessage
s
->
fprintf
fmt
"%s"
s
...
...
@@ -133,20 +139,33 @@ let term_expected_type ~loc ty1 ty2 =
"@[This term has type %a@ but is expected to have type@ %a@]"
print_dty
ty1
print_dty
ty2
let
specialize_fsymbol
~
loc
s
=
let
s
,
tl
,
ty
=
specialize_lsymbol
~
loc
s
in
match
ty
with
|
None
->
error
~
loc
TermExpected
|
Some
ty
->
s
,
tl
,
ty
(** Destructive typing environment, that is
environment + local variables.
It is only local to this module and created with [create_denv] below. *)
let
specialize_psymbol
~
loc
s
=
let
s
,
tl
,
ty
=
specialize_lsymbol
~
loc
s
in
match
ty
with
|
None
->
s
,
tl
|
Some
_
->
error
~
loc
PredicateExpected
type
denv
=
{
uc
:
theory_uc
;
(* the theory under construction *)
utyvars
:
(
string
,
type_var
)
Hashtbl
.
t
;
(* user type variables *)
dvars
:
dty
Mstr
.
t
;
(* local variables, to be bound later *)
}
let
create_denv
uc
=
{
uc
=
uc
;
utyvars
=
Hashtbl
.
create
17
;
dvars
=
Mstr
.
empty
;
}
(** Typing types *)
let
find_user_type_var
x
env
=
try
Hashtbl
.
find
env
.
utyvars
x
with
Not_found
->
(* TODO: shouldn't we localize this ident? *)
let
v
=
create_tvsymbol
(
id_fresh
x
)
in
let
v
=
create_ty_decl_var
~
user
:
true
v
in
Hashtbl
.
add
env
.
utyvars
x
v
;
v
(* parsed types -> intermediate types *)
let
rec
qloc
=
function
|
Qident
x
->
x
.
id_loc
...
...
@@ -156,6 +175,72 @@ let rec string_list_of_qualid acc = function
|
Qident
id
->
id
.
id
::
acc
|
Qdot
(
p
,
id
)
->
string_list_of_qualid
(
id
.
id
::
acc
)
p
let
specialize_tysymbol
loc
p
uc
=
let
sl
=
string_list_of_qualid
[]
p
in
let
ts
=
try
ns_find_ts
(
get_namespace
uc
)
sl
with
Not_found
->
error
~
loc
(
UnboundType
sl
)
in
ts
,
specialize_tysymbol
~
loc
ts
let
rec
type_inst
s
ty
=
match
ty
.
ty_node
with
|
Ty
.
Tyvar
n
->
Mtv
.
find
n
s
|
Ty
.
Tyapp
(
ts
,
tyl
)
->
Tyapp
(
ts
,
List
.
map
(
type_inst
s
)
tyl
)
let
rec
dty
env
=
function
|
PPTtyvar
{
id
=
x
}
->
Tyvar
(
find_user_type_var
x
env
)
|
PPTtyapp
(
p
,
x
)
->
let
loc
=
qloc
x
in
let
ts
,
tv
=
specialize_tysymbol
loc
x
env
.
uc
in
let
np
=
List
.
length
p
in
let
a
=
List
.
length
tv
in
if
np
<>
a
then
error
~
loc
(
TypeArity
(
x
,
a
,
np
));
let
tyl
=
List
.
map
(
dty
env
)
p
in
match
ts
.
ts_def
with
|
None
->
Tyapp
(
ts
,
tyl
)
|
Some
ty
->
let
add
m
v
t
=
Mtv
.
add
v
t
m
in
let
s
=
List
.
fold_left2
add
Mtv
.
empty
ts
.
ts_args
tyl
in
type_inst
s
ty
let
find_ns
find
p
ns
=
let
loc
=
qloc
p
in
let
sl
=
string_list_of_qualid
[]
p
in
try
find
ns
sl
with
Not_found
->
error
~
loc
(
UnboundSymbol
sl
)
let
find_prop_ns
=
find_ns
ns_find_prop
let
find_prop
p
uc
=
find_prop_ns
p
(
get_namespace
uc
)
let
find_tysymbol_ns
=
find_ns
ns_find_ts
let
find_tysymbol
q
uc
=
find_tysymbol_ns
q
(
get_namespace
uc
)
let
find_lsymbol_ns
=
find_ns
ns_find_ls
let
find_lsymbol
q
uc
=
find_lsymbol_ns
q
(
get_namespace
uc
)
let
specialize_lsymbol
p
uc
=
let
s
=
find_lsymbol
p
uc
in
s
,
specialize_lsymbol
(
qloc
p
)
s
let
specialize_fsymbol
p
uc
=
let
loc
=
qloc
p
in
let
s
,
(
tl
,
ty
)
=
specialize_lsymbol
p
uc
in
match
ty
with
|
None
->
error
~
loc
TermExpected
|
Some
ty
->
s
,
tl
,
ty
let
specialize_psymbol
p
uc
=
let
loc
=
qloc
p
in
let
s
,
(
tl
,
ty
)
=
specialize_lsymbol
p
uc
in
match
ty
with
|
None
->
s
,
tl
|
Some
_
->
error
~
loc
PredicateExpected
(** Typing types *)
let
split_qualid
=
function
|
Qident
id
->
[]
,
id
.
id
|
Qdot
(
p
,
id
)
->
string_list_of_qualid
[]
p
,
id
.
id
...
...
@@ -209,7 +294,8 @@ let binop = function
let
check_pat_linearity
pat
=
let
s
=
ref
Sstr
.
empty
in
let
add
id
=
if
Sstr
.
mem
id
.
id
!
s
then
errorm
~
loc
:
id
.
id_loc
"duplicate variable %s"
id
.
id
;
if
Sstr
.
mem
id
.
id
!
s
then
errorm
~
loc
:
id
.
id_loc
"duplicate variable %s"
id
.
id
;
s
:=
Sstr
.
add
id
.
id
!
s
in
let
rec
check
p
=
match
p
.
pat_desc
with
...
...
@@ -235,8 +321,7 @@ and dpat_node loc env = function
let
env
=
{
env
with
dvars
=
Mstr
.
add
x
ty
env
.
dvars
}
in
env
,
Pvar
x
,
ty
|
PPpapp
(
x
,
pl
)
->
let
s
=
find_lsymbol
x
env
.
th
in
let
s
,
tyl
,
ty
=
specialize_fsymbol
~
loc
s
in
let
s
,
tyl
,
ty
=
specialize_fsymbol
x
env
.
uc
in
let
env
,
pl
=
dpat_args
s
.
ls_name
loc
env
tyl
pl
in
env
,
Papp
(
s
,
pl
)
,
ty
|
PPpas
(
p
,
{
id
=
x
})
->
...
...
@@ -285,14 +370,12 @@ and dterm_node loc env = function
Tvar
x
,
ty
|
PPvar
x
->
(* 0-arity symbol (constant) *)
let
s
=
find_lsymbol
x
env
.
th
in
let
s
,
tyl
,
ty
=
specialize_fsymbol
~
loc
s
in
let
s
,
tyl
,
ty
=
specialize_fsymbol
x
env
.
uc
in
let
n
=
List
.
length
tyl
in
if
n
>
0
then
error
~
loc
(
BadNumberOfArguments
(
s
.
ls_name
,
0
,
n
));
Tapp
(
s
,
[]
)
,
ty
|
PPapp
(
x
,
tl
)
->
let
s
=
find_lsymbol
x
env
.
th
in
let
s
,
tyl
,
ty
=
specialize_fsymbol
~
loc
s
in
let
s
,
tyl
,
ty
=
specialize_fsymbol
x
env
.
uc
in
let
tl
=
dtype_args
s
.
ls_name
loc
env
tyl
tl
in
Tapp
(
s
,
tl
)
,
ty
|
PPconst
(
ConstInt
_
as
c
)
->
...
...
@@ -374,8 +457,7 @@ and dfmla env e = match e.pp_desc with
in
Fquant
(
q
,
uqu
,
trl
,
dfmla
env
a
)
|
PPapp
(
x
,
tl
)
->
let
s
=
find_lsymbol
x
env
.
th
in
let
s
,
tyl
=
specialize_psymbol
~
loc
:
e
.
pp_loc
s
in
let
s
,
tyl
=
specialize_psymbol
x
env
.
uc
in
let
tl
=
dtype_args
s
.
ls_name
e
.
pp_loc
env
tyl
tl
in
Fapp
(
s
,
tl
)
|
PPlet
({
id
=
x
}
,
e1
,
e2
)
->
...
...
@@ -399,7 +481,7 @@ and dfmla env e = match e.pp_desc with
let
f1
=
dfmla
env
f1
in
Fnamed
(
x
,
f1
)
|
PPvar
x
->
Fvar
(
snd
(
find_prop
x
env
.
th
))
Fvar
(
snd
(
find_prop
x
env
.
uc
))
|
PPconst
_
|
PPcast
_
->
error
~
loc
:
e
.
pp_loc
PredicateExpected
...
...
@@ -653,7 +735,7 @@ let add_logics dl th =
|
Some
id
->
{
denv
with
dvars
=
Mstr
.
add
id
.
id
(
dty
denv
ty
)
denv
.
dvars
}
in
let
denv
=
Hashtbl
.
find
denvs
id
in
let
denv
=
{
denv
with
th
=
th'
}
in
let
denv
=
{
denv
with
uc
=
th'
}
in
let
denv
=
List
.
fold_left
dadd_var
denv
d
.
ld_params
in
let
create_var
(
x
,
_
)
ty
=
let
id
=
match
x
with
...
...
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