diff options
| author | Son Ho | 2023-08-03 16:21:43 +0200 |
|---|---|---|
| committer | Son Ho | 2023-08-03 16:21:43 +0200 |
| commit | 931fabe3e8590815548d606b33fc8db31e9f6010 (patch) | |
| tree | ba99ca0412c8e08cd8e89edbbd287c3b306ebfd8 /compiler/PureMicroPasses.ml | |
| parent | fa682c18c8ffc5fa7224d9e9d0e0dd94250ada57 (diff) | |
Fix an issue with the extraction of aggregated arrays
Diffstat (limited to '')
| -rw-r--r-- | compiler/PureMicroPasses.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index 00620c58..58a5f9e2 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -611,7 +611,7 @@ let intro_struct_updates (ctx : trans_ctx) (def : fun_decl) : fun_decl = (!Config.backend <> Lean && !Config.backend <> Coq) || not is_rec then - let struct_id = adt_id in + let struct_id = AdtId adt_id in let init = None in let updates = FieldId.mapi @@ -1168,8 +1168,8 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl = Var v ) -> (* We check that this is the proper ADT, and the proper field *) if - proj_adt_id = struct_id && field_id = fid - && x.ty = adt_ty + AdtId proj_adt_id = struct_id + && field_id = fid && x.ty = adt_ty then Some v else None | _ -> None) |