idris 1.1.0 → 1.1.1

raw patch · 25 files changed

+521/−402 lines, 25 filesdep −tagsoupdep −zlibdep ~aesondep ~binarydep ~cheapskatesetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: tagsoup, zlib

Dependency ranges changed: aeson, binary, cheapskate, ieee754, optparse-applicative, process, safe, time, trifecta

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−0
• Setup.hs +42/−25
• docs/reference/partial-evaluation.rst +10/−10
• idris.cabal +22/−39
• jsrts/Runtime-node.js +1/−1
• libs/contrib/Text/Lexer.idr +27/−17
• libs/contrib/Text/Parser.idr +67/−26
• libs/contrib/Text/PrettyPrint/WL/Characters.idr +2/−2
• libs/contrib/Text/PrettyPrint/WL/Core.idr +4/−4
• libs/prelude/Prelude/Bits.idr +4/−4
• libs/prelude/Prelude/List.idr +5/−1
• libs/pruviloj/Pruviloj/Core.idr +48/−2
• rts/idris_rts.c +10/−4
• scripts/runidris +9/−2
• scripts/runidris-node +11/−4
• src/IRTS/CodegenC.hs +113/−230
• src/IRTS/Compiler.hs +2/−0
• src/Idris/Core/Binary.hs +4/−2
• src/Idris/DeepSeq.hs +0/−14
• src/Idris/Erasure.hs +120/−12
• src/Idris/IBC.hs +1/−1
• stack.yaml +3/−1
• test/TestRun.hs +2/−1
• test/base001/exit1.c +4/−0
• test/base001/sys.c +4/−0

@@ -1,3 +1,9 @@+# New in 1.1.1+++ Erasure analysis is now faster thanks to a bit smarter constraint solving.++ Fixed installation issue++ Fixed a potential segfault when concatenating strings+ # New in 1.1.0  ## Library Updates

@@ -1,11 +1,15 @@ {-# LANGUAGE CPP #-} +#if !defined(MIN_VERSION_Cabal)+# define MIN_VERSION_Cabal(x,y,z) 0+#endif+ import Control.Monad import Data.IORef import Control.Exception (SomeException, catch)  import Distribution.Simple-import Distribution.Simple.BuildPaths (autogenModulesDir)+import Distribution.Simple.BuildPaths import Distribution.Simple.InstallDirs as I import Distribution.Simple.LocalBuildInfo as L import qualified Distribution.Simple.Setup as S@@ -56,32 +60,37 @@  usesGMP :: S.ConfigFlags -> Bool usesGMP flags =-  case lookup (FlagName "gmp") (S.configConfigurationsFlags flags) of+  case lookup (mkFlagName "gmp") (S.configConfigurationsFlags flags) of     Just True -> True     Just False -> False     Nothing -> False  execOnly :: S.ConfigFlags -> Bool execOnly flags =-  case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of+  case lookup (mkFlagName "execonly") (S.configConfigurationsFlags flags) of     Just True -> True     Just False -> False     Nothing -> False  isRelease :: S.ConfigFlags -> Bool isRelease flags =-    case lookup (FlagName "release") (S.configConfigurationsFlags flags) of+    case lookup (mkFlagName "release") (S.configConfigurationsFlags flags) of       Just True -> True       Just False -> False       Nothing -> False  isFreestanding :: S.ConfigFlags -> Bool isFreestanding flags =-  case lookup (FlagName "freestanding") (S.configConfigurationsFlags flags) of+  case lookup (mkFlagName "freestanding") (S.configConfigurationsFlags flags) of     Just True -> True     Just False -> False     Nothing -> False +#if !(MIN_VERSION_Cabal(2,0,0))+mkFlagName :: String -> FlagName+mkFlagName = FlagName+#endif+ -- ----------------------------------------------------------------------------- -- Clean @@ -151,20 +160,22 @@     createDirectoryIfMissingVerbose verbosity True srcDir     rewriteFile toolPath (commonContent ++ toolContent) -idrisConfigure _ flags _ local = do+idrisConfigure _ flags pkgdesc local = do     configureRTS-    generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))-    if isFreestanding $ configFlags local-        then do-                toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"-                generateToolchainModule verbosity (autogenModulesDir local) toolDir-                targetDir <- lookupEnv "IDRIS_LIB_DIR"-                case targetDir of-                     Just d -> generateTargetModule verbosity (autogenModulesDir local) d-                     Nothing -> error $ "Trying to build freestanding without a target directory."-                                  ++ " Set it by defining IDRIS_LIB_DIR."-        else-                generateToolchainModule verbosity (autogenModulesDir local) Nothing+    withLibLBI pkgdesc local $ \_ libcfg -> do+      let libAutogenDir = autogenComponentModulesDir local libcfg+      generateVersionModule verbosity libAutogenDir (isRelease (configFlags local))+      if isFreestanding $ configFlags local+          then do+                  toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"+                  generateToolchainModule verbosity libAutogenDir toolDir+                  targetDir <- lookupEnv "IDRIS_LIB_DIR"+                  case targetDir of+                       Just d -> generateTargetModule verbosity libAutogenDir d+                       Nothing -> error $ "Trying to build freestanding without a target directory."+                                    ++ " Set it by defining IDRIS_LIB_DIR."+          else+                  generateToolchainModule verbosity libAutogenDir Nothing     where       verbosity = S.fromFlag $ S.configVerbosity flags       version   = pkgVersion . package $ localPkgDescr local@@ -175,6 +186,10 @@       -- the file after configure.       configureRTS = make verbosity ["-C", "rts", "clean"] +#if !(MIN_VERSION_Cabal(2,0,0))+      autogenComponentModulesDir lbi _ = autogenModulesDir lbi+#endif+ idrisPreSDist args flags = do   let dir = S.fromFlag (S.sDistDirectory flags)   let verb = S.fromFlag (S.sDistVerbosity flags)@@ -225,9 +240,10 @@         return (Nothing, []) #endif -idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do-      buildStdLib-      buildRTS+idrisBuild _ flags _ local +   = if (execOnly (configFlags local)) then buildRTS+        else do buildStdLib+                buildRTS    where       verbosity = S.fromFlag $ S.buildVerbosity flags @@ -246,10 +262,11 @@ -- ----------------------------------------------------------------------------- -- Copy/Install -idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do-      installStdLib-      installRTS-      installManPage+idrisInstall verbosity copy pkg local +   = if (execOnly (configFlags local)) then installRTS+        else do installStdLib+                installRTS+                installManPage    where       target = datadir $ L.absoluteInstallDirs pkg local copy 

@@ -4,15 +4,15 @@  As of version 0.9.15, Idris has support for *partial evaluation* of statically known arguments. This involves creating specialised versions-of functions with arguments annotated as ``[static]``.+of functions with arguments annotated as ``%static``.  (This is an implementation of the partial evaluator described in `this ICFP 2010 paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__. Please refer to this for more precise definitions of what follows.) -Partial evaluation is switched on by default. It can be disabled with-the ``--no-partial-eval`` flag.+Partial evaluation is switched off by default since Idris 1.0. It can+be enabled with the ``--partial-eval`` flag.  Introductory Example --------------------@@ -66,18 +66,18 @@ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  The trick is to mark the statically known arguments with the-``[static]`` flag:+``%static`` flag:  :: -    my_pow : Nat -> [static] Nat -> Nat+    my_pow : Nat -> %static Nat -> Nat     my_pow k Z = 1     my_pow k (S j) = mult k (my_pow k j)  When an argument is annotated in this way, Idris will try to create a specialised version whenever it accounts a call with a concrete value (i.e. a constant, constructor form, or globally defined function) in a-``[static]`` position. If ``my_pow`` is defined this way, and ``powFn``+``%static`` position. If ``my_pow`` is defined this way, and ``powFn`` defined as above, we can see the effect by typing ``:printdef powFn`` at the REPL: @@ -108,7 +108,7 @@ -------------------------  Type class dictionaries are very often statically known, so Idris-automatically marks any type class constraint as ``[static]`` and builds+automatically marks any type class constraint as ``%static`` and builds specialised versions of top level functions where the class is instantiated. For example, given: @@ -177,7 +177,7 @@  :: -    my_map : [static] (a -> b) -> List a -> List b+    my_map : %static (a -> b) -> List a -> List b     my_map f [] = []     my_map f (x :: xs) = f x :: my_map f xs @@ -246,11 +246,11 @@                 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))  The interpreter's type is written as follows, marking the expression to-be evaluated as ``[static]``:+be evaluated as ``%static``:  :: -    interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t+    interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t  This means that if we write an Idris program to calculate a factorial by calling ``interp`` on ``eFac``, the resulting definition will be

@@ -1,5 +1,5 @@ Name:           idris-Version:        1.1.0+Version:        1.1.1 License:        BSD3 License-file:   LICENSE Author:         Edwin Brady@@ -44,7 +44,7 @@  Build-type:     Custom -Tested-With:    GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1+Tested-With:    GHC == 7.10.3, GHC == 8.0.1  Data-files:            idrisdoc/styles.css                        jsrts/jsbn/jsbn-browser.js@@ -97,6 +97,14 @@   type:     git   location: git://github.com/idris-lang/Idris-dev.git +custom-setup+  setup-depends:+    Cabal >= 1.10 && <2.1,+    base  >= 4 && <5,+    directory,+    filepath,+    process+ Flag FFI   Description:  Build support for libffi   Default:      False@@ -111,7 +119,7 @@ -- Defaults to True because Hackage is a source release Flag release   Description:  This is an official release-  Default:      True+  Default:      False   manual:       True  Flag freestanding@@ -259,17 +267,17 @@                 , Tools_idris    Build-depends:  base >=4 && <5-                , aeson >= 0.6 && < 1.2+                , aeson >= 0.6 && < 1.3                 , annotated-wl-pprint >= 0.7 && < 0.8                 , ansi-terminal < 0.7                 , ansi-wl-pprint < 0.7                 , array >= 0.4.0.1 && < 0.6                 , base64-bytestring < 1.1-                , binary >= 0.7 && < 0.9+                , binary >= 0.8.4.1 && < 0.9                 , blaze-html >= 0.6.1.3 && < 0.10                 , blaze-markup >= 0.5.2.1 && < 0.9                 , bytestring < 0.11-                , cheapskate < 0.2+                , cheapskate >= 0.1.1 && < 0.2                 , code-page >= 0.1 && < 0.2                 , containers >= 0.5 && < 0.6                 , deepseq < 1.5@@ -277,20 +285,22 @@                 , filepath < 1.5                 , fingertree >= 0.1 && < 0.2                 , haskeline >= 0.7 && < 0.8-                , ieee754 >= 0.7 && <= 0.8.0+                , ieee754 >= 0.7 && < 0.9                 , mtl >= 2.1 && < 2.3                 , network < 2.7-                , optparse-applicative >= 0.13 && < 0.14+                , optparse-applicative >= 0.13 && < 0.15                 , parsers >= 0.9 && < 0.13                 , pretty < 1.2+                , process < 1.7                 , regex-tdfa >= 1.2+                , safe >= 0.3.9                 , split < 0.3                 , terminal-size < 0.4                 , text >=1.2.1.0 && < 1.3-                , time >= 1.4 && < 1.7+                , time >= 1.4 && < 1.9                 , transformers < 0.6                 , transformers-compat >= 0.3-                , trifecta >= 1.6 && < 1.7+                , trifecta >= 1.6 && < 1.8                 , uniplate >=1.6 && < 1.7                 , unordered-containers < 0.3                 , utf8-string < 1.1@@ -300,41 +310,14 @@                 , fsnotify >= 0.2 && < 2.2                 , async < 2.2 --  -- zlib >= 0.6.1 is broken with GHC < 7.10.3-  -- Travis is broken for 7.6 and 7.8 with a newer process-  if impl(ghc < 7.10.3)-     build-depends: zlib < 0.6.1-                  , process < 1.3-  else-     build-depends: process < 1.5--  -- safe 0.3.10 is having issues with cabal 1.20 and ghc 7.6.3, the-  -- hvr ghc ppa doesn't provide a new enough cabal library. Temporary-  -- fix until hvr ghc ppa is fixed or we deprecate support for 7.6.3.-  if impl(ghc < 7.8.4)-     build-depends: safe == 0.3.9-  else-     build-depends: safe >= 0.3.9--  if impl(ghc < 7.8.4)-     build-depends: tagsoup < 0.14.1-   Default-Language: Haskell2010-   ghc-prof-options: -auto-all -caf-all -  if os(linux)-     build-depends: unix < 2.8-  if os(freebsd)-     build-depends: unix < 2.8---   if os(dragonfly)---      build-depends: unix < 2.8-  if os(darwin)-     build-depends: unix < 2.8   if os(windows)      build-depends: mintty >= 0.1 && < 0.2                   , Win32 < 2.4+  else+     build-depends: unix < 2.8   if flag(FFI)      build-depends: libffi < 0.2      cpp-options:   -DIDRIS_FFI

@@ -22,7 +22,7 @@         }         i++;         if (i == b.length) {-            nb = new Buffer(b.length * 2);+            var nb = new Buffer(b.length * 2);             b.copy(nb)             b = nb;         }

@@ -23,11 +23,11 @@ inf : Bool -> Type -> Type inf True t = Inf t inf False t = t-  + ||| Sequence two recognisers. If either consumes a character, the sequence ||| is guaranteed to consume a character. export %inline-(<+>) : {c1 : Bool} -> +(<+>) : {c1 : Bool} ->         Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2) (<+>) {c1 = False} = SeqEmpty (<+>) {c1 = True} = SeqEat@@ -59,6 +59,17 @@ many : Lexer -> Recognise False many l = some l <|> Empty +||| Recognise many instances of `l` until an instance of `end` is+||| encountered.+|||+||| Useful for defining comments.+export+manyTill : (l : Lexer)+        -> (end : Lexer) -> Recognise False+manyTill l end = end+             <|> (l <+> manyTill l end)+             <|> Empty+ ||| Recognise any character export any : Lexer@@ -86,7 +97,7 @@ getString (MkStrLen str n) = str  strIndex : StrLen -> Nat -> Maybe Char-strIndex (MkStrLen str len) i +strIndex (MkStrLen str len) i     = if i >= len then Nothing                   else Just (assert_total (prim__strIndex str (cast i))) @@ -102,25 +113,25 @@ scan : Recognise c -> Nat -> StrLen -> Maybe Nat scan Empty idx str = pure idx scan Fail idx str = Nothing-scan (Pred f) idx str +scan (Pred f) idx str     = do c <- strIndex str idx          if f c             then Just (idx + 1)             else Nothing-scan (SeqEat r1 r2) idx str +scan (SeqEat r1 r2) idx str     = do idx' <- scan r1 idx str          -- TODO: Can we prove totality instead by showing idx has increased?          assert_total (scan r2 idx' str)-scan (SeqEmpty r1 r2) idx str +scan (SeqEmpty r1 r2) idx str     = do idx' <- scan r1 idx str          scan r2 idx' str-scan (Alt r1 r2) idx str +scan (Alt r1 r2) idx str     = case scan r1 idx str of            Nothing => scan r2 idx str            Just idx => Just idx  takeToken : Lexer -> StrLen -> Maybe (String, StrLen)-takeToken lex str +takeToken lex str     = do i <- scan lex 0 str -- i must be > 0 if successful          pure (substr 0 i (getString str), strTail i str) @@ -134,7 +145,7 @@ exact : String -> Lexer exact str with (unpack str)   exact str | [] = Fail -- Not allowed, Lexer has to consume-  exact str | (x :: xs) +  exact str | (x :: xs)       = foldl SeqEmpty (is x) (map is xs)  ||| Recognise a whitespace character@@ -185,8 +196,8 @@  fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String) fspanEnd k p "" = (k, "")-fspanEnd k p xxs -    = assert_total $ +fspanEnd k p xxs+    = assert_total $       let x = prim__strHead xxs           xs = prim__strTail xxs in           if p x then fspanEnd (S k) p xs@@ -195,14 +206,14 @@ -- Faster version of 'span' from the prelude (avoids unpacking) export fspan : (Char -> Bool) -> String -> (String, String)-fspan p xs +fspan p xs     = let (end, rest) = fspanEnd 0 p xs in           (substr 0 end xs, rest)  tokenise : (line : Int) -> (col : Int) ->-           List (TokenData a) -> TokenMap a -> +           List (TokenData a) -> TokenMap a ->            StrLen -> (List (TokenData a), (Int, Int, StrLen))-tokenise line col acc tmap str +tokenise line col acc tmap str     = case getFirstToken tmap str of            Just (tok, line', col', rest) =>            -- assert total because getFirstToken must consume something@@ -213,7 +224,7 @@     countNLs str = List.length (filter (== '\n') str)      getCols : String -> Int -> Int-    getCols x c +    getCols x c          = case fspan (/= '\n') (reverse x) of                 (incol, "") => c + cast (length incol)                 (incol, _) => cast (length incol)@@ -223,7 +234,7 @@     getFirstToken ((lex, fn) :: ts) str         = case takeToken lex str of                Just (tok, rest) => Just (MkToken line col (fn tok),-                                         line + cast (countNLs (unpack tok)), +                                         line + cast (countNLs (unpack tok)),                                          getCols tok col, rest)                Nothing => getFirstToken ts str @@ -235,4 +246,3 @@ lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String)) lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in                    (ts, (l, c, getString str'))-

@@ -3,7 +3,7 @@ %default total  -- TODO: Add some primitives for helping with error messages.--- e.g. perhaps set a string to state what we're currently trying to +-- e.g. perhaps set a string to state what we're currently trying to -- parse, or to say what the next expected token is in words  ||| Description of a language's grammar. The `tok` parameter is the type@@ -26,14 +26,14 @@                 Grammar tok c1 a -> (a -> Grammar tok c2 b) ->                 Grammar tok (c1 || c2) b      Alt : {c1, c2 : Bool} ->-           Grammar tok c1 ty -> Grammar tok c2 ty -> +           Grammar tok c1 ty -> Grammar tok c2 ty ->            Grammar tok (c1 && c2) ty  public export inf : Bool -> Type -> Type inf True t = Inf t inf False t = t-  + ||| Sequence two grammars. If either consumes some input, the sequence is ||| guaranteed to consume some input. If the first one consumes input, the ||| second is allowed to be recursive (because it means some input has been@@ -44,11 +44,11 @@         Grammar tok (c1 || c2) b (>>=) {c1 = False} = SeqEmpty (>>=) {c1 = True} = SeqEat-    + ||| Give two alternative grammars. If both consume, the combination is ||| guaranteed to consume. export-(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty -> +(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->         Grammar tok (c1 && c2) ty (<|>) = Alt @@ -82,21 +82,21 @@ eof : Grammar tok False () eof = EOF -||| Commit to an alternative; if the current branch of an alternative +||| Commit to an alternative; if the current branch of an alternative ||| fails to parse, no more branches will be tried export commit : Grammar tok False () commit = Commit  data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where-     Failure : {xs : List tok} -> +     Failure : {xs : List tok} ->                (committed : Bool) ->                (err : String) -> (rest : List tok) -> ParseResult xs c ty      EmptyRes : (committed : Bool) ->                 (val : ty) -> (more : List tok) -> ParseResult more False ty      NonEmptyRes : (committed : Bool) ->                    (val : ty) -> (more : List tok) ->-                   ParseResult (x :: xs ++ more) c ty +                   ParseResult (x :: xs ++ more) c ty  weakenRes : {whatever, c : Bool} -> {xs : List tok} ->             ParseResult xs c ty -> ParseResult xs (whatever && c) ty@@ -105,13 +105,13 @@ weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more -shorter : (more : List tok) -> .(ys : List tok) -> +shorter : (more : List tok) -> .(ys : List tok) ->           LTE (S (length more)) (S (length (ys ++ more))) shorter more [] = lteRefl shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))  doParse : {c : Bool} ->-          (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) -> +          (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->           ParseResult xs c ty doParse com xs act with (sizeAccessible xs)   doParse com xs (Empty val) | sml = EmptyRes com val xs@@ -120,17 +120,17 @@   doParse com xs Commit | sml = EmptyRes True () xs    doParse com [] (Terminal f) | sml = Failure com "End of input" []-  doParse com (x :: xs) (Terminal f) | sml +  doParse com (x :: xs) (Terminal f) | sml         = maybe              (Failure com "Unrecognised token" (x :: xs))              (\a => NonEmptyRes com {xs=[]} a xs)              (f x)   doParse com [] EOF | sml = EmptyRes com () []-  doParse com (x :: xs) EOF | sml +  doParse com (x :: xs) EOF | sml         = Failure com "Expected end of input" (x :: xs)   doParse com [] (NextIs f) | sml = Failure com "End of input" []-  doParse com (x :: xs) (NextIs f) | sml -        = if f x +  doParse com (x :: xs) (NextIs f) | sml+        = if f x              then EmptyRes com x (x :: xs)              else Failure com "Unrecognised token" (x :: xs)   doParse com xs (Alt x y) | sml with (doParse False xs x | sml)@@ -140,19 +140,19 @@                then Failure com msg ts                else weakenRes (doParse False xs y | sml)     -- Successfully parsed the first option, so use the outer commit flag-    doParse com xs (Alt x y) | sml | (EmptyRes _ val xs) +    doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)           = EmptyRes com val xs-    doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more) +    doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)           = NonEmptyRes com val more   doParse com xs (SeqEmpty act next) | (Access morerec)           = case doParse com xs act | Access morerec of                  Failure com msg ts => Failure com msg ts-                 EmptyRes com val xs => +                 EmptyRes com val xs =>                        case doParse com xs (next val) | (Access morerec) of                             Failure com' msg ts => Failure com' msg ts                             EmptyRes com' val xs => EmptyRes com' val xs                             NonEmptyRes com' val more => NonEmptyRes com' val more-                 NonEmptyRes {x} {xs=ys} com val more => +                 NonEmptyRes {x} {xs=ys} com val more =>                        case (doParse com more (next val) | morerec _ (shorter more ys)) of                             Failure com' msg ts => Failure com' msg ts                             EmptyRes com' val _ => NonEmptyRes com' val more@@ -160,13 +160,13 @@                                  rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in                                          NonEmptyRes com' val more'   doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)-    doParse com xs (SeqEat act next) | sml | Failure com' msg ts +    doParse com xs (SeqEat act next) | sml | Failure com' msg ts          = Failure com' msg ts-    doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more) +    doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)          = case doParse com' more (next val) | morerec _ (shorter more ys) of                 Failure com' msg ts => Failure com' msg ts                 EmptyRes com' val _ => NonEmptyRes com' val more-                NonEmptyRes {x=x1} {xs=xs1} com' val more' => +                NonEmptyRes {x=x1} {xs=xs1} com' val more' =>                      rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in                              NonEmptyRes com' val more'   -- This next line is not strictly necessary, but it stops the coverage@@ -180,7 +180,7 @@ ||| returns a pair of the parse result and the unparsed tokens (the remaining ||| input). export-parse : (xs : List tok) -> (act : Grammar tok c ty) -> +parse : (xs : List tok) -> (act : Grammar tok c ty) ->         Either (ParseError tok) (ty, List tok) parse xs act     = case doParse False xs act of@@ -190,7 +190,7 @@  ||| Parse one or more things export-some : Grammar tok True a -> +some : Grammar tok True a ->        Grammar tok True (List a) some p = do x <- p             (do xs <- some p@@ -198,14 +198,14 @@  ||| Parse zero or more things (may match the empty input) export-many : Grammar tok True a -> +many : Grammar tok True a ->        Grammar tok False (List a) many p = some p      <|> pure []  ||| Parse one or more things, separated by another thing export-sepBy1 : Grammar tok True () -> Grammar tok True a -> +sepBy1 : Grammar tok True () -> Grammar tok True a ->          Grammar tok True (List a) sepBy1 sep p = do x <- p                   (do sep@@ -215,7 +215,7 @@ ||| Parse zero or more things, separated by another thing. May ||| match the empty input. export-sepBy : Grammar tok True () -> Grammar tok True a -> +sepBy : Grammar tok True () -> Grammar tok True a ->         Grammar tok False (List a) sepBy sep p = sepBy1 sep p <|> pure [] @@ -227,3 +227,44 @@ optional p def = p <|> pure def  +||| Parse an instance of `p` that is between `left` and `right`.+export+between : (left  : Grammar tok True ())+       -> (right : Grammar tok True ())+       -> (p     : Grammar tok True a)+       -> Grammar tok True a+between left right contents = do+   left+   res <- contents+   right+   pure res++||| Parse one or more instances of `p` separated by `s`, returning the+||| parsed items and proof the resulting list is non-empty.+export+sepBy1' : (sep : Grammar tok True ())+       -> (p   : Grammar tok True a)+       -> Grammar tok True (xs : List a ** NonEmpty xs)+sepBy1' sep p+    = do x <- p+         (do sep+             xs <- sepBy1 sep p+             pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)++||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.+export+some' : (p : Grammar tok True a)+     -> Grammar tok True (xs : List a ** NonEmpty xs)+some' p = do+   x <- p+   (do xs <- some p+       pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)+++||| Optionally parse a thing. If the grammar provides a default use `optional` instead.+export+maybe : Grammar tok True a+     -> Grammar tok False (Maybe a)+maybe p =+      (do res <- p; pure $ Just res)+  <|> pure Nothing

@@ -69,8 +69,8 @@ tick : Doc tick = char '`' -tilda : Doc-tilda = char '~'+tilde : Doc+tilde = char '~'  hash : Doc hash = char '#'

@@ -128,10 +128,10 @@ showPrettyDoc doc = showPrettyDocS doc ""   where     showPrettyDocS : (doc : PrettyDoc) -> (acc : String) -> String-    showPrettyDocS Empty               = id-    showPrettyDocS (Chara c rest)      = strCons c . showPrettyDocS rest-    showPrettyDocS (Text len str rest) = (str ++) . showPrettyDocS rest-    showPrettyDocS (Line lvl rest)     = (('\n' `strCons` indentation lvl) ++) . showPrettyDocS rest+    showPrettyDocS Empty               acc = acc+    showPrettyDocS (Chara c rest)      acc = strCons c (showPrettyDocS rest acc)+    showPrettyDocS (Text len str rest) acc = str ++ (showPrettyDocS rest acc)+    showPrettyDocS (Line lvl rest)     acc = (strCons '\n' (indentation lvl)) ++ showPrettyDocS rest acc  private fits : (w : Int) -> (x : PrettyDoc) -> Bool

@@ -21,12 +21,12 @@ -- Convert to `List Bits8` -------------------------------------------------------------------------------- -||| Convert to list of `Bits8` with the most signficant byte at the+||| Convert to list of `Bits8` with the most significant byte at the ||| head. b8ToBytes : Bits8 -> List Bits8 b8ToBytes b = [b] -||| Convert to list of `Bits8` with the most signficant byte at the+||| Convert to list of `Bits8` with the most significant byte at the ||| head. b16ToBytes : Bits16 -> List Bits8 b16ToBytes b =@@ -34,7 +34,7 @@   , prim__truncB16_B8 b   ] -||| Convert to list of `Bits8` with the most signficant byte at the+||| Convert to list of `Bits8` with the most significant byte at the ||| head. b32ToBytes : Bits32 -> List Bits8 b32ToBytes b =@@ -44,7 +44,7 @@   , prim__truncB32_B8 b   ] -||| Convert to list of `Bits8` with the most signficant byte at the+||| Convert to list of `Bits8` with the most significant byte at the ||| head. b64ToBytes : Bits64 -> List Bits8 b64ToBytes b =

@@ -378,7 +378,7 @@ scanl f q []      = [q] scanl f q (x::xs) = q :: scanl f (f q x) xs -||| The scanl1 function is a variant of scanl that doesn't require an explicit +||| The scanl1 function is a variant of scanl that doesn't require an explicit ||| starting value. ||| It assumes the first element of the list to be the starting value and then ||| starts the fold with the element following it.@@ -854,6 +854,10 @@ -------------------------------------------------------------------------------- -- Properties --------------------------------------------------------------------------------++||| (::) is injective+consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)+consInjective Refl = (Refl, Refl)  ||| The empty list is a right identity for append. appendNilRightNeutral : (l : List a) ->

@@ -225,13 +225,16 @@         countPi (RBind _ (Pi _ _) body) = S (countPi body)         countPi _ = Z +||| A helper to extract the type representation for term.+getTTType : Raw -> Elab TT+getTTType r = snd <$> check !getEnv r  ||| Split a pair into its projections, binding them in the context ||| with the supplied names. A special case of Coq's `inversion`. both : Raw -> TTName -> TTName -> Elab () both tm n1 n2 =     do -- We don't know that the term is canonical, so let-bind projections applied to it-       (A, B) <- isPairTy (snd !(check !getEnv tm))+       (A, B) <- isPairTy !(getTTType tm)        remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve        remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve   where@@ -253,7 +256,6 @@        try (unproduct (Var n1))        try (unproduct (Var n2)) - ||| A special-purpose tactic that attempts to solve a goal using ||| `Refl`. This is useful for ensuring that goals in fact are trivial ||| when developing or testing other tactics; otherwise, consider@@ -268,3 +270,47 @@                 , NamePart `{reflexivity}                 , TextPart "is not applicable."                 ]++||| Attempt to swap the sides of equality in a goal. If the goal is `x = y`,+||| after the invocation the focus will be on a hole of type `y = x`.+symmetry : Elab ()+symmetry =+    do [_,_,_,_,res] <- apply (Var `{{sym}}) [True, True, True, True, False]+          | _ => fail [TextPart "Failed while applying", NamePart `{symmetry}]+       solve+       focus res++||| Swap the sides of an equality, saving the result in a `let`-binding.+||| Returns the generated name.+|||+||| @ t the equality proof to swap+||| @ hint a hint to use for generating the variable name for the result+symmetryAs : (t : Raw) -> (hint : String) -> Elab TTName+symmetryAs t hint =+    case !(getTTType t) of+      `((=) {A=~A} {B=~B} ~l ~r) =>+        do af <- forget A+           bf <- forget B+           lf <- forget l+           rf <- forget r+           let ts = the Raw $ `(sym {a=~af} {b=~bf} {left=~lf} {right=~rf} ~t)+           n <- gensym hint+           letbind n !(forget !(getTTType ts)) ts+           pure n+      tt => fail [TermPart tt, TextPart "is not an equality"]++||| Apply a function term to an argument term, saving the result in a+||| `let`-binding. Returns the generated name.+|||+||| @ f the function to apply+||| @ x the term to apply to+||| @ hint a hint to use for generating the variable name for the result+applyAs : (f : Raw) -> (x : Raw) -> (hint : String) -> Elab TTName+applyAs f x hint =+    case !(getTTType f) of+      `(~xty -> ~yty) =>+         do let fx = RApp f x+            n <- gensym hint+            letbind n !(forget !(getTTType fx)) fx+            pure n+      ftt => fail [TermPart ftt, TextPart "is not a function"]

@@ -460,6 +460,11 @@     case CT_STRING:         printf("STR[%s]", v->info.str.str);         break;+    case CT_STROFFSET:+        printf("OFFSET[");+        dumpVal((VAL)(v->info.str_offset->str));+        printf("]");+        break;     case CT_FWD:         printf("CT_FWD ");         dumpVal((VAL)(v->info.ptr));@@ -591,15 +596,16 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {     char *rs = GETSTR(r);     char *ls = GETSTR(l);-    // dumpVal(l);-    // printf("\n");-    Closure* cl = allocate(sizeof(Closure) + GETSTRLEN(l) + GETSTRLEN(r) + 1, 0);+    int llen = GETSTRLEN(l);+    int rlen = GETSTRLEN(r);++    Closure* cl = allocate(sizeof(Closure) + llen + rlen + 1, 0);     SETTY(cl, CT_STRING);     cl->info.str.str = (char*)cl + sizeof(Closure);     strcpy(cl->info.str.str, ls);     strcat(cl->info.str.str, rs); -    cl->info.str.len = GETSTRLEN(l) + GETSTRLEN(r);+    cl->info.str.len = llen + rlen;     return cl; } 

@@ -9,10 +9,17 @@     mkdir $RUNIDRIS_DIR     chmod 700 $RUNIDRIS_DIR fi-TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`"++OS=`uname -s`+case $OS in+    OpenBSD ) TEMP_NAME="runidris-`sha1 -q $1`" ;;+          * ) TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`" ;;+esac+ FP="$RUNIDRIS_DIR/$TEMP_NAME"+cp "$1" "$FP.idr" # idris won't compile the script unless it ends in .idr if [ ! -e $FP ]; then-    "${IDRIS:-idris}" $1 --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP+    "${IDRIS:-idris}" "$FP.idr" --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP fi shift "$FP" "$@"

@@ -9,10 +9,17 @@     mkdir $RUNIDRIS_DIR     chmod 700 $RUNIDRIS_DIR fi-TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`.js"++OS=`uname -s`+case $OS in+    OpenBSD ) TEMP_NAME="runidris-`sha1 -q $1`" ;;+          * ) TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`" ;;+esac+ FP="$RUNIDRIS_DIR/$TEMP_NAME"-if [ ! -e $FP ]; then-    "${IDRIS:-idris}" --codegen node --ibcsubdir "$RUNIDRIS_DIR" -i "." $1 -o $FP+cp "$1" "$FP.idr" # idris won't compile the script unless it ends in .idr+if [ ! -e "$FP.js" ]; then+    "${IDRIS:-idris}" --codegen node --ibcsubdir "$RUNIDRIS_DIR" -i "." "$FP.idr" -o "$FP.js" fi shift-node "$FP" "$@"+node "$FP.js" "$@"

@@ -9,7 +9,7 @@  module IRTS.CodegenC (codegenC) where -import Idris.AbsSyntax hiding (getBC)+import Idris.AbsSyntax import Idris.Core.TT import IRTS.Bytecode import IRTS.CodegenCommon@@ -21,12 +21,10 @@ import Util.System  import Control.Monad-import Control.Monad-import Control.Monad.RWS import Data.Bits import Data.Char-import Data.List (find, intercalate, nubBy, partition)-import qualified Data.Text as T+import Data.List (intercalate, nubBy)+import Debug.Trace import Numeric import System.Directory import System.Exit@@ -34,8 +32,6 @@ import System.IO import System.Process -import Debug.Trace- codegenC :: CodeGenerator codegenC ci = do codegenC' (simpleDecls ci)                            (outputFile ci)@@ -70,9 +66,7 @@          let bc = map toBC defs          let wrappers = genWrappers bc          let h = concatMap toDecl (map fst bc)-         let (state, cc) = execRWS (generateSrc bc) 0-                                         (CS { fnName = Nothing,-                                                level = 1 })+         let cc = concatMap (uncurry toC) bc          let hi = concatMap ifaceC (concatMap getExp exports)          d <- getIdrisCRTSDir          mprog <- readFile (d </> "idris_main" <.> "c")@@ -142,17 +136,12 @@ toDecl :: Name -> String toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n" -generateSrc :: [(Name, [BC])] -> RWS Int String CState ()-generateSrc bc = mapM_ toC bc--toC :: (Name, [BC]) -> RWS Int String CState ()-toC (f, code) = do-    modify (\s -> s { fnName = Just f })-    s <- get-    tell $ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n"-    tell $  indent (level s) ++ "INITFRAME;\n"-    bcc code-    tell $ "}\n\n"+toC :: Name -> [BC] -> String+toC f code+    = -- "/* " ++ show code ++ "*/\n\n" +++      "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" +++                 indent 1 ++ "INITFRAME;\n" +++                 concatMap (bcc 1) code ++ "}\n\n"  showCStr :: String -> String showCStr s = '"' : foldr ((++) . showChar) "\"" s@@ -188,27 +177,15 @@                  2 -> s                  _ -> error $ "Can't happen: String of invalid length " ++ show s -data CState = CS {-    fnName :: Maybe Name,-    level :: Int-}---bcc :: [BC] -> RWS Int String CState ()-bcc [] = return ()-bcc ((ASSIGN l r):xs) = do-    i <- get-    tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"-    bcc xs-bcc ((ASSIGNCONST l c):xs) = do-    i <- get-    tell $ indent (level i) ++ creg l ++ " = " ++ mkConst c ++ ";\n"-    bcc xs+bcc :: Int -> BC -> String+bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"+bcc i (ASSIGNCONST l c)+    = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"   where     mkConst (I i) = "MKINT(" ++ show i ++ ")"     mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"                    | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"-    mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"+    mkConst (Fl f) = "MKFLOAT(vm, " ++ (map toUpper $ show f) ++ ")"     mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"     mkConst (Str s) = "MKSTR(vm, " ++ showCStr s ++ ")"     mkConst (B8  x) = "idris_b8const(vm, "  ++ show x ++ "U)"@@ -221,21 +198,16 @@     mkConst c | isTypeConst c = "MKINT(42424242)"     mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented" -bcc ((UPDATE l r):xs) = do-    i <- get-    tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"-    bcc xs-bcc ((MKCON l loc tag []):xs) | tag < 256 = do-    i <- get-    tell $ indent (level i) ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"-    bcc xs-bcc ((MKCON l loc tag args):xs) = do-    i <- get-    let tab = indent (level i)-    tell $ tab ++ alloc loc tag ++-           tab ++ setArgs 0 args ++ "\n" ++-           tab ++ creg l ++ " = " ++ creg Tmp ++ ";\n"-    bcc xs+bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"+bcc i (MKCON l loc tag []) | tag < 256+    = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"+bcc i (MKCON l loc tag args)+    = indent i ++ alloc loc tag +++      indent i ++ setArgs 0 args ++ "\n" +++      indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"++--         "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " +++--         show (length args) ++ concatMap showArg args ++ ");\n"   where showArg r = ", " ++ creg r         setArgs i [] = ""         setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++@@ -247,94 +219,52 @@             = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++                     show (length args) ++ ");\n" -bcc ((PROJECT l loc a):xs) = do-    i <- get-    tell $ indent (level i) ++ "PROJECT(vm, " ++ creg l ++ ", "-                ++ show loc ++ ", " ++ show a ++ ");\n"-    bcc xs-bcc ((PROJECTINTO r t idx):xs) = do-    i <- get-    tell $ indent (level i) ++ creg r ++ " = GETARG(" ++ creg t-            ++ ", " ++ show idx ++ ");\n"-    bcc xs-bcc ((CASE True r code def):xs)-    | length code < 4 = do-        showCases def code-        bcc xs+bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc +++                                      ", " ++ show a ++ ");\n"+bcc i (PROJECTINTO r t idx)+    = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"+bcc i (CASE True r code def)+    | length code < 4 = showCase i def code   where-    showCode bc = do-        w <- getBC bc xs-        i <- get-        tell $ "{\n" ++ w ++ indent (level i) ++ "}\n"+    showCode :: Int -> [BC] -> String+    showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc +++                    indent i ++ "}\n" -    showCases Nothing [(t, c)] = do-        i <- get-        tell $ indent (level i)-        showCode c-    showCases (Just def) [] = do-        i <- get-        tell $ indent (level i)-        showCode def-    showCases def ((t, c) : cs) = do-        i <- get-        tell $ indent (level i) ++ "if (CTAG(" ++ creg r ++ ") == "-               ++ show t ++ ") "-        showCode c-        tell $ indent (level i) ++ "else\n"-        showCases def cs+    showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String+    showCase i Nothing [(t, c)] = indent i ++ showCode i c+    showCase i (Just def) [] = indent i ++ showCode i def+    showCase i def ((t, c) : cs)+        = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c+           ++ indent i ++ "else\n" ++ showCase i def cs -bcc ((CASE safe r code def):xs) = do-    i <- get-    tell $ indent (level i) ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n"-    mapM showCase code-    showDef def-    tell $ indent (level i) ++ "}\n"-    bcc xs+bcc i (CASE safe r code def)+    = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" +++      concatMap (showCase i) code +++      showDef i def +++      indent i ++ "}\n"   where     ctag True = "CTAG"     ctag False = "TAG" -    showCase (t, bc) = do-        w <- getBC bc xs-        is <- get-        let i = level is-        tell $ indent i ++ "case " ++ show t ++ ":\n"-                ++ w ++ indent (i + 1) ++ "break;\n"-    showDef Nothing = return $ ()-    showDef (Just c) = do-        w <- getBC c xs-        is <- get-        let i = level is-        tell $ indent i ++ "default:\n" ++ w ++ indent (i + 1) ++ "break;\n"--bcc ((CONSTCASE r code def):xs)+    showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"+                         ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"+    showDef i Nothing = ""+    showDef i (Just c) = indent i ++ "default:\n"+                         ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"+bcc i (CONSTCASE r code def)    | intConsts code-     = do-         is <- get-         let i = level is-         codes <- mapM getCode code-         defs <- showDefS def-         tell $ concatMap (iCase i (creg r)) codes-         tell $ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"-         bcc xs+--      = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" +++--        concatMap (showCase i) code +++--        showDef i def +++--        indent i ++ "}\n"+     = concatMap (iCase (creg r)) code +++       indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"    | strConsts code-     = do-         is <- get-         let i = level is-         codes <- mapM getCode code-         defs <- showDefS def-         tell $ concatMap (strCase i ("GETSTR(" ++ creg r ++ ")")) codes-             ++ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"-         bcc xs+     = concatMap (strCase ("GETSTR(" ++ creg r ++ ")")) code +++       indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"    | bigintConsts code-     = do-         is <- get-         let i = level is-         codes <- mapM getCode code-         defs <- showDefS def-         tell $ concatMap (biCase i (creg r)) codes ++-            indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"-         bcc xs+     = concatMap (biCase (creg r)) code +++       indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"    | otherwise = error $ "Can't happen: Can't compile const case " ++ show code   where     intConsts ((I _, _ ) : _) = True@@ -351,118 +281,71 @@     strConsts ((Str _, _ ) : _) = True     strConsts _ = False -    getCode (x, code) = do-        c <- getBC code xs-        return (x, c)--    strCase i sv (s, bc) =+    strCase sv (s, bc) =         indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++-            bc ++ indent i ++ "} else\n"-    biCase i bv (BI b, bc) =+           concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    biCase bv (BI b, bc) =         indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"-           ++  bc ++ indent i ++ "} else\n"-    iCase i v (I b, bc) =+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    iCase v (I b, bc) =         indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"-           ++ bc ++ indent i ++ "} else\n"-    iCase i v (Ch b, bc) =+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    iCase v (Ch b, bc) =         indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"-           ++ bc ++ indent i ++ "} else\n"-    iCase i v (B8 w, bc) =+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    iCase v (B8 w, bc) =         indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ bc ++ indent i ++ "} else\n"-    iCase i v (B16 w, bc) =+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    iCase v (B16 w, bc) =         indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ bc ++ indent i ++ "} else\n"-    iCase i v (B32 w, bc) =+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    iCase v (B32 w, bc) =         indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ bc ++ indent i ++ "} else\n"-    iCase i v (B64 w, bc) =+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    iCase v (B64 w, bc) =         indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"-           ++ bc ++ indent i ++ "} else\n"--    showDefS Nothing = return ""-    showDefS (Just c) = getBC c xs+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"+    showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"+                         ++ concatMap (bcc (i+1)) bc +++                            indent (i + 1) ++ "break;\n"+    showDef i Nothing = ""+    showDef i (Just c) = indent i ++ "default:\n"+                         ++ concatMap (bcc (i+1)) c +++                            indent (i + 1) ++ "break;\n"+    showDefS i Nothing = ""+    showDefS i (Just c) = concatMap (bcc (i+1)) c -bcc (CALL n:xs) = do-    i <- get-    tell $ indent (level i) ++ "CALL(" ++ cname n ++ ");\n"-    bcc xs-bcc (TAILCALL n:xs) = do-    i <- get-    tell $ indent (level i) ++ "TAILCALL(" ++ cname n ++ ");\n"-    bcc xs-bcc ((SLIDE n):xs) = do-    i <- get-    tell $ indent (level i) ++ "SLIDE(vm, " ++ show n ++ ");\n"-    bcc xs-bcc (REBASE:xs) = do-    i <- get-    tell $ indent (level i)++ "REBASE;\n"-    bcc xs-bcc ((RESERVE 0):xs) = bcc xs-bcc ((RESERVE n):xs) = do-    i <- get-    tell $ indent (level i) ++ "RESERVE(" ++ show n ++ ");\n"-    bcc xs-bcc ((ADDTOP 0):xs) = bcc xs-bcc ((ADDTOP n):xs) = do-    i <- get-    tell $ indent (level i) ++ "ADDTOP(" ++ show n ++ ");\n"-    bcc xs-bcc ((TOPBASE n):xs) = do-    i <- get-    tell $ indent (level i) ++ "TOPBASE(" ++ show n ++ ");\n"-    bcc xs-bcc ((BASETOP n):xs) = do-    i <- get-    tell $ indent (level i) ++ "BASETOP(" ++ show n ++ ");\n"-    bcc xs-bcc (STOREOLD:xs) = do-    i <- get-    tell $ indent (level i) ++ "STOREOLD;\n"-    bcc xs-bcc ((OP l fn args):xs) = do-    i <- get-    tell $ indent (level i) ++ doOp (creg l ++ " = ") fn args ++ ";\n"-    bcc xs-bcc ((FOREIGNCALL l rty (FStr fn@('&':name)) []):xs) = do-    i <- get-    tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"-    bcc xs-bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%wrapper"-      = do-          i <- get-          tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")+bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"+bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"+bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"+bcc i REBASE = indent i ++ "REBASE;\n"+bcc i (RESERVE 0) = ""+bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"+bcc i (ADDTOP 0) = ""+bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"+bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"+bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"+bcc i STOREOLD = indent i ++ "STOREOLD;\n"+bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"+bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])+      = indent i +++        c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"+bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"+      = indent i +++        c_irts (toFType rty) (creg l ++ " = ")             ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"-          bcc zs-bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%dynamic"-      = do-          i <- get-          tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")+bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"+      = indent i ++ c_irts (toFType rty) (creg l ++ " = ")             ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++              "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"-          bcc zs-bcc ((FOREIGNCALL l rty (FStr fn) args):xs) = do-    i <- get-    tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")-                 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"-    bcc xs-bcc ((FOREIGNCALL l rty _ args):_) = error "Foreign Function calls cannot be partially applied, without being inlined."-bcc ((NULL r):xs) = do-    i <- get-    tell $ indent (level i) ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed-    bcc xs-bcc ((ERROR str):xs) = do-    i <- get-    tell $ indent (level i) ++ "fprintf(stderr, "-        ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"-    bcc xs+bcc i (FOREIGNCALL l rty (FStr fn) args)+      = indent i +++        c_irts (toFType rty) (creg l ++ " = ")+                   (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"+bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."+bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed+bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n" -- bcc i c = error (show c) -- indent i ++ "// not done yet\n"--getBC code xs = do-    i <- get-    let (a, s, w) = runRWS (bcc code) 0 (i { level = level i + 1 })-    return w  fcall (t, arg) = irts_c (toFType t) (creg arg) -- Deconstruct the Foreign type in the defunctionalised expression and build

@@ -63,6 +63,8 @@                              Nothing -> []                              Just t -> freeNames t +        logCodeGen 1 "Running Erasure Analysis"+        iReport 3 "Running Erasure Analysis"         reachableNames <- performUsageAnalysis                               (rootNames ++ getExpNames exports)         maindef <- case mtm of

@@ -16,6 +16,8 @@ import Control.DeepSeq (($!!)) import Control.Monad (liftM2) import Data.Binary+import Data.Binary.Get+import Data.Binary.Put import qualified Data.Text as T import qualified Data.Text.Encoding as E import Data.Vector.Binary@@ -400,7 +402,7 @@                 BI x1 -> do putWord8 1                             put x1                 Fl x1 -> do putWord8 2-                            put x1+                            putDoublele x1                 Ch x1 -> do putWord8 3                             put x1                 Str x1 -> do putWord8 4@@ -427,7 +429,7 @@                            return (I x1)                    1 -> do x1 <- get                            return (BI x1)-                   2 -> do x1 <- get+                   2 -> do x1 <- getDoublele                            return (Fl x1)                    3 -> do x1 <- get                            return (Ch x1)

@@ -29,20 +29,6 @@ import Network.Socket (PortNumber)  -- These types don't have Generic instances-instance NFData CT.Options where-  rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()--instance NFData CT.ListType where-  rnf (CT.Bullet c) = rnf c `seq` ()-  rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()--instance NFData CT.CodeAttr where-  rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()--instance NFData CT.NumWrapper where-  rnf CT.PeriodFollowing = ()-  rnf CT.ParenFollowing = ()- instance NFData DynamicLib where     rnf (Lib x _) = rnf x `seq` () 

@@ -1,6 +1,6 @@ {-| Module      : Idris.Erasure-Description : Utilities to erase irrelevant stuff.+Description : Utilities to erase stuff not necessary for runtime. Copyright   : License     : BSD3 Maintainer  : The Idris Community.@@ -145,10 +145,54 @@         fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]         warn = logErasure 0 +type Constraint = (Cond, DepSet)+ -- | Find the minimal consistent usage by forward chaining.+--+-- We use a cleverer implementation that:+-- 1. First transforms Deps into a collection of numbered constraints+-- 2. For each node, we remember the numbers of constraints+--    that contain that node among their preconditions.+-- 3. When performing forward chaining, we perform unit propagation+--    only on the relevant constraints, not all constraints.+--+-- Typical numbers from the current version of Blodwen:+-- * 56 iterations until fixpoint+-- * out of 20k constraints total, 5-1000 are relevant per iteration minimalUsage :: Deps -> (Deps, (Set Name, UseMap))-minimalUsage = second gather . forwardChain+minimalUsage deps+    = fromNumbered *** gather+    $ forwardChain (index numbered) seedDeps seedDeps numbered   where+    numbered = toNumbered deps++    -- The initial solution. Consists of nodes that are+    -- reachable immediately, without any preconditions.+    seedDeps :: DepSet+    seedDeps = M.unionsWith S.union [ds | (cond, ds) <- IM.elems numbered, S.null cond]++    toNumbered :: Deps -> IntMap Constraint+    toNumbered = IM.fromList . zip [0..] . M.toList++    fromNumbered :: IntMap Constraint -> Deps+    fromNumbered = IM.foldr addConstraint M.empty+      where+        addConstraint (ns, vs) = M.insertWith (M.unionWith S.union) ns vs++    -- Build an index that maps every node to the set of constraints+    -- where the node appears among the preconditions.+    index :: IntMap Constraint -> Map Node IntSet+    index = IM.foldrWithKey (+            -- for each clause (i. ns --> _ds)+            \i (ns, _ds) ix -> foldr (+                -- for each node `n` in `ns`+                \n ix' -> M.insertWith IS.union n (IS.singleton i) ix'+              ) ix (S.toList ns)+        ) M.empty++    -- Convert a solution of constraints into:+    -- 1. the list of names used in the program+    -- 2. the list of arguments used, together with their reasons     gather :: DepSet -> (Set Name, UseMap)     gather = foldr ins (S.empty, M.empty) . M.toList        where@@ -156,17 +200,81 @@         ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)         ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap) -forwardChain :: Deps -> (Deps, DepSet)-forwardChain deps-    | Just trivials <- M.lookup S.empty deps-        = (M.unionWith S.union trivials)-            `second` forwardChain (remove trivials . M.delete S.empty $ deps)-    | otherwise = (deps, M.empty)+-- | In each iteration, we find the set of nodes immediately reachable+-- from the current set of constraints, and then reduce the set of constraints+-- based on that knowledge.+--+-- In the implementation, this is phase-shifted. We first reduce the set+-- of constraints, given the newly reachable nodes from the previous iteration,+-- and then compute the set of currently reachable nodes.+-- Then we decide whether to iterate further.+forwardChain+    :: Map Node IntSet   -- ^ node index+    -> DepSet            -- ^ all reachable nodes found so far+    -> DepSet            -- ^ nodes reached in the previous iteration+    -> IntMap Constraint -- ^ numbered constraints+    -> (IntMap Constraint, DepSet)+forwardChain index solution previouslyNew constrs+    -- no newly reachable nodes, fixed point has been reached+    | M.null currentlyNew+    = (constrs, solution)++    -- some newly reachable nodes, iterate more+    | otherwise+    = forwardChain index+        (M.unionWith S.union solution currentlyNew)+        currentlyNew+        constrs'   where-    -- Remove the given nodes from the Deps entirely,-    -- possibly creating new empty Conds.-    remove :: DepSet -> Deps -> Deps-    remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)+    -- which constraints could give new results,+    -- given that `previouslyNew` has been derived in the last iteration+    affectedIxs = IS.unions [+        M.findWithDefault IS.empty n index+        | n <- M.keys previouslyNew+      ]++    -- traverse all (potentially) affected constraints, building:+    -- 1. a set of newly reached nodes+    -- 2. updated set of constraints where the previously+    --    reached nodes have been removed+    (currentlyNew, constrs')+        = IS.foldr+            (reduceConstraint $ M.keysSet previouslyNew)+            (M.empty, constrs)+            affectedIxs++    -- Update the pair (newly reached nodes, numbered constraint set)+    -- by reducing the constraint with the given number.+    reduceConstraint+        :: Set Node  -- ^ nodes reached in the previous iteration+        -> Int       -- ^ constraint number+        -> (DepSet, IntMap (Cond, DepSet))+        -> (DepSet, IntMap (Cond, DepSet))+    reduceConstraint previouslyNew i (news, constrs)+        | Just (cond, deps) <- IM.lookup i constrs+        = case cond S.\\ previouslyNew of+            cond'+                -- This constraint's set of preconditions has shrunk+                -- to the empty set. We can add its RHS to the set of newly+                -- reached nodes, and remove the constraint altogether.+                | S.null cond'+                -> (M.unionWith S.union news deps, IM.delete i constrs)++                -- This constraint's set of preconditions has shrunk+                -- so we need to overwrite the numbered slot+                -- with the updated constraint.+                | S.size cond' < S.size cond+                -> (news, IM.insert i (cond', deps) constrs)++                -- This constraint's set of preconditions hasn't changed+                -- so we do not do anything about it.+                | otherwise+                -> (news, constrs)++        -- Constraint number present in index but not found+        -- among the constraints. This happens more and more frequently+        -- as we delete constraints from the set.+        | otherwise = (news, constrs)  -- | Build the dependency graph, starting the depth-first search from -- a list of Names.

@@ -48,7 +48,7 @@ import System.FilePath  ibcVersion :: Word16-ibcVersion = 161+ibcVersion = 162  -- | When IBC is being loaded - we'll load different things (and omit -- different structures/definitions) depending on which phase we're in.

@@ -1,3 +1,4 @@+#recheck extra-deps next on resolver or cabal file change resolver: lts-9.0  packages:@@ -9,7 +10,8 @@     GMP: true  extra-deps:-  - libffi-0.1+  - binary-0.8.5.1+  - cheapskate-0.1.1  nix:   enable: false

@@ -65,7 +65,8 @@   where     ref = path </> "expected"     output = path </> "output"-    diff ref new = ["diff", "--strip-trailing-cr", "-u", new, ref]+    diff ref new | os == "openbsd" = ["diff", "-u", new, ref]+                 | otherwise = ["diff", "--strip-trailing-cr", "-u", new, ref]  -- Should always output a 3-charater string from a postive Int indexToString :: Int -> String

@@ -1,6 +1,10 @@ #include <stdio.h> #include <stdlib.h> +#ifdef __OpenBSD__+#include <sys/wait.h>+#endif+ void doSystem(const char cmd[]) {   printf("exit1: Executing cmd '%s'\n", cmd);   int exitStatus = system(cmd);

@@ -2,6 +2,10 @@  #include <stdlib.h> +#ifdef __OpenBSD__+#include <sys/wait.h>+#endif+ int WIFEXITED_(int status) {   return WIFEXITED(status); }