diff --git a/backend/cn/lib/resources.ml b/backend/cn/lib/resources.ml index 0eb041a9d..909cd6c39 100644 --- a/backend/cn/lib/resources.ml +++ b/backend/cn/lib/resources.ml @@ -45,7 +45,8 @@ let addr_of pointer = (* assumption: the resource is owned *) -let derived_lc1 = function +let derived_lc1 (resource, _) = + match resource with | P { name = Owned (ct, _); pointer; iargs = _ } -> let here = Locations.other (__FUNCTION__ ^ ":" ^ string_of_int __LINE__) in let addr = addr_of pointer in @@ -59,7 +60,7 @@ let derived_lc1 = function (* assumption: both resources are owned at the same *) (* todo, depending on how much we need *) -let derived_lc2 resource (resource', _) = +let derived_lc2 (resource, _) (resource', _) = match (resource, resource') with | ( P { name = Owned (ct1, _); pointer = p1; iargs = _ }, P { name = Owned (ct2, _); pointer = p2; iargs = _ } ) -> @@ -72,11 +73,14 @@ let derived_lc2 resource (resource', _) = | _ -> [] -let pointer_facts = - let rec aux acc = function - | [] -> acc - | (r, _) :: rs -> - let acc = derived_lc1 r @ List.concat_map (derived_lc2 r) rs @ acc in - aux acc rs - in - fun resources -> aux [] resources +(* let pointer_facts = *) +(* let rec aux acc = function *) +(* | [] -> acc *) +(* | (r, _) :: rs -> *) +(* let acc = derived_lc1 r @ List.concat_map (derived_lc2 r) rs @ acc in *) +(* aux acc rs *) +(* in *) +(* fun resources -> aux [] resources *) + +let pointer_facts ~new_resource ~old_resources = + derived_lc1 new_resource @ List.concat_map (derived_lc2 new_resource) old_resources diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml index ed8f44e1a..63f58e152 100644 --- a/backend/cn/lib/typing.ml +++ b/backend/cn/lib/typing.ml @@ -445,7 +445,11 @@ let add_r_internal loc (r, RE.O oargs) = let@ simp_ctxt = simp_ctxt () in let r = Simplify.ResourceTypes.simp simp_ctxt r in let oargs = Simplify.IndexTerms.simp simp_ctxt oargs in - let pointer_facts = Resources.pointer_facts ((r, RE.O oargs) :: Context.get_rs s) in + let pointer_facts = + Resources.pointer_facts + ~new_resource:(r, RE.O oargs) + ~old_resources:(Context.get_rs s) + in let@ () = set_typing_context (Context.add_r loc (r, O oargs) s) in iterM (fun x -> add_c_internal (LC.T x)) pointer_facts