Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Ranged Integers #66

Open
wants to merge 10 commits into
base: master
Choose a base branch
from
Open

Ranged Integers #66

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
88210fe
Added delayed constraint
IBims1NicerTobi Feb 11, 2025
cec2fce
Removed clones
IBims1NicerTobi Feb 11, 2025
2ac9db2
Finished BinaryOpTypecheckConstraint
IBims1NicerTobi Feb 18, 2025
77cc284
Fixed operator sizes
IBims1NicerTobi Feb 18, 2025
d1fb001
Removed INT_CONCRETE_TYPE
IBims1NicerTobi Feb 18, 2025
84c9684
Add `FlatAlloc::try_map`
VonTum Feb 19, 2025
6b671d8
Removed constructor
IBims1NicerTobi Feb 19, 2025
940b99f
Fixed review
IBims1NicerTobi Feb 25, 2025
109a867
Fixed regression test
IBims1NicerTobi Feb 25, 2025
1d34f31
Fixed error message formatting
IBims1NicerTobi Mar 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
170 changes: 132 additions & 38 deletions src/instantiation/concrete_typecheck.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,15 @@
use std::ops::Deref;

use crate::alloc::{zip_eq, zip_eq3};
use sus_proc_macro::get_builtin_type;

use crate::alloc::{zip_eq, zip_eq3, UUID};
use crate::errors::ErrorInfoObject;
use crate::flattening::{DeclarationKind, ExpressionSource, WireReferenceRoot, WrittenType};
use crate::linker::LinkInfo;
use crate::typing::concrete_type::ConcreteGlobalReference;
use crate::typing::template::TemplateArgKind;
use crate::typing::{
concrete_type::{ConcreteType, BOOL_CONCRETE_TYPE, INT_CONCRETE_TYPE},
concrete_type::{ConcreteType, BOOL_CONCRETE_TYPE},
type_inference::{
DelayedConstraint, DelayedConstraintStatus, DelayedConstraintsList, FailedUnification,
},
Expand Down Expand Up @@ -52,7 +54,7 @@ impl InstantiationContext<'_, '_> {
)))
}

fn typecheck_all_wires(&self) {
fn typecheck_all_wires(&self, delayed_constraints: &mut DelayedConstraintsList<Self>) {
for this_wire_id in self.wires.id_range() {
let this_wire = &self.wires[this_wire_id];
let span = self.md.get_instruction_span(this_wire.original_instruction);
Expand Down Expand Up @@ -80,12 +82,12 @@ impl InstantiationContext<'_, '_> {
// TODO overloading
let (input_typ, output_typ) = match op {
UnaryOperator::Not => (BOOL_CONCRETE_TYPE, BOOL_CONCRETE_TYPE),
UnaryOperator::Negate => (INT_CONCRETE_TYPE, INT_CONCRETE_TYPE),
UnaryOperator::Negate => (self.new_int_type(), self.new_int_type()),
UnaryOperator::And | UnaryOperator::Or | UnaryOperator::Xor => {
(self.make_array_of(BOOL_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
}
UnaryOperator::Sum | UnaryOperator::Product => {
(self.make_array_of(INT_CONCRETE_TYPE), INT_CONCRETE_TYPE)
(self.make_array_of(self.new_int_type()), self.new_int_type())
}
};

Expand All @@ -104,6 +106,7 @@ impl InstantiationContext<'_, '_> {
}
&RealWireDataSource::BinaryOp { op, left, right } => {
// TODO overloading
// Typecheck generic INT
let ((in_left, in_right), out) = match op {
BinaryOperator::And => {
((BOOL_CONCRETE_TYPE, BOOL_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
Expand All @@ -114,39 +117,44 @@ impl InstantiationContext<'_, '_> {
BinaryOperator::Xor => {
((BOOL_CONCRETE_TYPE, BOOL_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
}
BinaryOperator::Add => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), INT_CONCRETE_TYPE)
}
BinaryOperator::Subtract => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), INT_CONCRETE_TYPE)
}
BinaryOperator::Multiply => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), INT_CONCRETE_TYPE)
}
BinaryOperator::Divide => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), INT_CONCRETE_TYPE)
}
BinaryOperator::Modulo => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), INT_CONCRETE_TYPE)
}
BinaryOperator::Equals => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
}
BinaryOperator::NotEquals => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
}
BinaryOperator::GreaterEq => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
}
BinaryOperator::Greater => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
}
BinaryOperator::LesserEq => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
}
BinaryOperator::Lesser => {
((INT_CONCRETE_TYPE, INT_CONCRETE_TYPE), BOOL_CONCRETE_TYPE)
BinaryOperator::Add
| BinaryOperator::Subtract
| BinaryOperator::Multiply
| BinaryOperator::Divide
| BinaryOperator::Modulo => {
delayed_constraints.push(BinaryOpTypecheckConstraint::new(
op,
left,
right,
this_wire_id,
span,
));
continue;
}
BinaryOperator::Equals => (
(self.new_int_type(), self.new_int_type()),
BOOL_CONCRETE_TYPE,
),
BinaryOperator::NotEquals => (
(self.new_int_type(), self.new_int_type()),
BOOL_CONCRETE_TYPE,
),
BinaryOperator::GreaterEq => (
(self.new_int_type(), self.new_int_type()),
BOOL_CONCRETE_TYPE,
),
BinaryOperator::Greater => (
(self.new_int_type(), self.new_int_type()),
BOOL_CONCRETE_TYPE,
),
BinaryOperator::LesserEq => (
(self.new_int_type(), self.new_int_type()),
BOOL_CONCRETE_TYPE,
),
BinaryOperator::Lesser => (
(self.new_int_type(), self.new_int_type()),
BOOL_CONCRETE_TYPE,
),
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wonder, it's not something that should concern us too badly, but maybe the boolean comparison ops should unify(left, right). Maybe, maybe not.

};
self.type_substitutor.unify_report_error(
&self.wires[this_wire_id].typ,
Expand Down Expand Up @@ -249,7 +257,7 @@ impl InstantiationContext<'_, '_> {
delayed_constraints.push(SubmoduleTypecheckConstraint { sm_id });
}

self.typecheck_all_wires();
self.typecheck_all_wires(&mut delayed_constraints);

delayed_constraints.resolve_delayed_constraints(self);

Expand Down Expand Up @@ -500,3 +508,89 @@ impl DelayedConstraint<InstantiationContext<'_, '_>> for SubmoduleTypecheckConst
.error(submod_instr.get_most_relevant_span(), message);
}
}

#[derive(Debug)]
struct BinaryOpTypecheckConstraint {
op: BinaryOperator,
left: UUID<WireIDMarker>,
right: UUID<WireIDMarker>,
out: UUID<WireIDMarker>,
span: Span,
}

impl BinaryOpTypecheckConstraint {
fn new(
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Redundant

op: BinaryOperator,
left: UUID<WireIDMarker>,
right: UUID<WireIDMarker>,
out: UUID<WireIDMarker>,
span: Span,
) -> Self {
Self {
op,
left,
right,
out,
span,
}
}
}

impl DelayedConstraint<InstantiationContext<'_, '_>> for BinaryOpTypecheckConstraint {
fn try_apply(&mut self, context: &mut InstantiationContext<'_, '_>) -> DelayedConstraintStatus {
if context.wires[self.left].typ.contains_unknown()
|| context.wires[self.right].typ.contains_unknown()
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You must call typ.fully_substitute() before you can call contains_unknown(). unify doesn't actually change the ConcreteType objects, it only changes the state of the TypeUnifier by adding to the substitution list

{
return DelayedConstraintStatus::NoProgress;
}
let left_complete_type = context.wires[self.left]
.typ
.try_fully_substitute(&context.type_substitutor)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, I see you're already doing a try_fully_substitute here. Then returning NoProgress should be when this returns None.

.unwrap();
let left_size = left_complete_type.unwrap_named().template_args[UUID::from_hidden_value(0)]
.unwrap_value()
.unwrap_integer();
let right_complete_type = context.wires[self.right]
.typ
.try_fully_substitute(&context.type_substitutor)
.unwrap();
#[rustfmt::skip]
let right_size = right_complete_type.unwrap_named().template_args[UUID::from_hidden_value(0)]
.unwrap_value()
.unwrap_integer();
let out_size = match self.op {
BinaryOperator::Add => left_size + right_size,
BinaryOperator::Subtract => left_size.clone(),
BinaryOperator::Multiply => left_size * right_size,
BinaryOperator::Divide => left_size.clone(),
BinaryOperator::Modulo => right_size.clone(),
_ => {
unreachable!("The BinaryOpTypecheckConstraint should only check arithmetic operation but got {}", self.op);
}
};
let mut template_args: FlatAlloc<ConcreteType, TemplateIDMarker> = FlatAlloc::new();
template_args.alloc(ConcreteType::new_int(out_size));
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could be combined with ConcreteType::new_int_type

let expected_out = ConcreteType::Named(ConcreteGlobalReference {
id: get_builtin_type!("int"),
template_args,
});

context.type_substitutor.unify_report_error(
&context.wires[self.out].typ,
&expected_out,
self.span,
"binary output",
);

DelayedConstraintStatus::Resolved
}

fn report_could_not_resolve_error(&self, context: &InstantiationContext<'_, '_>) {
let message = format!(
"Failed to Typecheck {:?} = {:?} {} {:?}",
self.out, self.right, self.op, self.left
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You should fully_substitute these, and ignore the return code. Otherwise this will just print type_variable_xyz

);

context.errors.error(self.span, message);
}
}
30 changes: 25 additions & 5 deletions src/instantiation/execute.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,13 @@ use crate::prelude::*;
use crate::typing::template::GlobalReference;

use num::BigInt;
use sus_proc_macro::get_builtin_type;

use crate::flattening::*;
use crate::value::{compute_binary_op, compute_unary_op, Value};

use crate::typing::{
abstract_type::DomainType,
concrete_type::{ConcreteType, INT_CONCRETE_TYPE},
template::TemplateArgKind,
abstract_type::DomainType, concrete_type::ConcreteType, template::TemplateArgKind,
};

use super::*;
Expand Down Expand Up @@ -181,9 +180,29 @@ impl InstantiationContext<'_, '_> {
self.template_args[*template_id].clone()
}
WrittenType::Named(named_type) => {
let mut template_args = FlatAlloc::new();
for template_arg in named_type.template_args.iter() {
let concrete_type = if let (_, Some(template_arg)) = template_arg {
match &template_arg.kind {
TemplateArgKind::Type(written_type) => {
self.concretize_type(written_type)?
}
TemplateArgKind::Value(uuid) => ConcreteType::Value(
self.generation_state
.get_generation_value(*uuid)
.unwrap()
.clone(),
),
}
} else {
ConcreteType::Unknown(self.type_substitutor.alloc())
};
template_args.alloc(concrete_type);
}

ConcreteType::Named(crate::typing::concrete_type::ConcreteGlobalReference {
id: named_type.id,
template_args: FlatAlloc::new(),
template_args,
})
}
WrittenType::Array(_, arr_box) => {
Expand Down Expand Up @@ -320,7 +339,8 @@ impl InstantiationContext<'_, '_> {
&WireReferencePathElement::ArrayAccess { idx, bracket_span } => {
let idx_wire = self.get_wire_or_constant_as_wire(idx, domain);
assert_eq!(
self.wires[idx_wire].typ, INT_CONCRETE_TYPE,
self.wires[idx_wire].typ.unwrap_named().id,
get_builtin_type!("int"),
"Caught by typecheck"
);
preamble.push(RealWirePathElem::ArrayAccess {
Expand Down
6 changes: 6 additions & 0 deletions src/instantiation/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -426,3 +426,9 @@ fn perform_instantiation(

context.extract()
}

impl InstantiationContext<'_, '_> {
pub fn new_int_type(&self) -> ConcreteType {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Redundant

self.type_substitutor.new_int_type()
}
}
8 changes: 6 additions & 2 deletions src/to_string.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,8 +140,12 @@ pub struct ConcreteTypeDisplay<'a, T: Index<TypeUUID, Output = StructType>> {
impl<T: Index<TypeUUID, Output = StructType>> Display for ConcreteTypeDisplay<'_, T> {
fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
match self.inner {
ConcreteType::Named(name) => {
f.write_str(&self.linker_types[name.id].link_info.get_full_name())
ConcreteType::Named(global_ref) => {
f.write_str(&self.linker_types[global_ref.id].link_info.get_full_name())?;
for template_arg in global_ref.template_args.iter() {
write!(f, "{}", template_arg.1.display(self.linker_types))?;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You should add the field names. Actually, there is a function that does this already: pretty_print_concrete_instance

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Where do I get the &LinkInfo from? Should it be added to the display proxy?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

&self.linker_types[global_ref.id].link_info

}
Ok(())
}
ConcreteType::Array(arr_box) => {
let (elem_typ, arr_size) = arr_box.deref();
Expand Down
37 changes: 32 additions & 5 deletions src/typing/concrete_type.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,17 +9,15 @@ use crate::value::Value;
use super::template::TVec;

use super::type_inference::ConcreteTypeVariableID;
use super::type_inference::ConcreteTypeVariableIDMarker;
use super::type_inference::HindleyMilner;
use super::type_inference::TypeSubstitutor;

pub const BOOL_CONCRETE_TYPE: ConcreteType = ConcreteType::Named(ConcreteGlobalReference {
id: get_builtin_type!("bool"),
template_args: FlatAlloc::new(),
});

pub const INT_CONCRETE_TYPE: ConcreteType = ConcreteType::Named(ConcreteGlobalReference {
id: get_builtin_type!("int"),
template_args: FlatAlloc::new(),
});

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct ConcreteGlobalReference<ID> {
pub id: ID,
Expand Down Expand Up @@ -47,13 +45,30 @@ pub enum ConcreteType {
}

impl ConcreteType {
pub fn new_int(int: BigInt) -> Self {
Self::Value(Value::Integer(int))
}
#[track_caller]
pub fn unwrap_value(&self) -> &Value {
let ConcreteType::Value(v) = self else {
unreachable!("unwrap_value on {self:?}")
};
v
}
#[track_caller]
pub fn unwrap_named(&self) -> &ConcreteGlobalReference<TypeUUID> {
let ConcreteType::Named(v) = self else {
unreachable!("unwrap_named")
};
v
}
pub fn down_array(&self) -> &ConcreteType {
let ConcreteType::Array(arr_box) = self else {
unreachable!("Must be an array!")
};
let (sub, _sz) = arr_box.deref();
sub
}
pub fn contains_unknown(&self) -> bool {
match self {
ConcreteType::Named(global_ref) => global_ref
Expand Down Expand Up @@ -103,4 +118,16 @@ impl ConcreteType {
1 // todo!() // Named structs are not implemented yet
}
}
pub fn try_fully_substitute(
&self,
substitutor: &TypeSubstitutor<Self, ConcreteTypeVariableIDMarker>,
) -> Option<Self> {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This implementation is incorrect. contains_unknown just checks this ConcreteType object, not the substituted version. You should base your return value on the boolean returned by fully_substitute

if self.contains_unknown() {
None
} else {
let mut self_clone = self.clone();
self_clone.fully_substitute(substitutor);
Some(self_clone)
}
}
}
Loading
Loading