Merge pull request #2 from danielkroeni/main

Make it compile with idris v0.4.0

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

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

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 ()

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

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