Implemented syntactic sugar for nested sigma types

rzk-lang · Apr 19, 2024 · f378bca · f378bca
1 parent 82d3b3f
commit f378bca
Show file tree

Hide file tree

Showing 7 changed files with 62 additions and 0 deletions.
diff --git a/rzk/grammar/Syntax.cf b/rzk/grammar/Syntax.cf
@@ -78,6 +78,10 @@ ParamVarShapeDeprecated. ParamDecl ::= "{" "(" Pattern ":" Term ")" "|" Term "}"
 paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ;
 define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ;
 
+-- Parameter declaration for Sigma types 
+SigmaParam. SigmaParam ::= Pattern ":" Term ;
+separator nonempty SigmaParam "," ;
+
 Restriction. Restriction ::= Term "↦" Term ;
 separator nonempty Restriction "," ;
 
@@ -106,6 +110,7 @@ RecOrDeprecated.  Term7 ::= "recOR" "(" Term "," Term "," Term "," Term ")" ;
 -- Types
 TypeFun.        Term1 ::= ParamDecl "→" Term1 ;
 TypeSigma.      Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;
+TypeSigmaNested. Term1 ::= "Σ" "(" [SigmaParam] ")" "," Term1 ;
 TypeUnit.       Term7 ::= "Unit" ;
 TypeId.         Term1 ::= Term2 "=_{" Term "}" Term2 ;
 TypeIdSimple.   Term1 ::= Term2 "=" Term2 ;

diff --git a/rzk/src/Language/Rzk/Free/Syntax.hs b/rzk/src/Language/Rzk/Free/Syntax.hs
@@ -280,6 +280,14 @@ toTerm bvars = go
       Rzk.TypeSigma _loc pat tA tB ->
         TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB)
 
+      Rzk.TypeSigmaNested _loc ((Rzk.SigmaParam _ patA tA) : (Rzk.SigmaParam _ patB tB) : ps) tN -> 
+        go (Rzk.TypeSigmaNested _loc ((Rzk.SigmaParam _loc patX tX) : ps) tN)
+        where
+          patX = Rzk.PatternPair _loc patA patB
+          tX = Rzk.TypeSigma _loc patA tA tB
+      Rzk.TypeSigmaNested _loc [Rzk.SigmaParam _ pat tA] tB -> go (Rzk.TypeSigma _loc pat tA tB)
+      Rzk.TypeSigmaNested _loc [] tN -> (go tN)
+
       Rzk.Lambda _loc [] body -> go body
       Rzk.Lambda _loc (Rzk.ParamPattern _ pat : params) body ->
         Lambda (patternVar pat) Nothing (toScopePattern pat bvars (Rzk.Lambda _loc params body))

diff --git a/rzk/src/Language/Rzk/Syntax/Abs.hs b/rzk/src/Language/Rzk/Syntax/Abs.hs
diff --git a/rzk/src/Language/Rzk/Syntax/Doc.txt b/rzk/src/Language/Rzk/Syntax/Doc.txt
diff --git a/rzk/src/Language/Rzk/Syntax/Par.y b/rzk/src/Language/Rzk/Syntax/Par.y
diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs
diff --git a/rzk/src/Language/Rzk/Syntax/Skel.hs b/rzk/src/Language/Rzk/Syntax/Skel.hs