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.

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

feat: Extension validation can take a closure of solutions #456

Merged
merged 2 commits into from
Aug 25, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
3 changes: 2 additions & 1 deletion src/builder/dataflow.rs
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,8 @@ impl DFGBuilder<Hugr> {

impl HugrBuilder for DFGBuilder<Hugr> {
fn finish_hugr(mut self) -> Result<Hugr, ValidationError> {
self.base.infer_extensions()?;
let closure = self.base.infer_extensions()?;
self.base.validate_with_extension_closure(closure)?;
Ok(self.base)
}
}
Expand Down
31 changes: 28 additions & 3 deletions src/extension/infer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,23 @@ use thiserror::Error;
pub type ExtensionSolution = HashMap<(Node, Direction), ExtensionSet>;

/// Infer extensions for a hugr. This is the main API exposed by this module
pub fn infer_extensions(hugr: &impl HugrView) -> Result<ExtensionSolution, InferExtensionError> {
///
/// Return a tuple of the solutions found for locations on the graph, and a
/// closure: a solution which would be valid if all of the variables in the graph
/// were instantiated to an empty extension set. This is used (by validation) to
/// concretise the extension requirements of the whole hugr.
pub fn infer_extensions(
hugr: &impl HugrView,
) -> Result<(ExtensionSolution, ExtensionSolution), InferExtensionError> {
let mut ctx = UnificationContext::new(hugr);
ctx.main_loop()
let solution = ctx.main_loop()?;
ctx.instantiate_variables();
let closed_solution = ctx.main_loop()?;
let closure: HashMap<(Node, Direction), ExtensionSet> = closed_solution
.into_iter()
.filter(|(loc, _)| !solution.contains_key(loc))
.collect();
Ok((solution, closure))
}

/// Metavariables don't need much
Expand Down Expand Up @@ -599,6 +613,16 @@ impl UnificationContext {
}
self.results()
}

/// Instantiate all variables in the graph with the empty extension set.
/// This is done to solve metas which depend on variables, which allows
/// us to come up with a fully concrete solution to pass into validation.
pub fn instantiate_variables(&mut self) {
for m in self.variables.clone().into_iter() {
self.add_solution(m, ExtensionSet::new());
}
self.variables = HashSet::new();
}
}

#[cfg(test)]
Expand Down Expand Up @@ -856,7 +880,8 @@ mod test {
let hugr = builder.base;
// TODO: when we put new extensions onto the graph after inference, we
// can call `finish_hugr` and just look at the graph
let solution = infer_extensions(&hugr)?;
let (solution, extra) = infer_extensions(&hugr)?;
assert!(extra.is_empty());
assert_eq!(
*solution.get(&(src.node(), Direction::Outgoing)).unwrap(),
rs
Expand Down
7 changes: 5 additions & 2 deletions src/extension/validate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,12 @@ pub struct ExtensionValidator {
impl ExtensionValidator {
/// Initialise a new extension validator, pre-computing the extension
/// requirements for each node in the Hugr.
pub fn new(hugr: &Hugr) -> Self {
///
/// The `closure` argument is a set of extensions which doesn't actually
/// live on the graph, but is used to close the graph for validation
pub fn new(hugr: &Hugr, closure: HashMap<(Node, Direction), ExtensionSet>) -> Self {
let mut validator = ExtensionValidator {
extensions: HashMap::new(),
extensions: closure,
};

for node in hugr.nodes() {
Expand Down
10 changes: 6 additions & 4 deletions src/hugr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ pub mod serialize;
pub mod validate;
pub mod views;

use std::collections::VecDeque;
use std::collections::{HashMap, VecDeque};
use std::iter;

pub(crate) use self::hugrmut::HugrInternalsMut;
Expand Down Expand Up @@ -194,10 +194,12 @@ impl Hugr {
}

/// Infer extension requirements
pub fn infer_extensions(&mut self) -> Result<(), InferExtensionError> {
let solution = infer_extensions(self)?;
pub fn infer_extensions(
&mut self,
) -> Result<HashMap<(Node, Direction), ExtensionSet>, InferExtensionError> {
let (solution, extension_closure) = infer_extensions(self)?;
self.instantiate_extensions(solution);
Ok(())
Ok(extension_closure)
}

/// TODO: Write this
Expand Down
25 changes: 20 additions & 5 deletions src/hugr/validate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ use pyo3::prelude::*;

use crate::extension::{
validate::{ExtensionError, ExtensionValidator},
InferExtensionError,
ExtensionSet, InferExtensionError,
};
use crate::ops::validate::{ChildrenEdgeData, ChildrenValidationError, EdgeValidationError};
use crate::ops::{OpTag, OpTrait, OpType, ValidateOp};
Expand All @@ -38,20 +38,35 @@ struct ValidationContext<'a> {
}

impl Hugr {
/// Check the validity of the HUGR.
/// Check the validity of the HUGR, assuming that it has no open extension
/// variables.
/// TODO: Add a version of validation which allows for open extension
/// variables (see github issue #457)
pub fn validate(&self) -> Result<(), ValidationError> {
let mut validator = ValidationContext::new(self);
self.validate_with_extension_closure(HashMap::new())
Copy link
Member

Choose a reason for hiding this comment

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

please add a todo for validating hugrs with input extension set variables

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I've added issue #457 after our discussion this morning

Copy link
Member

Choose a reason for hiding this comment

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

cool, the comment here can link to that then

}

/// Check the validity of a hugr, taking an argument of a closure for the
/// free extension variables
pub fn validate_with_extension_closure(
&self,
closure: HashMap<(Node, Direction), ExtensionSet>,
) -> Result<(), ValidationError> {
let mut validator = ValidationContext::new(self, closure);
validator.validate()
}
}

impl<'a> ValidationContext<'a> {
/// Create a new validation context.
pub fn new(hugr: &'a Hugr) -> Self {
pub fn new(
hugr: &'a Hugr,
extension_closure: HashMap<(Node, Direction), ExtensionSet>,
) -> Self {
Self {
hugr,
dominators: HashMap::new(),
extension_validator: ExtensionValidator::new(hugr),
extension_validator: ExtensionValidator::new(hugr, extension_closure),
}
}

Expand Down