@@ -373,12 +373,19 @@ declared (PFix _ _ _) = []
373declared (PTy _ _ _ _ n t) = [n]
373declared (PTy _ _ _ _ n t) = [n]
374declared (PPostulate _ _ _ _ n t) = [n]
374declared (PPostulate _ _ _ _ n t) = [n]
375declared (PClauses _ _ n _) = [] -- not a declaration
375declared (PClauses _ _ n _) = [] -- not a declaration
376−declared (PRecord _ _ _ n _ _ c _) = [n, c]
376+declared (PCAF _ n _) = [n]
377declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
377declared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
378 where fstt (_, a, _, _) = a
378 where fstt (_, a, _, _) = a
379+declared (PData _ _ _ _ (PLaterdecl n _)) = [n]
379declared (PParams _ _ ds) = concatMap declared ds
380declared (PParams _ _ ds) = concatMap declared ds
380−declared (PMutual _ ds) = concatMap declared ds
381declared (PNamespace _ ds) = concatMap declared ds
381declared (PNamespace _ ds) = concatMap declared ds
382+declared (PRecord _ _ _ n _ _ c _) = [n, c]
383+declared (PClass _ _ _ _ n _ ms) = n : concatMap declared ms
384+declared (PInstance _ _ _ _ _ _ _ _) = []
385+declared (PDSL n _) = [n]
386+declared (PSyntax _ _) = []
387+declared (PMutual _ ds) = concatMap declared ds
388+declared (PDirective _) = []
383-- get the names declared, not counting nested parameter blocks
390-- get the names declared, not counting nested parameter blocks
384tldeclared :: PDecl -> [Name]
391tldeclared :: PDecl -> [Name]
@@ -392,20 +399,27 @@ tldeclared (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
392tldeclared (PParams _ _ ds) = []
399tldeclared (PParams _ _ ds) = []
393tldeclared (PMutual _ ds) = concatMap tldeclared ds
400tldeclared (PMutual _ ds) = concatMap tldeclared ds
394tldeclared (PNamespace _ ds) = concatMap tldeclared ds
401tldeclared (PNamespace _ ds) = concatMap tldeclared ds
395−-- declared (PImport _) = []
402+
397defined :: PDecl -> [Name]
404defined :: PDecl -> [Name]
398defined (PFix _ _ _) = []
405defined (PFix _ _ _) = []
399defined (PTy _ _ _ _ n t) = []
406defined (PTy _ _ _ _ n t) = []
400defined (PPostulate _ _ _ _ n t) = []
407defined (PPostulate _ _ _ _ n t) = []
401defined (PClauses _ _ n _) = [n] -- not a declaration
408defined (PClauses _ _ n _) = [n] -- not a declaration
402−defined (PRecord _ _ _ n _ _ c _) = [n, c]
409+defined (PCAF _ n _) = [n]
403defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
410defined (PData _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
404 where fstt (_, a, _, _) = a
411 where fstt (_, a, _, _) = a
412+defined (PData _ _ _ _ (PLaterdecl n _)) = []
405defined (PParams _ _ ds) = concatMap defined ds
413defined (PParams _ _ ds) = concatMap defined ds
406−defined (PMutual _ ds) = concatMap defined ds
407defined (PNamespace _ ds) = concatMap defined ds
414defined (PNamespace _ ds) = concatMap defined ds
408−-- declared (PImport _) = []
415+defined (PRecord _ _ _ n _ _ c _) = [n, c]
416+defined (PClass _ _ _ _ n _ ms) = n : concatMap defined ms
417+defined (PInstance _ _ _ _ _ _ _ _) = []
418+defined (PDSL n _) = [n]
419+defined (PSyntax _ _) = []
420+defined (PMutual _ ds) = concatMap defined ds
421+defined (PDirective _) = []
410updateN :: [(Name, Name)] -> Name -> Name
424updateN :: [(Name, Name)] -> Name -> Name
411updateN ns n | Just n' <- lookup n ns = n'
425updateN ns n | Just n' <- lookup n ns = n'