aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/ast.rs74
-rw-r--r--src/checker.rs70
-rw-r--r--src/parser.rs8
3 files changed, 89 insertions, 63 deletions
diff --git a/src/ast.rs b/src/ast.rs
index 0590556..1b34fc3 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -2,7 +2,7 @@ use derive_more::Display;
// Set layer
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
pub enum BuiltIn {
Nat,
Int,
@@ -11,68 +11,75 @@ pub enum BuiltIn {
Bool,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
#[display(".{name} : {set}")]
pub struct RecordField {
pub name: String,
pub set: Set,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
#[display("{name}. : {set}")]
pub struct VariantField {
pub name: String,
pub set: Set,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
pub enum Set {
#[display("{_0}")]
BuiltIn(BuiltIn),
+
#[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
Record(Vec<RecordField>),
+
#[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
Variant(Vec<VariantField>),
+
#[display("set({_0})")]
ClaimedSet(Instance),
+
#[display("{_0}")]
Var(String),
}
// Signature layer
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
#[display("({name} : {set})")]
pub struct Param {
pub name: String,
pub set: Set,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
#[display(".{name} :: {signature}")]
pub struct SigField {
pub name: String,
pub signature: Signature,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
pub enum Signature {
#[display("Set")]
Set,
+
#[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
Theory(Vec<SigField>),
+
#[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)]
Ext {
params: Vec<Param>,
codomain: Box<Signature>,
},
+
#[display("{_0}")]
Var(String),
}
// Element layer
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
pub enum Literal {
Nat(u64),
Int(i64),
@@ -81,14 +88,14 @@ pub enum Literal {
Bool(bool),
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
#[display(".{name} = {element}")]
pub struct ElemAssign {
pub name: String,
pub element: Element,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
#[display(".{tag} {bound} => {body}")]
pub struct CaseArm {
pub tag: String,
@@ -96,21 +103,33 @@ pub struct CaseArm {
pub body: Element,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
pub enum Element {
#[display("{_0}")]
Literal(Literal),
+
#[display("{_0}")]
Var(String),
+
#[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
Record(Vec<ElemAssign>),
- #[display("{_0} .{_1}")]
- Project(Box<Element>, String),
- #[display("{_0}. {_1}")]
- Inject(String, Box<Element>),
+
+ #[display("{element} .{field}")]
+ Project {
+ element: Box<Element>,
+ field: String,
+ },
+
+ #[display("{field}. {element}")]
+ Inject {
+ field: String,
+ element: Box<Element>,
+ },
+
#[display("{_0} {_1}")]
App(Box<Element>, Box<Element>),
- #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
+
+ #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
Case {
scrutinee: Box<Element>,
arms: Vec<CaseArm>,
@@ -119,46 +138,57 @@ pub enum Element {
// Instance layer
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
#[display(".{name} = {instance}")]
pub struct InstAssign {
pub name: String,
pub instance: Instance,
}
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
pub enum Instance {
#[display("({_0} :: Set)")]
SetCoerce(Box<Set>),
+
#[display("{_0}")]
Var(String),
+
#[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(", "))]
Record(Vec<InstAssign>),
- #[display("for {}, {body}", params.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(""))]
+
+ #[display("for {}, {body}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(""))]
For {
params: Vec<Param>,
body: Box<Instance>,
},
+
#[display("{_0} {_1}")]
App(Box<Instance>, Box<Element>),
- #[display("{_0} .{_1}")]
- Project(Box<Instance>, String),
+
+ #[display("{instance} .{field}")]
+ Project {
+ instance: Box<Instance>,
+ field: String,
+ },
}
// Declarations
-#[derive(Clone, Debug, PartialEq, Display)]
+#[derive(Clone, PartialEq, Display)]
pub enum Decl {
#[display("let set {name} = {set}")]
Set { name: String, set: Set },
+
#[display("let element {name} : {set} = {element}")]
Element {
name: String,
set: Set,
element: Element,
},
+
#[display("let signature {name} = {signature}")]
Signature { name: String, signature: Signature },
+
#[display("let instance {name} :: {signature} = {instance}")]
Instance {
name: String,
diff --git a/src/checker.rs b/src/checker.rs
index 5f01a7d..d45a5a4 100644
--- a/src/checker.rs
+++ b/src/checker.rs
@@ -2,7 +2,7 @@ use crate::ast::*;
use tracing::{debug, instrument};
use derive_more::Display;
-use std::collections::{HashMap, HashSet};
+use std::collections::HashMap;
use std::fmt;
use std::iter::zip;
@@ -236,12 +236,36 @@ impl CheckState {
Ok(())
}
- #[instrument(skip(self), level = "debug")]
+ #[instrument(skip(self), level = "debug", fields(%set))]
fn check_set(&self, set: &Set) -> Result<Set, CheckError> {
match set {
Set::BuiltIn(_) => Ok(set.clone()),
- Set::Record(fields) => self.check_record(fields),
- Set::Variant(fields) => self.check_variant(fields),
+ Set::Record(fields) => {
+ let fields = fields
+ .iter()
+ .map(|RecordField { name, set }| {
+ let set = self.check_set(set)?;
+ Ok(RecordField {
+ name: name.clone(),
+ set,
+ })
+ })
+ .collect::<Result<Vec<_>, _>>()?;
+ Ok(Set::Record(fields))
+ }
+ Set::Variant(fields) => {
+ let fields = fields
+ .iter()
+ .map(|VariantField { name, set }| {
+ let set = self.check_set(set)?;
+ Ok(VariantField {
+ name: name.clone(),
+ set,
+ })
+ })
+ .collect::<Result<Vec<_>, _>>()?;
+ Ok(Set::Variant(fields))
+ }
Set::ClaimedSet(_) => Err(CheckError::Unimplemented("instances as sets".to_string())),
Set::Var(v) => {
if let Some(deref) = self.wf_sets.get(v) {
@@ -253,36 +277,6 @@ impl CheckState {
}
}
- #[instrument(skip(self), level = "debug")]
- fn check_record(&self, fields: &Vec<RecordField>) -> Result<Set, CheckError> {
- let fields = fields
- .iter()
- .map(|RecordField { name, set }| {
- let set = self.check_set(set)?;
- Ok(RecordField {
- name: name.clone(),
- set,
- })
- })
- .collect::<Result<Vec<_>, _>>()?;
- Ok(Set::Record(fields))
- }
-
- #[instrument(skip(self), level = "debug")]
- fn check_variant(&self, fields: &Vec<VariantField>) -> Result<Set, CheckError> {
- let fields = fields
- .iter()
- .map(|VariantField { name, set }| {
- let set = self.check_set(set)?;
- Ok(VariantField {
- name: name.clone(),
- set,
- })
- })
- .collect::<Result<Vec<_>, _>>()?;
- Ok(Set::Variant(fields))
- }
-
fn _check_literal_set_helper(&self, claimed: &Set, should_be: Set) -> Result<(), CheckError> {
if !self.set_equal(claimed, &should_be) {
Err(CheckError::WrongSetForElement(claimed.clone(), should_be))
@@ -291,7 +285,7 @@ impl CheckState {
}
}
- #[instrument(skip(self), level = "debug")]
+ #[instrument(skip(self), level = "debug", fields(%element, %set))]
fn check_element(&self, element: &Element, set: &Set) -> Result<Element, CheckError> {
match element {
Element::Literal(lit) => {
@@ -383,8 +377,10 @@ impl CheckState {
// resign?
Ok(Element::Record(assignations))
}
- Element::Project(_, _) => Err(CheckError::Unimplemented("element project".to_string())),
- Element::Inject(_, _) => Err(CheckError::Unimplemented("element inject".to_string())),
+ Element::Project { .. } => {
+ Err(CheckError::Unimplemented("element project".to_string()))
+ }
+ Element::Inject { .. } => Err(CheckError::Unimplemented("element inject".to_string())),
Element::App(_, _) => Err(CheckError::Unimplemented("element app".to_string())),
Element::Case { .. } => Err(CheckError::Unimplemented("element case".to_string())),
}
diff --git a/src/parser.rs b/src/parser.rs
index 7fa4241..8b75c2c 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -158,10 +158,10 @@ parser! {
= tags:(t:inject() _ { t })* head:atom_elem() projs:(p:project() { p })*
{
let base = projs.into_iter().fold(head, |acc, p| {
- Element::Project(Box::new(acc), p)
- });
+ Element::Project{element: Box::new(acc), field: p}}
+ );
tags.into_iter().rev().fold(base, |acc, t| {
- Element::Inject(t, Box::new(acc))
+ Element::Inject{field: t, element: Box::new(acc)}
})
}
@@ -196,7 +196,7 @@ parser! {
= head:atom_inst() projs:(p:project() { p })*
{
projs.into_iter().fold(head, |acc, p| {
- Instance::Project(Box::new(acc), p)
+ Instance::Project{instance: Box::new(acc), field: p}
})
}
generated by cgit v1.3.1 (git 2.54.0) at 2026-08-30 21:21:32 +0000