Skip to content

Commit 93e848b

Browse files
committed
fix(typecheck): reconcile register_builtins with resolver seed list (#135)
register_builtins had drifted from resolve.ml's seed_builtins: file-I/O (read_file/write_file/append_file/file_exists/is_directory), env/time (getenv/getcwd/time_now), and float-math (floor/ceil/round/trunc/sin/ cos/tan/atan/atan2/exp/log/log10/log2/cbrt) were seeded for resolution but never typed, so stdlib files using them failed typecheck with 'Unbound variable'. Add correct schemes (signatures per io.affine / math.affine headers). Also retype read_line as Unit -> Result<String,String> (io.affine pattern-matches it Ok/Err; effects.affine has its own extern decl so is unaffected). io.affine's file-I/O builtins now type; its remaining failure is the cross-module imported-type threading layer (split's scheme not seeded into the importer's typecheck) — separate, documented on #128. Full suite 233/233, zero regression; stdlib 12/19. Refs #128
1 parent d23b71d commit 93e848b

1 file changed

Lines changed: 31 additions & 1 deletion

File tree

lib/typecheck.ml

Lines changed: 31 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1196,7 +1196,8 @@ let register_builtins (ctx : context) : unit =
11961196
bind_var ctx "println" (TArrow (ty_string, QOmega, ty_unit, ESingleton "IO"));
11971197
bind_var ctx "eprint" (TArrow (ty_string, QOmega, ty_unit, ESingleton "IO"));
11981198
bind_var ctx "eprintln" (TArrow (ty_string, QOmega, ty_unit, ESingleton "IO"));
1199-
bind_var ctx "read_line" (TArrow (ty_unit, QOmega, ty_string, ESingleton "IO"));
1199+
bind_var ctx "read_line"
1200+
(TArrow (ty_unit, QOmega, TApp (TCon "Result", [ty_string; ty_string]), ESingleton "IO"));
12001201
bind_var ctx "int_to_string" (TArrow (ty_int, QOmega, ty_string, EPure));
12011202
bind_var ctx "int" (TArrow (ty_float, QOmega, ty_int, EPure));
12021203
bind_var ctx "float" (TArrow (ty_int, QOmega, ty_float, EPure));
@@ -1291,6 +1292,35 @@ let register_builtins (ctx : context) : unit =
12911292
bind_var ctx "int_to_char" (TArrow (ty_int, QOmega, ty_char, EPure));
12921293
bind_scheme ctx "show"
12931294
(poly1 (fun a -> TArrow (a, QOmega, ty_string, EPure)));
1295+
(* Reconcile with the resolver builtin-seed list (resolve.ml seed_builtins):
1296+
file-I/O / env / time / float-math builtins were seeded for resolution
1297+
but never typed here, so stdlib files using them failed typecheck with
1298+
"Unbound variable". Signatures per the io.affine / math.affine headers. *)
1299+
(* File I/O — effectful, Result/Option-returning *)
1300+
bind_var ctx "read_file"
1301+
(TArrow (ty_string, QOmega, res ty_string ty_string, ESingleton "IO"));
1302+
bind_var ctx "write_file"
1303+
(TArrow (ty_string, QOmega,
1304+
TArrow (ty_string, QOmega, res ty_unit ty_string, ESingleton "IO"), EPure));
1305+
bind_var ctx "append_file"
1306+
(TArrow (ty_string, QOmega,
1307+
TArrow (ty_string, QOmega, res ty_unit ty_string, ESingleton "IO"), EPure));
1308+
bind_var ctx "file_exists" (TArrow (ty_string, QOmega, ty_bool, ESingleton "IO"));
1309+
bind_var ctx "is_directory" (TArrow (ty_string, QOmega, ty_bool, ESingleton "IO"));
1310+
(* Environment / process / time *)
1311+
bind_var ctx "getenv" (TArrow (ty_string, QOmega, opt ty_string, ESingleton "IO"));
1312+
bind_var ctx "getcwd" (TArrow (ty_unit, QOmega, res ty_string ty_string, ESingleton "IO"));
1313+
bind_var ctx "time_now" (TArrow (ty_unit, QOmega, ty_float, ESingleton "IO"));
1314+
(* Float math — pure; floor/ceil/round/trunc truncate to Int per headers *)
1315+
let f_to_i = TArrow (ty_float, QOmega, ty_int, EPure) in
1316+
let f_to_f = TArrow (ty_float, QOmega, ty_float, EPure) in
1317+
bind_var ctx "floor" f_to_i; bind_var ctx "ceil" f_to_i;
1318+
bind_var ctx "round" f_to_i; bind_var ctx "trunc" f_to_i;
1319+
bind_var ctx "sin" f_to_f; bind_var ctx "cos" f_to_f; bind_var ctx "tan" f_to_f;
1320+
bind_var ctx "atan" f_to_f; bind_var ctx "exp" f_to_f; bind_var ctx "cbrt" f_to_f;
1321+
bind_var ctx "log" f_to_f; bind_var ctx "log10" f_to_f; bind_var ctx "log2" f_to_f;
1322+
bind_var ctx "atan2"
1323+
(TArrow (ty_float, QOmega, TArrow (ty_float, QOmega, ty_float, EPure), EPure));
12941324
bind_var ctx "panic" (TArrow (ty_string, QOmega, ty_never, EPure));
12951325
bind_var ctx "exit" (TArrow (ty_int, QOmega, ty_never, ESingleton "IO"));
12961326
(* TEA runtime — accepts any record, returns unit with IO effect *)

0 commit comments

Comments
 (0)