From b7472a31c0463d228d2a7a820251f5a5bd753922 Mon Sep 17 00:00:00 2001
From: butterunderflow <azhong.934@gmail.com>
Date: Sun, 4 Aug 2024 22:03:41 +0800
Subject: [PATCH 1/2] use an map to hint module expression of module type id
---
lib/typing/check.ml | 71 +++----
lib/typing/env.ml | 22 ++-
lib/typing/render.ml | 39 ++--
lib/typing/report.ml | 15 +-
tests/cram/test_dirs/list.t/run.t | 275 ++++++++++++++--------------
tests/cram/test_dirs/simple.t/run.t | 12 +-
tests/regular/render_typed_test.ml | 203 ++++++++++----------
tests/regular/typing_test.ml | 4 +-
8 files changed, 339 insertions(+), 302 deletions(-)
diff --git a/lib/typing/check.ml b/lib/typing/check.ml
index 4303cee..ceaf580 100644
--- a/lib/typing/check.ml
+++ b/lib/typing/check.ml
@@ -50,7 +50,7 @@ let rec check_expr (e : T.expr) (env : Env.t) : expr =
| T.ESeq (e0, e1) -> check_seq e0 e1 env
with
| U.UnificationError (t0, t1) ->
- Report.unification_error t0 t1 e.start_loc e.end_loc
+ Report.unification_error t0 t1 e.start_loc e.end_loc env
| U.OccurError (tv, te) -> Report.occur_error tv te e.start_loc e.end_loc
| e -> raise e
@@ -374,6 +374,7 @@ and make_mt_by_scope
module_dict = _;
curr;
history;
+ hints = _;
} =
I.MTMod
{
@@ -387,38 +388,42 @@ and make_mt_by_scope
}
and check_mod (me : T.mod_expr) (env : Env.t) : mod_expr =
- match me.node with
- | T.MEName name -> MEName (name, Env.lookup_module_def name env)
- | T.MEStruct body ->
- let body_typed, env' = check_top_levels body (Env.enter_env env) in
- let scope = absorb_history env' env in
- let mt = make_mt_by_scope scope in
- MEStruct (body_typed, mt)
- | T.MEFunctor ((name, ext_mt0), me1) ->
- let mt0 = normalize_mt ext_mt0 env in
- let me1_typed = check_mod me1 (Env.add_module name mt0 env) in
- MEFunctor ((name, mt0), me1_typed)
- | T.MEField (me, name) -> (
- let me_typed = check_mod me env in
- match get_mod_ty me_typed with
- | I.MTMod { mod_defs; _ } ->
- MEField (me_typed, name, List.assoc name mod_defs)
- | I.MTFun _ -> failwith "try get field from functor")
- | T.MEApply (me0, me1) -> (
- let me0_typed = check_mod me0 env in
- let me1_typed = check_mod me1 env in
- let mt0 = get_mod_ty me0_typed in
- let mt1 = get_mod_ty me1_typed in
- match mt0 with
- | I.MTMod _ -> failwith "try apply a structure"
- | I.MTFun (para_mt, body_mt) ->
- MEApply
- (me0_typed, me1_typed, apply_functor para_mt body_mt mt1 env))
- | T.MERestrict (me, mt) ->
- let me_typed = check_mod me env in
- let mt = normalize_mt mt env in
- let _subst = check_subtype (get_mod_ty me_typed) mt in
- MERestrict (me_typed, mt, shift_mt mt env)
+ let me_typed =
+ match me.node with
+ | T.MEName name -> MEName (name, Env.lookup_module_def name env)
+ | T.MEStruct body ->
+ let body_typed, env' = check_top_levels body (Env.enter_env env) in
+ let scope = absorb_history env' env in
+ let mt = make_mt_by_scope scope in
+ MEStruct (body_typed, mt)
+ | T.MEFunctor ((name, ext_mt0), me1) ->
+ let mt0 = normalize_mt ext_mt0 env in
+ let me1_typed = check_mod me1 (Env.add_module name mt0 env) in
+ MEFunctor ((name, mt0), me1_typed)
+ | T.MEField (me, name) -> (
+ let me_typed = check_mod me env in
+ match get_mod_ty me_typed with
+ | I.MTMod { mod_defs; _ } ->
+ MEField (me_typed, name, List.assoc name mod_defs)
+ | I.MTFun _ -> failwith "try get field from functor")
+ | T.MEApply (me0, me1) -> (
+ let me0_typed = check_mod me0 env in
+ let me1_typed = check_mod me1 env in
+ let mt0 = get_mod_ty me0_typed in
+ let mt1 = get_mod_ty me1_typed in
+ match mt0 with
+ | I.MTMod _ -> failwith "try apply a structure"
+ | I.MTFun (para_mt, body_mt) ->
+ MEApply
+ (me0_typed, me1_typed, apply_functor para_mt body_mt mt1 env))
+ | T.MERestrict (me, mt) ->
+ let me_typed = check_mod me env in
+ let mt = normalize_mt mt env in
+ let _subst = check_subtype (get_mod_ty me_typed) mt in
+ MERestrict (me_typed, mt, shift_mt mt env)
+ in
+ Env.try_record_hint me_typed env;
+ me_typed
(* apply a functor, add returned module type's id into environment *)
and apply_functor para_mt body_mt arg_mt env =
diff --git a/lib/typing/env.ml b/lib/typing/env.ml
index 7f7bb5e..5acb6b7 100644
--- a/lib/typing/env.ml
+++ b/lib/typing/env.ml
@@ -1,4 +1,5 @@
module I = Types_in
+module T = Typedtree
type scope = {
values : (string * I.bind_ty) list;
@@ -9,7 +10,8 @@ type scope = {
module_dict : (int * I.mod_ty) list;
(* UNUSED FIELD: designed for caching module id to their definition *)
curr : int;
- history : int list ref;
+ history : int list ref; (* module ids created in this scope *)
+ hints : (int * T.mod_expr) list ref;
}
type t = scope list
@@ -72,6 +74,15 @@ let record_history id (env : t) =
| [] -> failwith "neverreach"
| s :: _ -> s.history := id :: !(s.history)
+let try_record_hint me_typed (env : t) =
+ match env with
+ | [] -> failwith "neverreach"
+ | s :: _ -> (
+ let mt = T.get_mod_ty me_typed in
+ match mt with
+ | I.MTMod { id; _ } -> s.hints := (id, me_typed) :: !(s.hints)
+ | _ -> ())
+
let record_all_history ids (env : t) =
match env with
| [] -> failwith "neverreach"
@@ -119,6 +130,14 @@ let rec lookup_type_def tn env =
| Some def -> (s.curr, def)
| None -> lookup_type_def tn env')
+let rec lookup_hint id env =
+ match env with
+ | [] -> None
+ | s :: env' -> (
+ match List.assoc_opt id !(s.hints) with
+ | None -> lookup_hint id env'
+ | Some me -> Some me)
+
let get_curr env =
match env with
| s :: _ -> s.curr
@@ -134,6 +153,7 @@ let init_scope () =
module_dict = [];
curr = 0;
history = ref [];
+ hints = ref [];
}
let init () = [ init_scope () ]
diff --git a/lib/typing/render.ml b/lib/typing/render.ml
index 9999f73..b09cee6 100644
--- a/lib/typing/render.ml
+++ b/lib/typing/render.ml
@@ -174,7 +174,7 @@ module MakePP (Config : PPConfig) = struct
Fmt.fprintf fmt "@]@])")
else content_printer ()
- and pp_mod fmt me =
+ and pp_mod fmt ?(env : Env.t option) me =
match me with
| MEName (name, _) -> Fmt.pp_print_string fmt name
| MEStruct (tops, mt) ->
@@ -192,19 +192,19 @@ module MakePP (Config : PPConfig) = struct
Fmt.fprintf fmt "@[<v 2>functor (%s : " name;
pp_mod_ty fmt mt;
Fmt.fprintf fmt ")@\n-> @\n";
- pp_mod fmt me;
+ pp_mod fmt ?env me;
Fmt.fprintf fmt "@]"
| MEField (me, name, _) ->
Fmt.fprintf fmt "@[";
- pp_mod fmt me;
+ pp_mod fmt ?env me;
Fmt.fprintf fmt ".%s" name;
Fmt.fprintf fmt "@]"
| MEApply (me0, me1, mt) ->
pp_is_mod_ty fmt Config.show_mod_ty
(fun _ ->
- pp_mod fmt me0;
+ pp_mod fmt ?env me0;
Fmt.fprintf fmt "(";
- pp_mod fmt me1;
+ pp_mod fmt ?env me1;
Fmt.fprintf fmt ")")
mt
| MERestrict (me, mt, mt') ->
@@ -212,7 +212,7 @@ module MakePP (Config : PPConfig) = struct
(fun _ ->
Fmt.fprintf fmt "(";
Fmt.fprintf fmt "@[";
- pp_mod fmt me;
+ pp_mod fmt ?env me;
Fmt.fprintf fmt " : ";
Fmt.fprintf fmt "@[";
pp_mod_ty fmt mt;
@@ -298,12 +298,12 @@ module MakePP (Config : PPConfig) = struct
pp_ty fmt te;
Fmt.fprintf fmt "@]"
- and pp_ty fmt te =
+ and pp_ty fmt ?env te =
match te with
| I.TConsI ((id, name), tes) ->
Fmt.fprintf fmt "@[";
(match tes with
- | [] -> Fmt.fprintf fmt "()"
+ | [] -> Fmt.fprintf fmt "()@ "
| te0 :: tes ->
Fmt.fprintf fmt "(";
pp_ty fmt te0;
@@ -312,8 +312,14 @@ module MakePP (Config : PPConfig) = struct
Fmt.fprintf fmt ",@ ";
pp_ty fmt te)
tes;
- Fmt.fprintf fmt ")");
- Fmt.fprintf fmt "@ %d.%s" id name;
+ Fmt.fprintf fmt ")@ ");
+ (match (Option.bind env (Env.lookup_hint id), id) with
+ | Some me, _ ->
+ pp_mod fmt ?env me;
+ Fmt.fprintf fmt "."
+ | None, 0 (* 0 is default root module's structure type id *) -> ()
+ | None, _ -> Fmt.fprintf fmt "%d." id);
+ Fmt.fprintf fmt "%s" name;
Fmt.fprintf fmt "@]"
| I.TVarI { contents = I.Unbound tv } ->
Fmt.fprintf fmt "{%s}" (Ident.show_ident tv)
@@ -455,10 +461,10 @@ module MakePP (Config : PPConfig) = struct
prog;
Format.pp_print_flush fmt ()
- let pp_str_of_ty ty =
+ let pp_str_of_ty ?env ty =
let buf = Buffer.create 10 in
let formatter = Fmt.formatter_of_buffer buf in
- pp_ty formatter ty;
+ pp_ty formatter ?env ty;
Fmt.pp_print_flush formatter ();
Buffer.contents buf
end
@@ -471,7 +477,16 @@ module ShowAllConfig : PPConfig = struct
let show_mod_ty = true
end
+module ShowNothingConfig : PPConfig = struct
+ let show_const_ty = false
+
+ let show_bind_ty = false
+
+ let show_mod_ty = false
+end
+
module DefaultPP = MakePP (ShowAllConfig)
+module NoTypeHintPP = MakePP (ShowNothingConfig)
let default_dbg prog =
let buf = Buffer.create 50 in
diff --git a/lib/typing/report.ml b/lib/typing/report.ml
index 04b1a65..7e00cbf 100644
--- a/lib/typing/report.ml
+++ b/lib/typing/report.ml
@@ -1,15 +1,16 @@
module T = Types_in
-module PP = Render.DefaultPP
+module PP = Render.NoTypeHintPP
type err =
| UnificationError of (T.ty * T.ty * Lexing.position * Lexing.position)
(* error reportings *)
(* todo: support error tolerable type checking *)
-exception UnificationError of T.ty * T.ty * Lexing.position * Lexing.position
+exception
+ UnificationError of T.ty * T.ty * Lexing.position * Lexing.position * Env.t
-let unification_error t0 t1 loc1 loc2 =
- raise (UnificationError (t0, t1, loc1, loc2))
+let unification_error t0 t1 loc1 loc2 env =
+ raise (UnificationError (t0, t1, loc1, loc2, env))
exception ComponentInCompatible of string * T.bind_ty * T.bind_ty
@@ -33,10 +34,10 @@ let unknown_location () = Printf.printf "At some unknown location: "
let wrap_with_error_report f =
try Some (f ()) with
- | UnificationError (t0, t1, start, last) ->
+ | UnificationError (t0, t1, start, last, env) ->
print_code_range start last;
- Printf.printf "Can't unify `%s` with `%s`" (PP.pp_str_of_ty t0)
- (PP.pp_str_of_ty t1);
+ Printf.printf "Can't unify `%s` with `%s`" (PP.pp_str_of_ty ~env t0)
+ (PP.pp_str_of_ty ~env t1);
None
| OccurError (tv, te, start, last) ->
print_code_range start last;
diff --git a/tests/cram/test_dirs/list.t/run.t b/tests/cram/test_dirs/list.t/run.t
index 2dd4572..e8e6a82 100644
--- a/tests/cram/test_dirs/list.t/run.t
+++ b/tests/cram/test_dirs/list.t/run.t
@@ -4,180 +4,173 @@
$ cat test_list.typed
- external println_int : (() 0.int
- ->() 0.unit)= "ff_builtin_println_int"
+ external println_int : (() int
+ ->() unit)= "ff_builtin_println_int"
- external println_string : (() 0.string
- ->() 0.unit)= "ff_builtin_println_str"
+ external println_string : (() string
+ ->() unit)= "ff_builtin_println_str"
- external add : (() 0.int
- ->(() 0.int
- ->() 0.int))= "ff_builtin_add"
+ external add : (() int
+ ->(() int
+ ->() int))= "ff_builtin_add"
type ('a/0) list =
| Cons of (['a/0]
- * (['a/0]) 0.list)
+ * (['a/0]) list)
| Nil
let cons = fun x ->
fun y ->
(Cons[0] is (({{'_t/1}}
- * ({{'_t/1}}) 0.list)
- ->({{'_t/1}}) 0.list)) ((x is {'_t/1}), (y is {({{'_t/1}})
- 0.list}))
-
- let lst = (cons is ({() 0.int}
- ->(({() 0.int}) 0.list
- ->({() 0.int}) 0.list))) (3 is () 0.int) (cons is (
- {() 0.int}
- ->(
- ({
- () 0.int})
- 0.list
- ->
- ({
- () 0.int})
- 0.list))) (
- 2 is () 0.int) (cons is ({() 0.int}
- ->(({() 0.int}) 0.list
- ->({() 0.int}) 0.list))) (1 is () 0.int) (
- Nil[1] is ({() 0.int}) 0.list)
+ * ({{'_t/1}}) list)
+ ->({{'_t/1}}) list)) ((x is {'_t/1}), (y is {({{'_t/1}})
+ list}))
+
+ let lst = (cons is ({() int}
+ ->(({() int}) list
+ ->({() int}) list))) (3 is () int) (cons is (
+ {() int}
+ ->(({() int})
+ list
+ ->({
+ () int})
+ list))) (
+ 2 is () int) (cons is ({() int}
+ ->(({() int}) list
+ ->({() int}) list))) (1 is () int) (Nil[1] is
+ ({() int})
+ list)
let rec iter = fun lst ->
fun f ->
- match (lst is {({{'_t/20}}) 0.list}) with
+ match (lst is {({{'_t/20}}) list}) with
| (Cons[0]
((x is {'_t/20})
- * (lst is {({{'_t/20}}) 0.list}))) ->
+ * (lst is {({{'_t/20}}) list}))) ->
(f is {({'_t/20}
- ->{() 0.unit})}) (x is {'_t/20}) ;
- (iter is {(({'_t/20}) 0.list
+ ->{() unit})}) (x is {'_t/20}) ;
+ (iter is {(({'_t/20}) list
->{(({'_t/20}
- ->() 0.unit)
- ->{{() 0.unit}})})}) (lst is ({'_t/20})
- 0.list) (
+ ->() unit)
+ ->{{() unit}})})}) (lst is ({'_t/20})
+ list) (
f is ({'_t/20}
- ->() 0.unit))
- | Nil -> (() is () 0.unit)
+ ->() unit))
+ | Nil -> (() is () unit)
let print_int_lst = fun lst ->
- (iter is (({() 0.int}) 0.list
- ->(({() 0.int}
- ->() 0.unit)
- ->() 0.unit))) (lst is {({() 0.int}) 0.list}) (println_int is (
- () 0.int
- ->() 0.unit))
+ (iter is (({() int}) list
+ ->(({() int}
+ ->() unit)
+ ->() unit))) (lst is {({() int}) list}) (println_int is (
+ () int
+ ->() unit))
- let result = (print_int_lst is ((() 0.int) 0.list
- ->() 0.unit)) (lst is (() 0.int) 0.list)
+ let result = (print_int_lst is ((() int) list
+ ->() unit)) (lst is (() int) list)
let rec map = fun lst ->
fun f ->
- match (lst is {({{'_t/36}}) 0.list}) with
- | (Cons[0]
- ((x is {'_t/36})
- * (lst is {({{'_t/36}}) 0.list}))) ->
+ match (lst is {({{'_t/36}}) list}) with
+ | (Cons[0] ((x is {'_t/36})
+ * (lst is {({{'_t/36}}) list}))) ->
(cons is ({{'ret/39}}
- ->(({{'ret/39}}) 0.list
- ->({{'ret/39}}) 0.list))) (f is {({'_t/36}
- ->{'ret/39})}) (
- x is {'_t/36}) (map is {(({'_t/36}) 0.list
+ ->(({{'ret/39}}) list
+ ->({{'ret/39}}) list))) (f is {({'_t/36}
+ ->{'ret/39})}) (
+ x is {'_t/36}) (map is {(({'_t/36}) list
->{(({'_t/36}
->{'ret/39})
- ->{({{'ret/39}}) 0.list})})}) (
- lst is ({'_t/36}) 0.list) (f is ({'_t/36}
- ->{'ret/39}))
- | Nil -> (Nil[1] is ({{'ret/39}}) 0.list)
-
- let result = (print_int_lst is ((() 0.int) 0.list
- ->() 0.unit)) (map is (({() 0.int}) 0.list
- ->(({() 0.int}
- ->{() 0.int})
- ->({() 0.int})
- 0.list))) (
- lst is (() 0.int) 0.list) (add is (() 0.int
- ->(() 0.int
- ->() 0.int))) (7 is () 0.int)
-
- let lst = (cons is ({(() 0.int
- * () 0.int)}
- ->(({(() 0.int
- * () 0.int)}) 0.list
- ->({(() 0.int
- * () 0.int)}) 0.list))) ((2 is () 0.int), (
- 4 is () 0.int)) (cons is ({(() 0.int
- * () 0.int)}
- ->(({(() 0.int
- * () 0.int)}) 0.list
- ->({(() 0.int
- * () 0.int)}) 0.list))) ((1 is () 0.int), (
- 2 is () 0.int)) (Nil[1] is ({(() 0.int
- * () 0.int)}) 0.list)
+ ->{({{'ret/39}}) list})})}) (
+ lst is ({'_t/36}) list) (f is ({'_t/36}
+ ->{'ret/39}))
+ | Nil -> (Nil[1] is ({{'ret/39}}) list)
+
+ let result = (print_int_lst is ((() int) list
+ ->() unit)) (map is (({() int}) list
+ ->(({() int}
+ ->{() int})
+ ->({() int}) list))) (
+ lst is (() int) list) (add is (() int
+ ->(() int
+ ->() int))) (7 is () int)
+
+ let lst = (cons is ({(() int
+ * () int)}
+ ->(({(() int
+ * () int)}) list
+ ->({(() int
+ * () int)}) list))) ((2 is () int), (4 is
+ () int)) (
+ cons is ({(() int
+ * () int)}
+ ->(({(() int
+ * () int)}) list
+ ->({(() int
+ * () int)}) list))) ((1 is () int), (2 is () int)) (
+ Nil[1] is ({(() int
+ * () int)}) list)
let print_int_tu = fun tu ->
- match (tu is {({() 0.int}
- * {() 0.int})}) with
- | ((x is {() 0.int})
- * (y is {() 0.int})) ->
- (println_int is (() 0.int
- ->() 0.unit)) (x is {() 0.int}) ;
- (println_int is (() 0.int
- ->() 0.unit)) (y is {() 0.int})
+ match (tu is {({() int}
+ * {() int})}) with
+ | ((x is {() int})
+ * (y is {() int})) ->
+ (println_int is (() int
+ ->() unit)) (x is {() int}) ;
+ (println_int is (() int
+ ->() unit)) (y is {() int})
let print_int_tu_lst = fun lst ->
- (iter is (({(() 0.int
- * () 0.int)}) 0.list
- ->(({(() 0.int
- * () 0.int)}
- ->() 0.unit)
- ->() 0.unit))) (lst is {({(() 0.int
- * () 0.int)}) 0.list}) (
- print_int_tu is ((() 0.int
- * () 0.int)
- ->() 0.unit))
-
- let result = (print_int_tu_lst is (((() 0.int
- * () 0.int)) 0.list
- ->() 0.unit)) (lst is ((() 0.int
- * () 0.int))
- 0.list)
+ (iter is (({(() int
+ * () int)}) list
+ ->(({(() int
+ * () int)}
+ ->() unit)
+ ->() unit))) (lst is {({(() int
+ * () int)}) list}) (print_int_tu is (
+ (() int
+ * () int)
+ ->() unit))
+
+ let result = (print_int_tu_lst is (((() int
+ * () int)) list
+ ->() unit)) (lst is ((() int
+ * () int))
+ list)
let tu_adder = fun tu ->
- match (tu is {({() 0.int}
- * {() 0.int})}) with
- | ((x is {() 0.int})
- * (y is {() 0.int})) ->
- ((add is (() 0.int
- ->(() 0.int
- ->() 0.int))) (x is {() 0.int}) (1 is () 0.int), (add is (
- () 0.int
- ->(
- () 0.int
- ->
- () 0.int))) (
- y is {() 0.int}) (1 is () 0.int))
-
- let result = (print_int_tu_lst is (((() 0.int
- * () 0.int)) 0.list
- ->() 0.unit)) (map is (({(() 0.int
- * () 0.int)})
- 0.list
- ->(({(() 0.int
- *
- () 0.int)}
- ->{(
- () 0.int
- * () 0.int)})
- ->({(
- () 0.int
- *
- () 0.int)})
- 0.list))) (
- lst is ((() 0.int
- * () 0.int)) 0.list) (tu_adder is ((() 0.int
- * () 0.int)
- ->(() 0.int
- * () 0.int)))
+ match (tu is {({() int}
+ * {() int})}) with
+ | ((x is {() int})
+ * (y is {() int})) ->
+ ((add is (() int
+ ->(() int
+ ->() int))) (x is {() int}) (1 is () int), (add is (
+ () int
+ ->(() int
+ ->() int))) (
+ y is {() int}) (1 is () int))
+
+ let result = (print_int_tu_lst is (((() int
+ * () int)) list
+ ->() unit)) (map is (({(() int
+ * () int)})
+ list
+ ->(({(() int
+ * () int)}
+ ->{(() int
+ *
+ () int)})
+ ->({(() int
+ *
+ () int)})
+ list))) (
+ lst is ((() int
+ * () int)) list) (tu_adder is ((() int
+ * () int)
+ ->(() int
+ * () int)))
$ $FF test_list.fun
diff --git a/tests/cram/test_dirs/simple.t/run.t b/tests/cram/test_dirs/simple.t/run.t
index e802749..f48ed8f 100644
--- a/tests/cram/test_dirs/simple.t/run.t
+++ b/tests/cram/test_dirs/simple.t/run.t
@@ -196,19 +196,19 @@
$ cat simple1.typed
- let x = (1 is () 0.int)
+ let x = (1 is () int)
- let y = (1 is () 0.int)
+ let y = (1 is () int)
let z = fun x ->
- (y is () 0.int)
+ (y is () int)
let w = fun x ->
- (0 is () 0.int)
+ (0 is () int)
let m = fun x ->
- (w is ({() 0.int}
- ->() 0.int)) (1 is () 0.int)
+ (w is ({() int}
+ ->() int)) (1 is () int)
$ $FF simple.fun
diff --git a/tests/regular/render_typed_test.ml b/tests/regular/render_typed_test.ml
index ade10a5..295f481 100644
--- a/tests/regular/render_typed_test.ml
+++ b/tests/regular/render_typed_test.ml
@@ -12,11 +12,12 @@ let%expect_test "Test: pretty print typed expression" =
Format.pp_print_flush fmt ()
in
print_typed "1";
- [%expect {| (1 is () 0.int) |}];
+ [%expect {| (1 is () int) |}];
print_typed {|let x = 1 in x|};
[%expect {|
- let x = (1 is () 0.int)
- in (x is () 0.int) |}];
+ let x = (1 is () int)
+ in (x is () int)
+ |}];
print_typed {|fun x -> let y = x in y |};
[%expect
@@ -30,16 +31,16 @@ let%expect_test "Test: pretty print typed expression" =
[%expect
{|
if
- (true is () 0.bool)
+ (true is () bool)
then
- (1 is () 0.int)
+ (1 is () int)
else
- (2 is () 0.int) |}];
+ (2 is () int)
+ |}];
print_typed {| (1, 2, 3,4) |};
[%expect
- {|
- ((1 is () 0.int), (2 is () 0.int), (3 is () 0.int), (4 is () 0.int)) |}];
+ {| ((1 is () int), (2 is () int), (3 is () int), (4 is () int)) |}];
print_typed
{|
@@ -50,12 +51,13 @@ let%expect_test "Test: pretty print typed expression" =
[%expect
{|
let rec f = fun x ->
- (x is {() 0.int})
+ (x is {() int})
and y = fun x ->
- (f is ({() 0.int}
- ->{() 0.int})) (1 is () 0.int)
- in (f is (() 0.int
- ->() 0.int)) (1 is () 0.int) |}]
+ (f is ({() int}
+ ->{() int})) (1 is () int)
+ in (f is (() int
+ ->() int)) (1 is () int)
+ |}]
let%expect_test "Test: pretty print typed program" =
let print_typed str =
@@ -84,17 +86,18 @@ let%expect_test "Test: pretty print typed program" =
[%expect
{|
type () int_l =
- | Cons of () 0.int
+ | Cons of () int
| Nil
- let co = (Cons[0] is (() 0.int
- ->() 0.int_l)) (1 is () 0.int)
+ let co = (Cons[0] is (() int
+ ->() int_l)) (1 is () int)
- let c = (Nil[1] is () 0.int_l)
+ let c = (Nil[1] is () int_l)
- let f = match (c is () 0.int_l) with
- | (Cons[0] (x is () 0.int)) -> (x is () 0.int)
- | Nil -> (0 is () 0.int) |}];
+ let f = match (c is () int_l) with
+ | (Cons[0] (x is () int)) -> (x is () int)
+ | Nil -> (0 is () int)
+ |}];
print_typed
{|
@@ -331,7 +334,7 @@ let%expect_test "Test: pretty print typed program" =
type () t =
| Nil
- let z = (1 is () 0.int)
+ let z = (1 is () int)
let x = (Nil[0] is () 2.t)
@@ -341,7 +344,7 @@ let%expect_test "Test: pretty print typed program" =
val x : () 2.t
- val z : () 0.int
+ val z : () int
constr Nil[0] : () 2.t
@@ -442,9 +445,9 @@ module MMM = (M(F).K : I)
id = 1
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -456,11 +459,11 @@ module MMM = (M(F).K : I)
id = 2
- val z : () 0.int
+ val z : () int
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -470,21 +473,21 @@ module MMM = (M(F).K : I)
module MJ =
(struct
- let x = (1 is () 0.int)
+ let x = (1 is () int)
- let y = (1 is () 0.int)
+ let y = (1 is () int)
- let z = (1 is () 0.int)
+ let z = (1 is () int)
end is sig
id = 3
- val z : () 0.int
+ val z : () int
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -494,17 +497,17 @@ module MMM = (M(F).K : I)
module Simple =
(struct
- let x = (1 is () 0.int)
+ let x = (1 is () int)
- let y = (2 is () 0.int)
+ let y = (2 is () int)
end is sig
id = 4
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -516,9 +519,9 @@ module MMM = (M(F).K : I)
id = 1
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -529,9 +532,9 @@ module MMM = (M(F).K : I)
id = 1
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -545,9 +548,9 @@ module MMM = (M(F).K : I)
id = 6
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -559,9 +562,9 @@ module MMM = (M(F).K : I)
id = 7
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -576,9 +579,9 @@ module MMM = (M(F).K : I)
id = 7
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -589,9 +592,9 @@ module MMM = (M(F).K : I)
id = 6
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -610,9 +613,9 @@ module MMM = (M(F).K : I)
id = 1
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -621,25 +624,25 @@ module MMM = (M(F).K : I)
->
(((struct
- let x = (1 is () 0.int)
+ let x = (1 is () int)
- let y = (1 is () 0.int)
+ let y = (1 is () int)
- let z = (1 is () 0.int)
+ let z = (1 is () int)
- let w = (2 is () 0.int)
+ let w = (2 is () int)
end is sig
id = 8
- val w : () 0.int
+ val w : () int
- val z : () 0.int
+ val z : () int
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -648,11 +651,11 @@ module MMM = (M(F).K : I)
id = 2
- val z : () 0.int
+ val z : () int
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -661,11 +664,11 @@ module MMM = (M(F).K : I)
id = 9
- val z : () 0.int
+ val z : () int
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -681,9 +684,9 @@ module MMM = (M(F).K : I)
id = 11
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -694,9 +697,9 @@ module MMM = (M(F).K : I)
id = 12
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -712,9 +715,9 @@ module MMM = (M(F).K : I)
id = 1
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -723,9 +726,9 @@ module MMM = (M(F).K : I)
id = 13
- val y : () 0.int
+ val y : () int
- val x : () 0.int
+ val x : () int
Owned Modules = {
}
@@ -795,10 +798,10 @@ module MMM = (M(F).K : I)
print_typed {| let x = ();();();1 |};
[%expect
{|
- let x = (() is () 0.unit) ;
- (() is () 0.unit) ;
- (() is () 0.unit) ;
- (1 is () 0.int)
+ let x = (() is () unit) ;
+ (() is () unit) ;
+ (() is () unit) ;
+ (1 is () int)
|}];
(* constructor accessed by path *)
@@ -824,7 +827,7 @@ module MMM = (M(F).K : I)
type () t =
| Nil
- | Integer of () 0.int
+ | Integer of () int
end is sig
@@ -832,12 +835,12 @@ module MMM = (M(F).K : I)
constr Nil[0] : () 1.t
- constr Integer[1] : (() 0.int
+ constr Integer[1] : (() int
->() 1.t)
type () t =
| Nil
- | Integer of () 0.int
+ | Integer of () int
Owned Modules = {
}
@@ -847,8 +850,8 @@ module MMM = (M(F).K : I)
let c = (C.Nil[0] is () 1.t)
let result = match (c is () 1.t) with
- | Nil -> (() is () 0.unit)
- | (Integer[1] (i is () 0.int)) -> (() is () 0.unit)
+ | Nil -> (() is () unit)
+ | (Integer[1] (i is () int)) -> (() is () unit)
|}];
print_typed
@@ -872,25 +875,25 @@ module MMM = (M(F).K : I)
{|
type () list =
| Nil
- | Cons of (() 0.int
- * (() 0.int) 0.list)
+ | Cons of (() int
+ * (() int) list)
type ('a/0, 'b/0) tu =
| Tu of (['b/0]
* ['a/0])
- let x = (Tu[0] is (({() 0.int}
- * {() 0.string})
- ->({() 0.string}, {() 0.int}) 0.tu)) ((1 is () 0.int), (
- ""c"" is () 0.string))
+ let x = (Tu[0] is (({() int}
+ * {() string})
+ ->({() string}, {() int}) tu)) ((1 is () int), (""c"" is
+ () string))
- let result1 = match (x is (() 0.string, () 0.int) 0.tu) with
- | (Tu[0] ((a is {() 0.int})
- * (b is {() 0.string}))) -> (a is () 0.int)
+ let result1 = match (x is (() string, () int) tu) with
+ | (Tu[0] ((a is {() int})
+ * (b is {() string}))) -> (a is () int)
- let result2 = match (x is (() 0.string, () 0.int) 0.tu) with
- | (Tu[0] ((a is {() 0.int})
- * (b is {() 0.string}))) -> (b is () 0.string)
+ let result2 = match (x is (() string, () int) tu) with
+ | (Tu[0] ((a is {() int})
+ * (b is {() string}))) -> (b is () string)
|}];
print_typed
@@ -1009,21 +1012,21 @@ module MMM = (M(F).K : I)
->
(struct
- type t = () 0.int
+ type t = () int
- type s = () 0.int
+ type s = () int
- let x = (1 is () 0.int)
+ let x = (1 is () int)
end is sig
id = 4
- val x : () 0.int
+ val x : () int
- type s = () 0.int
+ type s = () int
- type t = () 0.int
+ type t = () int
Owned Modules = {
}
diff --git a/tests/regular/typing_test.ml b/tests/regular/typing_test.ml
index 769fcb7..9a330fe 100644
--- a/tests/regular/typing_test.ml
+++ b/tests/regular/typing_test.ml
@@ -1144,7 +1144,7 @@ let%expect_test "Error reporting test" =
let y = true
let z = x = y
|};
- [%expect {| 4:13-4:13 Can't unify `() 0.int` with `() 0.bool` |}];
+ [%expect {| 4:13-4:13 Can't unify `() int` with `() bool` |}];
print_typed
{|
@@ -1256,7 +1256,7 @@ let%expect_test "Error reporting test" =
let z = Y1.y = Y2.y
|};
- [%expect {| 25:21-25:21 Can't unify `() 6.t` with `() 7.t` |}];
+ [%expect {| 25:21-25:21 Can't unify `() Y1.t` with `() Y2.t` |}];
print_typed
{|
module type I = sig
From 90768871b289a7ee689cab9cfda33343201ea931 Mon Sep 17 00:00:00 2001
From: butterunderflow <azhong.934@gmail.com>
Date: Sun, 4 Aug 2024 22:10:42 +0800
Subject: [PATCH 2/2] refactor: avoid huge let expression
factor out `check_mod` to smaller parts
---
lib/typing/check.ml | 72 ++++++++++++++++++++++++++-------------------
1 file changed, 42 insertions(+), 30 deletions(-)
diff --git a/lib/typing/check.ml b/lib/typing/check.ml
index ceaf580..91b0b36 100644
--- a/lib/typing/check.ml
+++ b/lib/typing/check.ml
@@ -390,41 +390,53 @@ and make_mt_by_scope
and check_mod (me : T.mod_expr) (env : Env.t) : mod_expr =
let me_typed =
match me.node with
- | T.MEName name -> MEName (name, Env.lookup_module_def name env)
- | T.MEStruct body ->
- let body_typed, env' = check_top_levels body (Env.enter_env env) in
- let scope = absorb_history env' env in
- let mt = make_mt_by_scope scope in
- MEStruct (body_typed, mt)
+ | T.MEName name -> check_mod_name name env
+ | T.MEStruct body -> check_struct body env
| T.MEFunctor ((name, ext_mt0), me1) ->
- let mt0 = normalize_mt ext_mt0 env in
- let me1_typed = check_mod me1 (Env.add_module name mt0 env) in
- MEFunctor ((name, mt0), me1_typed)
- | T.MEField (me, name) -> (
- let me_typed = check_mod me env in
- match get_mod_ty me_typed with
- | I.MTMod { mod_defs; _ } ->
- MEField (me_typed, name, List.assoc name mod_defs)
- | I.MTFun _ -> failwith "try get field from functor")
- | T.MEApply (me0, me1) -> (
- let me0_typed = check_mod me0 env in
- let me1_typed = check_mod me1 env in
- let mt0 = get_mod_ty me0_typed in
- let mt1 = get_mod_ty me1_typed in
- match mt0 with
- | I.MTMod _ -> failwith "try apply a structure"
- | I.MTFun (para_mt, body_mt) ->
- MEApply
- (me0_typed, me1_typed, apply_functor para_mt body_mt mt1 env))
- | T.MERestrict (me, mt) ->
- let me_typed = check_mod me env in
- let mt = normalize_mt mt env in
- let _subst = check_subtype (get_mod_ty me_typed) mt in
- MERestrict (me_typed, mt, shift_mt mt env)
+ check_functor name ext_mt0 me1 env
+ | T.MEField (me, name) -> check_mod_field me name env
+ | T.MEApply (me0, me1) -> check_mod_apply me0 me1 env
+ | T.MERestrict (me, mt) -> check_mod_restrict me mt env
in
Env.try_record_hint me_typed env;
me_typed
+and check_mod_name name env = MEName (name, Env.lookup_module_def name env)
+
+and check_struct body env =
+ let body_typed, env' = check_top_levels body (Env.enter_env env) in
+ let scope = absorb_history env' env in
+ let mt = make_mt_by_scope scope in
+ MEStruct (body_typed, mt)
+
+and check_functor name ext_mt0 me1 env =
+ let mt0 = normalize_mt ext_mt0 env in
+ let me1_typed = check_mod me1 (Env.add_module name mt0 env) in
+ MEFunctor ((name, mt0), me1_typed)
+
+and check_mod_field me name env =
+ let me_typed = check_mod me env in
+ match get_mod_ty me_typed with
+ | I.MTMod { mod_defs; _ } ->
+ MEField (me_typed, name, List.assoc name mod_defs)
+ | I.MTFun _ -> failwith "try get field from functor"
+
+and check_mod_apply me0 me1 env =
+ let me0_typed = check_mod me0 env in
+ let me1_typed = check_mod me1 env in
+ let mt0 = get_mod_ty me0_typed in
+ let mt1 = get_mod_ty me1_typed in
+ match mt0 with
+ | I.MTMod _ -> failwith "try apply a structure"
+ | I.MTFun (para_mt, body_mt) ->
+ MEApply (me0_typed, me1_typed, apply_functor para_mt body_mt mt1 env)
+
+and check_mod_restrict me mt env =
+ let me_typed = check_mod me env in
+ let mt = normalize_mt mt env in
+ let _subst = check_subtype (get_mod_ty me_typed) mt in
+ MERestrict (me_typed, mt, shift_mt mt env)
+
(* apply a functor, add returned module type's id into environment *)
and apply_functor para_mt body_mt arg_mt env =
let subst = check_subtype arg_mt para_mt in