Skip to content

Commit e533bc4

Browse files
committed
chore: M5 CI/Workflow Sweep - final synchronisation
1 parent 2eec6ed commit e533bc4

2 files changed

Lines changed: 213 additions & 85 deletions

File tree

flake.lock

Lines changed: 61 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

src/abi/Foreign.idr

Lines changed: 152 additions & 85 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,39 @@
1-
||| Foreign Function Interface Declarations for Docudactyl
1+
||| SPDX-License-Identifier: PMPL-1.0-or-later
2+
||| Foreign Function Interface Declarations for DOCUDACTYL
23
|||
3-
||| Declares all C-compatible functions implemented in the Zig FFI layer
4-
||| (ffi/zig/src/docudactyl_ffi.zig). Chapel calls these directly; Idris2
5-
||| provides the type-level proofs that the interface is correct.
4+
||| This module declares all C-compatible functions that will be
5+
||| implemented in the Zig FFI layer.
66
|||
7-
||| SPDX-License-Identifier: PMPL-1.0-or-later
8-
||| Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
7+
||| All functions are declared here with type signatures and safety proofs.
8+
||| Implementations live in ffi/zig/
99

1010
module Docudactyl.ABI.Foreign
1111

1212
import Docudactyl.ABI.Types
1313
import Docudactyl.ABI.Layout
14-
import Data.So
1514

1615
%default total
1716

1817
--------------------------------------------------------------------------------
1918
-- Library Lifecycle
2019
--------------------------------------------------------------------------------
2120

22-
||| Initialise the Docudactyl FFI library.
23-
||| Returns a handle to Tesseract/GDAL/vips contexts, or Nothing on failure.
21+
||| Initialize the library
22+
||| Returns a handle to the library instance, or Nothing on failure
2423
export
25-
%foreign "C:ddac_init, libdocudactyl_ffi"
24+
%foreign "C:docudactyl_init, libdocudactyl"
2625
prim__init : PrimIO Bits64
2726

28-
||| Safe wrapper for library initialisation
27+
||| Safe wrapper for library initialization
2928
export
3029
init : IO (Maybe Handle)
3130
init = do
32-
ptr <- primIO Docudactyl.ABI.Foreign.prim__init
31+
ptr <- primIO prim__init
3332
pure (createHandle ptr)
3433

35-
||| Free all library resources (Tesseract, GDAL, vips).
36-
||| Safe to call with a null pointer.
34+
||| Clean up library resources
3735
export
38-
%foreign "C:ddac_free, libdocudactyl_ffi"
36+
%foreign "C:docudactyl_free, libdocudactyl"
3937
prim__free : Bits64 -> PrimIO ()
4038

4139
||| Safe wrapper for cleanup
@@ -44,107 +42,176 @@ free : Handle -> IO ()
4442
free h = primIO (prim__free (handlePtr h))
4543

4644
--------------------------------------------------------------------------------
47-
-- Core Parse Operation
45+
-- Core Operations
4846
--------------------------------------------------------------------------------
4947

50-
||| Parse a document. Dispatches to the correct C library based on file extension.
51-
|||
52-
||| Parameters (as raw Bits64 pointers to C strings):
53-
||| handle - library handle from ddac_init
54-
||| input_path - absolute path to input document
55-
||| output_path - absolute path for extracted content output
56-
||| output_fmt - output format (0=scheme, 1=json, 2=csv)
57-
|||
58-
||| Returns a raw pointer to a ddac_parse_result_t struct.
59-
||| In practice, Chapel reads the struct fields directly via extern record.
48+
||| Example operation: process data
6049
export
61-
%foreign "C:ddac_parse, libdocudactyl_ffi"
62-
prim__parse : Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO Bits64
50+
%foreign "C:docudactyl_process, libdocudactyl"
51+
prim__process : Bits64 -> Bits32 -> PrimIO Bits32
6352

64-
||| Safe wrapper for parse with type-checked status
53+
||| Safe wrapper with error handling
6554
export
66-
parse : Handle -> (inputPath : Bits64) -> (outputPath : Bits64) -> (outputFmt : Bits64) -> IO (Either ParseStatus Bits64)
67-
parse h inputPath outputPath outputFmt = do
68-
resultPtr <- primIO (Docudactyl.ABI.Foreign.prim__parse (handlePtr h) inputPath outputPath outputFmt)
69-
if resultPtr == 0
70-
then pure (Left Error)
71-
else pure (Right resultPtr)
55+
process : Handle -> Bits32 -> IO (Either Result Bits32)
56+
process h input = do
57+
result <- primIO (prim__process (handlePtr h) input)
58+
pure $ case result of
59+
0 => Left Error
60+
n => Right n
7261

7362
--------------------------------------------------------------------------------
74-
-- Version Information
63+
-- String Operations
7564
--------------------------------------------------------------------------------
7665

77-
||| Get library version string
78-
export
79-
%foreign "C:ddac_version, libdocudactyl_ffi"
80-
prim__version : PrimIO Bits64
81-
82-
||| Convert C string pointer to Idris String
66+
||| Convert C string to Idris String
8367
export
8468
%foreign "support:idris2_getString, libidris2_support"
8569
prim__getString : Bits64 -> String
8670

71+
||| Free C string
72+
export
73+
%foreign "C:docudactyl_free_string, libdocudactyl"
74+
prim__freeString : Bits64 -> PrimIO ()
75+
76+
||| Get string result from library
77+
export
78+
%foreign "C:docudactyl_get_string, libdocudactyl"
79+
prim__getResult : Bits64 -> PrimIO Bits64
80+
81+
||| Safe string getter
82+
export
83+
getString : Handle -> IO (Maybe String)
84+
getString h = do
85+
ptr <- primIO (prim__getResult (handlePtr h))
86+
if ptr == 0
87+
then pure Nothing
88+
else do
89+
let str = prim__getString ptr
90+
primIO (prim__freeString ptr)
91+
pure (Just str)
92+
93+
--------------------------------------------------------------------------------
94+
-- Array/Buffer Operations
95+
--------------------------------------------------------------------------------
96+
97+
||| Process array data
98+
export
99+
%foreign "C:docudactyl_process_array, libdocudactyl"
100+
prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32
101+
102+
||| Safe array processor
103+
export
104+
processArray : Handle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ())
105+
processArray h buf len = do
106+
result <- primIO (prim__processArray (handlePtr h) buf len)
107+
pure $ case resultFromInt result of
108+
Just Ok => Right ()
109+
Just err => Left err
110+
Nothing => Left Error
111+
where
112+
resultFromInt : Bits32 -> Maybe Result
113+
resultFromInt 0 = Just Ok
114+
resultFromInt 1 = Just Error
115+
resultFromInt 2 = Just InvalidParam
116+
resultFromInt 3 = Just OutOfMemory
117+
resultFromInt 4 = Just NullPointer
118+
resultFromInt _ = Nothing
119+
120+
--------------------------------------------------------------------------------
121+
-- Error Handling
122+
--------------------------------------------------------------------------------
123+
124+
||| Get last error message
125+
export
126+
%foreign "C:docudactyl_last_error, libdocudactyl"
127+
prim__lastError : PrimIO Bits64
128+
129+
||| Retrieve last error as string
130+
export
131+
lastError : IO (Maybe String)
132+
lastError = do
133+
ptr <- primIO prim__lastError
134+
if ptr == 0
135+
then pure Nothing
136+
else pure (Just (prim__getString ptr))
137+
138+
||| Get error description for result code
139+
export
140+
errorDescription : Result -> String
141+
errorDescription Ok = "Success"
142+
errorDescription Error = "Generic error"
143+
errorDescription InvalidParam = "Invalid parameter"
144+
errorDescription OutOfMemory = "Out of memory"
145+
errorDescription NullPointer = "Null pointer"
146+
147+
--------------------------------------------------------------------------------
148+
-- Version Information
149+
--------------------------------------------------------------------------------
150+
151+
||| Get library version
152+
export
153+
%foreign "C:docudactyl_version, libdocudactyl"
154+
prim__version : PrimIO Bits64
155+
87156
||| Get version as string
88157
export
89158
version : IO String
90159
version = do
91160
ptr <- primIO prim__version
92161
pure (prim__getString ptr)
93162

94-
--------------------------------------------------------------------------------
95-
-- Error Handling Utilities
96-
--------------------------------------------------------------------------------
97-
98-
||| Extract ParseStatus from a raw result status integer
163+
||| Get library build info
99164
export
100-
decodeStatus : Bits32 -> ParseStatus
101-
decodeStatus n = case intToParseStatus n of
102-
Just s => s
103-
Nothing => Error
165+
%foreign "C:docudactyl_build_info, libdocudactyl"
166+
prim__buildInfo : PrimIO Bits64
104167

105-
||| Extract ContentKind from a raw result content_kind integer
168+
||| Get build information
106169
export
107-
decodeContentKind : Bits32 -> ContentKind
108-
decodeContentKind n = case intToContentKind n of
109-
Just k => k
110-
Nothing => Unknown
170+
buildInfo : IO String
171+
buildInfo = do
172+
ptr <- primIO prim__buildInfo
173+
pure (prim__getString ptr)
174+
175+
--------------------------------------------------------------------------------
176+
-- Callback Support
177+
--------------------------------------------------------------------------------
178+
179+
||| Callback function type (C ABI)
180+
public export
181+
Callback : Type
182+
Callback = Bits64 -> Bits32 -> Bits32
111183

112-
||| Human-readable description of a parse status
184+
||| Register a callback
113185
export
114-
statusDescription : ParseStatus -> String
115-
statusDescription Ok = "Success"
116-
statusDescription Error = "Generic error"
117-
statusDescription FileNotFound = "File not found"
118-
statusDescription ParseError = "Parse error"
119-
statusDescription NullPointer = "Null pointer"
120-
statusDescription UnsupportedFormat = "Unsupported format"
121-
statusDescription OutOfMemory = "Out of memory"
186+
%foreign "C:docudactyl_register_callback, libdocudactyl"
187+
prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32
122188

123-
||| Human-readable description of a content kind
189+
||| Safe callback registration
124190
export
125-
contentKindDescription : ContentKind -> String
126-
contentKindDescription PDF = "PDF document"
127-
contentKindDescription Image = "Image (OCR)"
128-
contentKindDescription Audio = "Audio recording"
129-
contentKindDescription Video = "Video recording"
130-
contentKindDescription EPUB = "EPUB e-book"
131-
contentKindDescription GeoSpatial = "Geospatial data"
132-
contentKindDescription Unknown = "Unknown format"
191+
registerCallback : Handle -> Callback -> IO (Either Result ())
192+
registerCallback h cb = do
193+
result <- primIO (prim__registerCallback (handlePtr h) (cast cb))
194+
pure $ case resultFromInt result of
195+
Just Ok => Right ()
196+
Just err => Left err
197+
Nothing => Left Error
198+
where
199+
resultFromInt : Bits32 -> Maybe Result
200+
resultFromInt 0 = Just Ok
201+
resultFromInt _ = Just Error
133202

134203
--------------------------------------------------------------------------------
135-
-- Safety Proofs
204+
-- Utility Functions
136205
--------------------------------------------------------------------------------
137206

138-
||| Proof that init returns a non-null handle on success
139-
||| (This is a specification -- the Zig implementation must guarantee it)
140-
||| Given a proof that (ptr /= 0) evaluates to True, we can safely
141-
||| construct a Handle by converting the Bool equality to a So witness.
207+
||| Check if library is initialized
142208
export
143-
initNonNull : (ptr : Bits64) -> (prf : (ptr /= 0) = True) -> Maybe Handle
144-
initNonNull ptr prf = Just (MkHandle ptr (rewrite prf in Oh))
209+
%foreign "C:docudactyl_is_initialized, libdocudactyl"
210+
prim__isInitialized : Bits64 -> PrimIO Bits32
145211

146-
||| Proof that free is idempotent (calling twice is safe)
147-
||| Encoded as a specification: ddac_free(NULL) is a no-op in Zig.
212+
||| Check initialization status
148213
export
149-
freeIdempotent : String
150-
freeIdempotent = "ddac_free checks for null; double-free is a no-op"
214+
isInitialized : Handle -> IO Bool
215+
isInitialized h = do
216+
result <- primIO (prim__isInitialized (handlePtr h))
217+
pure (result /= 0)

0 commit comments

Comments
 (0)