rzk 0.5.3 → 0.5.4
raw patch · 5 files changed
+774/−11 lines, 5 files
Files
- ChangeLog.md +7/−0
- rzk.cabal +2/−2
- src/Language/Rzk/Syntax/Lex.x +292/−0
- src/Language/Rzk/Syntax/Par.y +456/−0
- src/Rzk/TypeCheck.hs +17/−9
ChangeLog.md view
@@ -6,6 +6,13 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.5.4 — 2022-08-19++This version contains minor improvements:++1. Improve typechecking by trying an easier unification strategy first (see [#76](https://github.com/rzk-lang/rzk/pull/76));+2. Update GitHub Action for Nix (see [#74](https://github.com/rzk-lang/rzk/pull/74)).+ ## v0.5.3 — 2022-07-12 This version contains a few minor improvements:
rzk.cabal view
@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.35.1. -- -- see: https://github.com/sol/hpack name: rzk-version: 0.5.3+version: 0.5.4 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at <https://github.com/rzk-lang/rzk#readme> category: Dependent Types
+ src/Language/Rzk/Syntax/Lex.x view
@@ -0,0 +1,292 @@+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).++-- Lexer definition for use with Alex 3+{+{-# OPTIONS -fno-warn-incomplete-patterns #-}+{-# OPTIONS_GHC -w #-}++{-# LANGUAGE PatternSynonyms #-}++module Language.Rzk.Syntax.Lex where++import Prelude++import qualified Data.Bits+import Data.Char (ord)+import Data.Function (on)+import Data.Word (Word8)+}++-- Predefined character classes++$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter (215 = \times) FIXME+$s = [a-z\222-\255] # [\247] -- small isolatin1 letter (247 = \div ) FIXME+$l = [$c $s] -- letter+$d = [0-9] -- digit+$i = [$l $d _ '] -- identifier character+$u = [. \n] -- universal: any character++-- Symbols and non-identifier-like reserved words++@rsyms = \Σ | \π \₁ | \π \₂ | \# "lang" | \; | "rzk" \- "1" | \# "set" \- "option" | \= | \# "unset" \- "option" | \# "check" | \: | \# "compute" | \# "compute" \- "whnf" | \# "compute" \- "nf" | \# "postulate" | \# "assume" | \# "variable" | \# "variables" | \# "section" | \# "end" | \# "define" | \: \= | \# "def" | \( | \) | \, | \| | \{ | \} | \↦ | "1" | \* \₁ | "2" | "0" \₂ | "1" \₂ | \× | \⊤ | \⊥ | \≡ | \≤ | \∧ | \∨ | \→ | \= \_ \{ | \[ | \] | \< | \> | \\ | "refl" \_ \{ | \* | \* \_ "1" | "0" \_ "2" | "1" \_ "2" | \= \= \= | \< \= | \/ \\ | \\ \/ | \- \> | \| \- \> | \∑++:-++-- Line comment "--"+"--" [.]* ;++-- Block comment "{-" "-}"+\{ \- [$u # \-]* \- ([$u # [\- \}]] [$u # \-]* \- | \-)* \} ;++-- Whitespace (skipped)+$white+ ;++-- Symbols+@rsyms+ { tok (eitherResIdent TV) }++-- token VarIdentToken+[$u # [\t \n \r \ \! \" \# \( \) \, \- \. \; \< \> \? \[ \\ \] \{ \| \}]] [$u # [\t \n \r \ \" \# \( \) \, \; \< \> \[ \\ \] \{ \| \}]] *+ { tok (eitherResIdent T_VarIdentToken) }++-- token HoleIdentToken+\?+ { tok (eitherResIdent T_HoleIdentToken) }++-- Keywords and Ident+$l $i*+ { tok (eitherResIdent TV) }++-- String+\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | r | f)))* \"+ { tok (TL . unescapeInitTail) }++{+-- | Create a token with position.+tok :: (String -> Tok) -> (Posn -> String -> Token)+tok f p = PT p . f++-- | Token without position.+data Tok+ = TK {-# UNPACK #-} !TokSymbol -- ^ Reserved word or symbol.+ | TL !String -- ^ String literal.+ | TI !String -- ^ Integer literal.+ | TV !String -- ^ Identifier.+ | TD !String -- ^ Float literal.+ | TC !String -- ^ Character literal.+ | T_VarIdentToken !String+ | T_HoleIdentToken !String+ deriving (Eq, Show, Ord)++-- | Smart constructor for 'Tok' for the sake of backwards compatibility.+pattern TS :: String -> Int -> Tok+pattern TS t i = TK (TokSymbol t i)++-- | Keyword or symbol tokens have a unique ID.+data TokSymbol = TokSymbol+ { tsText :: String+ -- ^ Keyword or symbol text.+ , tsID :: !Int+ -- ^ Unique ID.+ } deriving (Show)++-- | Keyword/symbol equality is determined by the unique ID.+instance Eq TokSymbol where (==) = (==) `on` tsID++-- | Keyword/symbol ordering is determined by the unique ID.+instance Ord TokSymbol where compare = compare `on` tsID++-- | Token with position.+data Token+ = PT Posn Tok+ | Err Posn+ deriving (Eq, Show, Ord)++-- | Pretty print a position.+printPosn :: Posn -> String+printPosn (Pn _ l c) = "line " ++ show l ++ ", column " ++ show c++-- | Pretty print the position of the first token in the list.+tokenPos :: [Token] -> String+tokenPos (t:_) = printPosn (tokenPosn t)+tokenPos [] = "end of file"++-- | Get the position of a token.+tokenPosn :: Token -> Posn+tokenPosn (PT p _) = p+tokenPosn (Err p) = p++-- | Get line and column of a token.+tokenLineCol :: Token -> (Int, Int)+tokenLineCol = posLineCol . tokenPosn++-- | Get line and column of a position.+posLineCol :: Posn -> (Int, Int)+posLineCol (Pn _ l c) = (l,c)++-- | Convert a token into "position token" form.+mkPosToken :: Token -> ((Int, Int), String)+mkPosToken t = (tokenLineCol t, tokenText t)++-- | Convert a token to its text.+tokenText :: Token -> String+tokenText t = case t of+ PT _ (TS s _) -> s+ PT _ (TL s) -> show s+ PT _ (TI s) -> s+ PT _ (TV s) -> s+ PT _ (TD s) -> s+ PT _ (TC s) -> s+ Err _ -> "#error"+ PT _ (T_VarIdentToken s) -> s+ PT _ (T_HoleIdentToken s) -> s++-- | Convert a token to a string.+prToken :: Token -> String+prToken t = tokenText t++-- | Finite map from text to token organized as binary search tree.+data BTree+ = N -- ^ Nil (leaf).+ | B String Tok BTree BTree+ -- ^ Binary node.+ deriving (Show)++-- | Convert potential keyword into token or use fallback conversion.+eitherResIdent :: (String -> Tok) -> String -> Tok+eitherResIdent tv s = treeFind resWords+ where+ treeFind N = tv s+ treeFind (B a t left right) =+ case compare s a of+ LT -> treeFind left+ GT -> treeFind right+ EQ -> t++-- | The keywords and symbols of the language organized as binary search tree.+resWords :: BTree+resWords =+ b "BOT" 39+ (b "*\8321" 20+ (b "#postulate" 10+ (b "#compute-whnf" 5+ (b "#compute" 3+ (b "#check" 2 (b "#assume" 1 N N) N) (b "#compute-nf" 4 N N))+ (b "#end" 8 (b "#define" 7 (b "#def" 6 N N) N) (b "#lang" 9 N N)))+ (b "#variables" 15+ (b "#unset-option" 13+ (b "#set-option" 12 (b "#section" 11 N N) N)+ (b "#variable" 14 N N))+ (b "*" 18 (b ")" 17 (b "(" 16 N N) N) (b "*_1" 19 N N))))+ (b ":" 30+ (b "0\8322" 25+ (b "/\\" 23 (b "->" 22 (b "," 21 N N) N) (b "0_2" 24 N N))+ (b "1\8322" 28 (b "1_2" 27 (b "1" 26 N N) N) (b "2" 29 N N)))+ (b "=" 35+ (b "<" 33 (b ";" 32 (b ":=" 31 N N) N) (b "<=" 34 N N))+ (b "=_{" 37 (b "===" 36 N N) (b ">" 38 N N)))))+ (b "unit" 59+ (b "]" 49+ (b "U" 44+ (b "TOP" 42 (b "Sigma" 41 (b "CUBE" 40 N N) N) (b "TOPE" 43 N N))+ (b "\\" 47 (b "[" 46 (b "Unit" 45 N N) N) (b "\\/" 48 N N)))+ (b "recOR" 54+ (b "idJ" 52 (b "first" 51 (b "as" 50 N N) N) (b "recBOT" 53 N N))+ (b "rzk-1" 57+ (b "refl_{" 56 (b "refl" 55 N N) N) (b "second" 58 N N))))+ (b "\8594" 69+ (b "}" 64+ (b "|" 62 (b "{" 61 (b "uses" 60 N N) N) (b "|->" 63 N N))+ (b "\960\8321" 67+ (b "\931" 66 (b "\215" 65 N N) N) (b "\960\8322" 68 N N)))+ (b "\8801" 74+ (b "\8743" 72+ (b "\8721" 71 (b "\8614" 70 N N) N) (b "\8744" 73 N N))+ (b "\8868" 76 (b "\8804" 75 N N) (b "\8869" 77 N N)))))+ where+ b s n = B bs (TS bs n)+ where+ bs = s++-- | Unquote string literal.+unescapeInitTail :: String -> String+unescapeInitTail = id . unesc . tail . id+ where+ unesc s = case s of+ '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs+ '\\':'n':cs -> '\n' : unesc cs+ '\\':'t':cs -> '\t' : unesc cs+ '\\':'r':cs -> '\r' : unesc cs+ '\\':'f':cs -> '\f' : unesc cs+ '"':[] -> []+ c:cs -> c : unesc cs+ _ -> []++-------------------------------------------------------------------+-- Alex wrapper code.+-- A modified "posn" wrapper.+-------------------------------------------------------------------++data Posn = Pn !Int !Int !Int+ deriving (Eq, Show, Ord)++alexStartPos :: Posn+alexStartPos = Pn 0 1 1++alexMove :: Posn -> Char -> Posn+alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1)+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1+alexMove (Pn a l c) _ = Pn (a+1) l (c+1)++type Byte = Word8++type AlexInput = (Posn, -- current position,+ Char, -- previous char+ [Byte], -- pending bytes on the current char+ String) -- current input string++tokens :: String -> [Token]+tokens str = go (alexStartPos, '\n', [], str)+ where+ go :: AlexInput -> [Token]+ go inp@(pos, _, _, str) =+ case alexScan inp 0 of+ AlexEOF -> []+ AlexError (pos, _, _, _) -> [Err pos]+ AlexSkip inp' len -> go inp'+ AlexToken inp' len act -> act pos (take len str) : (go inp')++alexGetByte :: AlexInput -> Maybe (Byte,AlexInput)+alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s))+alexGetByte (p, _, [], s) =+ case s of+ [] -> Nothing+ (c:s) ->+ let p' = alexMove p c+ (b:bs) = utf8Encode c+ in p' `seq` Just (b, (p', c, bs, s))++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar (p, c, bs, s) = c++-- | Encode a Haskell String to a list of Word8 values, in UTF8 format.+utf8Encode :: Char -> [Word8]+utf8Encode = map fromIntegral . go . ord+ where+ go oc+ | oc <= 0x7f = [oc]++ | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6)+ , 0x80 + oc Data.Bits..&. 0x3f+ ]++ | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12)+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)+ , 0x80 + oc Data.Bits..&. 0x3f+ ]+ | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18)+ , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f)+ , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f)+ , 0x80 + oc Data.Bits..&. 0x3f+ ]+}
+ src/Language/Rzk/Syntax/Par.y view
@@ -0,0 +1,456 @@+-- -*- haskell -*- File generated by the BNF Converter (bnfc 2.9.4.1).++-- Parser definition for use with Happy+{+{-# OPTIONS_GHC -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}+{-# LANGUAGE PatternSynonyms #-}++module Language.Rzk.Syntax.Par+ ( happyError+ , myLexer+ , pModule+ , pHoleIdent+ , pVarIdent+ , pListVarIdent+ , pLanguageDecl+ , pLanguage+ , pCommand+ , pListCommand+ , pDeclUsedVars+ , pSectionName+ , pPattern+ , pListPattern+ , pParam+ , pListParam+ , pParamDecl+ , pRestriction+ , pListRestriction+ , pTerm7+ , pTerm5+ , pTerm4+ , pTerm3+ , pTerm2+ , pTerm1+ , pTerm6+ , pTerm+ , pListTerm+ ) where++import Prelude++import qualified Language.Rzk.Syntax.Abs+import Language.Rzk.Syntax.Lex++}++%name pModule_internal Module+%name pHoleIdent_internal HoleIdent+%name pVarIdent_internal VarIdent+%name pListVarIdent_internal ListVarIdent+%name pLanguageDecl_internal LanguageDecl+%name pLanguage_internal Language+%name pCommand_internal Command+%name pListCommand_internal ListCommand+%name pDeclUsedVars_internal DeclUsedVars+%name pSectionName_internal SectionName+%name pPattern_internal Pattern+%name pListPattern_internal ListPattern+%name pParam_internal Param+%name pListParam_internal ListParam+%name pParamDecl_internal ParamDecl+%name pRestriction_internal Restriction+%name pListRestriction_internal ListRestriction+%name pTerm7_internal Term7+%name pTerm5_internal Term5+%name pTerm4_internal Term4+%name pTerm3_internal Term3+%name pTerm2_internal Term2+%name pTerm1_internal Term1+%name pTerm6_internal Term6+%name pTerm_internal Term+%name pListTerm_internal ListTerm+-- no lexer declaration+%monad { Err } { (>>=) } { return }+%tokentype {Token}+%token+ '#assume' { PT _ (TS _ 1) }+ '#check' { PT _ (TS _ 2) }+ '#compute' { PT _ (TS _ 3) }+ '#compute-nf' { PT _ (TS _ 4) }+ '#compute-whnf' { PT _ (TS _ 5) }+ '#def' { PT _ (TS _ 6) }+ '#define' { PT _ (TS _ 7) }+ '#end' { PT _ (TS _ 8) }+ '#lang' { PT _ (TS _ 9) }+ '#postulate' { PT _ (TS _ 10) }+ '#section' { PT _ (TS _ 11) }+ '#set-option' { PT _ (TS _ 12) }+ '#unset-option' { PT _ (TS _ 13) }+ '#variable' { PT _ (TS _ 14) }+ '#variables' { PT _ (TS _ 15) }+ '(' { PT _ (TS _ 16) }+ ')' { PT _ (TS _ 17) }+ '*' { PT _ (TS _ 18) }+ '*_1' { PT _ (TS _ 19) }+ '*₁' { PT _ (TS _ 20) }+ ',' { PT _ (TS _ 21) }+ '->' { PT _ (TS _ 22) }+ '/\\' { PT _ (TS _ 23) }+ '0_2' { PT _ (TS _ 24) }+ '0₂' { PT _ (TS _ 25) }+ '1' { PT _ (TS _ 26) }+ '1_2' { PT _ (TS _ 27) }+ '1₂' { PT _ (TS _ 28) }+ '2' { PT _ (TS _ 29) }+ ':' { PT _ (TS _ 30) }+ ':=' { PT _ (TS _ 31) }+ ';' { PT _ (TS _ 32) }+ '<' { PT _ (TS _ 33) }+ '<=' { PT _ (TS _ 34) }+ '=' { PT _ (TS _ 35) }+ '===' { PT _ (TS _ 36) }+ '=_{' { PT _ (TS _ 37) }+ '>' { PT _ (TS _ 38) }+ 'BOT' { PT _ (TS _ 39) }+ 'CUBE' { PT _ (TS _ 40) }+ 'Sigma' { PT _ (TS _ 41) }+ 'TOP' { PT _ (TS _ 42) }+ 'TOPE' { PT _ (TS _ 43) }+ 'U' { PT _ (TS _ 44) }+ 'Unit' { PT _ (TS _ 45) }+ '[' { PT _ (TS _ 46) }+ '\\' { PT _ (TS _ 47) }+ '\\/' { PT _ (TS _ 48) }+ ']' { PT _ (TS _ 49) }+ 'as' { PT _ (TS _ 50) }+ 'first' { PT _ (TS _ 51) }+ 'idJ' { PT _ (TS _ 52) }+ 'recBOT' { PT _ (TS _ 53) }+ 'recOR' { PT _ (TS _ 54) }+ 'refl' { PT _ (TS _ 55) }+ 'refl_{' { PT _ (TS _ 56) }+ 'rzk-1' { PT _ (TS _ 57) }+ 'second' { PT _ (TS _ 58) }+ 'unit' { PT _ (TS _ 59) }+ 'uses' { PT _ (TS _ 60) }+ '{' { PT _ (TS _ 61) }+ '|' { PT _ (TS _ 62) }+ '|->' { PT _ (TS _ 63) }+ '}' { PT _ (TS _ 64) }+ '×' { PT _ (TS _ 65) }+ 'Σ' { PT _ (TS _ 66) }+ 'π₁' { PT _ (TS _ 67) }+ 'π₂' { PT _ (TS _ 68) }+ '→' { PT _ (TS _ 69) }+ '↦' { PT _ (TS _ 70) }+ '∑' { PT _ (TS _ 71) }+ '∧' { PT _ (TS _ 72) }+ '∨' { PT _ (TS _ 73) }+ '≡' { PT _ (TS _ 74) }+ '≤' { PT _ (TS _ 75) }+ '⊤' { PT _ (TS _ 76) }+ '⊥' { PT _ (TS _ 77) }+ L_quoted { PT _ (TL _) }+ L_VarIdentToken { PT _ (T_VarIdentToken _) }+ L_HoleIdentToken { PT _ (T_HoleIdentToken _) }++%%++String :: { (Language.Rzk.Syntax.Abs.BNFC'Position, String) }+String : L_quoted { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), ((\(PT _ (TL s)) -> s) $1)) }++VarIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdentToken) }+VarIdentToken : L_VarIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.VarIdentToken (tokenText $1)) }++HoleIdentToken :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdentToken) }+HoleIdentToken : L_HoleIdentToken { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.HoleIdentToken (tokenText $1)) }++Module :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Module) }+Module+ : LanguageDecl ListCommand { (fst $1, Language.Rzk.Syntax.Abs.Module (fst $1) (snd $1) (snd $2)) }++HoleIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.HoleIdent) }+HoleIdent+ : HoleIdentToken { (fst $1, Language.Rzk.Syntax.Abs.HoleIdent (fst $1) (snd $1)) }++VarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.VarIdent) }+VarIdent+ : VarIdentToken { (fst $1, Language.Rzk.Syntax.Abs.VarIdent (fst $1) (snd $1)) }++ListVarIdent :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.VarIdent]) }+ListVarIdent+ : VarIdent { (fst $1, (:[]) (snd $1)) }+ | VarIdent ListVarIdent { (fst $1, (:) (snd $1) (snd $2)) }++LanguageDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.LanguageDecl) }+LanguageDecl+ : '#lang' Language ';' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.LanguageDecl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }++Language :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Language) }+Language+ : 'rzk-1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Rzk1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }++Command :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Command) }+Command+ : '#set-option' String '=' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#unset-option' String { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandUnsetOption (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#check' Term ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCheck (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#compute' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandCompute (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#compute-whnf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeWHNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#compute-nf' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandComputeNF (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | '#postulate' VarIdent DeclUsedVars ListParam ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandPostulate (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6)) }+ | '#postulate' VarIdent DeclUsedVars ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandPostulateNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5)) }+ | '#assume' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandAssume (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#variable' VarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariable (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#variables' ListVarIdent ':' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandVariables (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '#section' SectionName ';' ListCommand '#end' SectionName { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandSection (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }+ | '#define' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CommandDefine (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }+ | '#define' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefineNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }+ | '#def' VarIdent DeclUsedVars ListParam ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDef (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $4) (snd $6) (snd $8)) }+ | '#def' VarIdent DeclUsedVars ':' Term ':=' Term { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.commandDefNoParams (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $3) (snd $5) (snd $7)) }++ListCommand :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Command]) }+ListCommand+ : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, []) }+ | Command ';' ListCommand { (fst $1, (:) (snd $1) (snd $3)) }++DeclUsedVars :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.DeclUsedVars) }+DeclUsedVars+ : 'uses' '(' ListVarIdent ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.DeclUsedVars (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }+ | {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.noDeclUsedVars Language.Rzk.Syntax.Abs.BNFC'NoPosition) }++SectionName :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.SectionName) }+SectionName+ : {- empty -} { (Language.Rzk.Syntax.Abs.BNFC'NoPosition, Language.Rzk.Syntax.Abs.NoSectionName Language.Rzk.Syntax.Abs.BNFC'NoPosition) }+ | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.SomeSectionName (fst $1) (snd $1)) }++Pattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Pattern) }+Pattern+ : 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.PatternVar (fst $1) (snd $1)) }+ | '(' Pattern ',' Pattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternPair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }++ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) }+ListPattern+ : Pattern { (fst $1, (:[]) (snd $1)) }+ | Pattern ListPattern { (fst $1, (:) (snd $1) (snd $2)) }++Param :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Param) }+Param+ : Pattern { (fst $1, Language.Rzk.Syntax.Abs.ParamPattern (fst $1) (snd $1)) }+ | '(' ListPattern ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '(' ListPattern ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }+ | '{' Pattern ':' Term '|' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }++ListParam :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Param]) }+ListParam+ : Param { (fst $1, (:[]) (snd $1)) }+ | Param ListParam { (fst $1, (:) (snd $1) (snd $2)) }++ParamDecl :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.ParamDecl) }+ParamDecl+ : Term6 { (fst $1, Language.Rzk.Syntax.Abs.ParamType (fst $1) (snd $1)) }+ | '(' Term ':' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '(' Term ':' Term '|' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermShape (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }+ | '{' Pattern ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ParamTermTypeDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '{' '(' 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)) }++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)) }+ | Term '|->' Term { (fst $1, Language.Rzk.Syntax.Abs.ASCII_Restriction (fst $1) (snd $1) (snd $3)) }++ListRestriction :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Restriction]) }+ListRestriction+ : Restriction { (fst $1, (:[]) (snd $1)) }+ | Restriction ',' ListRestriction { (fst $1, (:) (snd $1) (snd $3)) }++Term7 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term7+ : 'U' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Universe (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'CUBE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseCube (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'TOPE' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.UniverseTope (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '*₁' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '0₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '1₂' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '⊤' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '⊥' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'recBOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'recOR' '(' ListRestriction ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOr (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3)) }+ | 'recOR' '(' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.RecOrDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9)) }+ | 'Unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '<' ParamDecl '→' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '(' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Pair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Unit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'refl' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Refl (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'refl_{' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTerm (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | 'refl_{' Term ':' Term '}' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ReflTermType (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | 'idJ' '(' Term ',' Term ',' Term ',' Term ',' Term ',' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.IdJ (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $7) (snd $9) (snd $11) (snd $13)) }+ | HoleIdent { (fst $1, Language.Rzk.Syntax.Abs.Hole (fst $1) (snd $1)) }+ | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.Var (fst $1) (snd $1)) }+ | '(' Term ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), (snd $2)) }+ | '*_1' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_CubeUnitStar (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '0_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_0 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '1_2' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Cube2_1 (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'TOP' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeTop (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | 'BOT' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TopeBottom (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) }+ | '<' ParamDecl '->' Term '>' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }++Term5 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term5+ : Term5 '×' Term6 { (fst $1, Language.Rzk.Syntax.Abs.CubeProduct (fst $1) (snd $1) (snd $3)) }+ | Term6 { (fst $1, (snd $1)) }+ | Term5 '*' Term6 { (fst $1, Language.Rzk.Syntax.Abs.ascii_CubeProduct (fst $1) (snd $1) (snd $3)) }++Term4 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term4+ : Term5 '≡' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeEQ (fst $1) (snd $1) (snd $3)) }+ | Term5 '≤' Term5 { (fst $1, Language.Rzk.Syntax.Abs.TopeLEQ (fst $1) (snd $1) (snd $3)) }+ | Term5 { (fst $1, (snd $1)) }+ | Term5 '===' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeEQ (fst $1) (snd $1) (snd $3)) }+ | Term5 '<=' Term5 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeLEQ (fst $1) (snd $1) (snd $3)) }++Term3 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term3+ : Term4 '∧' Term3 { (fst $1, Language.Rzk.Syntax.Abs.TopeAnd (fst $1) (snd $1) (snd $3)) }+ | Term4 { (fst $1, (snd $1)) }+ | Term4 '/\\' Term3 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeAnd (fst $1) (snd $1) (snd $3)) }++Term2 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term2+ : Term3 '∨' Term2 { (fst $1, Language.Rzk.Syntax.Abs.TopeOr (fst $1) (snd $1) (snd $3)) }+ | Term3 { (fst $1, (snd $1)) }+ | Term3 '\\/' Term2 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TopeOr (fst $1) (snd $1) (snd $3)) }++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)) }+ | 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)) }+ | Term2 { (fst $1, (snd $1)) }+ | ParamDecl '->' Term1 { (fst $1, Language.Rzk.Syntax.Abs.ASCII_TypeFun (fst $1) (snd $1) (snd $3)) }+ | 'Sigma' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigma (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }+ | '\\' ListParam '->' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Lambda (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) }+ | '∑' '(' Pattern ':' Term ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaAlt (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $3) (snd $5) (snd $8)) }++Term6 :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term6+ : Term6 '[' ListRestriction ']' { (fst $1, Language.Rzk.Syntax.Abs.TypeRestricted (fst $1) (snd $1) (snd $3)) }+ | Term6 Term7 { (fst $1, Language.Rzk.Syntax.Abs.App (fst $1) (snd $1) (snd $2)) }+ | 'π₁' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | 'π₂' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | Term7 { (fst $1, (snd $1)) }+ | 'first' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_First (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }+ | 'second' Term7 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_Second (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2)) }++Term :: { (Language.Rzk.Syntax.Abs.BNFC'Position, Language.Rzk.Syntax.Abs.Term) }+Term+ : Term2 'as' Term1 { (fst $1, Language.Rzk.Syntax.Abs.TypeAsc (fst $1) (snd $1) (snd $3)) }+ | Term1 { (fst $1, (snd $1)) }++ListTerm :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Term]) }+ListTerm+ : Term { (fst $1, (:[]) (snd $1)) }+ | Term ',' ListTerm { (fst $1, (:) (snd $1) (snd $3)) }++{++type Err = Either String++happyError :: [Token] -> Err a+happyError ts = Left $+ "syntax error at " ++ tokenPos ts +++ case ts of+ [] -> []+ [Err _] -> " due to lexer error"+ t:_ -> " before `" ++ (prToken t) ++ "'"++myLexer :: String -> [Token]+myLexer = tokens++-- Entrypoints++pModule :: [Token] -> Err Language.Rzk.Syntax.Abs.Module+pModule = fmap snd . pModule_internal++pHoleIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.HoleIdent+pHoleIdent = fmap snd . pHoleIdent_internal++pVarIdent :: [Token] -> Err Language.Rzk.Syntax.Abs.VarIdent+pVarIdent = fmap snd . pVarIdent_internal++pListVarIdent :: [Token] -> Err [Language.Rzk.Syntax.Abs.VarIdent]+pListVarIdent = fmap snd . pListVarIdent_internal++pLanguageDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.LanguageDecl+pLanguageDecl = fmap snd . pLanguageDecl_internal++pLanguage :: [Token] -> Err Language.Rzk.Syntax.Abs.Language+pLanguage = fmap snd . pLanguage_internal++pCommand :: [Token] -> Err Language.Rzk.Syntax.Abs.Command+pCommand = fmap snd . pCommand_internal++pListCommand :: [Token] -> Err [Language.Rzk.Syntax.Abs.Command]+pListCommand = fmap snd . pListCommand_internal++pDeclUsedVars :: [Token] -> Err Language.Rzk.Syntax.Abs.DeclUsedVars+pDeclUsedVars = fmap snd . pDeclUsedVars_internal++pSectionName :: [Token] -> Err Language.Rzk.Syntax.Abs.SectionName+pSectionName = fmap snd . pSectionName_internal++pPattern :: [Token] -> Err Language.Rzk.Syntax.Abs.Pattern+pPattern = fmap snd . pPattern_internal++pListPattern :: [Token] -> Err [Language.Rzk.Syntax.Abs.Pattern]+pListPattern = fmap snd . pListPattern_internal++pParam :: [Token] -> Err Language.Rzk.Syntax.Abs.Param+pParam = fmap snd . pParam_internal++pListParam :: [Token] -> Err [Language.Rzk.Syntax.Abs.Param]+pListParam = fmap snd . pListParam_internal++pParamDecl :: [Token] -> Err Language.Rzk.Syntax.Abs.ParamDecl+pParamDecl = fmap snd . pParamDecl_internal++pRestriction :: [Token] -> Err Language.Rzk.Syntax.Abs.Restriction+pRestriction = fmap snd . pRestriction_internal++pListRestriction :: [Token] -> Err [Language.Rzk.Syntax.Abs.Restriction]+pListRestriction = fmap snd . pListRestriction_internal++pTerm7 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm7 = fmap snd . pTerm7_internal++pTerm5 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm5 = fmap snd . pTerm5_internal++pTerm4 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm4 = fmap snd . pTerm4_internal++pTerm3 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm3 = fmap snd . pTerm3_internal++pTerm2 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm2 = fmap snd . pTerm2_internal++pTerm1 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm1 = fmap snd . pTerm1_internal++pTerm6 :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm6 = fmap snd . pTerm6_internal++pTerm :: [Token] -> Err Language.Rzk.Syntax.Abs.Term+pTerm = fmap snd . pTerm_internal++pListTerm :: [Token] -> Err [Language.Rzk.Syntax.Abs.Term]+pListTerm = fmap snd . pListTerm_internal+}+
src/Rzk/TypeCheck.hs view
@@ -107,8 +107,8 @@ withCommand command $ do mapM_ checkDefinedVar (varIdentAt path <$> vars) paramDecls <- concat <$> mapM paramToParamDecl params- ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT -- >>= pure . termIsWHNF- term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT >>= pure . termIsWHNF+ ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT+ term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars) fmap (decl :) $ localDeclPrepared decl $ do@@ -127,7 +127,7 @@ withCommand command $ do mapM_ checkDefinedVar (varIdentAt path <$> vars) paramDecls <- concat <$> mapM paramToParamDecl params- ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT -- >>= pure . termIsWHNF+ ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars) fmap (decl :) $ localDeclPrepared decl $@@ -137,7 +137,7 @@ traceTypeCheck Normal ("[ " <> show i <> " out of " <> show totalCommands <> " ]" <> " Checking " <> Rzk.printTree term <> " : " <> Rzk.printTree ty ) $ do withCommand command $ do- ty' <- typecheck (toTerm' ty) universeT >>= whnfT -- >>= pure . termIsWHNF+ ty' <- typecheck (toTerm' ty) universeT >>= whnfT _term' <- typecheck (toTerm' term) ty' go (i + 1) moreCommands @@ -1228,6 +1228,10 @@ -- unit : Unit whnfT :: Eq var => TermT var -> TypeCheck var (TermT var) whnfT tt = performing (ActionWHNF tt) $ case tt of+ -- use cached result if it exists+ Free (AnnF info _)+ | Just tt' <- infoWHNF info -> pure tt'+ -- universe constants UniverseT{} -> pure tt UniverseCubeT{} -> pure tt@@ -1263,9 +1267,6 @@ -- type ascriptions are ignored, since we already have a typechecked term TypeAscT _ty term _ty' -> whnfT term - Free (AnnF info _)- | Just tt' <- infoWHNF info -> pure tt'- -- check if we have cube or a tope term (if so, compute NF) _ -> typeOf tt >>= \case UniverseCubeT{} -> nfTope tt@@ -1281,7 +1282,7 @@ UniverseCubeT{} -> nfTope tt -- now we are in the type layer- _ -> do+ _ -> fmap termIsWHNF $ do -- check if we are in the empty context inBottom <- asks localTopesEntailBottom if inBottom@@ -1618,9 +1619,16 @@ where performUnification = unifyInCurrentContext mterm expected actual +unifyViaDecompose :: Eq var => TermT var -> TermT var -> TypeCheck var ()+unifyViaDecompose expected actual | expected == actual = return ()+unifyViaDecompose (AppT _ f x) (AppT _ g y) = do+ unify Nothing f g+ unify Nothing x y+unifyViaDecompose _ _ = issueTypeError (TypeErrorOther "cannot decompose")+ unifyInCurrentContext :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var () unifyInCurrentContext mterm expected actual = performing action $- unless (expected == actual) $ do -- NOTE: this gives a small, but noticeable speedup+ unifyViaDecompose expected actual `catchError` \_ -> do -- NOTE: this gives a small, but noticeable speedup expectedVal <- whnfT expected actualVal <- whnfT actual (expected', actual') <- asks covariance >>= \case