chore: add mandatory SPDX header and sync

Author: hyperpolymath

docs/proofs/papers/language-design-whitepaper.md.invariants.md

@@ -0,0 +1,3 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+# Invariant Path Scan: language-design-whitepaper.md
+

src/abi/Foreign.idr

@@ -1,126 +1,217 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
--- SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
--- Foreign.idr - FFI declarations for WokeLang
+||| SPDX-License-Identifier: PMPL-1.0-or-later
+||| Foreign Function Interface Declarations for WOKELANG
+|||
+||| This module declares all C-compatible functions that will be
+||| implemented in the Zig FFI layer.
+|||
+||| All functions are declared here with type signatures and safety proofs.
+||| Implementations live in ffi/zig/
 
-module WokeLang.ABI.Foreign
+module Wokelang.ABI.Foreign
 
-import WokeLang.ABI.Types
-import WokeLang.ABI.Layout
+import Wokelang.ABI.Types
+import Wokelang.ABI.Layout
 
 %default total
 
--- | C string type
-public export
-CString : Type
-CString = Ptr String
+--------------------------------------------------------------------------------
+-- Library Lifecycle
+--------------------------------------------------------------------------------
 
--- | C int type
-public export
-CInt : Type
-CInt = Bits32
+||| Initialize the library
+||| Returns a handle to the library instance, or Nothing on failure
+export
+%foreign "C:wokelang_init, libwokelang"
+prim__init : PrimIO Bits64
 
--- | C long long type
-public export
-CLongLong : Type
-CLongLong = Bits64
+||| Safe wrapper for library initialization
+export
+init : IO (Maybe Handle)
+init = do
+  ptr <- primIO prim__init
+  pure (createHandle ptr)
 
--- | C double type
-public export
-CDouble : Type
-CDouble = Double
+||| Clean up library resources
+export
+%foreign "C:wokelang_free, libwokelang"
+prim__free : Bits64 -> PrimIO ()
+
+||| Safe wrapper for cleanup
+export
+free : Handle -> IO ()
+free h = primIO (prim__free (handlePtr h))
 
--- ==== Interpreter Lifecycle ====
+--------------------------------------------------------------------------------
+-- Core Operations
+--------------------------------------------------------------------------------
 
--- | Create a new WokeLang interpreter
--- Returns null on failure
-%foreign "C:woke_interpreter_new,libwokelang"
+||| Example operation: process data
 export
-woke_interpreter_new : PrimIO (Ptr InterpreterHandle)
+%foreign "C:wokelang_process, libwokelang"
+prim__process : Bits64 -> Bits32 -> PrimIO Bits32
 
--- | Free a WokeLang interpreter
-%foreign "C:woke_interpreter_free,libwokelang"
+||| Safe wrapper with error handling
 export
-woke_interpreter_free : Ptr InterpreterHandle -> PrimIO ()
+process : Handle -> Bits32 -> IO (Either Result Bits32)
+process h input = do
+  result <- primIO (prim__process (handlePtr h) input)
+  pure $ case result of
+    0 => Left Error
+    n => Right n
 
--- ==== Execution ====
+--------------------------------------------------------------------------------
+-- String Operations
+--------------------------------------------------------------------------------
 
--- | Execute WokeLang source code
-%foreign "C:woke_exec,libwokelang"
+||| Convert C string to Idris String
 export
-woke_exec : Ptr InterpreterHandle -> CString -> PrimIO CInt
+%foreign "support:idris2_getString, libidris2_support"
+prim__getString : Bits64 -> String
 
--- | Execute and get return value
-%foreign "C:woke_eval,libwokelang"
+||| Free C string
 export
-woke_eval : Ptr InterpreterHandle -> CString -> Ptr (Ptr ValueHandle) -> PrimIO CInt
+%foreign "C:wokelang_free_string, libwokelang"
+prim__freeString : Bits64 -> PrimIO ()
 
--- ==== Value Operations ====
+||| Get string result from library
+export
+%foreign "C:wokelang_get_string, libwokelang"
+prim__getResult : Bits64 -> PrimIO Bits64
 
--- | Free a WokeLang value
-%foreign "C:woke_value_free,libwokelang"
+||| Safe string getter
 export
-woke_value_free : Ptr ValueHandle -> PrimIO ()
+getString : Handle -> IO (Maybe String)
+getString h = do
+  ptr <- primIO (prim__getResult (handlePtr h))
+  if ptr == 0
+    then pure Nothing
+    else do
+      let str = prim__getString ptr
+      primIO (prim__freeString ptr)
+      pure (Just str)
+
+--------------------------------------------------------------------------------
+-- Array/Buffer Operations
+--------------------------------------------------------------------------------
 
--- | Get value type
-%foreign "C:woke_value_type,libwokelang"
+||| Process array data
 export
-woke_value_type : Ptr ValueHandle -> PrimIO CInt
+%foreign "C:wokelang_process_array, libwokelang"
+prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32
 
--- | Get integer from value
-%foreign "C:woke_value_as_int,libwokelang"
+||| Safe array processor
 export
-woke_value_as_int : Ptr ValueHandle -> Ptr CLongLong -> PrimIO CInt
+processArray : Handle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ())
+processArray h buf len = do
+  result <- primIO (prim__processArray (handlePtr h) buf len)
+  pure $ case resultFromInt result of
+    Just Ok => Right ()
+    Just err => Left err
+    Nothing => Left Error
+  where
+    resultFromInt : Bits32 -> Maybe Result
+    resultFromInt 0 = Just Ok
+    resultFromInt 1 = Just Error
+    resultFromInt 2 = Just InvalidParam
+    resultFromInt 3 = Just OutOfMemory
+    resultFromInt 4 = Just NullPointer
+    resultFromInt _ = Nothing
 
--- | Get float from value
-%foreign "C:woke_value_as_float,libwokelang"
+--------------------------------------------------------------------------------
+-- Error Handling
+--------------------------------------------------------------------------------
+
+||| Get last error message
 export
-woke_value_as_float : Ptr ValueHandle -> Ptr CDouble -> PrimIO CInt
+%foreign "C:wokelang_last_error, libwokelang"
+prim__lastError : PrimIO Bits64
 
--- | Get boolean from value
-%foreign "C:woke_value_as_bool,libwokelang"
+||| Retrieve last error as string
 export
-woke_value_as_bool : Ptr ValueHandle -> Ptr CInt -> PrimIO CInt
+lastError : IO (Maybe String)
+lastError = do
+  ptr <- primIO prim__lastError
+  if ptr == 0
+    then pure Nothing
+    else pure (Just (prim__getString ptr))
 
--- | Get string from value (must free with woke_string_free)
-%foreign "C:woke_value_as_string,libwokelang"
+||| Get error description for result code
 export
-woke_value_as_string : Ptr ValueHandle -> PrimIO CString
+errorDescription : Result -> String
+errorDescription Ok = "Success"
+errorDescription Error = "Generic error"
+errorDescription InvalidParam = "Invalid parameter"
+errorDescription OutOfMemory = "Out of memory"
+errorDescription NullPointer = "Null pointer"
+
+--------------------------------------------------------------------------------
+-- Version Information
+--------------------------------------------------------------------------------
 
--- | Free string returned by woke_value_as_string
-%foreign "C:woke_string_free,libwokelang"
+||| Get library version
 export
-woke_string_free : CString -> PrimIO ()
+%foreign "C:wokelang_version, libwokelang"
+prim__version : PrimIO Bits64
 
--- ==== Value Creation ====
+||| Get version as string
+export
+version : IO String
+version = do
+  ptr <- primIO prim__version
+  pure (prim__getString ptr)
 
--- | Create integer value
-%foreign "C:woke_value_from_int,libwokelang"
+||| Get library build info
 export
-woke_value_from_int : CLongLong -> PrimIO (Ptr ValueHandle)
+%foreign "C:wokelang_build_info, libwokelang"
+prim__buildInfo : PrimIO Bits64
 
--- | Create float value
-%foreign "C:woke_value_from_float,libwokelang"
+||| Get build information
 export
-woke_value_from_float : CDouble -> PrimIO (Ptr ValueHandle)
+buildInfo : IO String
+buildInfo = do
+  ptr <- primIO prim__buildInfo
+  pure (prim__getString ptr)
+
+--------------------------------------------------------------------------------
+-- Callback Support
+--------------------------------------------------------------------------------
+
+||| Callback function type (C ABI)
+public export
+Callback : Type
+Callback = Bits64 -> Bits32 -> Bits32
 
--- | Create boolean value
-%foreign "C:woke_value_from_bool,libwokelang"
+||| Register a callback
 export
-woke_value_from_bool : CInt -> PrimIO (Ptr ValueHandle)
+%foreign "C:wokelang_register_callback, libwokelang"
+prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
 
--- | Create string value
-%foreign "C:woke_value_from_string,libwokelang"
+||| Safe callback registration
 export
-woke_value_from_string : CString -> PrimIO (Ptr ValueHandle)
+registerCallback : Handle -> Callback -> IO (Either Result ())
+registerCallback h cb = do
+  result <- primIO (prim__registerCallback (handlePtr h) (cast cb))
+  pure $ case resultFromInt result of
+    Just Ok => Right ()
+    Just err => Left err
+    Nothing => Left Error
+  where
+    resultFromInt : Bits32 -> Maybe Result
+    resultFromInt 0 = Just Ok
+    resultFromInt _ = Just Error
 
--- ==== Utility ====
+--------------------------------------------------------------------------------
+-- Utility Functions
+--------------------------------------------------------------------------------
 
--- | Get version string
-%foreign "C:woke_version,libwokelang"
+||| Check if library is initialized
 export
-woke_version : PrimIO CString
+%foreign "C:wokelang_is_initialized, libwokelang"
+prim__isInitialized : Bits64 -> PrimIO Bits32
 
--- | Get last error message
-%foreign "C:woke_last_error,libwokelang"
+||| Check initialization status
 export
-woke_last_error : PrimIO CString
+isInitialized : Handle -> IO Bool
+isInitialized h = do
+  result <- primIO (prim__isInitialized (handlePtr h))
+  pure (result /= 0)