Skip to content

Commit

Permalink
update pair to handle alias
Browse files Browse the repository at this point in the history
  • Loading branch information
MicroProofs committed Apr 27, 2024
1 parent 2c06732 commit eebf306
Show file tree
Hide file tree
Showing 10 changed files with 111 additions and 19 deletions.
20 changes: 19 additions & 1 deletion crates/aiken-lang/src/ast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -970,6 +970,11 @@ pub enum Annotation {
location: Span,
elems: Vec<Self>,
},
Pair {
location: Span,
fst: Box<Self>,
snd: Box<Self>,
},
}

impl Annotation {
Expand All @@ -979,7 +984,8 @@ impl Annotation {
| Annotation::Tuple { location, .. }
| Annotation::Var { location, .. }
| Annotation::Hole { location, .. }
| Annotation::Constructor { location, .. } => *location,
| Annotation::Constructor { location, .. }
| Annotation::Pair { location, .. } => *location,
}
}

Expand Down Expand Up @@ -1081,6 +1087,18 @@ impl Annotation {
} => name == o_name,
_ => false,
},
Annotation::Pair { fst, snd, .. } => {
if let Annotation::Pair {
fst: o_fst,
snd: o_snd,
..
} = other
{
fst.is_logically_equal(o_fst) && snd.is_logically_equal(o_snd)
} else {
false
}
}
}
}

Expand Down
6 changes: 5 additions & 1 deletion crates/aiken-lang/src/builtins.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1335,7 +1335,11 @@ pub fn tuple(elems: Vec<Rc<Type>>) -> Rc<Type> {
}

pub fn pair(fst: Rc<Type>, snd: Rc<Type>) -> Rc<Type> {
Rc::new(Type::Pair { fst, snd })
Rc::new(Type::Pair {
fst,
snd,
alias: None,
})
}

pub fn bool() -> Rc<Type> {
Expand Down
1 change: 1 addition & 0 deletions crates/aiken-lang/src/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -424,6 +424,7 @@ impl<'comments> Formatter<'comments> {
Annotation::Tuple { elems, .. } => {
wrap_args(elems.iter().map(|t| (self.annotation(t), false)))
}
Annotation::Pair { .. } => todo!(),
}
.group()
}
Expand Down
58 changes: 47 additions & 11 deletions crates/aiken-lang/src/tipo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ pub enum Type {
Pair {
fst: Rc<Type>,
snd: Rc<Type>,
alias: Option<Rc<TypeAliasAnnotation>>,
},
}

Expand Down Expand Up @@ -139,6 +140,18 @@ impl PartialEq for Type {
false
}
}
Type::Pair { fst, snd, .. } => {
if let Type::Pair {
fst: fst2,
snd: snd2,
..
} = other
{
fst == fst2 && snd == snd2
} else {
false
}
}
}
}
}
Expand All @@ -149,7 +162,8 @@ impl Type {
Type::App { alias, .. }
| Type::Fn { alias, .. }
| Type::Var { alias, .. }
| Type::Tuple { alias, .. } => alias.clone(),
| Type::Tuple { alias, .. }
| Type::Pair { alias, .. } => alias.clone(),
}
}

Expand Down Expand Up @@ -184,6 +198,7 @@ impl Type {
} => Type::Fn { args, ret, alias },
Type::Var { tipo, alias: _ } => Type::Var { tipo, alias },
Type::Tuple { elems, alias: _ } => Type::Tuple { elems, alias },
Type::Pair { fst, snd, alias: _ } => Type::Pair { fst, snd, alias },
})
}

Expand All @@ -196,6 +211,7 @@ impl Type {
_ => None,
},
Type::Tuple { .. } => Some((String::new(), "Tuple".to_string())),
Type::Pair { .. } => Some((String::new(), "Pair".to_string())),
}
}

Expand Down Expand Up @@ -346,22 +362,22 @@ impl Type {
.first()
.expect("unreachable: List should have an inner type")
.is_pair(),
Self::Var { tipo } => tipo.borrow().is_map(),
Self::Var { tipo, .. } => tipo.borrow().is_map(),
_ => false,
}
}

pub fn is_tuple(&self) -> bool {
match self {
Self::Var { tipo } => tipo.borrow().is_tuple(),
Self::Var { tipo, .. } => tipo.borrow().is_tuple(),
Self::Tuple { .. } => true,
_ => false,
}
}

pub fn is_pair(&self) -> bool {
match self {
Self::Var { tipo } => tipo.borrow().is_pair(),
Self::Var { tipo, .. } => tipo.borrow().is_pair(),
Self::Pair { .. } => true,
_ => false,
}
Expand All @@ -385,22 +401,22 @@ impl Type {
is_a_generic
}

Self::Var { tipo } => tipo.borrow().is_generic(),
Self::Tuple { elems } => {
Self::Var { tipo, .. } => tipo.borrow().is_generic(),
Self::Tuple { elems, .. } => {
let mut is_a_generic = false;
for elem in elems {
is_a_generic = is_a_generic || elem.is_generic();
}
is_a_generic
}
Self::Fn { args, ret } => {
Self::Fn { args, ret, .. } => {
let mut is_a_generic = false;
for arg in args {
is_a_generic = is_a_generic || arg.is_generic();
}
is_a_generic || ret.is_generic()
}
Self::Pair { fst, snd } => fst.is_generic() || snd.is_generic(),
Self::Pair { fst, snd, .. } => fst.is_generic() || snd.is_generic(),
}
}

Expand All @@ -415,7 +431,7 @@ impl Type {

pub fn get_generic(&self) -> Option<u64> {
match self {
Self::Var { tipo } => tipo.borrow().get_generic(),
Self::Var { tipo, .. } => tipo.borrow().get_generic(),
_ => None,
}
}
Expand Down Expand Up @@ -466,7 +482,7 @@ impl Type {
} else if self.is_tuple() {
match self {
Self::Tuple { .. } => UplcType::List(UplcType::Data.into()),
Self::Var { tipo } => tipo.borrow().get_uplc_type().unwrap(),
Self::Var { tipo, .. } => tipo.borrow().get_uplc_type().unwrap(),
_ => unreachable!(),
}
} else if self.is_pair() {
Expand Down Expand Up @@ -559,7 +575,7 @@ impl Type {

TypeVar::Link { tipo, .. } => tipo.find_private_type(),
},
Self::Pair { fst, snd } => {
Self::Pair { fst, snd, .. } => {
if let Some(private_type) = fst.find_private_type() {
Some(private_type)
} else {
Expand Down Expand Up @@ -745,6 +761,16 @@ pub fn convert_opaque_type(
}
.into()
}
Type::Pair { fst, snd, alias } => {
let fst = convert_opaque_type(fst, data_types, deep);
let snd = convert_opaque_type(snd, data_types, deep);
Type::Pair {
fst,
snd,
alias: alias.clone(),
}
.into()
}
}
}
}
Expand Down Expand Up @@ -834,6 +860,16 @@ pub fn find_and_replace_generics(
TypeVar::Generic { .. } | TypeVar::Unbound { .. } => unreachable!(),
}
}
Type::Pair { fst, snd, alias } => {
let fst = find_and_replace_generics(fst, mono_types);
let snd = find_and_replace_generics(snd, mono_types);
Type::Pair {
fst,
snd,
alias: alias.clone(),
}
.into()
}
}
} else {
tipo.clone()
Expand Down
18 changes: 16 additions & 2 deletions crates/aiken-lang/src/tipo/environment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use crate::{
RecordConstructor, RecordConstructorArg, Span, TypeAlias, TypedDefinition, TypedPattern,
UnqualifiedImport, UntypedArg, UntypedDefinition, Use, Validator, PIPE_VARIABLE,
},
builtins::{function, generic_var, tuple, unbound_var},
builtins::{function, generic_var, pair, tuple, unbound_var},
tipo::{fields::FieldMap, TypeAliasAnnotation},
IdGenerator,
};
Expand Down Expand Up @@ -644,6 +644,13 @@ impl<'a> Environment<'a> {
),
alias.clone(),
),
Type::Pair { fst, snd, alias } => Type::with_alias(
pair(
self.instantiate(fst.clone(), ids, hydrator),
self.instantiate(snd.clone(), ids, hydrator),
),
alias.clone(),
),
}
}

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

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

Expand Down Expand Up @@ -1976,5 +1983,12 @@ pub(crate) fn generalise(t: Rc<Type>, ctx_level: usize) -> Rc<Type> {
),
alias.clone(),
),
Type::Pair { fst, snd, alias } => Type::with_alias(
pair(
generalise(fst.clone(), ctx_level),
generalise(snd.clone(), ctx_level),
),
alias.clone(),
),
}
}
4 changes: 4 additions & 0 deletions crates/aiken-lang/src/tipo/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2442,5 +2442,9 @@ pub fn ensure_serialisable(allow_fn: bool, t: Rc<Type>, location: Span) -> Resul
location,
),
},
Type::Pair { fst, snd, .. } => {
ensure_serialisable(false, fst.clone(), location)?;
ensure_serialisable(false, snd.clone(), location)
}
}
}
8 changes: 7 additions & 1 deletion crates/aiken-lang/src/tipo/hydrator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use super::{
};
use crate::{
ast::Annotation,
builtins::{function, tuple},
builtins::{function, pair, tuple},
tipo::Span,
};
use std::{collections::HashMap, rc::Rc};
Expand Down Expand Up @@ -246,6 +246,12 @@ impl Hydrator {

Ok(tuple(typed_elems))
}
Annotation::Pair { fst, snd, .. } => {
let fst = self.do_type_from_annotation(fst, environment, unbounds)?;
let snd = self.do_type_from_annotation(snd, environment, unbounds)?;

Ok(pair(fst, snd))
}
}?;

Ok(environment.annotate(return_type, annotation))
Expand Down
11 changes: 10 additions & 1 deletion crates/aiken-lang/src/tipo/infer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -843,7 +843,7 @@ fn infer_fuzzer(
}),
},

Type::App { .. } | Type::Tuple { .. } => Err(could_not_unify()),
Type::App { .. } | Type::Tuple { .. } | Type::Pair { .. } => Err(could_not_unify()),
}
}

Expand Down Expand Up @@ -894,5 +894,14 @@ fn annotate_fuzzer(tipo: &Type, location: &Span) -> Result<Annotation, Error> {
location: *location,
tipo: Rc::new(tipo.clone()),
}),
Type::Pair { fst, snd, .. } => {
let fst = annotate_fuzzer(fst, location)?;
let snd = annotate_fuzzer(snd, location)?;
Ok(Annotation::Pair {
fst: Box::new(fst),
snd: Box::new(snd),
location: *location,
})
}
}
}
2 changes: 1 addition & 1 deletion crates/aiken-lang/src/tipo/pretty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ impl Printer {
Type::Var { tipo: typ, .. } => self.type_var_doc(&typ.borrow()),

Type::Tuple { elems, .. } => self.args_to_aiken_doc(elems).surround("(", ")"),
Type::Pair { fst, snd } => self
Type::Pair { fst, snd, .. } => self
.args_to_aiken_doc(&[fst.clone(), snd.clone()])
.surround("Pair<", ">"),
}
Expand Down
2 changes: 1 addition & 1 deletion crates/aiken-project/src/blueprint/definitions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ impl Reference {
elems = Self::from_types(elems, type_parameters)
),
},
Type::Pair { fst, snd } => Self {
Type::Pair { fst, snd, .. } => Self {
inner: format!(
"Pair{fst}{snd}",
fst = Self::from_type(fst, type_parameters),
Expand Down

0 comments on commit eebf306

Please sign in to comment.