summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Internal/Defs.hs
blob: a79b7be2ff465cc320f24999da6d9877a0a37f3a (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}

-- | Extract used definitions from terms.
module Agda.Syntax.Internal.Defs where

import Control.Monad.Reader
import Control.Monad.Writer

import qualified Data.Foldable as Fold

import Agda.Syntax.Common
import Agda.Syntax.Internal hiding (ArgInfo, Arg, Dom)

import Agda.Utils.Impossible
#include "undefined.h"

-- | @getDefs' lookup emb a@ extracts all used definitions
--   (functions, data/record types) from @a@, embedded into a monoid via @emb@.
--   Instantiations of meta variables are obtained via @lookup@.
--
--   Typical monoid instances would be @[QName]@ or @Set QName@.
--   Note that @emb@ can also choose to discard a used definition
--   by mapping to the unit of the monoid.
getDefs' :: (GetDefs a, Monoid b) => (MetaId -> Maybe Term) -> (QName -> b) -> a -> b
getDefs' lookup emb = execWriter . (`runReaderT` GetDefsEnv lookup emb) . getDefs

-- | Inputs to and outputs of @getDefs'@ are organized as a monad.
type GetDefsM b = ReaderT (GetDefsEnv b) (Writer b)

data GetDefsEnv b = GetDefsEnv
  { lookupMeta :: MetaId -> Maybe Term
  , embDef     :: QName -> b
  }

-- | What it takes to get the used definitions.
class Monad m => MonadGetDefs m where
  doDef  :: QName -> m ()
  doMeta :: MetaId -> m ()

instance Monoid b => MonadGetDefs (GetDefsM b) where
  doDef  d = tell . ($ d) =<< asks embDef
  doMeta x = getDefs . ($ x) =<< asks lookupMeta

-- | Getting the used definitions.
class GetDefs a where
  getDefs :: MonadGetDefs m => a -> m ()

instance GetDefs Clause where
  getDefs = getDefs . clauseBody

instance GetDefs ClauseBody where
  getDefs b = case b of
    Body v -> getDefs v
    Bind b -> getDefs b
    NoBody -> return ()

instance GetDefs Term where
  getDefs v = case v of
    Def d vs   -> doDef d >> getDefs vs
    Con c vs   -> getDefs vs
    Lit l      -> return ()
    Var i vs   -> getDefs vs
    Lam _ v    -> getDefs v
    Pi a b     -> getDefs a >> getDefs b
    Sort s     -> getDefs s
    Level l    -> getDefs l
    MetaV x vs -> getDefs x >> getDefs vs
    DontCare v -> getDefs v
    Shared p   -> getDefs $ derefPtr p  -- TODO: exploit sharing!
    ExtLam _ _ -> __IMPOSSIBLE__

instance GetDefs MetaId where
  getDefs x = doMeta x

instance GetDefs Type where
  getDefs (El s t) = getDefs s >> getDefs t

instance GetDefs Sort where
  getDefs s = case s of
    Type l    -> getDefs l
    Prop      -> return ()
    Inf       -> return ()
    SizeUniv  -> return ()
    DLub s s' -> getDefs s >> getDefs s'

instance GetDefs Level where
  getDefs (Max ls) = getDefs ls

instance GetDefs PlusLevel where
  getDefs ClosedLevel{} = return ()
  getDefs (Plus _ l)    = getDefs l

instance GetDefs LevelAtom where
  getDefs a = case a of
    MetaLevel x vs   -> getDefs x >> getDefs vs
    BlockedLevel _ v -> getDefs v
    NeutralLevel _ v -> getDefs v
    UnreducedLevel v -> getDefs v

-- collection instances

instance GetDefs a => GetDefs (Maybe a) where
  getDefs = Fold.mapM_ getDefs

instance GetDefs a => GetDefs [a] where
  getDefs = Fold.mapM_ getDefs

instance GetDefs a => GetDefs (Elim' a) where
  getDefs = Fold.mapM_ getDefs

instance GetDefs c => GetDefs (ArgInfo c) where
  getDefs = Fold.mapM_ getDefs

instance (GetDefs c, GetDefs a) => GetDefs (Arg c a) where
  getDefs (Arg c a) = getDefs c >> getDefs a

instance (GetDefs c, GetDefs a) => GetDefs (Dom c a) where
  getDefs (Dom c a) = getDefs c >> getDefs a

instance GetDefs a => GetDefs (Abs a) where
  getDefs = getDefs . unAbs

instance (GetDefs a, GetDefs b) => GetDefs (a,b) where
  getDefs (a,b) = getDefs a >> getDefs b