Skip to content

Commit

Permalink
Merge pull request #3460 from unisonweb/cp/typechecked-auto-fmt
Browse files Browse the repository at this point in the history
LSP Format support
  • Loading branch information
mergify[bot] authored Jan 22, 2024
2 parents 57881fd + a788762 commit e7df7ce
Show file tree
Hide file tree
Showing 40 changed files with 799 additions and 252 deletions.
2 changes: 1 addition & 1 deletion codebase2/util-serialization/U/Util/Serialization.hs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@
module U.Util.Serialization where

import Control.Applicative (Applicative (liftA2), liftA3)
import Control.Monad (foldM, replicateM, when, replicateM_)
import Control.Monad (foldM, replicateM, replicateM_, when)
import Data.Bits (Bits, clearBit, setBit, shiftL, shiftR, testBit, (.|.))
import Data.ByteString (ByteString, readFile, writeFile)
import qualified Data.ByteString as BS
Expand Down
18 changes: 18 additions & 0 deletions docs/language-server.markdown
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,19 @@

[![asciicast](https://asciinema.org/a/Kwa7NscffA3R8KCHxq1OavRm0.svg)](https://asciinema.org/a/Kwa7NscffA3R8KCHxq1OavRm0)

* [Overview](#overview)
* [Installation and setup](#installation-and-setup)
* [Settings](#settings)
* [NeoVim](#neovim)
* [VSCode](#vscode)

## Overview

Supported features:

* Autocompletion
* Inline type and parser error messages
* Format on save (you can disable this in your editor if you like)
* Show type on hover

Notes:
Expand All @@ -34,6 +41,17 @@ You can set this persistently in powershell using:

See [this issue](https://github.com/unisonweb/unison/issues/3487) for more details.

### Settings

Supported settings and their defaults. See information for your language server client about where to provide these.

```json
{
// A suggestion for the formatter about how wide (in columns) to print definitions.
"formattingWidth": 80
}
```

### NeoVim

Before configuring the LSP, install the Vim plugin for filetype detection and syntax highlighting.
Expand Down
1 change: 0 additions & 1 deletion lib/unison-util-relation/src/Unison/Util/BiMultimap.hs
Original file line number Diff line number Diff line change
Expand Up @@ -243,4 +243,3 @@ deriveRangeFromDomain :: Ord b => a -> NESet b -> Map b a -> Map b a
deriveRangeFromDomain x ys acc =
foldr (flip Map.insert x) acc ys
{-# INLINE deriveRangeFromDomain #-}

1 change: 1 addition & 0 deletions parser-typechecker/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ dependencies:
- http-client
- http-media
- http-types
- IntervalMap
- lens
- lucid
- megaparsec
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ hashFieldAccessors ::
)
hashFieldAccessors ppe declName vars declRef dd = do
let accessors :: [(v, (), Term.Term v ())]
accessors = DD.generateRecordAccessors (map (,()) vars) declName declRef
accessors = DD.generateRecordAccessors mempty (map (,()) vars) declName declRef
let typeLookup :: TypeLookup v ()
typeLookup =
TypeLookup
Expand Down
3 changes: 1 addition & 2 deletions parser-typechecker/src/Unison/KindInference.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@
-- Afterwards, the 'SolveState' holds the kinds of all decls and we
-- can check that type annotations in terms that may mention the
-- decls are well-kinded with 'kindCheckAnnotations'.

module Unison.KindInference
( inferDecls,
kindCheckAnnotations,
Expand All @@ -28,7 +27,7 @@ import Data.Map.Strict qualified as Map
import Unison.Codebase.BuiltinAnnotation (BuiltinAnnotation)
import Unison.DataDeclaration
import Unison.KindInference.Generate (declComponentConstraints, termConstraints)
import Unison.KindInference.Solve (KindError, verify, initialState, step, defaultUnconstrainedVars)
import Unison.KindInference.Solve (KindError, defaultUnconstrainedVars, initialState, step, verify)
import Unison.KindInference.Solve.Monad (Env (..), SolveState, run, runGen)
import Unison.Prelude
import Unison.PrettyPrintEnv qualified as PrettyPrintEnv
Expand Down
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
module Unison.KindInference.Constraint.Context
( ConstraintContext(..)
) where
( ConstraintContext (..),
)
where

import Unison.KindInference.UVar (UVar)
import Unison.Type (Type)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ module Unison.KindInference.Constraint.Unsolved
)
where

import Control.Lens (Traversal, Lens, Lens')
import Control.Lens (Lens, Lens', Traversal)
import Unison.KindInference.Constraint.Provenance (Provenance)
import Unison.KindInference.Constraint.Provenance qualified as Provenance

Expand Down
67 changes: 34 additions & 33 deletions parser-typechecker/src/Unison/KindInference/Generate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import Unison.KindInference.Constraint.Context (ConstraintContext (..))
import Unison.KindInference.Constraint.Provenance (Provenance (..))
import Unison.KindInference.Constraint.Provenance qualified as Provenance
import Unison.KindInference.Constraint.Unsolved (Constraint (..))
import Unison.KindInference.Generate.Monad (Gen, GeneratedConstraint, freshVar, pushType, lookupType, scopedType)
import Unison.KindInference.Generate.Monad (Gen, GeneratedConstraint, freshVar, lookupType, pushType, scopedType)
import Unison.KindInference.UVar (UVar)
import Unison.Prelude
import Unison.Reference (Reference)
Expand Down Expand Up @@ -241,41 +241,42 @@ declComponentConstraintTree decls = do
-- Add a kind variable for every datatype
declKind <- pushType (Type.ref (DD.annotation $ asDataDecl decl) ref)
pure (ref, decl, declKind)
(declConstraints, constructorConstraints) <- unzip <$> for decls \(ref, decl, declKind) -> do
let declAnn = DD.annotation $ asDataDecl decl
let declType = Type.ref declAnn ref
-- Unify the datatype with @k_1 -> ... -> k_n -> *@ where @n@ is
-- the number of type parameters
let tyVars = map (\tyVar -> Type.var declAnn tyVar) (DD.bound $ asDataDecl decl)
tyvarKinds <- for tyVars \tyVar -> do
-- it would be nice to annotate these type vars with their
-- precise location, but that information doesn't seem to be
-- available via "DataDeclaration", so we currently settle for
-- the whole decl annotation.
k <- freshVar tyVar
pure (k, tyVar)
(declConstraints, constructorConstraints) <-
unzip <$> for decls \(ref, decl, declKind) -> do
let declAnn = DD.annotation $ asDataDecl decl
let declType = Type.ref declAnn ref
-- Unify the datatype with @k_1 -> ... -> k_n -> *@ where @n@ is
-- the number of type parameters
let tyVars = map (\tyVar -> Type.var declAnn tyVar) (DD.bound $ asDataDecl decl)
tyvarKinds <- for tyVars \tyVar -> do
-- it would be nice to annotate these type vars with their
-- precise location, but that information doesn't seem to be
-- available via "DataDeclaration", so we currently settle for
-- the whole decl annotation.
k <- freshVar tyVar
pure (k, tyVar)

let tyvarKindsOnly = map fst tyvarKinds
constructorConstraints <-
Node <$> for (DD.constructors' $ asDataDecl decl) \(constructorAnn, _, constructorType) -> do
withInstantiatedConstructorType declType tyvarKindsOnly constructorType \constructorType -> do
constructorKind <- freshVar constructorType
ct <- typeConstraintTree constructorKind constructorType
pure $ ParentConstraint (IsType constructorKind (Provenance DeclDefinition constructorAnn)) ct
let tyvarKindsOnly = map fst tyvarKinds
constructorConstraints <-
Node <$> for (DD.constructors' $ asDataDecl decl) \(constructorAnn, _, constructorType) -> do
withInstantiatedConstructorType declType tyvarKindsOnly constructorType \constructorType -> do
constructorKind <- freshVar constructorType
ct <- typeConstraintTree constructorKind constructorType
pure $ ParentConstraint (IsType constructorKind (Provenance DeclDefinition constructorAnn)) ct

(fullyAppliedKind, _fullyAppliedType, declConstraints) <-
let phi (dk, dt, cts) (ak, at) = do
-- introduce a kind uvar for each app node
let t' = Type.app declAnn dt at
v <- freshVar t'
let cts' = Constraint (IsArr dk (Provenance DeclDefinition declAnn) ak v) cts
pure (v, t', cts')
in foldlM phi (declKind, declType, Node []) tyvarKinds
(fullyAppliedKind, _fullyAppliedType, declConstraints) <-
let phi (dk, dt, cts) (ak, at) = do
-- introduce a kind uvar for each app node
let t' = Type.app declAnn dt at
v <- freshVar t'
let cts' = Constraint (IsArr dk (Provenance DeclDefinition declAnn) ak v) cts
pure (v, t', cts')
in foldlM phi (declKind, declType, Node []) tyvarKinds

let finalDeclConstraints = case decl of
Left _effectDecl -> Constraint (IsAbility fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints
Right _dataDecl -> Constraint (IsType fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints
pure (finalDeclConstraints, constructorConstraints)
let finalDeclConstraints = case decl of
Left _effectDecl -> Constraint (IsAbility fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints
Right _dataDecl -> Constraint (IsType fullyAppliedKind (Provenance DeclDefinition declAnn)) declConstraints
pure (finalDeclConstraints, constructorConstraints)
pure (Node declConstraints `StrictOrder` Node constructorConstraints)

-- | This is a helper to unify the kind constraints on type variables
Expand Down
6 changes: 3 additions & 3 deletions parser-typechecker/src/Unison/KindInference/Solve.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module Unison.KindInference.Solve
)
where

import Unison.KindInference.Error (KindError(..), ConstraintConflict(..), improveError)
import Control.Lens (Prism', prism', review, (%~))
import Control.Monad.Reader (asks)
import Control.Monad.Reader qualified as M
Expand All @@ -22,6 +21,7 @@ import Unison.KindInference.Constraint.Provenance (Provenance (..))
import Unison.KindInference.Constraint.Solved qualified as Solved
import Unison.KindInference.Constraint.StarProvenance (StarProvenance (..))
import Unison.KindInference.Constraint.Unsolved qualified as Unsolved
import Unison.KindInference.Error (ConstraintConflict (..), KindError (..), improveError)
import Unison.KindInference.Generate (builtinConstraints)
import Unison.KindInference.Generate.Monad (Gen (..), GeneratedConstraint)
import Unison.KindInference.Solve.Monad
Expand Down Expand Up @@ -123,9 +123,9 @@ markVisiting x = do
OccCheckState {visitingSet, visitingStack} <- M.get
case Set.member x visitingSet of
True -> do
OccCheckState{solvedConstraints} <- M.get
OccCheckState {solvedConstraints} <- M.get
let loc = case U.lookupCanon x solvedConstraints of
Just (_, _, Descriptor { descriptorConstraint = Just (Solved.IsArr (Provenance _ loc) _ _ )}, _) -> loc
Just (_, _, Descriptor {descriptorConstraint = Just (Solved.IsArr (Provenance _ loc) _ _)}, _) -> loc
_ -> error "cycle without IsArr constraint"
addError (CycleDetected loc x solvedConstraints)
pure Cycle
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -718,7 +718,7 @@ union v0 v1 nc@NormalizedConstraints {constraintMap} =
IsEffectful -> [C.Effectful chosenCanon]
in addConstraints constraints nc {constraintMap = m}
where
noMerge m = pure nc { constraintMap = m }
noMerge m = pure nc {constraintMap = m}

modifyListC ::
forall vt v loc m.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ module Unison.PatternMatchCoverage.UFMap
)
where

import Control.Monad.Trans.Class
import Control.Monad.Fix (MonadFix)
import Control.Monad.Trans.Class
import Control.Monad.Trans.Except (ExceptT (..))
import Data.Foldable (foldl')
import Data.Functor ((<&>))
Expand Down
8 changes: 5 additions & 3 deletions parser-typechecker/src/Unison/PrintError.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1220,16 +1220,18 @@ rangeToEnglish (Range (L.Pos l c) (L.Pos l' c')) =
then "line " ++ show l
else "lines " ++ show l ++ "" ++ show l'

annotatedToEnglish :: (Annotated a, IsString s) => a -> s
annotatedToEnglish :: (Annotated a, IsString s, Semigroup s) => a -> s
annotatedToEnglish a = case ann a of
Intrinsic -> "an intrinsic"
External -> "an external"
Intrinsic -> "<intrinsic>"
External -> "<external>"
GeneratedFrom a -> "generated from: " <> annotatedToEnglish a
Ann start end -> rangeToEnglish $ Range start end

rangeForAnnotated :: (Annotated a) => a -> Maybe Range
rangeForAnnotated a = case ann a of
Intrinsic -> Nothing
External -> Nothing
GeneratedFrom a -> rangeForAnnotated a
Ann start end -> Just $ Range start end

showLexerOutput :: Bool
Expand Down
42 changes: 27 additions & 15 deletions parser-typechecker/src/Unison/Syntax/DeclParser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ where

import Control.Lens
import Control.Monad.Reader (MonadReader (..))
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map qualified as Map
import Text.Megaparsec qualified as P
import Unison.ABT qualified as ABT
Expand Down Expand Up @@ -140,7 +141,7 @@ dataDeclaration ::
Maybe (L.Token UnresolvedModifier) ->
P v m (v, DataDeclaration v Ann, Accessors v)
dataDeclaration maybeUnresolvedModifier = do
_ <- fmap void (reserved "type") <|> openBlockWith "type"
typeToken <- fmap void (reserved "type") <|> openBlockWith "type"
(name, typeArgs) <-
(,)
<$> TermParser.verifyRelativeVarName prefixDefinitionName
Expand All @@ -166,7 +167,7 @@ dataDeclaration maybeUnresolvedModifier = do
prefixVar = TermParser.verifyRelativeVarName prefixDefinitionName
dataConstructor :: P v m (Ann, v, Type v Ann)
dataConstructor = go <$> prefixVar <*> many TypeParser.valueTypeLeaf
record :: P v m ([(Ann, v, Type v Ann)], [(L.Token v, [(L.Token v, Type v Ann)])])
record :: P v m ([(Ann, v, Type v Ann)], [(L.Token v, [(L.Token v, Type v Ann)])], Ann)
record = do
_ <- openBlockWith "{"
let field :: P v m [(L.Token v, Type v Ann)]
Expand All @@ -178,29 +179,35 @@ dataDeclaration maybeUnresolvedModifier = do
Just _ -> maybe [f] (f :) <$> (optional semi *> optional field)
)
fields <- field
_ <- closeBlock
closingToken <- closeBlock
let lastSegment = name <&> (\v -> Var.named (Name.toText $ Name.unqualified (Name.unsafeFromVar v)))
pure ([go lastSegment (snd <$> fields)], [(name, fields)])
(constructors, accessors) <-
msum [record, (,[]) <$> sepBy (reserved "|") dataConstructor]
pure ([go lastSegment (snd <$> fields)], [(name, fields)], ann closingToken)
(constructors, accessors, closingAnn) <-
msum [Left <$> record, Right <$> sepBy (reserved "|") dataConstructor] <&> \case
Left (constructors, accessors, closingAnn) -> (constructors, accessors, closingAnn)
Right constructors ->
let closingAnn :: Ann
closingAnn = NonEmpty.last (ann eq NonEmpty.:| ((\(_, _, t) -> ann t) <$> constructors))
in (constructors, [], closingAnn)
_ <- closeBlock
let -- the annotation of the last constructor if present,
-- otherwise ann of name
closingAnn :: Ann
closingAnn = last (ann eq : ((\(_, _, t) -> ann t) <$> constructors))
case maybeUnresolvedModifier of
Nothing -> do
modifier <- defaultUniqueModifier (L.payload name)
-- ann spanning the whole Decl.
let declSpanAnn = ann typeToken <> closingAnn
pure
( L.payload name,
DD.mkDataDecl' modifier closingAnn typeArgVs constructors,
DD.mkDataDecl' modifier declSpanAnn typeArgVs constructors,
accessors
)
Just unresolvedModifier -> do
modifier <- resolveUnresolvedModifier unresolvedModifier (L.payload name)
-- ann spanning the whole Decl.
-- Technically the typeToken is redundant here, but this is more future proof.
let declSpanAnn = ann typeToken <> ann modifier <> closingAnn
pure
( L.payload name,
DD.mkDataDecl' (L.payload modifier) (ann modifier <> closingAnn) typeArgVs constructors,
DD.mkDataDecl' (L.payload modifier) declSpanAnn typeArgVs constructors,
accessors
)

Expand All @@ -210,7 +217,7 @@ effectDeclaration ::
Maybe (L.Token UnresolvedModifier) ->
P v m (v, EffectDeclaration v Ann)
effectDeclaration maybeUnresolvedModifier = do
_ <- fmap void (reserved "ability") <|> openBlockWith "ability"
abilityToken <- fmap void (reserved "ability") <|> openBlockWith "ability"
name <- TermParser.verifyRelativeVarName prefixDefinitionName
typeArgs <- many (TermParser.verifyRelativeVarName prefixDefinitionName)
let typeArgVs = L.payload <$> typeArgs
Expand All @@ -224,17 +231,22 @@ effectDeclaration maybeUnresolvedModifier = do
case maybeUnresolvedModifier of
Nothing -> do
modifier <- defaultUniqueModifier (L.payload name)
-- ann spanning the whole ability declaration.
let abilitySpanAnn = ann abilityToken <> closingAnn
pure
( L.payload name,
DD.mkEffectDecl' modifier closingAnn typeArgVs constructors
DD.mkEffectDecl' modifier abilitySpanAnn typeArgVs constructors
)
Just unresolvedModifier -> do
modifier <- resolveUnresolvedModifier unresolvedModifier (L.payload name)
-- ann spanning the whole ability declaration.
-- Technically the abilityToken is redundant here, but this is more future proof.
let abilitySpanAnn = ann abilityToken <> ann modifier <> closingAnn
pure
( L.payload name,
DD.mkEffectDecl'
(L.payload modifier)
(ann modifier <> closingAnn)
abilitySpanAnn
typeArgVs
constructors
)
Expand Down
8 changes: 5 additions & 3 deletions parser-typechecker/src/Unison/Syntax/FileParser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ import Unison.Names qualified as Names
import Unison.Names.ResolutionResult qualified as Names
import Unison.NamesWithHistory qualified as Names
import Unison.Parser.Ann (Ann)
import Unison.Parser.Ann qualified as Ann
import Unison.Prelude
import Unison.Syntax.DeclParser (declarations)
import Unison.Syntax.Lexer qualified as L
Expand Down Expand Up @@ -48,7 +49,7 @@ file = do
Left es -> resolutionFailures (toList es)
let accessors :: [[(v, Ann, Term v Ann)]]
accessors =
[ DD.generateRecordAccessors (toPair <$> fields) (L.payload typ) r
[ DD.generateRecordAccessors Ann.GeneratedFrom (toPair <$> fields) (L.payload typ) r
| (typ, fields) <- parsedAccessors,
Just (r, _) <- [Map.lookup (L.payload typ) (UF.datas env)]
]
Expand Down Expand Up @@ -194,9 +195,10 @@ stanza = watchExpression <|> unexpectedAction <|> binding
(kind, guid, ann) <- watched
_ <- guardEmptyWatch ann
msum
[ WatchBinding kind ann <$> TermParser.binding,
WatchExpression kind guid ann <$> TermParser.blockTerm
[ TermParser.binding <&> (\trm@(((trmSpanAnn, _), _)) -> WatchBinding kind (ann <> trmSpanAnn) trm),
TermParser.blockTerm <&> (\trm -> WatchExpression kind guid (ann <> ABT.annotation trm) trm)
]

guardEmptyWatch ann =
P.try $ do
op <- optional (L.payload <$> P.lookAhead closeBlock)
Expand Down
Loading

0 comments on commit e7df7ce

Please sign in to comment.