Skip to content

Commit 5fa9ee8

Browse files
committed
wip:trying to add ETApp for generic vtable pointer
1 parent 85f6fa8 commit 5fa9ee8

File tree

1 file changed

+15
-3
lines changed

1 file changed

+15
-3
lines changed

lib/AstOfLlbc.ml

Lines changed: 15 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1873,23 +1873,35 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr =
18731873
let trait_impl = env.get_nth_trait_impl id in
18741874
begin
18751875
match trait_impl.vtable with
1876-
| Some instance -> { instance with C.generics }
1876+
| Some instance -> { instance with generics }
18771877
| None -> failwith "Trait impl has no vtable instance"
18781878
end
18791879
| _ -> failwith "unsupported trait_ref kind in unsize cast"
18801880
in
18811881
let instance_def = env.get_nth_global vtable_instance.C.id in
1882-
let instance_ty =
1882+
let generic_typs = List.map (typ_of_ty env) vtable_instance.generics.types in
1883+
let cgs = List.map (expression_of_const_generic env) vtable_instance.generics.const_generics in
1884+
let ret_typ =
18831885
let subst =
18841886
Charon.Substitute.make_subst_from_generics instance_def.generics
18851887
vtable_instance.generics
18861888
in
18871889
let real_ty = Charon.Substitute.(ty_substitute subst instance_def.ty) in
18881890
typ_of_ty env real_ty
18891891
in
1890-
let vtable_instance =
1892+
L.log "Ast" "[debug] ret_typ:%a\n" ptyp ret_typ;
1893+
(* let ret_typ = typ_of_ty env instance_def.ty in *)
1894+
let instance_ty =
1895+
let ts = { K.n = List.length generic_typs; K.n_cgs = List.length cgs } in
1896+
K.TPoly (ts, ret_typ)
1897+
(* List.fold_right (fun t acc -> K.TArrow (t, acc)) generic_typs ret_typ *)
1898+
in
1899+
let vtable_func_head =
18911900
K.with_type instance_ty (K.EQualified (lid_of_name env instance_def.item_meta.name))
18921901
in
1902+
let vtable_instance =
1903+
K.with_type ret_typ (K.ETApp (vtable_func_head, cgs, [], generic_typs))
1904+
in
18931905
addrof vtable_instance
18941906
in
18951907
let coercion =

0 commit comments

Comments
 (0)