Partial fix for Coq backend
@@ -836,27 +836,10 @@ fn translate_expression<'a>(e: Expression, top_ctx: &'a TopLevelContext) -> RcDo
.append(RcDoc::space())
.append(make_paren(translate_expression(e2, top_ctx)))
}
- Expression::NewArray(_, typ, args) => {
- // retrieves the element type of the array. For named types (aliases), it looks up
- // the original definition in the typ_dict.
- let inner_ty = match typ {
- Some(BaseTyp::Named(ident, _)) => {
- let ident = &ident.0;
- match top_ctx.typ_dict.get(ident) {
- Some((alias_typ, DictEntry::Array)) => {
- match (alias_typ.1).0.clone() {
- BaseTyp::Array(_size, inner_ty) => inner_ty.as_ref().clone().0,
- _ => panic!(),
- }
- // translate_prefix_for_func_name((alias_typ.1).0.clone(), top_ctx)
- }
- _ => panic!(),
- }
- }
- Some(BaseTyp::Array(_size, inner_ty)) => inner_ty.as_ref().clone().0,
- // Should not happen - array should always have an element type
- _ => panic!(),
- };
+ Expression::NewArray(_array_name, inner_ty, args) => {
+ let inner_ty = inner_ty.unwrap();
+ // inner_ty is the type of the cell elements
+ // TODO: do the case when _array_name is None (the Seq case)
RcDoc::as_string(format!("{}_from_list", ARRAY_MODULE))
.append(RcDoc::space())
.append(translate_base_typ(inner_ty.clone()))
@@ -867,7 +850,7 @@ fn translate_expression<'a>(e: Expression, top_ctx: &'a TopLevelContext) -> RcDo
None,
make_list(
args.into_iter()
- .map(|(e, _)| translate_expression(e, top_ctx)),
+ .map(|(e, _)| translate_expression(e.clone(), top_ctx)),
),
false,
)
