From 1fe743de25d65711a3b5754ad04f99c50534efaf Mon Sep 17 00:00:00 2001 From: geffk2 Date: Fri, 19 Apr 2024 17:42:23 +0300 Subject: [PATCH] Corrected overlapping rule --- rzk/grammar/Syntax.cf | 2 +- rzk/src/Language/Rzk/Free/Syntax.hs | 7 +++---- rzk/src/Language/Rzk/Syntax/Abs.hs | 4 ++-- rzk/src/Language/Rzk/Syntax/Doc.txt | 2 +- rzk/src/Language/Rzk/Syntax/Par.y | 2 +- rzk/src/Language/Rzk/Syntax/Print.hs | 2 +- rzk/src/Language/Rzk/Syntax/Skel.hs | 2 +- 7 files changed, 10 insertions(+), 11 deletions(-) diff --git a/rzk/grammar/Syntax.cf b/rzk/grammar/Syntax.cf index cfabd6fed..0437d0326 100644 --- a/rzk/grammar/Syntax.cf +++ b/rzk/grammar/Syntax.cf @@ -110,7 +110,7 @@ RecOrDeprecated. Term7 ::= "recOR" "(" Term "," Term "," Term "," Term ")" ; -- Types TypeFun. Term1 ::= ParamDecl "→" Term1 ; TypeSigma. Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ; -TypeSigmaNested. Term1 ::= "Σ" "(" [SigmaParam] ")" "," Term1 ; +TypeSigmaNested. Term1 ::= "Σ" "(" SigmaParam "," [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 2a13f360a..48704f875 100644 --- a/rzk/src/Language/Rzk/Free/Syntax.hs +++ b/rzk/src/Language/Rzk/Free/Syntax.hs @@ -280,13 +280,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.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.TypeSigmaNested _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 -> diff --git a/rzk/src/Language/Rzk/Syntax/Abs.hs b/rzk/src/Language/Rzk/Syntax/Abs.hs index a88cb75ee..3e9db727c 100644 --- a/rzk/src/Language/Rzk/Syntax/Abs.hs +++ b/rzk/src/Language/Rzk/Syntax/Abs.hs @@ -123,7 +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) + | TypeSigmaNested a (SigmaParam' a) [SigmaParam' a] (Term' a) | TypeUnit a | TypeId a (Term' a) (Term' a) (Term' a) | TypeIdSimple a (Term' a) (Term' a) @@ -305,7 +305,7 @@ instance HasPosition Term where RecOrDeprecated p _ _ _ _ -> p TypeFun p _ _ -> p TypeSigma p _ _ _ -> p - TypeSigmaNested 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 965865777..1113056c8 100644 --- a/rzk/src/Language/Rzk/Syntax/Doc.txt +++ b/rzk/src/Language/Rzk/Syntax/Doc.txt @@ -164,7 +164,7 @@ All other symbols are terminals. | | **|** | //Term3// ``\/`` //Term2// | //Term1// | -> | //ParamDecl// ``→`` //Term1// | | **|** | ``Σ`` ``(`` //Pattern// ``:`` //Term// ``)`` ``,`` //Term1// - | | **|** | ``Σ`` ``(`` //[SigmaParam]// ``)`` ``,`` //Term1// + | | **|** | ``Σ`` ``(`` //SigmaParam// ``,`` //[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 51bc42bbb..3c2216e50 100644 --- a/rzk/src/Language/Rzk/Syntax/Par.y +++ b/rzk/src/Language/Rzk/Syntax/Par.y @@ -343,7 +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)) } + | 'Σ' '(' SigmaParam ',' 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 $5) (snd $8)) } | 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)) } diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs index b51d6a178..140bcb4d4 100644 --- a/rzk/src/Language/Rzk/Syntax/Print.hs +++ b/rzk/src/Language/Rzk/Syntax/Print.hs @@ -265,7 +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.TypeSigmaNested _ sigmaparam sigmaparams term -> prPrec i 1 (concatD [doc (showString "\931"), doc (showString "("), prt 0 sigmaparam, 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 71ccee72a..b7145b532 100644 --- a/rzk/src/Language/Rzk/Syntax/Skel.hs +++ b/rzk/src/Language/Rzk/Syntax/Skel.hs @@ -118,7 +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.TypeSigmaNested _ sigmaparam 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