← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/full/Agda/Interaction/MakeCase.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, d5cf60f
  • Date: 2015-05-20 13:08:33 UTC
  • mfrom: (1.1.7)
  • Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237
Tags: 2.4.2.2-2
[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Interaction/MakeCase.hs
1
 
{-# LANGUAGE CPP #-}
 
1
{-# LANGUAGE CPP             #-}
2
2
{-# LANGUAGE DoAndIfThenElse #-}
3
 
{-# LANGUAGE TupleSections #-}
 
3
{-# LANGUAGE TupleSections   #-}
4
4
 
5
5
module Agda.Interaction.MakeCase where
6
6
 
12
12
 
13
13
import Agda.Syntax.Common
14
14
import Agda.Syntax.Position
 
15
import qualified Agda.Syntax.Concrete as C
15
16
import qualified Agda.Syntax.Abstract as A
16
17
import qualified Agda.Syntax.Info as A
17
18
import Agda.Syntax.Internal
 
19
import Agda.Syntax.Scope.Monad (resolveName, ResolvedName(..))
 
20
import Agda.Syntax.Translation.ConcreteToAbstract
18
21
import Agda.Syntax.Translation.InternalToAbstract
19
22
 
20
23
import Agda.TypeChecking.Monad
27
30
 
28
31
import Agda.Interaction.BasicOps
29
32
 
 
33
import Agda.Utils.Functor
30
34
import Agda.Utils.List
31
35
import Agda.Utils.Monad
32
36
import qualified Agda.Utils.Pretty as P
33
37
import Agda.Utils.Size
34
38
import qualified Agda.Utils.HashMap as HMap
35
39
 
36
 
#include "../undefined.h"
 
40
#include "undefined.h"
37
41
import Agda.Utils.Impossible
38
42
 
39
 
data CaseContext = FunctionDef | ExtendedLambda Int Int
40
 
                 deriving (Eq)
 
43
data CaseContext
 
44
  = FunctionDef
 
45
  | ExtendedLambda Int Int
 
46
  deriving (Eq)
 
47
 
41
48
-- | Find the clause whose right hand side is the given meta
42
49
-- BY SEARCHING THE WHOLE SIGNATURE. Returns
43
50
-- the original clause, before record patterns have been translated
82
89
      MetaV m' _  -> m == m'
83
90
      _           -> False
84
91
 
 
92
 
85
93
-- | Parse variables (visible or hidden), returning their de Bruijn indices.
86
94
--   Used in 'makeCase'.
 
95
 
87
96
parseVariables :: InteractionId -> Range -> [String] -> TCM [Int]
88
97
parseVariables ii rng ss = do
 
98
 
 
99
  -- Get into the context of the meta.
89
100
  mId <- lookupInteractionId ii
90
101
  updateMetaVarRange mId rng
91
102
  mi  <- getMetaInfo <$> lookupMeta mId
92
 
  enterClosure mi $ \ _r -> do
93
 
    n  <- getContextSize
94
 
    xs <- forM (downFrom n) $ \ i -> do
95
 
      (,i) . P.render <$> prettyTCM (var i)
96
 
    forM ss $ \ s -> do
97
 
      case lookup s xs of
98
 
        Nothing -> typeError $ GenericError $ "Unbound variable " ++ s
99
 
        Just i  -> return i
 
103
  enterClosure mi $ \ r -> do
 
104
 
 
105
  -- Get printed representation of variables in context.
 
106
  n  <- getContextSize
 
107
  xs <- forM (downFrom n) $ \ i -> do
 
108
    (,i) . P.render <$> prettyTCM (var i)
 
109
 
 
110
  -- Get number of module parameters.  These cannot be split on.
 
111
  fv <- getModuleFreeVars =<< currentModule
 
112
  let numSplittableVars = n - fv
 
113
 
 
114
  -- Resolve each string to a variable.
 
115
  forM ss $ \ s -> do
 
116
    let failNotVar = typeError $ GenericError $ "Not a (splittable) variable: " ++ s
 
117
        done i
 
118
          | i < numSplittableVars = return i
 
119
          | otherwise             = failNotVar
 
120
 
 
121
    -- Note: the range in the concrete name is only approximate.
 
122
    resName <- resolveName $ C.QName $ C.Name r $ C.stringNameParts s
 
123
    case resName of
 
124
 
 
125
      -- Fail if s is a name, but not of a variable.
 
126
      DefinedName{}       -> failNotVar
 
127
      FieldName{}         -> failNotVar
 
128
      ConstructorName{}   -> failNotVar
 
129
      PatternSynResName{} -> failNotVar
 
130
 
 
131
      -- If s is a variable name in scope, get its de Bruijn index
 
132
      -- via the type checker.
 
133
      VarName x -> do
 
134
        (v, _) <- getVarInfo x
 
135
        case ignoreSharing v of
 
136
          Var i [] -> done i
 
137
          _        -> failNotVar
 
138
 
 
139
      -- If s is not a name, compare it to the printed variable representation.
 
140
      -- This fallback is to enable splitting on hidden variables.
 
141
      UnknownName -> do
 
142
        case filter ((s ==) . fst) xs of
 
143
          []      -> typeError $ GenericError $ "Unbound variable " ++ s
 
144
          [(_,i)] -> done i
 
145
          -- Issue 1325: Variable names in context can be ambiguous.
 
146
          _       -> typeError $ GenericError $ "Ambiguous variable " ++ s
 
147
 
100
148
 
101
149
-- | Entry point for case splitting tactic.
102
150
makeCase :: InteractionId -> Range -> String -> TCM (CaseContext , [A.Clause])
116
164
  let vars = words s
117
165
  if null vars then do
118
166
    -- split result
119
 
    res <- splitResult f =<< fixTarget (clauseToSplitClause clause)
120
 
    case res of
121
 
      Nothing  -> typeError $ GenericError $ "Cannot split on result here"
122
 
      Just cov -> (casectxt,) <$> do mapM (makeAbstractClause f) $ splitClauses cov
 
167
    (newPats, sc) <- fixTarget (clauseToSplitClause clause)
 
168
    res <- splitResult f sc
 
169
    scs <- case res of
 
170
      Nothing  -> if newPats then return [sc] else
 
171
        typeError $ GenericError $ "Cannot split on result here"
 
172
      Just cov -> mapM (snd <.> fixTarget) $ splitClauses cov
 
173
    (casectxt,) <$> mapM (makeAbstractClause f) scs
123
174
  else do
124
175
    -- split on variables
125
176
    vars <- parseVariables hole rng vars