add PTE to lock and tid types

src/flowInference.ml

@@ -231,7 +231,7 @@ let rec deep_type_normalization = function
   | `Ref (b,t) -> `Ref (b, deep_type_normalization t)
   | `IntArray -> `IntArray
   | `TVar -> assert false
-  | `Lock | `ThreadID -> failwith "not implemented in flowinference"
+  | `Lock _ | `ThreadID _ -> failwith "not implemented in flowinference"
 
 let rec simple_to_fltype ?tvar = function
   | `Mu (id,t) ->
@@ -244,7 +244,7 @@ let rec simple_to_fltype ?tvar = function
     assert (Option.map ((=) id) tvar |> Option.value ~default:false);
     `TVar
   | `Tuple tl -> `Tuple (List.map (simple_to_fltype ?tvar) tl)
-  | `Lock | `ThreadID -> failwith "not implemented in flowinference"
+  | `Lock _ | `ThreadID _ -> failwith "not implemented in flowinference"
 
 let%lq get_function_type f_name ctxt =
   let { f_type; _ } = StringMap.find f_name ctxt.fenv in
@@ -628,7 +628,7 @@ let rec walk_type ty step f st acc =
         )
       )
     )
-  | `Lock | `ThreadID -> failwith "not implemented in flowinference"
+  | `Lock _ | `ThreadID _ -> failwith "not implemented in flowinference"
 
 (** Walk two paths in parallel according to the type ty. Unlike type_walk, this
    walk function only calls the step function when:

src/ownershipInference.ml

@@ -256,7 +256,7 @@ let rec unfold_simple arg mu = function
   | `Array `Int -> `Array `Int
   | `Tuple tl_list -> `Tuple (List.map (unfold_simple arg mu) tl_list)
   | `Mu (id, t) -> `Mu (id, unfold_simple arg mu t)
-  | `Lock | `ThreadID -> failwith "not implemented in ownershipinference"
+  | `Lock _ | `ThreadID _ -> failwith "not implemented in ownershipinference"
 
 (** Walk a type, constraining the first occurrence of an
    ownership variable to be well-formed w.r.t [o].
@@ -352,7 +352,7 @@ let lift_to_ownership loc root t_simp =
           mmapi (fun i t -> simple_lift ~unfld (P.t_ind root i) t) tl
         in
         return @@ Tuple tl'
-    | `Lock | `ThreadID -> failwith "not implemented in ownershipinference"
+    | `Lock _ | `ThreadID _ -> failwith "not implemented in ownershipinference"
   in
   let%bind t = simple_lift ~unfld:IntSet.empty root t_simp in
   constrain_well_formed t >> return t

src/simpleTypes.ml

@@ -28,8 +28,12 @@ let rec type_to_string = function
   | `Mu (v,t) -> Printf.sprintf "(%s '%d.%s)" Greek.mu v @@ type_to_string t
   | `TVar v -> Printf.sprintf "'%d" v
   | `Array at -> Printf.sprintf "[%s]" @@ array_type_to_string at
-  | `Lock _ -> "lock"
-  | `ThreadID _ -> "tid"
+  | `Lock pte -> 
+      let l = StringMap.fold (fun x t l -> (x ^ ": " ^ type_to_string t) :: l) pte [] in
+      Printf.sprintf "(%s)lock" @@ String.concat ", " l
+  | `ThreadID pte ->
+      let l = StringMap.fold (fun x t l -> (x ^ ": " ^ type_to_string t) :: l) pte [] in
+      Printf.sprintf "(%s)tid" @@ String.concat ", " l
 and array_type_to_string = function
   | `Int -> "int"