idris 0.9.14.3 → 0.9.15

raw patch · 190 files changed

+4342/−5336 lines, 190 filesdep −Cabaldep −language-javadep −llvm-generaldep ~Win32dep ~annotated-wl-pprintdep ~ansi-terminalsetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: Cabal, language-java, llvm-general, llvm-general-pure

Dependency ranges changed: Win32, annotated-wl-pprint, ansi-terminal, ansi-wl-pprint, base, base64-bytestring, binary, blaze-html, bytestring, cheapskate, containers, deepseq, directory, filepath, fingertree, haskeline, hscurses, lens, libffi, mtl, network, optparse-applicative, pretty, process, split, text, time, transformers, trifecta, unix, unordered-containers, utf8-string, vector, vector-binary-instances, xml, zlib

API changes (from Hackage documentation)

Files

• Setup.hs +0/−19
• codegen/idris-c/Main.hs +0/−44
• config.mk +4/−1
• idris.cabal +89/−77
• jsrts/Runtime-common.js +9/−1
• libs/base/Control/Isomorphism.idr +58/−58
• libs/base/Control/Isomorphism/Primitives.idr +4/−4
• libs/base/Control/Monad/RWS.idr +19/−19
• libs/base/Data/Bits.idr +2/−2
• libs/base/Data/BoundedList.idr +5/−5
• libs/base/Data/Buffer.idr +2/−2
• libs/base/Data/HVect.idr +9/−9
• libs/base/Data/Hash.idr +85/−0
• libs/base/Data/Heap.idr +10/−10
• libs/base/Data/List.idr +13/−5
• libs/base/Data/Vect.idr +3/−3
• libs/base/Data/Vect/Quantifiers.idr +27/−5
• libs/base/Data/ZZ.idr +31/−22
• libs/base/Decidable/Order.idr +54/−65
• libs/base/Language/Reflection.idr +11/−9
• libs/base/Network/Socket.idr +51/−37
• libs/base/Syntax/PreorderReasoning.idr +3/−3
• libs/base/System/Concurrency/Process.idr +13/−13
• libs/base/base.ipkg +1/−1
• libs/effects/Effect/Memory.idr +12/−12
• libs/effects/Effects.idr +3/−5
• libs/prelude/Builtins.idr +37/−19
• libs/prelude/Decidable/Equality.idr +63/−63
• libs/prelude/Prelude.idr +11/−3
• libs/prelude/Prelude/Algebra.idr +54/−2
• libs/prelude/Prelude/Basics.idr +5/−3
• libs/prelude/Prelude/Bool.idr +5/−4
• libs/prelude/Prelude/Classes.idr +15/−0
• libs/prelude/Prelude/Either.idr +6/−6
• libs/prelude/Prelude/Fin.idr +46/−46
• libs/prelude/Prelude/Foldable.idr +2/−2
• libs/prelude/Prelude/List.idr +129/−28
• libs/prelude/Prelude/Maybe.idr +1/−1
• libs/prelude/Prelude/Nat.idr +116/−110
• libs/prelude/Prelude/Pairs.idr +6/−6
• libs/prelude/Prelude/Stream.idr +12/−0
• libs/prelude/Prelude/Strings.idr +2/−2
• libs/prelude/Prelude/Uninhabited.idr +3/−3
• libs/prelude/Prelude/Vect.idr +114/−67
• llvm/Makefile +0/−25
• llvm/defs.c +0/−182
• main/Main.hs +6/−3
• rts/arduino/idris_main.c +29/−0
• rts/idris_bitstring.c +217/−89
• rts/idris_gc.c +3/−1
• rts/idris_rts.c +2/−1
• rts/idris_rts.h +7/−0
• rts/idris_stats.h +2/−2
• src/IRTS/CodegenC.hs +4/−2
• src/IRTS/CodegenCommon.hs +0/−1
• src/IRTS/CodegenJava.hs +0/−757
• src/IRTS/CodegenJavaScript.hs +4/−0
• src/IRTS/CodegenLLVM.hs +0/−1320
• src/IRTS/Compiler.hs +1/−10
• src/IRTS/DumpBC.hs +1/−1
• src/IRTS/Java/ASTBuilding.hs +0/−141
• src/IRTS/Java/JTypes.hs +0/−331
• src/IRTS/Java/Mangling.hs +0/−116
• src/IRTS/Java/Pom.hs +0/−95
• src/IRTS/Lang.hs +1/−1
• src/Idris/AbsSyntax.hs +101/−47
• src/Idris/AbsSyntaxTree.hs +94/−105
• src/Idris/Apropos.hs +2/−3
• src/Idris/Chaser.hs +5/−1
• src/Idris/CmdOptions.hs +6/−3
• src/Idris/Core/Binary.hs +171/−1
• src/Idris/Core/Constraints.hs +12/−10
• src/Idris/Core/Elaborate.hs +2/−0
• src/Idris/Core/Evaluate.hs +29/−8
• src/Idris/Core/Execute.hs +6/−2
• src/Idris/Core/ProofState.hs +6/−6
• src/Idris/Core/TT.hs +16/−8
• src/Idris/Core/Unify.hs +8/−2
• src/Idris/Coverage.hs +7/−7
• src/Idris/DataOpts.hs +1/−1
• src/Idris/DeepSeq.hs +29/−30
• src/Idris/Delaborate.hs +51/−33
• src/Idris/Docs.hs +21/−19
• src/Idris/Docstrings.hs +242/−69
• src/Idris/Elab/Class.hs +4/−3
• src/Idris/Elab/Clause.hs +179/−104
• src/Idris/Elab/Data.hs +23/−19
• src/Idris/Elab/Instance.hs +8/−7
• src/Idris/Elab/Provider.hs +1/−1
• src/Idris/Elab/Record.hs +2/−2
• src/Idris/Elab/Transform.hs +99/−0
• src/Idris/Elab/Type.hs +17/−7
• src/Idris/Elab/Utils.hs +35/−1
• src/Idris/Elab/Value.hs +25/−2
• src/Idris/ElabDecls.hs +8/−38
• src/Idris/ElabQuasiquote.hs +125/−122
• src/Idris/ElabTerm.hs +80/−81
• src/Idris/Erasure.hs +4/−7
• src/Idris/Error.hs +0/−1
• src/Idris/Help.hs +5/−1
• src/Idris/IBC.hs +94/−82
• src/Idris/IdeSlave.hs +22/−1
• src/Idris/IdrisDoc.hs +7/−7
• src/Idris/Interactive.hs +1/−1
• src/Idris/Output.hs +125/−4
• src/Idris/ParseData.hs +34/−19
• src/Idris/ParseExpr.hs +19/−15
• src/Idris/ParseHelpers.hs +6/−4
• src/Idris/ParseOps.hs +5/−6
• src/Idris/Parser.hs +53/−29
• src/Idris/PartialEval.hs +169/−35
• src/Idris/Primitives.hs +9/−0
• src/Idris/Prover.hs +1/−1
• src/Idris/REPL.hs +189/−64
• src/Idris/REPLParser.hs +361/−175
• src/Idris/Transforms.hs +81/−39
• src/Idris/TypeSearch.hs +10/−9
• src/Idris/Unlit.hs +4/−2
• src/Pkg/Package.hs +7/−4
• src/Util/LLVMStubs.hs +0/−24
• src/Util/System.hs +0/−1
• test/Makefile +1/−1
• test/basic001/basic001a.idr +1/−1
• test/basic001/reg005.idr +2/−2
• test/basic005/test019.lidr +6/−6
• test/basic009/Faulty.idr +1/−1
• test/basic009/Main.idr +4/−4
• test/basic010/Main.idr +2/−2
• test/basic011/basic011.idr +16/−0
• test/basic011/expected +10/−0
• test/basic011/run +4/−0
• test/dsl001/test001.idr +3/−3
• test/dsl002/Resimp.idr +2/−2
• test/dsl003/DSLPi.idr +5/−5
• test/dsl003/expected +2/−2
• test/effects002/test025.idr +6/−6
• test/error004/FunErrTest.idr +3/−3
• test/ffi002/test023.idr +2/−2
• test/ffi005/Postulate.idr +1/−1
• test/interactive001/expected +1/−1
• test/interactive005/expected +34/−0
• test/interactive005/input +26/−0
• test/interactive005/interactive005.idr +3/−0
• test/interactive005/run +6/−0
• test/interactive006/expected +2/−0
• test/interactive006/input +1/−0
• test/interactive006/interactive006.idr +3/−0
• test/interactive006/run +3/−0
• test/io003/test018a.idr +5/−5
• test/primitives002/expected +2/−0
• test/primitives002/run +1/−0
• test/primitives003/test038.idr +5/−5
• test/proof001/test029.idr +2/−2
• test/proof002/Reflect.idr +9/−9
• test/proof003/test015.idr +1/−1
• test/quasiquote001/expected +3/−3
• test/quasiquote003/NoInfer.idr +2/−2
• test/quasiquote004/Quasiquote004.idr +1/−1
• test/reg002/reg002.idr +6/−6
• test/reg006/reg006.idr +3/−3
• test/reg007/reg007.lidr +1/−1
• test/reg009/reg009.lidr +6/−6
• test/reg012/reg012.lidr +13/−13
• test/reg017/reg017.idr +2/−2
• test/reg018/reg018d.idr +3/−3
• test/reg025/reg025.idr +7/−7
• test/reg026/reg026.idr +1/−1
• test/reg034/reg034.idr +2/−2
• test/reg035/reg035.idr +2/−2
• test/reg035/reg035a.lidr +7/−7
• test/reg035/reg035b.idr +1/−1
• test/reg041/ott.idr +1/−1
• test/reg044/reg044.idr +1/−1
• test/reg047/reg047.idr +3/−3
• test/reg047/reg047a.idr +4/−4
• test/reg048/test.idr +0/−26
• test/reg049/expected +1/−1
• test/reg049/reg049.idr +2/−2
• test/reg052/expected +1/−0
• test/reg052/reg052.idr +8/−0
• test/reg052/run +4/−0
• test/reg053/expected +0/−0
• test/reg053/four.idr +9/−0
• test/reg053/run +3/−0
• test/totality002/test017.idr +3/−3
• test/totality002/test017b.idr +1/−1
• test/totality006/expected +1/−1
• test/totality006/totality006.idr +6/−6
• test/totality006/totality006a.idr +6/−6
• test/tutorial004/tutorial004.idr +10/−10

@@ -50,13 +50,6 @@ -- ----------------------------------------------------------------------------- -- Flags -usesLLVM :: S.ConfigFlags -> Bool-usesLLVM flags =-  case lookup (FlagName "llvm") (S.configConfigurationsFlags flags) of-    Just True -> True-    Just False -> False-    Nothing -> True- usesGMP :: S.ConfigFlags -> Bool usesGMP flags =   case lookup (FlagName "gmp") (S.configConfigurationsFlags flags) of@@ -82,15 +75,12 @@  idrisClean _ flags _ _ = do       cleanStdLib-      cleanLLVM    where       verbosity = S.fromFlag $ S.cleanVerbosity flags        cleanStdLib = do          makeClean "libs" -      cleanLLVM = makeClean "llvm"-       makeClean dir = make verbosity [ "-C", dir, "clean", "IDRIS=idris" ]  @@ -189,7 +179,6 @@ idrisBuild _ flags _ local = do       buildStdLib       buildRTS-      when (usesLLVM $ configFlags local) buildLLVM    where       verbosity = S.fromFlag $ S.buildVerbosity flags @@ -202,8 +191,6 @@       buildRTS = make verbosity (["-C", "rts", "build"] ++                                     gmpflag (usesGMP (configFlags local))) -      buildLLVM = make verbosity ["-C", "llvm", "build"]-       gmpflag False = []       gmpflag True = ["GMP=-DIDRIS_GMP"] @@ -215,7 +202,6 @@ idrisInstall verbosity copy pkg local = do       installStdLib       installRTS-      when (usesLLVM $ configFlags local) installLLVM    where       target = datadir $ L.absoluteInstallDirs pkg local copy @@ -227,11 +213,6 @@          let target' = target </> "rts"          putStrLn $ "Installing run time system in " ++ target'          makeInstall "rts" target'--      installLLVM = do-         let target' = target </> "llvm"-         putStrLn $ "Installing LLVM library in " ++ target-         makeInstall "llvm" target'        makeInstall src target =          make verbosity [ "-C", src, "install" , "TARGET=" ++ target, "IDRIS=" ++ idrisCmd local]

@@ -1,44 +0,0 @@-module Main where--import Idris.Core.TT-import Idris.AbsSyntax-import Idris.ElabDecls-import Idris.REPL--import IRTS.Compiler-import IRTS.CodegenC--import System.Environment-import System.Exit--import Paths_idris--data Opts = Opts { inputs :: [FilePath],-                   output :: FilePath }--showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"-               exitWith ExitSuccess--getOpts :: IO Opts-getOpts = do xs <- getArgs-             return $ process (Opts [] "a.out") xs-  where-    process opts ("-o":o:xs) = process (opts { output = o }) xs-    process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs-    process opts [] = opts--c_main :: Opts -> Idris ()-c_main opts = do elabPrims-                 loadInputs (inputs opts) Nothing-                 mainProg <- elabMain-                 ir <- compile (Via "c") (output opts) mainProg-                 runIO $ codegenC ir--main :: IO ()-main = do opts <- getOpts-          if (null (inputs opts)) -             then showUsage-             else runMain (c_main opts)---

@@ -1,6 +1,9 @@ CC              ?=cc CABAL           :=cabal-CFLAGS          :=-O2 -Wall -DHAS_PTHREAD $(CFLAGS)+# IDRIS_ENABLE_STATS should not be set in final release+# Any flags defined here which alter the RTS API must also be added to src/IRTS/CodegenC.hs+CFLAGS          :=-O2 -Wall -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS)+ #CABALFLAGS	:= ## Disable building of Effects #CABALFLAGS :=-f NoEffects

@@ -1,5 +1,5 @@ Name:           idris-Version:        0.9.14.3+Version:        0.9.15 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -52,12 +52,28 @@                        jsrts/Runtime-node.js                        jsrts/jsbn/jsbn.js                        jsrts/jsbn/LICENSE+                       rts/arduino/idris_main.c+                       rts/idris_bitstring.c+                       rts/idris_bitstring.h+                       rts/idris_gc.c                        rts/idris_gc.h+                       rts/idris_gmp.c                        rts/idris_gmp.h+                       rts/idris_heap.c+                       rts/idris_heap.h                        rts/idris_main.c-                       rts/idris_rts.h+                       rts/idris_net.c                        rts/idris_net.h+                       rts/idris_opts.c+                       rts/idris_opts.h+                       rts/idris_rts.c+                       rts/idris_rts.h+                       rts/idris_stats.c+                       rts/idris_stats.h+                       rts/idris_stdfgn.c                        rts/idris_stdfgn.h+                       rts/mini-gmp.c+                       rts/mini-gmp.h                        rts/libtest.c  Extra-source-files:@@ -66,6 +82,7 @@                         rts/*.c                        rts/*.h+                       rts/arduino/*.c                        rts/windows/*.c                        rts/Makefile @@ -100,9 +117,6 @@                        libs/effects/Effect/*.idr                        libs/effects/*.idr -                       llvm/*.c-                       llvm/Makefile-                        test/Makefile                        test/runtest.pl                        test/reg001/run@@ -253,6 +267,12 @@                        test/reg051/run                        test/reg051/*.idr                        test/reg051/expected+                       test/reg052/run+                       test/reg052/*.idr+                       test/reg052/expected+                       test/reg053/run+                       test/reg053/*.idr+                       test/reg053/expected                         test/basic001/run                        test/basic001/*.idr@@ -285,6 +305,9 @@                        test/basic010/run                        test/basic010/*.idr                        test/basic010/expected+                       test/basic011/run+                       test/basic011/*.idr+                       test/basic011/expected                         test/buffer001-disabled/*.idr                        test/buffer001-disabled/run@@ -391,6 +414,14 @@                        test/interactive004/input                        test/interactive004/*.idr                        test/interactive004/expected+                       test/interactive005/run+                       test/interactive005/input+                       test/interactive005/*.idr+                       test/interactive005/expected+                       test/interactive006/run+                       test/interactive006/input+                       test/interactive006/*.idr+                       test/interactive006/expected                         test/io001/run                        test/io001/*.idr@@ -521,11 +552,6 @@   type:     git   location: git://github.com/idris-lang/Idris-dev.git -Flag LLVM-  Description:  Build the LLVM backend-  Default:      False-  manual:       True- Flag FFI   Description:  Build support for libffi   Default:      False@@ -578,6 +604,7 @@                 , Idris.Elab.Class                 , Idris.Elab.Instance                 , Idris.Elab.Provider+                , Idris.Elab.Transform                 , Idris.Elab.Value                  , Idris.AbsSyntax@@ -631,17 +658,12 @@                 , IRTS.Bytecode                 , IRTS.CodegenC                 , IRTS.CodegenCommon-                , IRTS.CodegenJava                 , IRTS.CodegenJavaScript                 , IRTS.JavaScript.AST                 , IRTS.Compiler                 , IRTS.Defunctionalise                 , IRTS.DumpBC                 , IRTS.Inliner-                , IRTS.Java.ASTBuilding-                , IRTS.Java.JTypes-                , IRTS.Java.Mangling-                , IRTS.Java.Pom                 , IRTS.Lang                 , IRTS.LangOpts                 , IRTS.Simplified@@ -650,10 +672,10 @@                 , Pkg.Package                 , Util.DynamicLinker                 , Util.ScreenSize+                , Util.System    Other-modules:                   Util.Pretty-                , Util.System                 , Util.Net                 , Util.Zlib @@ -664,42 +686,39 @@                 , Version_idris    Build-depends:  base >=4 && <5-                , Cabal-                , annotated-wl-pprint >= 0.5.3-                , ansi-terminal-                , ansi-wl-pprint-                , base64-bytestring-                , binary-                , blaze-html >= 0.6.1.3+                , annotated-wl-pprint >= 0.5.3 && < 0.6+                , ansi-terminal < 0.7+                , ansi-wl-pprint < 0.7+                , base64-bytestring < 1.1+                , binary >= 0.7 && < 0.8+                , blaze-html >= 0.6.1.3 && < 0.8                 , blaze-markup >= 0.5.2.1 && < 0.7.0.0-                , bytestring-                , cheapskate-                , containers >= 0.5-                , directory-                , directory >= 1.2-                , filepath-                , fingertree >= 0.1-                , haskeline >= 0.7-                , language-java >= 0.2.6-                , lens >= 4.1.1-                , mtl+                , bytestring < 0.11+                , cheapskate < 0.2+                , containers >= 0.5 && < 0.6+                , deepseq < 1.4+                , directory >= 1.2 && < 1.3+                , filepath < 1.4+                , fingertree >= 0.1 && < 0.2+                , haskeline >= 0.7 && < 0.8+                , lens >= 4.1.1 && < 4.5+                , mtl < 2.3+                , network < 2.7+                , optparse-applicative >= 0.11 && < 0.12                 , parsers >= 0.9 && < 0.13-                , pretty-                , process-                , split-                , text-                , time >= 1.4-                , transformers-                , trifecta >= 1.1-                , unordered-containers-                , utf8-string-                , vector-                , vector-binary-instances-                , network-                , xml-                , deepseq-                , zlib-                , optparse-applicative >= 0.10+                , pretty < 1.2+                , process < 1.3+                , split < 0.3+                , text < 1.3+                , time >= 1.4 && < 1.6+                , transformers < 0.5+                , trifecta >= 1.1 && < 1.6+                , unordered-containers < 0.3+                , utf8-string < 0.4+                , vector < 0.11+                , vector-binary-instances < 0.3+                , xml < 1.4+                , zlib < 0.6   Extensions:     MultiParamTypeClasses                 , DeriveFoldable                 , DeriveTraversable@@ -713,34 +732,27 @@    if os(linux)      cpp-options:   -DLINUX-     build-depends: unix+     build-depends: unix < 2.8   if os(freebsd)      cpp-options:   -DFREEBSD-     build-depends: unix+     build-depends: unix < 2.8 --   if os(dragonfly) --      cpp-options:   -DDRAGONFLY---      build-depends: unix+--      build-depends: unix < 2.8   if os(darwin)      cpp-options:   -DMACOSX-     build-depends: unix+     build-depends: unix < 2.8   if os(windows)      cpp-options:   -DWINDOWS-     build-depends: Win32-  if flag(LLVM)-     other-modules: IRTS.CodegenLLVM-     cpp-options:   -DIDRIS_LLVM-     build-depends: llvm-general == 3.3.8.*-                  , llvm-general-pure == 3.3.8.*-  else-     other-modules: Util.LLVMStubs+     build-depends: Win32 < 2.4   if flag(FFI)-     build-depends: libffi+     build-depends: libffi < 0.2      cpp-options:   -DIDRIS_FFI   if flag(GMP)-     build-depends: libffi+     build-depends: libffi < 0.2      cpp-options:   -DIDRIS_GMP   if flag(curses)-     build-depends: hscurses+     build-depends: hscurses < 1.5      cpp-options:   -DCURSES   if flag(freestanding)      other-modules: Target_idris@@ -759,18 +771,18 @@   ghc-prof-options: -auto-all -caf-all   ghc-options:      -threaded -rtsopts -funbox-strict-fields -Executable idris-c-  Main-is:        Main.hs-  hs-source-dirs: codegen/idris-c--  Build-depends:  idris-                , base-                , filepath-                , haskeline >= 0.7-                , transformers--  ghc-prof-options: -auto-all -caf-all-  ghc-options:      -threaded -rtsopts -funbox-strict-fields+-- Executable idris-c+--   Main-is:        Main.hs+--   hs-source-dirs: codegen/idris-c+-- +--   Build-depends:  idris+--                 , base+--                 , filepath+--                 , haskeline >= 0.7+--                 , transformers+-- +--   ghc-prof-options: -auto-all -caf-all+--   ghc-options:      -threaded -rtsopts -funbox-strict-fields  Executable idris-javascript   Main-is:        Main.hs

@@ -16,6 +16,14 @@ var i$ret; var i$callstack; +var i$Int = {};+var i$String = {};+var i$Integer = {};+var i$Float = {};+var i$Char = {};+var i$Ptr = {};+var i$Forgot = {};+ /** @constructor */ var i$CON = function(tag,args,app,ev) {   this.tag = tag;@@ -59,7 +67,7 @@      var res = fid; -    for(var i = 0; i < arguments.length; ++i) {+    for(var i = 0; i < (arguments.length ? arguments.length : 1); ++i) {       while (res instanceof i$CON) {         i$valstack_top += 1;         i$valstack[i$valstack_top] = res;

@@ -14,9 +14,9 @@  -- Isomorphism properties -||| Isomorphism is reflexive+||| Isomorphism is Reflexive isoRefl : Iso a a-isoRefl = MkIso id id (\x => refl) (\x => refl)+isoRefl = MkIso id id (\x => Refl) (\x => Refl)  ||| Isomorphism is transitive isoTrans : Iso a b -> Iso b c -> Iso a c@@ -43,8 +43,8 @@         swap (Left x) = Right x         swap (Right x) = Left x         swapSwap : (e : Either a' b') -> swap (swap e) = e-        swapSwap (Left x) = refl-        swapSwap (Right x) = refl+        swapSwap (Left x) = Refl+        swapSwap (Right x) = Refl  ||| Disjunction is associative eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))@@ -60,31 +60,31 @@         eitherAssoc2 (Right (Right x)) = Right x          ok1 : (x : Either a (Either b c)) -> eitherAssoc1 (eitherAssoc2 x) = x-        ok1 (Left x) = refl-        ok1 (Right (Left x)) = refl-        ok1 (Right (Right x)) = refl+        ok1 (Left x) = Refl+        ok1 (Right (Left x)) = Refl+        ok1 (Right (Right x)) = Refl          ok2 : (x : Either (Either a b) c) -> eitherAssoc2 (eitherAssoc1 x) = x-        ok2 (Left (Left x)) = refl-        ok2 (Left (Right x)) = refl-        ok2 (Right x) = refl+        ok2 (Left (Left x)) = Refl+        ok2 (Left (Right x)) = Refl+        ok2 (Right x) = Refl  ||| Disjunction with false is a no-op-eitherBotLeft : Iso (Either _|_ a) a+eitherBotLeft : Iso (Either Void a) a eitherBotLeft = MkIso to from ok1 ok2-  where to : Either _|_ a -> a-        to (Left x) = FalseElim x+  where to : Either Void a -> a+        to (Left x) = void x         to (Right x) = x-        from : a -> Either _|_ a+        from : a -> Either Void a         from = Right         ok1 : (x : a) -> to (from x) = x-        ok1 x = refl-        ok2 : (x : Either _|_ a) -> from (to x) = x-        ok2 (Left x) = FalseElim x-        ok2 (Right x) = refl+        ok1 x = Refl+        ok2 : (x : Either Void a) -> from (to x) = x+        ok2 (Left x) = void x+        ok2 (Right x) = Refl  ||| Disjunction with false is a no-op-eitherBotRight : Iso (Either a _|_) a+eitherBotRight : Iso (Either a Void) a eitherBotRight = isoTrans eitherComm eitherBotLeft  ||| Isomorphism is a congruence with regards to disjunction@@ -119,7 +119,7 @@         swap (x, y) = (y, x)          swapSwap : (x : (a', b')) -> swap (swap x) = x-        swapSwap (x, y) = refl+        swapSwap (x, y) = Refl  ||| Conjunction is associative pairAssoc : Iso (a, (b, c)) ((a, b), c)@@ -130,26 +130,26 @@     from : ((a, b), c) -> (a, (b, c))     from ((x, y), z) = (x, (y, z))     ok1 : (x : ((a, b), c)) -> to (from x) = x-    ok1 ((x, y), z) = refl+    ok1 ((x, y), z) = Refl     ok2 : (x : (a, (b, c))) -> from (to x) = x-    ok2 (x, (y, z)) = refl+    ok2 (x, (y, z)) = Refl  ||| Conjunction with truth is a no-op pairUnitRight : Iso (a, ()) a-pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok+pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok   where ok : (x : (a, ())) -> (fst x, ()) = x-        ok (x, ()) = refl+        ok (x, ()) = Refl  ||| Conjunction with truth is a no-op pairUnitLeft : Iso ((), a) a pairUnitLeft = isoTrans pairComm pairUnitRight  ||| Conjunction preserves falsehood-pairBotLeft : Iso (_|_, a) _|_-pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))+pairBotLeft : Iso (Void, a) Void+pairBotLeft = MkIso fst void (\x => void x) (\y => void (fst y))  ||| Conjunction preserves falsehood-pairBotRight : Iso (a, _|_) _|_+pairBotRight : Iso (a, Void) Void pairBotRight = isoTrans pairComm pairBotLeft  ||| Isomorphism is a congruence with regards to conjunction@@ -165,11 +165,11 @@           iso1 : (x : (a', b')) -> to'' (from'' x) = x           iso1 (x, y) = rewrite toFrom x in                         rewrite toFrom' y in-                        refl+                        Refl           iso2 : (x : (a, b)) -> from'' (to'' x) = x           iso2 (x, y) = rewrite fromTo x in                         rewrite fromTo' y in-                        refl+                        Refl  ||| Isomorphism is a congruence with regards to conjunction on the left pairCongLeft : Iso a a' -> Iso (a, b) (a', b)@@ -190,11 +190,11 @@         from (Left (x, y)) = (Left x, y)         from (Right (x, y)) = (Right x, y)         toFrom : (x : Either (a, c) (b, c)) -> to (from x) = x-        toFrom (Left (x, y)) = refl-        toFrom (Right (x, y)) = refl+        toFrom (Left (x, y)) = Refl+        toFrom (Right (x, y)) = Refl         fromTo : (x : (Either a b, c)) -> from (to x) = x-        fromTo (Left x, y) = refl-        fromTo (Right x, y) = refl+        fromTo (Left x, y) = Refl+        fromTo (Right x, y) = Refl  ||| Products distribute over sums distribRight : Iso (a, Either b c) (Either (a, b) (a, c))@@ -217,10 +217,10 @@ maybeCong : Iso a b -> Iso (Maybe a) (Maybe b) maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2   where ok1 : (y : Maybe b) -> map to (map from y) = y-        ok1 Nothing = refl+        ok1 Nothing = Refl         ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED         ok2 : (x : Maybe a) -> map from (map to x) = x-        ok2 Nothing = refl+        ok2 Nothing = Refl         ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED  ||| `Maybe a` is the same as `Either a ()`@@ -233,16 +233,16 @@         from (Left x)   = Just x         from (Right ()) = Nothing         iso1 : (x : Either a ()) -> to (from x) = x-        iso1 (Left x) = refl-        iso1 (Right ()) = refl+        iso1 (Left x) = Refl+        iso1 (Right ()) = Refl         iso2 : (y : Maybe a) -> from (to y) = y-        iso2 Nothing = refl-        iso2 (Just x) = refl+        iso2 Nothing = Refl+        iso2 (Just x) = Refl  ||| Maybe of void is just unit-maybeVoidUnit : Iso (Maybe _|_) ()-maybeVoidUnit = (Maybe _|_)     ={ maybeEither   }=-                (Either _|_ ()) ={ eitherBotLeft }=+maybeVoidUnit : Iso (Maybe Void) ()+maybeVoidUnit = (Maybe Void)     ={ maybeEither   }=+                (Either Void ()) ={ eitherBotLeft }=                 ()              QED  eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))@@ -268,28 +268,28 @@ maybeIsoS : Iso (Maybe (Fin n)) (Fin (S n)) maybeIsoS = MkIso forth back fb bf   where forth : Maybe (Fin n) -> Fin (S n)-        forth Nothing = fZ-        forth (Just x) = fS x+        forth Nothing = FZ+        forth (Just x) = FS x         back : Fin (S n) -> Maybe (Fin n)-        back fZ = Nothing-        back (fS x) = Just x+        back FZ = Nothing+        back (FS x) = Just x         bf : (x : Maybe (Fin n)) -> back (forth x) = x-        bf Nothing = refl-        bf (Just x) = refl+        bf Nothing = Refl+        bf (Just x) = Refl         fb : (y : Fin (S n)) -> forth (back y) = y-        fb fZ = refl-        fb (fS x) = refl+        fb FZ = Refl+        fb (FS x) = Refl -finZeroBot : Iso (Fin 0) _|_-finZeroBot = MkIso (\x => FalseElim (uninhabited x))-                   (\x => FalseElim x)-                   (\x => FalseElim x)-                   (\x => FalseElim (uninhabited x))+finZeroBot : Iso (Fin 0) Void+finZeroBot = MkIso (\x => void (uninhabited x))+                   (\x => void x)+                   (\x => void x)+                   (\x => void (uninhabited x))  eitherFinPlus : Iso (Either (Fin m) (Fin n)) (Fin (m + n)) eitherFinPlus {m = Z} {n=n} =   (Either (Fin 0) (Fin n)) ={ eitherCongLeft finZeroBot }=-  (Either _|_ (Fin n))     ={ eitherBotLeft             }=+  (Either Void (Fin n))     ={ eitherBotLeft             }=   (Fin n)                  QED eitherFinPlus {m = S k} {n=n} =   (Either (Fin (S k)) (Fin n))     ={ eitherCongLeft (isoSym maybeIsoS) }=@@ -302,8 +302,8 @@ finPairTimes : Iso (Fin m, Fin n) (Fin (m * n)) finPairTimes {m = Z} {n=n} =   (Fin Z, Fin n) ={ pairCongLeft finZeroBot }=-  (_|_, Fin n)   ={ pairBotLeft             }=-  _|_            ={ isoSym finZeroBot       }=+  (Void, Fin n)   ={ pairBotLeft             }=+  Void            ={ isoSym finZeroBot       }=   (Fin Z)        QED finPairTimes {m = S k} {n=n} =   (Fin (S k), Fin n)                  ={ pairCongLeft (isoSym maybeIsoS)      }=

@@ -20,16 +20,16 @@         fromZZ n = cast n          toFromZZ : (n : Integer) -> fromZZ (toZZ n) = n-        toFromZZ n = really_believe_me {a = n=n} {b = fromZZ (toZZ n) = n} refl+        toFromZZ n = really_believe_me {a = n=n} {b = fromZZ (toZZ n) = n} Refl          fromToZZ : (n : ZZ) -> toZZ (fromZZ n) = n-        fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} refl+        fromToZZ n = really_believe_me {a = n=n} {b = toZZ (fromZZ n) = n} Refl   packUnpackIso : Iso (List Char) String packUnpackIso = MkIso pack                       unpack-                      (\str => really_believe_me {a = str=str} {b = pack (unpack str) = str} refl)-                      (\cs  => really_believe_me {a = cs=cs}   {b = unpack (pack cs) = cs}   refl)+                      (\str => really_believe_me {a = str=str} {b = pack (unpack str) = str} Refl)+                      (\cs  => really_believe_me {a = cs=cs}   {b = unpack (pack cs) = cs}   Refl)  

@@ -16,35 +16,35 @@              (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a  instance Monad m => Functor (RWST r w s m) where-    map f (MkRWST m) = MkRWST $ \r => \s => do (a, s', w) <- m r s-                                               return (f a, s', w)+    map f (MkRWST m) = MkRWST $ \r,s => do  (a, s', w) <- m r s+                                            return (f a, s', w)  instance (Monoid w, Monad m) => Applicative (RWST r w s m) where-    pure a = MkRWST $ \_ => \s => return (a, s, neutral)-    (MkRWST f) <$> (MkRWST v) = MkRWST $ \r => \s => do (a, s', w)   <- v r s-                                                        (fn, ss, w') <- f r s-                                                        return (fn a, ss, w <+> w)+    pure a = MkRWST $ \_,s => return (a, s, neutral)+    (MkRWST f) <$> (MkRWST v) = MkRWST $ \r,s => do (a, s', w)   <- v r s+                                                    (fn, ss, w') <- f r s+                                                    return (fn a, ss, w <+> w)  instance (Monoid w, Monad m) => Monad (RWST r w s m) where-    (MkRWST m) >>= k = MkRWST $ \r => \s => do (a, s', w) <- m r s-                                               let MkRWST ka = k a-                                               (b, ss, w') <- ka r s'-                                               return (b, ss, w <+> w')+    (MkRWST m) >>= k = MkRWST $ \r,s => do  (a, s', w) <- m r s+                                            let MkRWST ka = k a+                                            (b, ss, w') <- ka r s'+                                            return (b, ss, w <+> w')  instance (Monoid w, Monad m) => MonadReader r (RWST r w s m) where-    ask                = MkRWST $ \r => \s => return (r, s, neutral)-    local f (MkRWST m) = MkRWST $ \r => \s => m (f r) s+    ask                = MkRWST $ \r,s => return (r, s, neutral)+    local f (MkRWST m) = MkRWST $ \r,s => m (f r) s  instance (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where-    tell w            = MkRWST $ \_ => \s => return ((), s, w)-    listen (MkRWST m) = MkRWST $ \r => \s => do (a, s', w) <- m r s-                                                return ((a, w), s', w)-    pass (MkRWST m)   = MkRWST $ \r => \s => do ((a, f), s', w) <- m r s-                                                return (a, s', f w)+    tell w            = MkRWST $ \_,s => return ((), s, w)+    listen (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s+                                            return ((a, w), s', w)+    pass (MkRWST m)   = MkRWST $ \r,s => do ((a, f), s', w) <- m r s+                                            return (a, s', f w)  instance (Monoid w, Monad m) => MonadState s (RWST r w s m) where-    get   = MkRWST $ \_ => \s => return (s,  s, neutral)-    put s = MkRWST $ \_ => \_ => return ((), s, neutral)+    get   = MkRWST $ \_,s => return (s,  s, neutral)+    put s = MkRWST $ \_,_ => return ((), s, neutral)  instance (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {} 

@@ -437,8 +437,8 @@     where       %assert_total       helper : Fin (S n) -> Bits n -> List Char-      helper fZ _ = []-      helper (fS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b+      helper FZ _ = []+      helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b  instance Show (Bits n) where     show = bitsToStr

@@ -10,8 +10,8 @@  ||| Compute the length of a list. length : BoundedList n a -> Fin (S n)-length [] = fZ-length (x :: xs) = fS (length xs)+length [] = FZ+length (x :: xs) = FS (length xs)  -------------------------------------------------------------------------------- -- Indexing into bounded lists@@ -19,8 +19,8 @@  index : Fin (S n) -> BoundedList n a -> Maybe a index _      []        = Nothing-index fZ     (x :: _)  = Just x-index (fS f) (_ :: xs) = index f xs+index FZ     (x :: _)  = Just x+index (FS f) (_ :: xs) = index f xs  -------------------------------------------------------------------------------- -- Adjusting bounds@@ -90,5 +90,5 @@ --------------------------------------------------------------------------------  zeroBoundIsEmpty : (xs : BoundedList 0 a) -> xs = the (BoundedList 0 a) []-zeroBoundIsEmpty [] = refl+zeroBoundIsEmpty [] = Refl zeroBoundIsEmpty (_ :: _) impossible

@@ -33,8 +33,8 @@ bitsFromNat (S k) = 1 + bitsFromNat k  bitsFromFin : Fin n -> Bits64-bitsFromFin fZ     = 0-bitsFromFin (fS k) = 1 + bitsFromFin k+bitsFromFin FZ     = 0+bitsFromFin (FS k) = 1 + bitsFromFin k  ||| Allocate an empty Buffer. The size hint can be used to avoid ||| unnecessary reallocations and copies under the hood if the

@@ -13,22 +13,22 @@  ||| Extract an element from an HVect index : (i : Fin k) -> HVect ts -> index i ts-index fZ (x::xs) = x-index (fS j) (x::xs) = index j xs+index FZ (x::xs) = x+index (FS j) (x::xs) = index j xs  deleteAt : (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)-deleteAt fZ (x::xs) = xs-deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs-deleteAt {l = Z}   (fS j) (x::xs) = absurd j+deleteAt FZ (x::xs) = xs+deleteAt {l = S m} (FS j) (x::xs) = x :: deleteAt j xs+deleteAt {l = Z}   (FS j) (x::xs) = absurd j deleteAt _ [] impossible  replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)-replaceAt fZ y (x::xs) = y::xs-replaceAt (fS j) y (x::xs) = x :: replaceAt j y xs+replaceAt FZ y (x::xs) = y::xs+replaceAt (FS j) y (x::xs) = x :: replaceAt j y xs  updateAt : (i : Fin k) -> (index i ts -> t) -> HVect ts -> HVect (replaceAt i t ts)-updateAt fZ f (x::xs) = f x :: xs-updateAt (fS j) f (x::xs) = x :: updateAt j f xs+updateAt FZ f (x::xs) = f x :: xs+updateAt (FS j) f (x::xs) = x :: updateAt j f xs  ||| Append two `HVect`s. (++) : HVect ts -> HVect us -> HVect (ts ++ us)

@@ -0,0 +1,85 @@+module Data.Hash++%access public+%default total++{- A general purpose Hashing library (not cryptographic)++   The core hash is djb2, which is very fast but does not have the best distribution+   Source: http://www.cse.yorku.ca/~oz/hash.html++   The salted version and the magic salt are copied from Haskell's bloomfilter library+   Source: https://hackage.haskell.org/package/bloomfilter-2.0.0.0/docs/src/Data-BloomFilter-Hash.html#Hashable+-}++||| A type that can be hashed+class Hashable a where+  saltedHash64 : a -> Bits64 -> Bits64 -- value to hash, salt, hash++||| Computes a non cryptographic hash+hash : Hashable a => a -> Bits64+hash x = saltedHash64 x 0x16fc397cf62f64d3++||| Given a user provided salt, computes a non cryptographic hash.+||| This version is meant to mitigate hash-flooding DoS attacks.+saltedHash : Hashable a => Bits64 -> a -> Bits64+saltedHash salt x = saltedHash64 x salt+++||| Nth byte of a Bits64+private+byte : Bits64 -> Bits64 -> Bits64+byte n w = prim__lshrB64 (prim__andB64 mask w) offset+  where offset = 8*n+        mask = prim__shlB64 0xff (the Bits64 offset)++||| Modulo of an integer, downsized to a Bits64+private+mod64 : Integer -> Bits64+mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)++instance Hashable Bits64 where+  saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)+                              salt+                              [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto++instance Hashable Integer where+  saltedHash64 i = saltedHash64 (mod64 i)++instance Hashable () where+  saltedHash64 _ salt = salt++instance Hashable Bool where+  saltedHash64 True  = saltedHash64 (the Bits64 1)+  saltedHash64 False = saltedHash64 (the Bits64 0)++instance Hashable Int where+  saltedHash64 w = saltedHash64 (prim__zextInt_B64 w)++instance Hashable Char where+  saltedHash64 w = saltedHash64 (the Int (cast w))++instance Hashable Bits8 where+  saltedHash64 w = saltedHash64 (prim__zextB8_B64 w)++instance Hashable Bits16 where+  saltedHash64 w = saltedHash64 (prim__zextB16_B64 w)++instance Hashable Bits32 where+  saltedHash64 w = saltedHash64 (prim__zextB32_B64 w)++instance Hashable a => Hashable (Maybe a) where+  saltedHash64 Nothing  salt = salt+  saltedHash64 (Just k) salt = saltedHash64 k salt++instance (Hashable a, Hashable b) => Hashable (a, b) where+  saltedHash64 (a,b) salt = saltedHash64 b (saltedHash64 a salt)++instance Hashable a => Hashable (List a) where+  saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l++instance Hashable a => Hashable (Vect n a) where+  saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l++instance Hashable String where+  saltedHash64 s = saltedHash64 (unpack s)

@@ -83,11 +83,11 @@ --------------------------------------------------------------------------------  findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a-findMinimum Empty          refl   impossible+findMinimum Empty          Refl   impossible findMinimum (Node s l e r) p    = e  deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a-deleteMinimum Empty          refl   impossible+deleteMinimum Empty          Refl   impossible deleteMinimum (Node s l e r) p    = merge l r  --------------------------------------------------------------------------------@@ -96,7 +96,7 @@  toList : Ord a => MaxiphobicHeap a -> List a toList Empty          = []-toList (Node s l e r) = toList' (Node s l e r) refl+toList (Node s l e r) = toList' (Node s l e r) Refl   where     %assert_total -- relies on deleteMinimum making heap smaller     toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a@@ -135,28 +135,28 @@ -- Properties -------------------------------------------------------------------------------- -total absurdBoolDischarge : False = True -> _|_+total absurdBoolDischarge : False = True -> Void absurdBoolDischarge p = replace {P = disjointTy} p ()   where     total disjointTy : Bool -> Type     disjointTy False  = ()-    disjointTy True   = _|_+    disjointTy True   = Void  total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z-isEmptySizeZero Empty          p = refl+isEmptySizeZero Empty          p = Refl isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd  total emptyHeapValid : Ord a => isValidHeap empty = True-emptyHeapValid = refl+emptyHeapValid = Refl  total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True-singletonHeapValid e = refl+singletonHeapValid e = Refl  {- total mergePreservesValidHeaps : Ord a => (left : MaxiphobicHeap a) ->   (right : MaxiphobicHeap a) -> (leftValid : isValidHeap left = True) ->   (rightValid : isValidHeap right = True) -> isValidHeap $ merge left right = True-mergePreservesValidHeaps Empty              Empty              lp rp = refl+mergePreservesValidHeaps Empty              Empty              lp rp = Refl mergePreservesValidHeaps Empty              (Node rs rl re rr) lp rp = rp mergePreservesValidHeaps (Node ls ll le lr) Empty              lp rp = lp mergePreservesValidHeaps (Node ls ll le lr) (Node rs rl re rr) lp rp =@@ -169,7 +169,7 @@  isEmptySizeZeroNodeAbsurd = proof {     intros;-    refine FalseElim;+    refine void;     refine absurdBoolDischarge;     exact p; }

@@ -2,9 +2,17 @@  %access public -||| A proof that some element is found in a list+||| A proof that some element is found in a list.+|||+||| Example: `the (Elem "bar" ["foo", "bar", "baz"]) (tactics { search })` data Elem : a -> List a -> Type where+     ||| A proof that the element is at the front of the list.+     |||+     ||| Example: `the (Elem "a" ["a", "b"]) Here`      Here : Elem x (x :: xs)+     ||| A proof that the element is after the front of the list+     |||+     ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`      There : Elem x xs -> Elem x (y :: xs)  instance Uninhabited (Elem {a} x []) where@@ -18,13 +26,13 @@ isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs) isElem x [] = No absurd isElem x (y :: xs) with (decEq x y)-  isElem x (x :: xs) | (Yes refl) = Yes Here+  isElem x (x :: xs) | (Yes Refl) = Yes Here   isElem x (y :: xs) | (No contra) with (isElem x xs)     isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)     isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)       where         mkNo : {xs' : List a} ->-               ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->-               Elem x' (y' :: xs') -> _|_-        mkNo f g Here = f refl+               ((x' = y') -> Void) -> (Elem x' xs' -> Void) ->+               Elem x' (y' :: xs') -> Void+        mkNo f g Here = f Refl         mkNo f g (There x) = g x

@@ -15,19 +15,19 @@      There : Elem x xs -> Elem x (y::xs)  ||| Nothing can be in an empty Vect-noEmptyElem : {x : a} -> Elem x [] -> _|_+noEmptyElem : {x : a} -> Elem x [] -> Void noEmptyElem Here impossible  ||| An item not in the head and not in the tail is not in the Vect at all neitherHereNorThere : {x, y : a} -> {xs : Vect n a} -> Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))-neitherHereNorThere xneqy xninxs Here = xneqy refl+neitherHereNorThere xneqy xninxs Here = xneqy Refl neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs  ||| A decision procedure for Elem isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs) isElem x [] = No noEmptyElem isElem x (y :: xs) with (decEq x y)-  isElem x (x :: xs) | (Yes refl) = Yes Here+  isElem x (x :: xs) | (Yes Refl) = Yes Here   isElem x (y :: xs) | (No xneqy) with (isElem x xs)     isElem x (y :: xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)     isElem x (y :: xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)

@@ -1,10 +1,16 @@ module Data.Vect.Quantifiers +||| A proof that some element of a vector satisfies some property+|||+||| @ P the property to be satsified data Any : (P : a -> Type) -> Vect n a -> Type where+  ||| A proof that the satisfying element is the first one in the `Vect`   Here  : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)+  ||| A proof that the satsifying element is in the tail of the `Vect`   There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs) -anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_+||| No element of an empty vector satisfies any property+anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void anyNilAbsurd (Here _) impossible anyNilAbsurd (There _) impossible @@ -15,7 +21,13 @@ anyElim _ f (Here p) = f p anyElim f _ (There p) = f p -any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)+||| Given a decision procedure for a property, determine if an element of a+||| vector satisfies it.+|||+||| @ P the property to be satisfied+||| @ dec the decision procedure+||| @ xs the vector to examine+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs) any _ Nil = No anyNilAbsurd any p (x::xs) with (p x)   | Yes prf = Yes (Here prf)@@ -24,23 +36,33 @@       Yes prf' => Yes (There prf')       No prf' => No (anyElim prf' prf) +||| A proof that all elements of a vector satisfy a property. It is a list of+||| proofs, corresponding element-wise to the `Vect`. data All : (P : a -> Type) -> Vect n a -> Type where   Nil : {P : a -> Type} -> All P Nil   (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs) +||| If there does not exist an element that satifies the property, then it is+||| the case that all elements do not satisfy. negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs negAnyAll {xs=Nil} _ = Nil negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x)) -notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> _|_+notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> Void notAllHere _ Nil impossible notAllHere np (p :: _) = np p -notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> _|_+notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> Void notAllThere _ Nil impossible notAllThere np (_ :: ps) = np ps -all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)+||| Given a decision procedure for a property, decide whether all elements of+||| a vector satisfy it.+|||+||| @ P the property+||| @ dec the decision procedure+||| @ xs the vector to examine+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs) all _ Nil = Yes Nil all d (x::xs) with (d x)   | No prf = No (notAllHere prf)

@@ -7,14 +7,18 @@ %access public  -||| An integer is either a positive nat or the negated successor of a nat.-||| Zero is arbitrarily chosen to be positive.+||| An integer is either a positive `Nat` or the negated successor of a `Nat`.+|||+||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen+||| to be positive.+||| data ZZ = Pos Nat | NegS Nat  instance Signed ZZ where   sign (Pos _) = Plus   sign (NegS _) = Minus +||| Take the absolute value of a `ZZ` absZ : ZZ -> Nat absZ (Pos n) = n absZ (NegS n) = S n@@ -23,28 +27,32 @@   show (Pos n) = show n   show (NegS n) = "-" ++ show (S n) -negZ : ZZ -> ZZ-negZ (Pos Z) = Pos Z-negZ (Pos (S n)) = NegS n-negZ (NegS n) = Pos (S n)+instance Neg ZZ where+  negate (Pos Z)     = Pos Z+  negate (Pos (S n)) = NegS n+  negate (NegS n)    = Pos (S n)  negNat : Nat -> ZZ negNat Z = Pos Z negNat (S n) = NegS n ++||| Construct a `ZZ` as the difference of two `Nat`s minusNatZ : Nat -> Nat -> ZZ minusNatZ n Z = Pos n minusNatZ Z (S m) = NegS m minusNatZ (S n) (S m) = minusNatZ n m +||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`. plusZ : ZZ -> ZZ -> ZZ plusZ (Pos n) (Pos m) = Pos (n + m) plusZ (NegS n) (NegS m) = NegS (S (n + m)) plusZ (Pos n) (NegS m) = minusNatZ n (S m) plusZ (NegS n) (Pos m) = minusNatZ m (S n) +||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`. subZ : ZZ -> ZZ -> ZZ-subZ n m = plusZ n (negZ m)+subZ n m = plusZ n (negate m)  instance Eq ZZ where   (Pos n) == (Pos m) = n == m@@ -58,13 +66,14 @@   compare (Pos _) (NegS _) = GT   compare (NegS _) (Pos _) = LT -+||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`. multZ : ZZ -> ZZ -> ZZ multZ (Pos n) (Pos m) = Pos $ n * m multZ (NegS n) (NegS m) = Pos $ (S n) * (S m) multZ (NegS n) (Pos m) = negNat $ (S n) * m multZ (Pos n) (NegS m) = negNat $ n * (S m) +||| Convert an `Integer` to an inductive representation. fromInt : Integer -> ZZ fromInt n = if n < 0             then NegS $ fromInteger {a=Nat} ((-n) - 1)@@ -100,21 +109,21 @@              -> n * m = x -> (Pos n) * (Pos m) = Pos x natMultZMult n m x h = cong h -doubleNegElim : (z : ZZ) -> negZ (negZ z) = z-doubleNegElim (Pos Z) = refl-doubleNegElim (Pos (S n)) = refl-doubleNegElim (NegS Z) = refl-doubleNegElim (NegS (S n)) = refl+doubleNegElim : (z : ZZ) -> negate (negate z) = z+doubleNegElim (Pos Z) = Refl+doubleNegElim (Pos (S n)) = Refl+doubleNegElim (NegS Z) = Refl+doubleNegElim (NegS (S n)) = Refl  -- Injectivity posInjective : Pos n = Pos m -> n = m-posInjective refl = refl+posInjective Refl = Refl  negSInjective : NegS n = NegS m -> n = m-negSInjective refl = refl+negSInjective Refl = Refl -posNotNeg : Pos n = NegS m -> _|_-posNotNeg refl impossible+posNotNeg : Pos n = NegS m -> Void+posNotNeg Refl impossible  -- Decidable equality instance DecEq ZZ where@@ -129,16 +138,16 @@  -- Plus plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right-plusZeroLeftNeutralZ (Pos n) = refl-plusZeroLeftNeutralZ (NegS n) = refl+plusZeroLeftNeutralZ (Pos n) = Refl+plusZeroLeftNeutralZ (NegS n) = Refl  plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n-plusZeroRightNeutralZ (NegS n) = refl+plusZeroRightNeutralZ (NegS n) = Refl  plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left) plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m-plusCommutativeZ (Pos n) (NegS m) = refl-plusCommutativeZ (NegS n) (Pos m) = refl+plusCommutativeZ (Pos n) (NegS m) = Refl+plusCommutativeZ (NegS n) (Pos m) = Refl plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m 

@@ -48,7 +48,7 @@  instance Preorder t ((=) {A = t} {B = t}) where   transitive a b c = trans {a = a} {b = b} {c = c}-  reflexive a = refl+  reflexive a = Refl  instance Equivalence t ((=) {A = t} {B = t}) where   symmetric a b prf = sym prf@@ -60,99 +60,88 @@ -- Natural numbers -------------------------------------------------------------------------------- -data NatLTE : Nat -> Nat -> Type where-  nEqn   : NatLTE n n-  nLTESm : NatLTE n m -> NatLTE n (S m)+total LTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->+                           LTE m n -> LTE n o ->+                           LTE m o+LTEIsTransitive Z n o                 LTEZero                  nlteo   = LTEZero+LTEIsTransitive (S m) (S n) (S o) (LTESucc mlten)    (LTESucc nlteo)   = LTESucc (LTEIsTransitive m n o mlten nlteo) -total NatLTEIsTransitive : (m : Nat) -> (n : Nat) -> (o : Nat) ->-                           NatLTE m n -> NatLTE n o ->-                           NatLTE m o-NatLTEIsTransitive m n n      mLTEn (nEqn) = mLTEn-NatLTEIsTransitive m n (S o)  mLTEn (nLTESm nLTEo)-  = nLTESm (NatLTEIsTransitive m n o mLTEn nLTEo)+total LTEIsReflexive : (n : Nat) -> LTE n n+LTEIsReflexive Z      = LTEZero+LTEIsReflexive (S n)  = LTESucc (LTEIsReflexive n) -total NatLTEIsReflexive : (n : Nat) -> NatLTE n n-NatLTEIsReflexive _ = nEqn+instance Preorder Nat LTE where+  transitive = LTEIsTransitive+  reflexive  = LTEIsReflexive -instance Preorder Nat NatLTE where-  transitive = NatLTEIsTransitive-  reflexive  = NatLTEIsReflexive+total LTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->+                              LTE m n -> LTE n m -> m = n+LTEIsAntisymmetric Z Z         LTEZero LTEZero = Refl+LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisymmetric n m mLTEn nLTEm)+   LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm)    | Refl = Refl            -total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->-                              NatLTE m n -> NatLTE n m -> m = n-NatLTEIsAntisymmetric n n nEqn nEqn = refl-NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible-NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible-NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible -instance Poset Nat NatLTE where-  antisymmetric = NatLTEIsAntisymmetric+instance Poset Nat LTE where+  antisymmetric = LTEIsAntisymmetric -total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_-zeroNeverGreater {n} (nLTESm _) impossible-zeroNeverGreater {n}  nEqn      impossible+total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void+zeroNeverGreater {n} LTEZero     impossible+zeroNeverGreater {n} (LTESucc _) impossible -total zeroAlwaysSmaller : {n : Nat} -> NatLTE Z n-zeroAlwaysSmaller {n = Z  } = nEqn-zeroAlwaysSmaller {n = S k} = nLTESm (zeroAlwaysSmaller {n = k}) +total zeroAlwaysSmaller : {n : Nat} -> LTE Z n+zeroAlwaysSmaller = LTEZero -total-nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_-nGTSm         disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)-nGTSm {n} {m} disprf (nEqn) impossible+total ltesuccinjective : {n : Nat} -> {m : Nat} -> (LTE n m -> Void) -> LTE (S n) (S m) -> Void+ltesuccinjective {n} {m} disprf (LTESucc nLTEm) = void (disprf nLTEm)+ltesuccinjective {n} {m} disprf LTEZero         impossible -total-decideNatLTE : (n : Nat) -> (m : Nat) -> Dec (NatLTE n m)-decideNatLTE    Z      Z  = Yes nEqn-decideNatLTE (S x)     Z  = No  zeroNeverGreater-decideNatLTE    x   (S y) with (decEq x (S y))-  | Yes eq      = rewrite eq in Yes nEqn-  | No _ with (decideNatLTE x y)-    | Yes nLTEm = Yes (nLTESm nLTEm)-    | No  nGTm  = No (nGTSm nGTm) -instance Decidable [Nat,Nat] NatLTE where-  decide = decideNatLTE+total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)+decideLTE    Z      y  = Yes LTEZero+decideLTE (S x)     Z  = No  zeroNeverGreater+decideLTE (S x)   (S y) with (decEq (S x) (S y))+  | Yes eq      = rewrite eq in Yes (reflexive x)+  | No _ with (decideLTE x y)+    | Yes nLTEm = Yes (LTESucc nLTEm)+    | No  nGTm  = No (ltesuccinjective nGTm) -total-lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)-lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n+instance Decidable [Nat,Nat] LTE where+  decide = decideLTE  total-shift : (m : Nat) -> (n : Nat) -> NatLTE m n -> NatLTE (S m) (S n)-shift Z      Z        _            = nEqn-shift Z     (S Z)     _            = nLTESm nEqn-shift Z     (S (S j)) _            = nLTESm (shift Z (S j) zeroAlwaysSmaller)-shift (S k)  Z        prf          = FalseElim (zeroNeverGreater prf)-shift (S k) (S k)     nEqn         = nEqn-shift (S k) (S j)     (nLTESm prf) = nLTESm (shift (S k) j prf)+lte : (m : Nat) -> (n : Nat) -> Dec (LTE m n)+lte m n = decide {ts = [Nat,Nat]} {p = LTE} m n -instance Ordered Nat NatLTE where-  order Z      n = Left zeroAlwaysSmaller-  order m      Z = Right zeroAlwaysSmaller+total+shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)+shift m n mLTEn = LTESucc mLTEn+      +instance Ordered Nat LTE where+  order Z      n = Left LTEZero+  order m      Z = Right LTEZero   order (S k) (S j) with (order k j)     order (S k) (S j) | Left  prf = Left  (shift k j prf)     order (S k) (S j) | Right prf = Right (shift j k prf) ------------------------------------------------------------------------------------ Finite numbers---------------------------------------------------------------------------------+----------------------------------------------------------------------------------+---- Finite numbers+----------------------------------------------------------------------------------  using (k : Nat)   data FinLTE : Fin k -> Fin k -> Type where-    FromNatPrf : {m : Fin k} -> {n : Fin k} -> NatLTE (finToNat m) (finToNat n) -> FinLTE m n+    FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n    instance Preorder (Fin k) FinLTE where     transitive m n o (FromNatPrf p1) (FromNatPrf p2) = -      FromNatPrf (NatLTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)-    reflexive n = FromNatPrf (NatLTEIsReflexive (finToNat n))+      FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)+    reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))    instance Poset (Fin k) FinLTE where     antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =-      finToNatInjective m n (NatLTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)+      finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)      instance Decidable [Fin k, Fin k] FinLTE where-    decide m n with (decideNatLTE (finToNat m) (finToNat n))+    decide m n with (decideLTE (finToNat m) (finToNat n))       | Yes prf    = Yes (FromNatPrf prf)       | No  disprf = No (\ (FromNatPrf prf) => disprf prf) 

@@ -79,20 +79,22 @@   ||| Types of named references-data NameType = Bound-              -- ^ reference which is just bound, e.g. by intro-              | Ref-              -- ^ reference to a variable-              | DCon Int Int-              -- ^ constructor with tag and number-              | TCon Int Int-              -- ^ type constructor with tag and number+data NameType =+  ||| A reference which is just bound, e.g. by intro+  Bound |+  ||| A reference to a de Bruijn-indexed variable+  Ref |+  ||| Data constructor with tag and number+  DCon Int Int |+  ||| Type constructor with tag and number+  TCon Int Int+ %name NameType nt, nt'  ||| Types annotations for bound variables in different ||| binding contexts data Binder a = Lam a-              | Pi a a +              | Pi a a               | Let a a               | NLet a a               | Hole a

@@ -4,8 +4,8 @@ module IdrisNet.Socket  %include C "idris_net.h"-%include C "sys/types.h" -%include C "sys/socket.h" +%include C "sys/types.h"+%include C "sys/socket.h" %include C "netdb.h"  %access public@@ -16,12 +16,17 @@ class ToCode a where   toCode : a -> Int --- Socket Families.--- The ones that people might actually use. We're not going to need US Government--- proprietary ones...-data SocketFamily = AF_UNSPEC -- Unspecified-                  | AF_INET   -- IP / UDP etc. IPv4-                  | AF_INET6  -- IP / UDP etc. IPv6+||| Socket Families+|||+||| The ones that people might actually use. We're not going to need US+||| Government proprietary ones.+data SocketFamily =+  ||| Unspecified+  AF_UNSPEC |+  ||| IP / UDP etc. IPv4+  AF_INET |+  |||  IP / UDP etc. IPv6+  AF_INET6  instance Show SocketFamily where   show AF_UNSPEC = "AF_UNSPEC"@@ -36,11 +41,16 @@ getSocketFamily : Int -> Maybe SocketFamily getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)] --- Socket Types.-data SocketType = NotASocket  -- Not a socket, used in certain operations-                | Stream      -- TCP-                | Datagram    -- UDP-                | RawSocket   -- Raw sockets. A guy can dream.+||| Socket Types.+data SocketType =+  ||| Not a socket, used in certain operations+  NotASocket |+  ||| TCP+  Stream |+  ||| UDP+  Datagram |+  ||| Raw sockets+  RawSocket  instance Show SocketType where   show NotASocket = "Not a socket"@@ -60,15 +70,17 @@ data BufPtr = BPtr Ptr data SockaddrPtr = SAPtr Ptr --- Protocol Number. Generally good enough to just set it to 0.+||| Protocol Number.+|||+||| Generally good enough to just set it to 0. ProtocolNumber : Type ProtocolNumber = Int --- SocketError: Error thrown by a socket operation+||| SocketError: Error thrown by a socket operation SocketError : Type SocketError = Int --- SocketDescriptor: Native C Socket Descriptor+||| SocketDescriptor: Native C Socket Descriptor SocketDescriptor : Type SocketDescriptor = Int @@ -86,7 +98,7 @@ Port : Type Port = Int --- Backlog used within listen() call -- number of incoming calls+||| Backlog used within listen() call -- number of incoming calls BACKLOG : Int BACKLOG = 20 @@ -109,7 +121,7 @@     (remote_port : Port) ->     UDPAddrInfo --- Frees a given pointer+||| Frees a given pointer public sock_free : BufPtr -> IO () sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr@@ -118,12 +130,14 @@ sockaddr_free : SockaddrPtr -> IO () sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr --- Allocates an amount of memory given by the ByteLength parameter.--- Used to allocate a mutable pointer to be given to the Recv functions.+||| Allocates an amount of memory given by the ByteLength parameter.+|||+||| Used to allocate a mutable pointer to be given to the Recv functions. public sock_alloc : ByteLength -> IO BufPtr sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl +||| The metadata about a socket record Socket : Type where   MkSocket : (descriptor : SocketDescriptor) ->              (family : SocketFamily) ->@@ -131,20 +145,21 @@              (protocolNumber : ProtocolNumber) ->              Socket +||| Get the C error number getErrno : IO Int getErrno = mkForeign (FFun "idrnet_errno" [] FInt) --- Creates a UNIX socket with the given family, socket type and protocol number.--- Returns either a socket or an error.+||| Creates a UNIX socket with the given family, socket type and protocol+||| number. Returns either a socket or an error. socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket) socket sf st pn = do   socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn   if socket_res == -1 then -- error     map Left getErrno-  else +  else     return $ Right (MkSocket socket_res sf st pn) -+||| Close a socket close : Socket -> IO () close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock) @@ -153,18 +168,18 @@ saString (Just sa) = show sa saString Nothing = "" --- Binds a socket to the given socket address and port.--- Returns 0 on success, an error code otherwise.+||| Binds a socket to the given socket address and port.+||| Returns 0 on success, an error code otherwise. bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int bind sock addr port = do-  bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt) +  bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)                            (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)   if bind_res == (-1) then -- error     getErrno   else return 0 -- Success --- Connects to a given address and port.--- Returns 0 on success, and an error number on error.+||| Connects to a given address and port.+||| Returns 0 on success, and an error number on error. connect : Socket -> SocketAddress -> Port -> IO Int connect sock addr port = do   conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)@@ -173,7 +188,7 @@     getErrno   else return 0 --- Listens on a bound socket.+||| Listens on a bound socket. listen : Socket -> IO Int listen sock = do   listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG@@ -181,7 +196,7 @@     getErrno   else return 0 --- Parses a textual representation of an IPv4 address into a SocketAddress+||| Parses a textual representation of an IPv4 address into a SocketAddress parseIPv4 : String -> SocketAddress parseIPv4 str = case splitted of                   (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4@@ -194,7 +209,7 @@         splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)  --- Retrieves a socket address from a sockaddr pointer+||| Retrieves a socket address from a sockaddr pointer getSockAddr : SockaddrPtr -> IO SocketAddress getSockAddr (SAPtr ptr) = do   addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr@@ -256,13 +271,13 @@        return $ Right (payload, recv_res)  --- Sends the data in a given memory location+||| Sends the data in a given memory location sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength) sendBuf sock (BPtr ptr) len = do   send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len   if send_res == (-1) then     map Left getErrno-  else +  else     return $ Right send_res  recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)@@ -313,7 +328,7 @@   recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)                  (descriptor sock) bl   let recv_ptr' = RFPtr recv_ptr-  if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"+  if !(nullPtr recv_ptr) then     map Left getErrno   else do     result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr@@ -332,7 +347,7 @@ recvFromBuf sock (BPtr ptr) bl = do   recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl   let recv_ptr' = RFPtr recv_ptr-  if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"+  if !(nullPtr recv_ptr) then     map Left getErrno   else do     result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr@@ -345,5 +360,4 @@       freeRecvfromStruct recv_ptr'       return $ Right (MkUDPAddrInfo addr port, result + 1) -   

@@ -1,6 +1,6 @@ module Syntax.PreorderReasoning --- QED is first to get the precedence to work out. It's just refl with an explicit argument.+-- QED is first to get the precedence to work out. It's just Refl with an explicit argument. syntax [expr] "QED" = qed expr -- foo ={ prf }= bar ={ prf' }= fnord QED -- is a proof that foo is related to fnord, with the intermediate step being bar, justified by prf and prf'@@ -9,7 +9,7 @@ namespace Equal   using (a : Type, x : a, y : a, z : a)     qed : (x : a) -> x = x-    qed x = the (x = x) refl+    qed x = the (x = x) Refl     step : (x : a) -> x = y -> (y = z) -> x = z-    step x refl refl = refl+    step x Refl Refl = Refl 

@@ -12,38 +12,38 @@ ||| Type safe message passing programs. Parameterised over the type of ||| message which can be send, and the return type. data Process : (msgType : Type) -> Type -> Type where-     lift : IO a -> Process msg a+     Lift : IO a -> Process msg a  instance Functor (Process msg) where-     map f (lift a) = lift (map f a)+     map f (Lift a) = Lift (map f a)  instance Applicative (Process msg) where-     pure = lift . return-     (lift f) <$> (lift a) = lift (f <$> a)+     pure = Lift . return+     (Lift f) <$> (Lift a) = Lift (f <$> a)  instance Monad (Process msg) where-     (lift io) >>= k = lift (do x <- io+     (Lift io) >>= k = Lift (do x <- io                                 case k x of-                                     lift v => v)+                                     Lift v => v)  run : Process msg x -> IO x-run (lift prog) = prog+run (Lift prog) = prog  ||| Get current process ID myID : Process msg (ProcID msg)-myID = lift (return (MkPID prim__vm))+myID = Lift (return (MkPID prim__vm))  ||| Send a message to another process send : ProcID msg -> msg -> Process msg ()-send (MkPID p) m = lift (sendToThread p (prim__vm, m))+send (MkPID p) m = Lift (sendToThread p (prim__vm, m))  ||| Return whether a message is waiting in the queue msgWaiting : Process msg Bool-msgWaiting = lift checkMsgs+msgWaiting = Lift checkMsgs  ||| Receive a message - blocks if there is no message waiting recv : Process msg msg-recv {msg} = do (senderid, m) <- lift get+recv {msg} = do (senderid, m) <- Lift get                 return m   where get : IO (Ptr, msg)         get = getMsg@@ -51,11 +51,11 @@ ||| receive a message, and return with the sender's process ID. recvWithSender : Process msg (ProcID msg, msg) recvWithSender {msg}-     = do (senderid, m) <- lift get+     = do (senderid, m) <- Lift get           return (MkPID senderid, m)   where get : IO (Ptr, msg)         get = getMsg  create : Process msg () -> Process msg (ProcID msg)-create (lift p) = do ptr <- lift (fork p)+create (Lift p) = do ptr <- Lift (fork p)                      return (MkPID ptr)

@@ -24,7 +24,7 @@           Data.Vect, Data.HVect, Data.Vect.Quantifiers,           Data.Floats, Data.Complex, Data.Heap, Data.Fun,           Data.Rel, Data.Buffer, Data.Erased,-          Data.List,+          Data.List, Data.Hash,            Control.Isomorphism, Control.Isomorphism.Primitives,           Control.Monad.Identity,

@@ -16,23 +16,23 @@      Free       : RawMemory () (MemoryChunk n i) (\v => ())      Initialize : Bits8 ->                   (size : Nat) ->-                  so (i + size <= n) ->+                  So (i + size <= n) ->                   RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (i + size))      Peek       : (offset : Nat) ->                   (size : Nat) ->-                  so (offset + size <= i) ->+                  So (offset + size <= i) ->                   RawMemory (Vect size Bits8)                             (MemoryChunk n i) (\v => MemoryChunk n i)       Poke       :  (offset : Nat) ->                   (Vect size Bits8) ->-                  so (offset <= i && offset + size <= n) ->+                  So (offset <= i && offset + size <= n) ->                   RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))       Move       : (src : MemoryChunk src_size src_init) ->                   (dst_offset : Nat) ->                   (src_offset : Nat) ->                   (size : Nat) ->-                  so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->-                  so (src_offset + size <= src_init) ->+                  So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->+                  So (src_offset + size <= src_init) ->                   RawMemory () (MemoryChunk dst_size dst_init)                             (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))       GetRawPtr  : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i) @@ -108,7 +108,7 @@              {n : Nat} ->              Bits8 ->              (size : Nat) ->-             so (i + size <= n) ->+             So (i + size <= n) ->              Eff () [RAW_MEMORY (MemoryChunk n i)]                         (\v => [RAW_MEMORY (MemoryChunk n (i + size))]) initialize c size prf = call $ Initialize c size prf@@ -119,7 +119,7 @@ peek : {i : Nat} ->        (offset : Nat) ->        (size : Nat) ->-       so (offset + size <= i) ->+       So (offset + size <= i) ->        { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)  peek offset size prf = call $ Peek offset size prf @@ -127,7 +127,7 @@        {i : Nat} ->        (offset : Nat) ->        Vect size Bits8 ->-       so (offset <= i && offset + size <= n) ->+       So (offset <= i && offset + size <= n) ->        Eff () [RAW_MEMORY (MemoryChunk n i)]                (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))]) poke offset content prf = call $ Poke offset content prf@@ -144,8 +144,8 @@         (dst_offset : Nat) ->         (src_offset : Nat) ->         (size : Nat) ->-        so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->-        so (src_offset + size <= src_init) ->+        So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->+        So (src_offset + size <= src_init) ->         Eff () [RAW_MEMORY (MemoryChunk dst_size dst_init)]                (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))]) move' src_ptr dst_offset src_offset size dst_bounds src_bounds@@ -160,8 +160,8 @@        (dst_offset : Nat) ->        (src_offset : Nat) ->        (size : Nat) ->-       so (dst_offset <= dst_init && dst_offset + size <= dst_size) ->-       so (src_offset + size <= src_init) ->+       So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->+       So (src_offset + size <= src_init) ->        Eff ()               [ Dst ::: RAW_MEMORY (MemoryChunk dst_size dst_init)               , Src ::: RAW_MEMORY (MemoryChunk src_size src_init)]

@@ -136,9 +136,7 @@ data Eff : (x : Type)            -> (es : List EFFECT)            -> (ce : x -> List EFFECT) -> Type where-     value    : a -> Eff a xs (\v => xs)-     with_val : (val : a) -> Eff () xs (\v => xs' val) ->-                Eff a xs xs'+     value    : (val : a) -> Eff a (xs val) xs      ebind    : Eff a xs xs' ->                 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''      callP    : (prf : EffElem e a xs) ->@@ -181,7 +179,8 @@ pure : a -> Eff a xs (\v => xs) pure = value -syntax pureM [val] = with_val val (pure ())+pureM : (val : a) -> Eff a (xs val) xs+pureM = value  (<$>) : Eff (a -> b) xs (\v => xs) ->         Eff a xs (\v => xs) -> Eff b xs (\v => xs)@@ -206,7 +205,6 @@  eff : Env m xs -> Eff a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b eff env (value x) k = k x env-eff env (with_val x prog) k = eff env prog (\p', env' => k x env') eff env (prog `ebind` c) k    = eff env prog (\p', env' => eff env' (c p') k) eff env (callP prf effP) k = execEff env prf effP k

@@ -3,14 +3,40 @@ %access public %default total -||| Dependent pairs, in their internal representation-||| @ a the type of the witness-||| @ P the type of the proof+||| The canonical single-element type, also known as the trivially+||| true proposition.+%elim data Unit =+  ||| The trivial constructor for `()`.+  MkUnit++||| The non-dependent pair type, also known as conjunction.+||| @A the type of the left elements in the pair+||| @B the type of the left elements in the pair+data Pair : (A : Type) -> (B : Type) -> Type where+   ||| A pair of elements+   ||| @a the left element of the pair+   ||| @b the right element of the pair+   MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B++||| Dependent pairs+|||+||| Dependent pairs represent existential quantification - they consist of a+||| witness for the existential claim and a proof that the property holds for+||| it. Another way to see dependent pairs is as just data - for instance, the+||| length of a vector paired with that vector.+|||+|||  @ a the type of the witness @ P the type of the proof data Sigma : (a : Type) -> (P : a -> Type) -> Type where-    Sg_intro : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P+    MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P -||| The eliminator for the empty type.-FalseElim : _|_ -> a+||| The empty type, also known as the trivially false proposition.+|||+||| Use `void` or `absurd` to prove anything if you have a variable of type `Void` in scope. +%elim data Void : Type where    +    +||| The eliminator for the `Void` type.+void : Void -> a+void {a} v = elim_for Void (\_ => a) v  ||| For 'symbol syntax. 'foo becomes Symbol_ "foo" data Symbol_ : String -> Type where@@ -27,20 +53,19 @@ (~=~) : (x : a) -> (y : b) -> Type (~=~) x y = (=) _ _ x y --- ------------------------------------------------------ [ For rewrite tactic ] ||| Perform substitution in a term according to some equality. ||| ||| This is used by the `rewrite` tactic and term. replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y-replace refl prf = prf+replace Refl prf = prf  ||| Symmetry of propositional equality sym : {l:a} -> {r:a} -> l = r -> r = l-sym refl = refl+sym Refl = Refl  ||| Transitivity of propositional equality trans : {a:x} -> {b:y} -> {c:z} -> a = b -> b = c -> a = c-trans refl refl = refl+trans Refl Refl = Refl  ||| There are two types of laziness: that arising from lazy functions, and that ||| arising from codata. They differ in their totality condition.@@ -79,7 +104,7 @@   ||| A read-only version of a unique value   data Borrowed : UniqueType -> NullType where        Read : {a : UniqueType} -> a -> Borrowed a-         +   ||| Make a read-only version of a unique value, which can be passed to another   ||| function without the unique value being consumed.   implicit@@ -88,13 +113,7 @@  par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type                   -- is better in any case?-par (Delay x) = x --malloc : Int -> a -> a-malloc size x = x -- compiled specially--trace_malloc : a -> a-trace_malloc x = x -- compiled specially+par (Delay x) = x  ||| Assert to the totality checker than y is always structurally smaller than ||| x (which is typically a pattern argument)@@ -119,4 +138,3 @@ public %assert_total really_believe_me : a -> b really_believe_me x = prim__believe_me _ _ x-

@@ -13,7 +13,7 @@ --------------------------------------------------------------------------------  ||| The negation of equality is symmetric (follows from symmetry of equality)-total negEqSym : {a : t} -> {b : t} -> (a = b -> _|_) -> (b = a -> _|_)+total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void) negEqSym p h = p (sym h)  @@ -31,17 +31,17 @@ --------------------------------------------------------------------------------  instance DecEq () where-  decEq () () = Yes refl+  decEq () () = Yes Refl  -------------------------------------------------------------------------------- -- Booleans ---------------------------------------------------------------------------------total trueNotFalse : True = False -> _|_-trueNotFalse refl impossible+total trueNotFalse : True = False -> Void+trueNotFalse Refl impossible  instance DecEq Bool where-  decEq True  True  = Yes refl-  decEq False False = Yes refl+  decEq True  True  = Yes Refl+  decEq False False = Yes Refl   decEq True  False = No trueNotFalse   decEq False True  = No (negEqSym trueNotFalse) @@ -49,11 +49,11 @@ -- Nat -------------------------------------------------------------------------------- -total OnotS : Z = S n -> _|_-OnotS refl impossible+total OnotS : Z = S n -> Void+OnotS Refl impossible  instance DecEq Nat where-  decEq Z     Z     = Yes refl+  decEq Z     Z     = Yes Refl   decEq Z     (S _) = No OnotS   decEq (S _) Z     = No (negEqSym OnotS)   decEq (S n) (S m) with (decEq n m)@@ -64,11 +64,11 @@ -- Maybe -------------------------------------------------------------------------------- -total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> _|_-nothingNotJust refl impossible+total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> Void+nothingNotJust Refl impossible  instance (DecEq t) => DecEq (Maybe t) where-  decEq Nothing Nothing = Yes refl+  decEq Nothing Nothing = Yes Refl   decEq (Just x') (Just y') with (decEq x' y')     | Yes p = Yes $ cong p     | No p = No $ \h : Just x' = Just y' => p $ justInjective h@@ -79,8 +79,8 @@ -- Either -------------------------------------------------------------------------------- -total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> _|_-leftNotRight refl impossible+total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> Void+leftNotRight Refl impossible  instance (DecEq a, DecEq b) => DecEq (Either a b) where   decEq (Left x') (Left y') with (decEq x' y')@@ -96,40 +96,40 @@ -- Fin -------------------------------------------------------------------------------- -total fZNotfS : {f : Fin n} -> fZ {k = n} = fS f -> _|_-fZNotfS refl impossible+total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void+FZNotFS Refl impossible  instance DecEq (Fin n) where-  decEq fZ fZ = Yes refl-  decEq fZ (fS f) = No fZNotfS-  decEq (fS f) fZ = No $ negEqSym fZNotfS-  decEq (fS f) (fS f') with (decEq f f')+  decEq FZ FZ = Yes Refl+  decEq FZ (FS f) = No FZNotFS+  decEq (FS f) FZ = No $ negEqSym FZNotFS+  decEq (FS f) (FS f') with (decEq f f')     | Yes p = Yes $ cong p-    | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h+    | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h  -------------------------------------------------------------------------------- -- Tuple -------------------------------------------------------------------------------- -lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> _|_) -> (y = y' -> _|_) -> ((x, y) = (x', y') -> _|_)-lemma_both_neq p_x_not_x' p_y_not_y' refl = p_x_not_x' refl+lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> Void) -> (y = y' -> Void) -> ((x, y) = (x', y') -> Void)+lemma_both_neq p_x_not_x' p_y_not_y' Refl = p_x_not_x' Refl -lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> _|_) -> ((x, y) = (x, y') -> _|_)-lemma_snd_neq refl p refl = p refl+lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> Void) -> ((x, y) = (x, y') -> Void)+lemma_snd_neq Refl p Refl = p Refl  lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->-                       (x = x' -> _|_) ->+                       (x = x' -> Void) ->                        (y = y') ->-                       ((x, y) = (x', y) -> _|_)-lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl+                       ((x, y) = (x', y) -> Void)+lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl  instance (DecEq a, DecEq b) => DecEq (a, b) where   decEq (a, b) (a', b')     with (decEq a a')-    decEq (a, b) (a, b')    | (Yes refl) with (decEq b b')-      decEq (a, b) (a, b)   | (Yes refl) | (Yes refl) = Yes refl-      decEq (a, b) (a, b')  | (Yes refl) | (No p) = No (\eq => lemma_snd_neq refl p eq)+    decEq (a, b) (a, b')    | (Yes Refl) with (decEq b b')+      decEq (a, b) (a, b)   | (Yes Refl) | (Yes Refl) = Yes Refl+      decEq (a, b) (a, b')  | (Yes Refl) | (No p) = No (\eq => lemma_snd_neq Refl p eq)     decEq (a, b) (a', b')   | (No p)     with (decEq b b')-      decEq (a, b) (a', b)  | (No p)     | (Yes refl) =  No (\eq => lemma_fst_neq_snd_eq p refl eq)+      decEq (a, b) (a', b)  | (No p)     | (Yes Refl) =  No (\eq => lemma_fst_neq_snd_eq p Refl eq)       decEq (a, b) (a', b') | (No p)     | (No p') = No (\eq => lemma_both_neq p p' eq)  @@ -137,28 +137,28 @@ -- List -------------------------------------------------------------------------------- -lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> _|_)-lemma_val_not_nil refl impossible+lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> Void)+lemma_val_not_nil Refl impossible -lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)-lemma_x_eq_xs_neq refl p refl = p refl+lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)+lemma_x_eq_xs_neq Refl p Refl = p Refl -lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> _|_)-lemma_x_neq_xs_eq p refl refl = p refl+lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> Void) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> Void)+lemma_x_neq_xs_eq p Refl Refl = p Refl -lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)-lemma_x_neq_xs_neq p p' refl = p refl+lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> Void) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)+lemma_x_neq_xs_neq p p' Refl = p Refl  instance DecEq a => DecEq (List a) where-  decEq [] [] = Yes refl+  decEq [] [] = Yes Refl   decEq (x :: xs) [] = No lemma_val_not_nil   decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)   decEq (x :: xs) (y :: ys) with (decEq x y)-    decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)-      decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl -      decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)+    decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)+      decEq (x :: xs) (x :: xs) | (Yes Refl) | (Yes Refl) = Yes Refl +      decEq (x :: xs) (x :: ys) | (Yes Refl) | (No p) = No (\eq => lemma_x_eq_xs_neq Refl p eq)     decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)-      decEq (x :: xs) (y :: xs) | (No p) | (Yes refl) = No (\eq => lemma_x_neq_xs_eq p refl eq)+      decEq (x :: xs) (y :: xs) | (No p) | (Yes Refl) = No (\eq => lemma_x_neq_xs_eq p Refl eq)       decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)  @@ -168,26 +168,26 @@  total vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y-vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl+vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl  total vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys-vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl+vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl  instance DecEq a => DecEq (Vect n a) where-  decEq [] [] = Yes refl+  decEq [] [] = Yes Refl   decEq (x :: xs) (y :: ys) with (decEq x y)-    decEq (x :: xs) (x :: ys)   | Yes refl with (decEq xs ys)-      decEq (x :: xs) (x :: xs) | Yes refl | Yes refl = Yes refl-      decEq (x :: xs) (x :: ys) | Yes refl | No  neq  = No (neq . vectInjective2)+    decEq (x :: xs) (x :: ys)   | Yes Refl with (decEq xs ys)+      decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl+      decEq (x :: xs) (x :: ys) | Yes Refl | No  neq  = No (neq . vectInjective2)     decEq (x :: xs) (y :: ys)   | No  neq             = No (neq . vectInjective1)  {- The following definition is elaborated in a wrong case-tree. Examination pending.  instance DecEq a => DecEq (Vect n a) where-  decEq [] [] = Yes refl+  decEq [] [] = Yes Refl   decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)-    decEq (x :: xs) (x :: xs) | (Yes refl, Yes refl) = Yes refl+    decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl     decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))     decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p)) -}@@ -202,8 +202,8 @@ instance DecEq Int where     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq        where primitiveEq : x = y-             primitiveEq = believe_me (refl {x})-             postulate primitiveNotEq : x = y -> _|_+             primitiveEq = believe_me (Refl {x})+             postulate primitiveNotEq : x = y -> Void  -------------------------------------------------------------------------------- -- Char@@ -212,8 +212,8 @@ instance DecEq Char where     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq        where primitiveEq : x = y-             primitiveEq = believe_me (refl {x})-             postulate primitiveNotEq : x = y -> _|_+             primitiveEq = believe_me (Refl {x})+             postulate primitiveNotEq : x = y -> Void  -------------------------------------------------------------------------------- -- Integer@@ -222,8 +222,8 @@ instance DecEq Integer where     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq        where primitiveEq : x = y-             primitiveEq = believe_me (refl {x})-             postulate primitiveNotEq : x = y -> _|_+             primitiveEq = believe_me (Refl {x})+             postulate primitiveNotEq : x = y -> Void  -------------------------------------------------------------------------------- -- Float@@ -232,8 +232,8 @@ instance DecEq Float where     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq        where primitiveEq : x = y-             primitiveEq = believe_me (refl {x})-             postulate primitiveNotEq : x = y -> _|_+             primitiveEq = believe_me (Refl {x})+             postulate primitiveNotEq : x = y -> Void  -------------------------------------------------------------------------------- -- String@@ -242,7 +242,7 @@ instance DecEq String where     decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq        where primitiveEq : x = y-             primitiveEq = believe_me (refl {x})-             postulate primitiveNotEq : x = y -> _|_+             primitiveEq = believe_me (Refl {x})+             postulate primitiveNotEq : x = y -> Void  

@@ -420,9 +420,9 @@           go (x :: xs) = n + (cast x * inc) :: go xs  instance Enum (Fin (S n)) where-  pred fZ = fZ-  pred (fS n) = weaken n-  succ n = case strengthen (fS n) of+  pred FZ = FZ+  pred (FS n) = weaken n+  succ n = case strengthen (FS n) of     Left _ => last     Right k => k   toNat n = cast n@@ -494,6 +494,7 @@  ---- some basic file handling +||| A file handle abstract data File = FHandle Ptr @@ -592,6 +593,7 @@ do_feof : Ptr -> IO Int do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h +||| Check if a file handle has reached the end feof : File -> IO Bool feof (FHandle h) = do eof <- do_feof h                       return (not (eof == 0))@@ -608,6 +610,7 @@ fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h                        return (p > 0) +||| Check if a foreign pointer is null partial nullPtr : Ptr -> IO Bool nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p@@ -630,6 +633,10 @@ validFile (FHandle h) = do x <- nullPtr h                            return (not x) +||| Loop while some test is true+|||+||| @ test the condition of the loop+||| @ body the loop body partial -- obviously while : (test : IO Bool) -> (body : IO ()) -> IO () while t b = do v <- t@@ -637,6 +644,7 @@                             while t b                     else return () +||| Read the contents of a file into a string partial -- no error checking! readFile : String -> IO String readFile fn = do h <- openFile fn Read

@@ -123,7 +123,7 @@ ||| + Inverse for `<+>`: |||     forall a,     a <+> inverse a == neutral |||     forall a,     inverse a <+> a == neutral-||| + Associativity of `<*>a:+||| + Associativity of `<*>`: |||     forall a b c, a <*> (b <*> c) == (a <*> b) <*> c ||| + Neutral for `<*>`: |||     forall a,     a <*> unity     == a@@ -264,9 +264,61 @@  class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { } +--   Fields.+||| Sets equipped with two binary operations, both associative and commutative+||| supplied with a neutral element, with+||| distributivity laws relating the two operations.  Must satisfy the following+||| laws:+|||+||| + Associativity of `<+>`:+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c+||| + Commutativity of `<+>`:+|||     forall a b,   a <+> b         == b <+> a+||| + Neutral for `<+>`:+|||     forall a,     a <+> neutral   == a+|||     forall a,     neutral <+> a   == a+||| + Inverse for `<+>`:+|||     forall a,     a <+> inverse a == neutral+|||     forall a,     inverse a <+> a == neutral+||| + Associativity of `<*>`:+|||     forall a b c, a <*> (b <*> c) == (a <*> b) <*> c+||| + Unity for `<*>`:+|||     forall a,     a <*> unity     == a+|||     forall a,     unity <*> a     == a+||| + InverseM of `<*>`:+|||     forall a,     a <*> inverseM a == unity+|||     forall a,     inverseM a <*> a == unity+||| + Distributivity of `<*>` and `<->`:+|||     forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)+|||     forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)+class RingWithUnity a => Field a where+  inverseM : a -> a +class (VerifiedRing a, Field a) => VerifiedField a where+  total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity+  total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity++--   vector spaces.+||| A Vector Space over a Field can be considered as an additive Abeliean Group+||| of Vectors adjoined to the Field structure by distributivity laws relating+||| the two operations. Such that we satisfy the following laws:+|||+||| + Unity for `<*>`:+|||     forall a,     a <*> unity     == a+|||     forall a,     unity <*> a     == a+||| + Distributivity of `<*>` and `<+>`:+|||     forall a x y, a <*> (x <+> y) == (a <*> x) <+> (a <*> y)+|||     forall a b x, (a <+> b) <*> x == (a <*> x) <+> (b <*> x)+class (Field a, AbelianGroup a) => VectorSpace a a where {}++class (VerifiedField a, VerifiedAbelianGroup a, VectorSpace a a) => VerifiedVectorSpace a a where+  total vectorspaceScalarUnityIsUnityL : (l : a) -> l <*> unity = l+  total vectorspaceScalarUnityIsUnityR : (r : a) -> unity <*> r = r+  total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : a) -> s <*> (x <+> y) = (s <*> x) <+> (s <*> y)+  total vectorspaceScalarIsDistributiveWRTFieldAddition  : (s, t : a) -> (x : a) -> (s <+> t) <*> x = (s <*> x) <+> (t <*> x)++ -- XXX todo:---   Fields and vector spaces. --   Structures where "abs" make sense. --   Euclidean domains, etc. --   Where to put fromInteger and fromRational?

@@ -1,7 +1,9 @@ module Prelude.Basics +import Builtins+        Not : Type -> Type-Not a = a -> _|_+Not a = a -> Void  ||| Identity function. id : a -> a@@ -42,7 +44,7 @@  ||| Equality is a congruence. cong : {f : t -> u} -> (a = b) -> f a = f b-cong refl = refl+cong Refl = Refl  ||| Decidability. A decidable property either holds or is a contradiction. data Dec : Type -> Type where@@ -53,5 +55,5 @@    ||| The case where the property holding would be a contradiction   ||| @ contra a demonstration that A would be a contradiction-  No  : {A : Type} -> (contra : A -> _|_) -> Dec A+  No  : {A : Type} -> (contra : A -> Void) -> Dec A 

@@ -21,13 +21,14 @@ ||| if you need to perform a Boolean test and convince the type checker of this ||| fact. |||-||| If you find yourself using `so` for something other than primitive types,+||| If you find yourself using `So` for something other than primitive types, ||| it may be appropriate to define a type of evidence for the property that you ||| care about instead.-data so : Bool -> Type where oh : so True+data So : Bool -> Type where +  Oh : So True -instance Uninhabited (so False) where-  uninhabited oh impossible+instance Uninhabited (So False) where+  uninhabited Oh impossible  -- Syntactic sugar for boolean elimination. syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

@@ -137,6 +137,21 @@       then compare xl yl       else compare xr yr +-- --------------------------------------------------------- [ Negatable Class ]+||| The `Neg` class defines unary negation (-).+class Neg a where+    ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.+    negate : a -> a++instance Neg Integer where+    negate x = prim__subBigInt 0 x++instance Neg Int where+    negate x = prim__subInt 0 x++instance Neg Float where+    negate x = prim__negFloat x+ -- --------------------------------------------------------- [ Numerical Class ] ||| The Num class defines basic numerical arithmetic. class Num a where

@@ -30,10 +30,10 @@ -- Misc. -------------------------------------------------------------------------------- -||| Perform a case analysis on a Boolean, providing clients with a `so` proof-choose : (b : Bool) -> Either (so b) (so (not b))-choose True  = Left oh-choose False = Right oh+||| Perform a case analysis on a Boolean, providing clients with a `So` proof+choose : (b : Bool) -> Either (So b) (So (not b))+choose True  = Left Oh+choose False = Right Oh  ||| Simply-typed eliminator for Either ||| @ f the action to take on Left@@ -97,9 +97,9 @@ ||| Left is injective total leftInjective : {b : Type} -> {x : a} -> {y : a}                     -> (Left {b = b} x = Left {b = b} y) -> (x = y)-leftInjective refl = refl+leftInjective Refl = Refl  ||| Right is injective total rightInjective : {a : Type} -> {x : b} -> {y : b}                      -> (Right {a = a} x = Right {a = a} y) -> (x = y)-rightInjective refl = refl+rightInjective Refl = Refl

@@ -12,39 +12,39 @@ ||| exceedingly inefficient at run time. ||| @ n the upper bound data Fin : (n : Nat) -> Type where-    fZ : Fin (S k)-    fS : Fin k -> Fin (S k)+    FZ : Fin (S k)+    FS : Fin k -> Fin (S k)  instance Uninhabited (Fin Z) where-  uninhabited fZ impossible-  uninhabited (fS f) impossible+  uninhabited FZ impossible+  uninhabited (FS f) impossible -fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n-fSInjective left _ refl = refl+FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n+FSInjective left _ Refl = Refl  instance Eq (Fin n) where-    (==) fZ fZ = True-    (==) (fS k) (fS k') = k == k'+    (==) FZ FZ = True+    (==) (FS k) (FS k') = k == k'     (==) _ _ = False  ||| There are no elements of `Fin Z`-FinZAbsurd : Fin Z -> _|_-FinZAbsurd fZ impossible+FinZAbsurd : Fin Z -> Void+FinZAbsurd FZ impossible  FinZElim : Fin Z -> a-FinZElim x = FalseElim (FinZAbsurd x)+FinZElim x = void (FinZAbsurd x)  ||| Convert a Fin to a Nat finToNat : Fin n -> Nat-finToNat fZ = Z-finToNat (fS k) = S (finToNat k)+finToNat FZ = Z+finToNat (FS k) = S (finToNat k)  ||| `finToNat` is injective finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn-finToNatInjective fZ     fZ     refl = refl-finToNatInjective (fS m) fZ     refl impossible-finToNatInjective fZ     (fS n) refl impossible-finToNatInjective (fS m) (fS n) prf  =+finToNatInjective FZ     FZ     Refl = Refl+finToNatInjective (FS m) FZ     Refl impossible+finToNatInjective FZ     (FS n) Refl impossible+finToNatInjective (FS m) (FS n) prf  =   cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))   instance Cast (Fin n) Nat where@@ -52,29 +52,29 @@  ||| Convert a Fin to an Integer finToInteger : Fin n -> Integer-finToInteger fZ     = 0-finToInteger (fS k) = 1 + finToInteger k+finToInteger FZ     = 0+finToInteger (FS k) = 1 + finToInteger k  instance Cast (Fin n) Integer where     cast x = finToInteger x  ||| Weaken the bound on a Fin by 1 weaken : Fin n -> Fin (S n)-weaken fZ     = fZ-weaken (fS k) = fS (weaken k)+weaken FZ     = FZ+weaken (FS k) = FS (weaken k)  ||| Weaken the bound on a Fin by some amount weakenN : (n : Nat) -> Fin m -> Fin (m + n)-weakenN n fZ = fZ-weakenN n (fS f) = fS (weakenN n f)+weakenN n FZ = FZ+weakenN n (FS f) = FS (weakenN n f)  ||| Attempt to tighten the bound on a Fin. ||| Return `Left` if the bound could not be tightened, or `Right` if it could. strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)-strengthen {n = S k} fZ = Right fZ-strengthen {n = S k} (fS i) with (strengthen i)-  strengthen (fS k) | Left x   = Left (fS x)-  strengthen (fS k) | Right x  = Right (fS x)+strengthen {n = S k} FZ = Right FZ+strengthen {n = S k} (FS i) with (strengthen i)+  strengthen (FS k) | Left x   = Left (FS x)+  strengthen (FS k) | Right x  = Right (FS x) strengthen f = Left f  ||| Add some natural number to a Fin, extending the bound accordingly@@ -82,24 +82,24 @@ ||| @ m the number to increase the Fin by shift : (m : Nat) -> Fin n -> Fin (m + n) shift Z f = f-shift {n=n} (S m) f = fS {k = (m + n)} (shift m f)+shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)  ||| The largest element of some Fin type last : Fin (S n)-last {n=Z} = fZ-last {n=S _} = fS last+last {n=Z} = FZ+last {n=S _} = FS last -total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'-fSinjective refl = refl+total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'+FSinjective Refl = Refl  instance Ord (Fin n) where-  compare  fZ     fZ    = EQ-  compare  fZ    (fS _) = LT-  compare (fS _)  fZ    = GT-  compare (fS x) (fS y) = compare x y+  compare  FZ     FZ    = EQ+  compare  FZ    (FS _) = LT+  compare (FS _)  FZ    = GT+  compare (FS x) (FS y) = compare x y    instance MinBound (Fin (S n)) where-  minBound = fZ+  minBound = FZ  instance MaxBound (Fin (S n)) where   maxBound = last@@ -107,28 +107,28 @@  ||| Add two Fins, extending the bound (+) : Fin n -> Fin m -> Fin (n + m)-(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')-(+) (fS f) f' = fS (f + f')+(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')+(+) (FS f) f' = FS (f + f')  ||| Substract two Fins, keeping the bound of the minuend (-) : Fin n -> Fin m -> Fin n-fZ - _ = fZ-f - fZ = f-(fS f) - (fS f') = weaken $ f - f'+FZ - _ = FZ+f - FZ = f+(FS f) - (FS f') = weaken $ f - f'  ||| Multiply two Fins, extending the bound (*) : Fin n -> Fin m -> Fin (n * m) (*) {n=Z} f f' = FinZElim f (*) {m=Z} f f' = FinZElim f'-(*) {n=S n} {m=S m} fZ     f' = fZ-(*) {n=S n} {m=S m} (fS f) f' = f' + (f * f')+(*) {n=S n} {m=S m} FZ     f' = FZ+(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')  -- Construct a Fin from an integer literal which must fit in the given Fin  natToFin : Nat -> (n : Nat) -> Maybe (Fin n)-natToFin Z     (S j) = Just fZ+natToFin Z     (S j) = Just FZ natToFin (S k) (S j) with (natToFin k j)-                          | Just k' = Just (fS k')+                          | Just k' = Just (FS k')                           | Nothing = Nothing natToFin _ _ = Nothing 

@@ -38,13 +38,13 @@ ||| predicate to all elements of a structure. `any` short-circuits ||| from left to right. any : Foldable t => (a -> Bool) -> t a -> Bool-any p = foldl (\x => \y => x || p y) False+any p = foldl (\x,y => x || p y) False  ||| The disjunction of the collective results of applying a ||| predicate to all elements of a structure. `all` short-circuits ||| from left to right. all : Foldable t => (a -> Bool) -> t a -> Bool-all p = foldl (\x => \y => x && p y)  True+all p = foldl (\x,y => x && p y)  True  ||| Add together all the elements of a structure sum : (Foldable t, Num a) => t a -> a

@@ -60,7 +60,7 @@ index : (n : Nat) -> (l : List a) -> (ok : lt n (length l) = True) -> a index Z     (x::xs) p    = x index (S n) (x::xs) p    = index n xs ?indexTailProof-index _     []      refl   impossible+index _     []      Refl   impossible  ||| Attempt to find a particular element of a list. |||@@ -73,7 +73,7 @@ ||| Get the first element of a non-empty list ||| @ ok proof that the list is non-empty head : (l : List a) -> {auto ok : isCons l = True} -> a-head []      {ok=refl}   impossible+head []      {ok=Refl}   impossible head (x::xs) {ok=p}    = x  ||| Attempt to get the first element of a list. If the list is empty, return@@ -85,7 +85,7 @@ ||| Get the tail of a non-empty list. ||| @ ok proof that the list is non-empty tail : (l : List a) -> {auto ok : isCons l = True} -> List a-tail []      {ok=refl}   impossible+tail []      {ok=Refl}   impossible tail (x::xs) {ok=p}    = xs  ||| Attempt to get the tail of a list.@@ -98,9 +98,9 @@ ||| Retrieve the last element of a non-empty list. ||| @ ok proof that the list is non-empty last : (l : List a) -> {auto ok : isCons l = True} -> a-last []         {ok=refl}   impossible+last []         {ok=Refl}   impossible last [x]        {ok=p}    = x-last (x::y::ys) {ok=p}    = last (y::ys) {ok=refl}+last (x::y::ys) {ok=p}    = last (y::ys) {ok=Refl}  ||| Attempt to retrieve the last element of a non-empty list. |||@@ -115,9 +115,9 @@ ||| Return all but the last element of a non-empty list. ||| @ ok proof that the list is non-empty init : (l : List a) -> {auto ok : isCons l = True} -> List a-init []         {ok=refl}   impossible+init []         {ok=Refl}   impossible init [x]        {ok=p}    = []-init (x::y::ys) {ok=p}    = x :: init (y::ys) {ok=refl}+init (x::y::ys) {ok=p}    = x :: init (y::ys) {ok=Refl}  ||| Attempt to Return all but the last element of a list. |||@@ -157,7 +157,7 @@ drop (S n) []      = [] drop (S n) (x::xs) = drop n xs -||| Take the longest prefix of a list such that all elements satsify some+||| Take the longest prefix of a list such that all elements satisfy some ||| Boolean predicate. ||| ||| @ p the predicate@@ -165,7 +165,7 @@ takeWhile p []      = [] takeWhile p (x::xs) = if p x then x :: takeWhile p xs else [] -||| Remove the longest prefix of a list such that all removed elements satsify some+||| Remove the longest prefix of a list such that all removed elements satisfy some ||| Boolean predicate. ||| ||| @ p the predicate@@ -251,8 +251,8 @@ ||| @ ok a proof that the lengths of the inputs are equal zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->   (ok : length l = length r) -> List c-zipWith f []      (y::ys) refl   impossible-zipWith f (x::xs) []      refl   impossible+zipWith f []      (y::ys) Refl   impossible+zipWith f (x::xs) []      Refl   impossible zipWith f []      []      p    = [] zipWith f (x::xs) (y::ys) p    = f x y :: (zipWith f xs ys ?zipWithTailProof) @@ -265,22 +265,22 @@ ||| @ ok' a proof that the lengths of the second and third inputs are equal zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->   (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d-zipWith3 f _       []      (z::zs) p    refl   impossible-zipWith3 f _       (y::ys) []      p    refl   impossible-zipWith3 f []      (y::ys) _       refl q      impossible-zipWith3 f (x::xs) []      _       refl q      impossible+zipWith3 f _       []      (z::zs) p    Refl   impossible+zipWith3 f _       (y::ys) []      p    Refl   impossible+zipWith3 f []      (y::ys) _       Refl q      impossible+zipWith3 f (x::xs) []      _       Refl q      impossible zipWith3 f []      []      []      p    q    = [] zipWith3 f (x::xs) (y::ys) (z::zs) p    q    =   f x y z :: (zipWith3 f xs ys zs ?zipWith3TailProof ?zipWith3TailProof')  ||| Combine two lists elementwise into pairs zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)-zip = zipWith (\x => \y => (x, y))+zip = zipWith (\x,y => (x, y))  ||| Combine three lists elementwise into tuples zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->   (length y = length z) -> List (a, b, c)-zip3 = zipWith3 (\x => \y => \z => (x, y, z))+zip3 = zipWith3 (\x,y,z => (x, y, z))  ||| Split a list of pairs into two lists unzip : List (a, b) -> (List a, List b)@@ -340,11 +340,16 @@     reverse' acc (x::xs) = reverse' (x::acc) xs  ||| Insert some separator between the elements of a list.+|||+||| ````idris example+||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])+||| ````+||| intersperse : a -> List a -> List a intersperse sep []      = [] intersperse sep (x::xs) = x :: intersperse' sep xs   where---     intersperse' : a -> List a -> List a+    intersperse' : a -> List a -> List a     intersperse' sep []      = []     intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys @@ -353,13 +358,15 @@  ||| Transposes rows and columns of a list of lists. |||-|||     > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]+||| ```idris example+||| with List transpose [[1, 2], [3, 4]]+||| ``` ||| ||| This also works for non square scenarios, thus ||| involution does not always hold: |||-|||     > transpose [[], [1, 2]] = [[1], [2]]-|||     > transpose (transpose [[], [1, 2]]) = [[1, 2]]+|||     transpose [[], [1, 2]] = [[1], [2]]+|||     transpose (transpose [[], [1, 2]]) = [[1, 2]] ||| ||| TODO: Solution which satisfies the totality checker? %assert_total@@ -468,6 +475,12 @@ -- Filters -------------------------------------------------------------------------------- +||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,+|||+||| ````idris example+||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]+||| ````+||| filter : (a -> Bool) -> List a -> List a filter p []      = [] filter p (x::xs) =@@ -476,6 +489,7 @@   else     filter p xs +||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function. nubBy : (a -> a -> Bool) -> List a -> List a nubBy = nubBy' []   where@@ -487,22 +501,53 @@       else         x :: nubBy' (x::acc) p xs +||| O(n^2). The nub function removes duplicate elements from a list. In+||| particular, it keeps only the first occurrence of each element. It is a+||| special case of nubBy, which allows the programmer to supply their own+||| equality test.+|||+||| ```idris example+||| nub (the (List _) [1,2,1,3])+||| ``` nub : Eq a => List a -> List a nub = nubBy (==) +||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate. deleteBy : (a -> a -> Bool) -> a -> List a -> List a deleteBy _  _ []      = [] deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys +||| `delete x` removes the first occurrence of `x` from its list argument. For+||| example,+|||+|||````idris example+|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']+|||````+|||+||| It is a special case of deleteBy, which allows the programmer to supply+||| their own equality test. delete : (Eq a) => a -> List a -> List a delete = deleteBy (==) +||| The `\\` function is list difference (non-associative). In the result of+||| `xs \\ ys`, the first occurrence of each element of ys in turn (if any) has+||| been removed from `xs`, e.g.,+|||+||| ```idris example+||| (([1,2] ++ [2,3]) \\ [1,2])+||| ``` (\\) : (Eq a) => List a -> List a -> List a (\\) =  foldl (flip delete)  unionBy : (a -> a -> Bool) -> List a -> List a -> List a unionBy eq xs ys =  xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs +||| The union function returns the list union of the two lists. For example,+|||+||| ```idris example+||| union ['d', 'o', 'g'] ['c', 'o', 'w']+||| ```+||| union : (Eq a) => List a -> List a -> List a union = unionBy (==) @@ -512,6 +557,10 @@  ||| Given a list and a predicate, returns a pair consisting of the longest ||| prefix of the list that satisfies a predicate and the rest of the list.+|||+||| ```idris example+||| span (<3) [1,2,3,2,1]+||| ``` span : (a -> Bool) -> List a -> (List a, List a) span p []      = ([], []) span p (x::xs) =@@ -521,9 +570,21 @@   else     ([], x::xs) +||| Given a list and a predicate, returns a pair consisting of the longest+||| prefix of the list that does not satisfy a predicate and the rest of the+||| list.+|||+||| ```idris example+||| break (>=3) [1,2,3,2,1]+||| ``` break : (a -> Bool) -> List a -> (List a, List a) break p = span (not . p) +||| Split on any elements that satisfy the given predicate.+|||+||| ```idris example+||| split (<2) [2,0,3,1,4]+||| ``` split : (a -> Bool) -> List a -> List (List a) split p xs =   case break p xs of@@ -538,6 +599,11 @@ splitAt : (n : Nat) -> (xs : List a) -> (List a, List a) splitAt n xs = (take n xs, drop n xs) +||| The partition function takes a predicate a list and returns the pair of lists of elements which do and do not satisfy the predicate, respectively; e.g.,+|||+||| ```idris example+||| partition (<3) [0, 1, 2, 3, 4, 5]+||| ``` partition : (a -> Bool) -> List a -> (List a, List a) partition p []      = ([], []) partition p (x::xs) =@@ -547,19 +613,43 @@     else       (lefts, x::rights) +||| The inits function returns all initial segments of the argument, shortest+||| first. For example,+|||+||| ```idris example+||| inits [1,2,3]+||| ``` inits : List a -> List (List a) inits xs = [] :: case xs of   []        => []   x :: xs'  => map (x ::) (inits xs') +||| The tails function returns all final segments of the argument, longest+||| first. For example,+|||+||| ```idris example+||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]+|||``` tails : List a -> List (List a) tails xs = xs :: case xs of   []        => []   _ :: xs'  => tails xs' +||| Split on the given element.+|||+||| ```idris example+||| splitOn 0 [1,0,2,0,0,3]+||| ```+||| splitOn : Eq a => a -> List a -> List (List a) splitOn a = split (== a) +||| Replaces all occurences of the first argument with the second argument in a list.+|||+||| ```idris example+||| replaceOn '-' ',' ['1', '-', '2', '-', '3']+||| ```+||| replaceOn : Eq a => a -> a -> List a -> List a replaceOn a b l = map (\c => if c == a then b else c) l @@ -576,15 +666,26 @@   else     False +||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second. isPrefixOf : Eq a => List a -> List a -> Bool isPrefixOf = isPrefixOfBy (==)  isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right) +||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second. isSuffixOf : Eq a => List a -> List a -> Bool isSuffixOf = isSuffixOfBy (==) +||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.+|||+||| ```idris example+||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']+||| ```+||| ```idris example+||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']+||| ```+||| isInfixOf : Eq a => List a -> List a -> Bool isInfixOf n h = any (isPrefixOf n) (tails h) @@ -651,7 +752,7 @@ ||| The empty list is a right identity for append. appendNilRightNeutral : (l : List a) ->   l ++ [] = l-appendNilRightNeutral []      = refl+appendNilRightNeutral []      = Refl appendNilRightNeutral (x::xs) =   let inductiveHypothesis = appendNilRightNeutral xs in     ?appendNilRightNeutralStepCase@@ -659,7 +760,7 @@ ||| Appending lists is associative. appendAssociative : (l : List a) -> (c : List a) -> (r : List a) ->   l ++ (c ++ r) = (l ++ c) ++ r-appendAssociative []      c r = refl+appendAssociative []      c r = Refl appendAssociative (x::xs) c r =   let inductiveHypothesis = appendAssociative xs c r in     ?appendAssociativeStepCase@@ -668,7 +769,7 @@ ||| of the input lists. lengthAppend : (left : List a) -> (right : List a) ->   length (left ++ right) = length left + length right-lengthAppend []      right = refl+lengthAppend []      right = Refl lengthAppend (x::xs) right =   let inductiveHypothesis = lengthAppend xs right in     ?lengthAppendStepCase@@ -676,7 +777,7 @@ ||| Mapping a function over a list doesn't change its length. mapPreservesLength : (f : a -> b) -> (l : List a) ->   length (map f l) = length l-mapPreservesLength f []      = refl+mapPreservesLength f []      = Refl mapPreservesLength f (x::xs) =   let inductiveHypothesis = mapPreservesLength f xs in     ?mapPreservesLengthStepCase@@ -685,7 +786,7 @@ ||| to appending them and then mapping the function. mapDistributesOverAppend : (f : a -> b) -> (l : List a) -> (r : List a) ->   map f (l ++ r) = map f l ++ map f r-mapDistributesOverAppend f []      r = refl+mapDistributesOverAppend f []      r = Refl mapDistributesOverAppend f (x::xs) r =   let inductiveHypothesis = mapDistributesOverAppend f xs r in     ?mapDistributesOverAppendStepCase@@ -693,7 +794,7 @@ ||| Mapping two functions is the same as mapping their composition. mapFusion : (f : b -> c) -> (g : a -> b) -> (l : List a) ->   map f (map g l) = map (f . g) l-mapFusion f g []      = refl+mapFusion f g []      = Refl mapFusion f g (x::xs) =   let inductiveHypothesis = mapFusion f g xs in     ?mapFusionStepCase@@ -701,7 +802,7 @@ ||| No list contains an element of the empty list by any predicate. hasAnyByNilFalse : (p : a -> a -> Bool) -> (l : List a) ->   hasAnyBy p [] l = False-hasAnyByNilFalse p []      = refl+hasAnyByNilFalse p []      = Refl hasAnyByNilFalse p (x::xs) =   let inductiveHypothesis = hasAnyByNilFalse p xs in     ?hasAnyByNilFalseStepCase

@@ -45,7 +45,7 @@ toMaybe False j = Nothing  justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y-justInjective refl = refl+justInjective Refl = Refl  ||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case ||| that the `Maybe` value is `Nothing`.

@@ -22,7 +22,7 @@ %name Nat k,j,i,n,m  instance Uninhabited (Z = S n) where-  uninhabited refl impossible+  uninhabited Refl impossible  -------------------------------------------------------------------------------- -- Syntactic tests@@ -94,9 +94,9 @@ ||| @ m the larger number data LTE  : (n, m : Nat) -> Type where   ||| Zero is the smallest Nat-  lteZero : LTE Z    right+  LTEZero : LTE Z    right   ||| If n <= m, then n + 1 <= m + 1-  lteSucc : LTE left right -> LTE (S left) (S right)+  LTESucc : LTE left right -> LTE (S left) (S right)  ||| Greater than or equal to total GTE : Nat -> Nat -> Type@@ -112,18 +112,18 @@  ||| A successor is never less than or equal zero succNotLTEzero : Not (S m `LTE` Z)-succNotLTEzero lteZero impossible+succNotLTEzero LTEZero impossible  ||| If two numbers are ordered, their predecessors are too fromLteSucc : (S m `LTE` S n) -> (m `LTE` n)-fromLteSucc (lteSucc x) = x+fromLteSucc (LTESucc x) = x  ||| A decision procedure for `LTE` isLTE : (m, n : Nat) -> Dec (m `LTE` n)-isLTE Z n = Yes lteZero+isLTE Z n = Yes LTEZero isLTE (S k) Z = No succNotLTEzero isLTE (S k) (S j) with (isLTE k j)-  isLTE (S k) (S j) | (Yes prf) = Yes (lteSucc prf)+  isLTE (S k) (S j) | (Yes prf) = Yes (LTESucc prf)   isLTE (S k) (S j) | (No contra) = No (contra . fromLteSucc)  ||| Boolean test than one Nat is less than or equal to another@@ -156,6 +156,14 @@ maximum (S n) Z = S n maximum (S n) (S m) = S (maximum n m) +||| Tail recursive cast Nat to Int+||| Note that this can overflow+toIntNat : Nat -> Int+toIntNat n = toIntNat' n 0 where+	toIntNat' : Nat -> Int -> Int+	toIntNat' Z     x = x+	toIntNat' (S n) x = toIntNat' n (x + 1)+ -------------------------------------------------------------------------------- -- Type class instances --------------------------------------------------------------------------------@@ -245,9 +253,7 @@   cast i = fromInteger (cast i)  instance Cast Nat Int where-  cast Z     = 0-  cast (S n) = 1 + cast {to=Int} n-+  cast = toIntNat  -------------------------------------------------------------------------------- -- Auxilliary notions@@ -329,18 +335,18 @@ -- An informative comparison view  -------------------------------------------------------------------------------- data CmpNat : Nat -> Nat -> Type where-     cmpLT : (y : _) -> CmpNat x (x + S y)-     cmpEQ : CmpNat x x-     cmpGT : (x : _) -> CmpNat (y + S x) y+     CmpLT : (y : _) -> CmpNat x (x + S y)+     CmpEQ : CmpNat x x+     CmpGT : (x : _) -> CmpNat (y + S x) y  total cmp : (x, y : Nat) -> CmpNat x y-cmp Z Z     = cmpEQ-cmp Z (S k) = cmpLT _-cmp (S k) Z = cmpGT _+cmp Z Z     = CmpEQ+cmp Z (S k) = CmpLT _+cmp (S k) Z = CmpGT _ cmp (S x) (S y) with (cmp x y)-  cmp (S x) (S (x + (S k))) | cmpLT k = cmpLT k-  cmp (S x) (S x)           | cmpEQ   = cmpEQ-  cmp (S (y + (S k))) (S y) | cmpGT k = cmpGT k+  cmp (S x) (S (x + (S k))) | CmpLT k = CmpLT k+  cmp (S x) (S x)           | CmpEQ   = CmpEQ+  cmp (S (y + (S k))) (S y) | CmpGT k = CmpGT k  -------------------------------------------------------------------------------- -- Properties@@ -351,26 +357,26 @@ ||| S preserves equality total eqSucc : (left : Nat) -> (right : Nat) -> (p : left = right) ->   S left = S right-eqSucc left _ refl = refl+eqSucc left _ Refl = Refl  ||| S is injective total succInjective : (left : Nat) -> (right : Nat) -> (p : S left = S right) ->   left = right-succInjective left _ refl = refl+succInjective left _ Refl = Refl  -- Plus total plusZeroLeftNeutral : (right : Nat) -> 0 + right = right-plusZeroLeftNeutral right = refl+plusZeroLeftNeutral right = Refl  total plusZeroRightNeutral : (left : Nat) -> left + 0 = left-plusZeroRightNeutral Z     = refl+plusZeroRightNeutral Z     = Refl plusZeroRightNeutral (S n) =   let inductiveHypothesis = plusZeroRightNeutral n in     ?plusZeroRightNeutralStepCase  total plusSuccRightSucc : (left : Nat) -> (right : Nat) ->   S (left + right) = left + (S right)-plusSuccRightSucc Z right        = refl+plusSuccRightSucc Z right        = Refl plusSuccRightSucc (S left) right =   let inductiveHypothesis = plusSuccRightSucc left right in     ?plusSuccRightSuccStepCase@@ -384,21 +390,21 @@  total plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left + (centre + right) = (left + centre) + right-plusAssociative Z        centre right = refl+plusAssociative Z        centre right = Refl plusAssociative (S left) centre right =   let inductiveHypothesis = plusAssociative left centre right in     ?plusAssociativeStepCase  total plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) ->   (p : left = right) -> left + c = right + c-plusConstantRight left _ c refl = refl+plusConstantRight left _ c Refl = Refl  total plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) ->   (p : left = right) -> c + left = c + right-plusConstantLeft left _ c refl = refl+plusConstantLeft left _ c Refl = Refl  total plusOneSucc : (right : Nat) -> 1 + right = S right-plusOneSucc n = refl+plusOneSucc n = Refl  total plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->   (p : left + right = left + right') -> right = right'@@ -423,24 +429,24 @@  -- Mult total multZeroLeftZero : (right : Nat) -> Z * right = Z-multZeroLeftZero right = refl+multZeroLeftZero right = Refl  total multZeroRightZero : (left : Nat) -> left * Z = Z-multZeroRightZero Z        = refl+multZeroRightZero Z        = Refl multZeroRightZero (S left) =   let inductiveHypothesis = multZeroRightZero left in     ?multZeroRightZeroStepCase  total multRightSuccPlus : (left : Nat) -> (right : Nat) ->   left * (S right) = left + (left * right)-multRightSuccPlus Z        right = refl+multRightSuccPlus Z        right = Refl multRightSuccPlus (S left) right =   let inductiveHypothesis = multRightSuccPlus left right in     ?multRightSuccPlusStepCase  total multLeftSuccPlus : (left : Nat) -> (right : Nat) ->   (S left) * right = right + (left * right)-multLeftSuccPlus left right = refl+multLeftSuccPlus left right = Refl  total multCommutative : (left : Nat) -> (right : Nat) ->   left * right = right * left@@ -451,33 +457,33 @@  total multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left * (centre + right) = (left * centre) + (left * right)-multDistributesOverPlusRight Z        centre right = refl+multDistributesOverPlusRight Z        centre right = Refl multDistributesOverPlusRight (S left) centre right =   let inductiveHypothesis = multDistributesOverPlusRight left centre right in     ?multDistributesOverPlusRightStepCase  total multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   (left + centre) * right = (left * right) + (centre * right)-multDistributesOverPlusLeft Z        centre right = refl+multDistributesOverPlusLeft Z        centre right = Refl multDistributesOverPlusLeft (S left) centre right =   let inductiveHypothesis = multDistributesOverPlusLeft left centre right in     ?multDistributesOverPlusLeftStepCase  total multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left * (centre * right) = (left * centre) * right-multAssociative Z        centre right = refl+multAssociative Z        centre right = Refl multAssociative (S left) centre right =   let inductiveHypothesis = multAssociative left centre right in     ?multAssociativeStepCase  total multOneLeftNeutral : (right : Nat) -> 1 * right = right-multOneLeftNeutral Z         = refl+multOneLeftNeutral Z         = Refl multOneLeftNeutral (S right) =   let inductiveHypothesis = multOneLeftNeutral right in     ?multOneLeftNeutralStepCase  total multOneRightNeutral : (left : Nat) -> left * 1 = left-multOneRightNeutral Z        = refl+multOneRightNeutral Z        = Refl multOneRightNeutral (S left) =   let inductiveHypothesis = multOneRightNeutral left in     ?multOneRightNeutralStepCase@@ -485,53 +491,53 @@ -- Minus total minusSuccSucc : (left : Nat) -> (right : Nat) ->   (S left) - (S right) = left - right-minusSuccSucc left right = refl+minusSuccSucc left right = Refl  total minusZeroLeft : (right : Nat) -> 0 - right = Z-minusZeroLeft right = refl+minusZeroLeft right = Refl  total minusZeroRight : (left : Nat) -> left - 0 = left-minusZeroRight Z        = refl-minusZeroRight (S left) = refl+minusZeroRight Z        = Refl+minusZeroRight (S left) = Refl  total minusZeroN : (n : Nat) -> Z = n - n-minusZeroN Z     = refl+minusZeroN Z     = Refl minusZeroN (S n) = minusZeroN n  total minusOneSuccN : (n : Nat) -> S Z = (S n) - n-minusOneSuccN Z     = refl+minusOneSuccN Z     = Refl minusOneSuccN (S n) = minusOneSuccN n  total minusSuccOne : (n : Nat) -> S n - 1 = n-minusSuccOne Z     = refl-minusSuccOne (S n) = refl+minusSuccOne Z     = Refl+minusSuccOne (S n) = Refl  total minusPlusZero : (n : Nat) -> (m : Nat) -> n - (n + m) = Z-minusPlusZero Z     m = refl+minusPlusZero Z     m = Refl minusPlusZero (S n) m = minusPlusZero n m  total minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   left - centre - right = left - (centre + right)-minusMinusMinusPlus Z        Z          right = refl-minusMinusMinusPlus (S left) Z          right = refl-minusMinusMinusPlus Z        (S centre) right = refl+minusMinusMinusPlus Z        Z          right = Refl+minusMinusMinusPlus (S left) Z          right = Refl+minusMinusMinusPlus Z        (S centre) right = Refl minusMinusMinusPlus (S left) (S centre) right =   let inductiveHypothesis = minusMinusMinusPlus left centre right in     ?minusMinusMinusPlusStepCase  total plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->   (left + right) - (left + right') = right - right'-plusMinusLeftCancel Z right right'        = refl+plusMinusLeftCancel Z right right'        = Refl plusMinusLeftCancel (S left) right right' =   let inductiveHypothesis = plusMinusLeftCancel left right right' in     ?plusMinusLeftCancelStepCase  total multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) ->   (left - centre) * right = (left * right) - (centre * right)-multDistributesOverMinusLeft Z        Z          right = refl+multDistributesOverMinusLeft Z        Z          right = Refl multDistributesOverMinusLeft (S left) Z          right =   ?multDistributesOverMinusLeftBaseCase-multDistributesOverMinusLeft Z        (S centre) right = refl+multDistributesOverMinusLeft Z        (S centre) right = Refl multDistributesOverMinusLeft (S left) (S centre) right =   let inductiveHypothesis = multDistributesOverMinusLeft left centre right in     ?multDistributesOverMinusLeftStepCase@@ -544,7 +550,7 @@ -- Power total powerSuccPowerLeft : (base : Nat) -> (exp : Nat) -> power base (S exp) =   base * (power base exp)-powerSuccPowerLeft base exp = refl+powerSuccPowerLeft base exp = Refl  total multPowerPowerPlus : (base : Nat) -> (exp : Nat) -> (exp' : Nat) ->   (power base exp) * (power base exp') = power base (exp + exp')@@ -554,22 +560,22 @@     ?multPowerPowerPlusStepCase  total powerZeroOne : (base : Nat) -> power base 0 = S Z-powerZeroOne base = refl+powerZeroOne base = Refl  total powerOneNeutral : (base : Nat) -> power base 1 = base-powerOneNeutral Z        = refl+powerOneNeutral Z        = Refl powerOneNeutral (S base) =   let inductiveHypothesis = powerOneNeutral base in     ?powerOneNeutralStepCase  total powerOneSuccOne : (exp : Nat) -> power 1 exp = S Z-powerOneSuccOne Z       = refl+powerOneSuccOne Z       = Refl powerOneSuccOne (S exp) =   let inductiveHypothesis = powerOneSuccOne exp in     ?powerOneSuccOneStepCase  total powerSuccSuccMult : (base : Nat) -> power base 2 = mult base base-powerSuccSuccMult Z        = refl+powerSuccSuccMult Z        = Refl powerSuccSuccMult (S base) =   let inductiveHypothesis = powerSuccSuccMult base in     ?powerSuccSuccMultStepCase@@ -583,11 +589,11 @@  -- Pred total predSucc : (n : Nat) -> pred (S n) = n-predSucc n = refl+predSucc n = Refl  total minusSuccPred : (left : Nat) -> (right : Nat) ->   left - (S right) = pred (left - right)-minusSuccPred Z        right = refl+minusSuccPred Z        right = Refl minusSuccPred (S left) Z =   let inductiveHypothesis = minusSuccPred left Z in     ?minusSuccPredStepCase@@ -598,125 +604,125 @@ -- boolElim total boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->   S (boolElim cond t f) = boolElim cond (S t) (S f)-boolElimSuccSucc True  t f = refl-boolElimSuccSucc False t f = refl+boolElimSuccSucc True  t f = Refl+boolElimSuccSucc False t f = Refl  total boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->   left + (boolElim cond t f) = boolElim cond (left + t) (left + f)-boolElimPlusPlusLeft True  left t f = refl-boolElimPlusPlusLeft False left t f = refl+boolElimPlusPlusLeft True  left t f = Refl+boolElimPlusPlusLeft False left t f = Refl  total boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->   (boolElim cond t f) + right = boolElim cond (t + right) (f + right)-boolElimPlusPlusRight True  right t f = refl-boolElimPlusPlusRight False right t f = refl+boolElimPlusPlusRight True  right t f = Refl+boolElimPlusPlusRight False right t f = Refl  total boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->   left * (boolElim cond t f) = boolElim cond (left * t) (left * f)-boolElimMultMultLeft True  left t f = refl-boolElimMultMultLeft False left t f = refl+boolElimMultMultLeft True  left t f = Refl+boolElimMultMultLeft False left t f = Refl  total boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->   (boolElim cond t f) * right = boolElim cond (t * right) (f * right)-boolElimMultMultRight True  right t f = refl-boolElimMultMultRight False right t f = refl+boolElimMultMultRight True  right t f = Refl+boolElimMultMultRight False right t f = Refl  -- Orders total lteNTrue : (n : Nat) -> lte n n = True-lteNTrue Z     = refl+lteNTrue Z     = Refl lteNTrue (S n) = lteNTrue n -total lteSuccZeroFalse : (n : Nat) -> lte (S n) Z = False-lteSuccZeroFalse Z     = refl-lteSuccZeroFalse (S n) = refl+total LTESuccZeroFalse : (n : Nat) -> lte (S n) Z = False+LTESuccZeroFalse Z     = Refl+LTESuccZeroFalse (S n) = Refl  -- Minimum and maximum total maximumAssociative : (l,c,r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r-maximumAssociative Z c r = refl-maximumAssociative (S k) Z r = refl-maximumAssociative (S k) (S j) Z = refl-maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in refl+maximumAssociative Z c r = Refl+maximumAssociative (S k) Z r = Refl+maximumAssociative (S k) (S j) Z = Refl+maximumAssociative (S k) (S j) (S i) = rewrite maximumAssociative k j i in Refl  total maximumCommutative : (l, r : Nat) -> maximum l r = maximum r l-maximumCommutative Z Z = refl-maximumCommutative Z (S k) = refl-maximumCommutative (S k) Z = refl-maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in refl+maximumCommutative Z Z = Refl+maximumCommutative Z (S k) = Refl+maximumCommutative (S k) Z = Refl+maximumCommutative (S k) (S j) = rewrite maximumCommutative k j in Refl  total maximumIdempotent : (n : Nat) -> maximum n n = n-maximumIdempotent Z = refl+maximumIdempotent Z = Refl maximumIdempotent (S k) = cong (maximumIdempotent k)  total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r-minimumAssociative Z c r = refl-minimumAssociative (S k) Z r = refl-minimumAssociative (S k) (S j) Z = refl-minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in refl+minimumAssociative Z c r = Refl+minimumAssociative (S k) Z r = Refl+minimumAssociative (S k) (S j) Z = Refl+minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl  total minimumCommutative : (l, r : Nat) -> minimum l r = minimum r l-minimumCommutative Z Z = refl-minimumCommutative Z (S k) = refl-minimumCommutative (S k) Z = refl-minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in refl+minimumCommutative Z Z = Refl+minimumCommutative Z (S k) = Refl+minimumCommutative (S k) Z = Refl+minimumCommutative (S k) (S j) = rewrite minimumCommutative k j in Refl  total minimumIdempotent : (n : Nat) -> minimum n n = n-minimumIdempotent Z = refl+minimumIdempotent Z = Refl minimumIdempotent (S k) = cong (minimumIdempotent k)  total minimumZeroZeroRight : (right : Nat) -> minimum 0 right = Z-minimumZeroZeroRight Z = refl+minimumZeroZeroRight Z = Refl minimumZeroZeroRight (S right) = minimumZeroZeroRight right  total minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = Z-minimumZeroZeroLeft Z        = refl-minimumZeroZeroLeft (S left) = refl+minimumZeroZeroLeft Z        = Refl+minimumZeroZeroLeft (S left) = Refl  total minimumSuccSucc : (left : Nat) -> (right : Nat) ->   minimum (S left) (S right) = S (minimum left right)-minimumSuccSucc Z        Z         = refl-minimumSuccSucc (S left) Z         = refl-minimumSuccSucc Z        (S right) = refl+minimumSuccSucc Z        Z         = Refl+minimumSuccSucc (S left) Z         = Refl+minimumSuccSucc Z        (S right) = Refl minimumSuccSucc (S left) (S right) =   let inductiveHypothesis = minimumSuccSucc left right in     ?minimumSuccSuccStepCase  total maximumZeroNRight : (right : Nat) -> maximum Z right = right-maximumZeroNRight Z         = refl-maximumZeroNRight (S right) = refl+maximumZeroNRight Z         = Refl+maximumZeroNRight (S right) = Refl  total maximumZeroNLeft : (left : Nat) -> maximum left Z = left-maximumZeroNLeft Z        = refl-maximumZeroNLeft (S left) = refl+maximumZeroNLeft Z        = Refl+maximumZeroNLeft (S left) = Refl  total maximumSuccSucc : (left : Nat) -> (right : Nat) ->   S (maximum left right) = maximum (S left) (S right)-maximumSuccSucc Z        Z         = refl-maximumSuccSucc (S left) Z         = refl-maximumSuccSucc Z        (S right) = refl+maximumSuccSucc Z        Z         = Refl+maximumSuccSucc (S left) Z         = Refl+maximumSuccSucc Z        (S right) = Refl maximumSuccSucc (S left) (S right) =   let inductiveHypothesis = maximumSuccSucc left right in     ?maximumSuccSuccStepCase  total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)-sucMaxL Z = refl+sucMaxL Z = Refl sucMaxL (S l) = cong (sucMaxL l)  total sucMaxR : (l : Nat) -> maximum l (S l) = (S l)-sucMaxR Z = refl+sucMaxR Z = Refl sucMaxR (S l) = cong (sucMaxR l)  total sucMinL : (l : Nat) -> minimum (S l) l = l-sucMinL Z = refl+sucMinL Z = Refl sucMinL (S l) = cong (sucMinL l)  total sucMinR : (l : Nat) -> minimum l (S l) = l-sucMinR Z = refl+sucMinR Z = Refl sucMinR (S l) = cong (sucMinR l)  -- div and mod total modZeroZero : (n : Nat) -> mod 0 n = Z-modZeroZero Z     = refl-modZeroZero (S n) = refl+modZeroZero Z     = Refl+modZeroZero (S n) = Refl  -------------------------------------------------------------------------------- -- Proofs

@@ -9,27 +9,27 @@    ||| Dependent pair where the first field is erased.   data Exists : (P : a -> Type) -> Type where-    evidence : .(x : a) -> (pf : P x) -> Exists P+    Evidence : .(x : a) -> (pf : P x) -> Exists P    ||| Dependent pair where the second field is erased.    data Subset : (a : Type) -> (P : a -> Type) -> Type where-    element : (x : a) -> .(pf : P x) -> Subset a P+    Element : (x : a) -> .(pf : P x) -> Subset a P    -- Monomorphic projections    namespace Exists     getWitness : Exists {a} P -> a-    getWitness (evidence x pf) = x+    getWitness (Evidence x pf) = x      getProof : (x : Exists {a} P) -> P (getWitness x)-    getProof (evidence x pf) = pf+    getProof (Evidence x pf) = pf    namespace Subset     getWitness : Subset a P -> a-    getWitness (element x pf) = x+    getWitness (Element x pf) = x      getProof : (x : Subset a P) -> P (getWitness x)-    getProof (element x pf) = pf+    getProof (Element x pf) = pf    namespace Sigma     getWitness : Sigma a P -> a

@@ -57,13 +57,25 @@ zipWith : (a -> b -> c) -> Stream a -> Stream b -> Stream c zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys +||| Combine three streams by applying a function element-wise along them+zipWith3 : (a -> b -> c -> d) -> Stream a -> Stream b -> Stream c -> Stream d+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs+ ||| Create a stream of pairs from two streams zip : Stream a -> Stream b -> Stream (a, b) zip = zipWith (\x,y => (x,y)) +||| Combine three streams into a stream of tuples elementwise+zip3 : Stream a -> Stream b -> Stream c -> Stream (a, b, c)+zip3 = zipWith3 (\x,y,z => (x,y,z))+ ||| Create a pair of streams from a stream of pairs unzip : Stream (a, b) -> (Stream a, Stream b) unzip xs = (map fst xs, map snd xs)++||| Split a stream of three-element tuples into three streams+unzip3 : Stream (a, b, c) -> (Stream a, Stream b, Stream c)+unzip3 xs = (map (\(x,_,_) => x) xs, map (\(_,x,_) => x) xs, map (\(_,_,x) => x) xs)  ||| Return the diagonal elements of a stream of streams diag : Stream (Stream a) -> Stream a

@@ -74,11 +74,11 @@     StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)  ||| Version of 'strHead' that statically verifies that the string is not empty.-strHead' : (x : String) -> so (not (x == "")) -> Char+strHead' : (x : String) -> So (not (x == "")) -> Char strHead' x p = assert_total $ prim__strHead x  ||| Version of 'strTail' that statically verifies that the string is not empty.-strTail' : (x : String) -> so (not (x == "")) -> String+strTail' : (x : String) -> So (not (x == "")) -> String strTail' x p = assert_total $ prim__strTail x  -- we need the 'believe_me' because the operations are primitives

@@ -6,9 +6,9 @@ class Uninhabited t where   ||| If I have a t, I've had a contradiction   ||| @ t the uninhabited type-  total uninhabited : t -> _|_+  total uninhabited : t -> Void -instance Uninhabited _|_ where+instance Uninhabited Void where   uninhabited a = a  ||| Use an absurd assumption to discharge a proof obligation@@ -16,4 +16,4 @@ ||| @ a the goal type ||| @ h the contradictory hypothesis absurd : Uninhabited t => (h : t) -> a-absurd h = FalseElim (uninhabited h)+absurd h = void (uninhabited h)

@@ -37,8 +37,8 @@  ||| Show that the length function on vectors in fact calculates the length private lengthCorrect : (n : Nat) -> (xs : Vect n a) -> length xs = n-lengthCorrect Z [] = refl-lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in refl+lengthCorrect Z     []        = Refl+lengthCorrect (S n) (x :: xs) = rewrite lengthCorrect n xs in Refl  -------------------------------------------------------------------------------- -- Indexing into vectors@@ -64,35 +64,36 @@  ||| Extract a particular element from a vector index : Fin n -> Vect n a -> a-index fZ     (x::xs) = x-index (fS k) (x::xs) = index k xs-index fZ     [] impossible+index FZ     (x::xs) = x+index (FS k) (x::xs) = index k xs+index FZ     [] impossible + ||| Insert an element at a particular index insertAt : Fin (S n) -> a -> Vect n a -> Vect (S n) a-insertAt fZ     y xs      = y :: xs-insertAt (fS k) y (x::xs) = x :: insertAt k y xs-insertAt (fS k) y []      = absurd k+insertAt FZ     y xs      = y :: xs+insertAt (FS k) y (x::xs) = x :: insertAt k y xs+insertAt (FS k) y []      = absurd k  ||| Construct a new vector consisting of all but the indicated element deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a-deleteAt           fZ     (x::xs) = xs-deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs-deleteAt {n = Z}   (fS k) (x::xs) = absurd k-deleteAt           _      [] impossible+deleteAt           FZ     (x::xs) = xs+deleteAt {n = S m} (FS k) (x::xs) = x :: deleteAt k xs+deleteAt {n = Z}   (FS k) (x::xs) = absurd k+deleteAt           _      []      impossible  ||| Replace an element at a particlar index with another replaceAt : Fin n -> t -> Vect n t -> Vect n t-replaceAt fZ     y (x::xs) = y :: xs-replaceAt (fS k) y (x::xs) = x :: replaceAt k y xs+replaceAt FZ     y (x::xs) = y :: xs+replaceAt (FS k) y (x::xs) = x :: replaceAt k y xs  ||| Replace the element at a particular index with the result of applying a function to it ||| @ i the index to replace at ||| @ f the update function ||| @ xs the vector to replace in updateAt : (i : Fin n) -> (f : t -> t) -> (xs : Vect n t) -> Vect n t-updateAt fZ     f (x::xs) = f x :: xs-updateAt (fS k) f (x::xs) = x :: updateAt k f xs+updateAt FZ     f (x::xs) = f x :: xs+updateAt (FS k) f (x::xs) = x :: updateAt k f xs  -------------------------------------------------------------------------------- -- Subvectors@@ -101,32 +102,51 @@ ||| Get the first m elements of a Vect ||| @ m the number of elements to take take : (n : Nat) -> Vect (n + m) a -> Vect n a-take Z xs = []+take Z     xs        = [] take (S k) (x :: xs) = x :: take k xs  ||| Remove the first m elements of a Vect ||| @ m the number of elements to remove drop : (n : Nat) -> Vect (n + m) a -> Vect m a-drop Z xs = xs+drop Z     xs        = xs drop (S k) (x :: xs) = drop k xs +||| Take the longest prefix of a Vect such that all elements satisfy some+||| Boolean predicate.+|||+||| @ p the predicate+takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)+takeWhile p []      = (_ ** [])+takeWhile p (x::xs) =+  let (len ** ys) = takeWhile p xs+  in if p x then+      (S len ** x :: ys)+    else+      (_ ** [])++||| Remove the longest prefix of a Vect such that all removed elements satisfy some+||| Boolean predicate.+|||+||| @ p the predicate+dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)+dropWhile p [] = (_ ** [])+dropWhile p (x::xs) =+  if p x then+    dropWhile p xs+  else+    (_ ** x::xs)+ -------------------------------------------------------------------------------- -- Transformations --------------------------------------------------------------------------------  ||| Reverse the order of the elements of a vector-total reverse : {n : Nat} -> Vect n a -> Vect n a-reverse {n} xs = reverse' [] (plusZeroRightNeutral n) xs-  where-    total reverse' : {m, j, l : Nat} ->-                     Vect m a -> (j + m = l) -> Vect j a -> Vect l a-    reverse' {m} {j = Z  } {l} acc prf []      ?= acc-    reverse' {m} {j = S k} {l} acc prf (x::xs)  =-      let prf1 : (m + (S k) = l) = rewrite plusCommutative m (S k) in prf in-      let prf2 : (S (m + k) = l) = rewrite plusSuccRightSucc m k in prf1 in-      let prf3 : (S (k + m) = l) = rewrite plusCommutative k m in prf2 in-      let prf4 : (k + (S m) = l) = rewrite sym $ plusSuccRightSucc k m in prf3 in-      reverse' (x::acc) prf4 xs+reverse : Vect n a -> Vect n a+reverse xs = go [] xs+  where go : Vect n a -> Vect m a -> Vect (n+m) a+        go {n}         acc []        = rewrite plusZeroRightNeutral n in acc+        go {n} {m=S m} acc (x :: xs) = rewrite sym $ plusSuccRightSucc n m+                                       in go (x::acc) xs  ||| Alternate an element between the other elements of a vector ||| @ sep the element to intersperse@@ -136,8 +156,9 @@ intersperse sep (x::xs) = x :: intersperse' sep xs   where     intersperse' : a -> Vect n a -> Vect (n + n) a-    intersperse' sep []      = []-    intersperse' sep (x::xs) ?= sep :: x :: intersperse' sep xs+    intersperse'         sep []      = []+    intersperse' {n=S n} sep (x::xs) = rewrite sym $ plusSuccRightSucc n n+                                       in sep :: x :: intersperse' sep xs  -------------------------------------------------------------------------------- -- Conversion from list (toList is provided by Foldable)@@ -147,7 +168,7 @@ fromList' : Vect n a -> (l : List a) -> Vect (length l + n) a fromList' ys [] = ys fromList' {n} ys (x::xs) =-  rewrite (plusSuccRightSucc (length xs) n) ==> +  rewrite (plusSuccRightSucc (length xs) n) ==>           Vect (plus (length xs) (S n)) a in   fromList' (x::ys) xs @@ -184,16 +205,31 @@ zipWith f []      []      = [] zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys +||| Combine three equal-length vectors into a vector with some function+zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d+zipWith3 f []      []      []      = []+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs+ ||| Combine two equal-length vectors pairwise zip : Vect n a -> Vect n b -> Vect n (a, b)-zip = zipWith (\x => \y => (x,y))+zip = zipWith (\x,y => (x,y)) +||| Combine three equal-length vectors elementwise into a vector of tuples+zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)+zip3 = zipWith3 (\x,y,z => (x,y,z))+ ||| Convert a vector of pairs to a pair of vectors unzip : Vect n (a, b) -> (Vect n a, Vect n b) unzip []           = ([], []) unzip ((l, r)::xs) with (unzip xs)   | (lefts, rights) = (l::lefts, r::rights) +||| Convert a vector of three-tuples to a triplet of vectors+unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)+unzip3 []            = ([], [], [])+unzip3 ((l,c,r)::xs) with (unzip3 xs)+  | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)+ -------------------------------------------------------------------------------- -- Equality --------------------------------------------------------------------------------@@ -212,7 +248,7 @@ --------------------------------------------------------------------------------  instance Ord a => Ord (Vect n a) where-  compare [] [] = EQ+  compare []      []      = EQ   compare (x::xs) (y::ys) =     if x /= y then       compare x y@@ -228,16 +264,25 @@   map f []        = []   map f (x::xs) = f x :: map f xs --- XXX: causes Idris to enter an infinite loop when type checking in the REPL---mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)---mapMaybe f []      = (_ ** [])---mapMaybe f (x::xs) = mapMaybe' (f x)--- XXX: working around the type restrictions on case statements---  where---    mapMaybe' : (Maybe b) -> (n ** Vect b n) -> (p ** Vect b p)---    mapMaybe' Nothing  (n ** tail) = (n   ** tail)---    mapMaybe' (Just j) (n ** tail) = (S n ** j::tail) +||| Map a partial function across a vector, returning those elements for which+||| the function had a value.+|||+||| The first projection of the resulting pair (ie the length) will always be+||| at most the length of the input vector. This is not, however, guaranteed+||| by the type.+|||+||| @ f the partial function (expressed by returning `Maybe`)+||| @ xs the vector to check for results+mapMaybe : (f : a -> Maybe b) -> (xs : Vect n a) -> (m : Nat ** Vect m b)+mapMaybe f []      = (_ ** [])+mapMaybe f (x::xs) =+  let (len ** ys) = mapMaybe f xs+  in case f x of+       Just y  => (S len ** y :: ys)+       Nothing => (  len **      ys)++ -------------------------------------------------------------------------------- -- Folds --------------------------------------------------------------------------------@@ -396,6 +441,15 @@ nub : Eq a => Vect n a -> (p ** Vect p a) nub = nubBy (==) +deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)+deleteBy _  _ []      = (_ ** [])+deleteBy eq x (y::ys) =+  let (len ** zs) = deleteBy eq x ys+  in if x `eq` y then (_ ** ys) else (S len ** y ::zs)++delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)+delete = deleteBy (==)+ -------------------------------------------------------------------------------- -- Splitting and breaking lists --------------------------------------------------------------------------------@@ -408,6 +462,15 @@ splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a) splitAt n xs = (take n xs, drop n xs) +partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))+partition p []      = ((_ ** []), (_ ** []))+partition p (x::xs) =+  let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in+    if p x then+      ((S leftLen ** x::lefts), (rightLen ** rights))+    else+      ((leftLen ** lefts), (S rightLen ** x::rights))+ -------------------------------------------------------------------------------- -- Predicates --------------------------------------------------------------------------------@@ -451,18 +514,18 @@   | (_ ** tail) = (_ ** j::tail)  diag : Vect n (Vect n a) -> Vect n a-diag [] = []+diag []             = [] diag ((x::xs)::xss) = x :: diag (map tail xss)  range : Vect n (Fin n)-range {n=Z} = []-range {n=S _} = fZ :: map fS range+range {n=Z}   = []+range {n=S _} = FZ :: map FS range  ||| Transpose a Vect of Vects, turning rows into columns and vice versa. ||| ||| As the types ensure rectangularity, this is an involution, unlike `Prelude.List.transpose`. transpose : Vect m (Vect n a) -> Vect n (Vect m a)-transpose [] = replicate _ []+transpose []        = replicate _ [] transpose (x :: xs) = zipWith (::) x (transpose xs)  --------------------------------------------------------------------------------@@ -470,32 +533,16 @@ --------------------------------------------------------------------------------  vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)-vectConsCong x xs xs refl = refl+vectConsCong x xs xs Refl = Refl  vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs-vectNilRightNeutral [] = refl+vectNilRightNeutral [] = Refl vectNilRightNeutral (x :: xs) =   vectConsCong _ _ _ (vectNilRightNeutral xs)  vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z-vectAppendAssociative [] y z = refl+vectAppendAssociative [] y z = Refl vectAppendAssociative (x :: xs) ys zs =   vectConsCong _ _ _ (vectAppendAssociative xs ys zs)  ------------------------------------------------------------------------------------ Proofs-----------------------------------------------------------------------------------Prelude.Vect.reverse'_lemma_1 = proof {-    intros;-    rewrite prf;-    rewrite sym (plusZeroRightNeutral m);-    exact value;-}--Prelude.Vect.intersperse'_lemma_1 = proof {-  intros;-  rewrite (plusSuccRightSucc n1 n1);-  trivial;-}

@@ -1,25 +0,0 @@-include ../config.mk--PKG_CONFIG_CFLAGS:=$(shell (pkg-config --version >/dev/null 2>&1) && pkg-config --cflags bdw-gc)-CFLAGS:=-Wextra -fPIC -Wno-unused-parameter $(PKG_CONFIG_CFLAGS) $(CFLAGS)-SOURCES=defs.c-OBJECTS=$(SOURCES:.c=.o)-LIB=libidris_rts.a--build: $(SOURCES) $(LIB)--$(LIB): $(OBJECTS)-	ar r $@ $(OBJECTS)-	ranlib $@--.c.o:-	$(CC) -c $(CFLAGS) $< -o $@--install: $(LIB)-	mkdir -p $(TARGET)-	install $(LIB) $(TARGET)--clean:-	rm -f $(OBJECTS) $(LIB)--.PHONY: build install clean

@@ -1,182 +0,0 @@-#include <stdlib.h>-#include <stdio.h>-#include <gmp.h>-#include <gc.h>-#include <string.h>-#include <inttypes.h>--extern char** environ;--void putStr(const char *str) {-  fputs(str, stdout);-}--void putErr(const char *str) {-  fputs(str, stderr);-}--void mpz_init_set_ull(mpz_t n, unsigned long long ull)-{-  mpz_init_set_ui(n, (unsigned int)(ull >> 32)); /* n = (unsigned int)(ull >> 32) */-  mpz_mul_2exp(n, n, 32);                   /* n <<= 32 */-  mpz_add_ui(n, n, (unsigned int)ull);      /* n += (unsigned int)ull */-}--void mpz_init_set_sll(mpz_t n, long long sll)-{-  mpz_init_set_si(n, (int)(sll >> 32));     /* n = (int)sll >> 32 */-  mpz_mul_2exp(n, n, 32 );             /* n <<= 32 */-  mpz_add_ui(n, n, (unsigned int)sll); /* n += (unsigned int)sll */-}--void mpz_set_sll(mpz_t n, long long sll)-{-  mpz_set_si(n, (int)(sll >> 32));     /* n = (int)sll >> 32 */-  mpz_mul_2exp(n, n, 32 );             /* n <<= 32 */-  mpz_add_ui(n, n, (unsigned int)sll); /* n += (unsigned int)sll */-}--unsigned long long mpz_get_ull(mpz_t n)-{-  unsigned int lo, hi;-  mpz_t tmp;--  mpz_init( tmp );-  mpz_mod_2exp( tmp, n, 64 );   /* tmp = (lower 64 bits of n) */--  lo = mpz_get_ui( tmp );       /* lo = tmp & 0xffffffff */ -  mpz_div_2exp( tmp, tmp, 32 ); /* tmp >>= 32 */-  hi = mpz_get_ui( tmp );       /* hi = tmp & 0xffffffff */--  mpz_clear( tmp );--  return (((unsigned long long)hi) << 32) + lo;-}--char *__idris_strCons(char c, char *s) {-  size_t len = strlen(s);-  char *result = GC_malloc_atomic(len+2);-  result[0] = c;-  memcpy(result+1, s, len);-  result[len+1] = 0;-  return result;-}--#define BUFSIZE 256-char *__idris_readStr(FILE* h) {-// Modified from 'safe-fgets.c' in the gdb distribution.-// (see http://www.gnu.org/software/gdb/current/)-  char *line_ptr;-  char* line_buf = (char *) GC_malloc (BUFSIZE);-  int line_buf_size = BUFSIZE;--  /* points to last byte */-  line_ptr = line_buf + line_buf_size - 1;--  /* so we can see if fgets put a 0 there */-  *line_ptr = 1;-  if (fgets (line_buf, line_buf_size, h) == 0)-    return "";--  /* we filled the buffer? */-  while (line_ptr[0] == 0 && line_ptr[-1] != '\n')-  {-    /* Make the buffer bigger and read more of the line */-    line_buf_size += BUFSIZE;-    line_buf = (char *) GC_realloc (line_buf, line_buf_size);--    /* points to last byte again */-    line_ptr = line_buf + line_buf_size - 1;-    /* so we can see if fgets put a 0 there */-    *line_ptr = 1;--    if (fgets (line_buf + line_buf_size - BUFSIZE - 1, BUFSIZE + 1, h) == 0)-      return "";-  }--  return line_buf;-}--void* fileOpen(char* name, char* mode) {-  FILE* f = fopen(name, mode);-  return (void*)f;-}--void fileClose(void* h) {-  FILE* f = (FILE*)h;-  fclose(f);-}--int fileEOF(void* h) {-  FILE* f = (FILE*)h;-  return feof(f);-}--int fileError(void* h) {-  FILE* f = (FILE*)h;-  return ferror(f);-}--void fputStr(void* h, char* str) {-  FILE* f = (FILE*)h;-  fputs(str, f);-}--int isNull(void* ptr) {-  return ptr==NULL;-}--char* getEnvPair(int i) {-    return *(environ + i);-}--void idris_memset(void* ptr, size_t offset, uint8_t c, size_t size) {-  memset(((uint8_t*)ptr) + offset, c, size);-}--uint8_t idris_peek(void* ptr, size_t offset) {-  return *(((uint8_t*)ptr) + offset);-}--void idris_poke(void* ptr, size_t offset, uint8_t data) {-  *(((uint8_t*)ptr) + offset) = data;-}--void idris_memmove(void* dest, void* src, size_t dest_offset, size_t src_offset, size_t size) {-  memmove(dest + dest_offset, src + src_offset, size);-}--void *__idris_gmpMalloc(size_t size) {-  return GC_malloc(size);-}--void *__idris_gmpRealloc(void *ptr, size_t oldSize, size_t size) {-  return GC_realloc(ptr, size);-}--void __idris_gmpFree(void *ptr, size_t oldSize) {-  GC_free(ptr);-}--char *__idris_strRev(const char *s) {-  int x = strlen(s);-  int y = 0;-  char *t = GC_malloc(x+1);--  t[x] = '\0';-  while(x>0) {-    t[y++] = s[--x];-  }-  return t;-}--int __idris_argc;-char **__idris_argv;--int idris_numArgs() {-    return __idris_argc;-}--const char* idris_getArg(int i) {-    return __idris_argv[i];-}

@@ -42,13 +42,16 @@           runMain (runIdris opts)  runIdris :: [Opt] -> Idris ()-runIdris [Client c] = do setVerbose False-                         setQuiet True-                         runIO $ runClient c runIdris opts = do        when (ShowIncs `elem` opts) $ runIO showIncs        when (ShowLibs `elem` opts) $ runIO showLibs        when (ShowLibdir `elem` opts) $ runIO showLibdir+       case opt getClient opts of+           []    -> return ()+           (c:_) -> do setVerbose False+                       setQuiet True+                       runIO $ runClient (getPort opts) c+                       runIO $ exitWith ExitSuccess        case opt getPkgCheck opts of            [] -> return ()            fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs

@@ -0,0 +1,29 @@+#include "idris_opts.h"+#include "idris_stats.h"+#include "idris_rts.h"+#include "Arduino.h"++// The default options should give satisfactory results under many circumstances.+RTSOpts opts = {+    .init_heap_size = 128,+    .max_stack_size = 128,+    .show_summary   = 0+};++// no argv or argc+int main() {+    init(); // arduino init function++    VM* vm = init_vm(opts.max_stack_size, opts.init_heap_size, 1);+    _idris__123_runMain0_125_(vm, NULL);++#ifdef IDRIS_DEBUG+    if (opts.show_summary) {+        idris_gcInfo(vm, 1);+    }+#endif++    Stats stats = terminate(vm);++    return 0;+}

@@ -1,58 +1,66 @@ #include "idris_rts.h"  VAL idris_b8CopyForGC(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 1);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8;+    cl->info.bits8 = A;     return cl; }  VAL idris_b16CopyForGC(VM *vm, VAL a) {+    uint16_t A = a->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 1);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16;+    cl->info.bits16 = A;     return cl; }  VAL idris_b32CopyForGC(VM *vm, VAL a) {+    uint32_t A = a->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 1);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32;+    cl->info.bits32 = A;     return cl; }  VAL idris_b64CopyForGC(VM *vm, VAL a) {+    uint64_t A = a->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 1);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64;+    cl->info.bits64 = A;     return cl; }  VAL idris_b8(VM *vm, VAL a) {+    uint8_t A = GETINT(a);     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = (uint8_t) GETINT(a);+    cl->info.bits8 = (uint8_t) A;     return cl; }  VAL idris_b16(VM *vm, VAL a) {+    uint16_t A = GETINT(a);     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = (uint16_t) GETINT(a);+    cl->info.bits16 = (uint16_t) A;     return cl; }  VAL idris_b32(VM *vm, VAL a) {+    uint32_t A = GETINT(a);     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = (uint32_t) GETINT(a);+    cl->info.bits32 = (uint32_t) A;     return cl; }  VAL idris_b64(VM *vm, VAL a) {+    uint64_t A = GETINT(a);     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = (uint64_t) GETINT(a);+    cl->info.bits64 = (uint64_t) A;     return cl; } @@ -89,51 +97,65 @@ }  VAL idris_b8Plus(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 + b->info.bits8;+    cl->info.bits8 = A + B;     return cl; }  VAL idris_b8Minus(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 - b->info.bits8;+    cl->info.bits8 = A - B;     return cl; }  VAL idris_b8Times(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 * b->info.bits8;+    cl->info.bits8 = A * B;     return cl; }  VAL idris_b8UDiv(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 / b->info.bits8;+    cl->info.bits8 = A / B;     return cl; }  VAL idris_b8SDiv(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = (uint8_t) (((int8_t) a->info.bits8) / ((int8_t) b->info.bits8));+    cl->info.bits8 = (uint8_t) (((int8_t) A) / ((int8_t) B));     return cl; }  VAL idris_b8URem(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 % b->info.bits8;+    cl->info.bits8 = A % B;     return cl; }  VAL idris_b8SRem(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = (uint8_t) (((int8_t) a->info.bits8) % ((int8_t) b->info.bits8));+    cl->info.bits8 = (uint8_t) (((int8_t) A) % ((int8_t) B));     return cl; } @@ -158,102 +180,127 @@ }  VAL idris_b8Compl(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = ~ a->info.bits8;+    cl->info.bits8 = ~ A;     return cl; }  VAL idris_b8And(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 & b->info.bits8;+    cl->info.bits8 = A & B;     return cl; }  VAL idris_b8Or(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 | b->info.bits8;+    cl->info.bits8 = A | B;     return cl; }  VAL idris_b8Xor(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 ^ b->info.bits8;+    cl->info.bits8 = A ^ B;     return cl; }  VAL idris_b8Shl(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 << b->info.bits8;+    cl->info.bits8 = A << B;     return cl; }  VAL idris_b8LShr(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = a->info.bits8 >> b->info.bits8;+    cl->info.bits8 = A >> B;     return cl; }  VAL idris_b8AShr(VM *vm, VAL a, VAL b) {+    uint8_t A = a->info.bits8;+    uint8_t B = b->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = (uint8_t) (((int8_t)a->info.bits8) >> ((int8_t)b->info.bits8));+    cl->info.bits8 = (uint8_t) (((int8_t) A) >> ((int8_t) B));     return cl; }  VAL idris_b16Plus(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 + b->info.bits16;+    cl->info.bits16 = A + B;     return cl; }  VAL idris_b16Minus(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 - b->info.bits16;+    cl->info.bits16 = A - B;     return cl; }  VAL idris_b16Times(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 * b->info.bits16;+    cl->info.bits16 = A * B;     return cl; }  VAL idris_b16UDiv(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 / b->info.bits16;+    cl->info.bits16 = A / B;     return cl; }  VAL idris_b16SDiv(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 =-    (uint16_t) (((int16_t) a->info.bits16) / ((int16_t) b->info.bits16));+    cl->info.bits16 = (uint16_t) (((int16_t) A) / ((int16_t) B));     return cl; }  VAL idris_b16URem(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 % b->info.bits16;+    cl->info.bits16 = A % B;     return cl; }  VAL idris_b16SRem(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 =-    (uint16_t) (((int16_t) a->info.bits16) % ((int16_t) b->info.bits16));+    cl->info.bits16 = (uint16_t) (((int16_t) A) % ((int16_t) B));     return cl; } @@ -278,102 +325,127 @@ }  VAL idris_b16Compl(VM *vm, VAL a) {+    uint16_t A = a->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = ~ a->info.bits16;+    cl->info.bits16 = ~ A;     return cl; }  VAL idris_b16And(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 & b->info.bits16;+    cl->info.bits16 = A & B;     return cl; }  VAL idris_b16Or(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 | b->info.bits16;+    cl->info.bits16 = A | B;     return cl; }  VAL idris_b16Xor(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 ^ b->info.bits16;+    cl->info.bits16 = A ^ B;     return cl; }  VAL idris_b16Shl(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 << b->info.bits16;+    cl->info.bits16 = A << B;     return cl; }  VAL idris_b16LShr(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = a->info.bits16 >> b->info.bits16;+    cl->info.bits16 = A >> B;     return cl; }  VAL idris_b16AShr(VM *vm, VAL a, VAL b) {+    uint16_t A = a->info.bits16;+    uint16_t B = b->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = (uint16_t) (((int16_t)a->info.bits16) >> ((int16_t)b->info.bits16));+    cl->info.bits16 = (uint16_t) (((int16_t) A) >> ((int16_t) B));     return cl; }  VAL idris_b32Plus(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 + b->info.bits32;+    cl->info.bits32 = A + B;     return cl; }  VAL idris_b32Minus(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 - b->info.bits32;+    cl->info.bits32 = A - B;     return cl; }  VAL idris_b32Times(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 * b->info.bits32;+    cl->info.bits32 = A * B;     return cl; }  VAL idris_b32UDiv(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 / b->info.bits32;+    cl->info.bits32 = A / B;     return cl; }  VAL idris_b32SDiv(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 =-    (uint32_t) (((int32_t) a->info.bits32) / ((int32_t) b->info.bits32));+    cl->info.bits32 = (uint32_t) (((int32_t) A) / ((int32_t) B));     return cl; }  VAL idris_b32URem(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 % b->info.bits32;+    cl->info.bits32 = A % B;     return cl; }  VAL idris_b32SRem(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 =-    (uint32_t) (((int32_t) a->info.bits32) % ((int32_t) b->info.bits32));+    cl->info.bits32 = (uint32_t) (((int32_t) A) % ((int32_t) B));     return cl; } @@ -398,102 +470,127 @@ }  VAL idris_b32Compl(VM *vm, VAL a) {+    uint32_t A = a->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = ~ a->info.bits32;+    cl->info.bits32 = ~ A;     return cl; }  VAL idris_b32And(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 & b->info.bits32;+    cl->info.bits32 = A & B;     return cl; }  VAL idris_b32Or(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 | b->info.bits32;+    cl->info.bits32 = A | B;     return cl; }  VAL idris_b32Xor(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 ^ b->info.bits32;+    cl->info.bits32 = A ^ B;     return cl; }  VAL idris_b32Shl(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 << b->info.bits32;+    cl->info.bits32 = A << B;     return cl; }  VAL idris_b32LShr(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = a->info.bits32 >> b->info.bits32;+    cl->info.bits32 = A >> B;     return cl; }  VAL idris_b32AShr(VM *vm, VAL a, VAL b) {+    uint32_t A = a->info.bits32;+    uint32_t B = b->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = (uint32_t) (((int32_t)a->info.bits32) >> ((int32_t)b->info.bits32));+    cl->info.bits32 = (uint32_t) (((int32_t)A) >> ((int32_t)B));     return cl; }  VAL idris_b64Plus(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 + b->info.bits64;+    cl->info.bits64 = A + B;     return cl; }  VAL idris_b64Minus(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 - b->info.bits64;+    cl->info.bits64 = A - B;     return cl; }  VAL idris_b64Times(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 * b->info.bits64;+    cl->info.bits64 = A * B;     return cl; }  VAL idris_b64UDiv(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 / b->info.bits64;+    cl->info.bits64 = A / B;     return cl; }  VAL idris_b64SDiv(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 =-    (uint64_t) (((int64_t) a->info.bits64) / ((int64_t) b->info.bits64));+    cl->info.bits64 = (uint64_t) (((int64_t) A) / ((int64_t) B));     return cl; }  VAL idris_b64URem(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 % b->info.bits64;+    cl->info.bits64 = A % B;     return cl; }  VAL idris_b64SRem(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 =-    (uint64_t) (((int64_t) a->info.bits64) % ((int64_t) b->info.bits64));+    cl->info.bits64 = (uint64_t) (((int64_t) A) % ((int64_t) B));     return cl; } @@ -518,177 +615,208 @@ }  VAL idris_b64Compl(VM *vm, VAL a) {+    uint64_t A = a->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = ~ a->info.bits64;+    cl->info.bits64 = ~ A;     return cl; }  VAL idris_b64And(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 & b->info.bits64;+    cl->info.bits64 = A & B;     return cl; }  VAL idris_b64Or(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 | b->info.bits64;+    cl->info.bits64 = A | B;     return cl; }  VAL idris_b64Xor(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 ^ b->info.bits64;+    cl->info.bits64 = A ^ B;     return cl; }  VAL idris_b64Shl(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 << b->info.bits64;+    cl->info.bits64 = A << B;     return cl; }  VAL idris_b64LShr(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = a->info.bits64 >> b->info.bits64;+    cl->info.bits64 = A >> B;     return cl; }  VAL idris_b64AShr(VM *vm, VAL a, VAL b) {+    uint64_t A = a->info.bits64;+    uint64_t B = b->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = (uint64_t) (((int64_t)a->info.bits64) >> ((int64_t)b->info.bits64));+    cl->info.bits64 = (uint64_t) (((int64_t) A) >> ((int64_t) B));     return cl; }  VAL idris_b8Z16(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = (uint16_t) a->info.bits8;+    cl->info.bits16 = (uint16_t) A;     return cl; }  VAL idris_b8Z32(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = (uint32_t) a->info.bits8;+    cl->info.bits32 = (uint32_t) A;     return cl; }  VAL idris_b8Z64(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);-    SETTY(cl, BITS16);-    cl->info.bits64 = (uint64_t) a->info.bits8;+    SETTY(cl, BITS64);+    cl->info.bits64 = (uint64_t) A;     return cl; }  VAL idris_b8S16(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = (uint16_t) (int16_t) (int8_t) a->info.bits8;+    cl->info.bits16 = (uint16_t) (int16_t) (int8_t) A;     return cl; }  VAL idris_b8S32(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = (uint32_t) (int32_t) (int8_t) a->info.bits8;+    cl->info.bits32 = (uint32_t) (int32_t) (int8_t) A;     return cl; }  VAL idris_b8S64(VM *vm, VAL a) {+    uint8_t A = a->info.bits8;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = (uint64_t) (int64_t) (int8_t) a->info.bits8;+    cl->info.bits64 = (uint64_t) (int64_t) (int8_t) A;     return cl; }  VAL idris_b16Z32(VM *vm, VAL a) {+    uint16_t A = a->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = (uint32_t) a->info.bits16;+    cl->info.bits32 = (uint32_t) A;     return cl; }  VAL idris_b16Z64(VM *vm, VAL a) {+    uint16_t A = a->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = (uint64_t) a->info.bits16;+    cl->info.bits64 = (uint64_t) A;     return cl; }  VAL idris_b16S32(VM *vm, VAL a) {+    uint16_t A = a->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = (uint32_t) (int32_t) (int16_t) a->info.bits16;+    cl->info.bits32 = (uint32_t) (int32_t) (int16_t) A;     return cl; }  VAL idris_b16S64(VM *vm, VAL a) {+    uint16_t A = a->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = (uint64_t) (int64_t) (int16_t) a->info.bits16;+    cl->info.bits64 = (uint64_t) (int64_t) (int16_t) A;     return cl; }  VAL idris_b16T8(VM *vm, VAL a) {+    uint16_t A = a->info.bits16;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = (uint8_t) a->info.bits16;+    cl->info.bits8 = (uint8_t) A;     return cl; }  VAL idris_b32Z64(VM *vm, VAL a) {+    uint32_t A = a->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = (uint64_t) a->info.bits32;+    cl->info.bits64 = (uint64_t) A;     return cl; }  VAL idris_b32S64(VM *vm, VAL a) {+    uint32_t A = a->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS64);-    cl->info.bits64 = (uint64_t) (int64_t) (int32_t) a->info.bits32;+    cl->info.bits64 = (uint64_t) (int64_t) (int32_t) A;     return cl; }  VAL idris_b32T8(VM *vm, VAL a) {+    uint32_t A = a->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = (uint8_t) a->info.bits32;+    cl->info.bits8 = (uint8_t) A;     return cl; }  VAL idris_b32T16(VM *vm, VAL a) {+    uint32_t A = a->info.bits32;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = (uint16_t) a->info.bits32;+    cl->info.bits16 = (uint16_t) A;     return cl; }  VAL idris_b64T8(VM *vm, VAL a) {+    uint64_t A = a->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS8);-    cl->info.bits8 = (uint8_t) a->info.bits64;+    cl->info.bits8 = (uint8_t) A;     return cl; }  VAL idris_b64T16(VM *vm, VAL a) {+    uint64_t A = a->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS16);-    cl->info.bits16 = (uint16_t) a->info.bits64;+    cl->info.bits16 = (uint16_t) A;     return cl; }  VAL idris_b64T32(VM *vm, VAL a) {+    uint64_t A = a->info.bits64;     VAL cl = allocate(vm, sizeof(Closure), 0);     SETTY(cl, BITS32);-    cl->info.bits32 = (uint32_t) a->info.bits64;+    cl->info.bits32 = (uint32_t) A;     return cl; } 

@@ -151,7 +151,9 @@     printf("Final heap use          %d\n", (int)(vm->heap.next - vm->heap.heap));     if (doGC) { idris_gc(vm); }     printf("Final heap use after GC %d\n", (int)(vm->heap.next - vm->heap.heap));-+#ifdef IDRIS_ENABLE_STATS     printf("Total allocations       %d\n", vm->stats.allocations);+#endif     printf("Number of collections   %d\n", vm->stats.collections);+ }

@@ -346,10 +346,11 @@ }  VAL idris_castIntStr(VM* vm, VAL i) {+    int x = (int) GETINT(i);     Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);     SETTY(cl, STRING);     cl -> info.str = (char*)cl + sizeof(Closure);-    sprintf(cl -> info.str, "%d", (int)(GETINT(i)));+    sprintf(cl -> info.str, "%d", x);     return cl; } 

@@ -13,6 +13,13 @@ #include "idris_heap.h" #include "idris_stats.h" +#ifndef EXIT_SUCCESS+#define EXIT_SUCCESS 0+#endif+#ifndef EXIT_FAILURE+#define EXIT_FAILURE 1+#endif+ // Closures  typedef enum {

@@ -1,10 +1,10 @@ #ifndef _IDRIS_STATS_H #define _IDRIS_STATS_H +#ifdef IDRIS_ENABLE_STATS #include <time.h>+#endif -// Should not be defined in release.-#define IDRIS_ENABLE_STATS  // TODO: measure user time, exclusive/inclusive stats typedef struct {

@@ -67,7 +67,8 @@              let gcc = comp ++ " " ++                        gccDbg dbg ++ " " ++                        gccFlags ++-                       " -DHAS_PTHREAD " +++                       -- # Any flags defined here which alter the RTS API must also be added to config.mk+                       " -DHAS_PTHREAD -DIDRIS_ENABLE_STATS" ++                        " -I. " ++ objs ++ " -x c " ++                        (if (exec == Executable) then "" else " -c ") ++                        " " ++ tmpn ++@@ -437,7 +438,7 @@ doOp v (LSExt (ITFixed from) (ITFixed to)) [x]     | nativeTyWidth from < nativeTyWidth to = bitCoerce v "S" from to x doOp v (LZExt ITNative (ITFixed to)) [x]-    = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, (uintptr_t)GETINT(" ++ creg x ++ ")"+    = v ++ "idris_b" ++ show (nativeTyWidth to) ++ "const(vm, (uintptr_t)GETINT(" ++ creg x ++ "))" doOp v (LZExt ITChar (ITFixed to)) [x]     = doOp v (LZExt ITNative (ITFixed to)) [x] doOp v (LZExt (ITFixed from) ITNative) [x]@@ -474,6 +475,7 @@ doOp v LFSqrt [x] = v ++ flUnOp "sqrt" (creg x) doOp v LFFloor [x] = v ++ flUnOp "floor" (creg x) doOp v LFCeil [x] = v ++ flUnOp "ceil" (creg x)+doOp v LFNegate [x] = v ++ "MKFLOAT(vm, -GETFLOAT(" ++ (creg x) ++ "))"  doOp v LStrHead [x] = v ++ "idris_strHead(vm, " ++ creg x ++ ")" doOp v LStrTail [x] = v ++ "idris_strTail(vm, " ++ creg x ++ ")"

@@ -25,7 +25,6 @@                                  outputType :: OutputType,                                  targetTriple :: String,                                  targetCPU :: String,-                                 optimisation :: Word,                                  includes :: [FilePath],                                  importDirs :: [FilePath],                                  compileObjs :: [String],

@@ -1,757 +0,0 @@-{-# LANGUAGE PatternGuards #-}-module IRTS.CodegenJava (codegenJava) where--import           Idris.Core.TT             hiding (mkApp)-import           IRTS.CodegenCommon-import           IRTS.Java.ASTBuilding-import           IRTS.Java.JTypes-import           IRTS.Java.Mangling-import           IRTS.Java.Pom (pomString)-import           IRTS.Lang-import           IRTS.Simplified-import           IRTS.System-import           Util.System--import           Control.Applicative       hiding (Const)-import           Control.Arrow-import           Control.Monad-import           Control.Monad.Error-import qualified Control.Monad.Trans       as T-import           Control.Monad.Trans.State-import           Data.List                 (foldl', isSuffixOf)-import qualified Data.Text                 as T-import qualified Data.Text.IO              as TIO-import qualified Data.Vector.Unboxed       as V-import           Language.Java.Parser-import           Language.Java.Pretty-import           Language.Java.Syntax      hiding (Name)-import qualified Language.Java.Syntax      as J-import           System.Directory-import           System.Exit-import           System.FilePath-import           System.IO-import           System.Process---------------------------------------------------------------------------- Main function-codegenJava :: CodeGenerator-codegenJava cg = codegenJava' [] (simpleDecls cg) (outputFile cg)-                                 (includes cg) (compileLibs cg)-                                 (outputType cg)--codegenJava' :: [(Name, SExp)] -> -- initialization of globals-                [(Name, SDecl)] -> -- decls-                FilePath -> -- output file name-                [String] -> -- headers-                [String] -> -- libs-                OutputType ->-                IO ()-codegenJava' globalInit defs out hdrs libs exec =-  withTgtDir exec out (codegenJava' exec)-  where-    codegenJava' :: OutputType -> FilePath -> IO ()-    codegenJava' Raw tgtDir = do-        srcDir <- prepareSrcDir exec tgtDir-        generateJavaFile globalInit defs hdrs srcDir out-    codegenJava' MavenProject tgtDir = do-      codegenJava' Raw tgtDir-      generatePom tgtDir out libs-    codegenJava' Object tgtDir = do-      codegenJava' MavenProject tgtDir-      invokeMvn tgtDir "compile"-      copyClassFiles tgtDir out-      cleanUpTmp tgtDir-    codegenJava' _  tgtDir = do-        codegenJava' MavenProject tgtDir-        invokeMvn tgtDir "package";-        copyJar tgtDir out-        makeJarExecutable out-        cleanUpTmp tgtDir---------------------------------------------------------------------------- Compiler IO--withTgtDir :: OutputType -> FilePath -> (FilePath -> IO ()) -> IO ()-withTgtDir Raw out action = action (dropFileName out)-withTgtDir MavenProject out action = createDirectoryIfMissing False out >> action out-withTgtDir _ out action = withTempdir (takeBaseName out) action--prepareSrcDir :: OutputType -> FilePath -> IO FilePath-prepareSrcDir Raw tgtDir = return tgtDir-prepareSrcDir _ tgtDir = do-  let srcDir = (tgtDir </> "src" </> "main" </> "java")-  createDirectoryIfMissing True srcDir-  return srcDir--javaFileName :: FilePath -> FilePath -> FilePath-javaFileName srcDir out =-  either error (\ (Ident clsName) -> srcDir </> clsName <.> "java") (mkClassName out)--generateJavaFile :: [(Name, SExp)] -> -- initialization of globals-                    [(Name, SDecl)] -> -- definitions-                    [String] -> -- headers-                    FilePath -> -- Source dir-                    FilePath -> -- output target-                    IO ()-generateJavaFile globalInit defs hdrs srcDir out = do-    let code = either error-                      (prettyPrint)-- flatIndent . prettyPrint)-                      (evalStateT (mkCompilationUnit globalInit defs hdrs out) mkCodeGenEnv)-    writeFile (javaFileName srcDir out) code--pomFileName :: FilePath -> FilePath-pomFileName tgtDir = tgtDir </> "pom.xml"--generatePom :: FilePath -> -- tgt dir-               FilePath -> -- output target-               [String] -> -- libs-               IO ()-generatePom tgtDir out libs = writeFile (pomFileName tgtDir) execPom-  where-    (Ident clsName) = either error id (mkClassName out)-    execPom = pomString clsName (takeBaseName out) libs-  --invokeMvn :: FilePath -> String -> IO ()-invokeMvn tgtDir command = do-   mvnCmd <- getMvn-   let args = ["-f", pomFileName tgtDir]-   (exit, mvout, err) <- readProcessWithExitCode mvnCmd (args ++ [command]) ""-   when (exit /= ExitSuccess) $-     error ("FAILURE: " ++ mvnCmd ++ " " ++ command ++ "\n" ++ err ++ mvout)--classFileDir :: FilePath -> FilePath-classFileDir tgtDir = tgtDir </> "target" </> "classes"--copyClassFiles :: FilePath -> FilePath -> IO ()-copyClassFiles tgtDir out = do-  classFiles <- map (\ clsFile -> classFileDir tgtDir </> clsFile)-                . filter ((".class" ==) . takeExtension)-                <$> getDirectoryContents (classFileDir tgtDir)-  mapM_ (\ clsFile -> copyFile clsFile (takeDirectory out </> takeFileName clsFile)) classFiles--jarFileName :: FilePath -> FilePath -> FilePath-jarFileName tgtDir out = tgtDir </> "target" </> (takeBaseName out) <.> "jar"--copyJar :: FilePath -> FilePath -> IO ()-copyJar tgtDir out =-  copyFile (jarFileName tgtDir out) out--makeJarExecutable :: FilePath -> IO ()-makeJarExecutable out = do-  handle <- openBinaryFile out ReadMode-  contents <- TIO.hGetContents handle-  hClose handle-  handle <- openBinaryFile out WriteMode-  TIO.hPutStr handle (T.append (T.pack jarHeader) contents)-  hFlush handle-  hClose handle-  perms <- getPermissions out-  setPermissions out (setOwnerExecutable True perms)--removePom :: FilePath -> IO ()-removePom tgtDir = removeFile (pomFileName tgtDir)--cleanUpTmp :: FilePath -> IO ()-cleanUpTmp tgtDir = do-  invokeMvn tgtDir "clean"-  removePom tgtDir---------------------------------------------------------------------------- Jar and Pom infrastructure--jarHeader :: String-jarHeader =-  "#!/usr/bin/env sh\n"-  ++ "MYSELF=`which \"$0\" 2>/dev/null`\n"-  ++ "[ $? -gt 0 -a -f \"$0\" ] && MYSELF=\"./$0\"\n"-  ++ "java=java\n"-  ++ "if test -n \"$JAVA_HOME\"; then\n"-  ++ "  java=\"$JAVA_HOME/bin/java\"\n"-  ++ "fi\n"-  ++ "exec \"$java\" $java_args -jar $MYSELF \"$@\"\n"-  ++ "exit 1\n"---------------------------------------------------------------------------- Code generation environment--data CodeGenerationEnv-  = CodeGenerationEnv-  { globalVariables :: [(Name, ArrayIndex)]-  , localVariables  :: [[(Int, Ident)]]-  , localVarCounter :: Int-  }--type CodeGeneration = StateT (CodeGenerationEnv) (Either String)--mkCodeGenEnv :: CodeGenerationEnv-mkCodeGenEnv = CodeGenerationEnv [] [] 0--varPos :: LVar -> CodeGeneration (Either ArrayIndex Ident)-varPos (Loc i) = do-  vars <- (concat . localVariables) <$> get-  case lookup i vars of-    (Just varName) -> return (Right varName)-    Nothing -> throwError $ "Invalid local variable id: " ++ show i-varPos (Glob name) = do-  vars <- globalVariables <$> get-  case lookup name vars of-    (Just varIdx) -> return (Left varIdx)-    Nothing -> throwError $ "Invalid global variable id: " ++ show name--pushScope :: CodeGeneration ()-pushScope =-  modify (\ env -> env { localVariables = []:(localVariables env) })--popScope :: CodeGeneration ()-popScope = do-  env <- get-  let lVars = tail $ localVariables env-  let vC = if null lVars then 0 else localVarCounter env-  put $ env { localVariables = tail (localVariables env)-            , localVarCounter = vC }--setVariable :: LVar -> CodeGeneration (Either ArrayIndex Ident)-setVariable (Loc i) = do-  env <- get-  let lVars = localVariables env-  let getter = localVar $ localVarCounter env-  let lVars' = ((i, getter) : head lVars) : tail lVars-  put $ env { localVariables = lVars'-            , localVarCounter = 1 + localVarCounter env}-  return (Right getter)-setVariable (Glob n) = do-  env <- get-  let gVars = globalVariables env-  let getter = globalContext @! length gVars-  let gVars' = (n, getter):gVars-  put (env { globalVariables = gVars' })-  return (Left getter)--pushParams :: [Ident] -> CodeGeneration ()-pushParams paramNames =-  let varMap = zipWith (flip (,)) paramNames [0..] in-  modify (\ env -> env { localVariables = varMap:(localVariables env)-                       , localVarCounter = (length varMap) + (localVarCounter env) })--flatIndent :: String -> String-flatIndent (' ' : ' ' : xs) = flatIndent xs-flatIndent (x:xs) = x:flatIndent xs-flatIndent [] = []---------------------------------------------------------------------------- Maintaining control structures over code blocks--data BlockPostprocessor-  = BlockPostprocessor-  { ppInnerBlock :: [BlockStmt] -> Exp -> CodeGeneration [BlockStmt]-  , ppOuterBlock :: [BlockStmt] -> CodeGeneration [BlockStmt]-  }--ppExp :: BlockPostprocessor -> Exp -> CodeGeneration [BlockStmt]-ppExp pp exp = ((ppInnerBlock pp) [] exp) >>= ppOuterBlock pp--addReturn :: BlockPostprocessor-addReturn =-  BlockPostprocessor-  { ppInnerBlock = (\ block exp -> return $ block ++ [jReturn exp])-  , ppOuterBlock = return-  }--ignoreResult :: BlockPostprocessor-ignoreResult =-  BlockPostprocessor-  { ppInnerBlock = (\ block exp -> return block)-  , ppOuterBlock = return-  }--ignoreOuter :: BlockPostprocessor -> BlockPostprocessor-ignoreOuter pp = pp { ppOuterBlock = return }--throwRuntimeException :: BlockPostprocessor -> BlockPostprocessor-throwRuntimeException pp =-  pp-  { ppInnerBlock =-       (\ blk exp -> return $-         blk ++ [ BlockStmt $ Throw-                    ( InstanceCreation-                      []-                      (toClassType runtimeExceptionType)-                      [exp]-                      Nothing-                    )-                ]-       )-  }---rethrowAsRuntimeException :: BlockPostprocessor -> BlockPostprocessor-rethrowAsRuntimeException pp =-  pp-  { ppOuterBlock =-      (\ blk -> do-          ex <- ppInnerBlock (throwRuntimeException pp) [] (ExpName $ J.Name [Ident "ex"])-          ppOuterBlock pp-            $ [ BlockStmt $ Try-                  (Block blk)-                  [Catch (FormalParam [] exceptionType False (VarId (Ident "ex"))) $-                    Block ex-                  ]-                  Nothing-              ]-      )-  }---------------------------------------------------------------------------- File structure--mkCompilationUnit :: [(Name, SExp)] -> [(Name, SDecl)] -> [String] -> FilePath -> CodeGeneration CompilationUnit-mkCompilationUnit globalInit defs hdrs out = do-  clsName <- mkClassName out-  CompilationUnit Nothing ( [ ImportDecl False idrisRts True-                            , ImportDecl True idrisPrelude True-                            , ImportDecl False bigInteger False-                            , ImportDecl False runtimeException False-                            , ImportDecl False byteBuffer False-                            ] ++ otherHdrs-                          )-                          <$> mkTypeDecl clsName globalInit defs-  where-    idrisRts = J.Name $ map Ident ["org", "idris", "rts"]-    idrisPrelude = J.Name $ map Ident ["org", "idris", "rts", "Prelude"]-    bigInteger = J.Name $ map Ident ["java", "math", "BigInteger"]-    runtimeException = J.Name $ map Ident ["java", "lang", "RuntimeException"]-    byteBuffer = J.Name $ map Ident ["java", "nio", "ByteBuffer"]-    otherHdrs = map ( (\ name -> ImportDecl False name False)-                      . J.Name-                      . map (Ident . T.unpack)-                      . T.splitOn (T.pack ".")-                      . T.pack)-                $ filter (not . isSuffixOf ".h") hdrs---------------------------------------------------------------------------- Main class--mkTypeDecl :: Ident -> [(Name, SExp)] -> [(Name, SDecl)] -> CodeGeneration [TypeDecl]-mkTypeDecl name globalInit defs =-  (\ body -> [ClassTypeDecl $ ClassDecl [ Public-                                        ,  Annotation $ SingleElementAnnotation-                                           (jName "SuppressWarnings")-                                           (EVVal . InitExp $ jString "unchecked")-                                        ]-              name-              []-              Nothing-              []-              body])-  <$> mkClassBody globalInit (map (second (prefixCallNamespaces name)) defs)--mkClassBody :: [(Name, SExp)] -> [(Name, SDecl)] -> CodeGeneration ClassBody-mkClassBody globalInit defs =-  (\ globals defs -> ClassBody . (globals++) . addMainMethod . mergeInnerClasses $ defs)-  <$> mkGlobalContext globalInit-  <*> mapM mkDecl defs--mkGlobalContext :: [(Name, SExp)] -> CodeGeneration [Decl]-mkGlobalContext [] = return []-mkGlobalContext initExps = do-  pushScope-  varInit <--    mapM (\ (name, exp) -> do-           pos <- setVariable (Glob name)-           mkUpdate ignoreResult (Glob name) exp-         ) initExps-  popScope-  return [ MemberDecl $ FieldDecl [Private, Static, Final]-                                      (array objectType)-                                      [ VarDecl (VarId $ globalContextID). Just . InitExp-                                        $ ArrayCreate objectType [jInt $ length initExps] 0-                                      ]-         , InitDecl True (Block $ concat varInit)-         ]--addMainMethod :: [Decl] -> [Decl]-addMainMethod decls-  | findMainMethod decls = mkMainMethod : decls-  | otherwise = decls-  where-    findMainMethod ((MemberDecl (MethodDecl _ _ _ name [] _ _)):_)-      | name == mangle' (sMN 0 "runMain") = True-    findMainMethod (_:decls) = findMainMethod decls-    findMainMethod [] = False--mkMainMethod :: Decl-mkMainMethod =-  simpleMethod-    [Public, Static]-    Nothing-    "main"-    [FormalParam [] (array stringType) False (VarId $ Ident "args")]-    $ Block [ BlockStmt . ExpStmt-              $ call "idris_initArgs" [ jConst "args" ]-            , BlockStmt . ExpStmt $ call (mangle' (sMN 0 "runMain")) []-            ]---------------------------------------------------------------------------- Inner classes (idris namespaces)--mergeInnerClasses :: [Decl] -> [Decl]-mergeInnerClasses = foldl' mergeInner []-  where-    mergeInner ((decl@(MemberDecl (MemberClassDecl (ClassDecl priv name targs ext imp (ClassBody body))))):decls)-               decl'@(MemberDecl (MemberClassDecl (ClassDecl _ name' _ ext' imp' (ClassBody body'))))-      | name == name' =-        (MemberDecl $ MemberClassDecl $-                    ClassDecl priv-                              name-                              targs-                              (mplus ext ext')-                              (imp ++ imp')-                              (ClassBody $ mergeInnerClasses (body ++ body')))-        : decls-      | otherwise = decl:(mergeInner decls decl')-    mergeInner (decl:decls) decl' = decl:(mergeInner decls decl')-    mergeInner [] decl' = [decl']----mkDecl :: (Name, SDecl) -> CodeGeneration Decl-mkDecl ((NS n (ns:nss)), decl) =-  (\ name body ->-    MemberDecl $ MemberClassDecl $ ClassDecl [Public, Static] name [] Nothing [] body)-  <$> mangle (UN ns)-  <*> mkClassBody [] [(NS n nss, decl)]-mkDecl (_, SFun name params stackSize body) = do-  (Ident methodName) <- mangle name-  methodParams <- mapM mkFormalParam params-  paramNames <- mapM mangle params-  pushParams paramNames-  methodBody <- mkExp addReturn body-  popScope-  return $-    simpleMethod [Public, Static] (Just objectType) methodName methodParams-      (Block methodBody)--mkFormalParam :: Name -> CodeGeneration FormalParam-mkFormalParam name =-  (\ name -> FormalParam [Final] objectType False (VarId name))-  <$> mangle name---------------------------------------------------------------------------- Expressions---- | Compile a simple expression and use the given continuation to postprocess--- the resulting value.-mkExp :: BlockPostprocessor -> SExp -> CodeGeneration [BlockStmt]--- Variables-mkExp pp (SV var) =-  (Nothing <>@! var) >>= ppExp pp---- Applications-mkExp pp (SApp pushTail name args) =-  mkApp pushTail name args >>= ppExp pp---- Bindings-mkExp pp (SLet    var newExp inExp) =-  mkLet pp var newExp inExp-mkExp pp (SUpdate var@(Loc i) newExp) = -- can only update locals-  mkUpdate pp var newExp-mkExp pp (SUpdate var newExp) =-  mkExp pp newExp---- Objects-mkExp pp (SCon _ conId _ args) =-  mkIdrisObject conId args >>= ppExp pp---- Case expressions-mkExp pp (SCase up var alts) = mkCase pp True var alts-mkExp pp (SChkCase var alts) = mkCase pp False var alts---- Projections-mkExp pp (SProj var i) =-  mkProjection var i >>= ppExp pp---- Constants-mkExp pp (SConst c) =-  ppExp pp $ mkConstant c---- Foreign function calls-mkExp pp (SForeign lang resTy text params) =-  mkForeign pp lang resTy text params---- Primitive functions-mkExp pp (SOp LFork [arg]) =-  (mkThread arg) >>= ppExp pp-mkExp pp (SOp LPar [arg]) =-  (Nothing <>@! arg) >>= ppExp pp-mkExp pp (SOp LRegisterPtr [ptr, i]) =-  (Nothing <>@! ptr) >>= ppExp pp-mkExp pp (SOp LNoOp args) =-  (Nothing <>@! (last args)) >>= ppExp pp-mkExp pp (SOp LNullPtr args) =-  ppExp pp $ Lit Null-mkExp pp (SOp op args) =-  (mkPrimitiveFunction op args) >>= ppExp pp---- Empty expressions-mkExp pp (SNothing) = ppExp pp $ Lit Null---- Errors-mkExp pp (SError err) = ppExp (throwRuntimeException pp) (jString err)---------------------------------------------------------------------------- Variable access--(<>@!) :: Maybe J.Type -> LVar -> CodeGeneration Exp-(<>@!) Nothing var =-  either ArrayAccess (\ n -> ExpName $ J.Name [n]) <$> varPos var-(<>@!) (Just castTo) var =-  (castTo <>) <$> (Nothing <>@! var)---------------------------------------------------------------------------- Application (wrap method calls in tail call closures)--mkApp :: Bool -> Name -> [LVar] -> CodeGeneration Exp-mkApp False name args =-  (\ methodName params ->-    (idrisClosureType ~> "unwrapTailCall") [call methodName params]-  )-  <$> mangleFull name-  <*> mapM (Nothing <>@!) args-mkApp True name args = mkMethodCallClosure name args--mkMethodCallClosure :: Name -> [LVar] -> CodeGeneration Exp-mkMethodCallClosure name args =-  (\ name args -> closure (call name args))-  <$> mangleFull name-  <*> mapM (Nothing <>@!) args---------------------------------------------------------------------------- Updates (change context array) and Let bindings (Update, execute)--mkUpdate :: BlockPostprocessor -> LVar -> SExp -> CodeGeneration [BlockStmt]-mkUpdate pp var exp =-  mkExp-    ( pp-      { ppInnerBlock =-           (\ blk rhs -> do-               pos <- setVariable var-               vExp <- Nothing <>@! var-               ppInnerBlock pp (blk ++ [pos @:= rhs]) vExp-           )-      }-    ) exp--mkLet :: BlockPostprocessor -> LVar -> SExp -> SExp -> CodeGeneration [BlockStmt]-mkLet pp var@(Loc pos) newExp inExp =-  mkUpdate (pp { ppInnerBlock =-                    (\ blk _ -> do-                        inBlk <- mkExp pp inExp-                        return (blk ++ inBlk)-                    )-               }-           ) var newExp-mkLet _ (Glob _) _ _ = T.lift $ Left "Cannot let bind to global variable"---------------------------------------------------------------------------- Object creation--mkIdrisObject :: Int -> [LVar] -> CodeGeneration Exp-mkIdrisObject conId args =-  (\ args ->-    InstanceCreation [] (toClassType idrisObjectType) ((jInt conId):args) Nothing-  )-  <$> mapM (Nothing <>@!) args---------------------------------------------------------------------------- Case expressions--mkCase :: BlockPostprocessor -> Bool -> LVar -> [SAlt] -> CodeGeneration [BlockStmt]-mkCase pp checked var cases-  | isDefaultOnlyCase cases = mkDefaultMatch pp cases-  | isConstCase cases = do-    ifte <- mkConstMatch (ignoreOuter pp) (\ pp -> mkDefaultMatch pp cases) var cases-    ppOuterBlock pp [BlockStmt ifte]-  | otherwise = do-    switchExp <- mkGetConstructorId checked var-    matchBlocks <- mkConsMatch (ignoreOuter pp) (\ pp -> mkDefaultMatch pp cases) var cases-    ppOuterBlock pp [BlockStmt $ Switch switchExp matchBlocks]--isConstCase :: [SAlt] -> Bool-isConstCase ((SConstCase _ _):_) = True-isConstCase ((SDefaultCase _):cases) = isConstCase cases-isConstCase _ = False--isDefaultOnlyCase :: [SAlt] -> Bool-isDefaultOnlyCase [SDefaultCase _] = True-isDefaultOnlyCase [] = True-isDefaultOnlyCase _ = False--mkDefaultMatch :: BlockPostprocessor -> [SAlt] -> CodeGeneration [BlockStmt]-mkDefaultMatch pp (x@(SDefaultCase branchExpression):_) =-  do pushScope-     stmt <- mkExp pp branchExpression-     popScope-     return stmt-mkDefaultMatch pp (x:xs) = mkDefaultMatch pp xs-mkDefaultMatch pp [] =-  ppExp (throwRuntimeException pp) (jString "Non-exhaustive pattern")--mkMatchConstExp :: LVar -> Const -> CodeGeneration Exp-mkMatchConstExp var c-  | isPrimitive cty =-    (\ var -> (primFnType ~> opName (LEq undefined)) [var, jc] ~==~ jInt 1)-    <$> (Just cty <>@! var)-  | isArray cty =-    (\ var -> (arraysType ~> "equals") [var, jc])-    <$> (Just cty <>@! var)-  | isString cty =-    (\ var -> ((primFnType ~> opName (LStrEq)) [var, jc] ~==~ jInt 1))-    <$> (Just cty <>@! var)-  | otherwise =-    (\ var -> (var ~> "equals") [jc])-    <$> (Just cty <>@! var)-  where-    cty = constType c-    jc = mkConstant c--mkConstMatch :: BlockPostprocessor ->-                (BlockPostprocessor -> CodeGeneration [BlockStmt]) ->-                LVar ->-                [SAlt] ->-                CodeGeneration Stmt-mkConstMatch pp getDefaultStmts var ((SConstCase constant branchExpression):cases) = do-  matchExp <- mkMatchConstExp var constant-  pushScope-  branchBlock <- mkExp pp branchExpression-  popScope-  otherBranches <- mkConstMatch pp getDefaultStmts var cases-  return-    $ IfThenElse matchExp (StmtBlock $ Block branchBlock) otherBranches-mkConstMatch pp getDefaultStmts var (c:cases) = mkConstMatch pp getDefaultStmts var cases-mkConstMatch pp getDefaultStmts _ [] = do-  defaultBlock <- getDefaultStmts pp-  return $ StmtBlock (Block defaultBlock)--mkGetConstructorId :: Bool -> LVar -> CodeGeneration Exp-mkGetConstructorId True var =-  (\ var -> ((idrisObjectType <> var) ~> "getConstructorId") [])-  <$> (Nothing <>@! var)-mkGetConstructorId False var =-  (\ var match ->-    Cond (InstanceOf var (toRefType idrisObjectType)) match (jInt (-1))-  )-  <$> (Nothing <>@! var)-  <*> mkGetConstructorId True var--mkConsMatch :: BlockPostprocessor ->-               (BlockPostprocessor -> CodeGeneration [BlockStmt]) ->-               LVar ->-               [SAlt] ->-               CodeGeneration [SwitchBlock]-mkConsMatch pp getDefaultStmts var ((SConCase parentStackPos consIndex _ params branchExpression):cases) = do-  pushScope-  caseBranch <- mkCaseBinding pp var parentStackPos params branchExpression-  popScope-  otherBranches <- mkConsMatch pp getDefaultStmts var cases-  return $-    (SwitchBlock (SwitchCase $ jInt consIndex) caseBranch):otherBranches-mkConsMatch pp getDefaultStmts var (c:cases)  = mkConsMatch pp getDefaultStmts var cases-mkConsMatch pp getDefaultStmts _ [] = do-  defaultBlock <- getDefaultStmts pp-  return $-    [SwitchBlock Default defaultBlock]--mkCaseBinding :: BlockPostprocessor -> LVar -> Int -> [Name] -> SExp -> CodeGeneration [BlockStmt]-mkCaseBinding pp var stackStart params branchExpression =-  mkExp pp (toLetIn var stackStart params branchExpression)-  where-    toLetIn :: LVar -> Int -> [Name] -> SExp -> SExp-    toLetIn var stackStart members start =-      foldr-        (\ pos inExp -> SLet (Loc (stackStart + pos)) (SProj var pos) inExp)-        start-        [0.. (length members - 1)]---------------------------------------------------------------------------- Projection (retrieve the n-th field of an object)--mkProjection :: LVar -> Int -> CodeGeneration Exp-mkProjection var memberNr =-  (\ var -> ArrayAccess $ ((var ~> "getData") []) @! memberNr)-  <$> (Just idrisObjectType <>@! var)---------------------------------------------------------------------------- Constants--mkConstantArray :: (V.Unbox a) => J.Type -> (a -> Const) -> V.Vector a -> Exp-mkConstantArray cty elemToConst elems =-  ArrayCreateInit-    cty-    0-    (ArrayInit . map (InitExp . mkConstant . elemToConst) $ V.toList elems)--mkConstant :: Const -> Exp-mkConstant c@(I        x) = constType c <> (Lit . Word $ toInteger x)-mkConstant c@(BI       x) = bigInteger (show x)-mkConstant c@(Fl       x) = constType c <> (Lit . Double $ x)-mkConstant c@(Ch       x) = constType c <> (Lit . Char $ x)-mkConstant c@(Str      x) = constType c <> (Lit . String $ x)-mkConstant c@(B8       x) = constType c <> (Lit . Word $ toInteger x)-mkConstant c@(B16      x) = constType c <> (Lit . Word $ toInteger x)-mkConstant c@(B32      x) = constType c <> (Lit . Word $ toInteger x)-mkConstant c@(B64      x) = (bigInteger (show c) ~> "longValue") []-mkConstant c@(B8V      x) = mkConstantArray (constType c) B8  x-mkConstant c@(B16V     x) = mkConstantArray (constType c) B16 x-mkConstant c@(B32V     x) = mkConstantArray (constType c) B32 x-mkConstant c@(B64V     x) = mkConstantArray (constType c) B64 x-mkConstant c@(AType    x) = ClassLit (Just $ box (constType c))-mkConstant c@(StrType   ) = ClassLit (Just $ stringType)-mkConstant c@(PtrType   ) = ClassLit (Just $ objectType)-mkConstant c@(ManagedPtrType) = ClassLit (Just $ objectType)-mkConstant c@(BufferType) = ClassLit (Just $ bufferType)-mkConstant c@(VoidType  ) = ClassLit (Just $ voidType)-mkConstant c@(Forgot    ) = ClassLit (Just $ objectType)---------------------------------------------------------------------------- Foreign function calls--mkForeign :: BlockPostprocessor -> FLang -> FType -> String -> [(FType, LVar)] -> CodeGeneration [BlockStmt]-mkForeign pp (LANG_C) resTy text params = mkForeign pp (LANG_JAVA FStatic) resTy text params-mkForeign pp (LANG_JAVA callType) resTy text params-  | callType <- FStatic      = do-    method <- liftParsed (parser name text)-    args <- foreignVarAccess params-    wrapReturn resTy (call method args)-  | callType <- FObject      = do-    method <- liftParsed (parser ident text)-    (tgt:args) <- foreignVarAccess params-    wrapReturn resTy ((tgt ~> (show $ pretty method)) args)-  | callType <- FConstructor = do-    clsTy <- liftParsed (parser classType text)-    args <- foreignVarAccess params-    wrapReturn resTy (InstanceCreation [] clsTy args Nothing)-  where-    foreignVarAccess args =-      mapM (\ (fty, var) -> (foreignType fty <>@! var)) args--    pp' = rethrowAsRuntimeException pp--    wrapReturn FUnit exp =-      ((ppInnerBlock pp') [BlockStmt $ ExpStmt exp] (Lit Null)) >>= ppOuterBlock pp'-    wrapReturn _     exp =-      ((ppInnerBlock pp') [] exp) >>= ppOuterBlock pp'---------------------------------------------------------------------------- Primitive functions--mkPrimitiveFunction :: PrimFn -> [LVar] -> CodeGeneration Exp-mkPrimitiveFunction op args =-  (\ args -> (primFnType ~> opName op) (endiannessArguments op ++ args))-  <$> sequence (zipWith (\ a t -> (Just t) <>@! a) args (sourceTypes op))--mkThread :: LVar -> CodeGeneration Exp-mkThread arg =-  (\ closure -> (closure ~> "fork") []) <$> mkMethodCallClosure (sMN 0 "EVAL") [arg]--

@@ -1213,6 +1213,8 @@       , (arg:_)                 <- args = jsCall "parseFloat" [translateReg arg]       | (LIntFloat ITNative)    <- op       , (arg:_)                 <- args = translateReg arg+      | (LIntFloat ITBig)       <- op+      , (arg:_)                 <- args = jsMeth (translateReg arg) "intValue" []       | (LFloatInt ITNative)    <- op       , (arg:_)                 <- args = translateReg arg       | (LChInt ITNative)       <- op@@ -1242,6 +1244,8 @@       , (arg:_)     <- args = jsCall "Math.floor" [translateReg arg]       | LFCeil      <- op       , (arg:_)     <- args = jsCall "Math.ceil" [translateReg arg]+      | LFNegate    <- op+      , (arg:_)     <- args = JSPreOp "-" (translateReg arg)        | LStrCons    <- op       , (lhs:rhs:_) <- args = invokeMeth lhs "concat" [rhs]

@@ -1,1320 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-module IRTS.CodegenLLVM (codegenLLVM) where--import IRTS.CodegenCommon-import IRTS.Lang-import IRTS.Simplified-import IRTS.System-import qualified Idris.Core.TT as TT-import Idris.Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)--import Util.System--import LLVM.General.Context-import LLVM.General.Diagnostic-import LLVM.General.AST-import LLVM.General.AST.AddrSpace-import LLVM.General.Target ( TargetMachine-                           , withTargetOptions, withTargetMachine, getTargetMachineDataLayout-                           , initializeAllTargets, lookupTarget-                           )-import LLVM.General.AST.DataLayout-import qualified LLVM.General.PassManager as PM-import qualified LLVM.General.Module as MO-import qualified LLVM.General.AST.IntegerPredicate as IPred-import qualified LLVM.General.AST.FloatingPointPredicate as FPred-import qualified LLVM.General.AST.Linkage as L-import qualified LLVM.General.AST.Visibility as V-import qualified LLVM.General.AST.CallingConvention as CC-import qualified LLVM.General.AST.Attribute as A-import qualified LLVM.General.AST.Global as G-import qualified LLVM.General.AST.Constant as C-import qualified LLVM.General.AST.Float as F-import qualified LLVM.General.Relocation as R-import qualified LLVM.General.CodeModel as CM-import qualified LLVM.General.CodeGenOpt as CGO--import Data.List-import Data.Maybe-import Data.Word-import Data.Map (Map)-import qualified Data.Map as M-import qualified Data.Set as S-import qualified Data.Vector.Unboxed as V-import Control.Applicative-import Control.Monad.RWS-import Control.Monad.Writer-import Control.Monad.State-import Control.Monad.Error--import qualified System.Info as SI (arch, os)-import System.IO-import System.Directory (removeFile)-import System.FilePath ((</>))-import System.Process (rawSystem)-import System.Exit (ExitCode(..))-import Debug.Trace--data Target = Target { triple :: String, dataLayout :: DataLayout }--codegenLLVM :: CodeGenerator-codegenLLVM ci = codegenLLVM' (simpleDecls ci) (targetTriple ci)-                              (targetCPU ci) (optimisation ci)-                              (outputFile ci) (outputType ci)--codegenLLVM' :: [(TT.Name, SDecl)] ->-                String -> -- target triple-                String -> -- target CPU-                Word -> -- Optimization degree-                FilePath -> -- output file name-                OutputType ->-                IO ()-codegenLLVM' defs triple cpu optimize file outty = withContext $ \context -> do-  initializeAllTargets-  (target, _) <- failInIO $ lookupTarget Nothing triple-  withTargetOptions $ \options ->-      withTargetMachine target triple cpu S.empty options R.Default CM.Default CGO.Default $ \tm ->-          do layout <- getTargetMachineDataLayout tm-             let ast = codegen (Target triple layout) (map snd defs)-             result <- runErrorT .  MO.withModuleFromAST context ast $ \m ->-                       do let opts = PM.defaultCuratedPassSetSpec-                                     { PM.optLevel = Just optimize-                                     , PM.simplifyLibCalls = Just True-                                     , PM.useInlinerWithThreshold = Just 225-                                     }-                          when (optimize /= 0) $ PM.withPassManager opts $ void . flip PM.runPassManager m-                          outputModule tm file outty m-             case result of-               Right _ -> return ()-               Left msg -> ierror msg--failInIO :: ErrorT String IO a -> IO a-failInIO = either fail return <=< runErrorT--outputModule :: TargetMachine -> FilePath -> OutputType -> MO.Module -> IO ()-outputModule _  file Raw    m = failInIO $ MO.writeBitcodeToFile file m-outputModule tm file Object m = failInIO $ MO.writeObjectToFile tm file m-outputModule tm file Executable m = withTmpFile $ \obj -> do-  outputModule tm obj Object m-  cc <- getCC-  defs <- (</> "llvm" </> "libidris_rts.a") <$> getDataDir-  exit <- rawSystem cc [obj, defs, "-lm", "-lgmp", "-lgc", "-o", file]-  when (exit /= ExitSuccess) $ ierror "FAILURE: Linking"-outputModule _ _ MavenProject _ = ierror "FAILURE: unsupported output type"--withTmpFile :: (FilePath -> IO a) -> IO a-withTmpFile f = do-  (path, handle) <- tempfile-  hClose handle-  result <- f path-  removeFile path-  return result--ierror :: String -> a-ierror msg = error $ "INTERNAL ERROR: IRTS.CodegenLLVM: " ++ msg--mainDef :: Global-mainDef =-    functionDefaults-    { G.returnType = IntegerType 32-    , G.parameters =-        ([ Parameter (IntegerType 32) (Name "argc") []-         , Parameter (PointerType (PointerType (IntegerType 8) (AddrSpace 0)) (AddrSpace 0)) (Name "argv") []-         ], False)-    , G.name = Name "main"-    , G.basicBlocks =-        [ BasicBlock (UnName 0)-          [ Do $ simpleCall "GC_init" [] -- Initialize Boehm GC-          , Do $ simpleCall "__gmp_set_memory_functions"-                     [ ConstantOperand . C.GlobalReference . Name $ "__idris_gmpMalloc"-                     , ConstantOperand . C.GlobalReference . Name $ "__idris_gmpRealloc"-                     , ConstantOperand . C.GlobalReference . Name $ "__idris_gmpFree"-                     ]-          , Do $ Store False (ConstantOperand . C.GlobalReference . Name $ "__idris_argc") -                       (LocalReference (Name "argc")) Nothing 0 []-          , Do $ Store False (ConstantOperand . C.GlobalReference . Name $ "__idris_argv") -                       (LocalReference (Name "argv")) Nothing 0 []-          , UnName 1 := idrCall "{runMain0}" [] ]-          (Do $ Ret (Just (ConstantOperand (C.Int 32 0))) [])-        ]}--initDefs :: Target -> [Definition]-initDefs tgt =-    [ TypeDefinition (Name "valTy")-      (Just $ StructureType False-                [ IntegerType 32-                , ArrayType 0 (PointerType valueType (AddrSpace 0))-                ])-    , TypeDefinition (Name "mpz")-        (Just $ StructureType False-                  [ IntegerType 32-                  , IntegerType 32-                  , PointerType intPtr (AddrSpace 0)-                  ])-    , GlobalDefinition $ globalVariableDefaults-      { G.name = Name "__idris_intFmtStr"-      , G.linkage = L.Internal-      , G.isConstant = True-      , G.hasUnnamedAddr = True-      , G.type' = ArrayType 5 (IntegerType 8)-      , G.initializer = Just $ C.Array (IntegerType 8) (map (C.Int 8 . fromIntegral . fromEnum) "%lld" ++ [C.Int 8 0])-      }-    , rtsFun "intStr" ptrI8 [IntegerType 64]-        [ BasicBlock (UnName 0)-          [ UnName 1 := simpleCall "GC_malloc_atomic" [ConstantOperand (C.Int (tgtWordSize tgt) 21)]-          , UnName 2 := simpleCall "snprintf"-                       [ LocalReference (UnName 1)-                       , ConstantOperand (C.Int (tgtWordSize tgt) 21)-                       , ConstantOperand $ C.GetElementPtr True (C.GlobalReference . Name $ "__idris_intFmtStr") [C.Int 32 0, C.Int 32 0]-                       , LocalReference (UnName 0)-                       ]-          ]-          (Do $ Ret (Just (LocalReference (UnName 1))) [])-        ]-    , GlobalDefinition $ globalVariableDefaults-      { G.name = Name "__idris_floatFmtStr"-      , G.linkage = L.Internal-      , G.isConstant = True-      , G.hasUnnamedAddr = True-      , G.type' = ArrayType 5 (IntegerType 8)-      , G.initializer = Just $ C.Array (IntegerType 8) (map (C.Int 8 . fromIntegral . fromEnum) "%g" ++ [C.Int 8 0])-      }-    , rtsFun "floatStr" ptrI8 [FloatingPointType 64 IEEE]-        [ BasicBlock (UnName 0)-          [ UnName 1 := simpleCall "GC_malloc_atomic" [ConstantOperand (C.Int (tgtWordSize tgt) 21)]-          , UnName 2 := simpleCall "snprintf"-                       [ LocalReference (UnName 1)-                       , ConstantOperand (C.Int (tgtWordSize tgt) 21)-                       , ConstantOperand $ C.GetElementPtr True (C.GlobalReference . Name $ "__idris_floatFmtStr") [C.Int 32 0, C.Int 32 0]-                       , LocalReference (UnName 0)-                       ]-          ]-          (Do $ Ret (Just (LocalReference (UnName 1))) [])-        ]-    , exfun "llvm.sin.f64" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.cos.f64" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.pow.f64"  (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.ceil.f64" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.floor.f64" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.exp.f64" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.log.f64" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.sqrt.f64" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "tan" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "asin" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "acos" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "atan" (FloatingPointType 64 IEEE) [ FloatingPointType 64 IEEE ] False-    , exfun "llvm.trap" VoidType [] False-    -- , exfun "llvm.llvm.memcpy.p0i8.p0i8.i32" VoidType [ptrI8, ptrI8, IntegerType 32, IntegerType 32, IntegerType 1] False-    -- , exfun "llvm.llvm.memcpy.p0i8.p0i8.i64" VoidType [ptrI8, ptrI8, IntegerType 64, IntegerType 32, IntegerType 1] False-    , exfun "memcpy" ptrI8 [ptrI8, ptrI8, intPtr] False-    , exfun "llvm.invariant.start" (PointerType (StructureType False []) (AddrSpace 0)) [IntegerType 64, ptrI8] False-    , exfun "snprintf" (IntegerType 32) [ptrI8, intPtr, ptrI8] True-    , exfun "strcmp" (IntegerType 32) [ptrI8, ptrI8] False-    , exfun "strlen" intPtr [ptrI8] False-    , exfun "GC_init" VoidType [] False-    , exfun "GC_malloc" ptrI8 [intPtr] False-    , exfun "GC_malloc_atomic" ptrI8 [intPtr] False-    , exfun "__gmp_set_memory_functions" VoidType-                [ PointerType (FunctionType ptrI8 [intPtr] False) (AddrSpace 0)-                , PointerType (FunctionType ptrI8 [ptrI8, intPtr, intPtr] False) (AddrSpace 0)-                , PointerType (FunctionType VoidType [ptrI8, intPtr] False) (AddrSpace 0)-                ] False-    , exfun "__gmpz_init" VoidType [pmpz] False-    , exfun "__gmpz_init_set_str" (IntegerType 32) [pmpz, ptrI8, IntegerType 32] False-    , exfun "__gmpz_get_str" ptrI8 [ptrI8, IntegerType 32, pmpz] False-    , exfun "__gmpz_get_ui" intPtr [pmpz] False-    , exfun "__gmpz_cmp" (IntegerType 32) [pmpz, pmpz] False-    , exfun "__gmpz_fdiv_q_2exp" VoidType [pmpz, pmpz, intPtr] False-    , exfun "__gmpz_mul_2exp" VoidType [pmpz, pmpz, intPtr] False-    , exfun "__gmpz_get_d" (FloatingPointType 64 IEEE) [pmpz] False-    , exfun "__gmpz_set_d" VoidType [pmpz, FloatingPointType 64 IEEE] False-    , exfun "mpz_get_ull" (IntegerType 64) [pmpz] False-    , exfun "mpz_init_set_ull" VoidType [pmpz, IntegerType 64] False-    , exfun "mpz_init_set_sll" VoidType [pmpz, IntegerType 64] False-    , exfun "__idris_strCons" ptrI8 [IntegerType 8, ptrI8] False-    , exfun "__idris_readStr" ptrI8 [ptrI8] False -- Actually pointer to FILE, but it's opaque anyway-    , exfun "__idris_gmpMalloc" ptrI8 [intPtr] False-    , exfun "__idris_gmpRealloc" ptrI8 [ptrI8, intPtr, intPtr] False-    , exfun "__idris_gmpFree" VoidType [ptrI8, intPtr] False-    , exfun "__idris_strRev" ptrI8 [ptrI8] False-    , exfun "strtoll" (IntegerType 64) [ptrI8, PointerType ptrI8 (AddrSpace 0), IntegerType 32] False-    , exfun "putErr" VoidType [ptrI8] False-    , exVar (stdinName tgt) ptrI8-    , exVar (stdoutName tgt) ptrI8-    , exVar (stderrName tgt) ptrI8-    , exVar "__idris_argc" (IntegerType 32)-    , exVar "__idris_argv" (PointerType ptrI8 (AddrSpace 0))-    , GlobalDefinition mainDef-    ] ++ map mpzBinFun ["add", "sub", "mul", "fdiv_q", "fdiv_r", "and", "ior", "xor"]-    where-      intPtr = IntegerType (tgtWordSize tgt)-      ptrI8 = PointerType (IntegerType 8) (AddrSpace 0)-      pmpz = PointerType mpzTy (AddrSpace 0)--      mpzBinFun n = exfun ("__gmpz_" ++ n) VoidType [pmpz, pmpz, pmpz] False--      rtsFun :: String -> Type -> [Type] -> [BasicBlock] -> Definition-      rtsFun name rty argtys def =-          GlobalDefinition $ functionDefaults-                               { G.linkage = L.Internal-                               , G.returnType = rty-                               , G.parameters = (flip map argtys $ \ty -> Parameter ty (UnName 0) [], False)-                               , G.name = Name $ "__idris_" ++ name-                               , G.basicBlocks = def-                               }--      exfun :: String -> Type -> [Type] -> Bool -> Definition-      exfun name rty argtys vari =-          GlobalDefinition $ functionDefaults-                               { G.returnType = rty-                               , G.name = Name name-                               , G.parameters = (flip map argtys $ \ty -> Parameter ty (UnName 0) [], vari)-                               }-      exVar :: String -> Type -> Definition-      exVar name ty = GlobalDefinition $ globalVariableDefaults { G.name = Name name, G.type' = ty }--isApple :: Target -> Bool-isApple (Target { triple = t }) = isJust . stripPrefix "-apple" $ dropWhile (/= '-') t--stdinName, stdoutName, stderrName :: Target -> String-stdinName t | isApple t = "__stdinp"-stdinName _ = "stdin"-stdoutName t | isApple t = "__stdoutp"-stdoutName _ = "stdout"-stderrName t | isApple t = "__stderrp"-stderrName _ = "stderr"--getStdIn, getStdOut, getStdErr :: Codegen Operand-getStdIn  = ConstantOperand . C.GlobalReference . Name . stdinName <$> asks target-getStdOut = ConstantOperand . C.GlobalReference . Name . stdoutName <$> asks target-getStdErr = ConstantOperand . C.GlobalReference . Name . stderrName <$> asks target--codegen :: Target -> [SDecl] -> Module-codegen tgt defs = Module "idris" (Just . dataLayout $ tgt) (Just . triple $ tgt) (initDefs tgt ++ globals ++ gendefs)-    where-      (gendefs, _, globals) = runRWS (mapM cgDef defs) tgt initialMGS--valueType :: Type-valueType = NamedTypeReference (Name "valTy")--nullValue :: C.Constant-nullValue = C.Null (PointerType valueType (AddrSpace 0))--primTy :: Type -> Type-primTy inner = StructureType False [IntegerType 32, inner]--mpzTy :: Type-mpzTy = NamedTypeReference (Name "mpz")--conType :: Word64 -> Type-conType nargs = StructureType False-                [ IntegerType 32-                , ArrayType nargs (PointerType valueType (AddrSpace 0))-                ]--data MGS = MGS { mgsNextGlobalName :: Word-               , mgsForeignSyms :: Map String (FType, [FType])-               }--type Modgen = RWS Target [Definition] MGS--initialMGS :: MGS-initialMGS = MGS { mgsNextGlobalName = 0-                 , mgsForeignSyms = M.empty-                 }--cgDef :: SDecl -> Modgen Definition-cgDef (SFun name argNames _ expr) = do-  nextGlobal <- gets mgsNextGlobalName-  existingForeignSyms <- gets mgsForeignSyms-  tgt <- ask-  let (_, CGS { nextGlobalName = nextGlobal', foreignSyms = foreignSyms' }, (allocas, bbs, globals)) =-          runRWS (do r <- cgExpr expr-                     case r of-                       Nothing -> terminate $ Unreachable []-                       Just r' -> terminate $ Ret (Just r') [])-                 (CGR tgt (show name))-                 (CGS 0 nextGlobal (Name "begin") [] (map (Just . LocalReference . Name . show) argNames) existingForeignSyms)-      entryTerm = case bbs of-                    [] -> Do $ Ret Nothing []-                    BasicBlock n _ _:_ -> Do $ Br n []-  tell globals-  put (MGS { mgsNextGlobalName = nextGlobal', mgsForeignSyms = foreignSyms' })-  return . GlobalDefinition $ functionDefaults-             { G.linkage = L.Internal-             , G.callingConvention = CC.Fast-             , G.name = Name (show name)-             , G.returnType = PointerType valueType (AddrSpace 0)-             , G.parameters = (flip map argNames $ \argName ->-                                   Parameter (PointerType valueType (AddrSpace 0)) (Name (show argName)) []-                              , False)-             , G.basicBlocks =-                 BasicBlock (Name "entry")-                                 (map (\(n, t) -> n := Alloca t Nothing 0 []) allocas)-                                 entryTerm-                 : bbs-             }--type CGW = ([(Name, Type)], [BasicBlock], [Definition])--type Env = [Maybe Operand]--data CGS = CGS { nextName :: Word-               , nextGlobalName :: Word-               , currentBlockName :: Name-               , instAccum :: [Named Instruction]-               , lexenv :: Env-               , foreignSyms :: Map String (FType, [FType])-               }--data CGR = CGR { target :: Target-               , funcName :: String }--type Codegen = RWS CGR CGW CGS--getFuncName :: Codegen String-getFuncName = asks funcName--getGlobalUnName :: Codegen Name-getGlobalUnName = do-  i <- gets nextGlobalName-  modify $ \s -> s { nextGlobalName = 1 + i }-  return (UnName i)--getUnName :: Codegen Name-getUnName = do-  i <- gets nextName-  modify $ \s -> s { nextName = 1 + i }-  return (UnName i)--getName :: String -> Codegen Name-getName n = do-  i <- gets nextName-  modify $ \s -> s { nextName = 1 + i }-  return (Name $ n ++ show i)--alloca :: Name -> Type -> Codegen ()-alloca n t = tell ([(n, t)], [], [])--terminate :: Terminator -> Codegen ()-terminate term = do-  name <- gets currentBlockName-  insts <- gets instAccum-  modify $ \s -> s { instAccum = ierror "Not in a block"-                   , currentBlockName = ierror "Not in a block" }-  tell ([], [BasicBlock name insts (Do term)], [])--newBlock :: Name -> Codegen ()-newBlock name = modify $ \s -> s { instAccum = []-                                 , currentBlockName = name-                                 }--inst :: Instruction -> Codegen Operand-inst i = do-  n <- getUnName-  modify $ \s -> s { instAccum = instAccum s ++ [n := i] }-  return $ LocalReference n--ninst :: String -> Instruction -> Codegen Operand-ninst name i = do-  n <- getName name-  modify $ \s -> s { instAccum = instAccum s ++ [n := i] }-  return $ LocalReference n--inst' :: Instruction -> Codegen ()-inst' i = modify $ \s -> s { instAccum = instAccum s ++ [Do i] }--insts :: [Named Instruction] -> Codegen ()-insts is = modify $ \s -> s { instAccum = instAccum s ++ is }--var :: LVar -> Codegen (Maybe Operand)-var (Loc level) = (!! level) <$> gets lexenv-var (Glob n) = return . Just . ConstantOperand . C.GlobalReference . Name $ show n--binds :: Env -> Codegen (Maybe Operand) -> Codegen (Maybe Operand)-binds vals cg = do-  envLen <- length <$> gets lexenv-  modify $ \s -> s { lexenv = lexenv s ++ vals }-  value <- cg-  modify $ \s -> s { lexenv = take envLen $ lexenv s }-  return value--replaceElt :: Int -> a -> [a] -> [a]-replaceElt _ val [] = error "replaceElt: Ran out of list"-replaceElt 0 val (x:xs) = val:xs-replaceElt n val (x:xs) = x : replaceElt (n-1) val xs--alloc' :: Operand -> Codegen Operand-alloc' size = inst $ simpleCall "GC_malloc" [size]--allocAtomic' :: Operand -> Codegen Operand-allocAtomic' size = inst $ simpleCall "GC_malloc_atomic" [size]--alloc :: Type -> Codegen Operand-alloc ty = do-  size <- sizeOf ty-  mem <- alloc' size-  inst $ BitCast mem (PointerType ty (AddrSpace 0)) []--allocAtomic :: Type -> Codegen Operand-allocAtomic ty = do-  size <- sizeOf ty-  mem <- allocAtomic' size-  inst $ BitCast mem (PointerType ty (AddrSpace 0)) []--sizeOf :: Type -> Codegen Operand-sizeOf ty = ConstantOperand . C.PtrToInt-            (C.GetElementPtr True (C.Null (PointerType ty (AddrSpace 0))) [C.Int 32 1])-            . IntegerType <$> getWordSize--loadInv :: Operand -> Instruction-loadInv ptr = Load False ptr Nothing 0 [("invariant.load", MetadataNode [])]--tgtWordSize :: Target -> Word32-tgtWordSize (Target { dataLayout = DataLayout { pointerLayouts = l } }) =-    fst . fromJust $ M.lookup (AddrSpace 0) l--getWordSize :: Codegen Word32-getWordSize = tgtWordSize <$> asks target--cgExpr :: SExp -> Codegen (Maybe Operand)-cgExpr (SV v) = var v-cgExpr (SApp tailcall fname args) = do-  argSlots <- mapM var args-  case sequence argSlots of-    Nothing -> return Nothing-    Just argVals -> do-      fn <- var (Glob fname)-      Just <$> inst ((idrCall (show fname) argVals) { isTailCall = tailcall })-cgExpr (SLet _ varExpr bodyExpr) = do-  val <- cgExpr varExpr-  binds [val] $ cgExpr bodyExpr-cgExpr (SUpdate (Loc level) expr) = do-  val <- cgExpr expr-  modify $ \s -> s { lexenv = replaceElt level val (lexenv s) }-  return val-cgExpr (SUpdate x expr) = cgExpr expr-cgExpr (SCon _ tag name args) = do-  argSlots <- mapM var args-  case sequence argSlots of-    Nothing -> return Nothing-    Just argVals -> do-      let ty = conType . fromIntegral . length $ argVals-      con <- alloc ty-      tagPtr <- inst $ GetElementPtr True con [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 0)] []-      inst' $ Store False tagPtr (ConstantOperand (C.Int 32 (fromIntegral tag))) Nothing 0 []-      forM_ (zip argVals [0..]) $ \(arg, i) -> do-        ptr <- inst $ GetElementPtr True con [ ConstantOperand (C.Int 32 0)-                                             , ConstantOperand (C.Int 32 1)-                                             , ConstantOperand (C.Int 32 i)] []-        inst' $ Store False ptr arg Nothing 0 []-      ptrI8 <- inst $ BitCast con (PointerType (IntegerType 8) (AddrSpace 0)) []-      inst' $ simpleCall "llvm.invariant.start" [ConstantOperand $ C.Int 64 (-1), ptrI8]-      Just <$> inst (BitCast con (PointerType valueType (AddrSpace 0)) [])-cgExpr (SCase _ inspect alts) = do-  val <- var inspect-  case val of-    Nothing -> return Nothing-    Just v -> cgCase v alts-cgExpr (SChkCase inspect alts) = do-  mval <- var inspect-  case mval of-    Nothing -> return Nothing-    Just val ->-        do endBBN <- getName "endChkCase"-           notNullBBN <- getName "notNull"-           originBlock <- gets currentBlockName-           isNull <- inst $ ICmp IPred.EQ val (ConstantOperand nullValue) []-           terminate $ CondBr isNull endBBN notNullBBN []-           newBlock notNullBBN-           ptr <- inst $ BitCast val (PointerType (IntegerType 32) (AddrSpace 0)) []-           flag <- inst $ Load False ptr Nothing 0 []-           isVal <- inst $ ICmp IPred.EQ flag (ConstantOperand (C.Int 32 (-1))) []-           conBBN <- getName "constructor"-           terminate $ CondBr isVal endBBN conBBN []-           newBlock conBBN-           result <- cgCase val alts-           caseExitBlock <- gets currentBlockName-           case result of-             Nothing -> do-               terminate $ Unreachable []-               newBlock endBBN-               return $ Just val-             Just caseVal -> do-               terminate $ Br endBBN []-               newBlock endBBN-               Just <$> inst (Phi (PointerType valueType (AddrSpace 0))-                              [(val, originBlock), (val, notNullBBN), (caseVal, caseExitBlock)] [])-cgExpr (SProj conVar idx) = do-  val <- var conVar-  case val of-    Nothing -> return Nothing-    Just v ->-        do ptr <- inst $ GetElementPtr True v-                  [ ConstantOperand (C.Int 32 0)-                  , ConstantOperand (C.Int 32 1)-                  , ConstantOperand (C.Int 32 (fromIntegral idx))-                  ] []-           Just <$> inst (Load False ptr Nothing 0 [])-cgExpr (SConst c) = Just <$> cgConst c-cgExpr (SForeign LANG_C rty fname args) = do-  func <- ensureCDecl fname rty (map fst args)-  argVals <- forM args $ \(fty, v) -> do-               v' <- var v-               case v' of-                 Just val -> return $ Just (fty, val)-                 Nothing -> return Nothing-  case sequence argVals of-    Nothing -> return Nothing-    Just argVals' -> do-      argUVals <- mapM (uncurry unbox) argVals'-      result <- inst Call { isTailCall = False-                          , callingConvention = CC.C-                          , returnAttributes = []-                          , function = Right func-                          , arguments = map (\v -> (v, [])) argUVals-                          , functionAttributes = []-                          , metadata = []-                          }-      Just <$> box rty result-cgExpr (SOp fn args) = do-  argVals <- mapM var args-  case sequence argVals of-    Just ops -> Just <$> cgOp fn ops-    Nothing -> return Nothing-cgExpr SNothing = return . Just . ConstantOperand $ nullValue-cgExpr (SError msg) = do-  str <- addGlobal' (ArrayType (2 + fromIntegral (length msg)) (IntegerType 8))-         (cgConst' (TT.Str (msg ++ "\n")))-  inst' $ simpleCall "putErr" [ConstantOperand $ C.GetElementPtr True str [ C.Int 32 0-                                                                          , C.Int 32 0]]-  inst' Call { isTailCall = True-             , callingConvention = CC.C-             , returnAttributes = []-             , function = Right . ConstantOperand . C.GlobalReference . Name $ "llvm.trap"-             , arguments = []-             , functionAttributes = [A.NoReturn]-             , metadata = []-             }-  return Nothing--cgCase :: Operand -> [SAlt] -> Codegen (Maybe Operand)-cgCase val alts =-    case find isConstCase alts of-      Just (SConstCase (TT.BI _) _) -> cgChainCase val defExp constAlts-      Just (SConstCase (TT.Str _) _) -> cgChainCase val defExp constAlts-      Just (SConstCase _ _) -> cgPrimCase val defExp constAlts-      Nothing -> cgConCase val defExp conAlts-    where-      defExp = getDefExp =<< find isDefCase alts-      constAlts = filter isConstCase alts-      conAlts = filter isConCase alts--      isConstCase (SConstCase {}) = True-      isConstCase _ = False--      isConCase (SConCase {}) = True-      isConCase _ = False--      isDefCase (SDefaultCase _) = True-      isDefCase _ = False--      getDefExp (SDefaultCase e) = Just e-      getDefExp _ = Nothing--cgPrimCase :: Operand -> Maybe SExp -> [SAlt] -> Codegen (Maybe Operand)-cgPrimCase caseValPtr defExp alts = do-  let caseTy = case head alts of-                 SConstCase (TT.I _)   _ -> IntegerType 32-                 SConstCase (TT.B8 _)  _ -> IntegerType 8-                 SConstCase (TT.B16 _) _ -> IntegerType 16-                 SConstCase (TT.B32 _) _ -> IntegerType 32-                 SConstCase (TT.B64 _) _ -> IntegerType 64-                 SConstCase (TT.Fl _)  _ -> FloatingPointType 64 IEEE-                 SConstCase (TT.Ch _)  _ -> IntegerType 32-  realPtr <- inst $ BitCast caseValPtr (PointerType (primTy caseTy) (AddrSpace 0)) []-  valPtr <- inst $ GetElementPtr True realPtr [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 1)] []-  caseVal <- inst $ Load False valPtr Nothing 0 []-  defBlockName <- getName "default"-  exitBlockName <- getName "caseExit"-  namedAlts <- mapM (\a -> do n <- nameAlt defBlockName a; return (n, a)) alts-  terminate $ Switch caseVal defBlockName (map (\(n, SConstCase c _) -> (cgConst' c, n)) namedAlts) []-  initEnv <- gets lexenv-  defResult <- cgDefaultAlt exitBlockName defBlockName defExp-  results <- forM namedAlts $ \(name, SConstCase _ exp) -> cgAlt initEnv exitBlockName name Nothing exp-  finishCase initEnv exitBlockName (defResult:results)--cgConCase :: Operand -> Maybe SExp -> [SAlt] -> Codegen (Maybe Operand)-cgConCase con defExp alts = do-  tagPtr <- inst $ GetElementPtr True con [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 0)] []-  tag <- inst $ Load False tagPtr Nothing 0 []-  defBlockName <- getName "default"-  exitBlockName <- getName "caseExit"-  namedAlts <- mapM (\a -> do n <- nameAlt defBlockName a; return (n, a)) alts-  terminate $ Switch tag defBlockName (map (\(n, SConCase _ tag _ _ _) ->-                                                (C.Int 32 (fromIntegral tag), n)) namedAlts) []-  initEnv <- gets lexenv-  defResult <- cgDefaultAlt exitBlockName defBlockName defExp-  results <- forM namedAlts $ \(name, SConCase _ _ _ argns exp) ->-             cgAlt initEnv exitBlockName name (Just (con, map show argns)) exp-  finishCase initEnv exitBlockName (defResult:results)--cgChainCase :: Operand -> Maybe SExp -> [SAlt] -> Codegen (Maybe Operand)-cgChainCase caseValPtr defExp alts = do-  let (caseTy, comparator) =-          case head alts of-            SConstCase (TT.BI _) _ -> (FArith (ATInt ITBig), "__gmpz_cmp")-            SConstCase (TT.Str _) _ -> (FString, "strcmp")-  caseVal <- unbox caseTy caseValPtr-  defBlockName <- getName "default"-  exitBlockName <- getName "caseExit"-  namedAlts <- mapM (\a -> do n <- nameAlt defBlockName a; return (n, a)) alts-  initEnv <- gets lexenv-  results <- forM namedAlts $ \(name, SConstCase c e) ->-             do const <- unbox caseTy =<< cgConst c-                cmp <- inst $ simpleCall comparator [const, caseVal]-                cmpResult <- inst $ ICmp IPred.EQ cmp (ConstantOperand (C.Int 32 0)) []-                elseName <- getName "else"-                terminate $ CondBr cmpResult name elseName []-                result <- cgAlt initEnv exitBlockName name Nothing e-                newBlock elseName-                return result-  modify $ \s -> s { lexenv = initEnv }-  fname <- getFuncName-  defaultVal <- cgExpr (fromMaybe (SError $ "Inexhaustive case failure in " ++ fname) defExp)-  defaultBlock <- gets currentBlockName-  defaultEnv <- gets lexenv-  defResult <- case defaultVal of-                 Just v -> do-                   terminate $ Br exitBlockName []-                   return $ Just (v, defaultBlock, defaultEnv)-                 Nothing -> do-                   terminate $ Unreachable []-                   return Nothing-  finishCase initEnv exitBlockName (defResult:results)--finishCase :: Env -> Name -> [Maybe (Operand, Name, Env)] -> Codegen (Maybe Operand)-finishCase initEnv exitBlockName results = do-  let definedResults = mapMaybe id results-  case definedResults of-    [] -> do modify $ \s -> s { lexenv = initEnv }-             return Nothing-    xs -> do-      newBlock exitBlockName-      mergeEnvs $ map (\(_, altBlock, altEnv) -> (altBlock, altEnv)) xs-      Just <$> inst (Phi (PointerType valueType (AddrSpace 0))-                (map (\(altVal, altBlock, _) -> (altVal, altBlock)) xs) [])---cgDefaultAlt :: Name -> Name -> Maybe SExp -> Codegen (Maybe (Operand, Name, Env))-cgDefaultAlt exitName name exp = do-  newBlock name-  fname <- getFuncName-  val <- cgExpr (fromMaybe (SError $ "Inexhaustive case failure in " ++ fname) exp)-  env <- gets lexenv-  block <- gets currentBlockName-  case val of-    Just v ->-        do terminate $ Br exitName []-           return $ Just (v, block, env)-    Nothing ->-        do terminate $ Unreachable []-           return Nothing--cgAlt :: Env -> Name -> Name -> Maybe (Operand, [String]) -> SExp-      -> Codegen (Maybe (Operand, Name, Env))-cgAlt initEnv exitBlockName name destr exp = do-  modify $ \s -> s { lexenv = initEnv }-  newBlock name-  locals <- case destr of-              Nothing -> return []-              Just (con, argns) ->-                  forM (zip argns [0..]) $ \(argName, i) ->-                      do ptr <- inst $ GetElementPtr True con [ ConstantOperand (C.Int 32 0)-                                                              , ConstantOperand (C.Int 32 1)-                                                              , ConstantOperand (C.Int 32 i)] []-                         Just <$> ninst argName (Load False ptr Nothing 0 [])-  altVal <- binds locals $ cgExpr exp-  altEnv <- gets lexenv-  altBlock <- gets currentBlockName-  case altVal of-    Just v -> do-      terminate $ Br exitBlockName []-      return $ Just (v, altBlock, altEnv)-    Nothing -> do-      terminate $ Unreachable []-      return Nothing--mergeEnvs :: [(Name, Env)] -> Codegen ()-mergeEnvs es = do-  let vars = transpose-             . map (\(block, env) -> map (\x -> (x, block)) env)-             $ es-  env <- forM vars $ \var ->-         case var of-           [] -> ierror "mergeEnvs: impossible"-           [(v, _)] -> return v-           vs@((v, _):_)-                  | all (== v) (map fst vs) -> return v-                  | otherwise ->-                      let valid = map (\(a, b) -> (fromJust a, b)) . filter (isJust . fst) $ vs in-                      Just <$> inst (Phi (PointerType valueType (AddrSpace 0)) valid [])-  modify $ \s -> s { lexenv = env }--nameAlt :: Name -> SAlt -> Codegen Name-nameAlt d (SDefaultCase _) = return d-nameAlt _ (SConCase _ _ name _ _) = getName (show name)-nameAlt _ (SConstCase const _) = getName (show const)--isHeapFTy :: FType -> Bool-isHeapFTy f = elem f [FString, FPtr, FAny, FArith (ATInt ITBig)]--box :: FType -> Operand -> Codegen Operand-box FUnit _ = return $ ConstantOperand nullValue-box fty fval = do-  let ty = primTy (ftyToTy fty)-  val <- if isHeapFTy fty then alloc ty else allocAtomic ty-  tagptr <- inst $ GetElementPtr True val [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 0)] []-  valptr <- inst $ GetElementPtr True val [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 1)] []-  inst' $ Store False tagptr (ConstantOperand (C.Int 32 (-1))) Nothing 0 []-  inst' $ Store False valptr fval Nothing 0 []-  ptrI8 <- inst $ BitCast val (PointerType (IntegerType 8) (AddrSpace 0)) []-  inst' $ simpleCall "llvm.invariant.start" [ConstantOperand $ C.Int 64 (-1), ptrI8]-  inst $ BitCast val (PointerType valueType (AddrSpace 0)) []--unbox :: FType -> Operand -> Codegen Operand-unbox FUnit x = return x-unbox fty bval = do-  val <- inst $ BitCast bval (PointerType (primTy (ftyToTy fty)) (AddrSpace 0)) []-  fvalptr <- inst $ GetElementPtr True val [ConstantOperand (C.Int 32 0), ConstantOperand (C.Int 32 1)] []-  inst $ Load False fvalptr Nothing 0 []--cgConst' :: TT.Const -> C.Constant-cgConst' (TT.I i) = C.Int 32 (fromIntegral i)-cgConst' (TT.B8  i) = C.Int 8  (fromIntegral i)-cgConst' (TT.B16 i) = C.Int 16 (fromIntegral i)-cgConst' (TT.B32 i) = C.Int 32 (fromIntegral i)-cgConst' (TT.B64 i) = C.Int 64 (fromIntegral i)-cgConst' (TT.B8V  v) = C.Vector (map ((C.Int  8) . fromIntegral) . V.toList $ v)-cgConst' (TT.B16V v) = C.Vector (map ((C.Int 16) . fromIntegral) . V.toList $ v)-cgConst' (TT.B32V v) = C.Vector (map ((C.Int 32) . fromIntegral) . V.toList $ v)-cgConst' (TT.B64V v) = C.Vector (map ((C.Int 64) . fromIntegral) . V.toList $ v)--cgConst' (TT.BI i) = C.Array (IntegerType 8) (map (C.Int 8 . fromIntegral . fromEnum) (show i) ++ [C.Int 8 0])-cgConst' (TT.Fl f) = C.Float (F.Double f)-cgConst' (TT.Ch c) = C.Int 32 . fromIntegral . fromEnum $ c-cgConst' (TT.Str s) = C.Array (IntegerType 8) (map (C.Int 8 . fromIntegral . fromEnum) s ++ [C.Int 8 0])-cgConst' x = ierror $ "Unsupported constant: " ++ show x--cgConst :: TT.Const -> Codegen Operand-cgConst c@(TT.I _) = box (FArith (ATInt ITNative)) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B8  _) = box (FArith (ATInt (ITFixed IT8))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B16 _) = box (FArith (ATInt (ITFixed IT16))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B32 _) = box (FArith (ATInt (ITFixed IT32))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B64 _) = box (FArith (ATInt (ITFixed IT64))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B8V  v) = box (FArith (ATInt (ITVec IT8  (V.length v)))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B16V v) = box (FArith (ATInt (ITVec IT16 (V.length v)))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B32V v) = box (FArith (ATInt (ITVec IT32 (V.length v)))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.B64V v) = box (FArith (ATInt (ITVec IT64 (V.length v)))) (ConstantOperand $ cgConst' c)-cgConst c@(TT.Fl _) = box (FArith ATFloat) (ConstantOperand $ cgConst' c)-cgConst c@(TT.Ch _) = box (FArith (ATInt ITChar)) (ConstantOperand $ cgConst' c)-cgConst c@(TT.Str s) = do-  str <- addGlobal' (ArrayType (1 + fromIntegral (length s)) (IntegerType 8)) (cgConst' c)-  box FString (ConstantOperand $ C.GetElementPtr True str [C.Int 32 0, C.Int 32 0])-cgConst c@(TT.BI i) = do-  let stringRepLen = (if i < 0 then 2 else 1) + fromInteger (numDigits 10 i)-  str <- addGlobal' (ArrayType stringRepLen (IntegerType 8)) (cgConst' c)-  mpz <- alloc mpzTy-  inst $ simpleCall "__gmpz_init_set_str" [mpz-                                          , ConstantOperand $ C.GetElementPtr True str [ C.Int 32 0, C.Int 32 0]-                                          , ConstantOperand $ C.Int 32 10-                                          ]-  box (FArith (ATInt ITBig)) mpz-cgConst x = return $ ConstantOperand nullValue--numDigits :: Integer -> Integer -> Integer-numDigits b n = 1 + fst (ilog b n) where-    ilog b n-        | n < b     = (0, n)-        | otherwise = let (e, r) = ilog (b*b) n-                      in  if r < b then (2*e, r) else (2*e+1, r `div` b)--addGlobal :: Global -> Codegen ()-addGlobal def = tell ([], [], [GlobalDefinition def])--addGlobal' :: Type -> C.Constant -> Codegen C.Constant-addGlobal' ty val = do-  name <- getGlobalUnName-  addGlobal $ globalVariableDefaults-                { G.name = name-                , G.linkage = L.Internal-                , G.hasUnnamedAddr = True-                , G.isConstant = True-                , G.type' = ty-                , G.initializer = Just val-                }-  return . C.GlobalReference $ name---ensureCDecl :: String -> FType -> [FType] -> Codegen Operand-ensureCDecl name rty argtys = do-  syms <- gets foreignSyms-  case M.lookup name syms of-    Nothing -> do addGlobal (ffunDecl name rty argtys)-                  modify $ \s -> s { foreignSyms = M.insert name (rty, argtys) (foreignSyms s) }-    Just (rty', argtys') -> unless (rty == rty' && argtys == argtys') . fail $-                            "Mismatched type declarations for foreign symbol \"" ++ name ++ "\": " ++ show (rty, argtys) ++ " vs " ++ show (rty', argtys')-  return $ ConstantOperand (C.GlobalReference (Name name))--ffunDecl :: String -> FType -> [FType] -> Global-ffunDecl name rty argtys =-    functionDefaults-    { G.returnType = ftyToTy rty-    , G.name = Name name-    , G.parameters = (flip map argtys $ \fty ->-                          Parameter (ftyToTy fty) (UnName 0) []-                     , False)-    }--ftyToTy :: FType -> Type-ftyToTy (FArith (ATInt ITNative)) = IntegerType 32-ftyToTy (FArith (ATInt ITBig)) = PointerType mpzTy (AddrSpace 0)-ftyToTy (FArith (ATInt (ITFixed ty))) = IntegerType (fromIntegral $ nativeTyWidth ty)-ftyToTy (FArith (ATInt (ITVec e c)))-    = VectorType (fromIntegral c) (IntegerType (fromIntegral $ nativeTyWidth e))-ftyToTy (FArith (ATInt ITChar)) = IntegerType 32-ftyToTy (FArith ATFloat) = FloatingPointType 64 IEEE-ftyToTy FString = PointerType (IntegerType 8) (AddrSpace 0)-ftyToTy FUnit = VoidType-ftyToTy FPtr = PointerType (IntegerType 8) (AddrSpace 0)-ftyToTy FAny = valueType---- Only use when known not to be ITBig-itWidth :: IntTy -> Word32-itWidth ITNative = 32-itWidth ITChar = 32-itWidth (ITFixed x) = fromIntegral $ nativeTyWidth x-itWidth x = ierror $ "itWidth: " ++ show x--itConst :: IntTy -> Integer -> C.Constant-itConst (ITFixed n) x = C.Int (fromIntegral $ nativeTyWidth n) x-itConst ITNative x = itConst (ITFixed IT32) x-itConst ITChar x = itConst (ITFixed IT32) x-itConst (ITVec elts size) x = C.Vector (replicate size (itConst (ITFixed elts) x))--cgOp :: PrimFn -> [Operand] -> Codegen Operand-cgOp (LTrunc ITBig ity) [x] = do-  nx <- unbox (FArith (ATInt ITBig)) x-  val <- inst $ simpleCall "mpz_get_ull" [nx]-  v <- case ity of-         (ITFixed IT64) -> return val-         _ -> inst $ Trunc val (ftyToTy (FArith (ATInt ity))) []-  box (FArith (ATInt ity)) v-cgOp (LZExt from ITBig) [x] = do-  nx <- unbox (FArith (ATInt from)) x-  nx' <- case from of-           (ITFixed IT64) -> return nx-           _ -> inst $ ZExt nx (IntegerType 64) []-  mpz <- alloc mpzTy-  inst' $ simpleCall "mpz_init_set_ull" [mpz, nx']-  box (FArith (ATInt ITBig)) mpz-cgOp (LSExt from ITBig) [x] = do-  nx <- unbox (FArith (ATInt from)) x-  nx' <- case from of-           (ITFixed IT64) -> return nx-           _ -> inst $ SExt nx (IntegerType 64) []-  mpz <- alloc mpzTy-  inst' $ simpleCall "mpz_init_set_sll" [mpz, nx']-  box (FArith (ATInt ITBig)) mpz---- ITChar, ITNative, and IT32 all share representation-cgOp (LChInt ITNative) [x] = return x-cgOp (LIntCh ITNative) [x] = return x--cgOp (LSLt   (ATInt ITBig)) [x,y] = mpzCmp IPred.SLT x y-cgOp (LSLe   (ATInt ITBig)) [x,y] = mpzCmp IPred.SLE x y-cgOp (LEq    (ATInt ITBig)) [x,y] = mpzCmp IPred.EQ  x y-cgOp (LSGe   (ATInt ITBig)) [x,y] = mpzCmp IPred.SGE x y-cgOp (LSGt   (ATInt ITBig)) [x,y] = mpzCmp IPred.SGT x y-cgOp (LPlus  (ATInt ITBig)) [x,y] = mpzBin "add" x y-cgOp (LMinus (ATInt ITBig)) [x,y] = mpzBin "sub" x y-cgOp (LTimes (ATInt ITBig)) [x,y] = mpzBin "mul" x y-cgOp (LSDiv  (ATInt ITBig)) [x,y] = mpzBin "fdiv_q" x y-cgOp (LSRem  (ATInt ITBig)) [x,y] = mpzBin "fdiv_r" x y-cgOp (LAnd   ITBig) [x,y] = mpzBin "and" x y-cgOp (LOr    ITBig) [x,y] = mpzBin "ior" x y-cgOp (LXOr   ITBig) [x,y] = mpzBin "xor" x y-cgOp (LCompl ITBig) [x]   = mpzUn "com" x-cgOp (LSHL   ITBig) [x,y] = mpzBit "mul_2exp" x y-cgOp (LASHR  ITBig) [x,y] = mpzBit "fdiv_q_2exp" x y--cgOp (LTrunc ITNative (ITFixed to)) [x]-    | 32 >= nativeTyWidth to = iCoerce Trunc IT32 to x-cgOp (LZExt ITNative (ITFixed to)) [x]-    | 32 <= nativeTyWidth to = iCoerce ZExt IT32 to x-cgOp (LSExt ITNative (ITFixed to)) [x]-    | 32 <= nativeTyWidth to = iCoerce SExt IT32 to x--cgOp (LTrunc (ITFixed from) ITNative) [x]-    | nativeTyWidth from >= 32 = iCoerce Trunc from IT32 x-cgOp (LZExt (ITFixed from) ITNative) [x]-    | nativeTyWidth from <= 32 = iCoerce ZExt from IT32 x-cgOp (LSExt (ITFixed from) ITNative) [x]-    | nativeTyWidth from <= 32 = iCoerce SExt from IT32 x--cgOp (LTrunc (ITFixed from) (ITFixed to)) [x]-    | nativeTyWidth from > nativeTyWidth to = iCoerce Trunc from to x-cgOp (LZExt (ITFixed from) (ITFixed to)) [x]-    | nativeTyWidth from < nativeTyWidth to = iCoerce ZExt from to x-cgOp (LSExt (ITFixed from) (ITFixed to)) [x]-    | nativeTyWidth from < nativeTyWidth to = iCoerce SExt from to x--cgOp (LSLt   (ATInt ity)) [x,y] = iCmp ity IPred.SLT x y-cgOp (LSLe   (ATInt ity)) [x,y] = iCmp ity IPred.SLE x y-cgOp (LLt    ity)         [x,y] = iCmp ity IPred.ULT x y-cgOp (LLe    ity)         [x,y] = iCmp ity IPred.ULE x y-cgOp (LEq    (ATInt ity)) [x,y] = iCmp ity IPred.EQ  x y-cgOp (LSGe   (ATInt ity)) [x,y] = iCmp ity IPred.SGE x y-cgOp (LSGt   (ATInt ity)) [x,y] = iCmp ity IPred.SGT x y-cgOp (LGe    ity)         [x,y] = iCmp ity IPred.UGE x y-cgOp (LGt    ity)         [x,y] = iCmp ity IPred.UGT x y-cgOp (LPlus  ty@(ATInt _)) [x,y] = binary ty x y (Add False False)-cgOp (LMinus ty@(ATInt _)) [x,y] = binary ty x y (Sub False False)-cgOp (LTimes ty@(ATInt _)) [x,y] = binary ty x y (Mul False False)-cgOp (LSDiv  ty@(ATInt _)) [x,y] = binary ty x y (SDiv False)-cgOp (LSRem  ty@(ATInt _)) [x,y] = binary ty x y SRem-cgOp (LUDiv  ity)          [x,y] = binary (ATInt ity) x y (UDiv False)-cgOp (LURem  ity)          [x,y] = binary (ATInt ity) x y URem-cgOp (LAnd   ity)          [x,y] = binary (ATInt ity) x y And-cgOp (LOr    ity)          [x,y] = binary (ATInt ity) x y Or-cgOp (LXOr   ity)          [x,y] = binary (ATInt ity) x y Xor-cgOp (LCompl ity)          [x] = unary (ATInt ity) x (Xor . ConstantOperand $ itConst ity (-1))-cgOp (LSHL   ity)          [x,y] = binary (ATInt ity) x y (Shl False False)-cgOp (LLSHR  ity)          [x,y] = binary (ATInt ity) x y (LShr False)-cgOp (LASHR  ity)          [x,y] = binary (ATInt ity) x y (AShr False)--cgOp (LSLt   ATFloat) [x,y] = fCmp FPred.OLT x y-cgOp (LSLe   ATFloat) [x,y] = fCmp FPred.OLE x y-cgOp (LEq    ATFloat) [x,y] = fCmp FPred.OEQ x y-cgOp (LSGe   ATFloat) [x,y] = fCmp FPred.OGE x y-cgOp (LSGt   ATFloat) [x,y] = fCmp FPred.OGT x y-cgOp (LPlus  ATFloat) [x,y] = binary ATFloat x y FAdd-cgOp (LMinus ATFloat) [x,y] = binary ATFloat x y FSub-cgOp (LTimes ATFloat) [x,y] = binary ATFloat x y FMul -cgOp (LSDiv  ATFloat) [x,y] = binary ATFloat x y FDiv--cgOp LFExp   [x] = nunary ATFloat "llvm.exp.f64" x -cgOp LFLog   [x] = nunary ATFloat "llvm.log.f64" x-cgOp LFSin   [x] = nunary ATFloat "llvm.sin.f64" x-cgOp LFCos   [x] = nunary ATFloat "llvm.cos.f64" x-cgOp LFTan   [x] = nunary ATFloat "tan" x-cgOp LFASin  [x] = nunary ATFloat "asin" x-cgOp LFACos  [x] = nunary ATFloat "acos" x-cgOp LFATan  [x] = nunary ATFloat "atan" x-cgOp LFSqrt  [x] = nunary ATFloat "llvm.sqrt.f64" x-cgOp LFFloor [x] = nunary ATFloat "llvm.floor.f64" x-cgOp LFCeil  [x] = nunary ATFloat "llvm.ceil.f64" x--cgOp (LIntFloat ITBig) [x] = do-  x' <- unbox (FArith (ATInt ITBig)) x-  uflt <- inst $ simpleCall "__gmpz_get_d" [ x' ]-  box (FArith ATFloat) uflt--cgOp (LIntFloat ity) [x] = do-  x' <- unbox (FArith (ATInt ity)) x-  x'' <- inst $ SIToFP x' (FloatingPointType 64 IEEE) []-  box (FArith ATFloat) x''--cgOp (LFloatInt ITBig) [x] = do-  x' <- unbox (FArith ATFloat) x-  z  <- alloc mpzTy-  inst' $ simpleCall "__gmpz_init" [z]-  inst' $ simpleCall "__gmpz_set_d" [ z, x' ]-  box (FArith (ATInt ITBig)) z--cgOp (LFloatInt ity) [x] = do-  x' <- unbox (FArith ATFloat) x-  x'' <- inst $ FPToSI x' (ftyToTy $ cmpResultTy ity) []-  box (FArith (ATInt ity)) x''--cgOp LFloatStr [x] = do-    x' <- unbox (FArith ATFloat) x-    ustr <- inst (idrCall "__idris_floatStr" [x'])-    box FString ustr --cgOp LNoOp xs = return $ last xs--cgOp (LMkVec ety c) xs | c == length xs = do-  nxs <- mapM (unbox (FArith (ATInt (ITFixed ety)))) xs-  vec <- foldM (\v (e, i) -> inst $ InsertElement v e (ConstantOperand (C.Int 32 i)) [])-               (ConstantOperand $ C.Vector (replicate c (C.Undef (IntegerType . fromIntegral $ nativeTyWidth ety))))-               (zip nxs [0..])-  box (FArith (ATInt (ITVec ety c))) vec--cgOp (LIdxVec ety c) [v,i] = do-  nv <- unbox (FArith (ATInt (ITVec ety c))) v-  ni <- unbox (FArith (ATInt (ITFixed IT32))) i-  elt <- inst $ ExtractElement nv ni []-  box (FArith (ATInt (ITFixed ety))) elt--cgOp (LUpdateVec ety c) [v,i,e] = do-  let fty = FArith (ATInt (ITVec ety c))-  nv <- unbox fty v-  ni <- unbox (FArith (ATInt (ITFixed IT32))) i-  ne <- unbox (FArith (ATInt (ITFixed ety))) e-  nv' <- inst $ InsertElement nv ne ni []-  box fty nv'--cgOp (LBitCast from to) [x] = do-  nx <- unbox (FArith from) x-  nx' <- inst $ BitCast nx (ftyToTy (FArith to)) []-  box (FArith to) nx'--cgOp LStrEq [x,y] = do-  x' <- unbox FString x-  y' <- unbox FString y-  cmp <- inst $ simpleCall "strcmp" [x', y']-  flag <- inst $ ICmp IPred.EQ cmp (ConstantOperand (C.Int 32 0)) []-  val <- inst $ ZExt flag (IntegerType 32) []-  box (FArith (ATInt (ITFixed IT32))) val--cgOp LStrLt [x,y] = do-  nx <- unbox FString x-  ny <- unbox FString y-  cmp <- inst $ simpleCall "strcmp" [nx, ny]-  flag <- inst $ ICmp IPred.ULT cmp (ConstantOperand (C.Int 32 0)) []-  val <- inst $ ZExt flag (IntegerType 32) []-  box (FArith (ATInt (ITFixed IT32))) val--cgOp (LIntStr ITBig) [x] = do-  x' <- unbox (FArith (ATInt ITBig)) x-  ustr <- inst $ simpleCall "__gmpz_get_str"-          [ ConstantOperand (C.Null (PointerType (IntegerType 8) (AddrSpace 0)))-          , ConstantOperand (C.Int 32 10)-          , x'-          ]-  box FString ustr-cgOp (LIntStr ity) [x] = do-  x' <- unbox (FArith (ATInt ity)) x-  x'' <- if itWidth ity < 64-         then inst $ SExt x' (IntegerType 64) []-         else return x'-  box FString =<< inst (idrCall "__idris_intStr" [x''])-cgOp (LStrInt ITBig) [s] = do-  ns <- unbox FString s-  mpz <- alloc mpzTy-  inst $ simpleCall "__gmpz_init_set_str" [mpz, ns, ConstantOperand $ C.Int 32 10]-  box (FArith (ATInt ITBig)) mpz-cgOp (LStrInt ity) [s] = do-  ns <- unbox FString s-  nx <- inst $ simpleCall "strtoll"-        [ns-        , ConstantOperand $ C.Null (PointerType (PointerType (IntegerType 8) (AddrSpace 0)) (AddrSpace 0))-        , ConstantOperand $ C.Int 32 10-        ]-  nx' <- case ity of-           (ITFixed IT64) -> return nx-           _ -> inst $ Trunc nx (IntegerType (itWidth ity)) []-  box (FArith (ATInt ity)) nx'--cgOp LStrConcat [x,y] = cgStrCat x y--cgOp LStrCons [c,s] = do-  nc <- unbox (FArith (ATInt ITChar)) c-  ns <- unbox FString s-  nc' <- inst $ Trunc nc (IntegerType 8) []-  r <- inst $ simpleCall "__idris_strCons" [nc', ns]-  box FString r--cgOp LStrHead [c] = do-  s <- unbox FString c-  c <- inst $ Load False s Nothing 0 []-  c' <- inst $ ZExt c (IntegerType 32) []-  box (FArith (ATInt ITChar)) c'--cgOp LStrIndex [s, i] = do-  ns <- unbox FString s-  ni <- unbox (FArith (ATInt (ITFixed IT32))) i-  p <- inst $ GetElementPtr True ns [ni] []-  c <- inst $ Load False p Nothing 0 []-  c' <- inst $ ZExt c (IntegerType 32) []-  box (FArith (ATInt ITChar)) c'--cgOp LStrTail [c] = do-  s <- unbox FString c-  c <- inst $ GetElementPtr True s [ConstantOperand $ C.Int 32 1] []-  box FString c--cgOp LStrLen [s] = do-  ns <- unbox FString s-  len <- inst $ simpleCall "strlen" [ns]-  ws <- getWordSize-  len' <- case ws of-            32 -> return len-            x | x > 32 -> inst $ Trunc len (IntegerType 32) []-              | x < 32 -> inst $ ZExt len (IntegerType 32) []-  box (FArith (ATInt (ITFixed IT32))) len'--cgOp LStrRev [s] = do-  ns <- unbox FString s-  box FString =<< inst (simpleCall "__idris_strRev" [ns])--cgOp LReadStr [p] = do-  np <- unbox FPtr p-  s <- inst $ simpleCall "__idris_readStr" [np]-  box FString s--cgOp LStdIn  [] = do-  stdin <- getStdIn-  ptr <- inst $ loadInv stdin-  box FPtr ptr-cgOp LStdOut  [] = do-  stdout <- getStdOut-  ptr <- inst $ loadInv stdout-  box FPtr ptr-cgOp LStdErr  [] = do-  stdErr <- getStdErr-  ptr <- inst $ loadInv stdErr-  box FPtr ptr--cgOp LNullPtr [] = box FPtr (ConstantOperand $ C.Null (PointerType (IntegerType 8) (AddrSpace 0)))--cgOp prim args = ierror $ "Unimplemented primitive: <" ++ show prim ++ ">("-                  ++ intersperse ',' (take (length args) ['a'..]) ++ ")"--iCoerce :: (Operand -> Type -> InstructionMetadata -> Instruction) -> NativeTy -> NativeTy -> Operand -> Codegen Operand-iCoerce _ from to x | from == to = return x-iCoerce operator from to x = do-  x' <- unbox (FArith (ATInt (ITFixed from))) x-  x'' <- inst $ operator x' (ftyToTy (FArith (ATInt (ITFixed to)))) []-  box (FArith (ATInt (ITFixed to))) x''--cgStrCat :: Operand -> Operand -> Codegen Operand-cgStrCat x y = do-  x' <- unbox FString x-  y' <- unbox FString y-  xlen <- inst $ simpleCall "strlen" [x']-  ylen <- inst $ simpleCall "strlen" [y']-  zlen <- inst $ Add False True xlen ylen []-  ws <- getWordSize-  total <- inst $ Add False True zlen (ConstantOperand (C.Int ws 1)) []-  mem <- allocAtomic' total-  inst $ simpleCall "memcpy" [mem, x', xlen]-  i <- inst $ PtrToInt mem (IntegerType ws) []-  offi <- inst $ Add False True i xlen []-  offp <- inst $ IntToPtr offi (PointerType (IntegerType 8) (AddrSpace 0)) []-  inst $ simpleCall "memcpy" [offp, y', ylen]-  j <- inst $ PtrToInt offp (IntegerType ws) []-  offj <- inst $ Add False True j ylen []-  end <- inst $ IntToPtr offj (PointerType (IntegerType 8) (AddrSpace 0)) []-  inst' $ Store False end (ConstantOperand (C.Int 8 0)) Nothing 0 []-  box FString mem--binary :: ArithTy -> Operand -> Operand-     -> (Operand -> Operand -> InstructionMetadata -> Instruction) -> Codegen Operand-binary ty x y instCon = do-  nx <- unbox (FArith ty) x-  ny <- unbox (FArith ty) y-  nr <- inst $ instCon nx ny []-  box (FArith ty) nr--unary :: ArithTy -> Operand -    -> (Operand -> InstructionMetadata -> Instruction) -> Codegen Operand-unary ty x instCon = do-  nx <- unbox (FArith ty) x-  nr <- inst $ instCon nx []-  box (FArith ty) nr--nunary :: ArithTy -> String-     -> Operand -> Codegen Operand-nunary ty name x = do-  nx <- unbox (FArith ty) x-  nr <- inst $ simpleCall name [nx]-  box (FArith ty) nr--iCmp :: IntTy -> IPred.IntegerPredicate -> Operand -> Operand -> Codegen Operand-iCmp ity pred x y = do-  nx <- unbox (FArith (ATInt ity)) x-  ny <- unbox (FArith (ATInt ity)) y-  nr <- inst $ ICmp pred nx ny []-  nr' <- inst $ SExt nr (ftyToTy $ cmpResultTy ity) []-  box (cmpResultTy ity) nr'--fCmp :: FPred.FloatingPointPredicate -> Operand -> Operand -> Codegen Operand-fCmp pred x y = do-  nx <- unbox (FArith ATFloat) x-  ny <- unbox (FArith ATFloat) y-  nr <- inst $ FCmp pred nx ny []-  box (FArith (ATInt (ITFixed IT32))) nr--cmpResultTy :: IntTy -> FType-cmpResultTy v@(ITVec _ _) = FArith (ATInt v)-cmpResultTy _ = FArith (ATInt (ITFixed IT32))--mpzBin :: String -> Operand -> Operand -> Codegen Operand-mpzBin name x y = do-  nx <- unbox (FArith (ATInt ITBig)) x-  ny <- unbox (FArith (ATInt ITBig)) y-  nz <- alloc mpzTy-  inst' $ simpleCall "__gmpz_init" [nz]-  inst' $ simpleCall ("__gmpz_" ++ name) [nz, nx, ny]-  box (FArith (ATInt ITBig)) nz--mpzBit :: String -> Operand -> Operand -> Codegen Operand-mpzBit name x y = do-  nx <- unbox (FArith (ATInt ITBig)) x-  ny <- unbox (FArith (ATInt ITBig)) y-  bitcnt <- inst $ simpleCall "__gmpz_get_ui" [ny]-  nz <- alloc mpzTy-  inst' $ simpleCall "__gmpz_init" [nz]-  inst' $ simpleCall ("__gmpz_" ++ name) [nz, nx, bitcnt]-  box (FArith (ATInt ITBig)) nz--mpzUn :: String -> Operand -> Codegen Operand-mpzUn name x = do-  nx <- unbox (FArith (ATInt ITBig)) x-  nz <- alloc mpzTy-  inst' $ simpleCall "__gmpz_init" [nz]-  inst' $ simpleCall ("__gmpz_" ++ name) [nz, nx]-  box (FArith (ATInt ITBig)) nz--mpzCmp :: IPred.IntegerPredicate -> Operand -> Operand -> Codegen Operand-mpzCmp pred x y = do-  nx <- unbox (FArith (ATInt ITBig)) x-  ny <- unbox (FArith (ATInt ITBig)) y-  cmp <- inst $ simpleCall "__gmpz_cmp" [nx, ny]-  result <- inst $ ICmp pred cmp (ConstantOperand (C.Int 32 0)) []-  i <- inst $ ZExt result (IntegerType 32) []-  box (FArith (ATInt (ITFixed IT32))) i--simpleCall :: String -> [Operand] -> Instruction-simpleCall name args =-    Call { isTailCall = False-         , callingConvention = CC.C-         , returnAttributes = []-         , function = Right . ConstantOperand . C.GlobalReference . Name $ name-         , arguments = map (\x -> (x, [])) args-         , functionAttributes = []-         , metadata = []-         }--idrCall :: String -> [Operand] -> Instruction-idrCall name args =-    Call { isTailCall = False-         , callingConvention = CC.Fast-         , returnAttributes = []-         , function = Right . ConstantOperand . C.GlobalReference . Name $ name-         , arguments = map (\x -> (x, [])) args-         , functionAttributes = []-         , metadata = []-         }--assert :: Operand -> String -> Codegen ()-assert condition message = do-  passed <- getName "assertPassed"-  failed <- getName "assertFailed"-  terminate $ CondBr condition passed failed []-  newBlock failed-  cgExpr (SError message)-  terminate $ Unreachable []-  newBlock passed