Thomasgorissen/inspector

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.
 --

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

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"

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.

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