make parser more lenient, add the one simplex example, fix naming for records

1 files changed, 20 insertions, 11 deletions

diff --git a/src/main.rs b/src/main.rs
index eb16b32..834792e 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -23,23 +23,32 @@ let signature Graph = theory {
     Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
 }
 
-let set FinTwo = variant [ zero : record{} | one : record{} ]
+let set Empty = variant[]
+let set Unit = record{}
+let element pt : Unit = {}
+let set F1 = variant [ one0 : Unit ]
+let set F2 = variant [ two0 : Unit | two1 : Unit ]
+let set F3 = variant [ three0 : Unit | three1 : Unit  | three2: Unit ]
 
-let instance natGraph :: Graph = {
-    .Node = FinTwo :: Set,
-    .Edge = for (s : set-of(Node)) (t : set-of(Node)), case s of [ zero. ignore => Bool :: Set | one. ignore => Nat :: Set ]
+let instance oneSimplex :: Graph = {
+    .Node = F3 :: Set,
+    .Edge = for (s : set-of(Node)) (t : set-of(Node)),
+              case s of [
+                three0. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Unit :: Set | three2. pt => Unit :: Set ]
+                | three1. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Unit :: Set ]
+                | three2. pt => case t of [ three0. pt => Empty :: Set | three1. pt => Empty :: Set | three2. pt => Empty :: Set ]
+              ]
 }
 
-let set NatEdges = record {
-  source: set-of(natGraph .Node),
-  target: set-of(natGraph .Node),
-  connected: set-of(natGraph .Edge source target)
+let set OneSimplexEdges = record {
+  source: set-of(oneSimplex .Node),
+  target: set-of(oneSimplex .Node),
+  connected: set-of(oneSimplex .Edge source target)
 }
 
-let element s_val : FinTwo = zero. {}
-let element edge : set-of(natGraph .Edge s_val ( one. {} )) = true
+let element edge : set-of(oneSimplex .Edge (three0. pt) (three1. pt)) = pt
 "#;
-    let programme = parser::debug_parse(src);
+    let programme = parser::parse(src);
 
     if let Err(e) = programme.check() {
         println!("{}", e);