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
d5b4d685
Commit
d5b4d685
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-03-23 21:09:48 by cvscast] Empty log message
Original author: cvscast Date: 2003-03-23 21:09:49+00:00
parent
5d2625ae
Changes
5
Hide whitespace changes
Inline
Side-by-side
driver/cduce.ml
View file @
d5b4d685
...
...
@@ -4,7 +4,6 @@ open Ident
let
quiet
=
ref
false
let
typing_env
=
State
.
ref
"Cduce.typing_env"
Typer
.
Env
.
empty
let
glb_env
=
State
.
ref
"Cduce.glb_env"
Typer
.
TypeEnv
.
empty
let
eval_env
=
Eval
.
global_env
let
print_norm
ppf
d
=
...
...
@@ -15,9 +14,9 @@ let print_value ppf v =
Location
.
protect
ppf
(
fun
ppf
->
Value
.
print
ppf
v
)
let
dump_env
ppf
=
Format
.
fprintf
ppf
"Global types:"
;
Typer
.
TypeEnv
.
iter
(
fun
x
_
->
Format
.
fprintf
ppf
" %s"
x
)
!
glb_env
;
Format
.
fprintf
ppf
".@
\n
"
;
(*
Format.fprintf ppf "Global types:";
List
.iter (fun x _ -> Format.fprintf ppf " %s" x)
(Typer.global_types ());
Format.fprintf ppf ".@\n";
*)
Eval
.
Env
.
iter
(
fun
x
v
->
let
t
=
Typer
.
Env
.
find
x
!
typing_env
in
...
...
@@ -83,23 +82,23 @@ let rec print_exn ppf = function
let
debug
ppf
=
function
|
`Subtype
(
t1
,
t2
)
->
Format
.
fprintf
ppf
"[DEBUG:subtype]@
\n
"
;
let
t1
=
Types
.
descr
(
Typer
.
typ
!
glb_env
t1
)
and
t2
=
Types
.
descr
(
Typer
.
typ
!
glb_env
t2
)
in
let
t1
=
Types
.
descr
(
Typer
.
typ
t1
)
and
t2
=
Types
.
descr
(
Typer
.
typ
t2
)
in
Format
.
fprintf
ppf
"%a <= %a : %b@
\n
"
print_norm
t1
print_norm
t2
(
Types
.
subtype
t1
t2
)
|
`Filter
(
t
,
p
)
->
Format
.
fprintf
ppf
"[DEBUG:filter]@
\n
"
;
let
t
=
Typer
.
typ
!
glb_env
t
and
p
=
Typer
.
pat
!
glb_env
p
in
let
t
=
Typer
.
typ
t
and
p
=
Typer
.
pat
p
in
let
f
=
Patterns
.
filter
(
Types
.
descr
t
)
p
in
List
.
iter
(
fun
(
x
,
t
)
->
Format
.
fprintf
ppf
" %s:%a@
\n
"
(
Id
.
value
x
)
print_norm
(
Types
.
descr
t
))
f
|
`Compile2
(
t
,
pl
)
->
Format
.
fprintf
ppf
"[DEBUG:compile2]@
\n
"
;
(* let t = Types.descr (Typer.typ
!glb_env
t) in
(* let t = Types.descr (Typer.typ t) in
let pl = List.map (fun p ->
let p = Typer.pat
!glb_env
p in
let p = Typer.pat p in
let a = Types.descr (Patterns.accept p) in
(Some p, Types.cap a t)) pl in
let d = Patterns.Compiler.make_dispatcher t pl in
...
...
@@ -108,13 +107,13 @@ let debug ppf = function
|
`Accept
p
->
Format
.
fprintf
ppf
"[DEBUG:accept]@
\n
"
;
let
p
=
Typer
.
pat
!
glb_env
p
in
let
p
=
Typer
.
pat
p
in
let
t
=
Patterns
.
accept
p
in
Format
.
fprintf
ppf
" %a@
\n
"
Types
.
Print
.
print
t
|
`Compile
(
t
,
pl
)
->
Format
.
fprintf
ppf
"[DEBUG:compile]@
\n
"
;
let
t
=
Typer
.
typ
!
glb_env
t
and
pl
=
List
.
map
(
Typer
.
pat
!
glb_env
)
pl
in
let
t
=
Typer
.
typ
t
and
pl
=
List
.
map
Typer
.
pat
pl
in
Patterns
.
Compile
.
debug_compile
ppf
t
pl
|
`Normal_record
p
->
assert
false
...
...
@@ -123,7 +122,7 @@ let debug ppf = function
let
mk_builtin
()
=
let
bi
=
List
.
map
(
fun
(
n
,
t
)
->
[
n
,
mknoloc
(
Ast
.
Internal
t
)])
Builtin
.
types
in
glb_env
:=
List
.
fold_left
Typer
.
register_global_types
!
glb_env
bi
List
.
iter
Typer
.
register_global_types
bi
let
()
=
mk_builtin
()
...
...
@@ -153,7 +152,7 @@ let run ppf ppf_err input =
let
phrase
ph
=
match
ph
.
descr
with
|
Ast
.
EvalStatement
e
->
let
(
fv
,
e
)
=
Typer
.
expr
!
glb_env
e
in
let
(
fv
,
e
)
=
Typer
.
expr
e
in
let
t
=
Typer
.
type_check
!
typing_env
e
Types
.
any
true
in
Location
.
dump_loc
ppf
e
.
Typed
.
exp_loc
;
if
not
!
quiet
then
...
...
@@ -163,7 +162,7 @@ let run ppf ppf_err input =
Format
.
fprintf
ppf
"=> @[%a@]@
\n
@."
print_value
v
|
Ast
.
LetDecl
(
p
,
{
descr
=
Ast
.
Abstraction
_
})
->
()
|
Ast
.
LetDecl
(
p
,
e
)
->
let
decl
=
Typer
.
let_decl
!
glb_env
p
e
in
let
decl
=
Typer
.
let_decl
p
e
in
type_decl
decl
;
eval_decl
decl
|
Ast
.
TypeDecl
_
->
()
...
...
@@ -172,7 +171,7 @@ let run ppf ppf_err input =
in
let
do_fun_decls
decls
=
let
decls
=
List
.
map
(
fun
(
p
,
e
)
->
Typer
.
let_decl
!
glb_env
p
e
)
decls
in
let
decls
=
List
.
map
(
fun
(
p
,
e
)
->
Typer
.
let_decl
p
e
)
decls
in
insert_type_bindings
(
Typer
.
type_rec_funs
!
typing_env
decls
);
List
.
iter
eval_decl
decls
in
...
...
@@ -201,7 +200,7 @@ let run ppf ppf_err input =
(
typs
,
(
p
,
e
)
::
funs
)
|
_
->
accu
)
([]
,
[]
)
p
in
glb_env
:=
Typer
.
register_global_types
!
glb_env
type_decls
;
Typer
.
register_global_types
type_decls
;
phrases
[]
p
;
true
with
...
...
driver/cduce.mli
View file @
d5b4d685
...
...
@@ -2,7 +2,6 @@ val quiet: bool ref
val
typing_env
:
Typer
.
env
ref
(* Types of toplevel bindings *)
val
eval_env
:
Eval
.
env
ref
(* Values of toplevel bindings *)
val
glb_env
:
Typer
.
glb
ref
(* Global types *)
val
print_exn
:
Format
.
formatter
->
exn
->
unit
...
...
parser/ast.ml
View file @
d5b4d685
...
...
@@ -149,3 +149,10 @@ and hash_regexp = function
|
Star
x
->
5
+
17
*
(
hash_regexp
x
)
|
WeakStar
x
->
6
+
17
*
(
hash_regexp
x
)
|
SeqCapture
(
x
,
y
)
->
7
+
17
*
(
Id
.
hash
x
)
+
257
*
(
hash_regexp
y
)
module
PpatTable
=
Hashtbl
.
Make
(
struct
type
t
=
ppat
let
equal
=
equal_ppat
let
hash
=
hash_ppat
end
)
typing/typer.ml
View file @
d5b4d685
(* TODO:
- rewrite type-checking of operators to propagate constraint
- rewrite translation of types and patterns -> hash cons
CONTINUE THIS...
Problem with same name for recursive binders in different
recursive type/patterns definitions because of hash-consing
*)
...
...
@@ -12,11 +15,10 @@ open Ast
open
Ident
module
S
=
struct
type
t
=
string
let
compare
=
compare
end
module
StringSet
=
Set
.
Make
(
S
)
module
TypeEnv
=
Map
.
Make
(
S
)
module
Env
=
Map
.
Make
(
Ident
.
Id
)
(*
module StringSet = Set.Make(S)
*)
exception
NonExhaustive
of
Types
.
descr
exception
Constraint
of
Types
.
descr
*
Types
.
descr
*
string
...
...
@@ -26,55 +28,6 @@ exception UnboundId of string
let
raise_loc
loc
exn
=
raise
(
Location
(
loc
,
exn
))
(* Internal representation as a graph (desugar recursive types and regexp),
to compute freevars, etc... *)
type
ti
=
{
id
:
int
;
mutable
seen
:
bool
;
mutable
loc'
:
loc
;
mutable
fv
:
fv
option
;
mutable
descr'
:
descr
;
mutable
type_node
:
Types
.
node
option
;
mutable
pat_node
:
Patterns
.
node
option
}
and
descr
=
|
IAlias
of
string
*
ti
|
IType
of
Types
.
descr
|
IOr
of
ti
*
ti
|
IAnd
of
ti
*
ti
|
IDiff
of
ti
*
ti
|
ITimes
of
ti
*
ti
|
IXml
of
ti
*
ti
|
IArrow
of
ti
*
ti
|
IOptional
of
ti
|
IRecord
of
bool
*
ti
label_map
|
ICapture
of
id
|
IConstant
of
id
*
Types
.
const
type
glb
=
ti
TypeEnv
.
t
let
mk'
=
let
counter
=
ref
0
in
fun
loc
->
incr
counter
;
let
rec
x
=
{
id
=
!
counter
;
seen
=
false
;
loc'
=
loc
;
fv
=
None
;
descr'
=
IAlias
(
"__dummy__"
,
x
);
type_node
=
None
;
pat_node
=
None
}
in
x
let
cons
loc
d
=
let
x
=
mk'
loc
in
x
.
descr'
<-
d
;
x
(* Note:
Compilation of Regexp is implemented as a ``rewriting'' of
the parsed syntax, in order to be able to print its result
...
...
@@ -183,6 +136,7 @@ module Regexp = struct
defs
:=
[]
;
mk_loc
!
re_loc
(
Recurs
(
n
,
d
))
(*
module H = Hashtbl.Make(
struct
type t = Ast.regexp * Ast.ppat
...
...
@@ -204,9 +158,338 @@ module Regexp = struct
let c = compile loc regexp queue in
H.add hash (regexp,queue) c;
c
*)
end
let
compile_regexp
=
Regexp
.
compile
noloc
(*
type descr =
| IType of Types.descr
| IOr of descr * descr
| IAnd of descr * descr
| IDiff of descr * descr
| ITimes of slot * slot
| IXml of slot * slot
| IArrow of slot * slot
| IOptional of slot descr
| IRecord of bool * slot label_map
| ICapture of id
| IConstant of id * Types.const
and slot = {
mutable fv : fv option;
mutable hash : int option;
mutable rank1: int; mutable rank2: int;
mutable gen1 : int; mutable gen2: int;
mutable d : slot descr option
}
let descr s =
match s.d with
| Some d -> d
| None -> assert false
let gen = ref 0
let rank = ref 0
let rec hash_descr = function
| IType x -> Types.hash_descr x
| IOr (d1,d2) -> 1 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IAnd (d1,d2) -> 2 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IDiff (d1,d2) -> 3 + 17 * (hash_descr d1) + 257 * (hash_descr d2)
| IOptional d -> 4 + 17 * (hash_descr d)
| ITimes (s1,s2) -> 5 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IXml (s1,s2) -> 6 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IArrow (s1,s2) -> 7 + 17 * (hash_slot s1) + 257 * (hash_slot s2)
| IRecord (o,r) -> (if o then 8 else 9) + 17 * (LabelMap.hash hash_slot r)
| ICapture x -> 10 + 17 * (Id.hash x)
| IConstant (x,y) -> 11 + 17 * (Id.hash x) + 257 * (Types.hash_const y)
and hash_slot s =
if s.gen1 = !gen then 13 * s.rank1
else (
incr rank;
s.rank1 <- !rank; s.gen1 <- !gen;
hash_descr (descr s)
)
let rec equal_descr d1 d2 =
(d1 == d2) ||
match (d1,d2) with
| IType x1, IType x2 -> Types.equal_descr x1 x2
| IOr (x1,y1), IOr (x2,y2)
| IAnd (x1,y1), IAnd (x2,y2)
| IDiff (x1,y1), IDiff (x2,y2) -> (equal_descr x1 x2) && (equal_descr y1 y2)
| IOptional x1, IOptional x2 -> equal_descr x1 x2
| ITimes (x1,y1), ITimes (x2,y2)
| IXml (x1,y1), IXml (x2,y2)
| IArrow (x1,y1), IArrow (x2,y2) -> (equal_slot x1 x2) && (equal_slot y1 y2)
| IRecord (o1,r1), IRecord (o2,r2) -> (o1 = o2) && (LabelMap.equal equal_slot r1 r2)
| ICapture x1, ICapture x2 -> Id.equal x1 x2
| IConstant (x1,y1), IConstant (x2,y2) -> (Id.equal x1 x2) && (Types.equal_const y1 y2)
| _ -> false
and equal_slot s1 s2 =
((s1.gen1 = !gen) && (s2.gen2 = !gen) && (s1.rank1 = s2.rank2))
||
((s1.gen1 <> !gen) && (s2.gen2 <> !gen) && (
incr rank;
s1.rank1 <- !rank; s1.gen1 <- !gen;
s2.rank2 <- !rank; s2.gen2 <- !gen;
equal_descr (descr s1) (descr s2)
))
module Arg = struct
type t = slot
let hash s =
match s.hash with
| Some h -> h
| None ->
incr gen; rank := 0;
let h = hash_slot s in
s.hash <- Some h;
h
let equal s1 s2 = incr gen; rank := 0; equal_slot s1 s2
end
module SlotTable = Hashtbl.Make(Arg)
let rec fv_slot s =
match s.fv with
| Some x -> x
| None ->
if s.gen1 = !gen then IdSet.empty
else (s.gen1 <- !gen; fv_descr (descr s))
and fv_descr = function
| IOr (d1,d2)
| IAnd (d1,d2)
| IDiff (d1,d2) -> IdSet.cup (fv_descr d1) (fv_descr d2)
| IOptional d -> fv_descr d
| ITimes (s1,s2)
| IXml (s1,s2)
| IArrow (s1,s2) -> IdSet.cup (fv_slot s1) (fv_slot s2)
| IRecord (o,r) -> List.fold_left IdSet.cup IdSet.empty (LabelMap.map_to_list fv_slot r)
| ICapture x | IConstant (x,_) -> IdSet.singleton x
| _ -> IdSet.empty
let compute_fv s =
match s.fv with
| Some x -> ()
| None ->
incr gen;
let x = fv_slot s in
s.fv <- Some x
let counter = ref 0
let todo = ref []
let rec flush_fv () =
List.iter compute_fv !todo;
todo := []
let mk () =
let s =
{ d = None;
fv = None;
hash = None;
rank1 = 0; rank2 = 0;
gen1 = 0; gen2 = 0 } in
todo := s :: !todo;
s
let compile_hash = Ast.PpatTable.create 65
let defs = ref []
let rec compile env { loc = loc; descr = d } =
match (d : Ast.ppat') with
| PatVar v ->
let (d,loop) =
try TypeEnv.find v env
with Not_found ->
raise_loc_generic loc ("Undefined type variable " ^ v) in
if !loop then
raise_loc_generic loc ("Unguarded recursion on type/pattern variable " ^ v);
loop := true;
let r = compile env d in
loop := false;
r
| Recurs (t, b) -> compile (compile_many env b) t
| Regexp (r,q) -> compile env (Regexp.compile loc r q)
| Internal t -> IType t
| Or (t1,t2) -> IOr (compile env t1, compile env t2)
| And (t1,t2) -> IAnd (compile env t1, compile env t2)
| Diff (t1,t2) -> IDiff (compile env t1, compile env t2)
| Prod (t1,t2) -> ITimes (compile_slot env t1, compile_slot env t2)
| XmlT (t1,t2) -> IXml (compile_slot env t1, compile_slot env t2)
| Arrow (t1,t2) -> IArrow (compile_slot env t1, compile_slot env t2)
| Optional t -> IOptional (compile env t)
| Record (o,r) -> IRecord (o, LabelMap.map (compile_slot env) r)
| Constant (x,v) -> IConstant (x,v)
| Capture x -> ICapture x
and compile_slot env ({ loc = loc; descr = d } as p) =
try Ast.PpatTable.find compile_hash p
with Not_found ->
let s = mk () in
defs := (s,p,env) :: !defs;
Ast.PpatTable.add compile_hash p s;
s
and compile_many env b =
List.fold_left (fun env (v,p) -> TypeEnv.add v (p,ref false) env) env b
let rec flush_defs () =
match !defs with
| [] -> ()
| (s,p,env)::t -> defs := t; s.d <- Some (compile env p); flush_defs ()
let typ_nodes = SlotTable.create 67
let pat_nodes = SlotTable.create 67
let rec typ = function
| IType t -> t
| IOr (s1,s2) -> Types.cup (typ s1) (typ s2)
| IAnd (s1,s2) -> Types.cap (typ s1) (typ s2)
| IDiff (s1,s2) -> Types.diff (typ s1) (typ s2)
| ITimes (s1,s2) -> Types.times (typ_node s1) (typ_node s2)
| IXml (s1,s2) -> Types.xml (typ_node s1) (typ_node s2)
| IArrow (s1,s2) -> Types.arrow (typ_node s1) (typ_node s2)
| IOptional s -> Types.Record.or_absent (typ s)
| IRecord (o,r) -> Types.record' (o, LabelMap.map typ_node r)
| ICapture x | IConstant (x,_) -> assert false
and typ_node s : Types.node =
try SlotTable.find typ_nodes s
with Not_found ->
let x = Types.make () in
SlotTable.add typ_nodes s x;
Types.define x (typ (descr s));
x
let rec pat d : Patterns.descr =
if IdSet.is_empty (fv_descr d)
then Patterns.constr (typ d)
else pat_aux d
and pat_aux = function
| IOr (s1,s2) -> Patterns.cup (pat s1) (pat s2)
| IAnd (s1,s2) -> Patterns.cap (pat s1) (pat s2)
| IDiff (s1,s2) when IdSet.is_empty (fv_descr s2) ->
let s2 = Types.neg (typ s2) in
Patterns.cap (pat s1) (Patterns.constr s2)
| IDiff _ ->
raise (Patterns.Error "Difference not allowed in patterns")
| ITimes (s1,s2) -> Patterns.times (pat_node s1) (pat_node s2)
| IXml (s1,s2) -> Patterns.xml (pat_node s1) (pat_node s2)
| IOptional _ ->
raise (Patterns.Error "Optional field not allowed in record patterns")
| IRecord (o,r) ->
let pats = ref [] in
let aux l s =
if IdSet.is_empty (fv_slot s) then typ_node s
else
( pats := Patterns.record l (pat_node s) :: !pats;
Types.any_node )
in
let constr = Types.record' (o,LabelMap.mapi aux r) in
List.fold_left Patterns.cap (Patterns.constr constr) !pats
(* TODO: can avoid constr when o=true, and all fields have fv *)
| ICapture x -> Patterns.capture x
| IConstant (x,c) -> Patterns.constant x c
| IArrow _ ->
raise (Patterns.Error "Arrow not allowed in patterns")
| IType _ -> assert false
and pat_node s : Patterns.node =
try SlotTable.find pat_nodes s
with Not_found ->
let x = Patterns.make (fv_slot s) in
SlotTable.add pat_nodes s x;
Patterns.define x (pat (descr s));
x
let glb = State.ref "Typer.glb_env" TypeEnv.empty
let register_global_types b =
List.iter (fun (v, { loc = loc }) ->
if TypeEnv.mem v !glb
then raise_loc_generic loc ("Multiple definition for type " ^ v)
) b;
glb := compile_many !glb b;
let b = List.map (fun (v,p) -> (v,p,compile !glb p)) b in
flush_defs ();
flush_fv ();
List.iter (fun (v,p,s) ->
if not (IdSet.is_empty (fv_descr s)) then
raise_loc_generic p.loc "Capture variables are not allowed in types";
Types.Print.register_global v (typ s)) b
let typ p =
let s = compile_slot !glb p in
flush_defs ();
flush_fv ();
if IdSet.is_empty (fv_slot s) then typ_node s
else raise_loc_generic p.loc "Capture variables are not allowed in types"
let pat p =
let s = compile_slot !glb p in
flush_defs ();
flush_fv ();
try pat_node s
with Patterns.Error e -> raise_loc_generic p.loc e
| Location (loc,exn) when loc = noloc -> raise (Location (p.loc, exn))
*)
(* Internal representation as a graph (desugar recursive types and regexp),
to compute freevars, etc... *)
type
ti
=
{
id
:
int
;
mutable
seen
:
bool
;
mutable
loc'
:
loc
;
mutable
fv
:
fv
option
;
mutable
descr'
:
descr
;
mutable
type_node
:
Types
.
node
option
;
mutable
pat_node
:
Patterns
.
node
option
}
and
descr
=
|
IAlias
of
string
*
ti
|
IType
of
Types
.
descr
|
IOr
of
ti
*
ti
|
IAnd
of
ti
*
ti
|
IDiff
of
ti
*
ti
|
ITimes
of
ti
*
ti
|
IXml
of
ti
*
ti
|
IArrow
of
ti
*
ti
|
IOptional
of
ti
|
IRecord
of
bool
*
ti
label_map
|
ICapture
of
id
|
IConstant
of
id
*
Types
.
const
type
glb
=
ti
TypeEnv
.
t
let
mk'
=
let
counter
=
ref
0
in
fun
loc
->
incr
counter
;
let
rec
x
=
{
id
=
!
counter
;
seen
=
false
;
loc'
=
loc
;
fv
=
None
;
descr'
=
IAlias
(
"__dummy__"
,
x
);
type_node
=
None
;
pat_node
=
None
}
in
x
let
cons
loc
d
=
let
x
=
mk'
loc
in
x
.
descr'
<-
d
;
x
let
rec
compile
env
{
loc
=
loc
;
descr
=
d
}
:
ti
=
...
...
@@ -376,24 +659,26 @@ let mk_typ e =
else
raise_loc_generic
e
.
loc'
"Capture variables are not allowed in types"
let
typ
glb
e
=
mk_typ
(
compile
glb
e
)
let
glb
=
State
.
ref
"Typer.glb_env"
TypeEnv
.
empty
let
typ
e
=
mk_typ
(
compile
!
glb
e
)
let
pat
glb
e
=
pat_node
(
compile
glb
e
)
let
pat
e
=
pat_node
(
compile
!
glb
e
)
let
register_global_types
glb
b
=
let
env'
=
compile_many
glb
b
in
List
.
fold_left
(
fun
glb
(
v
,
{
loc
=
loc
})
->
let
register_global_types
b
=
let
env'
=
compile_many
!
glb
b
in
List
.
iter
(
fun
(
v
,
{
loc
=
loc
})
->
let
t
=
TypeEnv
.
find
v
env'
in
let
d
=
Types
.
descr
(
mk_typ
t
)
in
(* let d = Types.normalize d in*)
Types
.
Print
.
register_global
v
d
;
if
TypeEnv
.
mem
v
glb
if
TypeEnv
.
mem
v
!
glb
then
raise_loc_generic
loc
(
"Multiple definition for type "
^
v
);
TypeEnv
.
add
v
t
glb
)
glb
b
glb
:=
TypeEnv
.
add
v
t
!
glb
)
b
...
...
@@ -404,19 +689,19 @@ module Fv = IdSet
(* IDEA: introduce a node Loc in the AST to override nolocs
in sub-expressions *)
let
rec
expr
loc'
glb
{
loc
=
loc
;
descr
=
d
}
=
let
rec
expr
loc'
{
loc
=
loc
;
descr
=
d
}
=
let
loc
=
if
loc
=
noloc
then
loc'
else
loc
in
let
(
fv
,
td
)
=
match
d
with
|
Forget
(
e
,
t
)
->
let
(
fv
,
e
)
=
expr
loc
glb
e
and
t
=
typ
glb
t
in
let
(
fv
,
e
)
=
expr
loc
e
and
t
=
typ
t
in
(
fv
,
Typed
.
Forget
(
e
,
t
))
|
Var
s
->
(
Fv
.
singleton
s
,
Typed
.
Var
s
)
|
Apply
(
e1
,
e2
)
->
let
(
fv1
,
e1
)
=
expr
loc
glb
e1
and
(
fv2
,
e2
)
=
expr
loc
glb
e2
in
let
(
fv1
,
e1
)
=
expr
loc
e1
and
(
fv2
,
e2
)
=
expr
loc
e2
in
(
Fv
.
cup
fv1
fv2
,
Typed
.
Apply
(
e1
,
e2
))
|
Abstraction
a
->
let
iface
=
List
.
map
(
fun
(
t1
,
t2
)
->
(
typ
glb
t1
,
typ
glb
t2
))
let
iface
=
List
.
map
(
fun
(
t1
,
t2
)
->
(
typ
t1
,
typ
t2
))
a
.
fun_iface
in
let
t
=
List
.
fold_left
(
fun
accu
(
t1
,
t2
)
->
Types
.
cap
accu
(
Types
.
arrow
t1
t2
))
...
...
@@ -424,7 +709,7 @@ let rec expr loc' glb { loc = loc; descr = d } =
let
iface
=
List
.
map
(
fun
(
t1
,
t2
)
->
(
Types
.
descr
t1
,
Types
.
descr
t2
))
iface
in
let
(
fv0
,
body
)
=
branches
loc
glb
a
.
fun_body
in
let
(
fv0
,
body
)
=
branches
loc
a
.
fun_body
in
let
fv
=
match
a
.
fun_name
with
|
None
->
fv0
|
Some
f
->
Fv
.
remove
f
fv0
in
...
...
@@ -439,46 +724,46 @@ let rec expr loc' glb { loc = loc; descr = d } =
)
|
Cst
c
->
(
Fv
.
empty
,
Typed
.
Cst
c
)
|
Pair
(
e1
,
e2
)
->
let
(
fv1
,
e1
)
=
expr
loc
glb
e1
and
(
fv2
,
e2
)
=
expr
loc
glb
e2
in
let
(
fv1
,
e1
)
=
expr
loc
e1
and
(
fv2
,
e2
)
=
expr
loc
e2
in
(
Fv
.
cup
fv1
fv2
,
Typed
.
Pair
(
e1
,
e2
))