1use super::translate_ctx::*;
3use charon_lib::ast::*;
4use hax_frontend_exporter as hax;
5
6impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
7 fn translate_constant_literal_to_raw_constant_expr(
8 &mut self,
9 span: Span,
10 v: &hax::ConstantLiteral,
11 ) -> Result<RawConstantExpr, Error> {
12 let lit = match v {
13 hax::ConstantLiteral::ByteStr(bs) => Literal::ByteStr(bs.clone()),
14 hax::ConstantLiteral::Str(..) => {
15 raise_error!(self, span, "found a `str` constants not behind a reference")
18 }
19 hax::ConstantLiteral::Char(c) => Literal::Char(*c),
20 hax::ConstantLiteral::Bool(b) => Literal::Bool(*b),
21 hax::ConstantLiteral::Int(i) => {
22 use hax::ConstantInt;
23 let scalar = match i {
24 ConstantInt::Int(v, int_type) => {
25 use hax::IntTy;
26 match int_type {
27 IntTy::Isize => ScalarValue::Isize(*v as i64),
28 IntTy::I8 => ScalarValue::I8(*v as i8),
29 IntTy::I16 => ScalarValue::I16(*v as i16),
30 IntTy::I32 => ScalarValue::I32(*v as i32),
31 IntTy::I64 => ScalarValue::I64(*v as i64),
32 IntTy::I128 => ScalarValue::I128(*v),
33 }
34 }
35 ConstantInt::Uint(v, int_type) => {
36 use hax::UintTy;
37 match int_type {
38 UintTy::Usize => ScalarValue::Usize(*v as u64),
39 UintTy::U8 => ScalarValue::U8(*v as u8),
40 UintTy::U16 => ScalarValue::U16(*v as u16),
41 UintTy::U32 => ScalarValue::U32(*v as u32),
42 UintTy::U64 => ScalarValue::U64(*v as u64),
43 UintTy::U128 => ScalarValue::U128(*v),
44 }
45 }
46 };
47 Literal::Scalar(scalar)
48 }
49 hax::ConstantLiteral::Float(value, float_type) => {
50 let value = value.clone();
51 let ty = match float_type {
52 hax::FloatTy::F16 => FloatTy::F16,
53 hax::FloatTy::F32 => FloatTy::F32,
54 hax::FloatTy::F64 => FloatTy::F64,
55 hax::FloatTy::F128 => FloatTy::F128,
56 };
57 Literal::Float(FloatValue { value, ty })
58 }
59 };
60 Ok(RawConstantExpr::Literal(lit))
61 }
62
63 pub(crate) fn translate_constant_expr_to_constant_expr(
69 &mut self,
70 span: Span,
71 v: &hax::ConstantExpr,
72 ) -> Result<ConstantExpr, Error> {
73 use hax::ConstantExprKind;
74 let ty = self.translate_ty(span, &v.ty)?;
75 let value = match v.contents.as_ref() {
76 ConstantExprKind::Literal(lit) => {
77 self.translate_constant_literal_to_raw_constant_expr(span, lit)?
78 }
79 ConstantExprKind::Adt { info, fields } => {
80 let fields: Vec<ConstantExpr> = fields
81 .iter()
82 .map(|f| self.translate_constant_expr_to_constant_expr(span, &f.value))
83 .try_collect()?;
84 use hax::VariantKind;
85 let vid = if let VariantKind::Enum { index, .. } = info.kind {
86 Some(VariantId::new(index))
87 } else {
88 None
89 };
90 RawConstantExpr::Adt(vid, fields)
91 }
92 ConstantExprKind::Array { fields } => {
93 let fields: Vec<ConstantExpr> = fields
94 .iter()
95 .map(|x| self.translate_constant_expr_to_constant_expr(span, x))
96 .try_collect()?;
97 RawConstantExpr::Array(fields)
98 }
99 ConstantExprKind::Tuple { fields } => {
100 let fields: Vec<ConstantExpr> = fields
101 .iter()
102 .map(|f| self.translate_constant_expr_to_constant_expr(span, f))
104 .try_collect()?;
105 RawConstantExpr::Adt(None, fields)
106 }
107 ConstantExprKind::TraitConst { impl_expr, name } => {
108 let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
109 let name = TraitItemName(name.clone());
110 RawConstantExpr::TraitConst(trait_ref, name)
111 }
112 ConstantExprKind::GlobalName {
113 id,
114 generics,
115 trait_refs,
116 ..
117 } => {
118 trace!(
119 "\n- generics: {:?}\n- trait_resf: {:?}\n",
120 generics,
121 trait_refs
122 );
123 let global_id = self.register_global_decl_id(span, id);
124 let generics = self.translate_generic_args(
125 span,
126 generics,
127 trait_refs,
128 None,
129 GenericsSource::item(global_id),
130 )?;
131 RawConstantExpr::Global(GlobalDeclRef {
132 id: global_id,
133 generics,
134 })
135 }
136 ConstantExprKind::Borrow(v)
137 if let ConstantExprKind::Literal(hax::ConstantLiteral::Str(s)) =
138 v.contents.as_ref() =>
139 {
140 RawConstantExpr::Literal(Literal::Str(s.clone()))
141 }
142 ConstantExprKind::Borrow(v) => {
143 let val = self.translate_constant_expr_to_constant_expr(span, v)?;
144 RawConstantExpr::Ref(Box::new(val))
145 }
146 ConstantExprKind::Cast { .. } => {
147 register_error!(
148 self,
149 span,
150 "Unsupported constant: `ConstantExprKind::Cast {{..}}`",
151 );
152 RawConstantExpr::Opaque("`ConstantExprKind::Cast {{..}}`".into())
153 }
154 ConstantExprKind::RawBorrow {
155 mutability: false, ..
156 } => {
157 register_error!(
158 self,
159 span,
160 "Unsupported constant: `ConstantExprKind::RawBorrow {{mutability: false, ..}}`",
161 );
162 RawConstantExpr::Opaque(
163 "ConstantExprKind::RawBorrow {{mutability: false, ..}}".into(),
164 )
165 }
166 ConstantExprKind::RawBorrow {
167 mutability: true,
168 arg,
169 } => {
170 let arg = self.translate_constant_expr_to_constant_expr(span, arg)?;
171 RawConstantExpr::MutPtr(Box::new(arg))
172 }
173 ConstantExprKind::ConstRef { id } => {
174 let var = self.lookup_const_generic_var(span, id)?;
175 RawConstantExpr::Var(var)
176 }
177 ConstantExprKind::FnPtr {
178 def_id: fn_id,
179 generics: substs,
180 generics_impls: trait_refs,
181 method_impl: trait_info,
182 } => {
183 let fn_ptr = self.translate_fn_ptr(span, fn_id, substs, trait_refs, trait_info)?;
184 RawConstantExpr::FnPtr(fn_ptr)
185 }
186 ConstantExprKind::Memory(bytes) => RawConstantExpr::RawMemory(bytes.clone()),
187 ConstantExprKind::Todo(msg) => {
188 register_error!(self, span, "Unsupported constant: {:?}", msg);
189 RawConstantExpr::Opaque(msg.into())
190 }
191 };
192
193 Ok(ConstantExpr { value, ty })
194 }
195
196 pub(crate) fn translate_constant_expr_to_const_generic(
199 &mut self,
200 span: Span,
201 v: &hax::ConstantExpr,
202 ) -> Result<ConstGeneric, Error> {
203 let value = self
206 .translate_constant_expr_to_constant_expr(span, v)?
207 .value;
208 match value {
209 RawConstantExpr::Var(v) => Ok(ConstGeneric::Var(v)),
210 RawConstantExpr::Literal(v) => Ok(ConstGeneric::Value(v)),
211 RawConstantExpr::Global(global_ref) => {
212 error_assert!(self, span, global_ref.generics.is_empty());
215 Ok(ConstGeneric::Global(global_ref.id))
216 }
217 RawConstantExpr::Adt(..)
218 | RawConstantExpr::Array { .. }
219 | RawConstantExpr::RawMemory { .. }
220 | RawConstantExpr::TraitConst { .. }
221 | RawConstantExpr::Ref(_)
222 | RawConstantExpr::MutPtr(_)
223 | RawConstantExpr::FnPtr { .. }
224 | RawConstantExpr::Opaque(_) => {
225 raise_error!(self, span, "Unexpected constant generic: {:?}", value)
226 }
227 }
228 }
229}