diff options
Diffstat (limited to 'src/main.rs')
| -rw-r--r-- | src/main.rs | 31 |
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); |