rename PolyFree to PolyFreeUpdatable

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

Hide file tree

Showing 6 changed files with 22 additions and 16 deletions.
diff --git a/src/frontend/display.ml b/src/frontend/display.ml
@@ -72,9 +72,10 @@ let collect_ids_scheme (fid_ht : unit FreeIDHashTable.t) (frid_ht : LabelSet.t F
     | TypeVariable(ptv) ->
         begin
           match ptv with
-          | PolyFree({contents = MonoLink(ty)})  -> aux_mono ty
-          | PolyFree({contents = MonoFree(fid)}) -> aux_free_id fid
-          | PolyBound(bid)                       -> aux_bound_id bid
+          | 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
         end
 
     | FuncType(poptrow, ptydom, ptycod) ->
@@ -395,8 +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
-  | PolyFree(tvuref) -> tvf_mono_updatable dispmap plev !tvuref
-  | PolyBound(bid)   -> dispmap |> DisplayMap.find_bound_id bid
+  | 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
 
 
 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,7 @@ 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(PolyFree(tvuref))), (rng, TypeVariable(Updatable(tvuref))))
+        ((rng, TypeVariable(PolyFreeUpdatable(tvuref))), (rng, TypeVariable(Updatable(tvuref))))
       in
       let (pty, macparamty) =
       match macparam with

diff --git a/src/frontend/signatureSubtyping.ml b/src/frontend/signatureSubtyping.ml
@@ -428,8 +428,10 @@ and subtype_poly_type_impl (internbid : type_intern) (internbrid : row_intern) (
     let (_, ptymain1) = pty1 in
     let (_, ptymain2) = pty2 in
     match (ptymain1, ptymain2) with
-    | (TypeVariable(PolyFree(_)), _)
-    | (_, TypeVariable(PolyFree(_))) ->
+    | (TypeVariable(PolyFreeUpdatable(_)), _)
+    | (_, TypeVariable(PolyFreeUpdatable(_)))
+    | (TypeVariable(PolyFreeMustBeBound(_)), _)
+    | (_, TypeVariable(PolyFreeMustBeBound(_))) ->
         false
 
     | (TypeVariable(PolyBound(bid1)), _) ->

diff --git a/src/frontend/typeConv.ml b/src/frontend/typeConv.ml
@@ -101,7 +101,7 @@ 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
-    | PolyFree(tvuref) ->
+    | PolyFreeUpdatable(tvuref) ->
         (rng, TypeVariable(Updatable(tvuref)))
 
     | PolyFreeMustBeBound(mbbid) ->
@@ -162,7 +162,7 @@ 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
-    | PolyFree(tvuref) ->
+    | PolyFreeUpdatable(tvuref) ->
         (rng, TypeVariable(Updatable(tvuref)))
 
     | PolyFreeMustBeBound(mbbid) ->
@@ -186,7 +186,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
-    | PolyFree(_) | PolyFreeMustBeBound(_) ->
+    | PolyFreeUpdatable(_) | PolyFreeMustBeBound(_) ->
         (rng, TypeVariable(ptv))
 
     | PolyBound(bid) ->
@@ -231,7 +231,7 @@ let lift_poly_general (intern_ty : FreeID.t -> BoundID.t option) (intern_row : F
                 | MonoFree(fid) ->
                     let ptvi =
                       match intern_ty fid with
-                      | None      -> PolyFree(tvuref)
+                      | None      -> PolyFreeUpdatable(tvuref)
                       | Some(bid) -> PolyBound(bid)
                     in
                     (rng, TypeVariable(ptvi))
@@ -489,8 +489,10 @@ 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(PolyFree(_)), _)
-    | (_, TypeVariable(PolyFree(_))) ->
+    | (TypeVariable(PolyFreeUpdatable(_)), _)
+    | (_, TypeVariable(PolyFreeUpdatable(_)))
+    | (TypeVariable(PolyFreeMustBeBound(_)), _)
+    | (_, TypeVariable(PolyFreeMustBeBound(_))) ->
         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(PolyFree(tvuref))) in
+      let pbeta = (rng, TypeVariable(PolyFreeUpdatable(tvuref))) in
       let tyenv =
         let ventry =
           {

diff --git a/src/frontend/types.cppo.ml b/src/frontend/types.cppo.ml
@@ -240,7 +240,7 @@ and mono_type_variable =
   | MustBeBound of MustBeBoundID.t
 
 and poly_type_variable =
-  | PolyFree            of mono_type_variable_updatable ref
+  | PolyFreeUpdatable   of mono_type_variable_updatable ref
   | PolyFreeMustBeBound of MustBeBoundID.t
   | PolyBound           of BoundID.t