@@ -292,7 +292,73 @@ instance ToJSON MetaInformation where
292292 toJSON m = object ["MetaInformation" .= show m]
293293
294294instance ToJSON Def where
295− toJSON d = object ["Def" .= show d]
295+ toJSON (Function ty tm) = object ["Function" .= (ty, tm)]
296+ toJSON (TyDecl nm ty) = object ["TyDecl" .= (nm, ty)]
297+ toJSON (Operator ty n f) = Null -- Operator and CaseOp omits same values as in IBC.hs
298+ toJSON (CaseOp info ty argTy _ _ cdefs) = object ["CaseOp" .= (info, ty, argTy, cdefs)]
299+
300+instance (ToJSON t) => ToJSON (TT t) where
301+ toJSON (P nt name term) = object ["P" .= (nt, name, term)]
302+ toJSON (V n) = object ["V" .= n]
303+ toJSON (Bind n b tt) = object ["Bind" .= (n, b, tt)]
304+ toJSON (App s t1 t2) = object ["App" .= (s, t1, t2)]
305+ toJSON (Constant c) = object ["Constant" .= c]
306+ toJSON (Proj tt n) = object ["Proj" .= (tt, n)]
307+ toJSON Erased = object ["Erased" .= Null]
308+ toJSON Impossible = object ["Impossible" .= Null]
309+ toJSON (Inferred tt) = object ["Inferred" .= tt]
310+ toJSON (TType u) = object ["TType" .= u]
311+ toJSON (UType u) = object ["UType" .= (show u)]
312+
313+instance ToJSON UExp where
314+ toJSON (UVar src n) = object ["UVar" .= (src, n)]
315+ toJSON (UVal n) = object ["UVal" .= n]
316+
317+
318+instance (ToJSON t) => ToJSON (AppStatus t) where
319+ toJSON Complete = object ["Complete" .= Null]
320+ toJSON MaybeHoles = object ["MaybeHoles" .= Null]
321+ toJSON (Holes ns) = object ["Holes" .= ns]
322+
323+instance (ToJSON t) => ToJSON (Binder t) where
324+ toJSON (Lam rc bty) = object ["Lam" .= (rc, bty)]
325+ toJSON (Pi c i t k) = object ["Pi" .= (c, i, t, k)]
326+ toJSON (Let t v) = object ["Let" .= (t, v)]
327+ toJSON (NLet t v) = object ["NLet" .= (t, v)]
328+ toJSON (Hole t) = object ["Hole" .= (t)]
329+ toJSON (GHole l ns t) = object ["GHole" .= (l, ns, t)]
330+ toJSON (Guess t v) = object ["Guess" .= (t, v)]
331+ toJSON (PVar rc t) = object ["PVar" .= (rc, t)]
332+ toJSON (PVTy t) = object ["PVTy" .= (t)]
333+
334+instance ToJSON ImplicitInfo where
335+ toJSON (Impl a b c) = object ["Impl" .= (a, b, c)]
336+
337+instance ToJSON NameType where
338+ toJSON Bound = object ["Bound" .= Null]
339+ toJSON Ref = object ["Ref" .= Null]
340+ toJSON (DCon a b c) = object ["DCon" .= (a, b, c)]
341+ toJSON (TCon a b) = object ["TCon" .= (a, b)]
342+
343+instance ToJSON CaseDefs where
344+ toJSON (CaseDefs rt ct) = object ["Runtime" .= rt, "Compiletime" .= ct]
345+
346+instance (ToJSON t) => ToJSON (SC' t) where
347+ toJSON (Case ct n alts) = object ["Case" .= (ct, n, alts)]
348+ toJSON (ProjCase t alts) = object ["ProjCase" .= (t, alts)]
349+ toJSON (STerm t) = object ["STerm" .= t]
350+ toJSON (UnmatchedCase s) = object ["UnmatchedCase" .= s]
351+ toJSON ImpossibleCase = object ["ImpossibleCase" .= Null]
352+
353+instance (ToJSON t) => ToJSON (CaseAlt' t) where
354+ toJSON (ConCase n c ns sc) = object ["ConCase" .= (n, c, ns, sc)]
355+ toJSON (FnCase n ns sc) = object ["FnCase" .= (n, ns, sc)]
356+ toJSON (ConstCase c sc) = object ["ConstCase" .= (c, sc)]
357+ toJSON (SucCase n sc) = object ["SucCase" .= (n, sc)]
358+ toJSON (DefaultCase sc) = object ["DefaultCase" .= sc]
359+
360+instance ToJSON CaseInfo where
361+ toJSON (CaseInfo a b c) = object ["CaseInfo" .= (a, b, c)]
296362
297363instance ToJSON Accessibility where
298364 toJSON a = object ["Accessibility" .= show a]