mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 02:07:25 +03:00
Add ability to manipulate scheme objects
This is step 0 in a plan to use the scheme evaluator to evaluate Idris expressions at compile time. As a proof of concept, I've got this working for a toy language here: https://github.com/edwinb/SchemeEval We won't be able to do anything interesting with this in Idris itself until the next release because it involves updating the bootstrap code and adding the ability to pass 'Integer' to foreign calls, which really should have been allowed anyway since it's for a backend to decide what it can cope with, not Idris itself.
This commit is contained in:
parent
328617d6fa
commit
c28b257fb5
@ -575,6 +575,7 @@ data NArgs : Type where
|
||||
NPtr : NArgs
|
||||
NGCPtr : NArgs
|
||||
NBuffer : NArgs
|
||||
NForeignObj : NArgs
|
||||
NIORes : Closure [] -> NArgs
|
||||
|
||||
getPArgs : {auto c : Ref Ctxt Defs} ->
|
||||
@ -611,6 +612,7 @@ getNArgs defs (NS _ (UN "AnyPtr")) [] = pure NPtr
|
||||
getNArgs defs (NS _ (UN "GCPtr")) [arg] = pure NGCPtr
|
||||
getNArgs defs (NS _ (UN "GCAnyPtr")) [] = pure NGCPtr
|
||||
getNArgs defs (NS _ (UN "Buffer")) [] = pure NBuffer
|
||||
getNArgs defs (NS _ (UN "ForeignObj")) [] = pure NForeignObj
|
||||
getNArgs defs (NS _ (UN "Unit")) [] = pure NUnit
|
||||
getNArgs defs (NS _ (UN "Struct")) [n, args]
|
||||
= do NPrimVal _ (Str n') <- evalClosure defs n
|
||||
@ -621,6 +623,7 @@ getNArgs defs n args = pure $ User n args
|
||||
nfToCFType : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> (inStruct : Bool) -> NF [] -> Core CFType
|
||||
nfToCFType _ _ (NPrimVal _ IntType) = pure CFInt
|
||||
nfToCFType _ _ (NPrimVal _ IntegerType) = pure CFInteger
|
||||
nfToCFType _ _ (NPrimVal _ Bits8Type) = pure CFUnsigned8
|
||||
nfToCFType _ _ (NPrimVal _ Bits16Type) = pure CFUnsigned16
|
||||
nfToCFType _ _ (NPrimVal _ Bits32Type) = pure CFUnsigned32
|
||||
@ -662,6 +665,7 @@ nfToCFType _ s (NTCon fc n_in _ _ args)
|
||||
NPtr => pure CFPtr
|
||||
NGCPtr => pure CFGCPtr
|
||||
NBuffer => pure CFBuffer
|
||||
NForeignObj => pure CFForeignObj
|
||||
NIORes uarg =>
|
||||
do narg <- evalClosure defs uarg
|
||||
carg <- nfToCFType fc s narg
|
||||
|
@ -153,6 +153,7 @@ public export
|
||||
data CFType : Type where
|
||||
CFUnit : CFType
|
||||
CFInt : CFType
|
||||
CFInteger : CFType
|
||||
CFInt8 : CFType
|
||||
CFInt16 : CFType
|
||||
CFInt32 : CFType
|
||||
@ -167,6 +168,7 @@ data CFType : Type where
|
||||
CFPtr : CFType
|
||||
CFGCPtr : CFType
|
||||
CFBuffer : CFType
|
||||
CFForeignObj : CFType
|
||||
CFWorld : CFType
|
||||
CFFun : CFType -> CFType -> CFType
|
||||
CFIORes : CFType -> CFType
|
||||
@ -350,6 +352,7 @@ export
|
||||
Show CFType where
|
||||
show CFUnit = "Unit"
|
||||
show CFInt = "Int"
|
||||
show CFInteger = "Integer"
|
||||
show CFInt8 = "Int_8"
|
||||
show CFInt16 = "Int_16"
|
||||
show CFInt32 = "Int_32"
|
||||
@ -364,6 +367,7 @@ Show CFType where
|
||||
show CFPtr = "Ptr"
|
||||
show CFGCPtr = "GCPtr"
|
||||
show CFBuffer = "Buffer"
|
||||
show CFForeignObj = "ForeignObj"
|
||||
show CFWorld = "%World"
|
||||
show (CFFun s t) = show s ++ " -> " ++ show t
|
||||
show (CFIORes t) = "IORes " ++ show t
|
||||
|
@ -235,6 +235,10 @@ Hashable CFType where
|
||||
h `hashWithSalt` 19
|
||||
CFInt64 =>
|
||||
h `hashWithSalt` 20
|
||||
CFForeignObj =>
|
||||
h `hashWithSalt` 21
|
||||
CFInteger =>
|
||||
h `hashWithSalt` 22
|
||||
|
||||
export
|
||||
Hashable Constant where
|
||||
|
@ -785,6 +785,8 @@ TTC CFType where
|
||||
toBuf b CFInt16 = tag 18
|
||||
toBuf b CFInt32 = tag 19
|
||||
toBuf b CFInt64 = tag 20
|
||||
toBuf b CFForeignObj = tag 21
|
||||
toBuf b CFInteger = tag 22
|
||||
|
||||
fromBuf b
|
||||
= case !getTag of
|
||||
@ -809,6 +811,8 @@ TTC CFType where
|
||||
18 => pure CFInt16
|
||||
19 => pure CFInt32
|
||||
20 => pure CFInt64
|
||||
21 => pure CFForeignObj
|
||||
22 => pure CFInteger
|
||||
_ => corrupt "CFType"
|
||||
|
||||
export
|
||||
|
@ -481,3 +481,70 @@
|
||||
(when x
|
||||
(((cdr x) (car x)) 'erased)
|
||||
(run))))))
|
||||
|
||||
;; For creating and reading back scheme objects
|
||||
|
||||
; read a scheme string and evaluate it, returning 'Just result' on success
|
||||
; TODO: catch exception!
|
||||
(define (blodwen-eval-scheme str)
|
||||
(box (eval (read (open-input-string str))))) ; box == Just
|
||||
|
||||
(define (blodwen-eval-okay obj)
|
||||
(if (null? obj)
|
||||
0
|
||||
1))
|
||||
|
||||
(define (blodwen-get-eval-result obj)
|
||||
(unbox obj))
|
||||
|
||||
(define (blodwen-debug-scheme obj)
|
||||
(display obj) (newline))
|
||||
|
||||
(define (blodwen-is-number obj)
|
||||
(if (number? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-integer obj)
|
||||
(if (integer? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-float obj)
|
||||
(if (flonum? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-char obj)
|
||||
(if (char? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-string obj)
|
||||
(if (string? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-procedure obj)
|
||||
(if (procedure? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-symbol obj)
|
||||
(if (symbol? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-vector obj)
|
||||
(if (vector? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-nil obj)
|
||||
(if (null? obj) 1 0))
|
||||
|
||||
(define (blodwen-is-pair obj)
|
||||
(if (pair? obj) 1 0))
|
||||
|
||||
(define (blodwen-make-symbol str)
|
||||
(string->symbol str))
|
||||
|
||||
; The below rely on checking that the objects are the right type first.
|
||||
|
||||
(define (blodwen-vector-ref obj i)
|
||||
(vector-ref obj i))
|
||||
|
||||
(define (blodwen-vector-length obj)
|
||||
(vector-length obj))
|
||||
|
||||
(define (blodwen-apply obj arg)
|
||||
(obj arg))
|
||||
|
||||
(define (blodwen-read-symbol sym)
|
||||
(symbol->string sym))
|
||||
|
||||
(define (blodwen-id x) x)
|
||||
|
Loading…
Reference in New Issue
Block a user