|
| 1 | +-- SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +-- |
| 4 | +||| Gnosis API ABI Types |
| 5 | +||| |
| 6 | +||| Dependent type definitions for the Gnosis stateful artefacts rendering API. |
| 7 | +||| These types prove correctness of the API contract at compile-time. |
| 8 | +||| |
| 9 | +||| The Gnosis API exposes three operations across all three interfaces |
| 10 | +||| (REST, gRPC, GraphQL): |
| 11 | +||| 1. Render — hydrate a template against 6scm context |
| 12 | +||| 2. Context — dump all resolved keys from 6scm files |
| 13 | +||| 3. Health — check engine availability |
| 14 | + |
| 15 | +module Gnosis.ABI.Types |
| 16 | + |
| 17 | +import Data.So |
| 18 | +import Data.Vect |
| 19 | + |
| 20 | +%default total |
| 21 | + |
| 22 | +-------------------------------------------------------------------------------- |
| 23 | +-- Render Mode |
| 24 | +-------------------------------------------------------------------------------- |
| 25 | + |
| 26 | +||| Render mode determines output format. |
| 27 | +public export |
| 28 | +data RenderMode = Plain | Badges |
| 29 | + |
| 30 | +||| Proof that render mode is one of exactly two values. |
| 31 | +public export |
| 32 | +renderModeExhaustive : (m : RenderMode) -> Either (m = Plain) (m = Badges) |
| 33 | +renderModeExhaustive Plain = Left Refl |
| 34 | +renderModeExhaustive Badges = Right Refl |
| 35 | + |
| 36 | +-------------------------------------------------------------------------------- |
| 37 | +-- Request Types |
| 38 | +-------------------------------------------------------------------------------- |
| 39 | + |
| 40 | +||| A render request must have either a template body or a template path. |
| 41 | +||| This is enforced at the type level. |
| 42 | +public export |
| 43 | +data TemplateSource |
| 44 | + = Inline (body : String) |
| 45 | + | FromFile (path : String) |
| 46 | + |
| 47 | +||| Proof that a template source is non-empty. |
| 48 | +public export |
| 49 | +data NonEmptySource : TemplateSource -> Type where |
| 50 | + InlineNonEmpty : So (length body > 0) -> NonEmptySource (Inline body) |
| 51 | + FileNonEmpty : So (length path > 0) -> NonEmptySource (FromFile path) |
| 52 | + |
| 53 | +||| A validated render request. |
| 54 | +public export |
| 55 | +record RenderRequest where |
| 56 | + constructor MkRenderRequest |
| 57 | + source : TemplateSource |
| 58 | + scmPath : String |
| 59 | + mode : RenderMode |
| 60 | + {auto 0 sourceValid : NonEmptySource source} |
| 61 | + |
| 62 | +||| A context dump request requires a valid SCM path. |
| 63 | +public export |
| 64 | +record ContextRequest where |
| 65 | + constructor MkContextRequest |
| 66 | + scmPath : String |
| 67 | + |
| 68 | +-------------------------------------------------------------------------------- |
| 69 | +-- Response Types |
| 70 | +-------------------------------------------------------------------------------- |
| 71 | + |
| 72 | +||| Result of a successful render operation. |
| 73 | +public export |
| 74 | +record RenderResponse where |
| 75 | + constructor MkRenderResponse |
| 76 | + output : String |
| 77 | + keysCount : Nat |
| 78 | + |
| 79 | +||| A single context entry (key-value pair from 6scm). |
| 80 | +public export |
| 81 | +record ContextEntry where |
| 82 | + constructor MkContextEntry |
| 83 | + key : String |
| 84 | + value : String |
| 85 | + |
| 86 | +||| Result of a context dump. |
| 87 | +public export |
| 88 | +record ContextResponse where |
| 89 | + constructor MkContextResponse |
| 90 | + entries : List ContextEntry |
| 91 | + count : Nat |
| 92 | + {auto 0 countCorrect : count = length entries} |
| 93 | + |
| 94 | +||| Health check result. |
| 95 | +public export |
| 96 | +data HealthStatus = Serving | NotServing |
| 97 | + |
| 98 | +||| Proof that health status maps to gRPC standard. |
| 99 | +public export |
| 100 | +healthStatusString : HealthStatus -> String |
| 101 | +healthStatusString Serving = "SERVING" |
| 102 | +healthStatusString NotServing = "NOT_SERVING" |
| 103 | + |
| 104 | +public export |
| 105 | +record HealthResponse where |
| 106 | + constructor MkHealthResponse |
| 107 | + status : HealthStatus |
| 108 | + version : String |
| 109 | + |
| 110 | +-------------------------------------------------------------------------------- |
| 111 | +-- API Contract |
| 112 | +-------------------------------------------------------------------------------- |
| 113 | + |
| 114 | +||| The Gnosis API contract: every operation returns a well-typed response. |
| 115 | +||| This interface is implemented by all three transports (REST, gRPC, GraphQL). |
| 116 | +public export |
| 117 | +interface GnosisAPI (m : Type -> Type) where |
| 118 | + render : RenderRequest -> m (Either String RenderResponse) |
| 119 | + context : ContextRequest -> m (Either String ContextResponse) |
| 120 | + health : m HealthResponse |
| 121 | + |
| 122 | +||| Proof that a render response with keysCount > 0 means the engine found data. |
| 123 | +public export |
| 124 | +renderFoundData : (resp : RenderResponse) -> So (resp.keysCount > 0) -> So (length resp.output > 0) |
| 125 | +renderFoundData resp prf = ?renderFoundDataProof |
| 126 | + |
| 127 | +-------------------------------------------------------------------------------- |
| 128 | +-- Transport Identifiers |
| 129 | +-------------------------------------------------------------------------------- |
| 130 | + |
| 131 | +||| The three API transports, each on a consecutive port. |
| 132 | +public export |
| 133 | +data Transport = REST | GRPC | GraphQL |
| 134 | + |
| 135 | +||| Port offset for each transport. |
| 136 | +public export |
| 137 | +portOffset : Transport -> Nat |
| 138 | +portOffset REST = 1 |
| 139 | +portOffset GRPC = 2 |
| 140 | +portOffset GraphQL = 3 |
| 141 | + |
| 142 | +||| Proof that all transports have distinct offsets. |
| 143 | +public export |
| 144 | +transportDistinct : (a : Transport) -> (b : Transport) -> Not (a = b) -> Not (portOffset a = portOffset b) |
| 145 | +transportDistinct REST REST contra = absurd (contra Refl) |
| 146 | +transportDistinct REST GRPC _ = \h => absurd h |
| 147 | +transportDistinct REST GraphQL _ = \h => absurd h |
| 148 | +transportDistinct GRPC REST _ = \h => absurd h |
| 149 | +transportDistinct GRPC GRPC contra = absurd (contra Refl) |
| 150 | +transportDistinct GRPC GraphQL _ = \h => absurd h |
| 151 | +transportDistinct GraphQL REST _ = \h => absurd h |
| 152 | +transportDistinct GraphQL GRPC _ = \h => absurd h |
| 153 | +transportDistinct GraphQL GraphQL contra = absurd (contra Refl) |
0 commit comments