Skip to content

Commit c9ab370

Browse files
W95PspNadrieril
W95Psp
authored and
Nadrieril
committed
feat(engine/phases): intro. Drop_metasized 
1 parent 9625d1a commit c9ab370

File tree

2 files changed

+207
-0
lines changed

2 files changed

+207
-0
lines changed

‎engine/lib/phases/phase_drop_metasized.ml‎

Lines changed: 192 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,192 @@
1+
(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
2+
3+
open! Prelude
4+
5+
module%inlined_contents Make (F : Features.T) = struct
6+
open Ast
7+
module FA = F
8+
module FB = FA
9+
10+
include
11+
Phase_utils.MakeBase (F) (FB)
12+
(struct
13+
let phase_id = [%auto_phase_name auto]
14+
end)
15+
16+
module UA = Ast_utils.Make (F)
17+
18+
module Implem : ImplemT.T = struct
19+
let metadata = metadata
20+
21+
module S = struct
22+
include Features.SUBTYPE.Id
23+
end
24+
25+
[%%inline_defs dmutability + dsafety_kind]
26+
27+
let rec dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr option =
28+
let* kind = dimpl_expr_kind span i.kind in
29+
let* goal = dtrait_goal span i.goal in
30+
Some B.{ kind; goal }
31+
32+
and dtrait_goal (span : span) (r : A.trait_goal) : B.trait_goal option =
33+
let*? _ = not (Concrete_ident.eq_name Core__marker__MetaSized r.trait) in
34+
Some
35+
B.{ trait = r.trait; args = List.map ~f:(dgeneric_value span) r.args }
36+
37+
and dimpl_expr_exn message span i =
38+
match dimpl_expr span i with
39+
| None -> Error.assertion_failure span message
40+
| Some impl -> impl
41+
42+
and dimpl_ident (span : span) (r : A.impl_ident) : B.impl_ident option =
43+
let* goal = dtrait_goal span r.goal in
44+
Some B.{ goal; name = r.name }
45+
46+
and dty (span : span) (ty : A.ty) : B.ty =
47+
match ty with
48+
| TAssociatedType { impl; item } ->
49+
let impl =
50+
dimpl_expr_exn "MetaSized has no associated type" span impl
51+
in
52+
TAssociatedType { impl; item }
53+
| [%inline_arms "dty.*" - TAssociatedType] -> auto
54+
55+
and dprojection_predicate (span : span) (r : A.projection_predicate) :
56+
B.projection_predicate =
57+
{
58+
impl = dimpl_expr_exn "MetaSized cannot be projected" span r.impl;
59+
assoc_item = r.assoc_item;
60+
typ = dty span r.typ;
61+
}
62+
63+
and dimpl_expr_kind (span : span) (i : A.impl_expr_kind) :
64+
B.impl_expr_kind option =
65+
match i with
66+
| Parent { impl; ident } ->
67+
let* impl = dimpl_expr span impl in
68+
let* ident = dimpl_ident span ident in
69+
Some (B.Parent { impl; ident })
70+
| Projection { impl; item; ident } ->
71+
let impl = dimpl_expr_exn "MetaSized have no projection" span impl in
72+
let* ident = dimpl_ident span ident in
73+
Some (B.Projection { impl; item; ident })
74+
| ImplApp { impl; args } ->
75+
let* impl = dimpl_expr span impl in
76+
let args = List.filter_map ~f:(dimpl_expr span) args in
77+
Some (B.ImplApp { impl; args })
78+
| Builtin tr ->
79+
let* tr = dtrait_goal span tr in
80+
Some (B.Builtin tr)
81+
| Concrete tr ->
82+
let* tr = dtrait_goal span tr in
83+
Some (B.Concrete tr)
84+
| [%inline_arms
85+
"dimpl_expr_kind.*" - Parent - Projection - ImplApp - Builtin
86+
- Concrete] ->
87+
map (fun x ->
88+
Some
89+
(let result : B.impl_expr_kind = x in
90+
result))
91+
92+
and dexpr' (span : span) (expr : A.expr') : B.expr' =
93+
match expr with
94+
| App { f; args; generic_args; bounds_impls; trait } ->
95+
let dgeneric_values = List.map ~f:(dgeneric_value span) in
96+
App
97+
{
98+
f = dexpr f;
99+
args = List.map ~f:dexpr args;
100+
generic_args = dgeneric_values generic_args;
101+
bounds_impls = List.filter_map ~f:(dimpl_expr span) bounds_impls;
102+
trait =
103+
Option.map
104+
~f:
105+
(dimpl_expr_exn "MetaSized have no method" span
106+
*** dgeneric_values)
107+
trait;
108+
}
109+
| [%inline_arms "dexpr'.*" - App] -> auto
110+
[@@inline_ands
111+
bindings_of dty - dimpl_expr - dexpr' - dprojection_predicate
112+
- dimpl_expr_kind - dty - dimpl_ident]
113+
114+
let rec dimpl_item' (span : span) (ii : A.impl_item') : B.impl_item' =
115+
match ii with
116+
| IIType { typ; parent_bounds } ->
117+
IIType
118+
{
119+
typ = dty span typ;
120+
parent_bounds =
121+
List.filter_map
122+
~f:(fun (impl, ident) ->
123+
let* impl = dimpl_expr span impl in
124+
let* ident = dimpl_ident span ident in
125+
Some (impl, ident))
126+
parent_bounds;
127+
}
128+
(* | _ -> Obj.magic () *)
129+
| [%inline_arms "dimpl_item'.*" - IIType] -> auto
130+
131+
and dtrait_item' (span : span) (ti : A.trait_item') : B.trait_item' =
132+
match ti with
133+
| TIType idents -> TIType (List.filter_map ~f:(dimpl_ident span) idents)
134+
| [%inline_arms "dtrait_item'.*" - TIType] -> auto
135+
136+
and dgeneric_constraint (span : span)
137+
(generic_constraint : A.generic_constraint) :
138+
B.generic_constraint option =
139+
match generic_constraint with
140+
| GCLifetime (lf, witness) ->
141+
Some (B.GCLifetime (lf, S.lifetime span witness))
142+
| GCType impl_ident ->
143+
let* impl = dimpl_ident span impl_ident in
144+
Some (B.GCType impl)
145+
| GCProjection projection ->
146+
Some (B.GCProjection (dprojection_predicate span projection))
147+
148+
and dgenerics (span : span) (g : A.generics) : B.generics =
149+
{
150+
params = List.map ~f:(dgeneric_param span) g.params;
151+
constraints =
152+
List.filter_map ~f:(dgeneric_constraint span) g.constraints;
153+
}
154+
155+
and ditem' (span : span) (item : A.item') : B.item' =
156+
match item with
157+
| Impl
158+
{
159+
generics;
160+
self_ty;
161+
of_trait = trait_id, trait_generics;
162+
items;
163+
parent_bounds;
164+
safety;
165+
} ->
166+
B.Impl
167+
{
168+
generics = dgenerics span generics;
169+
self_ty = dty span self_ty;
170+
of_trait =
171+
(trait_id, List.map ~f:(dgeneric_value span) trait_generics);
172+
items = List.map ~f:dimpl_item items;
173+
parent_bounds =
174+
List.filter_map
175+
~f:(fun (impl, ident) ->
176+
let* impl = dimpl_expr span impl in
177+
let* ident = dimpl_ident span ident in
178+
Some (impl, ident))
179+
parent_bounds;
180+
safety = dsafety_kind span safety;
181+
}
182+
| [%inline_arms "ditem'.*" - Impl] -> auto
183+
[@@inline_ands
184+
"Item.*" - ditem' - dimpl_item' - dtrait_item' - dgeneric_constraint
185+
- dgenerics]
186+
187+
[%%inline_defs ditems]
188+
end
189+
190+
include Implem
191+
end
192+
[@@add "subtype.ml"]

‎engine/lib/phases/phase_drop_metasized.mli‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
(** This phase gets rid of the MetaSized bound. See https://github.com/cryspen/hax/pull/1534. *)
2+
3+
open! Prelude
4+
5+
module Make (F : Features.T) : sig
6+
include module type of struct
7+
module FA = F
8+
module FB = FA
9+
module A = Ast.Make (F)
10+
module B = Ast.Make (FB)
11+
module ImplemT = Phase_utils.MakePhaseImplemT (A) (B)
12+
end
13+
14+
include ImplemT.T
15+
end

0 commit comments

Comments
 (0)