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/parser.rs | 32 +++++++++++++++++++-------------
 1 file changed, 19 insertions(+), 13 deletions(-)

(limited to 'src/parser.rs')

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