From c46cd13fb68d02f4a1da7c3ce8874d54ef68d7f8 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Tue, 14 Jan 2025 14:38:25 +0100 Subject: [PATCH] Add type arguments for associated constants. --- engine/lib/import_thir.ml | 8 ++++++-- .../src/snapshots/toolchain__naming into-fstar.snap | 2 +- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 356b8eb07..2b265117a 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -730,14 +730,18 @@ end) : EXPR = struct typ = TInt { size = S8; signedness = Unsigned }; }) l)) - | NamedConst { def_id = id; impl; _ } -> ( + | NamedConst { def_id = id; impl; args; _ } -> ( let kind : Concrete_ident.Kind.t = match impl with Some _ -> AssociatedItem Value | _ -> Value in let f = GlobalVar (def_id kind id) in match impl with | Some impl -> - let trait = Some (c_impl_expr e.span impl, []) in + let trait = + Some + ( c_impl_expr e.span impl, + List.map ~f:(c_generic_value e.span) args ) + in let f = { e = f; span; typ = TArrow ([], typ) } in App { f; trait; args = []; generic_args = []; bounds_impls = [] } | _ -> f) diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index f25ae1575..01f4b474e 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -158,7 +158,7 @@ let constants (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T) (_: Prims.unit) : usize = - (f_ASSOCIATED_CONSTANT #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT + (f_ASSOCIATED_CONSTANT #v_T #FStar.Tactics.Typeclasses.solve <: usize) +! v_INHERENT_CONSTANT let construct_structs (a b: usize) : Prims.unit = let _:t_StructA = { f_a = a } <: t_StructA in