aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/checker_set.rs48
-rw-r--r--src/checker_signature.rs10
-rw-r--r--src/checker_state.rs62
-rw-r--r--src/main.rs34
4 files changed, 100 insertions, 54 deletions
diff --git a/src/checker_set.rs b/src/checker_set.rs
index 2faca9e..7ff6e4a 100644
--- a/src/checker_set.rs
+++ b/src/checker_set.rs
@@ -10,10 +10,16 @@ impl CheckerState {
match set {
Set::BuiltIn(_) => Ok(set.clone()),
Set::Record(fields) => {
+ let mut ctx = self.clone();
let fields = fields
.into_iter()
.map(|RecordField { name, set }| {
- let set = self.check_set(set)?;
+ let set = ctx.check_set(set)?;
+ ctx.add_element(
+ name.clone(),
+ Value::Hypothetical(set.clone()),
+ set.clone(),
+ )?;
Ok(RecordField { name, set })
})
.collect::<Result<Vec<_>, _>>()?;
@@ -68,7 +74,7 @@ impl CheckerState {
// hypothetical from a call to check_element, in the context of
// check_element, we can safely ignore its payload. I'll point this
// out later as (*)
- ElementValue::Hypothetical(ref h_set) => {
+ Value::Hypothetical(ref h_set) => {
if !self.equal(set, &h_set) {
Err(CheckerError::WrongSetForElement {
value: value.clone(),
@@ -79,7 +85,7 @@ impl CheckerState {
Ok(value)
}
}
- ElementValue::Concrete(ref element @ Element::Literal(ref lit)) => {
+ Value::Concrete(ref element @ Element::Literal(ref lit)) => {
let value = value.clone();
// we may infer the type from the element
match lit {
@@ -101,20 +107,20 @@ impl CheckerState {
}
Ok(element.clone().into())
}
- ElementValue::Concrete(Element::Var(ref v)) => {
+ Value::Concrete(Element::Var(ref v)) => {
let lookup = self.lookup_element(&v)?;
// we have previously done the work to discover the type of
// this element, so what we're claiming now must match!
- if !self.equal(set, &lookup.set) {
+ if !self.equal(set, &lookup.container) {
return Err(CheckerError::WrongSetForElement {
value: value.clone(),
claimed: set.clone(),
- real: lookup.set.clone(),
+ real: lookup.container.clone(),
});
}
Ok(lookup.value.clone())
}
- ElementValue::Concrete(ref concrete @ Element::Record(ref assignations)) => {
+ Value::Concrete(ref concrete @ Element::Record(ref assignations)) => {
let rej = |reason| CheckerError::ElementDoesNotBelong {
element: concrete.clone(),
claimed: set.clone(),
@@ -159,18 +165,18 @@ impl CheckerState {
// rebuild, hypotheticals are contagious
let assignations = zip(element_fnames, sub_els)
.map(|(name, element)| match element {
- ElementValue::Concrete(element) => Some(ElemAssign { name, element }),
- ElementValue::Hypothetical(_) => None,
+ Value::Concrete(element) => Some(ElemAssign { name, element }),
+ Value::Hypothetical(_) => None,
})
.collect();
// resign?
Ok(if let Some(assignations) = assignations {
Element::Record(assignations).into()
} else {
- ElementValue::Hypothetical(set.clone())
+ Value::Hypothetical(set.clone())
})
}
- ElementValue::Concrete(Element::Project {
+ Value::Concrete(Element::Project {
element: ref inner,
ref field,
}) => {
@@ -193,7 +199,7 @@ impl CheckerState {
// enforce the correct typing of the element
let inner = self.check_element((*inner.clone()).into(), owner_set)?;
match inner {
- ElementValue::Concrete(inner) => {
+ Value::Concrete(inner) => {
// Unfortunately we still have to do something nasty here to obtain the data
let Element::Record(assignations) = inner else {
panic!(
@@ -212,10 +218,10 @@ impl CheckerState {
Ok(sub_element.into())
}
// correct by (*)
- ElementValue::Hypothetical(_) => Ok(ElementValue::Hypothetical(set.clone())),
+ Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
}
}
- ElementValue::Concrete(Element::Inject {
+ Value::Concrete(Element::Inject {
element: ref inner,
ref field,
}) => {
@@ -240,16 +246,16 @@ impl CheckerState {
let element = self.check_element((*inner.clone()).into(), field_set)?;
match element {
- ElementValue::Concrete(element) => Ok(Element::Inject {
+ Value::Concrete(element) => Ok(Element::Inject {
element: Box::new(element),
field: field.clone(),
}
.into()),
// correct by (*)
- ElementValue::Hypothetical(_) => Ok(ElementValue::Hypothetical(set.clone())),
+ Value::Hypothetical(_) => Ok(Value::Hypothetical(set.clone())),
}
}
- ElementValue::Concrete(
+ Value::Concrete(
ref element @ Element::Case {
ref arms,
ref scrutinee,
@@ -303,8 +309,8 @@ impl CheckerState {
// which variant are we, if any
let matching: Option<(String, Element)> = match scrutinee {
- ElementValue::Hypothetical(_) => None,
- ElementValue::Concrete(Element::Inject {
+ Value::Hypothetical(_) => None,
+ Value::Concrete(Element::Inject {
field,
element: inner,
}) => Some((field, *inner)),
@@ -348,13 +354,13 @@ impl CheckerState {
} else {
new_context.add_element(
binding_name,
- ElementValue::Hypothetical(field_set.clone()),
+ Value::Hypothetical(field_set.clone()),
binding_set,
)?;
new_context.check_element(arm.body.clone().into(), set)?;
};
}
- Ok(computed_output.unwrap_or(ElementValue::Hypothetical(set.clone())))
+ Ok(computed_output.unwrap_or(Value::Hypothetical(set.clone())))
}
}
}
diff --git a/src/checker_signature.rs b/src/checker_signature.rs
index 4fa723f..4d5f02c 100644
--- a/src/checker_signature.rs
+++ b/src/checker_signature.rs
@@ -12,14 +12,20 @@ impl CheckerState {
let deref = self.lookup_signature(&v)?;
Ok(deref.clone())
}
- Signature::Ext { params, codomain } => Err(CheckerError::Unimplemented(
+ Signature::Ext { .. } => Err(CheckerError::Unimplemented(
"extension signatures".to_string(),
)),
Signature::Theory(fields) => {
+ let mut ctx = self.clone();
let fields = fields
.into_iter()
.map(|SigField { signature, name }| {
- let signature = self.check_signature(signature)?;
+ let signature = ctx.check_signature(signature)?;
+ ctx.add_instance(
+ name.clone(),
+ InstanceValue::Hypothetical(signature.clone()),
+ signature.clone(),
+ )?;
Ok(SigField { name, signature })
})
.collect::<Result<Vec<_>, _>>()?;
diff --git a/src/checker_state.rs b/src/checker_state.rs
index 31c3bde..a14a6e4 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -37,6 +37,8 @@ pub enum CheckerError {
},
}
+// -----------------------------------------------------------------------------
+// Generics for wrapping fields, values, and coercing them
#[derive(Display, Clone)]
#[display("{field} @ {owner}")]
pub struct Field<T: std::fmt::Display> {
@@ -45,31 +47,45 @@ pub struct Field<T: std::fmt::Display> {
}
#[derive(Display, Clone)]
-pub enum ElementValue {
- Concrete(Element),
+pub enum Value<Term: std::fmt::Display, Type: std::fmt::Display> {
+ Concrete(Term),
#[display("_ : {_0}")]
- Hypothetical(Set),
+ Hypothetical(Type),
+}
+
+pub type ElementValue = Value<Element, Set>;
+pub type InstanceValue = Value<Instance, Signature>;
+
+impl From<Element> for Value<Element, Set> {
+ fn from(e: Element) -> Value<Element, Set> {
+ Value::Concrete(e)
+ }
}
-impl From<Element> for ElementValue {
- fn from(e: Element) -> ElementValue {
- ElementValue::Concrete(e)
+impl From<Instance> for Value<Instance, Signature> {
+ fn from(i: Instance) -> Value<Instance, Signature> {
+ Value::Concrete(i)
}
}
#[derive(Display, Clone)]
-#[display("{value} : {set}")]
-pub struct CheckedElement {
- pub value: ElementValue,
- pub set: Set,
+#[display("{value} : {container}")]
+pub struct Checked<Term: std::fmt::Display, Type: std::fmt::Display> {
+ pub value: Value<Term, Type>,
+ pub container: Type,
}
+pub type CheckedElement = Checked<Element, Set>;
+pub type CheckedInstance = Checked<Instance, Signature>;
+
+// -----------------------------------------------------------------------------
+// The checker state
#[derive(Default, Clone)]
pub struct CheckerState {
wf_sets: HashMap<String, Set>,
wf_elements: HashMap<String, CheckedElement>,
wf_signatures: HashMap<String, Signature>,
- wf_instances: HashMap<String, Instance>,
+ wf_instances: HashMap<String, CheckedInstance>,
record_fields: HashMap<String, Field<Set>>,
variant_fields: HashMap<String, Field<Set>>,
signature_fields: HashMap<String, Field<Signature>>,
@@ -239,15 +255,15 @@ impl CheckerState {
pub fn add_element(
&mut self,
name: String,
- element: ElementValue,
+ element: Value<Element, Set>,
set: Set,
) -> Result<(), CheckerError> {
self.assert_unbound_element(&name)?;
self.wf_elements.insert(
name,
- CheckedElement {
+ Checked {
value: element,
- set,
+ container: set,
},
);
Ok(())
@@ -344,6 +360,24 @@ impl CheckerState {
Ok(())
}
+ #[instrument(skip(self), level = "debug", fields(%name, %instance, %signature))]
+ pub fn add_instance(
+ &mut self,
+ name: String,
+ instance: InstanceValue,
+ signature: Signature,
+ ) -> Result<(), CheckerError> {
+ self.assert_unbound_element(&name)?;
+ self.wf_instances.insert(
+ name,
+ Checked {
+ value: instance,
+ container: signature,
+ },
+ );
+ Ok(())
+ }
+
pub fn lookup_signature(&self, name: &String) -> Result<&Signature, CheckerError> {
self.wf_signatures
.get(name)
diff --git a/src/main.rs b/src/main.rs
index 2b798e1..7d04891 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -19,35 +19,35 @@ fn main() {
let src = r#"
-let set X = record { .b : Bool, .n : Nat } // basic
-
+// let X be the set Y, call it Z
+let set X = record { .b : Bool, .n : Nat }
let set Y = X
-
let set Z = record { .y : Y }
-
-let set W = variant [ z. : Z | f. : Float ]
-
+// make some elements
let element x : X = { .b = true, .n = 41 }
-
let element z : Z = { .y = x }
+// exercise case matching
+let set Z_or_Float = variant [ z. : Z | f. : Float ]
+let element injected : Z_or_Float = z. z
+let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]
-let element the_nat : Nat = z .y .n
-
-let element injected : W = z. z
-
-let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => myf ]
+let signature Graph = theory {
+ .Node :: Set,
+ .Edge :: (s : Node) (t : Node) -> Set
+}
-// let signature Graph = theory {
-// .Node :: Set,
-// .Edge :: (s : Node) (t : Node) -> Set
-// }
-//
// let instance natPoset :: Graph = {
// .Node = Nat,
// .Edge = for (s : Nat) (t : Nat), Bool
// }
//
// let element node : set-of(natPoset .Node) = 7
+//
+// let set NatEdges = record {
+// .source: set-of(natPoset .Node),
+// .target: set-of(natPoset .Node),
+// .connected set-of(natPoset .Edge source target)
+// }
"#;
let programme = parser::parser::program(src);
generated by cgit v1.3.1 (git 2.54.0) at 2026-08-30 22:15:22 +0000