Skip to content

Commit

Permalink
Made naming consistent for Sigma Tuples
Browse files Browse the repository at this point in the history
  • Loading branch information
geffk2 committed May 1, 2024
1 parent 418c65b commit 1197dc1
Show file tree
Hide file tree
Showing 7 changed files with 23 additions and 23 deletions.
8 changes: 4 additions & 4 deletions rzk/grammar/Syntax.cf
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ RecOrDeprecated. Term7 ::= "recOR" "(" Term "," Term "," Term "," Term ")" ;
-- Types
TypeFun. Term1 ::= ParamDecl "" Term1 ;
TypeSigma. Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;
TypeSigmaNested. Term1 ::= "Σ" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
TypeSigmaTuple. Term1 ::= "Σ" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
TypeUnit. Term7 ::= "Unit" ;
TypeId. Term1 ::= Term2 "=_{" Term "}" Term2 ;
TypeIdSimple. Term1 ::= Term2 "=" Term2 ;
Expand Down Expand Up @@ -156,7 +156,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_TypeSigmaTuple. Term1 ::= "Sigma" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
ASCII_Lambda. Term1 ::= "\\" [Param] "->" Term1 ;
ASCII_Restriction. Restriction ::= Term "|->" Term ;
Expand All @@ -169,6 +169,6 @@ ASCII_Second. Term6 ::= "second" Term7 ;
-- Alternative Unicode syntax rules
unicode_TypeSigmaAlt. Term1 ::= "" "(" Pattern ":" Term ")" "," Term1 ; -- \sum
unicode_TypeSigmaNestedAlt. Term1 ::= "" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
unicode_TypeSigmaTupleAlt. Term1 ::= "" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
define unicode_TypeSigmaNestedAlt par pars t = TypeSigmaNested par pars t ;
define unicode_TypeSigmaTupleAlt par pars t = TypeSigmaTuple par pars t ;
8 changes: 4 additions & 4 deletions rzk/src/Language/Rzk/Free/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,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_TypeSigmaTuple loc p ps tN -> go (Rzk.TypeSigmaTuple 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)
Expand Down Expand Up @@ -288,12 +288,12 @@ 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)
Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) ((Rzk.SigmaParam _ patB tB) : ps) tN ->
go (Rzk.TypeSigmaTuple _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.TypeSigmaTuple _loc (Rzk.SigmaParam _ pat tA) [] tB -> go (Rzk.TypeSigma _loc pat tA tB)

Rzk.Lambda _loc [] body -> go body
Rzk.Lambda _loc (Rzk.ParamPattern _ pat : params) body ->
Expand Down
12 changes: 6 additions & 6 deletions rzk/src/Language/Rzk/Syntax/Abs.hs

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

6 changes: 3 additions & 3 deletions rzk/src/Language/Rzk/Syntax/Par.y

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions rzk/src/Language/Rzk/Syntax/Print.hs

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions rzk/src/Language/Rzk/Syntax/Skel.hs

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions rzk/src/Language/Rzk/VSCode/Tokenize.hs
Original file line number Diff line number Diff line change
Expand Up @@ -126,11 +126,11 @@ tokenizeTerm' varTokenType = go
[ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
, tokenizePattern pat
, foldMap go [a, b] ]
TypeSigmaNested loc p ps tN -> concat
TypeSigmaTuple loc p ps tN -> concat
[ mkToken (VarIdent loc "") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
, foldMap tokenizeSigmaParam (p : ps)
, go tN ]
ASCII_TypeSigmaNested loc p ps tN -> concat
ASCII_TypeSigmaTuple loc p ps tN -> concat
[ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]
, foldMap tokenizeSigmaParam (p : ps)
, go tN ]
Expand Down

0 comments on commit 1197dc1

Please sign in to comment.