Start working on separating pairs from 2 tuples in Aiken

co-authored-by: KtorZ <matthias.benkort@gmail.com>
This commit is contained in:
microproofs 2024-03-01 13:22:02 -05:00 committed by Kasey
parent a9c8054819
commit d05d8e7de6
8 changed files with 89 additions and 52 deletions

View File

@ -1334,6 +1334,10 @@ pub fn tuple(elems: Vec<Rc<Type>>) -> Rc<Type> {
Rc::new(Type::Tuple { elems, alias: None }) Rc::new(Type::Tuple { elems, alias: None })
} }
pub fn pair(fst: Rc<Type>, snd: Rc<Type>) -> Rc<Type> {
Rc::new(Type::Pair { fst, snd })
}
pub fn bool() -> Rc<Type> { pub fn bool() -> Rc<Type> {
Rc::new(Type::App { Rc::new(Type::App {
args: vec![], args: vec![],

View File

@ -762,7 +762,7 @@ impl<'a> CodeGenerator<'a> {
TypedExpr::TupleIndex { TypedExpr::TupleIndex {
index, tuple, tipo, .. index, tuple, tipo, ..
} => { } => {
if tuple.tipo().is_2_tuple() { if tuple.tipo().is_pair() {
AirTree::pair_index( AirTree::pair_index(
*index, *index,
tipo.clone(), tipo.clone(),
@ -1486,7 +1486,7 @@ impl<'a> CodeGenerator<'a> {
AirTree::let_assignment(&list_name, value, func_call) AirTree::let_assignment(&list_name, value, func_call)
} }
} else if tipo.is_2_tuple() { } else if tipo.is_pair() {
let tuple_inner_types = tipo.get_inner_types(); let tuple_inner_types = tipo.get_inner_types();
assert!(tuple_inner_types.len() == 2); assert!(tuple_inner_types.len() == 2);
@ -3833,7 +3833,7 @@ impl<'a> CodeGenerator<'a> {
} }
DefaultFunction::HeadList DefaultFunction::HeadList
if !constructor.tipo.return_type().unwrap().is_2_tuple() => if !constructor.tipo.return_type().unwrap().is_pair() =>
{ {
builder::undata_builtin( builder::undata_builtin(
builtin, builtin,
@ -4249,7 +4249,7 @@ impl<'a> CodeGenerator<'a> {
builder::undata_builtin(&func, count, tipo, arg_vec) builder::undata_builtin(&func, count, tipo, arg_vec)
} }
DefaultFunction::HeadList if !tipo.is_2_tuple() => { DefaultFunction::HeadList if !tipo.is_pair() => {
builder::undata_builtin(&func, count, tipo, arg_vec) builder::undata_builtin(&func, count, tipo, arg_vec)
} }
@ -4310,15 +4310,14 @@ impl<'a> CodeGenerator<'a> {
); );
return Some(term); return Some(term);
} else if tipo.is_map() { }
if tipo.is_map() {
let term = builtin let term = builtin
.apply(Term::map_data().apply(left)) .apply(Term::map_data().apply(left))
.apply(Term::map_data().apply(right)); .apply(Term::map_data().apply(right));
return Some(term); return Some(term);
} else if tipo.is_tuple() }
&& matches!(tipo.get_uplc_type(), UplcType::Pair(_, _)) if tipo.is_pair() {
{
let term = builtin let term = builtin
.apply(Term::map_data().apply( .apply(Term::map_data().apply(
Term::mk_cons().apply(left).apply(Term::empty_map()), Term::mk_cons().apply(left).apply(Term::empty_map()),
@ -4326,15 +4325,16 @@ impl<'a> CodeGenerator<'a> {
.apply(Term::map_data().apply( .apply(Term::map_data().apply(
Term::mk_cons().apply(right).apply(Term::empty_map()), Term::mk_cons().apply(right).apply(Term::empty_map()),
)); ));
return Some(term); return Some(term);
} else if tipo.is_list() || tipo.is_tuple() { }
if tipo.is_list() || tipo.is_tuple() {
let term = builtin let term = builtin
.apply(Term::list_data().apply(left)) .apply(Term::list_data().apply(left))
.apply(Term::list_data().apply(right)); .apply(Term::list_data().apply(right));
return Some(term); return Some(term);
} else if tipo.is_void() { }
if tipo.is_void() {
let term = left.choose_unit(right.choose_unit(Term::bool(true))); let term = left.choose_unit(right.choose_unit(Term::bool(true)));
return Some(term); return Some(term);
@ -4352,16 +4352,16 @@ impl<'a> CodeGenerator<'a> {
); );
return Some(term); return Some(term);
} else if tipo.is_map() { }
if tipo.is_map() {
let term = builtin let term = builtin
.apply(Term::map_data().apply(left)) .apply(Term::map_data().apply(left))
.apply(Term::map_data().apply(right)) .apply(Term::map_data().apply(right))
.if_then_else(Term::bool(false), Term::bool(true)); .if_then_else(Term::bool(false), Term::bool(true));
return Some(term); return Some(term);
} else if tipo.is_tuple() }
&& matches!(tipo.get_uplc_type(), UplcType::Pair(_, _)) if tipo.is_pair() {
{
let term = builtin let term = builtin
.apply(Term::map_data().apply( .apply(Term::map_data().apply(
Term::mk_cons().apply(left).apply(Term::empty_map()), Term::mk_cons().apply(left).apply(Term::empty_map()),
@ -4370,16 +4370,16 @@ impl<'a> CodeGenerator<'a> {
Term::mk_cons().apply(right).apply(Term::empty_map()), Term::mk_cons().apply(right).apply(Term::empty_map()),
)) ))
.if_then_else(Term::bool(false), Term::bool(true)); .if_then_else(Term::bool(false), Term::bool(true));
return Some(term); return Some(term);
} else if tipo.is_list() || tipo.is_tuple() { }
if tipo.is_list() || tipo.is_tuple() {
let term = builtin let term = builtin
.apply(Term::list_data().apply(left)) .apply(Term::list_data().apply(left))
.apply(Term::list_data().apply(right)) .apply(Term::list_data().apply(right))
.if_then_else(Term::bool(false), Term::bool(true)); .if_then_else(Term::bool(false), Term::bool(true));
return Some(term); return Some(term);
} else if tipo.is_void() { }
if tipo.is_void() {
return Some(Term::bool(false)); return Some(Term::bool(false));
} }
@ -4642,9 +4642,14 @@ impl<'a> CodeGenerator<'a> {
|| tipo.is_string() || tipo.is_string()
|| tipo.is_list() || tipo.is_list()
|| tipo.is_tuple() || tipo.is_tuple()
|| tipo.is_pair()
|| tipo.is_bool() || tipo.is_bool()
|| tipo.is_bls381_12_g1()
|| tipo.is_bls381_12_g2()
{ {
subject subject
} else if tipo.is_ml_result() {
unreachable!()
} else { } else {
Term::var( Term::var(
self.special_functions self.special_functions
@ -4709,7 +4714,7 @@ impl<'a> CodeGenerator<'a> {
Term::equals_string() Term::equals_string()
.apply(clause) .apply(clause)
.apply(Term::var(subject_name)) .apply(Term::var(subject_name))
} else if tipo.is_list() || tipo.is_tuple() { } else if tipo.is_list() || tipo.is_tuple() || tipo.is_pair() {
unreachable!("{:#?}", tipo) unreachable!("{:#?}", tipo)
} else { } else {
Term::equals_integer() Term::equals_integer()
@ -4787,7 +4792,7 @@ impl<'a> CodeGenerator<'a> {
.apply(next_clause.delay()); .apply(next_clause.delay());
} }
if tipo.is_2_tuple() { if tipo.is_pair() {
for (index, name) in indices.iter() { for (index, name) in indices.iter() {
if name == "_" { if name == "_" {
continue; continue;
@ -5256,7 +5261,7 @@ impl<'a> CodeGenerator<'a> {
let mut term = arg_stack.pop().unwrap(); let mut term = arg_stack.pop().unwrap();
let list_id = self.id_gen.next(); let list_id = self.id_gen.next();
if tipo.is_2_tuple() { if tipo.is_pair() {
assert!(names.len() == 2); assert!(names.len() == 2);
if names[1] != "_" { if names[1] != "_" {

View File

@ -112,7 +112,7 @@ impl ClauseProperties {
checked_index: -1, checked_index: -1,
}, },
} }
} else if t.is_tuple() { } else if t.is_tuple() || t.is_pair() {
ClauseProperties { ClauseProperties {
clause_var_name: constr_var, clause_var_name: constr_var,
complex_clause: false, complex_clause: false,
@ -154,7 +154,7 @@ impl ClauseProperties {
checked_index: -1, checked_index: -1,
}, },
} }
} else if t.is_tuple() { } else if t.is_tuple() || t.is_pair() {
ClauseProperties { ClauseProperties {
clause_var_name: constr_var, clause_var_name: constr_var,
complex_clause: false, complex_clause: false,
@ -356,7 +356,7 @@ pub fn get_generic_variant_name(t: &Rc<Type>) -> String {
"_ml_result".to_string() "_ml_result".to_string()
} else if t.is_map() { } else if t.is_map() {
"_map".to_string() "_map".to_string()
} else if t.is_2_tuple() { } else if t.is_pair() {
"_pair".to_string() "_pair".to_string()
} else if t.is_list() { } else if t.is_list() {
"_list".to_string() "_list".to_string()
@ -941,7 +941,7 @@ pub fn known_data_to_type(term: Term<Name>, field_type: &Type) -> Term<Name> {
Term::unmap_data().apply(term) Term::unmap_data().apply(term)
} else if field_type.is_string() { } else if field_type.is_string() {
Term::Builtin(DefaultFunction::DecodeUtf8).apply(Term::un_b_data().apply(term)) Term::Builtin(DefaultFunction::DecodeUtf8).apply(Term::un_b_data().apply(term))
} else if field_type.is_tuple() && matches!(field_type.get_uplc_type(), UplcType::Pair(_, _)) { } else if field_type.is_pair() {
Term::mk_pair_data() Term::mk_pair_data()
.apply(Term::head_list().apply(Term::var("__list_data"))) .apply(Term::head_list().apply(Term::var("__list_data")))
.apply(Term::head_list().apply(Term::tail_list().apply(Term::var("__list_data")))) .apply(Term::head_list().apply(Term::tail_list().apply(Term::var("__list_data"))))
@ -1098,7 +1098,7 @@ pub fn unknown_data_to_type_debug(
) )
.lambda("__val") .lambda("__val")
.apply(term) .apply(term)
} else if field_type.is_tuple() && matches!(field_type.get_uplc_type(), UplcType::Pair(_, _)) { } else if field_type.is_pair() {
Term::var("__val") Term::var("__val")
.delayed_choose_data( .delayed_choose_data(
error_term.clone(), error_term.clone(),
@ -1313,7 +1313,7 @@ pub fn convert_type_to_data(term: Term<Name>, field_type: &Rc<Type>) -> Term<Nam
Term::map_data().apply(term) Term::map_data().apply(term)
} else if field_type.is_string() { } else if field_type.is_string() {
Term::b_data().apply(Term::Builtin(DefaultFunction::EncodeUtf8).apply(term)) Term::b_data().apply(Term::Builtin(DefaultFunction::EncodeUtf8).apply(term))
} else if field_type.is_tuple() && matches!(field_type.get_uplc_type(), UplcType::Pair(_, _)) { } else if field_type.is_pair() {
Term::list_data() Term::list_data()
.apply( .apply(
Term::mk_cons() Term::mk_cons()

View File

@ -71,6 +71,11 @@ pub enum Type {
elems: Vec<Rc<Type>>, elems: Vec<Rc<Type>>,
alias: Option<Rc<TypeAliasAnnotation>>, alias: Option<Rc<TypeAliasAnnotation>>,
}, },
Pair {
fst: Rc<Type>,
snd: Rc<Type>,
},
} }
impl PartialEq for Type { impl PartialEq for Type {
@ -208,6 +213,7 @@ impl Type {
} => *opaque || args.iter().any(|arg| arg.contains_opaque()), } => *opaque || args.iter().any(|arg| arg.contains_opaque()),
Type::Tuple { elems, .. } => elems.iter().any(|elem| elem.contains_opaque()), Type::Tuple { elems, .. } => elems.iter().any(|elem| elem.contains_opaque()),
Type::Fn { .. } => false, Type::Fn { .. } => false,
Type::Pair { fst, snd } => fst.contains_opaque() || snd.contains_opaque(),
} }
} }
@ -218,7 +224,7 @@ impl Type {
} => { } => {
*contains_opaque = opaque; *contains_opaque = opaque;
} }
Type::Fn { .. } | Type::Var { .. } | Type::Tuple { .. } => (), Type::Fn { .. } | Type::Var { .. } | Type::Tuple { .. } | Type::Pair { .. } => (),
} }
} }
@ -343,24 +349,24 @@ impl Type {
} if "List" == name && module.is_empty() => args } if "List" == name && module.is_empty() => args
.first() .first()
.expect("unreachable: List should have an inner type") .expect("unreachable: List should have an inner type")
.is_2_tuple(), .is_pair(),
Self::Var { tipo, .. } => tipo.borrow().is_map(), Self::Var { tipo } => tipo.borrow().is_map(),
_ => false, _ => false,
} }
} }
pub fn is_tuple(&self) -> bool { pub fn is_tuple(&self) -> bool {
match self { match self {
Type::Var { tipo, .. } => tipo.borrow().is_tuple(), Self::Var { tipo } => tipo.borrow().is_tuple(),
Type::Tuple { .. } => true, Self::Tuple { .. } => true,
_ => false, _ => false,
} }
} }
pub fn is_2_tuple(&self) -> bool { pub fn is_pair(&self) -> bool {
match self { match self {
Type::Var { tipo, .. } => tipo.borrow().is_2_tuple(), Self::Var { tipo } => tipo.borrow().is_pair(),
Type::Tuple { elems, .. } => elems.len() == 2, Self::Pair { .. } => true,
_ => false, _ => false,
} }
} }
@ -375,7 +381,7 @@ impl Type {
pub fn is_generic(&self) -> bool { pub fn is_generic(&self) -> bool {
match self { match self {
Type::App { args, .. } => { Self::App { args, .. } => {
let mut is_a_generic = false; let mut is_a_generic = false;
for arg in args { for arg in args {
is_a_generic = is_a_generic || arg.is_generic(); is_a_generic = is_a_generic || arg.is_generic();
@ -383,21 +389,22 @@ impl Type {
is_a_generic is_a_generic
} }
Type::Var { tipo, .. } => tipo.borrow().is_generic(), Self::Var { tipo } => tipo.borrow().is_generic(),
Type::Tuple { elems, .. } => { Self::Tuple { elems } => {
let mut is_a_generic = false; let mut is_a_generic = false;
for elem in elems { for elem in elems {
is_a_generic = is_a_generic || elem.is_generic(); is_a_generic = is_a_generic || elem.is_generic();
} }
is_a_generic is_a_generic
} }
Type::Fn { args, ret, .. } => { Self::Fn { args, ret } => {
let mut is_a_generic = false; let mut is_a_generic = false;
for arg in args { for arg in args {
is_a_generic = is_a_generic || arg.is_generic(); is_a_generic = is_a_generic || arg.is_generic();
} }
is_a_generic || ret.is_generic() is_a_generic || ret.is_generic()
} }
Self::Pair { fst, snd } => fst.is_generic() || snd.is_generic(),
} }
} }
@ -412,7 +419,7 @@ impl Type {
pub fn get_generic(&self) -> Option<u64> { pub fn get_generic(&self) -> Option<u64> {
match self { match self {
Type::Var { tipo, .. } => tipo.borrow().get_generic(), Self::Var { tipo } => tipo.borrow().get_generic(),
_ => None, _ => None,
} }
} }
@ -446,6 +453,7 @@ impl Type {
} }
} }
// TODO: THIS WILL CHANGE DUE TO PAIRS
pub fn get_uplc_type(&self) -> UplcType { pub fn get_uplc_type(&self) -> UplcType {
if self.is_int() { if self.is_int() {
UplcType::Integer UplcType::Integer
@ -461,16 +469,12 @@ impl Type {
UplcType::List(UplcType::Data.into()) UplcType::List(UplcType::Data.into())
} else if self.is_tuple() { } else if self.is_tuple() {
match self { match self {
Self::Tuple { elems, .. } => { Self::Tuple { .. } => UplcType::List(UplcType::Data.into()),
if elems.len() == 2 { Self::Var { tipo } => tipo.borrow().get_uplc_type().unwrap(),
UplcType::Pair(UplcType::Data.into(), UplcType::Data.into())
} else {
UplcType::List(UplcType::Data.into())
}
}
Self::Var { tipo, .. } => tipo.borrow().get_uplc_type().unwrap(),
_ => unreachable!(), _ => unreachable!(),
} }
} else if self.is_pair() {
UplcType::Pair(UplcType::Data.into(), UplcType::Data.into())
} else if self.is_bls381_12_g1() { } else if self.is_bls381_12_g1() {
UplcType::Bls12_381G1Element UplcType::Bls12_381G1Element
} else if self.is_bls381_12_g2() { } else if self.is_bls381_12_g2() {
@ -559,6 +563,13 @@ impl Type {
TypeVar::Link { tipo, .. } => tipo.find_private_type(), TypeVar::Link { tipo, .. } => tipo.find_private_type(),
}, },
Self::Pair { fst, snd } => {
if let Some(private_type) = fst.find_private_type() {
Some(private_type)
} else {
snd.find_private_type()
}
}
} }
} }
@ -955,9 +966,9 @@ impl TypeVar {
} }
} }
pub fn is_2_tuple(&self) -> bool { pub fn is_pair(&self) -> bool {
match self { match self {
Self::Link { tipo } => tipo.is_2_tuple(), Self::Link { tipo } => tipo.is_pair(),
_ => false, _ => false,
} }
} }

View File

@ -1794,6 +1794,12 @@ fn unify_unbound_type(tipo: Rc<Type>, own_id: u64, location: Span) -> Result<(),
Ok(()) Ok(())
} }
Type::Pair { fst, snd } => {
unify_unbound_type(fst.clone(), own_id, location)?;
unify_unbound_type(snd.clone(), own_id, location)?;
Ok(())
}
Type::Var { .. } => unreachable!(), Type::Var { .. } => unreachable!(),
} }

View File

@ -86,6 +86,9 @@ impl Printer {
Type::Var { tipo: typ, .. } => self.type_var_doc(&typ.borrow()), Type::Var { tipo: typ, .. } => self.type_var_doc(&typ.borrow()),
Type::Tuple { elems, .. } => self.args_to_aiken_doc(elems).surround("(", ")"), Type::Tuple { elems, .. } => self.args_to_aiken_doc(elems).surround("(", ")"),
Type::Pair { fst, snd } => self
.args_to_aiken_doc(&[fst.clone(), snd.clone()])
.surround("Pair<", ">"),
} }
} }

View File

@ -145,6 +145,13 @@ impl Reference {
elems = Self::from_types(elems, type_parameters) elems = Self::from_types(elems, type_parameters)
), ),
}, },
Type::Pair { fst, snd } => Self {
inner: format!(
"Pair{fst}{snd}",
fst = Self::from_type(fst, type_parameters),
snd = Self::from_type(snd, type_parameters)
),
},
// NOTE: // NOTE:
// //

View File

@ -384,6 +384,7 @@ impl Annotated<Schema> {
} }
}, },
Type::Fn { .. } => unreachable!(), Type::Fn { .. } => unreachable!(),
Type::Pair { .. } => unreachable!(),
} }
} }
} }