From 14904e91c63f12bce3eabcb1b46fb8d2d6ede487 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Wed, 30 Oct 2024 19:48:24 +0100 Subject: [PATCH] Add prefix to names --- engine/backends/coq/coq/coq_backend.ml | 21 ++++++++++++- .../toolchain__literals into-coq.snap | 30 +++++++++---------- .../toolchain__reordering into-coq.snap | 4 +-- 3 files changed, 37 insertions(+), 18 deletions(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 2db7c6cee..1611f2286 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -64,10 +64,27 @@ struct let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend)) end +(* module CoqNamePolicy = Concrete_ident.DefaultNamePolicy *) +module CoqNamePolicy = struct + (* include Concrete_ident.DefaultNamePolicy *) + + let reserved_words : string Hash_set.t = Hash_set.of_list (module String) ["Definition"; "Inductive"; "match"; "if"; "then"; "else"; "as"; "into"; "end"; "Record"; "Arguments"; "Type"] (* TODO: Make complete *) + (** List of all words that have a special meaning in the target + language, and that should thus be escaped. *) + + let index_field_transform x : string = x (* tuple struct, field `0` *) + (** Transformation applied to indexes fields name (i.e. [x.1]) *) + + let field_name_transform : struct_name:string -> string -> string = fun ~struct_name x -> + struct_name ^ "_" ^ x + + let enum_constructor_name_transform : enum_name:string -> string -> string = fun ~enum_name x -> x + let struct_constructor_name_transform : string -> string = fun x -> x +end + module AST = Ast.Make (InputLanguage) module BackendOptions = Backend.UnitBackendOptions open Ast -module CoqNamePolicy = Concrete_ident.DefaultNamePolicy module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy) open AST @@ -127,6 +144,8 @@ struct object (self) inherit BasePrinter.base + val concrete_ident_view = (module U.Concrete_ident_view : Concrete_ident.VIEW_API) + method private primitive_to_string (id : primitive_ident) : document = match id with | Deref -> default_document_for "(TODO: Deref)" diff --git a/test-harness/src/snapshots/toolchain__literals into-coq.snap b/test-harness/src/snapshots/toolchain__literals into-coq.snap index 77d4150c3..930e617a0 100644 --- a/test-harness/src/snapshots/toolchain__literals into-coq.snap +++ b/test-harness/src/snapshots/toolchain__literals into-coq.snap @@ -47,13 +47,13 @@ Export Hax_lib (t_int). Record t_Foo : Type := { - f_field : t_u8; + Foo_f_field : t_u8; }. Arguments t_Foo:clear implicits. Arguments t_Foo. Arguments Build_t_Foo. #[export] Instance settable_t_Foo : Settable _ := - settable! (@Build_t_Foo) . + settable! (@Build_t_Foo) . (* NotImplementedYet *) @@ -76,18 +76,18 @@ Definition fn_pointer_cast (_ : unit) : unit := x in tt. -Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 := - let _ : t_Int := f_lift (3) in - let _ := f_gt (impl__Int___unsafe_from_str ("-340282366920938463463374607431768211455000"%string)) (impl__Int___unsafe_from_str ("340282366920938463463374607431768211455000"%string)) in - let _ := f_lt (x) (x) in - let _ := f_ge (x) (x) in - let _ := f_le (x) (x) in - let _ := f_ne (x) (x) in - let _ := f_eq (x) (x) in - let _ := f_add (x) (x) in - let _ := f_sub (x) (x) in - let _ := f_mul (x) (x) in - let _ := f_div (x) (x) in +Definition math_integers (x : t_Int) `{andb (PartialOrd_f_gt (x) (impl__Int___unsafe_from_str ("0"%string))) (PartialOrd_f_lt (x) (impl__Int___unsafe_from_str ("16"%string))) = true} : t_u8 := + let _ : t_Int := Abstraction_f_lift (3) in + let _ := PartialOrd_f_gt (impl__Int___unsafe_from_str ("-340282366920938463463374607431768211455000"%string)) (impl__Int___unsafe_from_str ("340282366920938463463374607431768211455000"%string)) in + let _ := PartialOrd_f_lt (x) (x) in + let _ := PartialOrd_f_ge (x) (x) in + let _ := PartialOrd_f_le (x) (x) in + let _ := PartialEq_f_ne (x) (x) in + let _ := PartialEq_f_eq (x) (x) in + let _ := Add_f_add (x) (x) in + let _ := Sub_f_sub (x) (x) in + let _ := Mul_f_mul (x) (x) in + let _ := Div_f_div (x) (x) in let _ : t_i16 := impl__Int__to_i16 (x) in let _ : t_i32 := impl__Int__to_i32 (x) in let _ : t_i64 := impl__Int__to_i64 (x) in @@ -98,7 +98,7 @@ Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl__Int___unsafe_from_s let _ : t_u64 := impl__Int__to_u64 (x) in let _ : t_u128 := impl__Int__to_u128 (x) in let _ : t_usize := impl__Int__to_usize (x) in - impl__Int__to_u8 (f_add (x) (f_mul (x) (x))). + impl__Int__to_u8 (Add_f_add (x) (Mul_f_mul (x) (x))). Definition numeric (_ : unit) : unit := let _ : t_usize := 123 in diff --git a/test-harness/src/snapshots/toolchain__reordering into-coq.snap b/test-harness/src/snapshots/toolchain__reordering into-coq.snap index d3b0567d8..aafff19ec 100644 --- a/test-harness/src/snapshots/toolchain__reordering into-coq.snap +++ b/test-harness/src/snapshots/toolchain__reordering into-coq.snap @@ -49,13 +49,13 @@ Arguments t_Foo. Record t_Bar : Type := { - 0 : t_Foo; + Bar_0 : t_Foo; }. Arguments t_Bar:clear implicits. Arguments t_Bar. Arguments Build_t_Bar. #[export] Instance settable_t_Bar : Settable _ := - settable! (@Build_t_Bar) <0>. + settable! (@Build_t_Bar) . Definition t_Foo_cast_to_repr (x : t_Foo) : t_isize := match x with