← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/full/Agda/Compiler/Epic/Smashing.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Compiler/Epic/Smashing.hs
1
1
{-# LANGUAGE CPP #-}
 
2
 
2
3
-- | Smash functions which return something that can be inferred
3
4
--   (something of a type with only one element)
4
5
 
5
6
module Agda.Compiler.Epic.Smashing where
6
7
 
7
 
import Control.Arrow((&&&))
8
 
import Control.Monad
9
8
import Control.Monad.State
10
 
import Control.Monad.Trans
11
9
 
12
10
import Data.List
13
 
import qualified Data.Map as M
14
 
import Data.Map (Map)
15
11
import Data.Maybe
16
12
 
17
13
import qualified Data.Set as S
24
20
import Agda.TypeChecking.Telescope
25
21
import Agda.TypeChecking.Pretty
26
22
import Agda.TypeChecking.Reduce
27
 
import Agda.TypeChecking.Rules.LHS.Unify
28
23
 
29
24
import Agda.Compiler.Epic.AuxAST as AA
30
25
import Agda.Compiler.Epic.CompileState
75
70
  where names = teleNames xs ++ teleNames ys
76
71
 
77
72
-- | Can a datatype be inferred? If so, return the only possible value.
78
 
inferable :: Set QName -> QName -> [Arg Term] ->  Compile TCM (Maybe Expr)
 
73
inferable :: Set QName -> QName -> [SI.Arg Term] ->  Compile TCM (Maybe Expr)
79
74
inferable visited dat args | dat `S.member` visited = return Nothing
80
75
inferable visited dat args = do
81
76
  lift $ reportSLn "epic.smashing" 10 $ "  inferring:" ++ (show dat)
88
83
            _   -> return Nothing
89
84
      r@Record{}   -> inferableArgs (recCon r) (recPars r)
90
85
      f@Function{} -> do
91
 
        term <- lift $ normalise $ Def dat args
 
86
        term <- lift $ normalise $ Def dat $ map SI.Apply args
92
87
        inferableTerm visited' term
93
88
      d -> do
94
89
        lift $ reportSLn "epic.smashing" 10 $ "  failed (inferable): " ++ (show d)
108
103
        (AA.Con tag c <$>) <$> sequence <$> forM (notForced forc $ flattenTel tel) (inferableTerm visited' . unEl . unDom)
109
104
    visited' = S.insert dat visited
110
105
 
111
 
inferableTerm visited t = case t of
112
 
    Def q as     -> inferable visited q as
 
106
inferableTerm visited t = do
 
107
  case t of
 
108
    Def q es    ->
 
109
      case allApplyElims es of
 
110
        Just vs -> inferable visited q vs
 
111
        Nothing -> return Nothing
113
112
    Pi _   b    -> (AA.Lam "_" <$>) <$> inferableTerm visited (unEl $ unAbs b)
114
113
    Sort {}     -> return . return $ AA.UNIT
115
114
    t           -> do