diff options
| author | Son HO | 2024-03-08 16:51:40 +0100 |
|---|---|---|
| committer | GitHub | 2024-03-08 16:51:40 +0100 |
| commit | 169d011cbfa83d853d0148bbf6b946e6ccbe4c4c (patch) | |
| tree | ed8953634d14313d5b7d6ad204343d64eb990baf /compiler/ReorderDecls.ml | |
| parent | b604bb9935007a1f0e9c7f556f8196f0e14c85ce (diff) | |
| parent | 873deb005b394aca3090497e6c21ab9f8c2676be (diff) | |
Merge pull request #83 from AeneasVerif/son/backs
Remove the option to split the forward/backward functions
Diffstat (limited to '')
| -rw-r--r-- | compiler/ReorderDecls.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/compiler/ReorderDecls.ml b/compiler/ReorderDecls.ml index 53c94ff4..f5443e03 100644 --- a/compiler/ReorderDecls.ml +++ b/compiler/ReorderDecls.ml @@ -5,11 +5,7 @@ open Pure (** The local logger *) let log = Logging.reorder_decls_log -type fun_id = { - def_id : FunDeclId.id; - lp_id : LoopId.id option; - rg_id : T.RegionGroupId.id option; -} +type fun_id = { def_id : FunDeclId.id; lp_id : LoopId.id option } [@@deriving show, ord] module FunIdOrderedType : OrderedType with type t = fun_id = struct @@ -43,11 +39,11 @@ let compute_body_fun_deps (e : texpression) : FunIdSet.t = | FunOrOp (Fun fid) -> ( match fid with | Pure _ -> () - | FromLlbc (fid, lp_id, rg_id) -> ( + | FromLlbc (fid, lp_id) -> ( match fid with | FunId (FAssumed _) -> () | TraitMethod (_, _, fid) | FunId (FRegular fid) -> - let id = { def_id = fid; lp_id; rg_id } in + let id = { def_id = fid; lp_id } in ids := FunIdSet.add id !ids)) end in @@ -71,7 +67,7 @@ let group_reorder_fun_decls (decls : fun_decl list) : (bool * fun_decl list) list = let module IntMap = MakeMap (OrderedInt) in let get_fun_id (decl : fun_decl) : fun_id = - { def_id = decl.def_id; lp_id = decl.loop_id; rg_id = decl.back_id } + { def_id = decl.def_id; lp_id = decl.loop_id } in (* Compute the list/set of identifiers *) let idl = List.map get_fun_id decls in |