From 6c42629b1d1088427b4f032bb0c81766816f371f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 16 Nov 2023 10:11:01 +0100 Subject: [PATCH 1/3] fix(engine): `NamedConsts` are `GlobalVar`s of kind `AssociatedItem Value` --- engine/lib/import_thir.ml | 6 +++++- .../src/snapshots/toolchain__naming into-coq.snap | 10 ++++++++++ .../src/snapshots/toolchain__naming into-fstar.snap | 10 ++++++++++ tests/naming/src/lib.rs | 9 +++++++++ 4 files changed, 34 insertions(+), 1 deletion(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index c02a8d498..90dd1c55f 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -602,7 +602,11 @@ end) : EXPR = struct typ = TInt { size = S8; signedness = Unsigned }; }) l)) - | NamedConst { def_id = id; _ } -> GlobalVar (def_id Value id) + | NamedConst { def_id = id; impl; _ } -> + let kind : Concrete_ident.Kind.t = + match impl with Some _ -> AssociatedItem Value | _ -> Value + in + GlobalVar (def_id kind id) | Closure { body; params; upvars; _ } -> let params = List.filter_map ~f:(fun p -> Option.map ~f:c_pat p.pat) params diff --git a/test-harness/src/snapshots/toolchain__naming into-coq.snap b/test-harness/src/snapshots/toolchain__naming into-coq.snap index f159f2484..e4d1f617e 100644 --- a/test-harness/src/snapshots/toolchain__naming into-coq.snap +++ b/test-harness/src/snapshots/toolchain__naming into-coq.snap @@ -60,6 +60,10 @@ Inductive t_Foo2 : Type := | Foo2_At_Foo2 | Foo2_B : Foo2_B -> t_Foo2. +Class t_FooTrait Self := { + f_ASSOCIATED_CONSTANT:uint_size ; +}. + Class t_T1 Self := { }. @@ -80,6 +84,12 @@ Instance t_Foo_t_t_T3_e_for_a : t_T3_e_for_a t_Foo_t := { (*Not implemented yet? todo(item)*) +Definition v_INHERENT_CONSTANT : uint_size := + (@repr WORDSIZE32 3). + +Definition constants : uint_size := + f_ASSOCIATED_CONSTANT.+v_INHERENT_CONSTANT. + Definition ff__g : unit := tt. diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index 78a9935df..b311c2a54 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -48,6 +48,8 @@ type t_Foo2 = | Foo2_A : t_Foo2 | Foo2_B { f_x:usize }: t_Foo2 +class t_FooTrait (v_Self: Type) = { f_ASSOCIATED_CONSTANT:usize } + class t_T1 (v_Self: Type) = { __marker_trait_t_T1:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] @@ -63,6 +65,14 @@ class t_T3_e_for_a (v_Self: Type) = { __marker_trait_t_T3_e_for_a:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () } +let v_INHERENT_CONSTANT: usize = sz 3 + +let constants + (#v_T: Type) + (#[FStar.Tactics.Typeclasses.tcresolve ()] ii0: Core.Marker.t_Sized v_T) + (#[FStar.Tactics.Typeclasses.tcresolve ()] ii1: t_FooTrait v_T) + : usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT + let ff__g: Prims.unit = () type t_f__g__impl__g__Foo = diff --git a/tests/naming/src/lib.rs b/tests/naming/src/lib.rs index b66a86615..ce722cf71 100644 --- a/tests/naming/src/lib.rs +++ b/tests/naming/src/lib.rs @@ -96,3 +96,12 @@ fn construct_structs(a: usize, b: usize) { let _ = StructC { a }; let _ = StructD { a, b }; } + +const INHERENT_CONSTANT: usize = 3; +trait FooTrait { + const ASSOCIATED_CONSTANT: usize; +} + +fn constants() -> usize { + ::ASSOCIATED_CONSTANT + INHERENT_CONSTANT +} From ab24ab98d92445c7839cb32de7d86fd907fb08d7 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 16 Nov 2023 14:14:31 +0100 Subject: [PATCH 2/3] fix(setup.sh): fix `DUNEJOBS` unset warning --- .utils/rebuild.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/.utils/rebuild.sh b/.utils/rebuild.sh index 5569caf8b..9a58e1f2b 100755 --- a/.utils/rebuild.sh +++ b/.utils/rebuild.sh @@ -17,6 +17,7 @@ if [[ "${1:-}" == "--online" ]]; then fi TARGETS="${1:-rust ocaml}" +DUNEJOBS=${DUNEJOBS:-} # required since `set -u` YELLOW=43 GREEN=42 From 1cb09fbe64dc457f4f2d9611a0d7ae2d7216abfe Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 15 Nov 2023 16:04:31 +0100 Subject: [PATCH 3/3] fix(engine): fixes issue #360 --- engine/lib/concrete_ident/concrete_ident.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index b55004648..ff294ee3f 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -137,7 +137,15 @@ end = struct let did : Imported.def_id = { krate; path } in match find did with | Some infos -> Some (infos, before, after) - | None -> failwith "invariant error" + | None -> + (* TODO: This happens in actual code but should not, see #363 and #360. + Make this into an error when #363 is fixed. *) + Logs.warn (fun m -> + m + "concrete_ident: invariant error, no `impl_info` found for \ + identifier `%s`." + ([%show: Imported.def_id] did)); + None end module Kind = struct