Syntax.TcInput

Typed vocabulary for the prism-tc-input-v1 checker-input artifact.

The document is the declaration interface consumed by the Rust checker. Its function bodies are NodeIds into prism-resolved-syntax-v1; no inferred Rust facts appear here.

Types

TcImport

type TcImport = TcImport {
  path: String,
  names: List(String),
  glob: Bool
} deriving (Eq, Show)

One import the module takes: the module path, the names taken from it, and whether the list was written as a glob.

TcCtor

type TcCtor = TcCtor {
  name: String,
  tag: Int,
  fields: List(String),
  args: List(String)
} deriving (Eq, Show)

One constructor of a data declaration: its name, its discriminant tag, its record field names, and its argument type spellings.

TcData

type TcData = TcData {
  name: String,
  params: List(String),
  is_newtype: Bool,
  derivs: List(String),
  ctors: List(TcCtor),
  span: Span
} deriving (Eq, Show)

A data declaration: its name, type parameters, newtype flag, derived class names, constructors, and the span of the declaration head.

TcOp

type TcOp = TcOp {
  name: String,
  grade: String,
  params: List(String),
  ret: String
} deriving (Eq, Show)

One operation of an effect declaration: its name, its resumption grade, its parameter type spellings, and its return type.

TcEffect

type TcEffect = TcEffect {
  name: String,
  params: List(String),
  ops: List(TcOp),
  span: Span
} deriving (Eq, Show)

An effect declaration: its name, type parameters, operations, and the span of the declaration head.

TcMethod

type TcMethod = TcMethod { name: String, ty: String } deriving (Eq, Show)

One method signature of a class: its name and its type spelling.

TcClass

type TcClass = TcClass {
  name: String,
  param: String,
  supers: List(String),
  methods: List(TcMethod),
  span: Span
} deriving (Eq, Show)

A class declaration: its name, its single type parameter, its superclass names, its method signatures, and the span of the declaration head.

TcConstraint

type TcConstraint = TcConstraint { cls: String, ty: String } deriving (Eq, Show)

One class constraint: the class named and the type it constrains.

TcInstance

type TcInstance = TcInstance {
  cls: String,
  head: String,
  module_name: String,
  context: List(TcConstraint)
} deriving (Eq, Show)

An instance declaration: the class, the head type it instantiates, the module that defines it, and its instance context.

TcParam

type TcParam = TcParam { name: String, is_borrow: Bool } deriving (Eq, Show)

One function parameter: its binder name and whether it is taken by borrow.

TcFunction

type TcFunction = TcFunction {
  name: String,
  params: List(TcParam),
  constraints: List(String),
  body: Int,
  span: Span
} deriving (Eq, Show)

A function declaration: its name, parameters, constraint spellings, the NodeId of its body in the resolved-syntax artifact, and the span of its head.

TcInputDoc

type TcInputDoc = TcInputDoc {
  schema: String,
  compiler: String,
  imports: List(TcImport),
  types: List(TcData),
  effects: List(TcEffect),
  classes: List(TcClass),
  instances: List(TcInstance),
  functions: List(TcFunction)
} deriving (Eq, Show)

A whole checker-input document: the schema tag, the compiler version that emitted it, and the module’s imports and declarations in source order.

Functions and Values

tc_input_schema

tc_input_schema : () -> String

The schema tag every checker-input document carries.