JSONTop.hs

module Agda.Interaction.JSONTop
    ( jsonREPL
    ) where

import Control.Monad
         ( (<=<), forM )
import Control.Monad.IO.Class
         ( MonadIO(..) )

import Data.ByteString.Lazy (ByteString)
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Text as T
import qualified Data.Set as Set

import Agda.Interaction.AgdaTop
import Agda.Interaction.Base
         ( CommandState(..), CurrentFile(..), ComputeMode(..), Rewrite(..)
         , OutputConstraint_boot(..), OutputForm_boot(..))
import Agda.Interaction.Output (OutputConstraint, OutputForm)
import qualified Agda.Interaction.BasicOps as B
import Agda.Interaction.EmacsTop
import Agda.Interaction.JSON
import Agda.Interaction.Response as R
import Agda.Interaction.Highlighting.JSON

import Agda.Syntax.Abstract.Pretty
         ( prettyATop )
import Agda.Syntax.Common
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Name
         ( NameInScope(..), Name )
import Agda.Syntax.Internal
         ( telToList, Dom'(..), Dom, MetaId(..), ProblemId(..), Blocker(..), alwaysUnblock )
import Agda.Syntax.Position
         ( Range, rangeIntervals, Interval'(..), Position'(..), noRange )
import Agda.Syntax.Scope.Base
         ( WhyInScopeData(..) )

import Agda.TypeChecking.Errors
         ( getAllWarningsOfTCErr )
import Agda.TypeChecking.Monad
         ( Comparison(..), inTopContext, TCM, TCErr, TCWarning, NamedMeta(..), withInteractionId )
import Agda.TypeChecking.Monad.MetaVars
         ( getInteractionRange, getMetaRange, withMetaId )
import Agda.TypeChecking.Pretty
         ( PrettyTCM(..), prettyTCM )
-- borrowed from EmacsTop, for temporarily serialising stuff
import Agda.TypeChecking.Pretty.Warning
         ( filterTCWarnings )
import Agda.TypeChecking.Warnings
         ( WarningsAndNonFatalErrors(..) )

import qualified Agda.Syntax.Common.Pretty as P
import Agda.Syntax.Common.Pretty
         ( Pretty(..), prettyShow )
import Agda.Utils.Time
         ( CPUTime(..) )

import Agda.VersionCommit

--------------------------------------------------------------------------------

-- | 'jsonREPL' is a interpreter like 'mimicGHCi', but outputs JSON-encoded strings.
--
--   'jsonREPL' reads Haskell values (that starts from 'IOTCM' ...) from stdin,
--   interprets them, and outputs JSON-encoded strings. into stdout.

jsonREPL :: TCM () -> TCM ()
jsonREPL = repl (liftIO . BS.putStrLn <=< jsonifyResponse) "JSON> "

instance EncodeTCM NameInScope where
instance ToJSON NameInScope where
  toJSON InScope    = toJSON True
  toJSON NotInScope = toJSON False

instance EncodeTCM Status where
instance ToJSON Status where
  toJSON status = object
    [ "showImplicitArguments"   .= sShowImplicitArguments status
    , "showIrrelevantArguments" .= sShowIrrelevantArguments status
    , "checked"                 .= sChecked status
    ]

instance EncodeTCM CommandState where
instance ToJSON CommandState where
  toJSON commandState = object
    [ "interactionPoints" .= theInteractionPoints commandState
    , "currentFile"       .= theCurrentFile commandState
    -- more?
    ]

instance EncodeTCM CurrentFile where
instance ToJSON CurrentFile where
  toJSON (CurrentFile path _ _ time) = toJSON (path, time)  -- backwards compat.

instance EncodeTCM ResponseContextEntry where
  encodeTCM entry = obj
    [ "originalName" @= encodePretty (respOrigName entry)
    , "reifiedName"  @= encodePretty (respReifName entry)
    , "binding"      #= prettyATop (unArg (respType entry))
    , "inScope"      @= respInScope entry
    ]

instance EncodeTCM (Position' ()) where
instance ToJSON (Position' ()) where
  toJSON p = object
    [ "pos"  .= toJSON (posPos p)
    , "line" .= toJSON (posLine p)
    , "col"  .= toJSON (posCol p)
    ]

instance EncodeTCM Range where
instance ToJSON Range where
  toJSON = toJSON . map prettyInterval . rangeIntervals
    where prettyInterval (Interval f s e) = object [ "start" .= (f <$ s), "end" .= (f <$ e) ]

instance EncodeTCM ProblemId where
instance EncodeTCM MetaId    where

instance ToJSON ProblemId where toJSON (ProblemId i) = toJSON i

instance ToJSON ModuleNameHash where
  toJSON (ModuleNameHash h) = toJSON h

instance ToJSON MetaId where
  toJSON m = object
    [ "id"     .= toJSON (metaId m)
    , "module" .= toJSON (metaModule m)
    ]

instance EncodeTCM InteractionId where
  encodeTCM ii@(InteractionId i) = obj
    [ "id"    @= toJSON i
    , "range" #= intervalsTCM
    ]
    where
      intervalsTCM = toJSON <$> getInteractionRange ii
instance ToJSON InteractionId where
  toJSON (InteractionId i) = toJSON i

instance EncodeTCM NamedMeta where
  encodeTCM m = obj
    [ "name"  #= nameTCM
    , "range" #= intervalsTCM
    ]
    where
      nameTCM = encodeShow <$> withMetaId (nmid m) (prettyATop m)
      intervalsTCM = toJSON <$> getMetaRange (nmid m)

instance EncodeTCM GiveResult where
instance ToJSON GiveResult where
  toJSON (Give_String s) = object [ "str" .= s ]
  toJSON Give_Paren   = object [ "paren" .= True ]
  toJSON Give_NoParen = object [ "paren" .= False ]

instance EncodeTCM MakeCaseVariant where
instance ToJSON MakeCaseVariant where
  toJSON R.Function = String "Function"
  toJSON R.ExtendedLambda = String "ExtendedLambda"

encodePretty :: Pretty a => a -> Value
encodePretty = encodeShow . pretty

encodeShow :: Show a => a -> Value
encodeShow = String . T.pack . show

encodePrettyTCM :: PrettyTCM a => a -> TCM Value
encodePrettyTCM = (encodeShow <$>) . prettyTCM

instance EncodeTCM Rewrite where
instance ToJSON Rewrite where toJSON = encodeShow

instance EncodeTCM CPUTime where
instance ToJSON CPUTime where toJSON = encodePretty

instance EncodeTCM ComputeMode where
instance ToJSON ComputeMode where toJSON = encodeShow

encodeOCCmp :: (a -> TCM Value)
  -> Comparison -> a -> a -> T.Text
  -> TCM Value
encodeOCCmp f c i j k = kind k
  [ "comparison"     @= encodeShow c
  , "constraintObjs" #= traverse f [i, j]
  ]

  -- Goals
encodeOC :: (a -> TCM Value)
  -> (b -> TCM Value)
  -> OutputConstraint b a
  -> TCM Value
encodeOC f encPrettyTCM = \case
 OfType i a -> kind "OfType"
  [ "constraintObj" #= f i
  , "type"          #= encPrettyTCM a
  ]
 CmpInType c a i j -> kind "CmpInType"
  [ "comparison"     @= encodeShow c
  , "type"           #= encPrettyTCM a
  , "constraintObjs" #= traverse f [i, j]
  ]
 CmpElim ps a is js -> kind "CmpElim"
  [ "polarities"     @= map encodeShow ps
  , "type"           #= encPrettyTCM a
  , "constraintObjs" #= traverse (traverse f) [is, js]
  ]
 JustType a -> kind "JustType"
  [ "constraintObj"  #= f a
  ]
 JustSort a -> kind "JustSort"
  [ "constraintObj"  #= f a
  ]
 CmpTypes  c i j -> encodeOCCmp f c i j "CmpTypes"
 CmpLevels c i j -> encodeOCCmp f c i j "CmpLevels"
 CmpTeles  c i j -> encodeOCCmp f c i j "CmpTeles"
 CmpSorts  c i j -> encodeOCCmp f c i j "CmpSorts"
 Assign i a -> kind "Assign"
  [ "constraintObj"  #= f i
  , "value"          #= encPrettyTCM a
  ]
 TypedAssign i v t -> kind "TypedAssign"
  [ "constraintObj"  #= f i
  , "value"          #= encPrettyTCM v
  , "type"           #= encPrettyTCM t
  ]
 PostponedCheckArgs i es t0 t1 -> kind "PostponedCheckArgs"
  [ "constraintObj"  #= f i
  , "ofType"         #= encPrettyTCM t0
  , "arguments"      #= forM es encPrettyTCM
  , "type"           #= encPrettyTCM t1
  ]
 IsEmptyType a -> kind "IsEmptyType"
  [ "type"           #= encPrettyTCM a
  ]
 SizeLtSat a -> kind "SizeLtSat"
  [ "type"           #= encPrettyTCM a
  ]
 FindInstanceOF i t cs -> kind "FindInstanceOF"
  [ "constraintObj"  #= f i
  , "candidates"     #= forM cs encodeKVPairs
  , "type"           #= encPrettyTCM t
  ]
  where encodeKVPairs (_, v, t) = obj -- TODO: encode kind
          [ "value"  #= encPrettyTCM v
          , "type"   #= encPrettyTCM t
          ]
 ResolveInstanceOF q -> kind "ResolveInstanceOF"
  [ "name"           @= encodePretty q
  ]
 PTSInstance a b -> kind "PTSInstance"
  [ "constraintObjs" #= traverse f [a, b]
  ]
 PostponedCheckFunDef name a err -> kind "PostponedCheckFunDef"
  [ "name"           @= encodePretty name
  , "type"           #= encPrettyTCM a
  , "error"          #= encodeTCM err
  ]
 DataSort q s -> kind "DataSort"
  [ "name"           @= encodePretty q
  , "sort"           #= f s
  ]
 CheckLock t lk -> kind "CheckLock"
  [ "head"           #= f t
  , "lock"           #= f lk
  ]
 UsableAtMod mod t -> kind "UsableAtMod"
  [ "mod"           @= encodePretty mod
  , "term"          #= f t
  ]

encodeNamedPretty :: PrettyTCM a => (Name, a) -> TCM Value
encodeNamedPretty (name, a) = obj
  [ "name" @= encodePretty name
  , "term" #= encodePrettyTCM a
  ]

instance EncodeTCM (OutputForm C.Expr C.Expr) where
  encodeTCM (OutputForm range problems unblock oc) = obj
    [ "range"      @= range
    , "problems"   @= problems
    , "unblocker"  @= unblock
    , "constraint" #= encodeOC (pure . encodePretty) (pure . encodePretty) oc
    ]

instance EncodeTCM Blocker where
  encodeTCM (UnblockOnMeta x)    = kind "UnblockOnMeta" [ "meta" @= x ]
  encodeTCM (UnblockOnProblem p) = kind "UnblockOnProblem" [ "id" @= p ]
  encodeTCM (UnblockOnDef q)     = kind "UnblockOnDef" [ "name" @= encodePretty q ]
  encodeTCM (UnblockOnAll us)    = kind "UnblockOnAll" [ "blockers" @= Set.toList us ]
  encodeTCM (UnblockOnAny us)    = kind "UnblockOnAny" [ "blockers" @= Set.toList us ]

instance EncodeTCM DisplayInfo where
  encodeTCM :: DisplayInfo -> TCM Value
  encodeTCM (Info_CompilationOk backend wes) = do
    ws <- filterTCWarnings (tcWarnings wes)
    es <- filterTCWarnings (nonFatalErrors wes)
    kind "CompilationOk"
      [ "backend"           @= encodePretty backend
      , "warnings"          #= encodeTCM ws
      , "errors"            #= encodeTCM es
      ]
  encodeTCM (Info_Constraints constraints) = kind "Constraints"
    [ "constraints"       #= forM constraints encodeTCM
    ]
  encodeTCM (Info_AllGoalsWarnings (vis, invis) wes) = do
    ws <- filterTCWarnings (tcWarnings wes)
    es <- filterTCWarnings (nonFatalErrors wes)
    kind "AllGoalsWarnings"
      [ "visibleGoals"      #= forM vis (\i -> withInteractionId (B.outputFormId $ OutputForm noRange [] alwaysUnblock i) $ encodeOC encodeTCM encodePrettyTCM i)
      , "invisibleGoals"    #= forM invis (encodeOC encodeTCM encodePrettyTCM)
      , "warnings"          #= encodeTCM ws
      , "errors"            #= encodeTCM es
      ]
  encodeTCM (Info_Time time) = kind "Time"
    [ "time"              @= time
    ]
  encodeTCM (Info_Error err) = encodeTCM err
  encodeTCM Info_Intro_NotFound = kind "IntroNotFound" []
  encodeTCM (Info_Intro_ConstructorUnknown introductions) = kind "IntroConstructorUnknown"
    [ "constructors"      @= map toJSON introductions
    ]
  encodeTCM (Info_Auto info) = kind "Auto"
    [ "info"              @= toJSON info
    ]
  encodeTCM (Info_ModuleContents names tele contents) = kind "ModuleContents"
    [ "contents"          #= forM contents encodeNamedPretty
    , "telescope"         #= forM (telToList tele) encodeDomType
    , "names"             @= map encodePretty names
    ]
    where
      encodeDomType :: PrettyTCM a => Dom (ArgName, a) -> TCM Value
      encodeDomType dom = obj
        [ "dom"       #= encodePrettyTCM (unDom dom)
        , "name"      @= fmap encodePretty (bareNameOf dom)
        , "finite"    @= toJSON (domIsFinite dom)
        , "cohesion"  @= encodeShow (modCohesion . argInfoModality $ domInfo dom)
        , "relevance" @= encodeShow (modRelevance . argInfoModality $ domInfo dom)
        , "hiding"    @= case argInfoHiding $ domInfo dom of
          Instance o -> show o
          o -> show o
        ]
  encodeTCM (Info_SearchAbout results search) = kind "SearchAbout"
    [ "results"           #= forM results encodeNamedPretty
    , "search"            @= toJSON search
    ]
  encodeTCM (Info_WhyInScope why@(WhyInScopeData y path _ _ _)) = kind "WhyInScope"
    [ "thing"             @= prettyShow y
    , "filepath"          @= toJSON path
    -- use Emacs message first
    , "message"           #= explainWhyInScope why
    ]
  encodeTCM (Info_NormalForm commandState computeMode time expr) = kind "NormalForm"
    [ "commandState"      @= commandState
    , "computeMode"       @= computeMode
    , "time"              @= time
    , "expr"              #= encodePrettyTCM expr
    ]
  encodeTCM (Info_InferredType commandState time expr) = kind "InferredType"
    [ "commandState"      @= commandState
    , "time"              @= time
    , "expr"              #= encodePrettyTCM expr
    ]
  encodeTCM (Info_Context ii ctx) = kind "Context"
    [ "interactionPoint"  @= ii
    , "context"           @= ctx
    ]
  encodeTCM Info_Version = kind "Version"
    [ "version"           @= (versionWithCommitInfo :: String)
    ]
  encodeTCM (Info_GoalSpecific ii info) = kind "GoalSpecific"
    [ "interactionPoint"  @= ii
    , "goalInfo"          #= withInteractionId ii (encodeGoalSpecific ii info)
    ]

instance EncodeTCM GoalTypeAux where
  encodeTCM GoalOnly = kind "GoalOnly" []
  encodeTCM (GoalAndHave expr _) = kind "GoalAndHave"
    [ "expr" #= encodePrettyTCM expr ]
  encodeTCM (GoalAndElaboration expr) = kind "GoalAndElaboration"
    [ "term" #= encodePrettyTCM expr ]

encodeGoalSpecific :: InteractionId -> GoalDisplayInfo -> TCM Value
encodeGoalSpecific ii = go
  where
  go (Goal_HelperFunction helperType) = kind "HelperFunction"
    [ "signature"   #= inTopContext (prettyATop helperType)
    ]
  go (Goal_NormalForm computeMode expr) = kind "NormalForm"
    [ "computeMode" @= computeMode
    , "expr"        #= B.showComputed computeMode expr
    ]
  go (Goal_GoalType rewrite goalType entries boundary outputForms) = kind "GoalType"
    [ "rewrite"     @= rewrite
    , "typeAux"     @= goalType
    , "type"        #= prettyTypeOfMeta rewrite ii
    , "entries"     @= entries
    , "boundary"    @= map encodePretty boundary
    , "outputForms" @= map encodePretty outputForms
    ]
  go (Goal_CurrentGoal rewrite) = kind "CurrentGoal"
    [ "rewrite"     @= rewrite
    , "type"        #= prettyTypeOfMeta rewrite ii
    ]
  go (Goal_InferredType expr) = kind "InferredType"
    [ "expr"        #= prettyATop expr
    ]

instance EncodeTCM Info_Error where
  encodeTCM :: Info_Error -> TCM Value
  encodeTCM (Info_GenericError err) = do
    ws <- filterTCWarnings =<< getAllWarningsOfTCErr err
    kind "Error"
      [ "warnings"          #= encodeTCM ws
      , "error"             #= encodeTCM err
      ]
  encodeTCM err = kind "Error"
    [ "warnings"          @= ([] :: [String])
    , "error"             #= obj
      [ "message"           #= showInfoError err
      ]
    ]

instance EncodeTCM TCErr where
  encodeTCM err = obj
    [ "message"     #= encodePrettyTCM err
    ]

instance EncodeTCM TCWarning where
  encodeTCM w = obj
    [ "message"     #= (P.render <$> prettyTCM w)
    ]

instance EncodeTCM Response where
  encodeTCM (Resp_HighlightingInfo info remove method modFile) =
    liftIO $ jsonifyHighlightingInfo info remove method modFile
  encodeTCM (Resp_DisplayInfo info) = kind "DisplayInfo"
    [ "info"          @= info
    ]
  encodeTCM (Resp_ClearHighlighting tokenBased) = kind "ClearHighlighting"
    [ "tokenBased"    @= tokenBased
    ]
  encodeTCM Resp_DoneAborting = kind "DoneAborting" []
  encodeTCM Resp_DoneExiting = kind "DoneExiting" []
  encodeTCM Resp_ClearRunningInfo = kind "ClearRunningInfo" []
  encodeTCM (Resp_RunningInfo debugLevel msg) = kind "RunningInfo"
    [ "debugLevel"    @= debugLevel
    , "message"       @= msg
    ]
  encodeTCM (Resp_Status status) = kind "Status"
    [ "status"        @= status
    ]
  encodeTCM (Resp_JumpToError filepath position) = kind "JumpToError"
    [ "filepath"      @= filepath
    , "position"      @= position
    ]
  encodeTCM (Resp_InteractionPoints interactionPoints) = kind "InteractionPoints"
    [ "interactionPoints" @= interactionPoints
    ]
  encodeTCM (Resp_GiveAction i giveResult) = kind "GiveAction"
    [ "interactionPoint"  @= i
    , "giveResult"        @= giveResult
    ]
  encodeTCM (Resp_MakeCase id variant clauses) = kind "MakeCase"
    [ "interactionPoint"  @= id
    , "variant"           @= variant
    , "clauses"           @= clauses
    ]
  encodeTCM (Resp_SolveAll solutions) = kind "SolveAll"
    [ "solutions"     @= map encodeSolution solutions
    ]
    where
      encodeSolution (i, expr) = object
        [ "interactionPoint"  .= i
        , "expression"        .= P.prettyShow expr
        ]
  encodeTCM (Resp_Mimer ii str) = kind "Mimer"
    [ "solution" @= str
    ]

-- | Convert Response to an JSON value for interactive editor frontends.
jsonifyResponse :: Response -> TCM ByteString
jsonifyResponse = pure . encode <=< encodeTCM