Fix pairs not being unwrapped when wrapped as fields

This commit is contained in:
microproofs 2024-10-31 01:03:54 -04:00
parent 25e4b42cd0
commit 27bf40260e
No known key found for this signature in database
GPG Key ID: 14F93C84DE6AFD17
5 changed files with 73 additions and 10 deletions

View File

@ -5371,6 +5371,11 @@ impl<'a> CodeGenerator<'a> {
)) ))
} }
} }
Air::ExtractField { tipo } => {
let arg = arg_stack.pop().unwrap();
Some(known_data_to_type(Term::head_list().apply(arg), &tipo))
}
} }
} }
} }

View File

@ -211,13 +211,16 @@ pub enum Air {
tipo: Rc<Type>, tipo: Rc<Type>,
is_expect: bool, is_expect: bool,
}, },
// Tuple Access // Pair Access
PairAccessor { PairAccessor {
fst: Option<String>, fst: Option<String>,
snd: Option<String>, snd: Option<String>,
tipo: Rc<Type>, tipo: Rc<Type>,
is_expect: bool, is_expect: bool,
}, },
ExtractField {
tipo: Rc<Type>,
},
// Misc. // Misc.
ErrorTerm { ErrorTerm {
tipo: Rc<Type>, tipo: Rc<Type>,

View File

@ -27,6 +27,7 @@ pub enum Path {
Pair(usize), Pair(usize),
Tuple(usize), Tuple(usize),
Constr(Rc<Type>, usize), Constr(Rc<Type>, usize),
OpaqueConstr(Rc<Type>),
List(usize), List(usize),
ListTail(usize), ListTail(usize),
} }
@ -43,6 +44,7 @@ impl ToString for Path {
Path::Constr(_, i) => { Path::Constr(_, i) => {
format!("constr_{}", i) format!("constr_{}", i)
} }
Path::OpaqueConstr(_) => "opaqueconstr".to_string(),
Path::List(i) => { Path::List(i) => {
format!("list_{}", i) format!("list_{}", i)
} }
@ -61,6 +63,7 @@ impl PartialEq for Path {
| (Path::Constr(_, a), Path::Constr(_, b)) | (Path::Constr(_, a), Path::Constr(_, b))
| (Path::List(a), Path::List(b)) | (Path::List(a), Path::List(b))
| (Path::ListTail(a), Path::ListTail(b)) => a == b, | (Path::ListTail(a), Path::ListTail(b)) => a == b,
(Path::OpaqueConstr(_), Path::OpaqueConstr(_)) => true,
_ => false, _ => false,
} }
} }
@ -1094,6 +1097,9 @@ impl<'a, 'b> TreeGen<'a, 'b> {
} => { } => {
let data_type = lookup_data_type_by_tipo(self.data_types, &current_tipo).unwrap(); let data_type = lookup_data_type_by_tipo(self.data_types, &current_tipo).unwrap();
let is_transparent =
data_type.opaque && data_type.constructors[0].arguments.len() == 1;
if data_type.constructors.len() == 1 || data_type.is_never() { if data_type.constructors.len() == 1 || data_type.is_never() {
arguments arguments
.iter() .iter()
@ -1103,7 +1109,11 @@ impl<'a, 'b> TreeGen<'a, 'b> {
let mut item_path = path.clone(); let mut item_path = path.clone();
if is_transparent {
item_path.push(Path::OpaqueConstr(tipo.clone()));
} else {
item_path.push(Path::Constr(tipo.clone(), index)); item_path.push(Path::Constr(tipo.clone(), index));
}
let (assigns, patts) = let (assigns, patts) =
self.map_pattern_to_row(arg_value, subject_tipo, item_path); self.map_pattern_to_row(arg_value, subject_tipo, item_path);
@ -1199,6 +1209,10 @@ pub fn get_tipo_by_path(mut subject_tipo: Rc<Type>, mut path: &[Path]) -> Rc<Typ
Path::List(_) => subject_tipo.get_inner_types().swap_remove(0), Path::List(_) => subject_tipo.get_inner_types().swap_remove(0),
Path::ListTail(_) => subject_tipo, Path::ListTail(_) => subject_tipo,
Path::Constr(tipo, index) => tipo.arg_types().unwrap().swap_remove(*index), Path::Constr(tipo, index) => tipo.arg_types().unwrap().swap_remove(*index),
Path::OpaqueConstr(tipo) => {
let x = tipo.arg_types().unwrap().swap_remove(0);
x
}
}; };
path = rest path = rest

View File

@ -14,6 +14,7 @@ use super::{
#[derive(Clone, Debug)] #[derive(Clone, Debug)]
pub enum Builtin { pub enum Builtin {
HeadList(Rc<Type>), HeadList(Rc<Type>),
ExtractField(Rc<Type>),
TailList, TailList,
UnConstrFields, UnConstrFields,
FstPair(Rc<Type>), FstPair(Rc<Type>),
@ -24,6 +25,7 @@ impl PartialEq for Builtin {
fn eq(&self, other: &Self) -> bool { fn eq(&self, other: &Self) -> bool {
match (self, other) { match (self, other) {
(Builtin::HeadList(_), Builtin::HeadList(_)) (Builtin::HeadList(_), Builtin::HeadList(_))
| (Builtin::ExtractField(_), Builtin::ExtractField(_))
| (Builtin::TailList, Builtin::TailList) | (Builtin::TailList, Builtin::TailList)
| (Builtin::UnConstrFields, Builtin::UnConstrFields) | (Builtin::UnConstrFields, Builtin::UnConstrFields)
| (Builtin::FstPair(_), Builtin::FstPair(_)) | (Builtin::FstPair(_), Builtin::FstPair(_))
@ -39,6 +41,7 @@ impl Builtin {
fn to_air_call(self, special_funcs: &mut CodeGenSpecialFuncs, arg: AirTree) -> AirTree { fn to_air_call(self, special_funcs: &mut CodeGenSpecialFuncs, arg: AirTree) -> AirTree {
match self { match self {
Builtin::HeadList(t) => AirTree::builtin(DefaultFunction::HeadList, t, vec![arg]), Builtin::HeadList(t) => AirTree::builtin(DefaultFunction::HeadList, t, vec![arg]),
Builtin::ExtractField(t) => AirTree::extract_field(t, arg),
Builtin::TailList => AirTree::builtin( Builtin::TailList => AirTree::builtin(
DefaultFunction::TailList, DefaultFunction::TailList,
Type::list(Type::data()), Type::list(Type::data()),
@ -58,10 +61,9 @@ impl Builtin {
pub fn tipo(&self) -> Rc<Type> { pub fn tipo(&self) -> Rc<Type> {
match self { match self {
Builtin::HeadList(t) => t.clone(), Builtin::HeadList(t) => t.clone(),
Builtin::ExtractField(t) => t.clone(),
Builtin::TailList => Type::list(Type::data()), Builtin::TailList => Type::list(Type::data()),
Builtin::UnConstrFields => Type::list(Type::data()), Builtin::UnConstrFields => Type::list(Type::data()),
Builtin::FstPair(t) => t.clone(), Builtin::FstPair(t) => t.clone(),
Builtin::SndPair(t) => t.clone(), Builtin::SndPair(t) => t.clone(),
} }
@ -72,6 +74,7 @@ impl ToString for Builtin {
fn to_string(&self) -> String { fn to_string(&self) -> String {
match self { match self {
Builtin::HeadList(_) => "head".to_string(), Builtin::HeadList(_) => "head".to_string(),
Builtin::ExtractField(_) => "extractfield".to_string(),
Builtin::TailList => "tail".to_string(), Builtin::TailList => "tail".to_string(),
Builtin::UnConstrFields => "unconstrfields".to_string(), Builtin::UnConstrFields => "unconstrfields".to_string(),
Builtin::FstPair(_) => "fst".to_string(), Builtin::FstPair(_) => "fst".to_string(),
@ -110,6 +113,8 @@ impl Builtins {
.into_iter() .into_iter()
.fold((vec![], vec![]), |(mut builtins, mut rebuilt_path), i| { .fold((vec![], vec![]), |(mut builtins, mut rebuilt_path), i| {
rebuilt_path.push(i.clone()); rebuilt_path.push(i.clone());
let is_list = matches!(i, Path::List(_));
match i { match i {
Path::Pair(i) => { Path::Pair(i) => {
if i == 0 { if i == 0 {
@ -133,10 +138,17 @@ impl Builtins {
builtins.push(Builtin::TailList); builtins.push(Builtin::TailList);
} }
if is_list {
builtins.push(Builtin::HeadList(get_tipo_by_path( builtins.push(Builtin::HeadList(get_tipo_by_path(
subject_tipo.clone(), subject_tipo.clone(),
&rebuilt_path, &rebuilt_path,
))); )));
} else {
builtins.push(Builtin::ExtractField(get_tipo_by_path(
subject_tipo.clone(),
&rebuilt_path,
)));
}
(builtins, rebuilt_path) (builtins, rebuilt_path)
} }
@ -147,7 +159,7 @@ impl Builtins {
builtins.push(Builtin::TailList); builtins.push(Builtin::TailList);
} }
builtins.push(Builtin::HeadList(get_tipo_by_path( builtins.push(Builtin::ExtractField(get_tipo_by_path(
subject_tipo.clone(), subject_tipo.clone(),
&rebuilt_path, &rebuilt_path,
))); )));
@ -162,6 +174,7 @@ impl Builtins {
(builtins, rebuilt_path) (builtins, rebuilt_path)
} }
Path::OpaqueConstr(_) => (builtins, rebuilt_path),
} }
}) })
.0, .0,

View File

@ -235,6 +235,10 @@ pub enum AirTree {
then: Box<AirTree>, then: Box<AirTree>,
otherwise: Box<AirTree>, otherwise: Box<AirTree>,
}, },
ExtractField {
tipo: Rc<Type>,
arg: Box<AirTree>,
},
// Misc. // Misc.
FieldsEmpty { FieldsEmpty {
constr: Box<AirTree>, constr: Box<AirTree>,
@ -970,6 +974,13 @@ impl AirTree {
} }
} }
pub fn extract_field(tipo: Rc<Type>, arg: AirTree) -> AirTree {
AirTree::ExtractField {
tipo,
arg: arg.into(),
}
}
pub fn pair_index(index: usize, tipo: Rc<Type>, tuple: AirTree) -> AirTree { pub fn pair_index(index: usize, tipo: Rc<Type>, tuple: AirTree) -> AirTree {
AirTree::cast_from_data( AirTree::cast_from_data(
AirTree::builtin( AirTree::builtin(
@ -1651,6 +1662,13 @@ impl AirTree {
msg.create_air_vec(air_vec); msg.create_air_vec(air_vec);
then.create_air_vec(air_vec); then.create_air_vec(air_vec);
} }
AirTree::ExtractField {
tipo,
arg: args_list,
} => {
air_vec.push(Air::ExtractField { tipo: tipo.clone() });
args_list.create_air_vec(air_vec);
}
} }
} }
@ -1666,6 +1684,7 @@ impl AirTree {
| AirTree::Pair { tipo, .. } | AirTree::Pair { tipo, .. }
| AirTree::Call { tipo, .. } | AirTree::Call { tipo, .. }
| AirTree::Builtin { tipo, .. } | AirTree::Builtin { tipo, .. }
| AirTree::ExtractField { tipo, .. }
| AirTree::BinOp { tipo, .. } | AirTree::BinOp { tipo, .. }
| AirTree::CastFromData { tipo, .. } | AirTree::CastFromData { tipo, .. }
| AirTree::When { tipo, .. } | AirTree::When { tipo, .. }
@ -1728,6 +1747,7 @@ impl AirTree {
| AirTree::Tuple { tipo, .. } | AirTree::Tuple { tipo, .. }
| AirTree::Call { tipo, .. } | AirTree::Call { tipo, .. }
| AirTree::Builtin { tipo, .. } | AirTree::Builtin { tipo, .. }
| AirTree::ExtractField { tipo, .. }
| AirTree::CastFromData { tipo, .. } | AirTree::CastFromData { tipo, .. }
| AirTree::CastToData { tipo, .. } | AirTree::CastToData { tipo, .. }
| AirTree::If { tipo, .. } | AirTree::If { tipo, .. }
@ -2077,7 +2097,8 @@ impl AirTree {
| AirTree::Constr { .. } | AirTree::Constr { .. }
| AirTree::RecordUpdate { .. } | AirTree::RecordUpdate { .. }
| AirTree::ErrorTerm { .. } | AirTree::ErrorTerm { .. }
| AirTree::Trace { .. } => {} | AirTree::Trace { .. }
| AirTree::ExtractField { .. } => {}
} }
match self { match self {
@ -2191,6 +2212,9 @@ impl AirTree {
); );
} }
} }
AirTree::ExtractField { tipo: _, arg } => {
arg.do_traverse_tree_with(tree_path, current_depth + 1, Fields::SecondField, with);
}
AirTree::BinOp { AirTree::BinOp {
name: _, name: _,
tipo: _, tipo: _,
@ -2735,6 +2759,10 @@ impl AirTree {
.do_find_air_tree_node(tree_path_iter), .do_find_air_tree_node(tree_path_iter),
_ => panic!("Tree Path index outside tree children nodes"), _ => panic!("Tree Path index outside tree children nodes"),
}, },
AirTree::ExtractField { tipo: _, arg } => match field {
Fields::SecondField => arg.as_mut().do_find_air_tree_node(tree_path_iter),
_ => panic!("Tree Path index outside tree children nodes"),
},
AirTree::Pair { tipo: _, fst, snd } => match field { AirTree::Pair { tipo: _, fst, snd } => match field {
Fields::SecondField => fst.as_mut().do_find_air_tree_node(tree_path_iter), Fields::SecondField => fst.as_mut().do_find_air_tree_node(tree_path_iter),
Fields::ThirdField => snd.as_mut().do_find_air_tree_node(tree_path_iter), Fields::ThirdField => snd.as_mut().do_find_air_tree_node(tree_path_iter),