diff options
| author | Aymeric Fromherz | 2024-05-23 11:33:46 +0200 |
|---|---|---|
| committer | Aymeric Fromherz | 2024-05-23 11:44:28 +0200 |
| commit | 7238177f5c7cff15f924e13c01d5b3b4802daf77 (patch) | |
| tree | fa4c0fed38383baa2f5791d310e2424c04ddf4a6 /compiler | |
| parent | e660a4d575ba55bd23c64b5bd7b4e435be82d7ed (diff) | |
Do not expand field projector for recursive structs to a let binding in Lean
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 6c925bcd..351f5cf2 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2902,14 +2902,9 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value) - if the ADT is an enumeration (which must have exactly one branch) - if we forbid using field projectors. *) - let is_rec_def = - T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls - in let use_let_with_cons = is_enum || !Config.dont_use_field_projectors - (* TODO: for now, we don't have field projectors over recursive ADTs in Lean. *) - || (!Config.backend = Lean && is_rec_def) (* Also, there is a special case when the ADT is to be extracted as a tuple, because it is a structure with unnamed fields. Some backends like Lean have projectors for tuples (like so: `x.3`), but others |