Skip to content

Commit f9a2a4d

Browse files
dc-makkmemarian
authored andcommitted
(frontend/translation_effect) Remove unused code
Whilst trying to understand how scoping is handled by the Core elaboration, I came across these functions and spent a bit too long trying to find where and how they are used before realising with_block_objects is the only important function for this. Hence, delete.
1 parent e88d46c commit f9a2a4d

1 file changed

Lines changed: 0 additions & 24 deletions

File tree

frontend/model/translation_effect.lem

Lines changed: 0 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -70,30 +70,6 @@ let wrapped_fresh_symbol_ descr bTy =
7070
let sym = Symbol.fresh_description descr in
7171
return (sym, Caux.mk_sym_pat sym bTy, Caux.mk_sym_pe sym)
7272

73-
74-
(* TODO: this does not need to be in the monad *)
75-
(* val wrapped_fresh_symbol_descr: C.core_base_type -> Symbol.symbol_description -> elabM (Symbol.sym * C.pattern * C.pexpr)
76-
* let wrapped_fresh_symbol_descr bTy descr =
77-
* let sym = Symbol.fresh_description descr in
78-
* return (sym, Caux.mk_sym_pat sym bTy, Caux.mk_sym_pe sym) *)
79-
80-
(* register C objects from block scope. *)
81-
val push_block_objects: list (Symbol.sym * (Ctype.qualifiers * Ctype.ctype)) -> elabM unit
82-
let push_block_objects binds = fun st ->
83-
((), <| st with
84-
visible_objects_types= List.foldl (fun acc (sym, qs_ty) -> Map.insert sym qs_ty acc) st.visible_objects_types binds;
85-
visible_objects= (List.map fst binds) :: st.visible_objects
86-
|>)
87-
88-
(* forget C objects from the most recent block. *)
89-
val pop_block_objects: elabM unit
90-
let pop_block_objects = fun st ->
91-
((), <| st with visible_objects=
92-
match st.visible_objects with
93-
| _ :: xs -> xs
94-
| _ -> error "[Translation.E.pop_block_objects] found an ill-formed scope stack."
95-
end |>)
96-
9773
val cheri_const_alias_map: elabM (map Symbol.sym Symbol.sym)
9874
let cheri_const_alias_map = fun st ->
9975
(st.cheri_const_alias, st)

0 commit comments

Comments
 (0)