diff options
| -rw-r--r-- | src/isail.ml | 21 | ||||
| -rw-r--r-- | src/slice.ml | 5 | ||||
| -rw-r--r-- | src/slice.mli | 2 |
3 files changed, 24 insertions, 4 deletions
diff --git a/src/isail.ml b/src/isail.ml index 094ad3df..8df34b13 100644 --- a/src/isail.ml +++ b/src/isail.ml @@ -266,6 +266,10 @@ let help = | ":compile" -> sprintf ":compile %s - Compile AST to a specified target, valid targets are lem, coq, ocaml, c, and ir (intermediate representation)" (color yellow "<target>") + | ":slice" -> + ":slice - Slice AST to the definitions which the functions given by :slice_roots depend on, up to the functions given by :slice_cuts" + | ":thin_slice" -> + ":thin_slice - Slice AST to the function definitions given with :slice_roots" | "" -> sprintf "Type %s for a list of commands, and %s %s for information about a specific command" (color green ":commands") (color green ":help") (color yellow "<command>") @@ -540,7 +544,22 @@ let handle_input' input = let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in let cuts = !slice_cuts |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in let g = G.prune roots cuts g in - Interactive.ast := Slice.filter_ast !slice_cuts g !Interactive.ast + Interactive.ast := Slice.filter_ast cuts g !Interactive.ast + | ":thin_slice" -> + let open Slice in + let module SliceNodeSet = Set.Make(Slice.Node) in + let module SliceNodeMap = Map.Make(Slice.Node) in + let module G = Graph.Make(Slice.Node) in + let g = Slice.graph_of_ast !Interactive.ast in + let roots = !slice_roots |> IdSet.elements |> List.map (fun id -> Function id) |> SliceNodeSet.of_list in + let keep = function + | (Function id,_) when IdSet.mem id (!slice_roots) -> None + | (Function id,_) -> Some (Function id) + | _ -> None + in + let cuts = SliceNodeMap.bindings g |> Util.map_filter keep |> SliceNodeSet.of_list in + let g = G.prune roots cuts g in + Interactive.ast := Slice.filter_ast cuts g !Interactive.ast | ":list_rewrites" -> let print_rewrite (name, rw) = print_endline (name ^ " " ^ Util.(String.concat " " (describe_rewrite rw) |> yellow |> clear)) diff --git a/src/slice.ml b/src/slice.ml index aec569cd..9dee4761 100644 --- a/src/slice.ml +++ b/src/slice.ml @@ -305,9 +305,10 @@ let id_of_reg_dec (DEC_aux (aux, _)) = let filter_ast cuts g (Defs defs) = let rec filter_ast' g = + let module NS = Set.Make(Node) in let module NM = Map.Make(Node) in function - | DEF_fundef fdef :: defs when IdSet.mem (id_of_fundef fdef) cuts -> filter_ast' g defs + | DEF_fundef fdef :: defs when NS.mem (Function (id_of_fundef fdef)) cuts -> filter_ast' g defs | DEF_fundef fdef :: defs when NM.mem (Function (id_of_fundef fdef)) g -> DEF_fundef fdef :: filter_ast' g defs | DEF_fundef _ :: defs -> filter_ast' g defs @@ -327,7 +328,7 @@ let filter_ast cuts g (Defs defs) = | DEF_type tdef :: defs when NM.mem (Type (id_of_typedef tdef)) g -> DEF_type tdef :: filter_ast' g defs | DEF_type _ :: defs -> filter_ast' g defs - | DEF_measure (id,_,_) :: defs when IdSet.mem id cuts -> filter_ast' g defs + | DEF_measure (id,_,_) :: defs when NS.mem (Function id) cuts -> filter_ast' g defs | (DEF_measure (id,_,_) as def) :: defs when NM.mem (Function id) g -> def :: filter_ast' g defs | DEF_measure _ :: defs -> filter_ast' g defs diff --git a/src/slice.mli b/src/slice.mli index 04f140fe..0c15defb 100644 --- a/src/slice.mli +++ b/src/slice.mli @@ -68,4 +68,4 @@ val graph_of_ast : Type_check.tannot defs -> Graph.Make(Node).graph val dot_of_ast : out_channel -> Type_check.tannot defs -> unit -val filter_ast : IdSet.t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs +val filter_ast : Set.Make(Node).t -> Graph.Make(Node).graph -> Type_check.tannot defs -> Type_check.tannot defs |