diff --git a/jl4-core/src/L4/API.hs b/jl4-core/src/L4/API.hs index cfb56150d..dc0ce83bd 100644 --- a/jl4-core/src/L4/API.hs +++ b/jl4-core/src/L4/API.hs @@ -41,7 +41,7 @@ import L4.Annotation (HasSrcRange(..), rangeOfNode) import L4.Parser.SrcSpan (SrcRange(..), SrcPos(..)) import L4.TypeCheck (severity, prettyCheckErrorWithContext, applyFinalSubstitution) import L4.TypeCheck.Types (CheckResult(..), CheckErrorWithContext(..), Severity(..), Substitution) -import L4.Print (prettyLayout) +import L4.Print (prettyLayout, prettyLayoutNF, ConstructorFieldNames, extractConstructorFieldNames) import L4.Syntax (Info(..), Type'(..), Resolved, OptionallyNamedType(..), TopDecl(..), Directive(..), Module(..), Section(..)) import L4.Annotation (emptyAnno) import qualified L4.Utils.IntervalMap as IV @@ -247,9 +247,10 @@ l4Eval source = -- Now evaluate the main module with the combined import environment (_env, results) <- EL.execEvalModuleWithEnv evalConfig result.tcdEntityInfo importEnv result.tcdModule + let conFields = extractConstructorFieldNames result.tcdEntityInfo pure $ encodeJson $ Aeson.object [ "success" .= True - , "results" .= Vector.fromList (map evalResultToJson results) + , "results" .= Vector.fromList (map (evalResultToJson conFields) results) ] -- | Evaluate a specific directive at a given source position. @@ -278,7 +279,8 @@ l4EvalDirective source line col directiveType = evalConfig <- EL.resolveEvalConfigWithSafeMode Nothing (lspDefaultPolicy defaultGraphVizOptions) True importEnv <- evaluateImports evalConfig result.tcdResolvedImports (_env, results) <- EL.execEvalModuleWithEnv evalConfig result.tcdEntityInfo importEnv result.tcdModule - let targetPos = MkSrcPos line col + let conFields = extractConstructorFieldNames result.tcdEntityInfo + targetPos = MkSrcPos line col matchesPos (EL.MkEvalDirectiveResult rng _ _) = fmap (.start) rng == Just targetPos matchingResult = List.find matchesPos results case matchingResult of @@ -288,14 +290,14 @@ l4EvalDirective source line col directiveType = Just (EL.MkEvalDirectiveResult _range res _mtrace) -> pure $ encodeJson $ Aeson.object [ "directiveType" .= directiveType - , "prettyText" .= prettyEvalResult res + , "prettyText" .= prettyEvalResult conFields res , "success" .= case res of EL.Assertion b -> Aeson.toJSON b EL.Reduction _ -> Aeson.Null , "structuredValue" .= case res of EL.Assertion b -> Aeson.toJSON b EL.Reduction (Left _) -> Aeson.Null - EL.Reduction (Right nf) -> Aeson.toJSON (prettyLayout nf) + EL.Reduction (Right nf) -> Aeson.toJSON (prettyLayoutNF conFields nf) ] -- | Evaluate a list of resolved imports and combine their environments. @@ -506,9 +508,9 @@ typeFunction n | n > 0 = typeFunction _ = error "Internal error: negative arity of type constructor" -- | Convert an evaluation result to JSON. -evalResultToJson :: EL.EvalDirectiveResult -> Aeson.Value -evalResultToJson edr = Aeson.object $ - [ "result" .= prettyEvalResult edr.result +evalResultToJson :: ConstructorFieldNames -> EL.EvalDirectiveResult -> Aeson.Value +evalResultToJson fields edr = Aeson.object $ + [ "result" .= prettyEvalResult fields edr.result , "success" .= isSuccess edr.result ] ++ case edr.range of @@ -520,11 +522,11 @@ evalResultToJson edr = Aeson.object $ isSuccess (EL.Reduction (Left _)) = False -- | Pretty print an evaluation directive result value. -prettyEvalResult :: EL.EvalDirectiveValue -> Text -prettyEvalResult (EL.Assertion True) = "assertion satisfied" -prettyEvalResult (EL.Assertion False) = "assertion failed" -prettyEvalResult (EL.Reduction (Left exc)) = Text.unlines (prettyEvalException exc) -prettyEvalResult (EL.Reduction (Right v)) = prettyLayout v +prettyEvalResult :: ConstructorFieldNames -> EL.EvalDirectiveValue -> Text +prettyEvalResult _fields (EL.Assertion True) = "assertion satisfied" +prettyEvalResult _fields (EL.Assertion False) = "assertion failed" +prettyEvalResult _fields (EL.Reduction (Left exc)) = Text.unlines (prettyEvalException exc) +prettyEvalResult fields (EL.Reduction (Right v)) = prettyLayoutNF fields v -- | Generate ladder diagram visualization data for a specific DECIDE rule by name. -- diff --git a/jl4-core/src/L4/EvaluateLazy.hs b/jl4-core/src/L4/EvaluateLazy.hs index fe5b3c756..21734a419 100644 --- a/jl4-core/src/L4/EvaluateLazy.hs +++ b/jl4-core/src/L4/EvaluateLazy.hs @@ -16,6 +16,7 @@ module L4.EvaluateLazy , execEvalExprInContextOfModule , prettyEvalException , prettyEvalDirectiveResult +, prettyEvalDirectiveResultWithFields ) where @@ -364,6 +365,21 @@ prettyEvalDirectiveResult (MkEvalDirectiveResult _range res mtrace) = Nothing -> Text.empty Just t -> "\n─────\n" <> prettyLayout t +-- | Like 'prettyEvalDirectiveResult' but uses named-field syntax (WITH / IS) +-- for constructors whose field names are provided. +prettyEvalDirectiveResultWithFields :: ConstructorFieldNames -> EvalDirectiveResult -> Text +prettyEvalDirectiveResultWithFields fields (MkEvalDirectiveResult _range res mtrace) = + prettyEvalDirectiveValueWithFields fields res + <> case mtrace of + Nothing -> Text.empty + Just t -> "\n─────\n" <> prettyLayout t + +prettyEvalDirectiveValueWithFields :: ConstructorFieldNames -> EvalDirectiveValue -> Text +prettyEvalDirectiveValueWithFields _fields (Assertion True) = "assertion satisfied" +prettyEvalDirectiveValueWithFields _fields (Assertion False) = "assertion failed" +prettyEvalDirectiveValueWithFields _fields (Reduction (Left exc)) = Text.unlines (prettyEvalException exc) +prettyEvalDirectiveValueWithFields fields (Reduction (Right v)) = prettyLayoutNF fields v + -- | Evaluate WHNF to NF, with a cutoff (which possibly could be made configurable). nf :: WHNF -> Eval NF nf = nfAux maximumStackSize diff --git a/jl4-core/src/L4/Print.hs b/jl4-core/src/L4/Print.hs index e0505abd7..73db684aa 100644 --- a/jl4-core/src/L4/Print.hs +++ b/jl4-core/src/L4/Print.hs @@ -1,9 +1,11 @@ module L4.Print where import Base +import qualified Base.Map as Map import qualified Base.Text as Text import L4.Evaluate.ValueLazy as Lazy import L4.Syntax +import qualified L4.TypeCheck.Types as TC import Data.Char import Data.Time (UTCTime, toGregorian) @@ -28,6 +30,35 @@ prettyLayout a = docText $ printWithLayout a docText :: Doc ann -> Text docText = renderStrict . layoutPretty (LayoutOptions Unbounded) +-- | A map from constructor 'Unique' to its field names (in order). +-- Used for pretty-printing constructor values with named fields. +type ConstructorFieldNames = Map Unique [Text] + +-- | Build a 'ConstructorFieldNames' map from type-checker 'EntityInfo'. +-- For each constructor, extracts the parameter names from its function type. +extractConstructorFieldNames :: TC.EntityInfo -> ConstructorFieldNames +extractConstructorFieldNames ei = Map.fromList + [ (u, names) + | (u, (_name, TC.KnownTerm ty Constructor)) <- Map.toList ei + , let names = fieldNamesFromType ty + , not (null names) + ] + where + fieldNamesFromType :: Type' Resolved -> [Text] + fieldNamesFromType (Fun _ params _) = mapMaybe paramName params + fieldNamesFromType (Forall _ _ inner) = fieldNamesFromType inner + fieldNamesFromType _ = [] + + paramName :: OptionallyNamedType Resolved -> Maybe Text + paramName (MkOptionallyNamedType _ (Just n) _) = Just (resolvedToText n) + paramName _ = Nothing + + resolvedToText :: Resolved -> Text + resolvedToText r = case rawName (getActual r) of + NormalName t -> t + QualifiedName _ t -> t + PreDef t -> t + -- | Hack to get the lines of a document as 'Doc'. Used for the trace printer -- and in situations where we need to prefix all the lines with something else. -- @@ -506,6 +537,65 @@ instance LayoutPrinter a => LayoutPrinter (Lazy.Value a) where Lazy.ValConstructor r [] -> printWithLayout r _ -> surround (printWithLayout v) "(" ")" +-- | Pretty-print an 'NF' value, using named fields (WITH / IS syntax) for +-- constructors whose field names are provided in the map. +prettyNFWithConstructorFields :: ConstructorFieldNames -> Lazy.NF -> Doc ann +prettyNFWithConstructorFields fields = goNF + where + goNF :: Lazy.NF -> Doc ann + goNF (Lazy.MkNF v) = goVal v + goNF Lazy.Omitted = "…" + + goVal :: Lazy.Value Lazy.NF -> Doc ann + goVal = \case + Lazy.ValConstructor r vs + | Just names <- Map.lookup (getUnique r) fields + , length names == length vs + , not (null vs) + -> printWithLayout r <+> "WITH" + <+> hsep (punctuate comma (zipWith fieldPair names vs)) + -- For everything else, delegate to the standard LayoutPrinter, + -- but recurse into nested NF values with field-name awareness. + Lazy.ValCons hd tl -> + "LIST" <+> goList hd tl + Lazy.ValConstructor r vs -> printWithLayout r <> case vs of + [] -> mempty + vals@(_:_) -> space <> "OF" <+> hsep (punctuate comma (fmap goNFParens vals)) + other -> printWithLayout other + + fieldPair :: Text -> Lazy.NF -> Doc ann + fieldPair name val = pretty (quoteIfNeeded name) <+> "IS" <+> goNF val + + goList :: Lazy.NF -> Lazy.NF -> Doc ann + goList v1 (Lazy.MkNF Lazy.ValNil) = goNF v1 + goList v1 (Lazy.MkNF (Lazy.ValCons v2 v3)) = goNF v1 <> comma <+> goList v2 v3 + goList Lazy.Omitted Lazy.Omitted = "..." + goList v1 Lazy.Omitted = goNF v1 <> comma <+> "..." + goList v1 v = goNF v1 <> comma <+> goNF v + + goNFParens :: Lazy.NF -> Doc ann + goNFParens nf = case nf of + Lazy.MkNF v -> goValParens v + Lazy.Omitted -> "…" + + goValParens :: Lazy.Value Lazy.NF -> Doc ann + goValParens v = case v of + Lazy.ValNumber{} -> goVal v + Lazy.ValString{} -> goVal v + Lazy.ValDate{} -> goVal v + Lazy.ValTime{} -> goVal v + Lazy.ValDateTime{} -> goVal v + Lazy.ValNil -> "EMPTY" + Lazy.ValClosure{} -> goVal v + Lazy.ValUnappliedConstructor{} -> goVal v + Lazy.ValAssumed{} -> goVal v + Lazy.ValConstructor _ [] -> goVal v + _ -> surround (goVal v) "(" ")" + +-- | Pretty-print an 'NF' to 'Text', using named fields when available. +prettyLayoutNF :: ConstructorFieldNames -> Lazy.NF -> Text +prettyLayoutNF fields nf = docText $ prettyNFWithConstructorFields fields nf + instance LayoutPrinter BinOp where printWithLayout = \ case BinOpPlus -> "PLUS" diff --git a/jl4-lsp/app/LSP/L4/Handlers.hs b/jl4-lsp/app/LSP/L4/Handlers.hs index cd09a1aea..bbd999ae2 100644 --- a/jl4-lsp/app/LSP/L4/Handlers.hs +++ b/jl4-lsp/app/LSP/L4/Handlers.hs @@ -184,7 +184,8 @@ scheduleDirectiveResultsNotification ide doc nuri = do in if lineNo > 0 && lineNo <= length ls then ls !! (lineNo - 1) else "" - evalUpdates = Maybe.mapMaybe (Inspector.evalDirectiveToUpdateItem getLineContent) evalResults + conFields = maybe mempty (extractConstructorFieldNames . (.entityInfo)) mTcResult + evalUpdates = Maybe.mapMaybe (Inspector.evalDirectiveToUpdateItem conFields getLineContent) evalResults checkUpdates = [ Inspector.DirectiveUpdateItem { directiveId = Text.pack (show lineNo) <> ":" <> Text.pack (show colNo) @@ -504,8 +505,10 @@ handlers evalConfig recorder = let nuri = toNormalizedUri reqParams.verDocId._uri targetPos = reqParams.srcPos - mResults <- liftIO $ runAction "l4/evalDirectiveResult" ide $ - use EvaluateLazy nuri + (mResults, mTcResult') <- liftIO $ runAction "l4/evalDirectiveResult" ide $ do + mEval <- use EvaluateLazy nuri + mTc <- use SuccessfulTypeCheck nuri + pure (mEval, mTc) case mResults of Nothing -> pure $ Left $ TResponseError @@ -514,12 +517,13 @@ handlers evalConfig recorder = , _xdata = Nothing } Just results -> do - let matchesPos (EL.MkEvalDirectiveResult rng _ _) = fmap (.start) rng == Just targetPos + let conFields = maybe mempty (extractConstructorFieldNames . (.entityInfo)) mTcResult' + matchesPos (EL.MkEvalDirectiveResult rng _ _) = fmap (.start) rng == Just targetPos matchingResult = List.find matchesPos results case matchingResult of Just evalRes -> pure $ Right $ Aeson.toJSON $ - Inspector.evalDirectiveToResult reqParams.directiveType evalRes + Inspector.evalDirectiveToResult conFields reqParams.directiveType evalRes Nothing | reqParams.directiveType == "#CHECK" -> do -- #CHECK results come from the type checker (CheckInfo), not the evaluator. -- Look for a CheckInfo item on the same line as the target position. diff --git a/jl4-lsp/src/LSP/L4/Inspector.hs b/jl4-lsp/src/LSP/L4/Inspector.hs index f39ce4fc8..daa54db8f 100644 --- a/jl4-lsp/src/LSP/L4/Inspector.hs +++ b/jl4-lsp/src/LSP/L4/Inspector.hs @@ -18,7 +18,7 @@ import Data.Ratio (numerator, denominator) import GHC.TypeLits (Symbol) import Language.LSP.Protocol.Types as LSP import L4.Parser.SrcSpan (SrcPos(..), SrcRange(..)) -import L4.Print (prettyLayout) +import L4.Print (prettyLayout, ConstructorFieldNames) import L4.Syntax (getActual) import qualified L4.EvaluateLazy as EL @@ -96,11 +96,11 @@ instance FromJSON DirectiveResult where -- Converting EvalDirectiveResult to DirectiveResult ------------------------------------------------------ -evalDirectiveToResult :: Text -> EL.EvalDirectiveResult -> DirectiveResult -evalDirectiveToResult dirType (EL.MkEvalDirectiveResult _range res mtrace) = +evalDirectiveToResult :: ConstructorFieldNames -> Text -> EL.EvalDirectiveResult -> DirectiveResult +evalDirectiveToResult fields dirType (EL.MkEvalDirectiveResult _range res mtrace) = DirectiveResult { directiveType = dirType - , prettyText = EL.prettyEvalDirectiveResult (EL.MkEvalDirectiveResult _range res mtrace) + , prettyText = EL.prettyEvalDirectiveResultWithFields fields (EL.MkEvalDirectiveResult _range res mtrace) , success = case res of EL.Assertion b -> Just b EL.Reduction (Right _) -> Just True @@ -217,17 +217,18 @@ instance FromJSON DirectiveResultsUpdatedParams where -- | Convert an 'EL.EvalDirectiveResult' to a 'DirectiveUpdateItem'. -- Returns 'Nothing' if the result carries no source range. evalDirectiveToUpdateItem - :: (Int -> Text) -- ^ get raw line content by 1-indexed line number + :: ConstructorFieldNames + -> (Int -> Text) -- ^ get raw line content by 1-indexed line number -> EL.EvalDirectiveResult -> Maybe DirectiveUpdateItem -evalDirectiveToUpdateItem getLineContent (EL.MkEvalDirectiveResult (Just rng@(MkSrcRange (MkSrcPos lineNo colNo) _ _ _)) res mtrace) = +evalDirectiveToUpdateItem fields getLineContent (EL.MkEvalDirectiveResult (Just rng@(MkSrcRange (MkSrcPos lineNo colNo) _ _ _)) res mtrace) = Just DirectiveUpdateItem { directiveId = Text.pack (show lineNo) <> ":" <> Text.pack (show colNo) - , prettyText = EL.prettyEvalDirectiveResult (EL.MkEvalDirectiveResult (Just rng) res mtrace) + , prettyText = EL.prettyEvalDirectiveResultWithFields fields (EL.MkEvalDirectiveResult (Just rng) res mtrace) , success = case res of EL.Assertion b -> Just b EL.Reduction (Right _) -> Just True EL.Reduction (Left _) -> Just False , lineContent = getLineContent lineNo } -evalDirectiveToUpdateItem _ _ = Nothing +evalDirectiveToUpdateItem _ _ _ = Nothing