packages feed

rzk 0.7.4 → 0.7.5

raw patch · 11 files changed

+237/−62 lines, 11 files

Files

ChangeLog.md view
@@ -6,9 +6,24 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.7.5 — 2024-08-18++Minor changes:++- Suport syntax sugar for nested Σ-types (see [#183](https://github.com/rzk-lang/rzk/pull/183))+- Improve error reporting (see [#176](https://github.com/rzk-lang/rzk/pull/176) and [#179](https://github.com/rzk-lang/rzk/pull/179))++Fixes:++- Support newer `lsp` (specifically, `lsp-2.7.0.0`, see [#188](https://github.com/rzk-lang/rzk/pull/188))+- Fix CI (see [#184](https://github.com/rzk-lang/rzk/pull/184))+- Fix build of nix flake on aarch64-darwin (see [#181](https://github.com/rzk-lang/rzk/pull/181))+- Small documentation fixes (see [#178](https://github.com/rzk-lang/rzk/pull/178))+ ## v0.7.4 — 2024-04-01  Fixes:+ - Fix caching in Rzk Language Server, especially in presence of errors (see [#167](https://github.com/rzk-lang/rzk/pull/167)) - Fix CI for the Rzk Playground (see [#174](https://github.com/rzk-lang/rzk/pull/174)) @@ -18,33 +33,37 @@ ## v0.7.3 — 2023-12-16  Fixes:+ - Fix overlapping edits in the formatter, hopefully making it idempotent (see [#160](https://github.com/rzk-lang/rzk/pull/160)); - Fix formatter crashing the language server (see [#161](https://github.com/rzk-lang/rzk/pull/161)); - Avoid unnecessary typechecking when semantics of a file has not changed (see [#159](https://github.com/rzk-lang/rzk/pull/159)); - Stop typechecking after the first parse error (avoid invalid cache) (see [`68ab0b4`](https://github.com/rzk-lang/rzk/commit/68ab0b4dd3d627756e10adb55cb16845b08d09d9));  Other:+ - Add unit tests for the formatter (see [#157](https://github.com/rzk-lang/rzk/pull/157));  ## v0.7.2 — 2023-12-12  Fixes:+ - Fixes for `rzk format`:-    - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));-    - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156));+  - Fix extra space after open parens in formatter (see [#155](https://github.com/rzk-lang/rzk/pull/155));+  - Replace line string content with tokens when checking open parens (see [#156](https://github.com/rzk-lang/rzk/pull/156)); - Throw an error when `rzk.yaml`'s `include` is empty (see [#154](https://github.com/rzk-lang/rzk/pull/154));  Changes to the Rzk website:-  - Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));-      - English is the default;-      - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;-  - Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));-      - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;-  - Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));-  - Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))-  - Add (default) social cards-  - Integrate ToC on the left-  - Use Inria Sans for English, PT Sans for Russian++- Support multiple languages in the documentation (see [#150](https://github.com/rzk-lang/rzk/pull/150));+  - English is the default;+  - Russian documentation is partially translated and is available at <http://rzk-lang.github.io/rzk/ru/>;+- Add a blog (see [#153](https://github.com/rzk-lang/rzk/pull/153) and [`e438820`](https://github.com/rzk-lang/rzk/commit/e4388202cea59531903c4c24b939841b2771ceb7));+  - The blog is not versioned and is always available at <https://rzk-lang.github.io/rzk/en/blog/>;+- Add a new [Other proof assistants for HoTT](https://rzk-lang.github.io/rzk/en/v0.7.2/related/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/related/));+- Add a new [Introduction to Dependent Types](https://rzk-lang.github.io/rzk/en/v0.7.2/getting-started/dependent-types.rzk/) page (also [in Russian](https://rzk-lang.github.io/rzk/ru/v0.7.2/getting-started/dependent-types.rzk/))+- Add (default) social cards+- Integrate ToC on the left+- Use Inria Sans for English, PT Sans for Russian  ## v0.7.1 — 2023-12-08
app/Main.hs view
@@ -16,7 +16,7 @@                                           (>=>)) import           Data.Version            (showVersion) -#ifdef LSP+#ifdef LSP_ENABLED import           Language.Rzk.VSCode.Lsp (runLsp) #endif @@ -66,7 +66,7 @@         Right _decls -> putStrLn "Everything is ok!"      Lsp ->-#ifdef LSP+#ifdef LSP_ENABLED       void runLsp #else       error "rzk lsp is not supported with this build"
grammar/Syntax.cf view
@@ -60,6 +60,7 @@ PatternUnit.      Pattern ::= "unit" ; PatternVar.       Pattern ::= VarIdent ; PatternPair.      Pattern ::= "(" Pattern "," Pattern ")" ;+PatternTuple.     Pattern ::= "(" Pattern "," Pattern "," [Pattern] ")" ; separator nonempty Pattern "" ;  -- Parameter introduction (for lambda abstractions)@@ -78,6 +79,10 @@ 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 +111,7 @@ -- Types TypeFun.        Term1 ::= ParamDecl "→" Term1 ; TypeSigma.      Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;+TypeSigmaTuple. Term1 ::= "Σ" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ; TypeUnit.       Term7 ::= "Unit" ; TypeId.         Term1 ::= Term2 "=_{" Term "}" Term2 ; TypeIdSimple.   Term1 ::= Term2 "=" Term2 ;@@ -115,6 +121,7 @@ App.            Term6 ::= Term6 Term7 ; Lambda.         Term1 ::= "\\" [Param] "→" Term1 ; Pair.           Term7 ::= "(" Term "," Term ")" ;+Tuple.          Term7 ::= "(" Term "," Term "," [Term] ")" ; First.          Term6 ::= "π₁" Term7 ; Second.         Term6 ::= "π₂" Term7 ; Unit.           Term7 ::= "unit" ;@@ -149,6 +156,7 @@  ASCII_TypeFun.        Term1 ::= ParamDecl "->" Term1 ; ASCII_TypeSigma.      Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;+ASCII_TypeSigmaTuple. Term1 ::= "Sigma" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;  ASCII_Lambda.         Term1 ::= "\\" [Param] "->" Term1 ; ASCII_Restriction. Restriction ::= Term "|->" Term ;@@ -161,4 +169,6 @@ -- Alternative Unicode syntax rules  unicode_TypeSigmaAlt.   Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ;    -- \sum+unicode_TypeSigmaTupleAlt. Term1 ::= "∑" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ; define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;+define unicode_TypeSigmaTupleAlt par pars t = TypeSigmaTuple par pars t ;
rzk.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           rzk-version:        0.7.4+version:        0.7.5 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@@ -13,7 +13,7 @@ bug-reports:    https://github.com/rzk-lang/rzk/issues author:         Nikolai Kudasov maintainer:     nickolay.kudasov@gmail.com-copyright:      2023 Nikolai Kudasov+copyright:      2023-2024 Nikolai Kudasov license:        BSD3 license-file:   LICENSE build-type:     Custom@@ -76,7 +76,7 @@     , yaml >=0.11.0.0   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)-    cpp-options: -DLSP+    cpp-options: -DLSP_ENABLED   if flag(lsp) && !impl(ghcjs)     exposed-modules:         Language.Rzk.VSCode.Config@@ -121,7 +121,7 @@     , yaml >=0.11.0.0   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)-    cpp-options: -DLSP+    cpp-options: -DLSP_ENABLED   if !impl(ghcjs)     build-depends:         optparse-generic >=1.4.0@@ -153,7 +153,7 @@     , yaml >=0.11.0.0   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)-    cpp-options: -DLSP+    cpp-options: -DLSP_ENABLED  test-suite rzk-test   type: exitcode-stdio-1.0@@ -185,4 +185,4 @@     , yaml >=0.11.0.0   default-language: Haskell2010   if flag(lsp) && !impl(ghcjs)-    cpp-options: -DLSP+    cpp-options: -DLSP_ENABLED
src/Language/Rzk/Free/Syntax.hs view
@@ -173,7 +173,13 @@     bindings (Rzk.PatternVar _loc (Rzk.VarIdent _ "_")) _ = []     bindings (Rzk.PatternVar _loc x)    t = [(varIdent x, t)]     bindings (Rzk.PatternPair _loc l r) t = bindings l (First t) <> bindings r (Second t)+    bindings (Rzk.PatternTuple loc p1 p2 ps) t = bindings (desugarTuple loc (reverse ps) p2 p1) t +desugarTuple loc ps p2 p1 =+  case ps of+    []          -> Rzk.PatternPair loc p1 p2+    pLast : ps' -> Rzk.PatternPair loc (desugarTuple loc ps' p2 p1) pLast+ toTerm :: (VarIdent -> Term a) -> Rzk.Term -> Term a toTerm bvars = go   where@@ -209,7 +215,6 @@         (Rzk.TypeFun loc (Rzk.ParamTermShape loc' (patternToTerm pat) cube tope) ret)       t@(Rzk.Lambda loc ((Rzk.ParamPatternShapeDeprecated loc' pat cube tope):params) body) -> deprecated t         (Rzk.Lambda loc ((Rzk.ParamPatternShape loc' [pat] cube tope):params) body)-       -- ASCII versions       Rzk.ASCII_CubeUnitStar loc -> go (Rzk.CubeUnitStar loc)       Rzk.ASCII_Cube2_0 loc -> go (Rzk.Cube2_0 loc)@@ -223,6 +228,7 @@        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_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)@@ -256,6 +262,8 @@       Rzk.Unit _loc -> Unit       Rzk.App _loc f x -> App (go f) (go x)       Rzk.Pair _loc l r -> Pair (go l) (go r)+      Rzk.Tuple _loc p1 p2 (p:ps) -> go (Rzk.Tuple _loc (Rzk.Pair _loc p1 p2) p ps)+      Rzk.Tuple _loc p1 p2 [] -> go (Rzk.Pair _loc p1 p2)       Rzk.First _loc term -> First (go term)       Rzk.Second _loc term -> Second (go term)       Rzk.Refl _loc -> Refl Nothing@@ -280,11 +288,18 @@       Rzk.TypeSigma _loc pat tA tB ->         TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB) +      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.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 ->         Lambda (patternVar pat) Nothing (toScopePattern pat bvars (Rzk.Lambda _loc params body))       Rzk.Lambda _loc (Rzk.ParamPatternType _ [] _ty : params) body ->-        go (Rzk.Lambda _loc params body)+        go (Rzk.Lambda _loc params body)                               Rzk.Lambda _loc (Rzk.ParamPatternType _ (pat:pats) ty : params) body ->         Lambda (patternVar pat) (Just (go ty, Nothing))           (toScopePattern pat bvars (Rzk.Lambda _loc (Rzk.ParamPatternType _loc pats ty : params) body))@@ -317,6 +332,7 @@       Rzk.PatternVar loc x    -> Rzk.Var loc x       Rzk.PatternPair loc l r -> Rzk.Pair loc (ptt l) (ptt r)       Rzk.PatternUnit loc     -> Rzk.Unit loc+      Rzk.PatternTuple loc p1 p2 ps -> patternToTerm (desugarTuple loc (reverse ps) p2 p1)  unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern unsafeTermToPattern = ttp
src/Language/Rzk/Syntax/Abs.hs view
@@ -72,6 +72,7 @@     = PatternUnit a     | PatternVar a (VarIdent' a)     | PatternPair a (Pattern' a) (Pattern' a)+    | PatternTuple a (Pattern' a) (Pattern' a) [Pattern' a]   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic)  type Param = Param' BNFC'Position@@ -91,6 +92,10 @@     | 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 +124,7 @@     | RecOrDeprecated a (Term' a) (Term' a) (Term' a) (Term' a)     | TypeFun a (ParamDecl' a) (Term' a)     | TypeSigma a (Pattern' a) (Term' a) (Term' a)+    | TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)     | TypeUnit a     | TypeId a (Term' a) (Term' a) (Term' a)     | TypeIdSimple a (Term' a) (Term' a)@@ -127,6 +133,7 @@     | App a (Term' a) (Term' a)     | Lambda a [Param' a] (Term' a)     | Pair a (Term' a) (Term' a)+    | Tuple a (Term' a) (Term' a) [Term' a]     | First a (Term' a)     | Second a (Term' a)     | Unit a@@ -148,6 +155,7 @@     | ASCII_TopeOr a (Term' a) (Term' a)     | ASCII_TypeFun a (ParamDecl' a) (Term' a)     | ASCII_TypeSigma a (Pattern' a) (Term' a) (Term' a)+    | ASCII_TypeSigmaTuple a (SigmaParam' a) [SigmaParam' a] (Term' a)     | ASCII_Lambda a [Param' a] (Term' a)     | ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a)     | ASCII_First a (Term' a)@@ -184,6 +192,9 @@ unicode_TypeSigmaAlt :: a -> Pattern' a -> Term' a -> Term' a -> Term' a unicode_TypeSigmaAlt = \ _a pat fst snd -> TypeSigma _a pat fst snd +unicode_TypeSigmaTupleAlt :: a -> SigmaParam' a -> [SigmaParam' a] -> Term' a -> Term' a+unicode_TypeSigmaTupleAlt = \ _a par pars t -> TypeSigmaTuple _a par pars t+ newtype VarIdentToken = VarIdentToken String   deriving (C.Eq, C.Ord, C.Show, C.Read, C.Data, C.Typeable, C.Generic, Data.String.IsString) @@ -253,6 +264,7 @@     PatternUnit p -> p     PatternVar p _ -> p     PatternPair p _ _ -> p+    PatternTuple p _ _ _ -> p  instance HasPosition Param where   hasPosition = \case@@ -269,6 +281,10 @@     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 +312,7 @@     RecOrDeprecated p _ _ _ _ -> p     TypeFun p _ _ -> p     TypeSigma p _ _ _ -> p+    TypeSigmaTuple p _ _ _ -> p     TypeUnit p -> p     TypeId p _ _ _ -> p     TypeIdSimple p _ _ -> p@@ -304,6 +321,7 @@     App p _ _ -> p     Lambda p _ _ -> p     Pair p _ _ -> p+    Tuple p _ _ _ -> p     First p _ -> p     Second p _ -> p     Unit p -> p@@ -325,6 +343,7 @@     ASCII_TopeOr p _ _ -> p     ASCII_TypeFun p _ _ -> p     ASCII_TypeSigma p _ _ _ -> p+    ASCII_TypeSigmaTuple p _ _ _ -> p     ASCII_Lambda p _ _ -> p     ASCII_TypeExtensionDeprecated p _ _ -> p     ASCII_First p _ -> p
src/Language/Rzk/Syntax/Par.y view
@@ -23,6 +23,8 @@   , pParam   , pListParam   , pParamDecl+  , pSigmaParam+  , pListSigmaParam   , pRestriction   , pListRestriction   , pTerm7@@ -58,6 +60,8 @@ %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@@ -230,6 +234,7 @@   : '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)) }+  | '(' Pattern ',' Pattern ',' ListPattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }  ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) } ListPattern@@ -257,6 +262,15 @@   | '{' '(' 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)) }@@ -285,6 +299,7 @@   | '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)) }+  | '(' Term ',' Term ',' ListTerm ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.Tuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) }   | '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)) }@@ -330,14 +345,17 @@ 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)) }+  | 'Σ' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.TypeSigmaTuple (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)) }+  | 'Sigma' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple (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)) }+  | '∑' '(' SigmaParam ',' ListSigmaParam ')' ',' Term1 { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.unicode_TypeSigmaTupleAlt (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@@ -420,6 +438,12 @@  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
src/Language/Rzk/Syntax/Print.hs view
@@ -198,6 +198,7 @@     Language.Rzk.Syntax.Abs.PatternUnit _ -> prPrec i 0 (concatD [doc (showString "unit")])     Language.Rzk.Syntax.Abs.PatternVar _ varident -> prPrec i 0 (concatD [prt 0 varident])     Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")])+    Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ","), prt 0 patterns, doc (showString ")")])  instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where   prt _ [] = concatD []@@ -224,6 +225,15 @@     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 +266,7 @@     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.TypeSigmaTuple _ 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])@@ -264,6 +275,7 @@     Language.Rzk.Syntax.Abs.App _ term1 term2 -> prPrec i 6 (concatD [prt 6 term1, prt 7 term2])     Language.Rzk.Syntax.Abs.Lambda _ params term -> prPrec i 1 (concatD [doc (showString "\\"), prt 0 params, doc (showString "\8594"), prt 1 term])     Language.Rzk.Syntax.Abs.Pair _ term1 term2 -> prPrec i 7 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ")")])+    Language.Rzk.Syntax.Abs.Tuple _ term1 term2 terms -> prPrec i 7 (concatD [doc (showString "("), prt 0 term1, doc (showString ","), prt 0 term2, doc (showString ","), prt 0 terms, doc (showString ")")])     Language.Rzk.Syntax.Abs.First _ term -> prPrec i 6 (concatD [doc (showString "\960\8321"), prt 7 term])     Language.Rzk.Syntax.Abs.Second _ term -> prPrec i 6 (concatD [doc (showString "\960\8322"), prt 7 term])     Language.Rzk.Syntax.Abs.Unit _ -> prPrec i 7 (concatD [doc (showString "unit")])@@ -285,6 +297,7 @@     Language.Rzk.Syntax.Abs.ASCII_TopeOr _ term1 term2 -> prPrec i 2 (concatD [prt 3 term1, doc (showString "\\/"), prt 2 term2])     Language.Rzk.Syntax.Abs.ASCII_TypeFun _ paramdecl term -> prPrec i 1 (concatD [prt 0 paramdecl, doc (showString "->"), prt 1 term])     Language.Rzk.Syntax.Abs.ASCII_TypeSigma _ pattern_ term1 term2 -> prPrec i 1 (concatD [doc (showString "Sigma"), doc (showString "("), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString ")"), doc (showString ","), prt 1 term2])+    Language.Rzk.Syntax.Abs.ASCII_TypeSigmaTuple _ sigmaparam sigmaparams term -> prPrec i 1 (concatD [doc (showString "Sigma"), doc (showString "("), prt 0 sigmaparam, doc (showString ","), prt 0 sigmaparams, doc (showString ")"), doc (showString ","), prt 1 term])     Language.Rzk.Syntax.Abs.ASCII_Lambda _ params term -> prPrec i 1 (concatD [doc (showString "\\"), prt 0 params, doc (showString "->"), prt 1 term])     Language.Rzk.Syntax.Abs.ASCII_TypeExtensionDeprecated _ paramdecl term -> prPrec i 7 (concatD [doc (showString "<"), prt 0 paramdecl, doc (showString "->"), prt 0 term, doc (showString ">")])     Language.Rzk.Syntax.Abs.ASCII_First _ term -> prPrec i 6 (concatD [doc (showString "first"), prt 7 term])
src/Language/Rzk/VSCode/Handlers.hs view
@@ -1,10 +1,12 @@+{-# OPTIONS_GHC -Wno-orphans #-}+{-# LANGUAGE CPP           #-} {-# LANGUAGE DataKinds           #-} {-# LANGUAGE LambdaCase          #-} {-# LANGUAGE OverloadedStrings   #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications    #-}-{-# OPTIONS_GHC -Wno-orphans #-}-{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ViewPatterns        #-}+{-# LANGUAGE RecordWildCards     #-}  module Language.Rzk.VSCode.Handlers (   typecheckFromConfigFile,@@ -40,6 +42,7 @@ import           System.FilePath               (makeRelative, (</>)) import           System.FilePath.Glob          (compile, globDir) +import           Data.Char                     (isDigit) import           Language.Rzk.Free.Syntax      (RzkPosition (RzkPosition),                                                 VarIdent (getVarIdent)) import           Language.Rzk.Syntax           (Module, VarIdent' (VarIdent),@@ -53,6 +56,7 @@                                                 formatTextEdits) import           Rzk.Project.Config            (ProjectConfig (include)) import           Rzk.TypeCheck+import           Text.Read                     (readMaybe)  -- | Given a list of file paths, reads them and parses them as Rzk modules, --   returning the same list of file paths but with the parsed module (or parse error)@@ -181,7 +185,7 @@         line = fromIntegral $ fromMaybe 0 $ extractLineNumber err      diagnosticOfParseError :: String -> Diagnostic-    diagnosticOfParseError err = Diagnostic (Range (Position 0 0) (Position 0 0))+    diagnosticOfParseError err = Diagnostic (Range (Position errLine errColumnStart) (Position errLine errColumnEnd))                       (Just DiagnosticSeverity_Error)                       (Just $ InR "parse-error")                       Nothing@@ -190,6 +194,27 @@                       Nothing                       (Just [])                       Nothing+      where+        (errLine, errColumnStart, errColumnEnd) = fromMaybe (0, 0, 0) $+          case words err of+            -- Happy parse error+            (take 9 -> ["syntax", "error", "at", "line", lineStr, "column", columnStr, "before", token]) -> do+              line <- readMaybe (takeWhile isDigit lineStr)+              columnStart <- readMaybe (takeWhile isDigit columnStr)+              return (line - 1, columnStart - 1, columnStart + fromIntegral (length token) - 3)+            -- Happy parse error due to lexer error+            (take 7 -> ["syntax", "error", "at", "line", lineStr, "column", columnStr]) -> do+              line <- readMaybe (takeWhile isDigit lineStr)+              columnStart <- readMaybe (takeWhile isDigit columnStr)+              return (line - 1, columnStart - 1, columnStart - 1)+            -- BNFC layout resolver error+            (take 14 -> ["Layout", "error", "at", "line", _lineStr, "column", _columnStr, "found", token, "at", "line", lineStr', "column", columnStr']) -> do+              -- line <- readMaybe (takeWhile isDigit lineStr)+              -- columnStart <- readMaybe (takeWhile isDigit columnStr)+              line' <- readMaybe (takeWhile isDigit lineStr')+              columnStart' <- readMaybe (takeWhile isDigit columnStr')+              return (line' - 1, columnStart', columnStart' + fromIntegral (length token) - 2)+            _ -> Nothing  instance Default T.Text where def = "" instance Default CompletionItem@@ -220,7 +245,7 @@     declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem]     declsToItems root (path, decls) = map (declToItem root path) decls     declToItem :: FilePath -> FilePath -> Decl' -> CompletionItem-    declToItem rootDir path (Decl name type' _ _ _) = def+    declToItem rootDir path (Decl name type' _ _ _ _loc) = def       & label .~ T.pack (printTree $ getVarIdent name)       & detail ?~ T.pack (show type')       & documentation ?~ InR (MarkupContent MarkupKind_Markdown $ T.pack $@@ -255,7 +280,11 @@         let edits = formatTextEdits (filter (/= '\r') $ T.unpack sourceCode)         return (Right $ map formattingEditToTextEdit edits)     case possibleEdits of+#if MIN_VERSION_lsp(2,7,0)+      Left err    -> res $ Left $ TResponseError (InR ErrorCodes_InternalError) err Nothing+#else       Left err    -> res $ Left $ ResponseError (InR ErrorCodes_InternalError) err Nothing+#endif       Right edits -> do         res $ Right $ InL edits   else do
src/Language/Rzk/VSCode/Tokenize.hs view
@@ -63,6 +63,7 @@   PatternVar _loc var    -> mkToken var SemanticTokenTypes_Parameter [SemanticTokenModifiers_Declaration]   PatternPair _loc l r   -> foldMap tokenizePattern [l, r]   pat@(PatternUnit _loc) -> mkToken pat SemanticTokenTypes_EnumMember [SemanticTokenModifiers_Declaration]+  PatternTuple _loc p1 p2 ps -> foldMap tokenizePattern (p1 : p2 : ps)  tokenizeTope :: Term -> [SemanticTokenAbsolute] tokenizeTope = tokenizeTerm' (Just SemanticTokenTypes_String)@@ -125,8 +126,17 @@         [ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]         , tokenizePattern pat         , foldMap go [a, b] ]+      TypeSigmaTuple loc p ps tN -> concat +        [ mkToken (VarIdent loc "∑") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]+        , foldMap tokenizeSigmaParam (p : ps)+        , go tN ]+      ASCII_TypeSigmaTuple loc p ps tN -> concat +        [ mkToken (VarIdent loc "Sigma") SemanticTokenTypes_Class [SemanticTokenModifiers_DefaultLibrary]+        , foldMap tokenizeSigmaParam (p : ps)+        , go tN ]       TypeId _loc x a y -> foldMap go [x, a, y]       TypeIdSimple _loc x y -> foldMap go [x, y]+                TypeRestricted _loc type_ rs -> concat         [ go type_@@ -139,6 +149,7 @@       ASCII_Lambda loc params body -> go (Lambda loc params body)        Pair _loc l r -> foldMap go [l, r]+      Tuple _loc p1 p2 ps -> foldMap go (p1:p2:ps)       First loc t -> concat         [ mkToken (VarIdent loc "π₁") SemanticTokenTypes_Function [SemanticTokenModifiers_DefaultLibrary]         , go t ]@@ -200,6 +211,11 @@     , tokenizeTerm cube     , tokenizeTope tope     ]++tokenizeSigmaParam :: SigmaParam -> [SemanticTokenAbsolute]+tokenizeSigmaParam (SigmaParam _loc pat type_) = concat +  [ tokenizePattern pat +  , tokenizeTerm type_ ]  mkToken :: (HasPosition a, Print a) => a -> SemanticTokenTypes -> [SemanticTokenModifiers] -> [SemanticTokenAbsolute] mkToken x tokenType tokenModifiers =
src/Rzk/TypeCheck.hs view
@@ -1,10 +1,10 @@ {-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}-{-# LANGUAGE DeriveFoldable       #-}-{-# LANGUAGE DeriveFunctor        #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE LambdaCase           #-}-{-# LANGUAGE OverloadedStrings    #-}-{-# LANGUAGE RecordWildCards      #-}+{-# LANGUAGE DeriveFoldable    #-}+{-# LANGUAGE DeriveFunctor     #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE LambdaCase        #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RecordWildCards   #-} module Rzk.TypeCheck where  import           Control.Applicative      ((<|>))@@ -45,6 +45,7 @@   , declValue        :: Maybe (TermT var)   , declIsAssumption :: Bool   , declUsedVars     :: [var]+  , declLocation     :: Maybe LocationInfo   } deriving Eq  type Decl' = Decl VarIdent@@ -135,7 +136,8 @@           paramDecls <- concat <$> mapM paramToParamDecl params           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)+          loc <- asks location+          let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars) loc           fmap (first (decl :)) $             localDeclPrepared decl $ do               Context{..} <- ask@@ -154,7 +156,8 @@           mapM_ checkDefinedVar (varIdentAt path <$> vars)           paramDecls <- concat <$> mapM paramToParamDecl params           ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT-          let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars)+          loc <- asks location+          let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars) loc           fmap (first (decl :)) $             localDeclPrepared decl $               go (i + 1) moreCommands@@ -191,7 +194,8 @@           <> " Checking #assume " <> intercalate " " [ Rzk.printTree name | name <- names ] ) $ do         withCommand command $ do           ty' <- typecheck (toTerm' ty) universeT-          let decls = [ Decl (varIdentAt path name) ty' Nothing True [] | name <- names ]+          loc <- asks location+          let decls = [ Decl (varIdentAt path name) ty' Nothing True [] loc | name <- names ]           fmap (first (decls <>)) $             localDeclsPrepared decls $               go (i + 1) moreCommands@@ -451,14 +455,17 @@   trace ("Warning: " <> message) $     return () -issueTypeError :: TypeError var -> TypeCheck var a-issueTypeError err = do+fromTypeError :: TypeError var -> TypeCheck var (TypeErrorInScopedContext var)+fromTypeError err = do   context <- ask-  throwError $ PlainTypeError $ TypeErrorInContext+  return $ PlainTypeError $ TypeErrorInContext     { typeErrorError = err     , typeErrorContext = context     } +issueTypeError :: TypeError var -> TypeCheck var a+issueTypeError err = fromTypeError err >>= throwError+ panicImpossible :: String -> a panicImpossible msg = error $ unlines   [ "PANIC! Impossible happened (" <> msg <> ")!"@@ -576,7 +583,7 @@ data LocationInfo = LocationInfo   { locationFilePath :: Maybe FilePath   , locationLine     :: Maybe Int-  }+  } deriving (Eq)  data Verbosity   = Debug@@ -623,6 +630,7 @@   , varOrig                :: Maybe VarIdent   , varIsAssumption        :: Bool -- FIXME: perhaps, introduce something like decl kind?   , varDeclaredAssumptions :: [var]+  , varLocation            :: Maybe LocationInfo   } deriving (Functor, Foldable)  data Context var = Context@@ -700,26 +708,34 @@     (decls, errs) <- sectionBody     localDeclsPrepared decls $       performing (ActionCloseSection name) $ do-        (\ decls' -> (decls', errs)) <$> endSection errs+        result <- (Right <$> endSection errs) `catchError` (return . Left)+        case result of+          Left err              -> return ([], errs <> [err])+          Right (decls', errs') -> return (decls', errs')+        -- (\ decls' -> (decls', errs)) <$> endSection errs  startSection :: Maybe Rzk.SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a startSection name = local $ \Context{..} -> Context   { localScopes = ScopeInfo { scopeName = name, scopeVars = [] } : localScopes   , .. } -endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent [Decl']+endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) endSection errs = askCurrentScope >>= scopeToDecls errs -scopeToDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> ScopeInfo var -> TypeCheck var [Decl var]+scopeToDecls :: Eq var => [TypeErrorInScopedContext var] -> ScopeInfo var -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var]) scopeToDecls errs ScopeInfo{..} = do-  decls <- collectScopeDecls errs [] scopeVars+  (decls, errs') <- collectScopeDecls errs [] scopeVars   -- only issue unused variable errors if there were no errors prior in the section-  when (null errs) $ do-    forM_ decls $ \Decl{..} -> do-      let unusedUsedVars = declUsedVars `intersect` map fst scopeVars-      when (not (null unusedUsedVars)) $-        issueTypeError $ TypeErrorUnusedUsedVariables unusedUsedVars declName-  return decls+  -- when (null errs) $ do+  unusedErrors <- forM decls $ \Decl{..} -> do+    let unusedUsedVars = declUsedVars `intersect` map fst scopeVars+    if null errs && not (null unusedUsedVars)+      then do+        err <- local (\c -> c { location = declLocation }) $+          fromTypeError (TypeErrorUnusedUsedVariables unusedUsedVars declName)+        return [err]+      else return []+  return (decls, errs' <> concat unusedErrors)  insertExplicitAssumptionFor   :: Eq var => var -> (var, VarInfo var) -> TermT var -> TermT var@@ -738,6 +754,7 @@       , varIsAssumption = varIsAssumption       , varOrig = varOrig       , varDeclaredAssumptions = varDeclaredAssumptions+      , varLocation = varLocation       }  makeAssumptionExplicit@@ -776,29 +793,38 @@       , varIsAssumption = varIsAssumption xInfo       , varOrig = varOrig xInfo       , varDeclaredAssumptions = varDeclaredAssumptions xInfo \\ [a]+      , varLocation = varLocation xInfo       }     xs' = map (fmap (insertExplicitAssumptionFor' a (x, xInfo))) xs -collectScopeDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var [Decl var]+collectScopeDecls :: Eq var => [TypeErrorInScopedContext var] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var]) collectScopeDecls errs recentVars (decl@(var, VarInfo{..}) : vars)   | varIsAssumption = do       (used, recentVars') <- makeAssumptionExplicit decl recentVars       -- only issue unused vars error if there were no other errors previously-      when (null errs) $ do-        when (not used) $ do-          issueTypeError $ TypeErrorUnusedVariable var varType-      collectScopeDecls errs recentVars' vars+      -- when (null errs) $ do+      unusedErr <-+        if null errs && not used+          then local (\c -> c { location = varLocation }) $+            pure <$> fromTypeError (TypeErrorUnusedVariable var varType)+          else return []+      collectScopeDecls (errs <> unusedErr) recentVars' vars   | otherwise = do       collectScopeDecls errs (decl : recentVars) vars-collectScopeDecls _ recentVars [] = return (toDecl <$> recentVars)+collectScopeDecls errs recentVars [] = do+  loc <- asks location+  return (toDecl loc <$> recentVars, errs)   where-    toDecl (var, VarInfo{..}) = Decl+    toDecl loc (var, VarInfo{..}) = Decl       { declName = var       , declType = varType       , declValue = varValue       , declIsAssumption = varIsAssumption       , declUsedVars = varDeclaredAssumptions+      , declLocation = updatePosition (varOrig >>= fmap fst . Rzk.hasPosition . fromVarIdent) <$> loc -- FIXME       }+    updatePosition Nothing l       = l+    updatePosition (Just lineNo) l = l { locationLine = Just lineNo }  abstractAssumption :: Eq var => (var, VarInfo var) -> Decl var -> Decl var abstractAssumption (var, VarInfo{..}) Decl{..} = Decl@@ -807,6 +833,7 @@   , declValue = (\body -> lambdaT newDeclType varOrig Nothing (abstract var body)) <$> declValue   , declIsAssumption = declIsAssumption   , declUsedVars = declUsedVars+  , declLocation = declLocation   }   where     newDeclType = typeFunT varOrig varType Nothing (abstract var declType)@@ -923,13 +950,13 @@ localDeclsPrepared (decl : decls) = localDeclPrepared decl . localDeclsPrepared decls  localDecl :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a-localDecl (Decl x ty term isAssumption vars) tc = do+localDecl (Decl x ty term isAssumption vars loc) tc = do   ty' <- whnfT ty   term' <- traverse whnfT term-  localDeclPrepared (Decl x ty' term' isAssumption vars) tc+  localDeclPrepared (Decl x ty' term' isAssumption vars loc) tc  localDeclPrepared :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a-localDeclPrepared (Decl x ty term isAssumption vars) tc = do+localDeclPrepared (Decl x ty term isAssumption vars loc) tc = do   checkTopLevelDuplicate x   local update tc   where@@ -939,6 +966,7 @@       , varOrig = Just x       , varIsAssumption = isAssumption       , varDeclaredAssumptions = vars+      , varLocation = loc       }  type TypeCheck var = ReaderT (Context var) (Except (TypeErrorInScopedContext var))@@ -1302,15 +1330,16 @@       switch Contravariant = Covariant  enterScopeContext :: Maybe VarIdent -> TermT var -> Context var -> Context (Inc var)-enterScopeContext orig ty =+enterScopeContext orig ty context =   addVarInCurrentScope Z VarInfo     { varType   = S <$> ty     , varValue  = Nothing     , varOrig   = orig     , varIsAssumption = False     , varDeclaredAssumptions = []+    , varLocation = location context     }-  . fmap S+    (S <$> context)  enterScope :: Maybe VarIdent -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b enterScope orig ty action = do@@ -1774,7 +1803,7 @@               []   -> nfT type_               rs'' -> TypeRestrictedT ty <$> nfT type_ <*> pure rs'' -checkDefinedVar :: Eq var => var -> TypeCheck var ()+checkDefinedVar :: VarIdent -> TypeCheck VarIdent () checkDefinedVar x = asks (lookup x . varInfos) >>= \case   Nothing  -> issueTypeError $ TypeErrorUndefined x   Just _ty -> return ()