From f378bcaaa0f07fa5689b7acd72de89b12551433e Mon Sep 17 00:00:00 2001
From: geffk2 <sluxx@icloud.com>
Date: Fri, 19 Apr 2024 16:12:53 +0300
Subject: [PATCH] Implemented syntactic sugar for nested sigma types

---
 rzk/grammar/Syntax.cf                |  5 +++++
 rzk/src/Language/Rzk/Free/Syntax.hs  |  8 ++++++++
 rzk/src/Language/Rzk/Syntax/Abs.hs   | 10 ++++++++++
 rzk/src/Language/Rzk/Syntax/Doc.txt  |  4 ++++
 rzk/src/Language/Rzk/Syntax/Par.y    | 20 ++++++++++++++++++++
 rzk/src/Language/Rzk/Syntax/Print.hs | 10 ++++++++++
 rzk/src/Language/Rzk/Syntax/Skel.hs  |  5 +++++
 7 files changed, 62 insertions(+)

diff --git a/rzk/grammar/Syntax.cf b/rzk/grammar/Syntax.cf
index 2c3ce32f6..cfabd6fed 100644
--- 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
index 786b17b6b..2a13f360a 100644
--- 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
index ad4c07fbe..a88cb75ee 100644
--- a/rzk/src/Language/Rzk/Syntax/Abs.hs
+++ b/rzk/src/Language/Rzk/Syntax/Abs.hs
@@ -91,6 +91,10 @@ data ParamDecl' a
     | ParamVarShapeDeprecated a (Pattern' a) (Term' a) (Term' a)
   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
 
+type SigmaParam = SigmaParam' BNFC'Position
+data SigmaParam' a = SigmaParam a (Pattern' a) (Term' a)
+  deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)
+
 type Restriction = Restriction' BNFC'Position
 data Restriction' a
     = Restriction a (Term' a) (Term' a)
@@ -119,6 +123,7 @@ data Term' a
     | RecOrDeprecated a (Term' a) (Term' a) (Term' a) (Term' a)
     | TypeFun a (ParamDecl' a) (Term' a)
     | TypeSigma a (Pattern' a) (Term' a) (Term' a)
+    | TypeSigmaNested a [SigmaParam' a] (Term' a)
     | TypeUnit a
     | TypeId a (Term' a) (Term' a) (Term' a)
     | TypeIdSimple a (Term' a) (Term' a)
@@ -269,6 +274,10 @@ instance HasPosition ParamDecl where
     ParamTermTypeDeprecated p _ _ -> p
     ParamVarShapeDeprecated p _ _ _ -> p
 
+instance HasPosition SigmaParam where
+  hasPosition = \case
+    SigmaParam p _ _ -> p
+
 instance HasPosition Restriction where
   hasPosition = \case
     Restriction p _ _ -> p
@@ -296,6 +305,7 @@ instance HasPosition Term where
     RecOrDeprecated p _ _ _ _ -> p
     TypeFun p _ _ -> p
     TypeSigma p _ _ _ -> p
+    TypeSigmaNested p _ _ -> p
     TypeUnit p -> p
     TypeId p _ _ _ -> p
     TypeIdSimple p _ _ -> p
diff --git a/rzk/src/Language/Rzk/Syntax/Doc.txt b/rzk/src/Language/Rzk/Syntax/Doc.txt
index ea571c2c7..965865777 100644
--- a/rzk/src/Language/Rzk/Syntax/Doc.txt
+++ b/rzk/src/Language/Rzk/Syntax/Doc.txt
@@ -111,6 +111,9 @@ All other symbols are terminals.
   |  |  **|**  | ``{`` //Pattern// ``:`` //Term// ``}``
   |  |  **|**  | ``{`` ``(`` //Pattern// ``:`` //Term// ``)`` ``|`` //Term// ``}``
   |  |  **|**  | ``{`` //Pattern// ``:`` //Term// ``|`` //Term// ``}``
+  | //SigmaParam// | -> | //Pattern// ``:`` //Term//
+  | //[SigmaParam]// | -> | //SigmaParam//
+  |  |  **|**  | //SigmaParam// ``,`` //[SigmaParam]//
   | //Restriction// | -> | //Term// ``↦`` //Term//
   |  |  **|**  | //Term// ``|->`` //Term//
   | //[Restriction]// | -> | //Restriction//
@@ -161,6 +164,7 @@ All other symbols are terminals.
   |  |  **|**  | //Term3// ``\/`` //Term2//
   | //Term1// | -> | //ParamDecl// ``→`` //Term1//
   |  |  **|**  | ``Σ`` ``(`` //Pattern// ``:`` //Term// ``)`` ``,`` //Term1//
+  |  |  **|**  | ``Σ`` ``(`` //[SigmaParam]// ``)`` ``,`` //Term1//
   |  |  **|**  | //Term2// ``=_{`` //Term// ``}`` //Term2//
   |  |  **|**  | //Term2// ``=`` //Term2//
   |  |  **|**  | ``\`` //[Param]// ``→`` //Term1//
diff --git a/rzk/src/Language/Rzk/Syntax/Par.y b/rzk/src/Language/Rzk/Syntax/Par.y
index f2967f020..51bc42bbb 100644
--- a/rzk/src/Language/Rzk/Syntax/Par.y
+++ b/rzk/src/Language/Rzk/Syntax/Par.y
@@ -23,6 +23,8 @@ module Language.Rzk.Syntax.Par
   , pParam
   , pListParam
   , pParamDecl
+  , pSigmaParam
+  , pListSigmaParam
   , pRestriction
   , pListRestriction
   , pTerm7
@@ -58,6 +60,8 @@ import Language.Rzk.Syntax.Lex
 %name pParam_internal Param
 %name pListParam_internal ListParam
 %name pParamDecl_internal ParamDecl
+%name pSigmaParam_internal SigmaParam
+%name pListSigmaParam_internal ListSigmaParam
 %name pRestriction_internal Restriction
 %name pListRestriction_internal ListRestriction
 %name pTerm7_internal Term7
@@ -257,6 +261,15 @@ ParamDecl
   | '{' '(' Pattern ':' Term ')' '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
   | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.paramVarShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }
 
+SigmaParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.SigmaParam) }
+SigmaParam
+  : Pattern ':' Term { (fst $1, Language.Rzk.Syntax.Abs.SigmaParam (fst $1) (snd $1) (snd $3)) }
+
+ListSigmaParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.SigmaParam]) }
+ListSigmaParam
+  : SigmaParam { (fst $1, (:[]) (snd $1)) }
+  | SigmaParam ',' ListSigmaParam { (fst $1, (:) (snd $1) (snd $3)) }
+
 Restriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Restriction) }
 Restriction
   : Term '↦' Term { (fst $1, Language.Rzk.Syntax.Abs.Restriction (fst $1) (snd $1) (snd $3)) }
@@ -330,6 +343,7 @@ Term1 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term)
 Term1
   : ParamDecl '→' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeFun (fst $1) (snd $1) (snd $3)) }
   | 'Σ' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }
+  | 'Σ' '(' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigmaNested (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $6)) }
   | Term2 '=_{' Term '}' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeId (fst $1) (snd $1) (snd $3) (snd $5)) }
   | Term2 '=' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TypeIdSimple (fst $1) (snd $1) (snd $3)) }
   | '\\' ListParam '→' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }
@@ -421,6 +435,12 @@ pListParam = fmap snd . pListParam_internal
 pParamDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.ParamDecl
 pParamDecl = fmap snd . pParamDecl_internal
 
+pSigmaParam :: [Token] -> Err Language.Rzk.Syntax.Abs.SigmaParam
+pSigmaParam = fmap snd . pSigmaParam_internal
+
+pListSigmaParam :: [Token] -> Err [Language.Rzk.Syntax.Abs.SigmaParam]
+pListSigmaParam = fmap snd . pListSigmaParam_internal
+
 pRestriction :: [Token] -> Err Language.Rzk.Syntax.Abs.Restriction
 pRestriction = fmap snd . pRestriction_internal
 
diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs
index c31b45a6e..b51d6a178 100644
--- a/rzk/src/Language/Rzk/Syntax/Print.hs
+++ b/rzk/src/Language/Rzk/Syntax/Print.hs
@@ -224,6 +224,15 @@ instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where
     Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated _ pattern_ term -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term, doc (showString "}")])
     Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString "|"), prt 0 term2, doc (showString "}")])
 
+instance Print (Language.Rzk.Syntax.Abs.SigmaParam' a) where
+  prt i = \case
+    Language.Rzk.Syntax.Abs.SigmaParam _ pattern_ term -> prPrec i 0 (concatD [prt 0 pattern_, doc (showString ":"), prt 0 term])
+
+instance Print [Language.Rzk.Syntax.Abs.SigmaParam' a] where
+  prt _ [] = concatD []
+  prt _ [x] = concatD [prt 0 x]
+  prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs]
+
 instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where
   prt i = \case
     Language.Rzk.Syntax.Abs.Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "\8614"), prt 0 term2])
@@ -256,6 +265,7 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where
     Language.Rzk.Syntax.Abs.RecOrDeprecated _ term1 term2 term3 term4 -> prPrec i 7 (concatD [doc (showString "recOR"), doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ","), prt 0 term3, doc (showString ","), prt 0 term4, doc (showString ")")])
     Language.Rzk.Syntax.Abs.TypeFun _ paramdecl term -> prPrec i 1 (concatD [prt 0 paramdecl, doc (showString "\8594"), prt 1 term])
     Language.Rzk.Syntax.Abs.TypeSigma _ pattern_ term1 term2 -> prPrec i 1 (concatD [doc (showString "\931"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString ","), prt 1 term2])
+    Language.Rzk.Syntax.Abs.TypeSigmaNested _ sigmaparams term -> prPrec i 1 (concatD [doc (showString "\931"), doc (showString "("), prt 0 sigmaparams, doc (showString ")"), doc (showString ","), prt 1 term])
     Language.Rzk.Syntax.Abs.TypeUnit _ -> prPrec i 7 (concatD [doc (showString "Unit")])
     Language.Rzk.Syntax.Abs.TypeId _ term1 term2 term3 -> prPrec i 1 (concatD [prt 2 term1, doc (showString "=_{"), prt 0 term2, doc (showString "}"), prt 2 term3])
     Language.Rzk.Syntax.Abs.TypeIdSimple _ term1 term2 -> prPrec i 1 (concatD [prt 2 term1, doc (showString "="), prt 2 term2])
diff --git a/rzk/src/Language/Rzk/Syntax/Skel.hs b/rzk/src/Language/Rzk/Syntax/Skel.hs
index f563fd074..71ccee72a 100644
--- a/rzk/src/Language/Rzk/Syntax/Skel.hs
+++ b/rzk/src/Language/Rzk/Syntax/Skel.hs
@@ -87,6 +87,10 @@ transParamDecl x = case x of
   Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated _ pattern_ term -> failure x
   Language.Rzk.Syntax.Abs.ParamVarShapeDeprecated _ pattern_ term1 term2 -> failure x
 
+transSigmaParam :: Show a => Language.Rzk.Syntax.Abs.SigmaParam' a -> Result
+transSigmaParam x = case x of
+  Language.Rzk.Syntax.Abs.SigmaParam _ pattern_ term -> failure x
+
 transRestriction :: Show a => Language.Rzk.Syntax.Abs.Restriction' a -> Result
 transRestriction x = case x of
   Language.Rzk.Syntax.Abs.Restriction _ term1 term2 -> failure x
@@ -114,6 +118,7 @@ transTerm x = case x of
   Language.Rzk.Syntax.Abs.RecOrDeprecated _ term1 term2 term3 term4 -> failure x
   Language.Rzk.Syntax.Abs.TypeFun _ paramdecl term -> failure x
   Language.Rzk.Syntax.Abs.TypeSigma _ pattern_ term1 term2 -> failure x
+  Language.Rzk.Syntax.Abs.TypeSigmaNested _ sigmaparams term -> failure x
   Language.Rzk.Syntax.Abs.TypeUnit _ -> failure x
   Language.Rzk.Syntax.Abs.TypeId _ term1 term2 term3 -> failure x
   Language.Rzk.Syntax.Abs.TypeIdSimple _ term1 term2 -> failure x