summaryrefslogtreecommitdiff
path: root/src/full/Agda/Compiler/Epic/Static.hs
blob: 13fee876d6d81b09bdc1ba92493f95c32b385349 (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
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleInstances #-}

-- | Find the places where the builtin static is used and do some normalisation
--   there.
module Agda.Compiler.Epic.Static where

import Control.Applicative
import Control.Monad
import Control.Monad.State

import qualified Data.Map as Map
import Data.Traversable (traverse)

import Agda.Syntax.Common
import Agda.Syntax.Internal as I

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Sharing
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Pretty

import Agda.Utils.Monad
import qualified Agda.Utils.HashMap as HM

import Agda.Compiler.Epic.CompileState

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

normaliseStatic :: CompiledClauses -> Compile TCM CompiledClauses
normaliseStatic = evaluateCC

evaluateCC :: CompiledClauses -> Compile TCM CompiledClauses
evaluateCC ccs = case ccs of
    Case n brs -> do
        cbrs <- forM (Map.toList $ conBranches brs) $ \(c, WithArity n cc) -> (,) c <$> (WithArity n <$> evaluateCC cc)
        lbrs <- forM (Map.toList $ litBranches brs) $ \(l, cc) -> (,) l <$> evaluateCC cc
        cab <- case catchAllBranch brs of
            Nothing -> return Nothing
            Just cc -> Just <$> evaluateCC cc
        return $ Case n Branches
            { conBranches    = Map.fromList cbrs
            , litBranches    = Map.fromList lbrs
            , catchAllBranch = cab
            }
    Done n t   -> Done n <$> evaluate t
    Fail       -> return Fail

etaExpand :: Term -> Compile TCM Term
etaExpand def@(Def n ts) = do
    defs <- lift (sigDefinitions <$> use stImports)
    let f   = maybe __IMPOSSIBLE__ theDef (HM.lookup n defs)
        len = length . clausePats . head .  funClauses $ f
        toEta :: Num a => a
        toEta = fromIntegral $ len - length ts
        term  = raise toEta def `apply` [ defaultArg $ Var i [] | i <- [toEta - 1, toEta - 2 .. 0]]
    return $ foldr (\ v t -> Lam defaultArgInfo (Abs v t)) term $ replicate toEta "staticVar"
etaExpand x = return x

class Evaluate a where
  evaluate :: a -> Compile TCM a

instance Evaluate a => Evaluate [a] where
  evaluate = traverse evaluate

instance Evaluate a => Evaluate (I.Arg a) where
  evaluate = traverse evaluate

instance Evaluate a => Evaluate (Abs a) where
  evaluate = traverse evaluate  -- TODO: maintain context

instance Evaluate a => Evaluate (Elim' a) where
  evaluate = traverse evaluate

instance Evaluate Term where
  evaluate term = case term of
    Var x es     -> Var x <$> evaluate es
    Lam h b      -> Lam h <$> evaluate b
{-
      ab' <- evaluateTerm (unAbs ab)
      return $ Lam h $ Abs (absName ab) ab'
-}
    Lit l        -> return $ Lit l
    Def n es     -> ifNotM (isStatic n) {- then -} (Def n <$> evaluate es) $ {- else -} do
        feta <- return term -- etaExpand term
        f <- lift $ normalise feta
        lift $ reportSDoc "epic.static" 10 $ vcat
          [ text "STATIC pragma fired"
          , nest 2 $ vcat
            [ text "before :" <+> prettyTCM term
            , text "after  :" <+> prettyTCM f
            ]
          ]
        return f
    Con c args   -> Con c <$> evaluate args
    Pi  arg abs  -> return term
    Sort s       -> return term
    MetaV i args -> return term
    Level l      -> return term
    DontCare i   -> return term
    Shared{}     -> updateSharedTermT evaluate term
    ExtLam{}     -> __IMPOSSIBLE__
    where
{-
    evaluateTerms :: Args -> Compile TCM Args
    evaluateTerms as = forM as $ \x -> do
      y <- evaluateTerm (unArg x)
      return x { unArg = y }
-}
    isStatic :: QName -> Compile TCM Bool
    isStatic q = do
      defs <- lift (sigDefinitions <$> use stImports)
      return $ case fmap theDef $ HM.lookup q defs of
          Nothing -> False
          Just (f@Function{}) -> funStatic f
          Just _              -> False