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
cduce
cduce
Commits
e89e9232
Commit
e89e9232
authored
Apr 28, 2014
by
Pietro Abate
Browse files
Fill gamma env in abstraction
parent
46de929d
Changes
1
Hide whitespace changes
Inline
Side-by-side
typing/typer.ml
View file @
e89e9232
...
...
@@ -51,7 +51,7 @@ type item =
type
t
=
{
ids
:
item
Env
.
t
;
delta
:
Var
.
Set
.
t
;
gamma
:
Var
.
var
Env
.
t
;
gamma
:
Types
.
Node
.
t
id_map
;
ns
:
Ns
.
table
;
keep_ns
:
bool
}
...
...
@@ -108,7 +108,7 @@ let type_schema env loc name uri =
let
empty_env
=
{
ids
=
Env
.
empty
;
delta
=
Var
.
Set
.
empty
;
(* set of bounded type variables *)
gamma
=
Env
.
empty
;
(* map from expression variables to types *)
gamma
=
IdMap
.
empty
;
(* map from expression variables to types *)
ns
=
Ns
.
def_table
;
keep_ns
=
false
}
...
...
@@ -874,17 +874,13 @@ and type_check' loc env ed constr precise = match ed with
ignore
(
type_check
env
e
t
false
);
(
ed
,
verify
loc
t
constr
)
(* TODO: Fix this branch *)
|
Subst
(
e
,
sigma
)
->
type_check
env
e
constr
precise
|
Subst
(
e
,
sigma
)
->
(
ed
,
type_check
env
e
constr
precise
)
|
Check
(
t0
,
e
,
t
)
->
let
te
=
type_check
env
e
Types
.
any
true
in
t0
:=
Types
.
cup
!
t0
te
;
(
ed
,
verify
loc
(
Types
.
cap
te
(
Types
.
descr
t
))
constr
)
|
Subst
(
e
,
sigma
)
->
(
ed
,
type_check
env
e
constr
precise
)
|
Abstraction
a
->
let
t
=
try
Types
.
Arrow
.
check_strenghten
a
.
fun_typ
constr
...
...
@@ -905,14 +901,14 @@ and type_check' loc env ed constr precise = match ed with
let
sigma
=
(* Tallying. su t2 *)
[]
in
(* p_j : t_j -> e^j_i sigma_{H_i} *)
List
.
iter
(
fun
br
->
br
.
body
.
exp_descr
<-
Subst
(
br
.
body
,
sigma
)
br
.
br_
body
.
exp_descr
<-
Subst
(
br
.
br_
body
,
sigma
)
)
a
.
fun_body
.
br_branches
)
a
.
fun_iface
;
(
ed
,
t
)
|
Match
(
e
,
b
)
->
let
t
=
type_check
env
e
b
.
br_accept
true
in
(
Match
(
e
.
exp_descr
,
b
)
,
type_check_branches
loc
env
t
b
constr
precise
)
(
ed
,
type_check_branches
loc
env
t
b
constr
precise
)
|
Try
(
e
,
b
)
->
let
te
=
type_check
env
e
constr
precise
in
...
...
@@ -1121,7 +1117,7 @@ and branches_aux loc env targ tres constr precise = function
b
.
br_used
<-
true
;
let
res
=
Patterns
.
filter
targ'
p
in
(* t_i // p_i *)
(* update gamma *)
let
env
=
{
env
with
gamma
=
IdMap
.
merge
env
.
gamma
res
}
in
let
env
=
{
env
with
gamma
=
IdMap
.
merge
(
fun
_
v2
->
v2
)
env
.
gamma
res
}
in
let
res
=
IdMap
.
map
Types
.
descr
res
in
b
.
br_vars_empty
<-
...
...
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