basic checking sketch

1 files changed, 10 insertions, 180 deletions

diff --git a/src/parser.rs b/src/parser.rs
index a0da79c..f98673e 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -1,176 +1,6 @@
-use derive_more::Display;
 use peg::parser;
 
-// 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 SetField {
-    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<SetField>),
-    #[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}")]
-    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(Vec<Decl>);
+use crate::ast::*;
 
 parser! {
     pub grammar parser() for str {
@@ -272,8 +102,8 @@ parser! {
 
         // set layer
 
-        rule set_field() -> SetField
-        = n:project_lower() _ ":" _ s:set() { SetField { name: n, set: s } }
+        rule set_field() -> RecordField
+        = n:project_lower() _ ":" _ s:set() { RecordField { name: n, set: s } }
 
         rule variant_field() -> VariantField
         = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
@@ -281,7 +111,7 @@ parser! {
         rule claimed_set() -> Instance
         = kw_set() "(" _ i:instance() _ ")" { i }
 
-        pub rule set() -> Set
+        rule set() -> Set
         = kw_record()  _ "{" fs:(set_field() ** ",") _ "}" { Set::Record(fs) }
         / kw_variant() _ "{" _ vs:(variant_field() ** "|") "}" { Set::Variant(vs) }
         / b:builtin() { Set::BuiltIn(b) }
@@ -299,7 +129,7 @@ parser! {
         rule sig_field() -> SigField
         = n:project_upper() _ "::" _ s:signature() { SigField { name: n, signature: s } }
 
-        pub rule signature() -> Signature
+        rule signature() -> Signature
         = kw_Set()    { Signature::Set }
         / kw_theory() _ "{" fs:(sig_field() ** ",") _ "}" { Signature::Theory(fs) }
         / ps:param_list() _ "->" _ cod:signature() { Signature::Ext { params: ps, codomain: Box::new(cod) } }
@@ -339,7 +169,7 @@ parser! {
         rule case_arm() -> CaseArm
         = t:inject() _ x:elem_var() _ "=>" _ body:element() { CaseArm { tag: t, bound: x, body } }
 
-        pub rule element() -> Element
+        rule element() -> Element
         = kw_case() __ scrut:element() _ kw_of() _ "{" arms:(_ a:case_arm() _ { a }) ** "|"  _ "}" { Element::Case { scrutinee: Box::new(scrut), arms } }
         / app_elem()
 
@@ -371,7 +201,7 @@ parser! {
             })
         }
 
-        pub rule instance() -> Instance
+        rule instance() -> Instance
         = kw_for() __ ps:param_list() _ "," _ body:instance() { Instance::For { params: ps, body: Box::new(body) } }
         / app_inst()
 
@@ -451,12 +281,12 @@ let set Maybe = variant {
                 .Edge :: (s : Node) (t : Node) -> Set
             }
 
-            let instance loop :: Graph = {
+            let instance natPoset :: Graph = {
                 .Node = Nat,
-                .Edge = for (s : Nat) (t : Nat), Nat
+                .Edge = for (s : Nat) (t : Nat), Bool
             }
 
-            let element node : set(loop .Node) = 7
+            let element node : set(natPoset .Node) = 7
         "#;
 
         debug_parse(src);