0 | module Idris.Desugar.Mutual
 1 |
 2 | import Idris.Syntax
 3 | import TTImp.TTImp
 4 |
 5 | %default total
 6 |
 7 | -- Get the declaration to process on each pass of a mutual block
 8 | -- Essentially: types on the first pass
 9 | --  i.e. type constructors of data declarations
10 | --       function types
11 | --       interfaces (in full, since it includes function types)
12 | --       records (just the generated type constructor)
13 | --       implementation headers (i.e. note their existence, but not the bodies)
14 | -- Everything else on the second pass
15 | getDecl : Pass -> PDecl-> Maybe PDecl
16 | getDecl p (MkWithData fc $ PImplementation vis opts _ is cons n ps iname nusing ds)
17 |     = Just (MkWithData fc $ PImplementation vis opts p is cons n ps iname nusing ds)
18 |
19 | getDecl p (MkWithData fc $ PNamespace ns ds)
20 |     = Just (MkWithData fc $ PNamespace ns (assert_total $ mapMaybe (getDecl p) ds))
21 |
22 | getDecl AsType d@(MkWithData _ $ PClaim _) = Just d
23 | getDecl AsType (MkWithData fc $ PData doc vis mbtot (MkPData dfc tyn (Just tyc) _ _))
24 |     = Just (MkWithData fc $ PData doc vis mbtot (MkPLater dfc tyn tyc))
25 | getDecl AsType d@(MkWithData _ $ PInterface {}) = Just d
26 | getDecl AsType d@(MkWithData fc $ PRecord doc vis mbtot (MkPRecord n ps _ _ _))
27 |     = Just (MkWithData fc $ PData doc vis mbtot (MkPLater d.fc n (mkRecType ps)))
28 |   where
29 |     mkRecType : List PBinder -> PTerm
30 |     mkRecType [] = PType d.fc
31 |     mkRecType (MkPBinder p (MkBasicMultiBinder c (n ::: []) t) :: ts)
32 |       = PPi d.fc c p (Just n.val) t (mkRecType ts)
33 |     mkRecType (MkPBinder p (MkBasicMultiBinder c (n ::: x :: xs) t) :: ts)
34 |       = PPi d.fc c p (Just n.val) t
35 |           (assert_total $ mkRecType (MkPBinder p (MkBasicMultiBinder c (x ::: xs) t) :: ts))
36 | getDecl AsType d@(MkWithData _ $ PFixity _ ) = Just d
37 | getDecl AsType d@(MkWithData _ $ PDirective _) = Just d
38 | getDecl AsType d = Nothing
39 |
40 | getDecl AsDef (MkWithData _ $ PClaim _) = Nothing
41 | getDecl AsDef d@(MkWithData _ $ PData _ _ _ (MkPLater {})) = Just d
42 | getDecl AsDef (MkWithData _ $ PInterface {}) = Nothing
43 | getDecl AsDef d@(MkWithData _ $ PRecord _ _ _ (MkPRecordLater {})) = Just d
44 | getDecl AsDef (MkWithData _ $ PFixity _ ) = Nothing
45 | getDecl AsDef (MkWithData _ $ PDirective _) = Nothing
46 | getDecl AsDef d = Just d
47 |
48 | getDecl p (MkWithData fc $ PParameters ps pds)
49 |     = Just (MkWithData fc $ PParameters ps (assert_total $ mapMaybe (getDecl p) pds))
50 | getDecl p (MkWithData fc $ PUsing ps pds)
51 |     = Just (MkWithData fc $ PUsing ps (assert_total $ mapMaybe (getDecl p) pds))
52 |
53 | getDecl Single d = Just d
54 |
55 | export
56 | splitMutual : List PDecl -> (List PDecl, List PDecl)
57 | splitMutual ds = (mapMaybe (getDecl AsType) ds, mapMaybe (getDecl AsDef) ds)
58 |