From 0886a16d73145270e953b8c2e0a4452b518ea16e Mon Sep 17 00:00:00 2001 From: tslil Date: Fri, 1 May 2026 12:36:24 +0100 Subject: working on fixing app, rework ast to have generics etc --- src/main.rs | 63 ++++++++++++++++++++++++++++++++++--------------------------- 1 file changed, 35 insertions(+), 28 deletions(-) (limited to 'src/main.rs') diff --git a/src/main.rs b/src/main.rs index 834792e..1925b41 100644 --- a/src/main.rs +++ b/src/main.rs @@ -18,35 +18,42 @@ fn main() { .init(); let src = r#" -let signature Graph = theory { - Node :: Set, - Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set +// let signature Graph = theory { +// Vertex :: Set, +// Edge :: (s : set-of(Vertex)) (t : set-of(Vertex)) -> Set +// } + +// 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 oneSimplex :: Graph = { +// .Vertex = F3 :: Set, +// .Edge = for (s : set-of(Vertex)) (t : set-of(Vertex)), +// 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 OneSimplexEdges = record { +// source: set-of(oneSimplex .Vertex), +// target: set-of(oneSimplex .Vertex), +// connected: set-of(oneSimplex .Edge source target) +// } + +// let element vertex0 : F3 = three0. {} +// let element vertex1 : F3 = three1. {} +// let element edge01 : set-of(oneSimplex .Edge vertex0 vertex1) = pt + +let signature S = theory { + F :: (x : Nat) (y : Bool) -> Set, + G :: (z : set-of(F 3 5)) -> Set } - -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 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 OneSimplexEdges = record { - source: set-of(oneSimplex .Node), - target: set-of(oneSimplex .Node), - connected: set-of(oneSimplex .Edge source target) -} - -let element edge : set-of(oneSimplex .Edge (three0. pt) (three1. pt)) = pt "#; let programme = parser::parse(src); -- cgit v1.3.1