1 files changed, 172 insertions, 0 deletions
diff --git a/src/ast.rs b/src/ast.rs
new file mode 100644
index 0000000..0590556
--- /dev/null
+++ b/src/ast.rs
@@ -0,0 +1,172 @@
+use derive_more::Display;
+
+// Set layer
+
+#[derive(Clone, Debug, PartialEq, Display)]
+pub enum BuiltIn {
+    Nat,
+    Int,
+    Float,
+    Str,
+    Bool,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} : {set}")]
+pub struct RecordField {
+    pub name: String,
+    pub set: Set,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display("{name}. : {set}")]
+pub struct VariantField {
+    pub name: String,
+    pub set: Set,
+}
+
+#[derive(Clone, Debug, 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)]
+#[display("({name} : {set})")]
+pub struct Param {
+    pub name: String,
+    pub set: Set,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} :: {signature}")]
+pub struct SigField {
+    pub name: String,
+    pub signature: Signature,
+}
+
+#[derive(Clone, Debug, 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)]
+pub enum Literal {
+    Nat(u64),
+    Int(i64),
+    Float(f64),
+    Str(String),
+    Bool(bool),
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} = {element}")]
+pub struct ElemAssign {
+    pub name: String,
+    pub element: Element,
+}
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{tag} {bound} => {body}")]
+pub struct CaseArm {
+    pub tag: String,
+    pub bound: String,
+    pub body: Element,
+}
+
+#[derive(Clone, Debug, 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("{_0} {_1}")]
+    App(Box<Element>, Box<Element>),
+    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
+    Case {
+        scrutinee: Box<Element>,
+        arms: Vec<CaseArm>,
+    },
+}
+
+// Instance layer
+
+#[derive(Clone, Debug, PartialEq, Display)]
+#[display(".{name} = {instance}")]
+pub struct InstAssign {
+    pub name: String,
+    pub instance: Instance,
+}
+
+#[derive(Clone, Debug, 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(""))]
+    For {
+        params: Vec<Param>,
+        body: Box<Instance>,
+    },
+    #[display("{_0} {_1}")]
+    App(Box<Instance>, Box<Element>),
+    #[display("{_0} .{_1}")]
+    Project(Box<Instance>, String),
+}
+
+// Declarations
+
+#[derive(Clone, Debug, 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,
+        signature: Signature,
+        instance: Instance,
+    },
+}
+
+#[derive(Display)]
+#[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))]
+pub struct Programme(pub Vec<Decl>);