From e1e888f23935bfb34830fe160593e09df75a7f20 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 8 Mar 2024 08:03:37 +0100 Subject: Update the code generation --- compiler/ExtractBase.ml | 8 ++++++-- compiler/ExtractTypes.ml | 5 ----- 2 files changed, 6 insertions(+), 7 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index db887539..5aa8323e 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -782,9 +782,13 @@ let ctx_get_termination_measure (def_id : A.FunDeclId.id) let unop_name (unop : unop) : string = match unop with | Not -> ( - match !backend with FStar | Lean -> "not" | Coq -> "negb" | HOL4 -> "~") + match !backend with + | FStar -> "not" + | Lean -> "¬" + | Coq -> "negb" + | HOL4 -> "~") | Neg (int_ty : integer_type) -> ( - match !backend with Lean -> "-" | _ -> int_name int_ty ^ "_neg") + match !backend with Lean -> "-." | _ -> int_name int_ty ^ "_neg") | Cast _ -> (* We never directly use the unop name in this case *) raise (Failure "Unsupported") diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 51e3fd77..a3dbf3cc 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -31,11 +31,6 @@ let extract_literal (fmt : F.formatter) (inside : bool) (cv : literal) : unit = (* We need to add parentheses if the value is negative *) if sv.value >= Z.of_int 0 then F.pp_print_string fmt (Z.to_string sv.value) - else if !backend = Lean then - (* TODO: parsing issues with Lean because there are ambiguous - interpretations between int values and nat values *) - F.pp_print_string fmt - ("(-(" ^ Z.to_string (Z.neg sv.value) ^ ":Int))") else F.pp_print_string fmt ("(" ^ Z.to_string sv.value ^ ")"); (match !backend with | Coq -> -- cgit v1.2.3 From 44248ccfe3bfb8c45e5bb434d8dfb3dfa6e6b69c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 8 Mar 2024 09:42:29 +0100 Subject: Update the generation of constant bodies for Lean --- compiler/Extract.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 6c523549..0a21d4ec 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1863,8 +1863,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (fun fmt -> let body = match !backend with - | FStar -> "eval_global " ^ body_name - | Lean -> "eval_global " ^ body_name ^ " (by decide)" + | FStar | Lean -> "eval_global " ^ body_name | Coq -> body_name ^ "%global" | HOL4 -> "get_return_value " ^ body_name in -- cgit v1.2.3 From 5427563a8000f281ac614a2501fb9983beb44f21 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 23 Feb 2024 16:37:58 -0800 Subject: Fix tuple indexing for Lean backend --- compiler/Extract.ml | 37 +++++++++++++++++++++++++++++++++---- 1 file changed, 33 insertions(+), 4 deletions(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 0a21d4ec..d7ef5f34 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -577,12 +577,17 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) in (* Check if we extract the type as a tuple, and it only has one field. In this case, there is no projection. *) - let has_one_field = + let num_fields = match proj.adt_id with | TAdtId id -> ( let d = TypeDeclId.Map.find id ctx.trans_types in - match d.kind with Struct [ _ ] -> true | _ -> false) - | _ -> false + match d.kind with + | Struct fields -> Some (List.length fields) + | _ -> None) + | _ -> None + in + let has_one_field = + match num_fields with Some len -> len = 1 | None -> false in if is_tuple_struct && has_one_field then extract_texpression ctx fmt inside arg @@ -590,7 +595,31 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter) (* Exactly one argument: pretty-print *) let field_name = (* Check if we need to extract the type as a tuple *) - if is_tuple_struct then FieldId.to_string proj.field_id + if is_tuple_struct then + match !backend with + | FStar | HOL4 | Coq -> FieldId.to_string proj.field_id + | 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 *) + 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" else ctx_get_field proj.adt_id proj.field_id ctx in (* Open a box *) -- cgit v1.2.3 From a7452421be018e5d75065e2038f2f50042a80f3c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 8 Mar 2024 10:42:10 +0100 Subject: Update the code generated for tuple projectors --- compiler/Config.ml | 4 ++++ compiler/Extract.ml | 57 ++++++++++++++++++++++++++++++++++++----------------- compiler/Main.ml | 4 ++++ 3 files changed, 47 insertions(+), 18 deletions(-) (limited to 'compiler') 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 -- cgit v1.2.3