summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2024-03-08 10:42:10 +0100
committerSon Ho2024-03-08 10:42:10 +0100
commita7452421be018e5d75065e2038f2f50042a80f3c (patch)
tree700439fbe96ea5980216e06b388e863ed8ac314b /compiler
parent5427563a8000f281ac614a2501fb9983beb44f21 (diff)
Update the code generated for tuple projectors
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Config.ml4
-rw-r--r--compiler/Extract.ml57
-rw-r--r--compiler/Main.ml4
3 files changed, 47 insertions, 18 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index 2bb1ca34..3b0070c0 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -469,3 +469,7 @@ let use_tuple_structs = ref true
let backend_has_tuple_projectors () =
match !backend with Lean -> true | Coq | FStar | HOL4 -> false
+
+(** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do
+ we use better projector syntax? *)
+let use_nested_tuple_projectors = ref false
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 *)
diff --git a/compiler/Main.ml b/compiler/Main.ml
index 0b8ec439..4a2d01dc 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -123,6 +123,10 @@ let () =
( "-split-fwd-back",
Arg.Clear return_back_funs,
" Split the forward and backward functions." );
+ ( "-tuple-nested-proj",
+ Arg.Set use_nested_tuple_projectors,
+ " Use nested projectors for tuples (e.g., (0, 1).snd.fst instead of \
+ (0, 1).1)." );
]
in