From 31de6d4406fa5663ecdbc1341521a61b86b13783 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 27 Apr 2026 18:07:06 +0100
Subject: flip to agda-like grammar, sets & signatures do not have dots in
 their fields, but applications of those do as do constructions

---
 src/main.rs   | 34 +++++++++++++++++-----------------
 src/parser.rs | 32 +++++++++++++++++++-------------
 2 files changed, 36 insertions(+), 30 deletions(-)

(limited to 'src')

diff --git a/src/main.rs b/src/main.rs
index 7d04891..491f6d6 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -20,34 +20,34 @@ fn main() {
     let src = r#"
 
 // let X be the set Y, call it Z
-let set X = record { .b : Bool, .n : Nat }
+let set X = record { b : Bool, n : Nat }
 let set Y = X
-let set Z = record { .y : Y }
+let set Z = record { y : Y }
 // make some elements
 let element x : X = { .b = true, .n = 41 }
 let element z : Z = { .y = x }
 // exercise case matching
-let set Z_or_Float = variant [ z. : Z | f. : Float ]
+let set Z_or_Float = variant [ z : Z | f : Float ]
 let element injected : Z_or_Float = z. z
 let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]
 
 let signature Graph = theory {
-    .Node :: Set,
-    .Edge :: (s : Node) (t : Node) -> Set
+    Node :: Set,
+    Edge :: (s : Node) (t : Node) -> Set
 }
 
-// let instance natPoset :: Graph = {
-//     .Node = Nat,
-//     .Edge = for (s : Nat) (t : Nat), Bool
-// }
-//
-// let element node : set-of(natPoset .Node) = 7
-//
-// let set NatEdges = record {
-//   .source: set-of(natPoset .Node),
-//   .target: set-of(natPoset .Node),
-//   .connected set-of(natPoset .Edge source target)
-// }
+let instance natPoset :: Graph = {
+    .Node = Nat,
+    .Edge = for (s : Nat) (t : Nat), Bool
+}
+
+let element node : set-of(natPoset .Node) = 7
+
+let set NatEdges = record {
+  source: set-of(natPoset .Node),
+  target: set-of(natPoset .Node),
+  connected: set-of(natPoset .Edge source target)
+}
 "#;
     let programme = parser::parser::program(src);
 
diff --git a/src/parser.rs b/src/parser.rs
index 4599f7e..6810927 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -111,10 +111,10 @@ parser! {
         // set layer
 
         rule set_field() -> RecordField
-        = n:project_lower() _ ":" _ s:set() { RecordField { name: n, set: s } }
+        = _ n:lower_ident() _ ":" _ s:set() { RecordField { name: n, set: s } }
 
         rule variant_field() -> VariantField
-        = n:inject_lower() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
+        = _ n:lower_ident() _ ":" _ s:set() _ { VariantField { name: n, set: s } }
 
         rule claimed_set() -> Instance
         = kw_set_of() "(" _ i:instance() _ ")" { i }
@@ -135,7 +135,7 @@ parser! {
         rule param_list() -> Vec<Param> = param() ++ _
 
         rule sig_field() -> SigField
-        = n:project_upper() _ "::" _ s:signature() { SigField { name: n, signature: s } }
+        = _ n:upper_ident() _ "::" _ s:signature() { SigField { name: n, signature: s } }
 
         rule signature() -> Signature
         = kw_Set()    { Signature::Set }
@@ -176,7 +176,7 @@ parser! {
         // instance layer
 
         rule inst_assign() -> InstAssign
-        = n:project() _ "=" _ i:instance()
+        = n:project_upper() _ "=" _ i:instance()
         { InstAssign { name: n, instance: i } }
 
         rule atom_inst() -> Instance
@@ -244,16 +244,16 @@ mod tests {
     fn test_sets() {
         let src = r#"
 let set Config = record {
-    .enabled : Bool,
-    .count   : Nat,
-    .offset  : Int,
-    .scale   : Float,
-    .label   : Str
+    enabled : Bool,
+    count   : Nat,
+    offset  : Int,
+    scale   : Float,
+    label   : Str
 }
 
 let set Maybe = variant [
-    none. : record {}
-  | some. : Config
+    none : record {}
+  | some : Config
 ]
         "#;
 
@@ -277,8 +277,8 @@ let set Maybe = variant [
     fn test_theories_and_instances() {
         let src = r#"
             let signature Graph = theory {
-                .Node :: Set,
-                .Edge :: (s : Node) (t : Node) -> Set
+                Node :: Set,
+                Edge :: (s : Node) (t : Node) -> Set
             }
 
             let instance natPoset :: Graph = {
@@ -287,6 +287,12 @@ let set Maybe = variant [
             }
 
             let element node : set-of(natPoset .Node) = 7
+
+            let set NatEdges = record {
+              source: set-of(natPoset .Node),
+              target: set-of(natPoset .Node),
+              connected: set-of(natPoset .Edge source target)
+            }
         "#;
 
         debug_parse(src);
-- 
cgit v1.3.1