sessions

cfamily.Session

record Session (L : Constructs)

A debugging session: the names of the program’s variables, how its types are written, its functions (none when it did not check), the nodes it stops at (the ones the program wrote, as a set: asked at every step, so a lookup that takes time logarithmic in the program’s size) and the configuration.

cfamily.DebugStop

def DebugStop (L : Constructs) : Type

Where the debugger stopped.

cfamily.Session.rejected

def Session.rejected {L : Constructs} (names : Names) (types : TypeText L) (n : NodeId) (why : Refusal) : Session L

A session that cannot run: stopped at the node n, where the program did not check, refused for why (with the names and types the host shows).

cfamily.Session.unsupported

def Session.unsupported {L : Constructs} (names : Names) (types : TypeText L) (n : NodeId) (construct : String) : Session L

A session that cannot run: stopped at a construct not supported yet.

cfamily.Session.of

def Session.of {L : Constructs} (d : Dialect L) (types : TypeText L) (mismatch : Option String) (p : Program) : Session L

A session for a program of a dialect, how it writes types, and why the program is not the dialect’s (none when it is): checked once, at its start with no input yet.

cfamily.Session.ofWritten

def Session.ofWritten {L : Constructs} (d : Dialect L) (types : TypeText L) (mismatch : Option String) (p : Program) (written : Program) : Session L

As Session.of, where the program did not check placed in what it wrote and stopping only at its nodes (written: a dialect may run more, such as a board’s items and the sketch rewritten for them).

cfamily.Session.load

def Session.load {L : Constructs} (d : Dialect L) (typesOf : Program -> TypeText L) (mismatch : Program -> Option String) (empty : Program) (source : String) : Session L

A session for a program given as JSON, with how the dialect writes a program’s types and why a program is not its: JSON it cannot read is a program that did not check (its types written as the empty program’s).

cfamily.Session.stopSet

def Session.stopSet (ns : List NodeId) : Map NodeId Unit

The nodes ns as a set to stop at.

cfamily.Session.with

def Session.with {L : Constructs} (x : Session L) (c : Configuration L) : Session L

The configuration replaced.

cfamily.Session.breakpoints

def Session.breakpoints (text : String) : List String

The breakpoints: one node per line.

cfamily.Session.runCounted

def Session.runCounted {L : Constructs} (d : Dialect L) (kind : Nat) (breakpoints : String) (closed : Bool) (fuel : Nat) (x : Session L) : DebugStop L * Visits

Runs to the next stop (kind 0 continue, 1 step in, 2 step over, 3 step out; closed when no more input comes), with how many times the run entered each node the program wrote.

cfamily.Session.run

def Session.run {L : Constructs} (d : Dialect L) (kind : Nat) (breakpoints : String) (closed : Bool) (fuel : Nat) (x : Session L) : DebugStop L

Runs to the next stop: kind 0 continue, 1 step in, 2 step over, 3 step out; closed when no more input comes.

cfamily.Session.resumed

def Session.resumed {L : Constructs} (x : Session L) (s : DebugStop L) : Session L

The session resumed from a stop (unchanged when the run cannot go on).

cfamily.Session.finish

def Session.finish {L : Constructs} (d : Dialect L) (fuel : Nat) (left : Nat) (x : Session L) : DebugStop L

Runs on to a stop that is not a divergence (going on past at most left of them, as the implementation does), no more input coming.

cfamily.Session.report

def Session.report {L : Constructs} (d : Dialect L) (input : String) (fuel : Nat) (x : Session L) : String

A run to its end with all the input given at once, as JSON: the stop’s kind (Stop.kindName), node, output and details. cella diff-translation runs a case’s runDef with it.

cfamily.DebugStop.state

def DebugStop.state {L : Constructs} (s : DebugStop L) : Option (State L)

The state at a stop.

cfamily.DebugStop.kind

def DebugStop.kind {L : Constructs} (s : DebugStop L) : Nat

Which kind of stop it is, as the debugging host reads it (Stop.kind).

cfamily.DebugStop.node

def DebugStop.node {L : Constructs} (s : DebugStop L) : String

The node a stop is at: where the program did not check, else the stop’s.

cfamily.DebugStop.output

def DebugStop.output {L : Constructs} (s : DebugStop L) : String

The output so far at a stop.

cfamily.DebugStop.errorOutput

def DebugStop.errorOutput {L : Constructs} (s : DebugStop L) : String

The error output so far at a stop.

cfamily.DebugStop.detail

def DebugStop.detail {L : Constructs} (d : Dialect L) (s : DebugStop L) : String

A stop’s details as JSON: the reason for undefined or unspecified behavior, or where and why the program did not check.

cfamily.DebugStop.noted

def DebugStop.noted {L : Constructs} (s : DebugStop L) : Option (State L)

The state that holds the notes at a stop: after the move that noted a divergence (the stop itself reports the state before that move), else the stop’s.

cfamily.DebugStop.divergences

def DebugStop.divergences {L : Constructs} (d : Dialect L) (s : DebugStop L) : String

The divergences from the standard recorded so far, as JSON.

cfamily.Session.feed

def Session.feed {L : Constructs} (text : String) (x : Session L) : Session L

More input.

cfamily.Session.globals

def Session.globals {L : Constructs} (d : Dialect L) (x : Session L) : String

The global variables as JSON.

cfamily.Session.frames

def Session.frames {L : Constructs} (d : Dialect L) (at : String) (x : Session L) : String

The calls, stopped at a node, as JSON.

cfamily.Session.setError

def Session.setError {L : Constructs} (n : Nat) (x : DeclId) (text : String) (s : Session L) : String

Why an integer variable of the n-th call cannot be set from text (empty when it can).

cfamily.Session.set

def Session.set {L : Constructs} (n : Nat) (x : DeclId) (text : String) (s : Session L) : Session L

The session with an integer variable of the n-th call set from text (unchanged when it cannot be).