From 0501538497f296e12894260df2a6672220218cd4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Kro=CC=88ni?= <daniel.kroeni@fhnw.ch>
Date: Fri, 25 Jun 2021 09:54:48 +0200
Subject: [PATCH] Make it compile with idris v0.4.0

---
 README.md                         | 2 +-
 grin/src/Data/String/Builder.idr  | 1 -
 grin/src/GRIN/Analysis/Inline.idr | 4 ++--
 src/GRIN/Data.idr                 | 4 ++++
 src/GRIN/PrimOps.idr              | 4 ++++
 5 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/README.md b/README.md
index f917313..61bddde 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 # Idris2grin
 GRIN backend for Idris2.  
 
-This only works with recent versions of idris2 (v0.3.0 +).
+This only works with recent versions of idris2 (v0.4.0 +).
 
 ## Todo
 - [x] Finish unfinished functions
diff --git a/grin/src/Data/String/Builder.idr b/grin/src/Data/String/Builder.idr
index 325df16..65aee44 100644
--- a/grin/src/Data/String/Builder.idr
+++ b/grin/src/Data/String/Builder.idr
@@ -34,7 +34,6 @@ runBuilder (MkBuilder size tree) = unsafePerformIO $ do
         | Nothing => pure ""
     runBuilderTree b 0 tree
     str <- getString b 0 size
-    freeBuffer b
     pure str
 
 export
diff --git a/grin/src/GRIN/Analysis/Inline.idr b/grin/src/GRIN/Analysis/Inline.idr
index b437712..1a5aea2 100644
--- a/grin/src/GRIN/Analysis/Inline.idr
+++ b/grin/src/GRIN/Analysis/Inline.idr
@@ -25,7 +25,7 @@ inlineSimpleDefs : Ord name => Monad m => GrinT name m ()
 inlineSimpleDefs = do
     MkProg _ defs m <- gets prog
     modify $ record { toInline =
-        delete m $ foldMap @{(%search, MonoidMergeLeft)} simpleDef defs }
+        delete m $ foldMap @{%search} @{MonoidMergeLeft} simpleDef defs }
 
 calledSExp : Eq name => name -> SExp name -> Nat
 calledExp : Eq name => name -> Exp name -> Nat
@@ -36,7 +36,7 @@ calledSExp _ _ = 0
 
 calledExp fn (SimpleExp e) = calledSExp fn e
 calledExp fn (Bind _ rhs rest) = calledSExp fn rhs + calledExp fn rest
-calledExp fn (Case _ alts) = foldMap @{(%search, Additive)} (calledExp fn . altExp) alts
+calledExp fn (Case _ alts) = foldMap @{%search} @{Additive} (calledExp fn . altExp) alts
 
 export
 inlineUsedOnce : Ord name => Monad m => GrinT name m ()
diff --git a/src/GRIN/Data.idr b/src/GRIN/Data.idr
index da8721a..b2fafc8 100644
--- a/src/GRIN/Data.idr
+++ b/src/GRIN/Data.idr
@@ -415,6 +415,10 @@ getCFType : CFType -> Maybe (GType GName)
 getCFType = \case
     CFUnit => Just $ SimpleType UnitTy
     CFInt => Just $ SimpleType $ IntTy $ Signed 64
+    CFInt8 => Just $ SimpleType $ IntTy $ Signed 8
+    CFInt16 => Just $ SimpleType $ IntTy $ Signed 16
+    CFInt32 => Just $ SimpleType $ IntTy $ Signed 32
+    CFInt64 => Just $ SimpleType $ IntTy $ Signed 64
     CFUnsigned8 => Just $ SimpleType $ IntTy $ Unsigned 8
     CFUnsigned16 => Just $ SimpleType $ IntTy $ Unsigned 16
     CFUnsigned32 => Just $ SimpleType $ IntTy $ Unsigned 32
diff --git a/src/GRIN/PrimOps.idr b/src/GRIN/PrimOps.idr
index dec7368..cee7995 100644
--- a/src/GRIN/PrimOps.idr
+++ b/src/GRIN/PrimOps.idr
@@ -126,6 +126,10 @@ getCFTypeCon : CFType -> Maybe (Maybe (Tag GName))
 getCFTypeCon = \case
     CFUnit => Just Nothing
     CFInt => just2 intTag
+    CFInt8 => just2 int8Tag
+    CFInt16 => just2 int16Tag
+    CFInt32 => just2 int32Tag
+    CFInt64 => just2 int64Tag
     CFUnsigned8 => just2 bits8Tag
     CFUnsigned16 => just2 bits16Tag
     CFUnsigned32 => just2 bits32Tag