mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-14 03:14:14 +03:00
d5377be628
More documentation to follow, but in brief: - IO is now a synonym of IO' FFI_C - IO' is parameterised over an ffi description, which explains which types are allowed in foreign calls, and what a foreign call target is (in C, that's a String giving the function name, for example) - New function "foreign" for building a foreign call, given an ffi description, call target, and the type of the call. The type is enough to build a structure which the compiler uses to generate the call. The type of main now needs to be IO' x (), where x can be any FFI description. There is currently only an ffi description for C; Javascript will follow. FFI_C should also work for the llvm backend (it's really about the calling convention, not the backend specifically). Small changes will be needed to the various code generators.
100 lines
2.8 KiB
Idris
100 lines
2.8 KiB
Idris
-- Test for problem with parameter propagation in fromState'
|
|
|
|
data StateTy : Type where
|
|
STInt : StateTy
|
|
STString : StateTy
|
|
STMaybe : StateTy -> StateTy
|
|
STList : StateTy -> StateTy
|
|
|
|
interpSTy : StateTy -> Type
|
|
interpSTy STInt = Int
|
|
interpSTy STString = String
|
|
interpSTy (STMaybe a) = Maybe (interpSTy a)
|
|
interpSTy (STList a) = List (interpSTy a)
|
|
|
|
data State : StateTy -> Type where
|
|
MkState : (t : StateTy) -> Ptr -> State t
|
|
|
|
abstract
|
|
data StateC : StateTy -> Type where
|
|
MkStateC : Int -> (t : StateTy) -> Ptr -> StateC t
|
|
|
|
isObj : Ptr -> IO Bool
|
|
isObj p = do
|
|
"object" <- mkForeign (FFun "typeof %0" [FPtr] FString) p
|
|
| _ => pure False
|
|
pure True
|
|
|
|
stateVarName : String
|
|
stateVarName = "__IDR__IQUERY__STATE__"
|
|
|
|
stateVarExists : IO Bool
|
|
stateVarExists = do
|
|
o <- mkForeign (FFun ("typeof " ++ stateVarName) [] FString)
|
|
pure $ if o == "object" then True else False
|
|
|
|
initStateVar : IO Ptr
|
|
initStateVar = mkForeign (FFun (stateVarName ++ " = {count: 0}") [] FPtr)
|
|
|
|
getStateVar : IO (Maybe Ptr)
|
|
getStateVar = case !stateVarExists of
|
|
True => map Just $ mkForeign (FFun stateVarName [] FPtr)
|
|
False => pure Nothing
|
|
|
|
getStateVar' : IO Ptr
|
|
getStateVar' = case !getStateVar of
|
|
Just s => pure s
|
|
Nothing => initStateVar
|
|
|
|
stateCExists : Ptr -> Int -> IO Bool
|
|
stateCExists c n = do
|
|
r <- mkForeign (FFun "typeof %0[%1]" [FPtr,FInt] FString) c n
|
|
pure $ if r == "object" then True else False
|
|
|
|
incCount : Ptr -> IO Int
|
|
incCount c = do
|
|
n <- mkForeign (FFun "%0.count" [FPtr] FInt) c
|
|
mkForeign (FFun "%0.count++" [FPtr] FUnit) c
|
|
pure n
|
|
|
|
infixl 5 =>>
|
|
public
|
|
(=>>) : IO (Maybe (State a)) -> (State a -> IO (Maybe b))
|
|
-> IO (Maybe b)
|
|
s =>> f = do
|
|
(Just s') <- s
|
|
| Nothing => pure Nothing
|
|
f s'
|
|
|
|
infixl 5 :=>
|
|
public
|
|
(:=>) : IO (Maybe (State a)) -> (State a -> IO ()) -> IO Bool
|
|
(:=>) s f = do
|
|
(Just s') <- s
|
|
| Nothing => pure False
|
|
f s'
|
|
pure True
|
|
|
|
public
|
|
access : Nat -> State (STList t) -> IO (Maybe (State t))
|
|
access n (MkState (STList t) p) = do
|
|
r <- mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p (fromNat n)
|
|
True <- isObj r
|
|
| False => pure Nothing
|
|
pure $ Just $ MkState t r
|
|
|
|
fromState' : State t -> IO (interpSTy t)
|
|
fromState' (MkState STInt p) = mkForeign (FFun "%0.val" [FPtr] FInt) p
|
|
fromState' (MkState STString p) = mkForeign (FFun "%0.val" [FPtr] FString) p
|
|
fromState' (MkState (STMaybe a) p) = do
|
|
isNull <- (mkForeign (FFun "(%0.val == null).toString()" [FPtr] FString) p)
|
|
case isNull == "true" of
|
|
True => pure Nothing
|
|
False => pure $ Just !(fromState' (MkState a p))
|
|
fromState' (MkState (STList a) p) = do
|
|
n <- mkForeign (FFun "%0.val.length" [FPtr] FInt) p
|
|
ps <- sequence $ map
|
|
(\n => mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p n) [0..(n-1)]
|
|
sequence $ map (\p' => fromState' (MkState a p')) ps
|
|
|