← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/Compiler/MAlonzo/Misc.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
  • Date: 2013-04-10 11:46:43 UTC
  • mfrom: (4.1.5 experimental)
  • Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn
Tags: 2.3.2-1
[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
  Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
  removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/full/Agda/Compiler/MAlonzo/Misc.hs
3
3
module Agda.Compiler.MAlonzo.Misc where
4
4
 
5
5
import Control.Monad.State
6
 
import Data.Generics
7
6
import Data.List as L
8
7
import Data.Map as M
9
8
import Data.Set as S
11
10
import Data.Function
12
11
import qualified Language.Haskell.Exts.Syntax as HS
13
12
import System.IO
14
 
import System.Time
15
13
 
16
14
import Agda.Interaction.Imports
17
15
import Agda.Syntax.Common
85
83
ihname s i = HS.Ident $ s ++ show i
86
84
 
87
85
unqhname :: String -> QName -> HS.Name
 
86
{- NOT A GOOD IDEA, see Issue 728
88
87
unqhname s q | ("d", "main") == (s, show(qnameName q)) = HS.Ident "main"
89
88
             | otherwise = ihname s (idnum $ nameId $ qnameName $ q)
90
 
  where idnum (NameId x _) = fromIntegral x
 
89
-}
 
90
unqhname s q = ihname s (idnum $ nameId $ qnameName $ q)
 
91
   where idnum (NameId x _) = fromIntegral x
91
92
 
92
93
-- the toplevel module containing the given one
93
94
tlmodOf :: ModuleName -> TCM HS.ModuleName
124
125
 
125
126
-- qualify name s by the module of builtin b
126
127
bltQual :: String -> String -> TCM HS.QName
127
 
bltQual b s = do (Def q _) <- getBuiltin b; xqual q (HS.Ident s)
 
128
bltQual b s = do
 
129
  Def q _ <- ignoreSharing <$> getBuiltin b
 
130
  xqual q (HS.Ident s)
128
131
 
129
132
-- sub-naming for cascaded definitions for concsecutive clauses
130
133
dsubname q i | i == 0    = unqhname "d"                     q
187
190
 
188
191
dummy :: a
189
192
dummy = error "MAlonzo : this dummy value should not have been eval'ed."
190
 
 
191
 
 
192
 
--------------------------------------------------
193
 
--------------------------------------------------
194
 
gshow' :: Data a => a -> String
195
 
gshow' = ( \t ->
196
 
           "("
197
 
           ++ showConstr (toConstr t)
198
 
           ++ concat (gmapQ ((++) " " . gshow') t)
199
 
           ++ ")" )
200
 
         `extQ` (show :: String -> String)
201
 
         `extQ` (show :: Name -> String)
202
 
         `extQ` (show :: QName -> String)
203
 
         `extQ` (show :: ModuleName -> String)
204
 
         `extQ` (gshow' . M.toList :: M.Map QName [AbstractName] -> String)
205
 
         `extQ` (gshow' . M.toList :: M.Map QName [AbstractModule] -> String)
206
 
         `extQ` (gshow' . M.toList :: M.Map ModuleName Section -> String)
207
 
         `extQ` (gshow' . M.toList :: M.Map QName Definition -> String)
208
 
         `extQ` (gshow' . M.toList :: M.Map TermHead [Pattern] -> String)
209
 
         `extQ` (gshow' . M.toList :: M.Map TermHead [Arg Pattern] -> String)
210
 
         `extQ` (gshow' . M.toList :: M.Map String (Builtin String) -> String)
211
 
         `extQ` (show :: Scope -> String)