Skip to content

Instantly share code, notes, and snippets.

@lenary
Last active August 29, 2015 14:08
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save lenary/e32e242a91c56382bc5c to your computer and use it in GitHub Desktop.
Save lenary/e32e242a91c56382bc5c to your computer and use it in GitHub Desktop.
RFC: Idris Primitives Changes

I'm currently writing an Erlang backend for the Idris compiler. Right now I've got to the internally "primitive" operations, and would like to see an increased reliance on compiling to these primitives in the Prelude rather than using the foreign function calls that are currently used.

This would probably be a breaking change for lots of backends, so I thought I'd propose it before making any major code changes.

I'm willing to do all these changes to the C and conventional backends, I'd just like to run the idea of them past a few set of eyes before I start.

Some background:

The list of current primitives (over 70) is in Lang.hs below. They cover a wide variety of functionality, most of which is mathematical operations, but there's some more important stuff about I/O: LPrintNum, LPrintStr, LReadStr, LStdIn, LStdOut, LStdErr.

However, if you look in the Prelude (both Prelude.idr and IO.idr), you'll see that these aren't really used. At the idris-level, a primitive invocation by convention is a function beginning with prim__. Instead, in lots of places in Prelude.idr, Idris just directly uses an FFI call to some C. These are below in Prelude.idr (there is a single FFI call in IO.idr, we'll ignore it for now).

Why is this a problem?

It's not a massive problem, but it would be easier for code-generators to not have to special-case all the foreign functions in the Prelude. Instead, it would be easier if all these foreign calls were primitives. That way, a code generator can completely ignore foreign functions, and still know they have a system that will compile any Idris program that relies only on the prelude and basic libraries.

How do we chose what should be a primitive, and what is fine to be a FFI Call? In my opinion, anything in the prelude should just be a primitive. There are a lot of networking functions in libs/base/networking which also use FFIs, but I think that they probably shouldn't be primitives, to keep the number of primitives as low as possible.

What primitives should be added?

I propose this short list below (categorised). Where a type is intbool that just means an integer, with 0 representing false, and non-zero representing success.

Files:

  • LReadChr (args: file handle; return: char) - Read a character from that file
  • LFileOpen (args: name, mode; return: file handle) - Open a file, with a given mode
  • LFileClose (args: file handle; return: unit) - Close an opened file
  • LFileFlush (args: file handle; return: unit) - Flush a file to disk
  • LFileEOF (args: file handle; return: intbool) - Has the file reached EOF?
  • LFileError (args: file handle; return: intbool) - Have any errors occured in the stream?
  • LFilePoll (args: file handle; return: intbool) - Poll the file, is it ready for reading?

Processes:

  • LPOpen (args: command, mode; return: file handle) - Open a process, with a given mode
  • LPClose (args: file handle; return: unit) - Close an opened process

Pointers:

  • LPtrNull (args: pointer; return: intbool) - Is the pointer null?
  • LStrNull (args: string; return: intbool) - Is this the null string?
  • LPtrEq (args: pointer a, pointer b; return intbool) - are the supplied pointers equal?

VM:

  • LForceGC (args: vm pointer; return: unit) - Force the VM to perform GC

This short list should cover all uses. Some places where symmetry is expected (LPrintChar for LReadChar for example), aren't needed as they can be implemented in terms of other primitives (in this case, LPrintStr).

What should be changed?

In an effort to improve the reusability of the current primitives, I propose that we also make the following breaking changes:

Files:

  • LPrintStr - it currently only takes a string to print to stdout. Instead, I think it should also take the file handle to print to, so that this can be used for files as well as stdout/stderr.
  • LPrintNum - this can be removed, I think, as not only is it not currently used, but the same behaviour can be achieved through combinations of LPrintStr and LIntStr a.
-- From src/IRTS/Lang.hs:41-81, reformatted for clarity.
data PrimFn = LPlus ArithTy -- Math
| LMinus ArithTy
| LTimes ArithTy
| LUDiv IntTy
| LSDiv ArithTy
| LURem IntTy
| LSRem ArithTy
| LAnd IntTy
| LOr IntTy
| LXOr IntTy
| LCompl IntTy
| LSHL IntTy
| LLSHR IntTy
| LASHR IntTy
| LEq ArithTy
| LLt IntTy
| LLe IntTy
| LGt IntTy
| LGe IntTy
| LSLt ArithTy
| LSLe ArithTy
| LSGt ArithTy
| LSGe ArithTy
| LSExt IntTy IntTy
| LZExt IntTy IntTy
| LTrunc IntTy IntTy
| LStrConcat -- Strings
| LStrLt
| LStrEq
| LStrLen
| LIntFloat IntTy -- Casts
| LFloatInt IntTy
| LIntStr IntTy
| LStrInt IntTy
| LFloatStr
| LStrFloat
| LChInt IntTy
| LIntCh IntTy
| LPrintNum -- StdIO
| LPrintStr
| LReadStr
| LBitCast ArithTy ArithTy -- Cast?
| LFExp -- Math
| LFLog
| LFSin
| LFCos
| LFTan
| LFASin
| LFACos
| LFATan
| LFSqrt
| LFFloor
| LFCeil
| LFNegate
| LMkVec NativeTy Int -- Vectors
| LIdxVec NativeTy Int
| LUpdateVec NativeTy Int
| LStrHead -- Strings
| LStrTail
| LStrCons
| LStrIndex
| LStrRev
| LStdIn -- StdIO
| LStdOut
| LStdErr
| LAllocate -- Buffers
| LAppendBuffer
| LSystemInfo -- ?
| LAppend IntTy Endianness -- Buffers?
| LPeek IntTy Endianness
| LFork -- Runtime
| LPar
| LVMPtr
| LNullPtr
| LRegisterPtr -- For FFI?
| LNoOp
deriving (Show,Eq)
--- A Subset of `libs/prelude/Prelude.idr` to show FFI Usage. `--` implies elided lines.
--
getChar : IO Char
getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
--
do_fopen : String -> String -> IO Ptr
do_fopen f m
= mkForeign (FFun "fileOpen" [FString, FString] FPtr) f m
--
do_fclose : Ptr -> IO ()
do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h
--
fgetc : File -> IO Char
fgetc (FHandle h) = return (cast !(mkForeign (FFun "fgetc" [FPtr] FInt) h))
--
fgetc' : File -> IO (Maybe Char)
fgetc' (FHandle h)
= do x <- mkForeign (FFun "fgetc" [FPtr] FInt) h
--
fflush : File -> IO ()
fflush (FHandle h) = mkForeign (FFun "fflush" [FPtr] FUnit) h
--
do_popen : String -> String -> IO Ptr
do_popen f m = mkForeign (FFun "do_popen" [FString, FString] FPtr) f m
--
pclose : File -> IO ()
pclose (FHandle h) = mkForeign (FFun "pclose" [FPtr] FUnit) h
--
do_fwrite : Ptr -> String -> IO ()
do_fwrite h s
= mkForeign (FFun "fputStr" [FPtr, FString] FUnit) h s
--
do_feof : Ptr -> IO Int
do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
--
do_ferror : Ptr -> IO Int
do_ferror h = mkForeign (FFun "fileError" [FPtr] FInt) h
--
fpoll : File -> IO Bool
fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
return (p > 0)
--
nullPtr : Ptr -> IO Bool
nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
return (ok /= 0)
--
nullStr : String -> IO Bool
nullStr p = do ok <- mkForeign (FFun "isNull" [FString] FInt) p
return (ok /= 0)
--
eqPtr : Ptr -> Ptr -> IO Bool
eqPtr x y = do eq <- mkForeign (FFun "idris_eqPtr" [FPtr, FPtr] FInt) x y
return (eq /= 0)
--
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment