11-- SPDX-License-Identifier: PMPL-1.0-or-later
2- -- SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell (@ hyperpolymath)
2+ -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
33--
44-- LithBridge.idr - Type definitions with proofs for Lith Lith.Bridge ABI
55-- Media-Type: text/x-idris
@@ -25,75 +25,75 @@ import Data.List
2525||| Non-null database handle
2626||| @ ptr The pointer value (guaranteed non-zero)
2727public export
28- data FdbDb : Type where
29- MkFdbDb : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> FdbDb
28+ data LithDb : Type where
29+ MkLithDb : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> LithDb
3030
3131||| Non-null transaction handle
3232||| Transactions are ACID-compliant with rollback via journal inverses
3333public export
34- data FdbTxn : Type where
35- MkFdbTxn : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> FdbTxn
34+ data LithTxn : Type where
35+ MkLithTxn : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> LithTxn
3636
3737||| Non-null cursor handle for query results
3838public export
39- data FdbCursor : Type where
40- MkFdbCursor : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> FdbCursor
39+ data LithCursor : Type where
40+ MkLithCursor : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> LithCursor
4141
4242||| Non-null collection handle
4343public export
44- data FdbCollection : Type where
45- MkFdbCollection : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> FdbCollection
44+ data LithCollection : Type where
45+ MkLithCollection : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> LithCollection
4646
4747||| Non-null schema handle
4848public export
49- data FdbSchema : Type where
50- MkFdbSchema : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> FdbSchema
49+ data LithSchema : Type where
50+ MkLithSchema : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> LithSchema
5151
5252||| Non-null journal handle
5353public export
54- data FdbJournal : Type where
55- MkFdbJournal : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> FdbJournal
54+ data LithJournal : Type where
55+ MkLithJournal : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> LithJournal
5656
5757||| Non-null migration handle
5858public export
59- data FdbMigration : Type where
60- MkFdbMigration : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> FdbMigration
59+ data LithMigration : Type where
60+ MkLithMigration : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> LithMigration
6161
6262-- ------------------------------------------------------------------------------
6363-- Status Codes
6464-- ------------------------------------------------------------------------------
6565
6666||| Result status codes for FFI operations
6767public export
68- data FdbStatus : Type where
68+ data LithStatus : Type where
6969 ||| Operation succeeded
70- StatusOk : FdbStatus
70+ StatusOk : LithStatus
7171 ||| Invalid argument provided
72- StatusInvalidArg : FdbStatus
72+ StatusInvalidArg : LithStatus
7373 ||| Database file not found
74- StatusNotFound : FdbStatus
74+ StatusNotFound : LithStatus
7575 ||| Permission denied
76- StatusPermissionDenied : FdbStatus
76+ StatusPermissionDenied : LithStatus
7777 ||| Database already exists
78- StatusAlreadyExists : FdbStatus
78+ StatusAlreadyExists : LithStatus
7979 ||| Constraint violation
80- StatusConstraintViolation : FdbStatus
80+ StatusConstraintViolation : LithStatus
8181 ||| Type mismatch
82- StatusTypeMismatch : FdbStatus
82+ StatusTypeMismatch : LithStatus
8383 ||| Out of memory
84- StatusOutOfMemory : FdbStatus
84+ StatusOutOfMemory : LithStatus
8585 ||| I/O error
86- StatusIOError : FdbStatus
86+ StatusIOError : LithStatus
8787 ||| Corruption detected
88- StatusCorruption : FdbStatus
88+ StatusCorruption : LithStatus
8989 ||| Transaction conflict (optimistic concurrency control)
90- StatusConflict : FdbStatus
90+ StatusConflict : LithStatus
9191 ||| Internal error
92- StatusInternalError : FdbStatus
92+ StatusInternalError : LithStatus
9393
9494||| Convert status to integer for FFI
9595public export
96- statusToInt : FdbStatus -> Int32
96+ statusToInt : LithStatus -> Int32
9797statusToInt StatusOk = 0
9898statusToInt StatusInvalidArg = 1
9999statusToInt StatusNotFound = 2
@@ -314,21 +314,21 @@ record Migration where
314314
315315||| Result type for FFI operations
316316public export
317- record FdbResult (a : Type ) where
318- constructor MkFdbResult
319- status : FdbStatus
317+ record LithResult (a : Type ) where
318+ constructor MkLithResult
319+ status : LithStatus
320320 value : Maybe a
321321 errorMessage : Maybe String
322322
323323||| Smart constructor for success result
324324public export
325- ok : a -> FdbResult a
326- ok v = MkFdbResult StatusOk (Just v) Nothing
325+ ok : a -> LithResult a
326+ ok v = MkLithResult StatusOk (Just v) Nothing
327327
328328||| Smart constructor for error result
329329public export
330- err : FdbStatus -> String -> FdbResult a
331- err s msg = MkFdbResult s Nothing (Just msg)
330+ err : LithStatus -> String -> LithResult a
331+ err s msg = MkLithResult s Nothing (Just msg)
332332
333333-- ------------------------------------------------------------------------------
334334-- Integration with Proven Library
@@ -371,7 +371,7 @@ validateDbPath path =
371371 else if isPrefixOf " /" path then Nothing
372372 else Just path
373373
374- ||| Validate FQL query using inline checks.
374+ ||| Validate GQL query using inline checks.
375375||| Returns Nothing if the query is invalid, or Just the validated query.
376376||| Checks: non-empty, no obvious injection patterns (semicolons, comment
377377||| markers, DROP/DELETE keywords in uppercase).
0 commit comments