diff options
Diffstat (limited to 'compiler/Extract.ml')
-rw-r--r-- | compiler/Extract.ml | 57 |
1 files changed, 39 insertions, 18 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index d7ef5f34..dbca4f8f 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -601,25 +601,46 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) | Lean -> (* Tuples in Lean are syntax sugar for nested products/pairs, so we need to map the field id accordingly. - A field id i maps to: - (.2)^i if i is the last element of the tuple - (.2)^i.1 otherwise - where (.2)^i denotes .2 repeated i times. - For example, 3 maps to .2.2.2 if the tuple has 4 fields and - to .2.2.2.1 if it has more than 4 fields. - Note that the first "." is added below *) + + We give two possibilities: + - either we use the custom syntax [.#i], like in: [(0, 1).#1] + - or we introduce nested projections which use the field + projectors [.1] and [.2], like in: [(0, 1).2.1] + + This necessary in some situations, for instance if we have + in Rust: + {[ + struct Tuple(u32, (u32, u32)); + ]} + + The issue comes from the fact that in Lean [A * B * C] and [A * (B * + C)] are the same type. As a result, in Rust, field 1 of [Tuple] is + the pair (an element of type [(u32, u32)]), however in Lean it would + be the first element of the pair (an element of type [u32]). If such + situations happen, we allow to force using the nested projectors by + providing the proper command line argument. TODO: we can actually + check the type to determine exactly when we need to use nested + projectors and when we don't. + + When using nested projectors, a field id i maps to: + - (.2)^i if i is the last element of the tuple + - (.2)^i.1 otherwise + where (.2)^i denotes .2 repeated i times. + For example, 3 maps to .2.2.2 if the tuple has 4 fields and + to .2.2.2.1 if it has more than 4 fields. + Note that the first "." is added below. + *) let field_id = FieldId.to_int proj.field_id in - (* Helper: repeat "2.2.2..." *) - let rec repeat_snd n = - match n with - | 0 -> "" - | 1 -> "2" - | _ -> "2." ^ repeat_snd (n - 1) - in - let twos_prefix = repeat_snd field_id in - if field_id + 1 = Option.get num_fields then twos_prefix - else if field_id = 0 then "1" - else twos_prefix ^ ".1" + if !Config.use_nested_tuple_projectors then + (* Nested projection: "2.2.2..." *) + if field_id = 0 then "1" + else + let twos_prefix = + String.concat "." (Collections.List.repeat field_id "2") + in + if field_id + 1 = Option.get num_fields then twos_prefix + else twos_prefix ^ ".1" + else "#" ^ string_of_int field_id else ctx_get_field proj.adt_id proj.field_id ctx in (* Open a box *) |