summaryrefslogtreecommitdiff
path: root/src/ast/typed.rs
diff options
context:
space:
mode:
authorGreg Brown <gmb60@cam.ac.uk>2020-11-20 16:04:50 +0000
committerGreg Brown <gmb60@cam.ac.uk>2020-11-20 16:04:50 +0000
commitaa7585d8bf84f27adeaf57e35f430e2e82a5d208 (patch)
treed96b08c3156b976455091d862f157b8e52c66c2d /src/ast/typed.rs
parent8939af712e6c3ae5d23019ec5dd941f1dae6c7fb (diff)
Precompute properties of well-typed terms
Diffstat (limited to 'src/ast/typed.rs')
-rw-r--r--src/ast/typed.rs17
1 files changed, 14 insertions, 3 deletions
diff --git a/src/ast/typed.rs b/src/ast/typed.rs
index 48ca740..e277cbb 100644
--- a/src/ast/typed.rs
+++ b/src/ast/typed.rs
@@ -1,4 +1,5 @@
use super::Typed;
+use super::VariableError;
use std::collections::BTreeSet;
use std::fmt::Display;
@@ -79,6 +80,8 @@ impl FlastSet {
pub trait NullContext {
type PushNull: NullContext;
+ fn get_depth(&self) -> usize;
+
fn get_nullable(&self, index: usize) -> Option<bool>;
fn push_nullable<F: FnOnce(&mut Self::PushNull) -> R, R>(&mut self, nullable: bool, f: F) -> R;
@@ -115,15 +118,23 @@ pub trait Type {
type Err: Display;
/// # Errors
- /// Returns [`None`] if the nullity cannot be determined.
+ /// Returns [`Err`] if there is a variable with an index greater than or equal
+ /// to `depth`.
+ fn closed(&self, depth: usize) -> Result<(), VariableError>;
+
+ /// # Errors
+ /// Returns [`None`] only if `self.closed(context.get_depth())` returns an
+ /// [`Err`].
fn is_nullable<C: NullContext>(&self, context: &mut C) -> Option<bool>;
/// # Errors
- /// Returns [`None`] if the first set cannot be determined.
+ /// Returns [`None`] only if `self.closed(context.get_depth())` returns an
+ /// [`Err`].
fn first_set<C: FirstSetContext>(&self, context: &mut C) -> Option<FirstSet>;
/// # Errors
- /// Returns [`None`] if the flast set cannot be determined.
+ /// Returns [`None`] only if `self.closed(context.get_depth())` returns an
+ /// [`Err`].
fn flast_set<C: FlastSetContext>(&self, context: &mut C) -> Option<FlastSet>;
/// # Errors