querying

cfamily.QueryDialect

record QueryDialect (L : Constructs)

What the type query needs of a dialect: its checking, how it writes types, the common types tried for a slot’s display, and its own type spellings (given the whole reader, for the types inside).

cfamily.TypeSyntax.named

def TypeSyntax.named : List (String * TypeSyntax)

C’s type names.

cfamily.TypeSyntax.ofName

def TypeSyntax.ofName (s : String) : TypeSyntax

The type a C name stands for: a standard type, else a typedef’s name.

cfamily.QueryDialect.typeWithin

def QueryDialect.typeWithin {L : Constructs} (qd : QueryDialect L) (fuel : Nat) (text : String) : Option TypeSyntax

A type read from its spelling within fuel: the dialect’s spellings first, then C’s (a pointer, const, a struct or union tag, a name).

cfamily.QueryDialect.typeOf

def QueryDialect.typeOf {L : Constructs} (qd : QueryDialect L) (text : String) : Option TypeSyntax

A type read from its spelling, as Ty.text writes it.

cfamily.TypedExpr.elsewhere

def TypedExpr.elsewhere {L : Constructs} (n : NodeId) (es : List (TypedExpr L)) : List (TypedExpr L)

The expressions among es at nodes other than n.

cfamily.TypedExpr.option

def TypedExpr.option {L : Constructs} (m : Option (TypedExpr L)) : List (TypedExpr L)

An optional expression as a list.

cfamily.TypedStmt.expressions

def TypedStmt.expressions {L : Constructs} (s : TypedStmt L) : List (TypedExpr L)

The expressions a statement itself has (not those of the statements inside it).

cfamily.CheckedProgram.statements

def CheckedProgram.statements {L : Constructs} (c : CheckedProgram L) : List (TypedStmt L)

A checked program’s statements: the globals’ and the functions’ bodies, with the statements inside.

cfamily.CheckedProgram.expressions

def CheckedProgram.expressions {L : Constructs} (c : CheckedProgram L) : List (TypedExpr L)

A checked program’s expressions, each the ones inside first.

cfamily.CheckedProgram.errors

def CheckedProgram.errors {L : Constructs} (c : CheckedProgram L) : List (NodeId * Refusal)

The statements that did not check, with their reasons.

cfamily.Query.isSlot

def Query.isSlot (n : NodeId) : Bool

Whether a node is a hole’s (<node>#<slot>): its types are the slot’s, reported there.

cfamily.Query.firstTypes

def Query.firstTypes {L : Constructs} (seen : List (NodeId * Ty L)) (xs : List (NodeId * Ty L)) : List (NodeId * Ty L)

The first type given for each node, holes left out.

cfamily.CheckedProgram.declarations

def CheckedProgram.declarations {L : Constructs} (c : CheckedProgram L) : List (DeclId * Ty L)

The declarations’ types: the functions’ parameters and the declared variables.

cfamily.CheckedProgram.nodeTypes

def CheckedProgram.nodeTypes {L : Constructs} (p : Platform) (c : CheckedProgram L) : List (NodeId * Ty L)

Each node’s type: the declarations’, then the expressions’ before any implicit conversion.

cfamily.QueryRun

data QueryRun (L : Constructs)

A check for the query: checked (with the statements that did not check inside), or stopped at an error outside any statement.

cfamily.QueryDialect.run

def QueryDialect.run {L : Constructs} (qd : QueryDialect L) (p : Program) (holes : List (NodeId * TypeSyntax)) : QueryRun L

Checks the program with the holes standing for the types given.

cfamily.QueryRun.errors

def QueryRun.errors {L : Constructs} (r : QueryRun L) : List (NodeId * Refusal)

A run’s errors.

cfamily.Query.newHoles

def Query.newHoles (holes : List (NodeId * TypeSyntax)) (es : List (NodeId * Refusal)) : List NodeId

The holes the errors report that are not given a type yet.

cfamily.QueryDialect.holes

def QueryDialect.holes {L : Constructs} (qd : QueryDialect L) (fuel : Nat) (p : Program) (holes : List (NodeId * TypeSyntax)) : List (NodeId * TypeSyntax)

The holes: a hole without a type is reported at its node; it is given int and checking starts again, until no new hole appears (the next hole in the same statement is seen only then).

cfamily.Query.setHole

def Query.setHole (holes : List (NodeId * TypeSyntax)) (n : NodeId) (t : TypeSyntax) : List (NodeId * TypeSyntax)

The holes with one given another type.

cfamily.FitLevel

data FitLevel

How a candidate fits a hole: exactly, converted without loss, narrowed with loss, or not at all (with the reason).

cfamily.FitLevel.rank

def FitLevel.rank (l : FitLevel) : Nat

The levels in order, the best first.

cfamily.FitLevel.worse

def FitLevel.worse (a : FitLevel) (b : FitLevel) : FitLevel

The worse of two levels.

cfamily.FitLevel.name

def FitLevel.name (l : FitLevel) : String

A level’s name.

cfamily.FitLevel.ofIntegers

def FitLevel.ofIntegers (s : IntegerType) (t : IntegerType) : FitLevel

The level of an integer value converted to an integer type.

cfamily.FitLevel.toFloat

def FitLevel.toFloat {L : Constructs} (f : FloatFormat) (from : Ty L) : FitLevel

The level of a value converted to a floating format.

cfamily.FitLevel.ofExpression

def FitLevel.ofExpression {L : Constructs} (p : Platform) (e : TypedExpr L) : FitLevel

The level one expression with the hole’s node gives: the hole itself is exact; a conversion around it (the checker gives a conversion its operand’s node) is as lossy as it is; its address and what that address designates are exact (how C++ binds a reference to it and reads it through the reference: the identity conversion, [over.ics.ref]p1; the object itself has the node too and gives its own level).

cfamily.CheckedProgram.holeLevel

def CheckedProgram.holeLevel {L : Constructs} (p : Platform) (c : CheckedProgram L) (n : NodeId) : FitLevel

The level a hole is checked at: the worst of the expressions with its node.

cfamily.Query.newErrors

def Query.newErrors (base : List (NodeId * Refusal)) (es : List (NodeId * Refusal)) : List (NodeId * Refusal)

The errors not already in the base (the base gives each hole its displayed type).

cfamily.QueryContext

record QueryContext (L : Constructs)

What the query on one program has: the dialect, the program, the holes with their types, the base’s errors.

cfamily.QueryContext.with

def QueryContext.with {L : Constructs} (qc : QueryContext L) (n : NodeId) (t : TypeSyntax) : Either String (CheckedProgram L)

The program checked with one hole given another type, if no new error appears.

cfamily.QueryDialect.platform

def QueryDialect.platform {L : Constructs} (qd : QueryDialect L) : Platform

The platform the dialect checks for.

cfamily.QueryContext.fit

def QueryContext.fit {L : Constructs} (qc : QueryContext L) (n : NodeId) (t : TypeSyntax) : FitLevel

How a candidate type fits a hole.

cfamily.QueryContext.fitText

def QueryContext.fitText {L : Constructs} (qc : QueryContext L) (n : NodeId) (s : String) : FitLevel

How a candidate written as text fits a hole.

cfamily.QueryContext.probesThatFit

def QueryContext.probesThatFit {L : Constructs} (qc : QueryContext L) (n : NodeId) : List (String * FitLevel)

The dialect’s common types that fit a hole without loss.

cfamily.Query.candidate

def Query.candidate (f : String * FitLevel) : String

A candidate’s name.

cfamily.Query.commas

def Query.commas (xs : List String) : String

Texts separated by commas.

cfamily.Query.display

def Query.display (fits : List (String * FitLevel)) : String

A slot’s display: the one exact type it expects, else the types it accepts.

cfamily.CheckedProgram.holeResult

def CheckedProgram.holeResult {L : Constructs} (p : Platform) (c : CheckedProgram L) (n : NodeId) : Option (Ty L)

The type a hole’s value ends up converted to: the outermost expression with its node.

cfamily.QueryContext.expected

def QueryContext.expected {L : Constructs} (qc : QueryContext L) (n : NodeId) : Option (Ty L)

The slot’s target type: the type a hole is converted to when every common type that fits is converted to the same one; none when the slot takes anything or depends on the candidate.

cfamily.Query.chosen

def Query.chosen {L : Constructs} (qd : QueryDialect L) (fits : List (String * FitLevel)) : TypeSyntax

A hole’s chosen type: its first common type that fits without loss, else int (the other nodes’ types are computed with it).

cfamily.QuerySlot

record QuerySlot (L : Constructs)

A slot: its label, display, expected type, and how each candidate fits.

cfamily.QueryResult

record QueryResult (L : Constructs)

The answer of the type query.

cfamily.QueryContext.slot

def QueryContext.slot {L : Constructs} (qc : QueryContext L) (candidates : List String) (n : NodeId) : QuerySlot L

A slot’s answer.

cfamily.QueryDialect.answer

def QueryDialect.answer {L : Constructs} (qd : QueryDialect L) (p : Program) (candidates : List String) (holes : List (NodeId * TypeSyntax)) : QueryResult L

The answer with the holes given their chosen types.

cfamily.Program.query

def Program.query {L : Constructs} (qd : QueryDialect L) (p : Program) (candidates : List String) : QueryResult L

The type query on a program and candidate types written as C or as the dialect writes them.

cfamily.QueryResult.slot

def QueryResult.slot {L : Constructs} (q : QueryResult L) (label : NodeId) : Option (QuerySlot L)

A slot by its label.

cfamily.QueryResult.fitOf

def QueryResult.fitOf {L : Constructs} (q : QueryResult L) (label : NodeId) (candidate : String) : String

How a candidate fits a slot, by name.

cfamily.QueryResult.expects

def QueryResult.expects {L : Constructs} (tt : TypeText L) (q : QueryResult L) (label : NodeId) : String

A slot’s expected type as written, or (none).

cfamily.QueryResult.display

def QueryResult.display {L : Constructs} (q : QueryResult L) (label : NodeId) : String

A slot’s display.

cfamily.QueryResult.typeOf

def QueryResult.typeOf {L : Constructs} (tt : TypeText L) (q : QueryResult L) (n : NodeId) : String

A node’s type as written.

cfamily.FitLevel.json

def FitLevel.json (l : FitLevel) : Json

A fit as JSON: its level, and the reason when it does not fit.

cfamily.QuerySlot.json

def QuerySlot.json {L : Constructs} (tt : TypeText L) (s : QuerySlot L) : Json

A slot as JSON.

cfamily.Query.errorJson

def Query.errorJson (e : NodeId * Refusal) : Json

The error e as JSON: its node, its reason, its kind and details as a verdict’s problem has them (reject and none when it is not structured), and the type expected and the type given when it is a value that does not convert (null otherwise).

cfamily.Refusal.kind

def Refusal.kind (r : Refusal) : String

The kind of the refusal r as a problem has it: reject when it is not structured.

cfamily.Refusal.params

def Refusal.params (r : Refusal) : List (String * ParamValue)

The details of the refusal r: none when it is not structured.

cfamily.QueryResult.json

def QueryResult.json {L : Constructs} (tt : TypeText L) (q : QueryResult L) : String

The answer as JSON: nodes, slots and errors.