Some fixes for making tests work

- Fixing incremental compilation
- Bringing some changes in from Idris 2 (constant folding, buffers)
- Temporarily disable identity optimisation because it doesn't work yet,
  probably due to reversing argument order somewhere

libs/base/Data/Buffer.idr

@@ -40,6 +40,9 @@ newBuffer size
 --             else pure $ Just $ MkBuffer buf size 0
 
 
+------------------------------------------------------------------------
+-- BitsN primitives
+
 -- There is no endianness indication (LE/BE) for UInt8 since it is a single byte
 
 -- TODO: remove me when we remove the deprecated `setByte` in a future release
@@ -149,38 +152,85 @@ getBits64 : HasIO io => Buffer -> (offset : Int) -> io Bits64
 getBits64 buf offset
     = primIO (prim__getBits64 buf offset)
 
+------------------------------------------------------------------------
+-- IntN primitives
+
+-- There is no endianness indication (LE/BE) for Int8 since it is a single byte
+
+%foreign "scheme:blodwen-buffer-setint8"
+prim__setInt8 : Buffer -> (offset : Int) -> (val : Int8) -> PrimIO ()
+
+export %inline
+setInt8 : HasIO io => Buffer -> (offset : Int) -> (val : Int8) -> io ()
+setInt8 buf offset val
+    = primIO (prim__setInt8 buf offset val)
+
+%foreign "scheme:blodwen-buffer-getint8"
+prim__getInt8 : Buffer -> (offset : Int) -> PrimIO Int8
+
+export %inline
+getInt8 : HasIO io => Buffer -> (offset : Int) -> io Int8
+getInt8 buf offset
+    = primIO (prim__getInt8 buf offset)
+
 %foreign "scheme:blodwen-buffer-setint16"
          "RefC:setBufferInt16LE"
          "node:lambda:(buf,offset,value)=>buf.writeInt16LE(value, offset)"
-prim__setInt16 : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()
+prim__setInt16 : Buffer -> (offset : Int) -> (val : Int16) -> PrimIO ()
 
 export %inline
-setInt16 : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
+setInt16 : HasIO io => Buffer -> (offset : Int) -> (val : Int16) -> io ()
 setInt16 buf offset val
     = primIO (prim__setInt16 buf offset val)
 
+%foreign "scheme:blodwen-buffer-getint16"
+prim__getInt16 : Buffer -> (offset : Int) -> PrimIO Int16
+
+export %inline
+getInt16 : HasIO io => Buffer -> (offset : Int) -> io Int16
+getInt16 buf offset
+    = primIO (prim__getInt16 buf offset)
 
 
 %foreign "scheme:blodwen-buffer-setint32"
          "RefC:setBufferInt32LE"
          "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
-prim__setInt32 : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()
+prim__setInt32 : Buffer -> (offset : Int) -> (val : Int32) -> PrimIO ()
 
 export %inline
-setInt32 : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
+setInt32 : HasIO io => Buffer -> (offset : Int) -> (val : Int32) -> io ()
 setInt32 buf offset val
     = primIO (prim__setInt32 buf offset val)
 
 %foreign "scheme:blodwen-buffer-getint32"
          "RefC:getBufferInt32LE"
          "node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
-prim__getInt32 : Buffer -> (offset : Int) -> PrimIO Int
+prim__getInt32 : Buffer -> (offset : Int) -> PrimIO Int32
 
 export %inline
-getInt32 : HasIO io => Buffer -> (offset : Int) -> io Int
+getInt32 : HasIO io => Buffer -> (offset : Int) -> io Int32
 getInt32 buf offset
     = primIO (prim__getInt32 buf offset)
 
+%foreign "scheme:blodwen-buffer-setint64"
+prim__setInt64 : Buffer -> (offset : Int) -> (val : Int64) -> PrimIO ()
+
+export %inline
+setInt64 : HasIO io => Buffer -> (offset : Int) -> (val : Int64) -> io ()
+setInt64 buf offset val
+    = primIO (prim__setInt64 buf offset val)
+
+%foreign "scheme:blodwen-buffer-getint64"
+prim__getInt64 : Buffer -> (offset : Int) -> PrimIO Int64
+
+export %inline
+getInt64 : HasIO io => Buffer -> (offset : Int) -> io Int64
+getInt64 buf offset
+    = primIO (prim__getInt64 buf offset)
+
+------------------------------------------------------------------------
+-- Int (backend-dependent: 64 on scheme, refc, and 32 on js)
+
 %foreign "scheme:blodwen-buffer-setint"
          "RefC:setBufferInt64LE"
          "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
@@ -201,6 +251,9 @@ getInt : HasIO io => Buffer -> (offset : Int) -> io Int
 getInt buf offset
     = primIO (prim__getInt buf offset)
 
+------------------------------------------------------------------------
+-- Double
+
 %foreign "scheme:blodwen-buffer-setdouble"
          "RefC:setBufferDouble"
          "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, offset)"
@@ -221,6 +274,83 @@ getDouble : HasIO io => Buffer -> (offset : Int) -> io Double
 getDouble buf offset
     = primIO (prim__getDouble buf offset)
 
+------------------------------------------------------------------------
+-- Bool
+
+export
+setBool : HasIO io => Buffer -> (offset : Int) -> (val : Bool) -> io ()
+setBool buf offset val = setBits8 buf offset (ifThenElse val 0 1)
+
+export
+getBool : HasIO io => Buffer -> (offset : Int) -> io Bool
+getBool buf offset = (0 ==) <$> getBits8 buf offset
+
+------------------------------------------------------------------------
+-- Arbitrary precision nums
+
+||| setNat returns the end offset
+export
+setNat : HasIO io => Buffer -> (offset : Int) -> (val : Nat) -> io Int
+setNat buf offset val
+  = do let limbs = toLimbs (cast val)
+       let len = foldl (const . (1+)) 0 limbs -- tail recursive length
+       setInt64 buf offset len
+       setLimbs (offset + 8) limbs
+
+  where
+
+  toLimbs : Integer -> List Bits32
+  toLimbs 0 = []
+  toLimbs (-1) = [-1]
+  toLimbs x = fromInteger (prim__and_Integer x 0xffffffff) ::
+              toLimbs (assert_smaller x (prim__shr_Integer x 32))
+
+  setLimbs : (offset : Int) -> List Bits32 -> io Int
+  setLimbs offset [] = pure offset
+  setLimbs offset (limb :: limbs)
+    = do setBits32 buf offset limb
+         setLimbs (offset + 4) limbs
+
+||| getNat returns the end offset
+export
+getNat : HasIO io => Buffer -> (offset : Int) -> io (Int, Nat)
+getNat buf offset
+  = do len <- getInt64 buf offset
+       when (len < 0) $ assert_total $ idris_crash "corrupt Nat"
+       limbs <- getLimbs [<] (offset + 8) len
+       pure (offset + 8 + 4 * cast len, cast $ fromLimbs limbs)
+
+  where
+
+  fromLimbs : List Bits32 -> Integer
+  fromLimbs [] = 0
+  fromLimbs (x :: xs) = cast x + prim__shl_Integer (fromLimbs xs) 32
+
+  getLimbs : SnocList Bits32 -> (offset : Int) -> (len : Int64) -> io (List Bits32)
+  getLimbs acc offset 0 = pure (acc <>> [])
+  getLimbs acc offset len
+    = do limb <- getBits32 buf offset
+         getLimbs (acc :< limb) (offset + 4) (assert_smaller len (len -1))
+
+||| setInteger returns the end offset
+export
+setInteger : HasIO io => Buffer -> (offset : Int) -> (val : Integer) -> io Int
+setInteger buf offset val = if val < 0
+  then do setBool buf offset True
+          setNat buf (offset + 1) (cast (- val))
+  else do setBool buf offset False
+          setNat buf (offset + 1) (cast val)
+
+||| getInteger returns the end offset
+export
+getInteger : HasIO io => Buffer -> (offset : Int) -> io (Int, Integer)
+getInteger buf offset
+  = do b <- getBool buf offset
+       map (ifThenElse b negate id . cast) <$> getNat buf (offset + 1)
+
+------------------------------------------------------------------------
+-- String
+
 -- Get the length of a string in bytes, rather than characters
 export
 %foreign "scheme:blodwen-stringbytelen"

src/Compiler/CompileExpr.idr

@@ -749,7 +749,10 @@ toCDef n ty erased (Function fi _ tree _)
     toLam _ d = d
 toCDef n ty _ (ExternDef arity)
     = let (ns ** args) = mkArgList 0 arity in
-          pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
+          -- Reverse the args since we build them in the wrong order (most
+          -- recently bound lambda is last argument to primitive)
+          pure $ MkFun _ (CExtPrim emptyFC !(getFullName n)
+                             (reverse (map toArgExp (getVars args))))
   where
     toArgExp : (Var ns) -> CExp ns
     toArgExp (MkVar p) = CLocal emptyFC p

src/Compiler/Inline.idr

@@ -602,7 +602,7 @@ compileAndInlineAll
              traverse_ fixArityDef cns
              traverse_ inlineHeuristics cns
              traverse_ constantFold cns
-             traverse_ setIdentity cns
+--              traverse_ setIdentity cns
              transform k cns
 
     nonErased : Name -> Core Bool

src/Compiler/Opts/ConstantFold.idr

@@ -70,6 +70,11 @@ lookup fc (MkVar p) rho = case go p rho of
       Z => Left (MkVar First)
       S i' => bimap later weaken (go (dropLater p) (Wk rho ws'))
 
+replace : CExp vars -> Bool
+replace (CLocal _ _)   = True
+replace (CPrimVal _ _) = True
+replace _              = False
+
 -- constant folding of primitive functions
 -- if a primitive function is applied to only constant
 -- then replace with the result
@@ -82,13 +87,11 @@ constFold rho (CLocal fc p) = lookup fc (MkVar p) rho
 constFold rho e@(CRef fc x) = CRef fc x
 constFold rho (CLam fc x y)
   = CLam fc x $ constFold (wk rho (mkSizeOf [<x])) y
-constFold rho (CLet fc x inlineOK y z) =
+constFold rho (CLet fc x inl y z) =
     let val = constFold rho y
-     in case val of
-        CPrimVal _ _ => if inlineOK
-            then constFold (rho :< val) z
-            else CLet fc x inlineOK val (constFold (wk rho (mkSizeOf [<x])) z)
-        _ => CLet fc x inlineOK val (constFold (wk rho (mkSizeOf [<x])) z)
+     in if replace val
+          then constFold (rho :< val) z
+          else CLet fc x inl val (constFold (wk rho (mkSizeOf [<x])) z)
 constFold rho (CApp fc (CRef fc2 n) [x]) =
   if n == NS typesNS (UN $ Basic "prim__integerToNat")
      then case constFold rho x of
@@ -98,6 +101,7 @@ constFold rho (CApp fc (CRef fc2 n) [x]) =
      else CApp fc (CRef fc2 n) [constFold rho x]
 constFold rho (CApp fc x xs) = CApp fc (constFold rho x) (constFold rho <$> xs)
 constFold rho (CCon fc x y tag xs) = CCon fc x y tag $ constFold rho <$> xs
+constFold rho (COp fc BelieveMe [CErased _, CErased _ , x]) = constFold rho x
 constFold rho (COp {arity} fc fn xs) =
     let xs' = map (constFold rho) xs
         e = constRight fc fn xs'

src/Compiler/Opts/Identity.idr

@@ -119,7 +119,8 @@ checkIdentity fn (v :: vs) exp idx = if cexpIdentity fn idx v Nothing Nothing ex
 
 calcIdentity : (fullName : Name) -> CDef -> Maybe Nat
 calcIdentity fn (MkFun args exp)
-   = checkIdentity fn (makeArgs {vars=[<]} args) (rewrite appendLinLeftNeutral args in exp) Z
+   = checkIdentity fn (makeArgs {vars=[<]} args)
+                   (rewrite appendLinLeftNeutral args in exp) Z
 calcIdentity _ _ = Nothing
 
 getArg : FC -> Nat -> (args : SnocList Name) -> Maybe (CExp args)

src/Core/Binary.idr

@@ -23,7 +23,7 @@ import Libraries.System.File.Buffer
 export
 ttcVersion : Int
 ttcVersion
-  = 20221207 -- the date of the update
+  = 20230917 -- the date of the update
     * 1000   -- so as to be bigger than Idris 2!
     + 0      -- update number on given date
 

src/Core/Binary/Prims.idr

@@ -311,7 +311,7 @@ TTC String where
            tbl <- get STable
            idx <- fromBuf
            case lookup idx tbl of
-                Nothing => do coreLift $ printLn (IntMap.toList tbl)
+                Nothing => do coreLift $ putStrLn ("String table error " ++ show (IntMap.toList tbl))
                               corrupt ("StringTable entry " ++ show idx)
                 Just str => pure str
 

src/Core/Case/Util.idr

@@ -68,7 +68,8 @@ mkAlt fc sc (MkDataCon cn t ar qs)
     mkScope (q :: qs) (vs :< v) = TArg q v (weaken (mkScope qs vs))
 
 emptyRHSTm : FC -> Term vars -> Term vars
-emptyRHSTm fc (Case cfc ct c sc scTy alts) = Case cfc ct c sc scTy (map emptyRHSalt alts)
+emptyRHSTm fc (Case cfc ct c sc scTy alts)
+    = Case cfc ct c sc scTy (map emptyRHSalt alts)
   where
     emptyRHSscope : forall vars . FC -> CaseScope vars -> CaseScope vars
     emptyRHSscope fc (RHS fs tm) = RHS fs (emptyRHSTm fc tm)
@@ -86,12 +87,13 @@ export
 mkAltTm : {vars : _} ->
         FC -> Term vars -> DataCon -> CaseAlt vars
 mkAltTm fc sc (MkDataCon cn t ar qs)
-    = ConCase fc cn t (mkScope qs (map (MN "m") (take ar [0..])))
+    = ConCase fc cn t (mkScope zero qs (map (MN "m") (take ar [0..])))
   where
-    mkScope : List RigCount -> SnocList Name -> CaseScope vars
-    mkScope _ [<] = RHS [] (emptyRHSTm fc sc)
-    mkScope [] (vs :< v) = Arg top v (weaken (mkScope [] vs))
-    mkScope (q :: qs) (vs :< v) = Arg q v (weaken (mkScope qs vs))
+    mkScope : SizeOf more -> List RigCount -> SnocList Name ->
+              CaseScope (vars ++ more)
+    mkScope s _ [<] = RHS [] (weakenNs s (emptyRHSTm fc sc))
+    mkScope s [] (vs :< v) = Arg top v (mkScope (suc s) [] vs)
+    mkScope s (q :: qs) (vs :< v) = Arg q v (mkScope (suc s) qs vs)
 
 export
 tagIs : Int -> TCaseAlt vars -> Bool

src/Core/Coverage.idr

@@ -1,6 +1,5 @@
 module Core.Coverage
 
-import Core.Case.Tree
 import Core.Case.Util
 import Core.Context
 import Core.Context.Log
@@ -308,24 +307,25 @@ buildArgs defs known not ps cs@(Case fc PatMatch c (Local lfc idx el) ty altsIn)
          let var = nameAt el
          buildArgsAlt var not altsN
   where
-    buildArgSc : {vars : _} ->
+    buildArgSc : {vars, more : _} ->
+                 SizeOf more ->
                  FC -> Name ->
                  KnownVars vars Int -> KnownVars vars (List Int) ->
                  Name -> Int -> SnocList (RigCount, Name) ->
-                 CaseScope vars -> Core (List (SnocList (RigCount, ClosedTerm)))
-    buildArgSc fc var known not' n t args (RHS _ tm)
+                 CaseScope (vars ++ more) -> Core (List (SnocList (RigCount, ClosedTerm)))
+    buildArgSc s fc var known not' n t args (RHS _ tm)
         = do let con = Ref fc (DataCon t (length args)) n
              let app = applySpine fc con
                              (map (\ (c, n) => (c, (Ref fc Bound n))) args)
              let ps' = map (\ (c, t) => (c, substName var app t)) ps
-             buildArgs defs known not' ps' tm
-    buildArgSc fc var known not' n t args (Arg c x sc)
-        = buildArgSc fc var (weaken known) (weaken not') n t (args :< (c, x)) sc
+             buildArgs defs (weakenNs s known) (weakenNs s not') ps' tm
+    buildArgSc s fc var known not' n t args (Arg c x sc)
+        = buildArgSc (suc s) fc var known not' n t (args :< (c, x)) sc
 
     buildArgAlt : Name -> KnownVars vars (List Int) ->
                   CaseAlt vars -> Core (List (SnocList (RigCount, ClosedTerm)))
     buildArgAlt var not' (ConCase cfc n t sc)
-        = buildArgSc cfc var ((MkVar el, t) :: known) not' n t [<] sc
+        = buildArgSc zero cfc var ((MkVar el, t) :: known) not' n t [<] sc
     buildArgAlt var not' (DelayCase cfc t a sc)
         = let l = mkSizeOf [< t, a]
               ps' = map (\ (c, tm) =>

src/Core/InitPrimitives.idr

@@ -39,6 +39,7 @@ addPrim p
                               (Function (MkFnInfo NotHole False False)
                                         fndef fndef Nothing)
          ignore $ addDef (opName (fn p)) primdef
+         setFlag EmptyFC (opName (fn p)) Inline
          compileDef (opName (fn p))
 
 export

src/Core/TTCFile.idr

@@ -475,6 +475,6 @@ readTotalReq fname
     = do Right buffer <- readNoStringTable "TT2" fname
              | _ => pure Nothing
          bin <- newRef Bin buffer -- for reading the file into
-         importHashes <- fromBuf {a = List (Namespace,Int)}
+         importHashes <- fromBuf {a = List (RawNamespace,Int)}
          totalReq <- fromBuf
          pure (Just totalReq)

src/Idris/Driver.idr

@@ -82,9 +82,9 @@ updateEnv
          catch (addPkgDir "prelude" anyBounds) (const (pure ()))
          catch (addPkgDir "base" anyBounds) (const (pure ()))
          addDataDir (prefix_dir (dirs (options defs)) </>
-                        ("idris2-" ++ showVersion False version) </> "support")
+                        ("yaffle-" ++ showVersion False version) </> "support")
          addLibDir (prefix_dir (dirs (options defs)) </>
-                        ("idris2-" ++ showVersion False version) </> "lib")
+                        ("yaffle-" ++ showVersion False version) </> "lib")
          Just cwd <- coreLift $ currentDir
               | Nothing => throw (InternalError "Can't get current directory")
          addLibDir cwd

src/Idris/ModTree.idr

@@ -146,7 +146,8 @@ checkTotalReq sourceFile ttcFile expected
   = catch (do log "totality.requirement" 20 $
                 "Reading totalReq from " ++ ttcFile
               Just got <- ttc $ readTotalReq ttcFile
-                | Nothing => pure False
+                | Nothing => do coreLift $ putStrLn "Not here"
+                                pure False
               log "totality.requirement" 20 $ unwords
                 [ "Got", show got, "and expected", show expected ++ ":"
                 , "we", ifThenElse (got < expected) "should" "shouldn't"
@@ -155,7 +156,8 @@ checkTotalReq sourceFile ttcFile expected
               -- first time around) was strictly less stringent than what we
               -- expect now then we need to rebuild.
               pure (got < expected))
-          (\error => pure False)
+          (\error => do coreLift $ printLn error
+                        pure False)
 
 needsBuildingTime : {auto c : Ref Ctxt Defs} ->
                     (sourceFile : String) -> (ttcFile : String) ->