From 36fd3c158c08af5b48d9801a607f3be812d2ecc7 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 29 Jan 2019 18:46:58 +0000
Subject: Add an option to crudely slice a function out of a Sail model Not
 ideal because it keeps everything that's not a function, but good enough for
 quick tests extracted from arm.

---
 src/specialize.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/specialize.mli')

diff --git a/src/specialize.mli b/src/specialize.mli
index f2c94a48..28029747 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -71,3 +71,6 @@ val specialize : tannot defs -> Env.t -> tannot defs * Env.t
 val instantiations_of : id -> tannot defs -> typ_arg KBindings.t list
 
 val string_of_instantiation : typ_arg KBindings.t -> string
+
+(* Remove all function definitions except for the given set *)
+val slice_defs : Env.t -> tannot defs -> IdSet.t -> tannot defs
-- 
cgit v1.2.3