diff options
| author | Son HO | 2024-05-24 17:08:42 +0200 |
|---|---|---|
| committer | GitHub | 2024-05-24 17:08:42 +0200 |
| commit | fbfa0e13ab56ee847e891fa7d798d2eb226b6794 (patch) | |
| tree | 58f0a2de653f57a986bb5e5f26453a1fbdf0ef17 /compiler/SymbolicToPure.ml | |
| parent | 0baa0519cf477fe1fa447417585960fc811bcae9 (diff) | |
| parent | 169af47945f013e61b14d67e7ebdc9c03636c5a2 (diff) | |
Merge pull request #194 from AeneasVerif/afromher/recursive_projectors
Support field projectors for recursive structs in Lean backend
Diffstat (limited to '')
| -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 8dfe0abe..d6d2e018 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2903,14 +2903,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 |