Finish the EncodeTCM instance for DisplayInfo

[ice1000]

agda/src/full/Agda/Interaction/JSONTop.hs

Lines 44 to 110 in ed526b5

	-- we leave some of the fields as Null for the moment
	instance ToJSON DisplayInfo where
	toJSON _ = Null
	-- toJSON (Info_CompilationOk warningsAndErrors) = object
	-- [ "kind" .= String "CompilationOk"
	-- , "warnings" .= Null
	-- , "errors" .= Null
	-- ]
	-- toJSON (Info_Constraints constraints) = object
	-- [ "kind" .= String "Constraints"
	-- , "constraints" .= Null
	-- ]
	-- toJSON (Info_AllGoalsWarnings _goals _warningsAndErrors) = object
	-- [ "kind" .= String "AllGoalsWarnings"
	-- , "goals" .= Null
	-- , "warnings" .= Null
	-- , "errors" .= Null
	-- ]
	-- toJSON (Info_Time doc) = object
	-- [ "kind" .= String "Time"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_Error msg) = object
	-- [ "kind" .= String "Error"
	-- , "payload" .= Null
	-- ]
	-- toJSON Info_Intro_NotFound = object
	-- [ "kind" .= String "IntroNotFound"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_Intro_ConstructorUnknown introductions) = object
	-- [ "kind" .= String "IntroConstructorUnknown"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_Auto _) = object
	-- [ "kind" .= String "Auto"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_ModuleContents _ _ _) = object
	-- [ "kind" .= String "ModuleContents"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_SearchAbout _ _) = object
	-- [ "kind" .= String "SearchAbout"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_WhyInScope _ _ _ _ _) = object
	-- [ "kind" .= String "WhyInScope"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_NormalForm _) = object
	-- [ "kind" .= String "NormalForm"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_NormalForm _ _) = object
	-- [ "kind" .= String "NormalForm"
	-- , "payload" .= Null
	-- ]
	-- toJSON (Info_GoalType doc) = object [ "kind" .= String "GoalType", "payload" .= render doc ]
	-- toJSON (Info_CurrentGoal doc) = object [ "kind" .= String "CurrentGoal", "payload" .= render doc ]
	-- toJSON (Info_InferredType doc) = object [ "kind" .= String "InferredType", "payload" .= render doc ]
	-- toJSON (Info_Context ii doc) = object [ "kind" .= String "Context", "payload" .= render doc ]
	-- toJSON (Info_HelperFunction doc) = object [ "kind" .= String "HelperFunction", "payload" .= render doc ]
	-- toJSON Info_Version = object
	-- [ "kind" .= String "Version"
	-- , "version" .= (("Agda version " ++ versionWithCommitInfo) :: String)
	-- ]

And I need this for a toy I'm working on. Probably taking this myself.

[ice1000]

Reference: f9915d9

[banacorn]

Hope that this will be useful https://github.com/banacorn/agda/blob/json/src/full/Agda/Interaction/JSONTop.hs#L80

Here's the serialization of all of the concrete syntax tree: https://github.com/banacorn/agda/tree/json/src/full/Agda/Interaction/JSON/Syntax

[ice1000]

Here's the serialization of all of the concrete syntax tree: https://github.com/banacorn/agda/tree/json/src/full/Agda/Interaction/JSON/Syntax

Wow look at that. Is this thing ready or there's something missing?

[ice1000]

Hope that this will be useful https://github.com/banacorn/agda/blob/json/src/full/Agda/Interaction/JSONTop.hs#L80

I've pushed a modified version of this into the current master Agda

[banacorn]

Wow look at that. Is this thing ready or there's something missing?

I've built a prototype last year (with agda-mode on Atom as the frontend).
You can do lots of fancy stuff if the frontend also has access to the AST (especially source locations). For example, when there's a type error, you can hover the cursor on those "code part" of the error message and it will highlight the corresponding source code.

[ice1000]

Cool, but you don't have access to the TCM do you? And does that mean you don't have contextual information?

[banacorn]

I have access to the TCM, and in fact most of the serialization would need to be done in the TCM.
IIRC that's because most information we need are not readily stored as Concrete syntax tree, you need to convert them from Internal or Abstract to Concrete, and that can only be done in the TCM

Edit: relevant PR #3192

[banacorn]

It would be nice if we can serialize stuff without the TCM, but that's a lot of work.

[ice1000]

I tend to include (and keep it even after the entire AST serialization is implemented) a pretty-printed term because this interface can be used in many places and we shouldn't need to always impl full AST deserialization.

[banacorn]

I tend to include (and keep it even after the entire AST serialization is implemented) a pretty-printed term because this interface can be used in many places and we shouldn't need to always impl full AST deserialization.

We can add some flags for different "depths" of serialization, but then there will be the problem of "where to draw the line".
Or perhaps we can simply just include the pretty-printed term in the serialized JSON.

[ice1000]

We can add some flags for different "depths" of serialization, but then there will be the problem of "where to draw the line".

I'd say it's not necessary, we can simply include all the info. I believe modern deserializers will allow ignoring unknown fields :).

[jespercockx]

@ice1000 what's the status on this issue?

[ice1000]

@ice1000 what's the status on this issue?

I'm not sure, there's a lot of thins can be made, but speaking of instance EncodeTCM DisplayInfo (EncodeTCM supersedes ToJSON to some extent), it's already finished (not including serializing the entire AST).
Maybe I should close this?

[ice1000]

Probably not, I just saw some Nulls. Reopening

[ice1000]

Will be closed by #4213