Skip to content

Commit

Permalink
fix: found various unify and type issues while running tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@MicroProofs
MicroProofs committed May 3, 2024
1 parent 1c75dd4 commit 69e6a1a
Show file tree
Hide file tree
Showing 5 changed files with 525 additions and 137 deletions.
61 changes: 36 additions & 25 deletions crates/aiken-lang/src/gen_uplc.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -372,32 +372,42 @@ impl<'a> CodeGenerator<'a> {
},
..
} => {
let data_type = lookup_data_type_by_tipo(&self.data_types, tipo)
.expect("Creating a record with no record definition.");
if tipo.is_pair() {
assert!(args.len() == 2);

let (constr_index, _) = data_type
.constructors
.iter()
.enumerate()
.find(|(_, dt)| &dt.name == constr_name)
.unwrap();
let arg1 = self.build(&args[0].value, module_build_name, &[]);

let constr_args = args
.iter()
.zip(constr_tipo.arg_types().unwrap())
.map(|(arg, tipo)| {
if tipo.is_data() {
AirTree::cast_to_data(
self.build(&arg.value, module_build_name, &[]),
arg.value.tipo(),
)
} else {
self.build(&arg.value, module_build_name, &[])
}
})
.collect_vec();
let arg2 = self.build(&args[1].value, module_build_name, &[]);

AirTree::pair(arg1, arg2, tipo.clone())
} else {
let data_type = lookup_data_type_by_tipo(&self.data_types, tipo)
.expect("Creating a record with no record definition.");

let (constr_index, _) = data_type
.constructors
.iter()
.enumerate()
.find(|(_, dt)| &dt.name == constr_name)
.unwrap();

AirTree::create_constr(constr_index, constr_tipo.clone(), constr_args)
let constr_args = args
.iter()
.zip(constr_tipo.arg_types().unwrap())
.map(|(arg, tipo)| {
if tipo.is_data() {
AirTree::cast_to_data(
self.build(&arg.value, module_build_name, &[]),
arg.value.tipo(),
)
} else {
self.build(&arg.value, module_build_name, &[])
}
})
.collect_vec();

AirTree::create_constr(constr_index, constr_tipo.clone(), constr_args)
}
}

TypedExpr::Var {
Expand Down Expand Up @@ -5420,12 +5430,13 @@ impl<'a> CodeGenerator<'a> {

match (extract_constant(&fst), extract_constant(&snd)) {
(Some(fst), Some(snd)) => {
let mut pair_fields = builder::convert_constants_to_data(vec![fst, snd]);
let term = Term::Constant(
UplcConstant::ProtoPair(
UplcType::Data,
UplcType::Data,
fst.clone(),
snd.clone(),
pair_fields.remove(0).into(),
pair_fields.remove(0).into(),
)
.into(),
);
Expand Down
18 changes: 13 additions & 5 deletions crates/aiken-lang/src/gen_uplc/builder.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -695,13 +695,21 @@ pub fn pattern_has_conditions(
Pattern::Constructor {
arguments, tipo, ..
} => {
let data_type =
lookup_data_type_by_tipo(data_types, tipo).expect("Data type not found");

data_type.constructors.len() > 1
|| arguments
if tipo.is_pair()
|| (tipo.is_function() && tipo.return_type().map(|t| t.is_pair()).unwrap_or(false))
{
arguments
.iter()
.any(|arg| pattern_has_conditions(&arg.value, data_types))
} else {
let data_type = lookup_data_type_by_tipo(data_types, tipo)
.unwrap_or_else(|| panic!("Data type not found: {:#?}", tipo));

data_type.constructors.len() > 1
|| arguments
.iter()
.any(|arg| pattern_has_conditions(&arg.value, data_types))
}
}
Pattern::Assign { pattern, .. } => pattern_has_conditions(pattern, data_types),
Pattern::Var { .. } | Pattern::Discard { .. } => false,
Expand Down
194 changes: 136 additions & 58 deletions crates/aiken-lang/src/tipo/environment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1495,94 +1495,172 @@ impl<'a> Environment<'a> {
.map_err(|e| e.flip_unify());
}

match (lhs.deref(), rhs.deref()) {
(
Type::App {
module: m1,
name: n1,
args: args1,
public: _,
contains_opaque: _,
alias: _,
},
Type::App {
match lhs.deref() {
Type::App {
module: m1,
name: n1,
args: args1,
public: _,
contains_opaque: _,
alias: _,
} => {
if let Type::App {
module: m2,
name: n2,
args: args2,
public: _,
contains_opaque: _,
alias: _,
},
) if m1 == m2 && n1 == n2 && args1.len() == args2.len() => {
for (a, b) in args1.iter().zip(args2) {
unify_enclosed_type(
lhs.clone(),
rhs.clone(),
self.unify(a.clone(), b.clone(), location, false),
)?;
} = rhs.deref()
{
if m1 == m2 && n1 == n2 && args1.len() == args2.len() {
for (a, b) in args1.iter().zip(args2) {
unify_enclosed_type(
lhs.clone(),
rhs.clone(),
self.unify(a.clone(), b.clone(), location, false),
)?;
}
Ok(())
} else {
Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})
}
} else {
Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})
}
Ok(())
}

(
Type::Tuple {
elems: elems1,
alias: _,
},
Type::Tuple {
Type::Tuple {
elems: elems1,
alias: _,
} => {
if let Type::Tuple {
elems: elems2,
alias: _,
},
) if elems1.len() == elems2.len() => {
for (a, b) in elems1.iter().zip(elems2) {
unify_enclosed_type(
lhs.clone(),
rhs.clone(),
self.unify(a.clone(), b.clone(), location, false),
)?;
} = rhs.deref()
{
if elems1.len() == elems2.len() {
for (a, b) in elems1.iter().zip(elems2) {
unify_enclosed_type(
lhs.clone(),
rhs.clone(),
self.unify(a.clone(), b.clone(), location, false),
)?;
}
Ok(())
} else {
Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})
}
} else {
Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})
}
Ok(())
}

(
Type::Fn {
args: args1,
ret: retrn1,
alias: _,
},
Type::Fn {
Type::Fn {
args: args1,
ret: retrn1,
alias: _,
} => {
if let Type::Fn {
args: args2,
ret: retrn2,
alias: _,
},
) if args1.len() == args2.len() => {
for (a, b) in args1.iter().zip(args2) {
self.unify(a.clone(), b.clone(), location, allow_cast)
.map_err(|_| Error::CouldNotUnify {
} = rhs.deref()
{
if args1.len() == args2.len() {
for (a, b) in args1.iter().zip(args2) {
self.unify(a.clone(), b.clone(), location, allow_cast)
.map_err(|_| Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})?;
}
self.unify(retrn1.clone(), retrn2.clone(), location, false)
.map_err(|_| Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})
} else {
Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})?;
})
}
} else {
Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})
}
self.unify(retrn1.clone(), retrn2.clone(), location, false)
.map_err(|_| Error::CouldNotUnify {
}
Type::Pair { fst, snd, alias: _ } => {
if let Type::Pair {
fst: fst2,
snd: snd2,
alias: _,
} = rhs.deref()
{
unify_enclosed_type(
lhs.clone(),
rhs.clone(),
self.unify(fst.clone(), fst2.clone(), location, false),
)?;

unify_enclosed_type(
lhs.clone(),
rhs.clone(),
self.unify(snd.clone(), snd2.clone(), location, false),
)?;

Ok(())
} else {
Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
})
}
}

_ => Err(Error::CouldNotUnify {
location,
expected: lhs.clone(),
given: rhs.clone(),
situation: None,
rigid_type_names: HashMap::new(),
}),
Type::Var { .. } => unreachable!(),
}
}

Expand Down Expand Up @@ -1801,7 +1879,7 @@ fn unify_unbound_type(tipo: Rc<Type>, own_id: u64, location: Span) -> Result<(),

Ok(())
}
Type::Pair { fst, snd, .. } => {
Type::Pair { fst, snd, alias: _ } => {
unify_unbound_type(fst.clone(), own_id, location)?;
unify_unbound_type(snd.clone(), own_id, location)?;

Expand Down
11 changes: 8 additions & 3 deletions crates/aiken-lang/src/tipo/exhaustive.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ use std::{collections::BTreeMap, iter, ops::Deref};
use itertools::Itertools;

use crate::{
ast, builtins,
ast,
builtins::{self, PAIR},
tipo::{self, environment::Environment, error::Error},
};

Expand Down Expand Up @@ -563,6 +564,8 @@ pub(super) fn simplify(
constructor: super::PatternConstructor::Record { name, .. },
..
} => {
let (empty, pair) = (&"".to_string(), &PAIR.to_string());

let (module, type_name, arity) = match tipo.deref() {
tipo::Type::App {
name: type_name,
Expand All @@ -575,11 +578,13 @@ pub(super) fn simplify(
module,
..
} => (module, type_name, args.len()),
tipo::Type::Pair { .. } => (empty, pair, 2),
_ => {
unreachable!("ret should be a Type::App")
unreachable!("ret should be a Type::App or Type::Pair")
}
},
_ => unreachable!("tipo should be a Type::App"),
tipo::Type::Pair { .. } => (empty, pair, 2),
_ => unreachable!("tipo should be a Type::App or Type::Pair"),
};

let alts = environment.get_constructors_for_type(module, type_name, *location)?;
Expand Down

0 comments on commit 69e6a1a

Please sign in to comment.