primitives

cpp.Primitives.boundsName

def Primitives.boundsName : String

The primitive a precondition that does not hold is (an access past the object).

cpp.Primitives.internal

def Primitives.internal (f : String) : Option String

The internal function a primitive called as a statement is (cpp.construction), if it is one.

cpp.Primitives.reading

def Primitives.reading (f : String) : Option Bool

Whether a primitive reads standard input into a string’s layout, and how much: a line (true) or a word.

cpp.Primitives.read

def Primitives.read (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (line : Bool) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

__cella_read_word(data, size, capacity) and __cella_read_line(...): a word (whitespace skipped first) or a line (up to the newline, which is read and not kept) read into a string’s layout, its three parts lvalues.

cpp.Primitives.lvalues

def Primitives.lvalues (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (es : List Expr) : CheckResult Cpp.constructs (List (Lifted Cpp.constructs))

Expressions checked as lvalues, in order.

cpp.Primitives.choosing

def Primitives.choosing (f : String) : Option Nat

A primitive marking an implementation’s choice: noting it (0), releasing a block because of it (1), keeping a block under a new number because of it (2).

cpp.Primitives.choiceName

def Primitives.choiceName (e : Expr) : Option String

The name of a choice: a string literal.

cpp.Primitives.choose

def Primitives.choose (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (kind : Nat) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

__cella_implementation_choice("name"): the run notes that it assumes the choice. __cella_choice_release(p, "name"): the block released (as __cella_release), only because of the choice. __cella_choice_keep(p, "name"): the block p (an lvalue) points to is kept under a new number and p set to it, so a pointer taken before still reaches it assuming the choice.

cpp.Primitives.advance

def Primitives.advance (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

__cella_advance(us): the simulated time advanced by us microseconds.

cpp.Primitives.environmental

def Primitives.environmental (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (tag : EnvironmentStatement) (count : Nat) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

An environment statement with its operands checked in order (there must be count of them).

cpp.Primitives.showing

def Primitives.showing (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (tag : EnvironmentStatement) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

__cella_show_text’s index and text, or __cella_show_name’s index and pointer: the pointer’s value (an array decays to a pointer to its first character).

cpp.Primitives.show

def Primitives.show (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (what : Nat) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

__cella_show("kind", index, value) (0), __cella_show_text("kind", index, text) (1) and __cella_show_name("kind", index, pointer) (2): the kind is a string literal.

cpp.Primitives.outOfBounds

def Primitives.outOfBounds (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

__cella_out_of_bounds() at the node m (args empty): out of bounds, nothing known of where; __cella_out_of_bounds(index, size): an index past a container’s elements, both reported (an environment statement, checked by checker with the context c and the names env).

cpp.Primitives.require

def Primitives.require (checker : Checker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (m : NodeId) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

__cella_require(ok, "name", detail): the name is a string literal.

cpp.Primitives.notModeled

def Primitives.notModeled (m : NodeId) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

What a library does not model yet (__cella_unsupported("String(double)"), a string literal): the verdict is unknown, with the reason, not a rejection of a valid program. A library function is checked only when used, so only a program that uses it is affected.

cpp.Primitives.cannotTell

def Primitives.cannotTell (m : NodeId) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

Where a run cannot tell what happens next (__cella_undetermined("HD44780 busy"), a string literal): the run stops there and the verdict is unknown, with the reason; only a run reaching it is affected.

cpp.Primitives.halt

def Primitives.halt (m : NodeId) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

Where the host stops watching (__cella_halt()): the run ends there, exit code 0, nothing after it run.

cpp.Primitives.asynchronous

def Primitives.asynchronous (f : String) : Bool

The environment’s primitives that let simulated time pass (__cella_wait, __cella_elapse): the timers’ events and the interrupts they run are the hardware’s, asynchronous to the code that waits, not its effects.

cpp.Primitives.interrupt

def Primitives.interrupt (statements : StatementChecker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (m : NodeId) (args : List Expr) : CheckResult Cpp.constructs (TypedStmt Cpp.constructs)

An interrupt handler run (__cella_interrupt(handler)): a call through the pointer, as written; what the handler does is not an effect of the code it interrupts (the effect summaries see a primitive without a body).

cpp.Primitives.statement

def Primitives.statement (checker : Checker Cpp.constructs) (statements : StatementChecker Cpp.constructs) (c : StatementContext Cpp.constructs) (env : Env Cpp.constructs) (s : Stmt) : Option (CheckResult Cpp.constructs (TypedStmt Cpp.constructs))

A primitive called as a statement: what it does. None for any other statement.

cpp.Primitives.moveIfNoexcept

def Primitives.moveIfNoexcept (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (x : Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

__cella_move_if_noexcept(x): x as an xvalue when moving an object of its class cannot throw or it cannot be copied, else x as it is (libc++’s std::move_if_noexcept, [utility]); an object not of a class as it is.

cpp.Primitives.inputLook

def Primitives.inputLook (g : Globals Cpp.constructs) (n : NodeId) (left : Bool) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

__cella_peek() and __cella_available(): the next byte of standard input without taking it (-1 when there is none) and how many are left, both an int (Serial’s peek() and available(); getchar() takes one).

cpp.Primitives.ahead

def Primitives.ahead (input : List Char) : Int

The next byte of standard input, -1 when there is none.

cpp.Primitives.clock

def Primitives.clock (g : Globals Cpp.constructs) (n : NodeId) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

__cella_clock(): the simulated time in microseconds, an unsigned long long.

cpp.Primitives.input

def Primitives.input (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (real : Bool) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

__cella_input("kind", index, fallback) (a long) and __cella_input_real(...) (a double): the host’s input for kind:index now, else the fallback; the kind is a string literal.

cpp.Primitives.given

def Primitives.given (inputs : List TimedInput) (key : String) (now : Nat) : Option Value

The host’s input for a key at a time: the value of the last one given for it at or before the time.

cpp.Primitives.inputValue

def Primitives.inputValue (evaluator : Evaluator Cpp.constructs) (s : State Cpp.constructs) (kind : String) (real : Bool) (operands : List (TypedExpr Cpp.constructs)) : Evaluated Cpp.constructs Value

Evaluating an input: its index and fallback, then the host’s value for kind:index (a double converts an integer given).

cpp.Primitives.expression

def Primitives.expression (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (e : Expr) : Option (CheckResult Cpp.constructs (Lifted Cpp.constructs))

A primitive called as an expression: __cella_allocate<T>(n), a block of n objects of T not constructed; __cella_move_if_noexcept(x); __cella_clock(). None for any other expression.

cpp.Primitives.within

def Primitives.within (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

__cella_points_within(p, start, n): a bool, its three operands checked in order.

cpp.Primitives.inside

def Primitives.inside (p : Pointer) (start : Pointer) (count : Int) : Bool

Whether a pointer points to one of the n elements from start: the same array, start <= p < start + n.

cpp.Primitives.withinValue

def Primitives.withinValue (evaluator : Evaluator Cpp.constructs) (s : State Cpp.constructs) (operands : List (TypedExpr Cpp.constructs)) : Evaluated Cpp.constructs Value

Evaluating __cella_points_within: its operands, then 1 or 0.

cpp.Primitives.eepromByte

def Primitives.eepromByte (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

__cella_eeprom_read(address): an unsigned char, its operand checked.

cpp.Primitives.levels

def Primitives.levels (checker : Checker Cpp.constructs) (g : Globals Cpp.constructs) (env : Env Cpp.constructs) (n : NodeId) (args : List Expr) : CheckResult Cpp.constructs (Lifted Cpp.constructs)

__cella_pin_levels(first, count): an int, its two operands checked in order.

cpp.Primitives.shownAt

def Primitives.shownAt (e : Environment) (kind : String) (pin : Nat) : Int

A value the host was shown for a key now (mode:2), 0 when none.

cpp.Primitives.driven

def Primitives.driven (e : Environment) (pin : Nat) : Option Int

The level a chip drives a pin to now: the last drive from a time not after now; none when none drives it or the last one lets it go.

cpp.Primitives.pinLevel

def Primitives.pinLevel (e : Environment) (pin : Nat) : Bool

A pin’s level now, as the headers’ __cella_pin_input gives it: an output’s written level (as shown); an input’s driven level, else the host’s input for digital:pin (unconnected: 0, 1 with the pull-up, mode 3).

cpp.Primitives.levelBits

def Primitives.levelBits (e : Environment) (first : Nat) (count : Nat) (j : Nat) : Nat

The levels of count pins from first, the j-th in bit j.

cpp.Primitives.levelsValue

def Primitives.levelsValue (evaluator : Evaluator Cpp.constructs) (s : State Cpp.constructs) (operands : List (TypedExpr Cpp.constructs)) : Evaluated Cpp.constructs Value

Evaluating __cella_pin_levels: its operands, then the pins’ levels now.

cpp.Primitives.eepromAt

def Primitives.eepromAt (environment : Environment) (address : Nat) : Nat

The EEPROM’s byte at an address: the last one written there, else what the host gave it at power-up (eeprom:<address>), else 0xFF (erased).

cpp.Primitives.eepromValue

def Primitives.eepromValue (evaluator : Evaluator Cpp.constructs) (s : State Cpp.constructs) (operands : List (TypedExpr Cpp.constructs)) : Evaluated Cpp.constructs Value

Evaluating __cella_eeprom_read: its address, then the byte there.

cpp.Primitives.traceLimit

def Primitives.traceLimit : Nat

The most pin changes kept for the host (the old model’s traceLimit).

cpp.Primitives.operand

def Primitives.operand (vs : List Value) (j : Nat) : Int

The j-th of an environment statement’s operands’ values, as an integer (0 when there is none).

cpp.Primitives.keyed

def Primitives.keyed {A : Type} (key : String) (v : A) (table : List (String * A)) : List (String * A)

A table with the key’s value replaced, or added at the end when the key is new.

cpp.Primitives.changed

def Primitives.changed (tag : EnvironmentStatement) (vs : List Value) (e : Environment) : Environment

The environment after a statement of it, given its operands’ values.

cpp.Primitives.owner

def Primitives.owner (scopes : List Scope) (k : List (Frame Cpp.constructs)) (b : Nat) : DeclId

The declaration owning a block among the scopes, the current ones and those the calls saved (“” when none does: allocated).

cpp.Primitives.elementIndices

def Primitives.elementIndices (t : Ty Cpp.constructs) (indices : List Nat) : String

The element indices of an array type a path goes through ([1] for the second element; nothing past a member).

cpp.Primitives.ownerOf

def Primitives.ownerOf (s : State Cpp.constructs) (scopes : List Scope) (k : List (Frame Cpp.constructs)) (v : Value) : DeclId

The declaration of the object a value points into, with the elements of an array it points to (arm@3[1]; “” for a pointer into no block).

cpp.Primitives.run

def Primitives.run (ev : Evaluator Cpp.constructs) (n : NodeId) (tag : EnvironmentStatement) (es : List (TypedExpr Cpp.constructs)) (k : List (Frame Cpp.constructs)) (s : State Cpp.constructs) : Configuration Cpp.constructs

Running a statement of the environment: its operands’ values, then the environment changed by them.