From 9ddfae4e89ed193e8979631bdd2f1bc2d1fde8c2 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 9 Oct 2019 08:36:41 -0700 Subject: [PATCH] [sledge] Change Term.rename to preserve sharing in cyclic records Reviewed By: bennostein Differential Revision: D17665265 fbshipit-source-id: 50844096a --- sledge/src/import/import.ml | 1 + sledge/src/import/import.mli | 1 + sledge/src/import/vector.ml | 2 + sledge/src/import/vector.mli | 3 +- sledge/src/symbheap/term.ml | 108 ++++++++++++++++++++++------------- 5 files changed, 73 insertions(+), 42 deletions(-) diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index 4949f74d4..70fea3dc1 100644 --- a/sledge/src/import/import.ml +++ b/sledge/src/import/import.ml @@ -29,6 +29,7 @@ include ( (* undeprecate *) external ( == ) : 'a -> 'a -> bool = "%eq" +external ( != ) : 'a -> 'a -> bool = "%noteq" include Stdio module Command = Core.Command diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli index 8e7b6b8b0..af68fc744 100644 --- a/sledge/src/import/import.mli +++ b/sledge/src/import/import.mli @@ -30,6 +30,7 @@ include module type of ( (* undeprecate *) external ( == ) : 'a -> 'a -> bool = "%eq" +external ( != ) : 'a -> 'a -> bool = "%noteq" include module type of Stdio module Command = Core.Command diff --git a/sledge/src/import/vector.ml b/sledge/src/import/vector.ml index 53092b7f2..eb2f92d36 100644 --- a/sledge/src/import/vector.ml +++ b/sledge/src/import/vector.ml @@ -70,12 +70,14 @@ let map_preserving_phys_equal xs ~f = let mapi x ~f = v (Array.mapi (a x) ~f) let map2_exn x y ~f = v (Array.map2_exn (a x) (a y) ~f) +let map_inplace x ~f = Array.map_inplace (a x) ~f let fold_map x ~init ~f = let s, x = Array.fold_map (a x) ~init ~f in (s, v x) let concat xs = v (Array.concat (al xs)) +let copy x = v (Array.copy (a x)) let of_array = v let of_list x = v (Array.of_list x) let of_list_rev x = v (Array.of_list_rev x) diff --git a/sledge/src/import/vector.mli b/sledge/src/import/vector.mli index b025d1616..5b37018cd 100644 --- a/sledge/src/import/vector.mli +++ b/sledge/src/import/vector.mli @@ -86,8 +86,8 @@ val init : int -> f:(int -> 'a) -> 'a t (* val append : 'a t -> 'a t -> 'a t *) val concat : 'a t list -> 'a t +val copy : 'a t -> 'a t -(* val copy : 'a t -> 'a t *) (* val sub : ('a t, 'a t) Base__Blit_intf.sub *) (* val subo : ('a t, 'a t) Base__Blit_intf.subo *) @@ -153,6 +153,7 @@ val of_list_rev : 'a list -> 'a t (* val of_list_map : 'a list -> f:('a -> 'b) -> 'b t *) (* val of_list_rev_map : 'a list -> f:('a -> 'b) -> 'b t *) +val map_inplace : 'a t -> f:('a -> 'a) -> unit val find_exn : 'a t -> f:('a -> bool) -> 'a (* val find_map_exn : 'a t -> f:('a -> 'b option) -> 'b *) diff --git a/sledge/src/symbheap/term.ml b/sledge/src/symbheap/term.ml index 8dfd1e03c..cde3aff17 100644 --- a/sledge/src/symbheap/term.ml +++ b/sledge/src/symbheap/term.ml @@ -1046,50 +1046,76 @@ let of_exp e = (** Transform *) let map e ~f = - let map_ : (t -> t) -> t -> t = - fun map_ e -> - let map1 op ~f x = - let x' = f x in - if x' == x then e else norm1 op x' - in - let map2 op ~f x y = - let x' = f x in - let y' = f y in - if x' == x && y' == y then e else norm2 op x' y' - in - let map3 op ~f x y z = - let x' = f x in - let y' = f y in - let z' = f z in - if x' == x && y' == y && z' == z then e else norm3 op x' y' z' - in - let mapN op ~f xs = - let xs' = Vector.map_preserving_phys_equal ~f xs in - if xs' == xs then e else normN op xs' - in - let map_qset mk ~f args = - let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in - if args' == args then e else mk args' - in - match e with - | Add args -> map_qset addN ~f args - | Mul args -> map_qset mulN ~f args - | Ap1 (op, x) -> map1 op ~f x - | Ap2 (op, x, y) -> map2 op ~f x y - | Ap3 (op, x, y, z) -> map3 op ~f x y z - | ApN (op, xs) -> mapN op ~f xs - | RecN (op, xs) -> RecN (op, Vector.map ~f:map_ xs) - | _ -> e + let map1 op ~f x = + let x' = f x in + if x' == x then e else norm1 op x' + in + let map2 op ~f x y = + let x' = f x in + let y' = f y in + if x' == x && y' == y then e else norm2 op x' y' + in + let map3 op ~f x y z = + let x' = f x in + let y' = f y in + let z' = f z in + if x' == x && y' == y && z' == z then e else norm3 op x' y' z' in - fix map_ (fun e -> e) e + let mapN mk ~f xs = + let xs' = Vector.map_preserving_phys_equal ~f xs in + if xs' == xs then e else mk xs' + in + let map_qset mk ~f args = + let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in + if args' == args then e else mk args' + in + match e with + | Add args -> map_qset addN ~f args + | Mul args -> map_qset mulN ~f args + | Ap1 (op, x) -> map1 op ~f x + | Ap2 (op, x, y) -> map2 op ~f x y + | Ap3 (op, x, y, z) -> map3 op ~f x y z + | ApN (op, xs) -> mapN (normN op) ~f xs + | RecN (_, xs) -> + assert ( + xs == Vector.map_preserving_phys_equal ~f xs + || fail "Term.map does not support updating subterms of RecN." ) ; + e + | _ -> e + +(** Pre-order transformation that preserves cycles. Each subterm [x] from + root to leaves is presented to [f]. If [f x = Some x'] then the subterms + of [x] are not traversed and [x] is transformed to [x']. Otherwise + traversal proceeds to the subterms of [x], followed by rebuilding the + term structure on the transformed subterms. Cycles (through terms + involving [RecN]) are preserved. *) +let map_rec_pre ~f e = + let rec map_rec_pre_f memo e = + match f e with + | Some e' -> e' + | None -> ( + match e with + | RecN (op, xs) -> ( + match List.Assoc.find ~equal:( == ) memo e with + | None -> + let xs' = Vector.copy xs in + let e' = RecN (op, xs') in + let memo = List.Assoc.add ~equal:( == ) memo e e' in + let changed = ref false in + Vector.map_inplace xs' ~f:(fun x -> + let x' = map_rec_pre_f memo x in + if x' != x then changed := true ; + x' ) ; + if !changed then e' else e + | Some e' -> e' ) + | _ -> map ~f:(map_rec_pre_f memo) e ) + in + map_rec_pre_f [] e let rename sub e = - let rec rename_ sub e = - match e with - | Var _ -> Var.Subst.apply sub e - | _ -> map ~f:(rename_ sub) e - in - rename_ sub e |> check invariant + map_rec_pre e ~f:(function + | Var _ as v -> Some (Var.Subst.apply sub v) + | _ -> None ) (** Query *)