From 745369b83c85afcaec68650a1381331faa161b16 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 2 Feb 2021 04:35:17 -0800 Subject: [PATCH] [sledge] Implement Context.norm in terms of Theory.map_solvables Reviewed By: jvillard Differential Revision: D25883726 fbshipit-source-id: 8def2fd85 --- sledge/src/fol/context.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index 8c49d8c90..c59d8c2ad 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -68,12 +68,11 @@ end = struct let subst s e = Term.map_trms ~f:(subst_ s) e (** apply a substitution to maximal non-interpreted subterms *) - let rec norm s a = + let norm s a = [%trace] ~call:(fun {pf} -> pf "@ %a" Trm.pp a) ~retn:(fun {pf} -> pf "%a" Trm.pp) - @@ fun () -> - if Theory.is_interpreted a then Trm.map ~f:(norm s) a else apply s a + @@ fun () -> Theory.map_solvables ~f:(apply s) a (** compose two substitutions *) let compose r s =