← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/With.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/TypeChecking/With.hs
1
 
{-# LANGUAGE CPP #-}
 
1
{-# LANGUAGE CPP           #-}
2
2
{-# LANGUAGE PatternGuards #-}
3
3
 
4
4
module Agda.TypeChecking.With where
35
35
import Agda.Utils.Permutation
36
36
import Agda.Utils.Size
37
37
 
38
 
#include "../undefined.h"
 
38
#include "undefined.h"
39
39
import Agda.Utils.Impossible
40
40
 
41
41
-- showPat moved to TypeChecking.Pretty as prettyTCM instance
48
48
    reportSDoc "tc.with.abstract" 20 $ text "  vs = " <+> prettyTCM vs
49
49
    as <- etaContract =<< normalise as
50
50
    reportSDoc "tc.with.abstract" 20 $ text "  as = " <+> prettyTCM as
51
 
    reportSDoc "tc.with.abstract" 30 $ text "normalizing b = " <+> prettyTCM (telePi_ delta2 b)
52
 
    b  <- normalise (telePi_ delta2 b)
 
51
    b <- return $ telePi_ delta2 b
 
52
    reportSDoc "tc.with.abstract" 30 $ text "normalizing b = " <+> prettyTCM b
 
53
    b  <- normalise b
53
54
    reportSDoc "tc.with.abstract" 30 $ text "eta-contracting b = " <+> prettyTCM b
54
55
    b  <- etaContract b
55
56
    reportSDoc "tc.with.abstract" 20 $ text "  b  = " <+> prettyTCM b
376
377
patsToTerms :: Permutation -> [I.NamedArg Pattern] -> [I.Arg DisplayTerm]
377
378
patsToTerms perm ps = evalState (toTerms ps) xs
378
379
  where
379
 
    xs   = permute (invertP perm) $ downFrom (size perm)
 
380
    xs   = permute (invertP __IMPOSSIBLE__ perm) $ downFrom (size perm)
380
381
    tick = do x : xs <- get; put xs; return x
381
382
 
382
383
    toTerms :: [I.NamedArg Pattern] -> State [Nat] [I.Arg DisplayTerm]
387
388
      ProjP d     -> __IMPOSSIBLE__ -- TODO: convert spine to non-spine ... DDef d . defaultArg
388
389
      VarP _      -> DTerm . var <$> tick
389
390
      DotP t      -> DDot t <$ tick
390
 
      ConP c _ ps -> DCon (conName c) <$> toTerms ps
 
391
      ConP c _ ps -> DCon c <$> toTerms ps
391
392
      LitP l      -> return $ DTerm (Lit l)
392
393
 
393
394
{- OLD