Merge branch 'main' into doc

hacspec · Nov 17, 2023 · 00c73bc · 00c73bc
2 parents 8c940ec + 773b342
commit 00c73bc
Show file tree

Hide file tree

Showing 6 changed files with 44 additions and 2 deletions.
diff --git 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

diff --git 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

diff --git 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
@@ -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
@@ -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
@@ -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<T: FooTrait>() -> usize {
+    <T as FooTrait>::ASSOCIATED_CONSTANT + INHERENT_CONSTANT
+}