idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 20:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1438 from edwinb/more-ttc-wrangling

Browse Source 
Substantial reduction in TTC size
This commit is contained in:
Edwin Brady 2021-05-19 18:06:09 +01:00 committed by GitHub
commit daf30ee4f6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
3 changed files with 35 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Binary.idr
View File

@ -33,7 +33,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 53
ttcVersion = 54
export
checkTTCVersion : String -> Int -> Int -> Core ()

22
src/Core/TTC.idr
View File

@ -261,8 +261,8 @@ mutual
export
{vars : _} -> TTC (Term vars) where
toBuf b (Local {name} fc c idx y)
= if idx < 244
then do tag (12 + cast idx)
= if idx < 243
then do tag (13 + cast idx)
toBuf b c
else do tag 0
toBuf b c
@ -278,11 +278,14 @@ mutual
toBuf b x;
toBuf b bnd; toBuf b scope
toBuf b (App fc fn arg)
= do tag 4;
toBuf b fn; toBuf b arg
-- let (fn, args) = getFnArgs (App fc fn arg)
-- toBuf b fn; -- toBuf b p;
-- toBuf b args
= do let (fn, args) = getFnArgs (App fc fn arg)
case args of
[arg] => do tag 4
toBuf b fn
toBuf b arg
args => do tag 12
toBuf b fn
toBuf b args
toBuf b (As fc s as tm)
= do tag 5;
toBuf b as; toBuf b s; toBuf b tm
@ -334,8 +337,11 @@ mutual
pure (PrimVal emptyFC c)
10 => pure (Erased emptyFC False)
11 => pure (TType emptyFC)
12 => do fn <- fromBuf b
args <- fromBuf b
pure (apply emptyFC fn args)
idxp => do c <- fromBuf b
let idx : Nat = fromInteger (cast (idxp - 12))
let idx : Nat = fromInteger (cast (idxp - 13))
let Just name = getName idx vars
| Nothing => corrupt "Term"
pure (Local {name} emptyFC c idx (mkPrf idx))

35
src/Libraries/Utils/Binary.idr
View File

@ -154,23 +154,28 @@ getTag {b}
export
TTC Int where
toBuf b val
= do chunk <- get Bin
if avail chunk >= 8
then
do coreLift $ setInt (buf chunk) (loc chunk) val
put Bin (appended 8 chunk)
else do chunk' <- extendBinary 8 chunk
coreLift $ setInt (buf chunk') (loc chunk') val
put Bin (appended 8 chunk')
= if val >= -127 && val < 128
then tag (val + 127)
else do tag 255
chunk <- get Bin
if avail chunk >= 8
then
do coreLift $ setInt (buf chunk) (loc chunk) val
put Bin (appended 8 chunk)
else do chunk' <- extendBinary 8 chunk
coreLift $ setInt (buf chunk') (loc chunk') val
put Bin (appended 8 chunk')
fromBuf b
= do chunk <- get Bin
if toRead chunk >= 8
then
do val <- coreLift $ getInt (buf chunk) (loc chunk)
put Bin (incLoc 8 chunk)
pure val
else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))
= case !getTag of
255 => do chunk <- get Bin
if toRead chunk >= 8
then
do val <- coreLift $ getInt (buf chunk) (loc chunk)
put Bin (incLoc 8 chunk)
pure val
else throw (TTCError (EndOfBuffer ("Int " ++ show (loc chunk, size chunk))))
t => pure (t - 127)
export
TTC String where