← 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/Forcing.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/Forcing.hs
1
 
{-# LANGUAGE CPP, ScopedTypeVariables #-}
 
1
{-# LANGUAGE CPP #-}
 
2
{-# LANGUAGE ScopedTypeVariables #-}
 
3
 
2
4
module Agda.Compiler.Epic.Forcing where
3
5
 
4
6
import Control.Applicative
5
 
import Control.Arrow (first, second)
6
7
import Control.Monad
7
8
import Control.Monad.State
8
 
import Control.Monad.Trans
9
9
 
10
10
import Data.Char
11
11
import Data.List hiding (sort)
12
 
import qualified Data.Map as M
13
12
import Data.Maybe
14
13
 
15
14
import Agda.Syntax.Common
16
 
import qualified Agda.Syntax.Internal as SI
 
15
import qualified Agda.Syntax.Internal as I
17
16
import Agda.Syntax.Literal
18
17
import Agda.Syntax.Position(noRange)
19
18
import Agda.Syntax.Internal(Tele(..), Telescope, Term, Abs(..), unAbs, absName, Type, Args, QName, unEl)
20
19
import Agda.TypeChecking.Monad
 
20
import Agda.TypeChecking.Rules.LHS.Problem (FlexibleVars, defaultFlexibleVar)
21
21
import Agda.TypeChecking.Rules.LHS.Unify
22
 
import Agda.TypeChecking.Rules.LHS.Instantiate
23
22
import Agda.TypeChecking.Substitute
24
 
  (raiseFrom, raise, applySubst, apply, wkS, raiseS, dropS, (++#), TelV(..))
 
23
  (applySubst, apply, wkS, raiseS, dropS, (++#), TelV(..))
25
24
import qualified Agda.TypeChecking.Substitute as S
26
25
import Agda.TypeChecking.Pretty as P
27
26
import Agda.TypeChecking.Reduce
28
27
import Agda.TypeChecking.Telescope
29
28
import Agda.Utils.List
30
29
import Agda.Utils.Monad
31
 
import Agda.Utils.Permutation
32
30
import Agda.Utils.Size
33
31
import qualified Agda.Utils.HashMap as HM
34
32
 
41
39
#include "../../undefined.h"
42
40
import Agda.Utils.Impossible
43
41
 
44
 
 
45
42
-- | Returns how many parameters a datatype has
46
43
dataParameters :: QName -> Compile TCM Nat
47
44
dataParameters = lift . dataParametersTCM
102
99
      , text "term:" <+> prettyTCM term
103
100
      , text "to:"   <+> prettyTCM (unAbs to)
104
101
      ]
105
 
    (st, arg) <- case SI.unEl . unDom $ t' of
106
 
            SI.Def st arg -> return (st, arg)
 
102
    (st, arg) <- case I.unEl . unDom $ t' of
 
103
            I.Def st es -> return (st, fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es)
107
104
            s          -> do
108
105
              report 10 $ vcat
109
106
                [ text "ERROR!!!"
140
137
    (xs', typ) <- insertTele er (n - 1) ins term (unAbs xs)
141
138
    return (ExtendTel x $ Abs (absName xs) xs' , typ)
142
139
 
143
 
mkCon c n = SI.Con c [ defaultArg $ SI.Var (fromIntegral i) [] | i <- [n - 1, n - 2 .. 0] ]
 
140
-- TODO: restore fields in ConHead
 
141
mkCon c n = I.Con (I.ConHead c []) [ defaultArg $ I.Var (fromIntegral i) [] | i <- [n - 1, n - 2 .. 0] ]
144
142
 
145
 
unifyI :: Telescope -> [Nat] -> Type -> Args -> Args -> Compile TCM [Maybe Term]
 
143
unifyI :: Telescope -> FlexibleVars -> Type -> Args -> Args -> Compile TCM [Maybe Term]
146
144
unifyI tele flex typ a1 a2 = lift $ addCtxTel tele $ unifyIndices_ flex typ a1 a2
147
145
 
148
146
takeTele 0 _ = EmptyTel
188
186
        let n = fromMaybe __IMPOSSIBLE__ $ elemIndex x vars
189
187
        (Case v <$>) . forM brs $ \ br -> case br of
190
188
            BrInt i e -> do
191
 
              (tele'', _) <-  insertTele __IMPOSSIBLE__ n Nothing (SI.Lit (LitChar noRange (chr i))) tele
 
189
              (tele'', _) <-  insertTele __IMPOSSIBLE__ n Nothing (I.Lit (LitChar noRange (chr i))) tele
192
190
              BrInt i <$> forcedExpr (replaceAt n vars []) tele'' e
193
191
 
194
192
            Default e -> Default <$> rec e
205
203
                  else do
206
204
                    -- unify the telescope type with the return type of the constructor
207
205
                    unif <- case (unEl ntyp, unEl ctyp) of
208
 
                        (SI.Def st a1, SI.Def st' a2) | st == st' -> do
 
206
                        (I.Def st es1, I.Def st' es2) | st == st' -> do
 
207
                            let a1 = fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es1
 
208
                            let a2 = fromMaybe __IMPOSSIBLE__ $ I.allApplyElims es2
209
209
                            typPars <- dataParameters st
210
210
                            setType <- getType st
211
211
                            report 10 $ vcat
213
213
                              , text "ctyp:" <+> prettyTCM ctyp
214
214
                              ]
215
215
                            unifyI (takeTele (n + length as) tele'')
216
 
                                   [0 .. n + length as]
 
216
                                   (map defaultFlexibleVar [0 .. n + length as])
217
217
                                   (setType `apply` take typPars a1)
218
218
                                   (drop typPars a1)
219
219
                                   (drop typPars a2)
220
220
                        _ -> __IMPOSSIBLE__
221
221
                    let
222
222
                        lower = wkS (-1) . dropS 1
223
 
                        subT 0 tel = let ss = [fromMaybe (SI.Var n []) t
 
223
                        subT 0 tel = let ss = [fromMaybe (I.Var n []) t
224
224
                                                | (n , t) <- zip [0..] unif] ++#
225
225
                                              raiseS (length unif)
226
226
                                      in (applySubst ss tel, lower ss)
246
246
    rec = forcedExpr vars tele
247
247
 
248
248
-- | replace the forcedVar with pattern matching from the outside.
249
 
replaceForced :: ([Var],[Var]) -> Telescope -> [Var] -> [Maybe SI.Term] -> Expr -> Compile TCM Expr
 
249
replaceForced :: ([Var],[Var]) -> Telescope -> [Var] -> [Maybe I.Term] -> Expr -> Compile TCM Expr
250
250
replaceForced (vars,_) tele [] _ e = forcedExpr vars tele e
251
251
replaceForced (vars,uvars) tele (fvar : fvars) unif e = do
252
252
    let n = fromMaybe __IMPOSSIBLE__ $ elemIndex fvar uvars
253
253
    mpos <- findPosition n unif
254
254
    case mpos of
255
 
        Nothing -> case unif !! n of
 
255
        Nothing -> case fromMaybe __IMPOSSIBLE__ $ unif !!! n of
256
256
            Nothing | fvar `notElem` fv e ->
257
257
              replaceForced (vars, uvars) tele fvars unif e
258
258
            Nothing -> do
270
270
                subst fvar v <$> replaceForced (vars, uvars)
271
271
                                               tele fvars unif (Let v te e)
272
272
        Just (pos , term) -> do
273
 
            (build, v) <- buildTerm (uvars !! pos) n term
 
273
            (build, v) <- buildTerm (fromMaybe __IMPOSSIBLE__ $ uvars !!! pos) n term
274
274
            build . subst fvar v <$> replaceForced (vars, uvars) tele fvars unif
275
275
                                     e
276
276
  where
279
279
-- | Given a term containg the forced var, dig out the variable by inserting
280
280
-- the proper case-expressions.
281
281
buildTerm :: Var -> Nat -> Term -> Compile TCM (Expr -> Expr, Var)
282
 
buildTerm var idx (SI.Var i _) | idx == i = return (id, var)
283
 
buildTerm var idx (SI.Con c args) = do
 
282
buildTerm var idx (I.Var i _) | idx == i = return (id, var)
 
283
buildTerm var idx (I.Con con args) = do
 
284
    let c = I.conName con
284
285
    vs <- replicateM (length args) newName
285
286
    (pos , arg) <- fromMaybe __IMPOSSIBLE__ <$> findPosition idx (map (Just . unArg) args)
286
 
    (fun' , v) <- buildTerm (vs !! pos) idx arg
 
287
    (fun2 , v) <- buildTerm (fromMaybe __IMPOSSIBLE__ $ vs !!! pos) idx arg
287
288
    tag <- getConstrTag c
288
 
    let fun e = casee (Var var) [Branch tag c vs e]
289
 
    return (fun . fun' , v)
 
289
    let fun1 e = casee (Var var) [Branch tag c vs e]
 
290
    return (fun1 . fun2 , v)
290
291
buildTerm _ _ _ = __IMPOSSIBLE__
291
292
 
292
293
 
293
294
-- | Find the location where a certain Variable index is by searching the constructors
294
295
--   aswell. i.e find a term that can be transformed into a pattern that contains the
295
296
--   same value the index. This fails if no such term is present.
296
 
findPosition :: Nat -> [Maybe SI.Term] -> Compile TCM (Maybe (Nat, SI.Term))
 
297
findPosition :: Nat -> [Maybe I.Term] -> Compile TCM (Maybe (Nat, I.Term))
297
298
findPosition var ts = (listToMaybe . catMaybes <$>) . forM (zip [0..] ts) $ \ (n, mt) -> do
298
299
    ifM (maybe (return False) pred mt)
299
300
        (return (Just (n, fromMaybe __IMPOSSIBLE__ mt)))
301
302
  where
302
303
    pred :: Term -> Compile TCM Bool
303
304
    pred t = case t of
304
 
      SI.Var i _ | var == i -> return True
305
 
      SI.Con c args         -> do
306
 
          forc <- getForcedArgs c
 
305
      I.Var i _ | var == i -> return True
 
306
      I.Con c args         -> do
 
307
          forc <- getForcedArgs $ I.conName c
307
308
          or <$> mapM (pred . unArg) (notForced forc args)
308
309
      _                  -> return False