0 | module Core.TT.Traversals
5 | import Data.SortedSet
6 | import Libraries.Data.NameMap
12 | unBinds : Term vars -> Exists (\ outer => Term (outer <>> vars))
13 | unBinds (Bind _ x _ scope) = let (Evidence outer t) = unBinds scope in
14 | Evidence (outer :< x) t
15 | unBinds t = Evidence [<] t
18 | onPRefs : Monoid m =>
21 | onPRefs f = go neutral where
23 | go : m -> Term vars' -> m
24 | gos : m -> List (Term vars') -> m
26 | go acc (Local fc isLet idx p) = acc
27 | go acc (Ref fc x name) = acc <+> f name
28 | go acc (Meta fc x y xs) = gos acc xs
29 | go acc (Bind fc x b scope) = go (acc <+> concatMap (onPRefs f) b) scope
30 | go acc (App fc fn arg) = go (go acc fn) arg
31 | go acc (As fc x as pat) = go (go acc as) pat
32 | go acc (TDelayed fc x y) = go acc y
33 | go acc (TDelay fc x ty arg) = go (go acc ty) arg
34 | go acc (TForce fc x y) = go acc y
35 | go acc (PrimVal fc c) = acc
36 | go acc (Erased fc imp) = acc
37 | go acc (TType fc u) = acc
40 | gos acc (x :: xs) = gos (go acc x) xs
43 | allGlobals : Term vars -> NameMap ()
44 | allGlobals = onPRefs (\ n => singleton n ())
47 | onConstants : Monoid m =>
50 | onConstants f = go neutral where
52 | go : m -> Term vars' -> m
53 | gos : m -> List (Term vars') -> m
55 | go acc (Local fc isLet idx p) = acc
56 | go acc (Ref fc x name) = acc
57 | go acc (Meta fc x y xs) = gos acc xs
58 | go acc (Bind fc x b scope) = go (acc <+> concatMap (onConstants f) b) scope
59 | go acc (App fc fn arg) = go (go acc fn) arg
60 | go acc (As fc x as pat) = go (go acc as) pat
61 | go acc (TDelayed fc x y) = go acc y
62 | go acc (TDelay fc x ty arg) = go (go acc ty) arg
63 | go acc (TForce fc x y) = go acc y
64 | go acc (PrimVal fc c) = acc <+> f c
65 | go acc (Erased fc imp) = acc
66 | go acc (TType fc u) = acc
69 | gos acc (x :: xs) = gos (go acc x) xs
72 | allConstants : Term vars -> SortedSet Constant
73 | allConstants = onConstants @{MkMonoid @{MkSemigroup union} empty} singleton
76 | mapTermM : Monad m =>
77 | ({vars : _} -> Term vars -> m (Term vars)) ->
78 | ({vars : _} -> Term vars -> m (Term vars))
79 | mapTermM f t = act t where
81 | act : {vars : _} -> Term vars -> m (Term vars)
82 | go : {vars : _} -> Term vars -> m (Term vars)
86 | go t@(Local fc isLet idx p) = pure t
87 | go t@(Ref fc x name) = pure t
88 | go t@(Meta fc x y xs) = Meta fc x y <$> traverse act xs
89 | go t@(Bind fc x b scope) = Bind fc x <$> traverse act b <*> act scope
90 | go t@(App fc fn arg) = App fc <$> act fn <*> act arg
91 | go t@(As fc x as pat) = As fc x <$> act as <*> act pat
92 | go t@(TDelayed fc x y) = TDelayed fc x <$> act y
93 | go t@(TDelay fc x ty arg) = TDelay fc x <$> act ty <*> act arg
94 | go t@(TForce fc x y) = pure t
95 | go t@(PrimVal fc c) = pure t
96 | go t@(Erased fc imp) = pure t
97 | go t@(TType fc u) = pure t
100 | mapTerm : ({vars : _} -> Term vars -> Term vars) ->
101 | ({vars : _} -> Term vars -> Term vars)
102 | mapTerm f t = act t where
104 | act : {vars : _} -> Term vars -> Term vars
105 | go : {vars : _} -> Term vars -> Term vars
109 | go t@(Local fc isLet idx p) = t
110 | go t@(Ref fc x name) = t
111 | go t@(Meta fc x y xs) = Meta fc x y (map act xs)
112 | go t@(Bind fc x b scope) = Bind fc x (map act b) (act scope)
113 | go t@(App fc fn arg) = App fc (act fn) (act arg)
114 | go t@(As fc x as pat) = As fc x (act as) (act pat)
115 | go t@(TDelayed fc x y) = TDelayed fc x (act y)
116 | go t@(TDelay fc x ty arg) = TDelay fc x (act ty) (act arg)
117 | go t@(TForce fc x y) = t
118 | go t@(PrimVal fc c) = t
119 | go t@(Erased fc imp) = t
120 | go t@(TType fc u) = t