diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ast.rs | 3 | ||||
| -rw-r--r-- | src/checker_set.rs | 30 | ||||
| -rw-r--r-- | src/checker_signature.rs | 8 | ||||
| -rw-r--r-- | src/parser.rs | 12 |
4 files changed, 41 insertions, 12 deletions
@@ -108,6 +108,9 @@ pub struct ElemAssign { #[derive(Clone, PartialEq, Display, Debug)] pub enum Element { + #[display{"element-of({_0})"}] + ClaimedElement(Box<Instance>), + #[display("{_0}")] Literal(Literal), diff --git a/src/checker_set.rs b/src/checker_set.rs index f13f686..2f934e2 100644 --- a/src/checker_set.rs +++ b/src/checker_set.rs @@ -120,6 +120,17 @@ impl CheckerState { } Ok(element.clone().into()) } + Element::ClaimedElement(instance) => { + let instance = self.check_instance( + instance.as_ref(), + set.map(|s| Signature::FromSet(s.clone())).as_ref(), + )?; + if let Instance::ElementCoerce(element) = instance { + Ok(element) + } else { + Ok(Element::ClaimedElement(Box::new(instance))) + } + } Element::Var(v) => { let lookup = self.lookup_element(&v)?; @@ -275,12 +286,13 @@ impl CheckerState { match inner { // We're stuck on something that bottoms out in a binding // blocking computation, nothing to be done here - Element::Var(_) | Element::Project { .. } | Element::Case { .. } => { - Ok(Element::Project { - element: Box::new(inner), - field: field.clone(), - }) - } + Element::Var(_) + | Element::Project { .. } + | Element::Case { .. } + | Element::ClaimedElement(_) => Ok(Element::Project { + element: Box::new(inner), + field: field.clone(), + }), Element::Record(assignations) => { let sub_element = assignations .into_iter() @@ -382,7 +394,10 @@ impl CheckerState { } => Some((field.clone(), *inner.clone())), // These are all the cases which could become stuck on a // formal binding - Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None, + Element::Var(_) + | Element::Project { .. } + | Element::Case { .. } + | Element::ClaimedElement(_) => None, Element::Literal(_) | Element::Record(_) => panic!( "invariant violation: scrutinee is a non-variant value at variant set" ), @@ -394,6 +409,7 @@ impl CheckerState { let posit_equality_with = match &scrutinee { Element::Var(v) => Some(v.clone()), Element::Inject { .. } + | Element::ClaimedElement(_) | Element::Project { .. } | Element::Case { .. } | Element::Literal(_) diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 1ce8bc8..6acd271 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -336,7 +336,10 @@ impl CheckerState { ref field, element: ref inner, } => Some((field.clone(), *inner.clone())), - Element::Var(_) | Element::Project { .. } | Element::Case { .. } => None, + Element::ClaimedElement(_) + | Element::Var(_) + | Element::Project { .. } + | Element::Case { .. } => None, Element::Literal(_) | Element::Record(_) => panic!( "invariant violation: scrutinee is a non-variant value at variant set" ), @@ -344,7 +347,8 @@ impl CheckerState { let posit_equality_with = match &scrutinee { Element::Var(v) => Some(v.clone()), - Element::Inject { .. } + Element::ClaimedElement(_) + | Element::Inject { .. } | Element::Project { .. } | Element::Case { .. } | Element::Literal(_) diff --git a/src/parser.rs b/src/parser.rs index 8dbc31e..6ab5900 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -32,6 +32,7 @@ parser! { rule kw_theory() = "theory" wb() rule kw_case() = "case" wb() rule kw_of() = "of" wb() + rule kw_element_of() = "element-of" wb() rule kw_for() = "for" wb() rule kw_set() = "set" wb() rule kw_set_of() = "set-of" wb() @@ -48,8 +49,8 @@ parser! { kw_let_set() / kw_let_element() / kw_let_signature() / kw_let_instance() / kw_record() / kw_variant() / kw_theory() / kw_case() / kw_of() / kw_for() - / kw_Set() / kw_set_of() / kw_set() - / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() + / kw_Set() / kw_set_of() / kw_set() / kw_element_of() + / kw_Nat() / kw_Int() / kw_Float() / kw_Str() / kw_Bool() / kw_true() / kw_false() // ==================================================================== @@ -205,8 +206,13 @@ parser! { = _ t:inject() _ x:elem_var() _ "=>" _ body:element() _ { CaseArm { tag: t, bound: x, body } } + rule claimed_element() -> Instance + = kw_element_of() _ "(" _ i:instance() _ ")" { i } + + rule element() -> Element - = kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } + = i:claimed_element() { Element::ClaimedElement(Box::new(i)) } + / kw_case() _ scrut:element() _ kw_of() _ "[" _ arms:(case_arm() ** "|") _ "]" { Element::Case { scrutinee: Box::new(scrut), arms } } / d:dot_elem() { d } // ==================================================================== |