diff options
Diffstat (limited to 'compiler/SymbolicToPure.ml')
| -rw-r--r-- | compiler/SymbolicToPure.ml | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 71f8e4fc..848bfe50 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 @@ -3534,10 +3529,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ] else output in - let output = - if effect_info.can_fail && inputs <> [] then mk_result_ty output - else output - in + let output = if effect_info.can_fail then mk_result_ty output else output in (back_info, output) in |