From fd016e07e65f2faf837ea7c470f9320f46b26e80 Mon Sep 17 00:00:00 2001 From: Takashi Suwa Date: Mon, 16 Sep 2024 05:03:32 +0900 Subject: [PATCH] make `ModuleTypechecker` use `Typechecker.typecheck_nonrec` --- src/frontend/errorReporting.ml | 5 ++- src/frontend/moduleTypechecker.ml | 70 ++++--------------------------- src/frontend/typeError.ml | 2 +- src/frontend/typecheckUtil.ml | 10 ----- src/frontend/typechecker.ml | 6 +-- src/frontend/typechecker.mli | 2 + 6 files changed, 18 insertions(+), 77 deletions(-) diff --git a/src/frontend/errorReporting.ml b/src/frontend/errorReporting.ml index fcba947d5..3e32031a9 100644 --- a/src/frontend/errorReporting.ml +++ b/src/frontend/errorReporting.ml @@ -595,10 +595,11 @@ let make_type_error_message = function NormalLine("tests must be stage-1 non-recursive bindings."); ] - | NonemptyManualQuantifier(rng) -> + | TestMustBeUnitToUnit(rng, pty) -> [ NormalLine(Printf.sprintf "at %s:" (Range.to_string rng)); - NormalLine("no type/row variable should be bound here."); + NormalLine("tests must be of type unit -> unit, but this one has type"); + DisplayLine(Display.show_poly_type pty); ] diff --git a/src/frontend/moduleTypechecker.ml b/src/frontend/moduleTypechecker.ml index c62a68bb4..9890a1ca9 100644 --- a/src/frontend/moduleTypechecker.ml +++ b/src/frontend/moduleTypechecker.ml @@ -692,30 +692,6 @@ and typecheck_binding_list (config : typecheck_config) (tyenv : Typeenv.t) (utbi return ((quant, ssig), binds) -and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (ident : var_name ranged) (utast1 : untyped_abstract_tree) (ty_expected_opt : mono_type option) = - let open ResultMonad in - let presub = { pre with level = Level.succ pre.level; } in - let evid = EvalVarID.fresh ident in - let* (e1_raw, ty1) = Typechecker.typecheck presub tyenv utast1 in - let e1 = e1_raw in - let* () = - match ty_expected_opt with - | None -> return () - | Some(ty_expected) -> unify ty1 ty_expected - in -(* - let should_be_polymorphic = is_nonexpansive_expression e1 in -*) - let should_be_polymorphic = true in - let pty = - if should_be_polymorphic then - TypeConv.generalize pre.level (TypeConv.erase_range_of_type ty1) - else - TypeConv.lift_poly (TypeConv.erase_range_of_type ty1) - in - return (evid, e1, pty) - - and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind : untyped_binding) : (binding list * StructSig.t abstracted) ok = let open ResultMonad in let (rng, utbindmain) = utbind in @@ -738,25 +714,16 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind : if valattr.ValueAttribute.is_test then match (stage, valbind) with | (Stage1, UTNonRec(utletbind)) -> - let - UTLetBinding{ - identifier = ident; - quantifier = mnquant; - parameters = param_units; - return_type = mntyopt_ret; - body = utast_body; - } = utletbind - in - let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *) - let* () = check_empty_manual_quantifier rng mnquant in - let (_, test_name) = ident in - let ty_expected = + let pty_expected = let ty_dom = (Range.dummy "test-dom", BaseType(UnitType)) in let ty_cod = (Range.dummy "test-cod", BaseType(UnitType)) in - (Range.dummy "test-func", FuncType(RowEmpty, ty_dom, ty_cod)) + Poly(Range.dummy "test-func", FuncType(RowEmpty, ty_dom, ty_cod)) in - let* (evid, e1, _pty) = typecheck_nonrec pre tyenv ident utast1 (Some(ty_expected)) in - return ([ BindTest(evid, test_name, e1) ], (OpaqueIDMap.empty, StructSig.empty)) + let* (test_name, pty1, evid, e1) = Typechecker.typecheck_nonrec pre tyenv utletbind in + if TypeConv.poly_type_equal pty_expected pty1 then + return ([ BindTest(evid, test_name, e1) ], (OpaqueIDMap.empty, StructSig.empty)) + else + err @@ TestMustBeUnitToUnit(rng, pty1) | _ -> err @@ TestMustBeStage1NonRec(rng) @@ -764,30 +731,11 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind : let* (rec_or_nonrecs, ssig) = match valbind with | UTNonRec(utletbind) -> - let - UTLetBinding{ - identifier = ident; - quantifier = ManualQuantifier(typarams, rowparams); - parameters = param_units; - return_type = _mntyopt_ret; - body = utast_body; - } = utletbind - in - let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *) - let* (typarammap, _) = pre.type_parameters |> add_type_parameters (Level.succ Level.bottom) typarams in - let* (rowparammap, _) = pre.row_parameters |> add_row_parameters (Level.succ Level.bottom) rowparams in - let pre = - { pre with - type_parameters = typarammap; - row_parameters = rowparammap; - } - in - let* (evid, e1, pty) = typecheck_nonrec pre tyenv ident utast1 None in + let* (varnm, pty1, evid, e1) = Typechecker.typecheck_nonrec pre tyenv utletbind in let ssig = - let (_, varnm) = ident in let ventry = { - val_type = pty; + val_type = pty1; val_name = Some(evid); val_stage = pre.stage; } diff --git a/src/frontend/typeError.ml b/src/frontend/typeError.ml index 3e3196ef2..8f83e95ee 100644 --- a/src/frontend/typeError.ml +++ b/src/frontend/typeError.ml @@ -69,4 +69,4 @@ type type_error = | ValueAttributeError of ValueAttribute.error | ModuleAttributeError of ModuleAttribute.error | TestMustBeStage1NonRec of Range.t - | NonemptyManualQuantifier of Range.t + | TestMustBeUnitToUnit of Range.t * poly_type diff --git a/src/frontend/typecheckUtil.ml b/src/frontend/typecheckUtil.ml index 7f8a1f2f0..368f41103 100644 --- a/src/frontend/typecheckUtil.ml +++ b/src/frontend/typecheckUtil.ml @@ -124,13 +124,3 @@ let add_row_parameters (lev : Level.t) (rowvars : (row_variable_name ranged * ma ) (rowparammap, Alist.empty) in return (rowparammap, Alist.to_list bridacc) - - -let check_empty_manual_quantifier (rng : Range.t) (mnquant : manual_quantifier) : unit ok = - let open ResultMonad in - match mnquant with - | ManualQuantifier([], []) -> - return () - - | _ -> - err @@ NonemptyManualQuantifier(rng) diff --git a/src/frontend/typechecker.ml b/src/frontend/typechecker.ml index bb5568aee..f8e666886 100644 --- a/src/frontend/typechecker.ml +++ b/src/frontend/typechecker.ml @@ -648,7 +648,7 @@ let rec typecheck (pre : pre) (tyenv : Typeenv.t) ((rng, utastmain) : untyped_ab return (PatternMatch(rng, eO, patbrs), beta) | UTLetIn(UTNonRec(utletbind), utast2) -> - let* (varnm, evid, e1, pty1) = typecheck_nonrec pre tyenv utletbind in + let* (varnm, pty1, evid, e1) = typecheck_nonrec pre tyenv utletbind in let tyenv = let ventry = { @@ -1226,7 +1226,7 @@ and typecheck_letrec (pre : pre) (tyenv : Typeenv.t) (utrecbinds : untyped_let_b return tuples -and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (utletbind : untyped_let_binding) : (var_name * EvalVarID.t * abstract_tree * poly_type) ok = +and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (utletbind : untyped_let_binding) : (var_name * poly_type * EvalVarID.t * abstract_tree) ok = let open ResultMonad in let UTLetBinding{ @@ -1258,7 +1258,7 @@ and typecheck_nonrec (pre : pre) (tyenv : Typeenv.t) (utletbind : untyped_let_bi (* If `e1` should be typed monomorphically: *) TypeConv.lift_poly (TypeConv.erase_range_of_type ty1) in - return (varnm, evid, e1, pty1) + return (varnm, pty1, evid, e1) and typecheck_let_mutable (pre : pre) (tyenv : Typeenv.t) (ident : var_name ranged) (utastI : untyped_abstract_tree) : (Typeenv.t * EvalVarID.t * abstract_tree * mono_type) ok = diff --git a/src/frontend/typechecker.mli b/src/frontend/typechecker.mli index d33973108..7e96e1f70 100644 --- a/src/frontend/typechecker.mli +++ b/src/frontend/typechecker.mli @@ -7,6 +7,8 @@ val typecheck : pre -> type_environment -> untyped_abstract_tree -> (abstract_tr val typecheck_letrec : pre -> type_environment -> untyped_let_binding list -> ((var_name * poly_type * EvalVarID.t * letrec_binding) list, type_error) result +val typecheck_nonrec : pre -> type_environment -> untyped_let_binding -> (var_name * poly_type * EvalVarID.t * abstract_tree, type_error) result + val main : typecheck_config -> stage -> Typeenv.t -> untyped_abstract_tree -> (mono_type * abstract_tree, type_error) result val are_unifiable : mono_type -> mono_type -> bool