Added ASCII and Unicode rules

rzk-lang · Apr 19, 2024 · fbaf19c · fbaf19c
1 parent 1fe743d
commit fbaf19c
Show file tree

Hide file tree

Showing 7 changed files with 15 additions and 0 deletions.
diff --git a/rzk/grammar/Syntax.cf b/rzk/grammar/Syntax.cf
@@ -154,6 +154,7 @@ ASCII_TopeOr.         Term2 ::= Term3 "\\/" Term2 ;
 
 ASCII_TypeFun.        Term1 ::= ParamDecl "->" Term1 ;
 ASCII_TypeSigma.      Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;
+ASCII_TypeSigmaNested. Term1 ::= "Sigma" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 
 ASCII_Lambda.         Term1 ::= "\\" [Param] "->" Term1 ;
 ASCII_Restriction. Restriction ::= Term "|->" Term ;
@@ -166,4 +167,6 @@ ASCII_Second.         Term6 ::= "second" Term7 ;
 -- Alternative Unicode syntax rules
 
 unicode_TypeSigmaAlt.   Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ;    -- \sum
+unicode_TypeSigmaNestedAlt. Term1 ::= "∑" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
 define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
+define unicode_TypeSigmaNestedAlt par pars t = TypeSigmaNested par pars t ;
diff --git a/rzk/src/Language/Rzk/Free/Syntax.hs b/rzk/src/Language/Rzk/Free/Syntax.hs
@@ -223,6 +223,7 @@ toTerm bvars = go
 
       Rzk.ASCII_TypeFun loc param ret -> go (Rzk.TypeFun loc param ret)
       Rzk.ASCII_TypeSigma loc pat ty ret -> go (Rzk.TypeSigma loc pat ty ret)
+      Rzk.ASCII_TypeSigmaNested loc p ps tN -> go (Rzk.TypeSigmaNested loc p ps tN)
       Rzk.ASCII_Lambda loc pat ret -> go (Rzk.Lambda loc pat ret)
       Rzk.ASCII_TypeExtensionDeprecated loc shape type_ -> go (Rzk.TypeExtensionDeprecated loc shape type_)
       Rzk.ASCII_First loc term -> go (Rzk.First loc term)

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