~ubuntu-branches/ubuntu/raring/agda/raring-proposed

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

Committer: Bazaar Package Importer
Author(s): Iain Lane
Date: 2010-01-05 23:43:20 UTC
mfrom: (1.1.1 upstream)
Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu

Tags: 2.2.6-1

http://bugs.debian.org/559197

* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian)
* debian/README.source: Remove, no repacking so not necessary any more
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed.
    (Closes: #559197).
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

files added:
doc/release-notes/2-2-6.txt

src/full/Agda/Auto

src/full/Agda/Auto/Auto.hs

src/full/Agda/Auto/Convert.hs

src/full/Agda/Auto/NarrowingSearch.hs

src/full/Agda/Auto/Print.hs

src/full/Agda/Auto/SearchControl.hs

src/full/Agda/Auto/Syntax.hs

src/full/Agda/Auto/Typecheck.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs-boot

src/full/Agda/Interaction/FindFile.hs

src/full/Agda/Interaction/FindFile.hs-boot

src/full/Agda/TypeChecking/Level.hs

src/full/Agda/TypeChecking/MetaVars

src/full/Agda/TypeChecking/MetaVars/Occurs.hs

src/full/Agda/Utils/IO

src/full/Agda/Utils/IO/Binary.hs

src/full/Agda/Utils/IO/Locale.hs

src/full/Agda/Utils/IO/UTF8.hs

files removed:
debian/README.source

src/full/Agda/Utils/IO.hs

src/full/Agda/Utils/Monad

src/full/Agda/Utils/Monad/Undo.hs

src/full/Agda/Utils/Serialise.hs

files modified:
Agda.cabal

README

debian/50agda.el

debian/changelog

debian/control

debian/copyright

dist/build/Agda/Syntax/Parser/Lexer.hs

dist/build/Agda/Syntax/Parser/Parser.hs

src/agda-mode/Main.hs

src/data/Agda.css

src/data/emacs-mode/agda-input.el

src/data/emacs-mode/agda2-abbrevs.el

src/data/emacs-mode/agda2-highlight.el

src/data/emacs-mode/agda2-mode.el

src/data/emacs-mode/annotation.el

src/full/Agda/Compiler/Agate/Common.hs

src/full/Agda/Compiler/Agate/OptimizedPrinter.hs

src/full/Agda/Compiler/Alonzo/Main.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs

src/full/Agda/Compiler/MAlonzo/Encode.hs

src/full/Agda/Compiler/MAlonzo/Misc.hs

src/full/Agda/Compiler/MAlonzo/Primitives.hs

src/full/Agda/Interaction/BasicOps.hs

src/full/Agda/Interaction/CommandLine/CommandLine.hs

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/GhciTop.hs

src/full/Agda/Interaction/Highlighting/Emacs.hs

src/full/Agda/Interaction/Highlighting/Generate.hs

src/full/Agda/Interaction/Highlighting/HTML.hs

src/full/Agda/Interaction/Highlighting/Precise.hs

src/full/Agda/Interaction/Highlighting/Vim.hs

src/full/Agda/Interaction/Imports.hs

src/full/Agda/Interaction/MakeCase.hs

src/full/Agda/Interaction/Monad.hs

src/full/Agda/Interaction/Options.hs

src/full/Agda/Main.hs

src/full/Agda/Syntax/Abstract.hs

src/full/Agda/Syntax/Abstract/Name.hs

src/full/Agda/Syntax/Common.hs

src/full/Agda/Syntax/Concrete.hs

src/full/Agda/Syntax/Concrete/Definitions.hs

src/full/Agda/Syntax/Concrete/Name.hs

src/full/Agda/Syntax/Concrete/Pretty.hs

src/full/Agda/Syntax/Info.hs

src/full/Agda/Syntax/Internal.hs

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Parser.hs

src/full/Agda/Syntax/Parser/LexActions.hs

src/full/Agda/Syntax/Parser/Lexer.x

src/full/Agda/Syntax/Parser/Monad.hs

src/full/Agda/Syntax/Parser/Parser.y

src/full/Agda/Syntax/Parser/Tokens.hs

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Strict.hs

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

src/full/Agda/TypeChecking/Conversion.hs-boot

src/full/Agda/TypeChecking/Errors.hs

src/full/Agda/TypeChecking/Free.hs

src/full/Agda/TypeChecking/Injectivity.hs

src/full/Agda/TypeChecking/MetaVars.hs

src/full/Agda/TypeChecking/MetaVars.hs-boot

src/full/Agda/TypeChecking/Monad/Base.hs

src/full/Agda/TypeChecking/Monad/Builtin.hs

src/full/Agda/TypeChecking/Monad/Debug.hs

src/full/Agda/TypeChecking/Monad/Imports.hs

src/full/Agda/TypeChecking/Monad/MetaVars.hs

src/full/Agda/TypeChecking/Monad/Options.hs

src/full/Agda/TypeChecking/Monad/Signature.hs

src/full/Agda/TypeChecking/Monad/SizedTypes.hs

src/full/Agda/TypeChecking/Monad/State.hs

src/full/Agda/TypeChecking/Pretty.hs

src/full/Agda/TypeChecking/Primitive.hs

src/full/Agda/TypeChecking/Records.hs

src/full/Agda/TypeChecking/Records.hs-boot

src/full/Agda/TypeChecking/Reduce.hs

src/full/Agda/TypeChecking/Rules/Builtin.hs

src/full/Agda/TypeChecking/Rules/Data.hs

src/full/Agda/TypeChecking/Rules/Decl.hs

src/full/Agda/TypeChecking/Rules/Def.hs

src/full/Agda/TypeChecking/Rules/LHS.hs

src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs

src/full/Agda/TypeChecking/Rules/LHS/Split.hs

src/full/Agda/TypeChecking/Rules/LHS/Unify.hs

src/full/Agda/TypeChecking/Rules/Record.hs

src/full/Agda/TypeChecking/Rules/Term.hs

src/full/Agda/TypeChecking/Serialise.hs

src/full/Agda/TypeChecking/SizedTypes.hs

src/full/Agda/TypeChecking/Substitute.hs

src/full/Agda/TypeChecking/Telescope.hs

src/full/Agda/TypeChecking/Test/Generators.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Impossible.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/QuickCheck.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/TestHelpers.hs

src/full/Agda/undefined.h

Show diffs side-by-side

added added

removed removed

src/full/Agda/Compiler/MAlonzo/Primitives.hs

module Agda.Compiler.MAlonzo.Primitives where

import Control.Monad.Reader

import Control.Monad.State

import Data.Char

import Data.List as L

import Data.Map as M

import Language.Haskell.Syntax

import {-# SOURCE #-} Agda.Compiler.MAlonzo.Compiler (term)

import Agda.Compiler.MAlonzo.Misc

import Agda.Compiler.MAlonzo.Pretty

import Agda.Syntax.Common

import Agda.Syntax.Internal

import Agda.TypeChecking.Monad

import Agda.TypeChecking.Monad.Builtin

import Agda.TypeChecking.Reduce

import Agda.TypeChecking.Substitute

import Agda.TypeChecking.Pretty

import Agda.Utils.Monad

forList toH toA = decls ["NIL", "CONS"]

toH (concat

["let { f <<0>> = [];"

," f (<<1>> x xs) = x : f (unsafeCoerce xs)"

," f (<<1>> x xs) = x : f (Unsafe.Coerce.unsafeCoerce xs)"

,"} in f"])

toA (concat

["let { f [] = <<0>>;"

," f (c:cs) = <<1>> c (unsafeCoerce (f cs));"

," f (c:cs) = <<1>> c (Unsafe.Coerce.unsafeCoerce (f cs));"

,"} in f"])

natToFrom hty to from = let

totxt = repl ["<<0>>", "<<1>>", hty] (concat

["let { f <<0>> = 0 :: <<2>>;"

," f (<<1>> x) = 1 + f (unsafeCoerce x);"

," f (<<1>> x) = 1 + f (Unsafe.Coerce.unsafeCoerce x);"

,"} in f"])

fromtxt = repl ["<<0>>", "<<1>>", hty] (concat

["let { f x | x <= (0 :: <<2>>) = <<0>>"

," | True = <<1>> (unsafeCoerce (f (x - 1)))"

," | True = <<1>> (Unsafe.Coerce.unsafeCoerce (f (x - 1)))"

,"} in f"])

in decls ["ZERO", "SUC"] to totxt from fromtxt

decls cs n1 b1 n2 b2 =

106

110

107

111

-- Definition bodies for primitive functions

108

112

primBody :: String -> TCM HsExp

109

primBody s = (hsVarUQ . HsIdent <$>) $ maybe unimplemented id $ L.lookup s $

113

primBody s = maybe unimplemented (either (hsVarUQ . HsIdent) id <$>) $

114

L.lookup s $

110

115

[

111

116

-- Integer functions

112

117

"primIntegerPlus" |-> binAsis "(+)" "Integer"

172

177

, "primStringAppend" |-> binAsis "(++)" "String"

173

178

, "primStringEquality" |-> rel "(==)" "String"

174

179

, "primShowString" |-> return "(show :: String -> String)"

180

181

-- Trust me

182

, ("primTrustMe" , Right <$> do

183

refl <- primRefl

184

flip runReaderT 0 $

185

term $ lam "A" (lam "x" (lam "y" (refl `apply` [var 2, var 1]))))

175

186

]

176

187

where

177

(|->) = (,)

188

x |-> s = (x, Left <$> s)

178

189

bin blt op ty from to = do

179

190

from' <- bltQual' blt from

180

191

to' <- bltQual' blt to

192

203

pred p = do toHB <- bltQual' "BOOL" mazHBoolToBool

193

204

return $ repl [p, toHB] $ "(\\ x -> <<1>> (<<0>> x))"

194

205

opty t = t ++ "->" ++ t ++ "->" ++ t

195

unimplemented = return$ prettyPrint$ rtmError$ "not yet implemented: "++ s

206

unimplemented = typeError $ NotImplemented s

207

208

lam x t = Lam Hidden (Abs x t)

209

var x = Arg Hidden (Var x [])

196

210

197

211

----------------------

198

212

Older »