refactoring around PolyFree

gfngfn · Sep 16, 2024 · add95ad · add95ad
1 parent 2ef1a7c
commit add95ad
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 33 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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