necoherence/semantic_composition

Types

AvailableValue

pub type AvailableValue {
  AvailableValue(
    producer: ProducerRef,
    contract: semantic_types.SlotContract,
    resource: option.Option(ResourceLotRef),
  )
}

Constructors

AvailableValue(
  producer: ProducerRef,
  contract: semantic_types.SlotContract,
  resource: option.Option(ResourceLotRef),
)

BindingCompatibility

</>

pub type BindingCompatibility {
  Inclusion(certificate: InclusionCertificate)
  SuppliedBindingValue(
    value: semantic_types.SlotValue(exact_json.JsonValue),
  )
}

Constructors

Inclusion(certificate: InclusionCertificate)

SuppliedBindingValue(
  value: semantic_types.SlotValue(exact_json.JsonValue),
)

BindingExpr

</>

pub type BindingExpr {
  Source(
    value: ValueRef,
    projection: semantic_validation.ProjectionCertificate,
    compatibility: BindingCompatibility,
  )
  Product(
    construction: String,
    type_ref: semantic_types.TypeRef,
    fields: List(#(String, BindingExpr)),
  )
}

Constructors

Source(
  value: ValueRef,
  projection: semantic_validation.ProjectionCertificate,
  compatibility: BindingCompatibility,
)

Product(
  construction: String,
  type_ref: semantic_types.TypeRef,
  fields: List(#(String, BindingExpr)),
)

BranchFact

</>

pub type BranchFact {
  BranchFact(
    guard: GuardId,
    inspected: ValueRef,
    arm: GuardArm,
    refinement: option.Option(semantic_types.SlotContract),
    assumptions: List(semantic_validation.ProjectionAssumption),
    exact: option.Option(
      semantic_types.SlotValue(exact_json.JsonValue),
    ),
  )
}

Constructors

BranchFact(
  guard: GuardId,
  inspected: ValueRef,
  arm: GuardArm,
  refinement: option.Option(semantic_types.SlotContract),
  assumptions: List(semantic_validation.ProjectionAssumption),
  exact: option.Option(
    semantic_types.SlotValue(exact_json.JsonValue),
  ),
)

BranchTrace

</>

pub type BranchTrace {
  BranchTrace(steps: List(TraceStep), terminal: ReturnPlan)
}

Constructors

BranchTrace(steps: List(TraceStep), terminal: ReturnPlan)

CandidateBudget

</>

pub type CandidateBudget {
  CandidateBudget(
    bindings: Int,
    branch_nodes: Int,
    exhausted_bindings: Bool,
    exhausted_branches: Bool,
  )
}

Constructors

CandidateBudget(
  bindings: Int,
  branch_nodes: Int,
  exhausted_bindings: Bool,
  exhausted_branches: Bool,
)

CandidateTree

</>

pub type CandidateTree {
  CandidateTree(
    tree: PlanTree,
    success: Bool,
    certificates: List(ResourceTraceCertificate),
    nodes: Int,
  )
}

Constructors

CandidateTree(
  tree: PlanTree,
  success: Bool,
  certificates: List(ResourceTraceCertificate),
  nodes: Int,
)

CheckedAcyclic

opaque </>

pub opaque type CheckedAcyclic

CheckedClosure

opaque </>

pub opaque type CheckedClosure

CheckedComposition

opaque </>

pub opaque type CheckedComposition

CheckedCompositionClosure

opaque </>

pub opaque type CheckedCompositionClosure

CheckedInclusion

opaque </>

pub opaque type CheckedInclusion

CheckedReachability

opaque </>

pub opaque type CheckedReachability

ChoiceCoverage

</>

pub type ChoiceCoverage {
  ChoiceCoverage(choice: ChoiceSkeleton, children: List(Int))
}

Constructors

ChoiceCoverage(choice: ChoiceSkeleton, children: List(Int))

ChoiceSkeleton

</>

pub type ChoiceSkeleton {
  InvocationChoice(
    invocation: InvocationPlan,
    outcomes: List(OutcomeId),
    empty_outcomes: List(OutcomeId),
  )
  GuardChoice(
    guard: GuardId,
    inspected: ValueRef,
    arms: List(GuardArm),
  )
}

Constructors

InvocationChoice(
  invocation: InvocationPlan,
  outcomes: List(OutcomeId),
  empty_outcomes: List(OutcomeId),
)

GuardChoice(
  guard: GuardId,
  inspected: ValueRef,
  arms: List(GuardArm),
)

ClosedSearchState

</>

pub type ClosedSearchState {
  ClosedSearchState(
    state: SearchState,
    terminals: List(TerminalCoverage),
    choices: List(ChoiceCoverage),
    rejected_connections: List(ConnectionFailure),
    missing_supply: List(MissingSupply),
  )
}

Constructors

ClosedSearchState(
  state: SearchState,
  terminals: List(TerminalCoverage),
  choices: List(ChoiceCoverage),
  rejected_connections: List(ConnectionFailure),
  missing_supply: List(MissingSupply),
)

CompatibilityDecision

</>

pub type CompatibilityDecision {
  Compatible(certificate: InclusionCertificate)
  Incompatible(certificate: CounterexampleCertificate)
  CompatibilityUnknown(obligations: List(TypeObligation))
}

Constructors

Compatible(certificate: InclusionCertificate)

Incompatible(certificate: CounterexampleCertificate)

CompatibilityUnknown(obligations: List(TypeObligation))

CompositionClosureWitness

</>

pub type CompositionClosureWitness {
  CompositionClosureWitness(
    input_snapshot: CompositionInput,
    root: Int,
    states: List(ClosedSearchState),
  )
}

Constructors

CompositionClosureWitness(
  input_snapshot: CompositionInput,
  root: Int,
  states: List(ClosedSearchState),
)

CompositionDecision

</>

pub type CompositionDecision {
  Solved(
    composition: CheckedComposition,
    selection: SelectionEvidence,
  )
  Unreachable(closure: CompositionClosureWitness)
  CompositionUnknown(
    obligations: List(UnresolvedObligation),
    frontier: List(SearchState),
    rejected_connections: List(ConnectionFailure),
  )
  Ambiguous(
    candidates: List(VerifiedCompositionCandidate),
    canonical_plans: List(String),
  )
}

Constructors

Solved(
  composition: CheckedComposition,
  selection: SelectionEvidence,
)

Unreachable(closure: CompositionClosureWitness)

CompositionUnknown(
  obligations: List(UnresolvedObligation),
  frontier: List(SearchState),
  rejected_connections: List(ConnectionFailure),
)

Ambiguous(
  candidates: List(VerifiedCompositionCandidate),
  canonical_plans: List(String),
)

CompositionEffect

</>

pub type CompositionEffect {
  PureFunction
  HttpRequestResponse
  DataOnly
}

Constructors

```
PureFunction
```
```
HttpRequestResponse
```
```
DataOnly
```

CompositionEngineFailure

</>

pub type CompositionEngineFailure {
  ContractViolation(reason: String)
  ResourceFailure(failure: typed_mapping.SolverFailure)
  Witness(failure: WitnessFailure)
}

Constructors

```
ContractViolation(reason: String)
```

ResourceFailure(failure: typed_mapping.SolverFailure)

```
Witness(failure: WitnessFailure)
```

CompositionInput

</>

pub type CompositionInput {
  CompositionInput(
    identity: String,
    revision: String,
    basis: SemanticBasis,
    signatures: List(FunctionSignature),
    initial_inputs: List(InitialInput),
    initial_resources: List(ResourceLot),
    goal: GoalSpec,
    invocation_domain: InvocationDomain,
    allowed_effects: List(CompositionEffect),
    explicit_order: List(#(SiteId, SiteId)),
    selection_policy: option.Option(SelectionPolicy),
    bounds: SearchBounds,
  )
}

Constructors

CompositionInput(
  identity: String,
  revision: String,
  basis: SemanticBasis,
  signatures: List(FunctionSignature),
  initial_inputs: List(InitialInput),
  initial_resources: List(ResourceLot),
  goal: GoalSpec,
  invocation_domain: InvocationDomain,
  allowed_effects: List(CompositionEffect),
  explicit_order: List(#(SiteId, SiteId)),
  selection_policy: option.Option(SelectionPolicy),
  bounds: SearchBounds,
)

CompositionInputFailure

</>

pub type CompositionInputFailure {
  InputBasisMismatch
  DuplicateIdentity(kind: String, identity: String)
  UnresolvedType(reference: semantic_types.TypeRef)
  UnresolvedFunction(reference: FunctionRef)
  InvalidSignature(function: FunctionRef, reason: String)
  InvalidInitialValue(
    input: InputId,
    failure: semantic_types.ValueFailure,
  )
  InvalidInitialCertificate(input: InputId, condition: String)
  InvalidInvocationDomain(reason: String)
  InvalidResourceDeclaration(reason: String)
  InvalidBound(reason: String)
  OperationEffectMismatch(
    operation: semantic_types.DefinitionRef,
    expected: CompositionEffect,
    supplied: CompositionEffect,
  )
}

Constructors

```
InputBasisMismatch
```

DuplicateIdentity(kind: String, identity: String)

UnresolvedType(reference: semantic_types.TypeRef)

UnresolvedFunction(reference: FunctionRef)

InvalidSignature(function: FunctionRef, reason: String)

InvalidInitialValue(
  input: InputId,
  failure: semantic_types.ValueFailure,
)

InvalidInitialCertificate(input: InputId, condition: String)

```
InvalidInvocationDomain(reason: String)
```

InvalidResourceDeclaration(reason: String)

```
InvalidBound(reason: String)
```

OperationEffectMismatch(
  operation: semantic_types.DefinitionRef,
  expected: CompositionEffect,
  supplied: CompositionEffect,
)

CompositionPlan

</>

pub type CompositionPlan {
  CompositionPlan(
    input_identity: String,
    input_revision: String,
    root: PlanTree,
  )
}

Constructors

CompositionPlan(
  input_identity: String,
  input_revision: String,
  root: PlanTree,
)

CompositionWitness

</>

pub type CompositionWitness {
  CompositionWitness(
    input_snapshot: CompositionInput,
    initial_membership: List(
      #(InputId, semantic_types.SlotValue(exact_json.JsonValue)),
    ),
    resource_traces: List(ResourceTraceCertificate),
  )
}

Constructors

CompositionWitness(
  input_snapshot: CompositionInput,
  initial_membership: List(
    #(InputId, semantic_types.SlotValue(exact_json.JsonValue)),
  ),
  resource_traces: List(ResourceTraceCertificate),
)

ConnectionFailure

</>

pub type ConnectionFailure {
  ConnectionFailure(
    value: option.Option(ValueRef),
    destination: semantic_types.SlotContract,
    counterexample: CounterexampleCertificate,
  )
}

Constructors

ConnectionFailure(
  value: option.Option(ValueRef),
  destination: semantic_types.SlotContract,
  counterexample: CounterexampleCertificate,
)

ConstructionRule

</>

pub type ConstructionRule {
  ConstructionRule(
    identity: String,
    type_ref: semantic_types.TypeRef,
    nested_fields: List(#(String, String)),
    field_constraints: List(FieldConstraint),
  )
}

Constructors

ConstructionRule(
  identity: String,
  type_ref: semantic_types.TypeRef,
  nested_fields: List(#(String, String)),
  field_constraints: List(FieldConstraint),
)

CounterexampleCertificate

</>

pub type CounterexampleCertificate {
  CounterexampleCertificate(
    basis: SemanticBasis,
    source: semantic_types.SlotContract,
    destination: semantic_types.SlotContract,
    value: semantic_types.SlotValue(exact_json.JsonValue),
    destination_failure: semantic_types.ValueFailure,
  )
}

Constructors

CounterexampleCertificate(
  basis: SemanticBasis,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  value: semantic_types.SlotValue(exact_json.JsonValue),
  destination_failure: semantic_types.ValueFailure,
)

DeclaredGuard

</>

pub type DeclaredGuard {
  DeclaredGuard(
    id: GuardId,
    source_type: semantic_types.TypeRef,
    path: List(semantic_types.PathStep),
    kind: GuardKind,
  )
}

Constructors

DeclaredGuard(
  id: GuardId,
  source_type: semantic_types.TypeRef,
  path: List(semantic_types.PathStep),
  kind: GuardKind,
)

Enumeration

</>

pub type Enumeration {
  Enumeration(
    terminals: List(ReturnPlan),
    choices: List(ChoiceSkeleton),
    unknown: List(UnresolvedObligation),
    failures: List(ConnectionFailure),
    missing: List(MissingSupply),
    budget: CandidateBudget,
  )
}

Constructors

Enumeration(
  terminals: List(ReturnPlan),
  choices: List(ChoiceSkeleton),
  unknown: List(UnresolvedObligation),
  failures: List(ConnectionFailure),
  missing: List(MissingSupply),
  budget: CandidateBudget,
)

FailureEmbedding

</>

pub type FailureEmbedding {
  FailureEmbedding(
    id: FailureEmbeddingId,
    origin: FailureOrigin,
    contract: semantic_types.SlotContract,
    final_resources: List(ResourceGoal),
  )
}

Constructors

FailureEmbedding(
  id: FailureEmbeddingId,
  origin: FailureOrigin,
  contract: semantic_types.SlotContract,
  final_resources: List(ResourceGoal),
)

FailureEmbeddingId

</>

pub type FailureEmbeddingId {
  FailureEmbeddingId(value: String)
}

Constructors

```
FailureEmbeddingId(value: String)
```

FailureOrigin

</>

pub type FailureOrigin {
  FunctionFailure(function: FunctionRef, outcome: OutcomeId)
  GuardFailure(guard: GuardId, arm: GuardArm)
}

Constructors

FunctionFailure(function: FunctionRef, outcome: OutcomeId)

GuardFailure(guard: GuardId, arm: GuardArm)

FieldConstraint

</>

pub type FieldConstraint {
  FieldConstraint(
    field: String,
    source: SourceConstraint,
    presence: FieldPresence,
  )
}

Constructors

FieldConstraint(
  field: String,
  source: SourceConstraint,
  presence: FieldPresence,
)

FieldPresence

</>

pub type FieldPresence {
  Required
  Optional
}

Constructors

```
Required
```
```
Optional
```

FunctionForm

</>

pub type FunctionForm {
  Pure
  Operation(reference: semantic_types.DefinitionRef)
  DeclaredTransform
}

Constructors

```
Pure
```

Operation(reference: semantic_types.DefinitionRef)

```
DeclaredTransform
```

FunctionRef

</>

pub type FunctionRef {
  FunctionRef(
    identity: String,
    revision: String,
    content_digest: String,
  )
}

Constructors

FunctionRef(
  identity: String,
  revision: String,
  content_digest: String,
)

FunctionSignature

</>

pub type FunctionSignature {
  FunctionSignature(
    reference: FunctionRef,
    form: FunctionForm,
    effect: CompositionEffect,
    inputs: List(InputPort),
    outcomes: List(OutcomeContract),
    resource_inputs: List(ResourceRequirement),
    assumption_ref: String,
    handles_failure: option.Option(FailureOrigin),
  )
}

Constructors

FunctionSignature(
  reference: FunctionRef,
  form: FunctionForm,
  effect: CompositionEffect,
  inputs: List(InputPort),
  outcomes: List(OutcomeContract),
  resource_inputs: List(ResourceRequirement),
  assumption_ref: String,
  handles_failure: option.Option(FailureOrigin),
)

GoalPort

</>

pub type GoalPort {
  GoalPort(
    id: GoalPortId,
    contract: semantic_types.SlotContract,
    source_constraint: SourceConstraint,
  )
}

Constructors

GoalPort(
  id: GoalPortId,
  contract: semantic_types.SlotContract,
  source_constraint: SourceConstraint,
)

GoalPortId

</>

pub type GoalPortId {
  GoalPortId(value: String)
}

Constructors

```
GoalPortId(value: String)
```

GoalSpec

</>

pub type GoalSpec {
  GoalSpec(
    outputs: List(GoalPort),
    failures: List(FailureEmbedding),
    final_resources: List(ResourceGoal),
  )
}

Constructors

GoalSpec(
  outputs: List(GoalPort),
  failures: List(FailureEmbedding),
  final_resources: List(ResourceGoal),
)

GuardArm

</>

pub type GuardArm {
  GuardPresent
  GuardAbsent
  GuardNull
  GuardVariant(tag: String)
  UnknownVariant
  GuardAccepted
  GuardRejected
}

Constructors

```
GuardPresent
```
```
GuardAbsent
```
```
GuardNull
```
```
GuardVariant(tag: String)
```
```
UnknownVariant
```
```
GuardAccepted
```
```
GuardRejected
```

GuardId

</>

pub type GuardId {
  GuardId(value: String)
}

Constructors

```
GuardId(value: String)
```

GuardKind

</>

pub type GuardKind {
  Presence
  Variants
  Validate(contract: semantic_types.SlotContract)
}

Constructors

```
Presence
```
```
Variants
```

Validate(contract: semantic_types.SlotContract)

InclusionCertificate

</>

pub type InclusionCertificate {
  InclusionCertificate(
    basis: SemanticBasis,
    source: semantic_types.SlotContract,
    destination: semantic_types.SlotContract,
    root: Int,
    empty_types: List(semantic_types.TypeRef),
    pairs: List(PairEntry),
  )
}

Constructors

InclusionCertificate(
  basis: SemanticBasis,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  root: Int,
  empty_types: List(semantic_types.TypeRef),
  pairs: List(PairEntry),
)

InclusionFailure

</>

pub type InclusionFailure {
  InclusionBasisMismatch
  ContractMismatch
  UndefinedMeaning(
    obligations: List(semantic_types.SemanticObligation),
  )
  MissingPair
  PairMismatch(index: Int)
  RuleMismatch(index: Int)
  ChildCoverage(index: Int)
  ForgedEmptiness
  CounterexampleMismatch
  InclusionUnresolved(obligation: TypeObligation)
}

Constructors

```
InclusionBasisMismatch
```
```
ContractMismatch
```

UndefinedMeaning(
  obligations: List(semantic_types.SemanticObligation),
)

```
MissingPair
```
```
PairMismatch(index: Int)
```
```
RuleMismatch(index: Int)
```
```
ChildCoverage(index: Int)
```
```
ForgedEmptiness
```
```
CounterexampleMismatch
```

InclusionUnresolved(obligation: TypeObligation)

InclusionRule

</>

pub type InclusionRule {
  EmptySource
  InclusionBoolean
  IntegerIntersection
  FiniteStrings
  StringConditions
  BytesLength
  InclusionUnit
  JsonDomain
  PlainObjectDomain
  UnfoldSource
  UnfoldDestination
  InclusionArray
  InclusionProduct
  SourceUnion
  DestinationUnion
  SourceRecord
  DestinationRecord
  ProductTagCases
}

Constructors

```
EmptySource
```
```
InclusionBoolean
```
```
IntegerIntersection
```
```
FiniteStrings
```
```
StringConditions
```
```
BytesLength
```
```
InclusionUnit
```
```
JsonDomain
```
```
PlainObjectDomain
```
```
UnfoldSource
```
```
UnfoldDestination
```
```
InclusionArray
```
```
InclusionProduct
```
```
SourceUnion
```
```
DestinationUnion
```
```
SourceRecord
```
```
DestinationRecord
```
```
ProductTagCases
```

InitialInput

</>

pub type InitialInput {
  InitialInput(
    id: InputId,
    contract: semantic_types.SlotContract,
    source: InitialSource,
    resource: option.Option(LotId),
  )
}

Constructors

InitialInput(
  id: InputId,
  contract: semantic_types.SlotContract,
  source: InitialSource,
  resource: option.Option(LotId),
)

InitialSource

</>

pub type InitialSource {
  Argument
  SuppliedValue(
    value: semantic_types.SlotValue(exact_json.JsonValue),
  )
}

Constructors

```
Argument
```

SuppliedValue(
  value: semantic_types.SlotValue(exact_json.JsonValue),
)

InputId

</>

pub type InputId {
  InputId(value: String)
}

Constructors

```
InputId(value: String)
```

InputPort

</>

pub type InputPort {
  InputPort(
    id: PortId,
    contract: semantic_types.SlotContract,
    source_constraint: SourceConstraint,
    resource_requirement: option.Option(RequirementId),
  )
}

Constructors

InputPort(
  id: PortId,
  contract: semantic_types.SlotContract,
  source_constraint: SourceConstraint,
  resource_requirement: option.Option(RequirementId),
)

InvocationDomain

</>

pub type InvocationDomain {
  InvocationDomain(
    identity: String,
    revision: String,
    sites: List(InvocationSite),
    permitted_projections: List(PermittedProjection),
    permitted_constructions: List(ConstructionRule),
    permitted_transforms: List(FunctionRef),
    guards: List(DeclaredGuard),
  )
}

Constructors

InvocationDomain(
  identity: String,
  revision: String,
  sites: List(InvocationSite),
  permitted_projections: List(PermittedProjection),
  permitted_constructions: List(ConstructionRule),
  permitted_transforms: List(FunctionRef),
  guards: List(DeclaredGuard),
)

InvocationPlan

</>

pub type InvocationPlan {
  InvocationPlan(
    site: SiteId,
    function: FunctionRef,
    bindings: List(#(PortId, BindingExpr)),
    resources: List(ResourceBinding),
  )
}

Constructors

InvocationPlan(
  site: SiteId,
  function: FunctionRef,
  bindings: List(#(PortId, BindingExpr)),
  resources: List(ResourceBinding),
)

InvocationSite

</>

pub type InvocationSite {
  InvocationSite(id: SiteId, function: FunctionRef)
}

Constructors

InvocationSite(id: SiteId, function: FunctionRef)

LotId

</>

pub type LotId {
  LotId(value: String)
}

Constructors

```
LotId(value: String)
```

LoweringFailure

</>

pub type LoweringFailure {
  InvalidLowering(reason: String)
  UnknownLowering(obligation: UnresolvedObligation)
}

Constructors

```
InvalidLowering(reason: String)
```

UnknownLowering(obligation: UnresolvedObligation)

MissingSupply

</>

pub type MissingSupply {
  MissingSupply(
    site: option.Option(SiteId),
    port: String,
    contract: semantic_types.SlotContract,
  )
}

Constructors

MissingSupply(
  site: option.Option(SiteId),
  port: String,
  contract: semantic_types.SlotContract,
)

NormalizedResourceBinding

</>

pub type NormalizedResourceBinding {
  NormalizedResourceBinding(
    transition: String,
    lot: ResourceLotRef,
    read: Int,
    consume: Int,
    required_revision: Int,
  )
}

Constructors

NormalizedResourceBinding(
  transition: String,
  lot: ResourceLotRef,
  read: Int,
  consume: Int,
  required_revision: Int,
)

OutcomeContract

</>

pub type OutcomeContract {
  OutcomeContract(
    id: OutcomeId,
    form: OutcomeForm,
    value_ports: List(OutputPort),
    produced_resources: List(ResourceProduction),
  )
}

Constructors

OutcomeContract(
  id: OutcomeId,
  form: OutcomeForm,
  value_ports: List(OutputPort),
  produced_resources: List(ResourceProduction),
)

OutcomeForm

</>

pub type OutcomeForm {
  Success
  DeclaredFailure
}

Constructors

```
Success
```
```
DeclaredFailure
```

OutcomeId

</>

pub type OutcomeId {
  OutcomeId(value: String)
}

Constructors

```
OutcomeId(value: String)
```

OutputPort

</>

pub type OutputPort {
  OutputPort(
    id: PortId,
    contract: semantic_types.SlotContract,
    resource_production: option.Option(ProductionId),
  )
}

Constructors

OutputPort(
  id: PortId,
  contract: semantic_types.SlotContract,
  resource_production: option.Option(ProductionId),
)

PairEntry

</>

pub type PairEntry {
  PairEntry(
    pair: TypePair,
    source_shape: semantic_types.TypeShape,
    destination_shape: semantic_types.TypeShape,
    rule: InclusionRule,
    children: List(Int),
  )
}

Constructors

PairEntry(
  pair: TypePair,
  source_shape: semantic_types.TypeShape,
  destination_shape: semantic_types.TypeShape,
  rule: InclusionRule,
  children: List(Int),
)

PermittedProjection

</>

pub type PermittedProjection {
  PermittedProjection(
    source_type: semantic_types.TypeRef,
    path: List(semantic_types.PathStep),
  )
}

Constructors

PermittedProjection(
  source_type: semantic_types.TypeRef,
  path: List(semantic_types.PathStep),
)

PlanNode

</>

pub type PlanNode {
  Invoke(
    invocation: InvocationPlan,
    arms: List(#(OutcomeId, PlanTree)),
    empty_outcomes: List(OutcomeId),
  )
  Guard(
    guard: GuardId,
    inspected: ValueRef,
    arms: List(#(GuardArm, PlanTree)),
  )
  Return(terminal: ReturnPlan)
}

Constructors

Invoke(
  invocation: InvocationPlan,
  arms: List(#(OutcomeId, PlanTree)),
  empty_outcomes: List(OutcomeId),
)

Guard(
  guard: GuardId,
  inspected: ValueRef,
  arms: List(#(GuardArm, PlanTree)),
)

```
Return(terminal: ReturnPlan)
```

PlanTree

</>

pub type PlanTree {
  PlanTree(rank: Int, node: PlanNode)
}

Constructors

```
PlanTree(rank: Int, node: PlanNode)
```

PortId

</>

pub type PortId {
  PortId(value: String)
}

Constructors

```
PortId(value: String)
```

PreparedCompositionInput

opaque </>

pub opaque type PreparedCompositionInput

ProducerRef

</>

pub type ProducerRef {
  Initial(id: InputId)
  InvocationOutcome(
    site: SiteId,
    outcome: OutcomeId,
    port: PortId,
  )
}

Constructors

```
Initial(id: InputId)
```

InvocationOutcome(site: SiteId, outcome: OutcomeId, port: PortId)

ProductionId

</>

pub type ProductionId {
  ProductionId(value: String)
}

Constructors

```
ProductionId(value: String)
```

RawComposition

</>

pub type RawComposition {
  RawComposition(
    plan: CompositionPlan,
    witness: CompositionWitness,
    selection: SelectionEvidence,
  )
}

Constructors

RawComposition(
  plan: CompositionPlan,
  witness: CompositionWitness,
  selection: SelectionEvidence,
)

RequirementId

</>

pub type RequirementId {
  RequirementId(value: String)
}

Constructors

```
RequirementId(value: String)
```

ResourceBinding

</>

pub type ResourceBinding {
  ResourceBinding(
    requirement: RequirementId,
    lot: ResourceLotRef,
    inclusion: InclusionCertificate,
  )
}

Constructors

ResourceBinding(
  requirement: RequirementId,
  lot: ResourceLotRef,
  inclusion: InclusionCertificate,
)

ResourceBounds

</>

pub type ResourceBounds {
  ResourceBounds(
    max_bindings: Int,
    max_search_steps: Int,
    max_tokens: Int,
  )
}

Constructors

ResourceBounds(
  max_bindings: Int,
  max_search_steps: Int,
  max_tokens: Int,
)

ResourceCorrespondence

</>

pub type ResourceCorrespondence {
  ResourceCorrespondence(
    lots: List(ResourceLotCorrespondence),
    values: List(ValueCorrespondence),
    normalized_bindings: List(NormalizedResourceBinding),
    execution_order: List(String),
  )
}

Constructors

ResourceCorrespondence(
  lots: List(ResourceLotCorrespondence),
  values: List(ValueCorrespondence),
  normalized_bindings: List(NormalizedResourceBinding),
  execution_order: List(String),
)

ResourceGoal

</>

pub type ResourceGoal {
  ResourceGoal(
    lot: ResourceLotRef,
    multiplicity: Int,
    revision: Int,
  )
}

Constructors

ResourceGoal(
  lot: ResourceLotRef,
  multiplicity: Int,
  revision: Int,
)

ResourceIdentityConstraint

</>

pub type ResourceIdentityConstraint {
  AnyResource
  Exactly(producer: ResourceProducer)
}

Constructors

```
AnyResource
```
```
Exactly(producer: ResourceProducer)
```

ResourceLot

</>

pub type ResourceLot {
  ResourceLot(
    id: LotId,
    token_type: semantic_types.TypeRef,
    producer: ResourceProducer,
    revision: Int,
    quantity: Int,
    provenance: String,
  )
}

Constructors

ResourceLot(
  id: LotId,
  token_type: semantic_types.TypeRef,
  producer: ResourceProducer,
  revision: Int,
  quantity: Int,
  provenance: String,
)

ResourceLotCorrespondence

</>

pub type ResourceLotCorrespondence {
  ResourceLotCorrespondence(
    lot: ResourceLotRef,
    place: String,
    producer: ResourceProducer,
    token_target: String,
    token_type: String,
    revision: Int,
    quantity: Int,
    provenance: String,
  )
}

Constructors

ResourceLotCorrespondence(
  lot: ResourceLotRef,
  place: String,
  producer: ResourceProducer,
  token_target: String,
  token_type: String,
  revision: Int,
  quantity: Int,
  provenance: String,
)

ResourceLotRef

</>

pub type ResourceLotRef {
  InitialLot(id: LotId)
  ProducedLot(
    site: SiteId,
    outcome: OutcomeId,
    production: ProductionId,
  )
}

Constructors

```
InitialLot(id: LotId)
```

ProducedLot(
  site: SiteId,
  outcome: OutcomeId,
  production: ProductionId,
)

ResourceProducer

</>

pub type ResourceProducer {
  InitialResource(identity: String, revision: String)
  OutcomeResource(site: SiteId, outcome: OutcomeId)
}

Constructors

InitialResource(identity: String, revision: String)

OutcomeResource(site: SiteId, outcome: OutcomeId)

ResourceProduction

</>

pub type ResourceProduction {
  ResourceProduction(
    id: ProductionId,
    token_type: semantic_types.TypeRef,
    revision: Int,
    quantity: Int,
    provenance: String,
  )
}

Constructors

ResourceProduction(
  id: ProductionId,
  token_type: semantic_types.TypeRef,
  revision: Int,
  quantity: Int,
  provenance: String,
)

ResourceRequirement

</>

pub type ResourceRequirement {
  ResourceRequirement(
    id: RequirementId,
    token_type: semantic_types.TypeRef,
    mode: typed_mapping.BindingMode,
    multiplicity: Int,
    required_revision: Int,
    identity: ResourceIdentityConstraint,
  )
}

Constructors

ResourceRequirement(
  id: RequirementId,
  token_type: semantic_types.TypeRef,
  mode: typed_mapping.BindingMode,
  multiplicity: Int,
  required_revision: Int,
  identity: ResourceIdentityConstraint,
)

ResourceTraceCertificate

</>

pub type ResourceTraceCertificate {
  ResourceTraceCertificate(
    trace: BranchTrace,
    lowering: typed_mapping.SolverInput,
    correspondence: ResourceCorrespondence,
    reachability: typed_mapping.ReachabilityWitness,
    acyclicity: typed_mapping.AcyclicWitness,
    value_sources: List(
      #(
        ProducerRef,
        semantic_types.SlotValue(exact_json.JsonValue),
      ),
    ),
  )
}

Constructors

ResourceTraceCertificate(
  trace: BranchTrace,
  lowering: typed_mapping.SolverInput,
  correspondence: ResourceCorrespondence,
  reachability: typed_mapping.ReachabilityWitness,
  acyclicity: typed_mapping.AcyclicWitness,
  value_sources: List(
    #(ProducerRef, semantic_types.SlotValue(exact_json.JsonValue)),
  ),
)

ReturnPlan

</>

pub type ReturnPlan {
  ReturnSuccess(outputs: List(#(GoalPortId, BindingExpr)))
  ReturnFailure(
    embedding: FailureEmbeddingId,
    value: BindingExpr,
  )
}

Constructors

ReturnSuccess(outputs: List(#(GoalPortId, BindingExpr)))

ReturnFailure(embedding: FailureEmbeddingId, value: BindingExpr)

SampleObligation

</>

pub type SampleObligation {
  SampleBound
}

Constructors

```
SampleBound
```

SampleResult

</>

pub type SampleResult(a) {
  SampleResult(
    values: List(a),
    obligations: List(SampleObligation),
  )
}

Constructors

SampleResult(
  values: List(a),
  obligations: List(SampleObligation),
)

SearchBounds

</>

pub type SearchBounds {
  SearchBounds(
    max_expanded_states: Int,
    max_binding_candidates: Int,
    max_type_obligations: Int,
    max_branch_nodes: Int,
    resource_bounds: option.Option(ResourceBounds),
    max_sample_length: Int,
  )
}

Constructors

SearchBounds(
  max_expanded_states: Int,
  max_binding_candidates: Int,
  max_type_obligations: Int,
  max_branch_nodes: Int,
  resource_bounds: option.Option(ResourceBounds),
  max_sample_length: Int,
)

SearchState

</>

pub type SearchState {
  SearchState(
    available: List(AvailableValue),
    used_sites: List(SiteId),
    used_guards: List(GuardId),
    facts: List(BranchFact),
    trace: List(TraceStep),
    pending_failure: option.Option(FailureOrigin),
  )
}

Constructors

SearchState(
  available: List(AvailableValue),
  used_sites: List(SiteId),
  used_guards: List(GuardId),
  facts: List(BranchFact),
  trace: List(TraceStep),
  pending_failure: option.Option(FailureOrigin),
)

SelectionEvidence

</>

pub type SelectionEvidence {
  AnyFeasibleEvidence
  Unique(
    closure: CompositionClosureWitness,
    canonical_plan: String,
  )
}

Constructors

```
AnyFeasibleEvidence
```

Unique(
  closure: CompositionClosureWitness,
  canonical_plan: String,
)

SelectionPolicy

</>

pub type SelectionPolicy {
  RequireUnique
  AnyFeasible
}

Constructors

```
RequireUnique
```
```
AnyFeasible
```

SemanticBasis

</>

pub type SemanticBasis {
  SemanticBasis(
    profile: semantic_types.SemanticProfile,
    sources: List(semantic_types.SourceRef),
  )
}

Constructors

SemanticBasis(
  profile: semantic_types.SemanticProfile,
  sources: List(semantic_types.SourceRef),
)

SiteId

</>

pub type SiteId {
  SiteId(value: String)
}

Constructors

```
SiteId(value: String)
```

SourceConstraint

</>

pub type SourceConstraint {
  AnyCompatible
  InitialOnly(
    input: InputId,
    path: List(semantic_types.PathStep),
  )
  ProducedBy(
    site: SiteId,
    outcome: OutcomeId,
    port: PortId,
    path: List(semantic_types.PathStep),
  )
}

Constructors

```
AnyCompatible
```

InitialOnly(input: InputId, path: List(semantic_types.PathStep))

ProducedBy(
  site: SiteId,
  outcome: OutcomeId,
  port: PortId,
  path: List(semantic_types.PathStep),
)

TerminalAssessment

</>

pub type TerminalAssessment {
  Feasible(certificate: ResourceTraceCertificate)
  ResourceUnreachable(
    trace: BranchTrace,
    lowering: typed_mapping.SolverInput,
    correspondence: ResourceCorrespondence,
    closure: typed_mapping.ClosureWitness,
  )
  RejectedLowering(trace: BranchTrace, reason: String)
  EmptyValues(producers: List(ProducerRef))
  TerminalUnknown(obligations: List(UnresolvedObligation))
}

Constructors

Feasible(certificate: ResourceTraceCertificate)

ResourceUnreachable(
  trace: BranchTrace,
  lowering: typed_mapping.SolverInput,
  correspondence: ResourceCorrespondence,
  closure: typed_mapping.ClosureWitness,
)

RejectedLowering(trace: BranchTrace, reason: String)

EmptyValues(producers: List(ProducerRef))

TerminalUnknown(obligations: List(UnresolvedObligation))

TerminalCoverage

</>

pub type TerminalCoverage {
  TerminalCoverage(
    terminal: ReturnPlan,
    assessment: TerminalAssessment,
  )
}

Constructors

TerminalCoverage(
  terminal: ReturnPlan,
  assessment: TerminalAssessment,
)

TraceStep

</>

pub type TraceStep {
  InvocationStep(invocation: InvocationPlan, outcome: OutcomeId)
  GuardStep(guard: GuardId, inspected: ValueRef, arm: GuardArm)
}

Constructors

InvocationStep(invocation: InvocationPlan, outcome: OutcomeId)

GuardStep(guard: GuardId, inspected: ValueRef, arm: GuardArm)

TypeObligation

</>

pub type TypeObligation {
  TypeObligation(
    pair: TypePair,
    path: List(semantic_types.PathStep),
    reason: TypeObligationReason,
  )
}

Constructors

TypeObligation(
  pair: TypePair,
  path: List(semantic_types.PathStep),
  reason: TypeObligationReason,
)

TypeObligationReason

</>

pub type TypeObligationReason {
  TypeMeaning(
    obligations: List(semantic_types.SemanticObligation),
  )
  ConstraintImplication
  TypePresence
  UnionRemainder
  ExtraField(name: String)
  TypeInhabitation
  ObligationBoundExhausted
}

Constructors

TypeMeaning(obligations: List(semantic_types.SemanticObligation))

```
ConstraintImplication
```
```
TypePresence
```
```
UnionRemainder
```
```
ExtraField(name: String)
```
```
TypeInhabitation
```
```
ObligationBoundExhausted
```

TypePair

</>

pub type TypePair {
  TypePair(
    source: semantic_types.SlotContract,
    destination: semantic_types.SlotContract,
    source_tag: option.Option(String),
  )
}

Constructors

TypePair(
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  source_tag: option.Option(String),
)

UnresolvedObligation

</>

pub type UnresolvedObligation {
  UnresolvedTypeObligation(
    value: option.Option(ValueRef),
    obligations: List(TypeObligation),
  )
  UnresolvedMeaning(
    obligations: List(semantic_types.SemanticObligation),
  )
  InvalidValidationCertificate(condition: String)
  Inhabitation(
    producer: ProducerRef,
    contract: semantic_types.SlotContract,
  )
  BranchInhabitation
  StateBoundExhausted
  BindingBoundExhausted
  BranchBoundExhausted
  ResourceSolverUnknown(reason: typed_mapping.UnknownReason)
  ResourceCapacityBound(required: Int, limit: Int)
  UnresolvedUniqueness
}

Constructors

UnresolvedTypeObligation(
  value: option.Option(ValueRef),
  obligations: List(TypeObligation),
)

UnresolvedMeaning(
  obligations: List(semantic_types.SemanticObligation),
)

InvalidValidationCertificate(condition: String)

Inhabitation(
  producer: ProducerRef,
  contract: semantic_types.SlotContract,
)

```
BranchInhabitation
```
```
StateBoundExhausted
```
```
BindingBoundExhausted
```
```
BranchBoundExhausted
```

ResourceSolverUnknown(reason: typed_mapping.UnknownReason)

ResourceCapacityBound(required: Int, limit: Int)

```
UnresolvedUniqueness
```

ValueCorrespondence

</>

pub type ValueCorrespondence {
  ValueCorrespondence(
    producer: ProducerRef,
    place: String,
    token_target: String,
    revision: Int,
  )
}

Constructors

ValueCorrespondence(
  producer: ProducerRef,
  place: String,
  token_target: String,
  revision: Int,
)

ValueRef

</>

pub type ValueRef {
  ValueRef(
    producer: ProducerRef,
    path: List(semantic_types.PathStep),
  )
}

Constructors

ValueRef(
  producer: ProducerRef,
  path: List(semantic_types.PathStep),
)

VerifiedCompositionCandidate

opaque </>

pub opaque type VerifiedCompositionCandidate

WitnessFailure

</>

pub type WitnessFailure {
  InputRevisionMismatch
  InitialMembership(input: InputId)
  ProducerMismatch(value: ValueRef)
  ProjectionMismatch(
    failure: semantic_validation.ProjectionFailure,
  )
  SourceConstraintMismatch(value: ValueRef)
  InclusionMismatch(failure: InclusionFailure)
  SuppliedValueMismatch(value: ValueRef)
  ConstructionMismatch(reference: semantic_types.TypeRef)
  MissingBinding(identity: String)
  SignatureMismatch(site: SiteId)
  GuardNotDominating(value: ValueRef)
  IncompleteBranchCoverage(identity: String)
  FailureEmbeddingMismatch(embedding: FailureEmbeddingId)
  GoalMismatch
  RankViolation
  ResourceLoweringMismatch(reason: String)
  ResourceReplayMismatch(reason: String)
  ForgedClosure(reason: String)
  ForgedAcyclicity(reason: String)
  MissingEvidence(reason: String)
}

Constructors

```
InputRevisionMismatch
```
```
InitialMembership(input: InputId)
```
```
ProducerMismatch(value: ValueRef)
```

ProjectionMismatch(
  failure: semantic_validation.ProjectionFailure,
)

SourceConstraintMismatch(value: ValueRef)

InclusionMismatch(failure: InclusionFailure)

```
SuppliedValueMismatch(value: ValueRef)
```

ConstructionMismatch(reference: semantic_types.TypeRef)

```
MissingBinding(identity: String)
```
```
SignatureMismatch(site: SiteId)
```
```
GuardNotDominating(value: ValueRef)
```

IncompleteBranchCoverage(identity: String)

FailureEmbeddingMismatch(embedding: FailureEmbeddingId)

```
GoalMismatch
```
```
RankViolation
```

ResourceLoweringMismatch(reason: String)

```
ResourceReplayMismatch(reason: String)
```
```
ForgedClosure(reason: String)
```
```
ForgedAcyclicity(reason: String)
```
```
MissingEvidence(reason: String)
```

Values

acyclic_input

</>

pub fn acyclic_input(
  checked: CheckedAcyclic,
) -> typed_mapping.SolverInput

acyclic_witness

</>

pub fn acyclic_witness(
  checked: CheckedAcyclic,
) -> typed_mapping.AcyclicWitness

add_discriminator

</>

pub fn add_discriminator(
  tag_model: option.Option(semantic_types.TagModel),
  value: exact_json.JsonValue,
  tag: String,
) -> option.Option(exact_json.JsonValue)

at

</>

pub fn at(values: List(a), index: Int) -> option.Option(a)

bounded_slot_samples

</>

pub fn bounded_slot_samples(
  graph: semantic_types.SemanticGraph,
  contract: semantic_types.SlotContract,
  limit: Int,
  max_sample_length: Int,
) -> SampleResult(semantic_types.SlotValue(exact_json.JsonValue))

candidate_components

</>

pub fn candidate_components(
  prepared: PreparedCompositionInput,
  candidate: CandidateTree,
) -> Result(
  #(CompositionPlan, CompositionWitness),
  CompositionEngineFailure,
)

candidate_key

</>

pub fn candidate_key(
  input: CompositionInput,
  candidate: CandidateTree,
) -> String

candidate_plan

</>

pub fn candidate_plan(
  candidate: VerifiedCompositionCandidate,
) -> CompositionPlan

candidate_prepared

</>

pub fn candidate_prepared(
  candidate: VerifiedCompositionCandidate,
) -> PreparedCompositionInput

candidate_witness

</>

pub fn candidate_witness(
  candidate: VerifiedCompositionCandidate,
) -> CompositionWitness

check_assignable

</>

pub fn check_assignable(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  max_obligations: Int,
) -> CompatibilityDecision

check_assignable_bounded

</>

pub fn check_assignable_bounded(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  bounds: SearchBounds,
) -> CompatibilityDecision

check_function

</>

pub fn check_function(
  graph: semantic_types.SemanticGraph,
  input: CompositionInput,
  function: FunctionSignature,
) -> Result(Nil, CompositionInputFailure)

check_return

</>

pub fn check_return(
  prepared: PreparedCompositionInput,
  state: SearchState,
  terminal: ReturnPlan,
) -> Result(Bool, WitnessFailure)

checked_inclusion_certificate

</>

pub fn checked_inclusion_certificate(
  checked: CheckedInclusion,
) -> InclusionCertificate

checked_inclusion_graph

</>

pub fn checked_inclusion_graph(
  checked: CheckedInclusion,
) -> semantic_types.SemanticGraph

checked_plan

</>

pub fn checked_plan(
  checked: CheckedComposition,
) -> CompositionPlan

checked_prepared

</>

pub fn checked_prepared(
  checked: CheckedComposition,
) -> PreparedCompositionInput

checked_raw

</>

pub fn checked_raw(checked: CheckedComposition) -> RawComposition

checked_witness

</>

pub fn checked_witness(
  checked: CheckedComposition,
) -> CompositionWitness

choice_states

</>

pub fn choice_states(
  prepared: PreparedCompositionInput,
  state: SearchState,
  choice: ChoiceSkeleton,
) -> Result(List(SearchState), WitnessFailure)

closure_canonical_plans

</>

pub fn closure_canonical_plans(
  checked: CheckedCompositionClosure,
) -> List(String)

closure_witness

</>

pub fn closure_witness(
  checked: CheckedCompositionClosure,
) -> CompositionClosureWitness

collect

</>

pub fn collect(
  values: List(a),
  action: fn(a) -> Result(b, e),
) -> Result(List(b), e)

decide_ambiguous

</>

pub fn decide_ambiguous(
  prepared: PreparedCompositionInput,
  first: CandidateTree,
  second: CandidateTree,
) -> Result(CompositionDecision, CompositionEngineFailure)

decide_unreachable

</>

pub fn decide_unreachable(
  prepared: PreparedCompositionInput,
  closure: CompositionClosureWitness,
) -> Result(CompositionDecision, CompositionEngineFailure)

default_resource_token_bound

</>

pub const default_resource_token_bound: Int

default_search_bounds

</>

pub fn default_search_bounds() -> SearchBounds

distinct_candidates

</>

pub fn distinct_candidates(
  input: CompositionInput,
  candidates: List(CandidateTree),
) -> List(CandidateTree)

effective_projection

</>

pub fn effective_projection(
  prepared: PreparedCompositionInput,
  state: SearchState,
  value: ValueRef,
) -> Result(
  semantic_validation.ProjectionCertificate,
  WitnessFailure,
)

enumerate_state

</>

pub fn enumerate_state(
  prepared: PreparedCompositionInput,
  state: SearchState,
  budget: CandidateBudget,
) -> Enumeration

evaluate_guard_arm

</>

pub fn evaluate_guard_arm(
  graph: semantic_types.SemanticGraph,
  guard: DeclaredGuard,
  inspected: semantic_types.SlotValue(exact_json.JsonValue),
) -> Result(GuardArm, semantic_types.ValueDecision)

fresh_budget

</>

pub fn fresh_budget() -> CandidateBudget

goal_unreachable

</>

pub fn goal_unreachable(
  checked: CheckedCompositionClosure,
) -> Bool

guard_declaration

</>

pub fn guard_declaration(
  input: CompositionInput,
  id: GuardId,
) -> option.Option(DeclaredGuard)

inclusion_samples

</>

pub fn inclusion_samples(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.TypeRef,
  destination: semantic_types.TypeRef,
  limit: Int,
) -> List(exact_json.JsonValue)

inclusion_samples_bounded

</>

pub fn inclusion_samples_bounded(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.TypeRef,
  destination: semantic_types.TypeRef,
  bounds: SearchBounds,
) -> SampleResult(exact_json.JsonValue)

inclusion_slot_samples

</>

pub fn inclusion_slot_samples(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.TypeRef,
  limit: Int,
) -> List(semantic_types.SlotValue(exact_json.JsonValue))

index_of

</>

pub fn index_of(
  values: List(a),
  value: a,
  index: Int,
) -> option.Option(Int)

initial_state

</>

pub fn initial_state(
  prepared: PreparedCompositionInput,
) -> SearchState

lower_resource_trace

</>

pub fn lower_resource_trace(
  prepared: PreparedCompositionInput,
  trace: BranchTrace,
) -> Result(
  #(typed_mapping.SolverInput, ResourceCorrespondence),
  LoweringFailure,
)

merge_choice

</>

pub fn merge_choice(
  input: CompositionInput,
  state: SearchState,
  choice: ChoiceSkeleton,
  children: List(List(CandidateTree)),
  budget: CandidateBudget,
) -> #(List(CandidateTree), CandidateBudget)

prepare_composition

</>

pub fn prepare_composition(
  graph: semantic_types.SemanticGraph,
  input: CompositionInput,
  check_signature: fn(FunctionSignature) -> Result(
    Nil,
    CompositionInputFailure,
  ),
) -> Result(PreparedCompositionInput, CompositionInputFailure)

prepared_empty

</>

pub fn prepared_empty(
  prepared: PreparedCompositionInput,
) -> List(semantic_types.TypeRef)

prepared_graph

</>

pub fn prepared_graph(
  prepared: PreparedCompositionInput,
) -> semantic_types.SemanticGraph

prepared_initial_obligations

</>

pub fn prepared_initial_obligations(
  prepared: PreparedCompositionInput,
) -> List(semantic_types.SemanticObligation)

prepared_input

</>

pub fn prepared_input(
  prepared: PreparedCompositionInput,
) -> CompositionInput

project_owned

</>

pub fn project_owned(
  tag_model: option.Option(semantic_types.TagModel),
  value: semantic_types.SlotValue(exact_json.JsonValue),
  path: List(semantic_types.PathStep),
) -> semantic_types.SlotValue(exact_json.JsonValue)

reachability_input

</>

pub fn reachability_input(
  checked: CheckedReachability,
) -> typed_mapping.SolverInput

reachability_witness

</>

pub fn reachability_witness(
  checked: CheckedReachability,
) -> typed_mapping.ReachabilityWitness

replace_at

</>

pub fn replace_at(
  values: List(a),
  index: Int,
  value: a,
) -> List(a)

require

</>

pub fn require(condition: Bool, failure: e) -> Result(Nil, e)

resolved_shape

</>

pub fn resolved_shape(
  graph: semantic_types.SemanticGraph,
  reference: semantic_types.TypeRef,
) -> option.Option(semantic_types.TypeShape)

resource_closure_input

</>

pub fn resource_closure_input(
  checked: CheckedClosure,
) -> typed_mapping.SolverInput

resource_closure_witness

</>

pub fn resource_closure_witness(
  checked: CheckedClosure,
) -> typed_mapping.ClosureWitness

resource_trace_meaning

</>

pub fn resource_trace_meaning(
  prepared: PreparedCompositionInput,
  correspondence: ResourceCorrespondence,
) -> Result(Nil, UnresolvedObligation)

sample_value_fuel

</>

pub fn sample_value_fuel(
  graph: semantic_types.SemanticGraph,
  reference: semantic_types.TypeRef,
  active: List(semantic_types.TypeRef),
  fuel: Int,
  max_sample_length: Int,
) -> SampleResult(exact_json.JsonValue)

samples

</>

pub fn samples(
  graph: semantic_types.SemanticGraph,
  reference: semantic_types.TypeRef,
  active: List(semantic_types.TypeRef),
  limit: Int,
) -> List(exact_json.JsonValue)

semantic_basis

</>

pub fn semantic_basis(
  graph: semantic_types.SemanticGraph,
) -> SemanticBasis

slot_empty

</>

pub fn slot_empty(
  contract: semantic_types.SlotContract,
  empty: List(semantic_types.TypeRef),
) -> Bool

slot_samples

</>

pub fn slot_samples(
  graph: semantic_types.SemanticGraph,
  contract: semantic_types.SlotContract,
  limit: Int,
) -> List(semantic_types.SlotValue(exact_json.JsonValue))

unique

</>

pub fn unique(values: List(a)) -> List(a)

verify_acyclic_witness

</>

pub fn verify_acyclic_witness(
  input: typed_mapping.SolverInput,
  witness: typed_mapping.AcyclicWitness,
) -> Result(CheckedAcyclic, WitnessFailure)

verify_closure_witness

</>

pub fn verify_closure_witness(
  input: typed_mapping.SolverInput,
  witness: typed_mapping.ClosureWitness,
) -> Result(CheckedClosure, WitnessFailure)

verify_composition

</>

pub fn verify_composition(
  prepared: PreparedCompositionInput,
  raw: RawComposition,
) -> Result(CheckedComposition, WitnessFailure)

verify_composition_closure

</>

pub fn verify_composition_closure(
  prepared: PreparedCompositionInput,
  witness: CompositionClosureWitness,
) -> Result(CheckedCompositionClosure, WitnessFailure)

verify_counterexample

</>

pub fn verify_counterexample(
  graph: semantic_types.SemanticGraph,
  certificate: CounterexampleCertificate,
) -> Result(Nil, InclusionFailure)

verify_inclusion

</>

pub fn verify_inclusion(
  graph: semantic_types.SemanticGraph,
  source: semantic_types.SlotContract,
  destination: semantic_types.SlotContract,
  certificate: InclusionCertificate,
) -> Result(CheckedInclusion, InclusionFailure)

verify_reachability_witness

</>

pub fn verify_reachability_witness(
  input: typed_mapping.SolverInput,
  witness: typed_mapping.ReachabilityWitness,
) -> Result(CheckedReachability, WitnessFailure)

verify_return_values

</>

pub fn verify_return_values(
  prepared: PreparedCompositionInput,
  terminal: ReturnPlan,
  values: List(
    #(ProducerRef, semantic_types.SlotValue(exact_json.JsonValue)),
  ),
) -> Result(Nil, WitnessFailure)

verify_unreachable_composition

</>

pub fn verify_unreachable_composition(
  prepared: PreparedCompositionInput,
  witness: CompositionClosureWitness,
) -> Result(Nil, WitnessFailure)

verify_value_models

</>

pub fn verify_value_models(
  prepared: PreparedCompositionInput,
  state: SearchState,
  values: List(
    #(ProducerRef, semantic_types.SlotValue(exact_json.JsonValue)),
  ),
) -> Result(Nil, WitnessFailure)