From add95ad9e1667d4f229ce1973bcacf297c40aa6d Mon Sep 17 00:00:00 2001 From: Takashi Suwa Date: Mon, 16 Sep 2024 12:05:49 +0900 Subject: [PATCH] refactoring around `PolyFree` --- src/frontend/display.ml | 14 +++++++------- src/frontend/moduleTypechecker.ml | 3 ++- src/frontend/signatureSubtyping.ml | 6 ++---- src/frontend/typeConv.ml | 26 +++++++++----------------- src/frontend/typechecker.ml | 2 +- src/frontend/types.cppo.ml | 5 ++--- 6 files changed, 23 insertions(+), 33 deletions(-) diff --git a/src/frontend/display.ml b/src/frontend/display.ml index bbd23870f..299edf0a6 100644 --- a/src/frontend/display.ml +++ b/src/frontend/display.ml @@ -72,10 +72,10 @@ let collect_ids_scheme (fid_ht : unit FreeIDHashTable.t) (frid_ht : LabelSet.t F | TypeVariable(ptv) -> begin match ptv with - | PolyFreeUpdatable({contents = MonoLink(ty)}) -> aux_mono ty - | PolyFreeUpdatable({contents = MonoFree(fid)}) -> aux_free_id fid - | PolyFreeMustBeBound(mbbid) -> aux_bound_id (MustBeBoundID.to_bound_id mbbid) - | PolyBound(bid) -> aux_bound_id bid + | PolyFree(Updatable({contents = MonoLink(ty)})) -> aux_mono ty + | PolyFree(Updatable({contents = MonoFree(fid)})) -> aux_free_id fid + | PolyFree(MustBeBound(mbbid)) -> aux_bound_id (MustBeBoundID.to_bound_id mbbid) + | PolyBound(bid) -> aux_bound_id bid end | FuncType(poptrow, ptydom, ptycod) -> @@ -396,9 +396,9 @@ and show_mono_row_by_map (dispmap : DisplayMap.t) (row : mono_row) : string opti let tvf_poly (dispmap : DisplayMap.t) (plev : paren_level) (ptv : poly_type_variable) : string = match ptv with - | PolyFreeUpdatable(tvuref) -> tvf_mono_updatable dispmap plev !tvuref - | PolyFreeMustBeBound(mbbid) -> dispmap |> DisplayMap.find_bound_id (MustBeBoundID.to_bound_id mbbid) - | PolyBound(bid) -> dispmap |> DisplayMap.find_bound_id bid + | PolyFree(Updatable(tvuref)) -> tvf_mono_updatable dispmap plev !tvuref + | PolyFree(MustBeBound(mbbid)) -> dispmap |> DisplayMap.find_bound_id (MustBeBoundID.to_bound_id mbbid) + | PolyBound(bid) -> dispmap |> DisplayMap.find_bound_id bid let rvf_poly (dispmap : DisplayMap.t) (prv : poly_row_variable) : string = diff --git a/src/frontend/moduleTypechecker.ml b/src/frontend/moduleTypechecker.ml index 4e5ddff3f..62e0f808b 100644 --- a/src/frontend/moduleTypechecker.ml +++ b/src/frontend/moduleTypechecker.ml @@ -119,7 +119,8 @@ let add_macro_parameters_to_type_environment (tyenv : Typeenv.t) (pre : pre) (ma let (ptybody, beta) = let tvid = fresh_free_id pre.quantifiability (Level.succ pre.level) in let tvuref = ref (MonoFree(tvid)) in - ((rng, TypeVariable(PolyFreeUpdatable(tvuref))), (rng, TypeVariable(Updatable(tvuref)))) + let tv = Updatable(tvuref) in + ((rng, TypeVariable(PolyFree(tv))), (rng, TypeVariable(tv))) in let (pty, macparamty) = match macparam with diff --git a/src/frontend/signatureSubtyping.ml b/src/frontend/signatureSubtyping.ml index fc09b2f00..72d4761cc 100644 --- a/src/frontend/signatureSubtyping.ml +++ b/src/frontend/signatureSubtyping.ml @@ -428,10 +428,8 @@ and subtype_poly_type_impl (internbid : type_intern) (internbrid : row_intern) ( let (_, ptymain1) = pty1 in let (_, ptymain2) = pty2 in match (ptymain1, ptymain2) with - | (TypeVariable(PolyFreeUpdatable(_)), _) - | (_, TypeVariable(PolyFreeUpdatable(_))) - | (TypeVariable(PolyFreeMustBeBound(_)), _) - | (_, TypeVariable(PolyFreeMustBeBound(_))) -> + | (TypeVariable(PolyFree(_)), _) + | (_, TypeVariable(PolyFree(_))) -> false | (TypeVariable(PolyBound(bid1)), _) -> diff --git a/src/frontend/typeConv.ml b/src/frontend/typeConv.ml index 7acbf91bf..17f15e605 100644 --- a/src/frontend/typeConv.ml +++ b/src/frontend/typeConv.ml @@ -101,11 +101,8 @@ fun intern_ty intern_row prow -> let make_type_instantiation_intern (lev : level) (qtfbl : quantifiability) (bid_ht : mono_type_variable BoundIDHashTable.t) = let intern_ty (rng : Range.t) (ptv : poly_type_variable) : mono_type = match ptv with - | PolyFreeUpdatable(tvuref) -> - (rng, TypeVariable(Updatable(tvuref))) - - | PolyFreeMustBeBound(mbbid) -> - (rng, TypeVariable(MustBeBound(mbbid))) + | PolyFree(tv) -> + (rng, TypeVariable(tv)) | PolyBound(bid) -> begin @@ -162,11 +159,8 @@ let instantiate (lev : level) (qtfbl : quantifiability) ((Poly(pty)) : poly_type let instantiate_by_map_mono (bidmap : mono_type BoundIDMap.t) (Poly(pty) : poly_type) : mono_type = let intern_ty (rng : Range.t) (ptv : poly_type_variable) = match ptv with - | PolyFreeUpdatable(tvuref) -> - (rng, TypeVariable(Updatable(tvuref))) - - | PolyFreeMustBeBound(mbbid) -> - (rng, TypeVariable(MustBeBound(mbbid))) + | PolyFree(tv) -> + (rng, TypeVariable(tv)) | PolyBound(bid) -> begin @@ -186,7 +180,7 @@ let instantiate_by_map_mono (bidmap : mono_type BoundIDMap.t) (Poly(pty) : poly_ let instantiate_by_map_poly (bidmap : poly_type_body BoundIDMap.t) (Poly(pty) : poly_type) : poly_type = let intern_ty (rng : Range.t) (ptv : poly_type_variable) : poly_type_body = match ptv with - | PolyFreeUpdatable(_) | PolyFreeMustBeBound(_) -> + | PolyFree(_) -> (rng, TypeVariable(ptv)) | PolyBound(bid) -> @@ -231,8 +225,8 @@ let lift_poly_general (intern_ty : FreeID.t -> BoundID.t option) (intern_row : F | MonoFree(fid) -> let ptvi = match intern_ty fid with - | None -> PolyFreeUpdatable(tvuref) | Some(bid) -> PolyBound(bid) + | None -> PolyFree(tv) in (rng, TypeVariable(ptvi)) end @@ -243,7 +237,7 @@ let lift_poly_general (intern_ty : FreeID.t -> BoundID.t option) (intern_row : F let bid = MustBeBoundID.to_bound_id mbbid in PolyBound(bid) else - PolyFreeMustBeBound(mbbid) + PolyFree(tv) in (rng, TypeVariable(ptvi)) end @@ -489,10 +483,8 @@ let rec poly_type_equal (Poly(pty1) : poly_type) (Poly(pty2) : poly_type) : bool | (TypeVariable(PolyBound(bid1)), TypeVariable(PolyBound(bid2))) -> BoundID.equal bid1 bid2 - | (TypeVariable(PolyFreeUpdatable(_)), _) - | (_, TypeVariable(PolyFreeUpdatable(_))) - | (TypeVariable(PolyFreeMustBeBound(_)), _) - | (_, TypeVariable(PolyFreeMustBeBound(_))) -> + | (TypeVariable(PolyFree(_)), _) + | (_, TypeVariable(PolyFree(_))) -> false | (DataType(ptys1, tyid1), DataType(ptys2, tyid2)) -> diff --git a/src/frontend/typechecker.ml b/src/frontend/typechecker.ml index 4eff5751c..7970cb974 100644 --- a/src/frontend/typechecker.ml +++ b/src/frontend/typechecker.ml @@ -100,7 +100,7 @@ let add_optionals_to_type_environment ~(cons : label ranged -> mono_type -> 'a - let evid = EvalVarID.fresh ident in let fid = fresh_free_id qtfbl lev in let tvuref = ref (MonoFree(fid)) in - let pbeta = (rng, TypeVariable(PolyFreeUpdatable(tvuref))) in + let pbeta = (rng, TypeVariable(PolyFree(Updatable(tvuref)))) in let tyenv = let ventry = { diff --git a/src/frontend/types.cppo.ml b/src/frontend/types.cppo.ml index a79ffd30a..1fee63177 100644 --- a/src/frontend/types.cppo.ml +++ b/src/frontend/types.cppo.ml @@ -240,9 +240,8 @@ and mono_type_variable = | MustBeBound of MustBeBoundID.t and poly_type_variable = - | PolyFreeUpdatable of mono_type_variable_updatable ref - | PolyFreeMustBeBound of MustBeBoundID.t - | PolyBound of BoundID.t + | PolyFree of mono_type_variable + | PolyBound of BoundID.t and mono_type = (mono_type_variable, mono_row_variable) typ