board

arduino.LibraryPart

record LibraryPart

A part of a library: its name (one module) and its items, made when a sketch includes it (a library’s items are a large tree: a sketch for a board that includes none of its libraries does not build them).

arduino.HeaderLibrary

record HeaderLibrary

A library a sketch includes by a header’s name: its parts, each after the ones it uses.

arduino.LibraryPart.of

def LibraryPart.of (name : String) (items : Unit -> List Item) : LibraryPart

The part name with its items, made when they are needed.

arduino.HeaderLibrary.single

def HeaderLibrary.single (header : String) (name : String) (items : Unit -> List Item) : HeaderLibrary

The library a sketch includes by header, of one part name with its items (made when they are needed).

arduino.BoardLibraries

record BoardLibraries

The libraries a sketch may include, by the boards’ processor: the AVR ones’, the ESP ones’ (the ESP32’s and the ESP8266’s), the ESP32’s only (WiFi.h: the ESP8266’s is ESP8266WiFi.h) and the ESP8266’s only (its EEPROM.h is a flash sector, the ESP32’s an NVS blob).

arduino.BoardLibraries.none

def BoardLibraries.none : BoardLibraries

No library on any board.

arduino.BoardLibraries.onAvr

def BoardLibraries.onAvr (libraries : List HeaderLibrary) : BoardLibraries

The libraries given on the AVR boards only.

arduino.CoreEntry

record CoreEntry

A core’s entry: the function a run starts at (AVR’s main, ESP32’s app_main, ESP8266’s user_init), its items (the core’s main.cpp), linked from the core’s archive only when the program does not define a function of that name, and what it runs before the sketch’s setup (AVR’s init(); the ESP cores’ startup is not modeled).

arduino.Board

record Board

A board: its name, items, the core’s entry, target and libraries, and the headers of the libraries other boards have and it does not (a sketch that includes one is rejected at the include, as the compiler stops there).

arduino.CoreEntry.avr

def CoreEntry.avr : CoreEntry

AVR’s entry: ArduinoCore-avr’s main.cpp (it calls init() before setup).

arduino.CoreEntry.esp32

def CoreEntry.esp32 : CoreEntry

The ESP32’s entry: arduino-esp32’s app_main (a sketch’s main is just a function).

arduino.CoreEntry.esp8266

def CoreEntry.esp8266 : CoreEntry

The ESP8266’s entry: esp8266/Arduino’s user_init (a sketch’s main is just a function).

arduino.Board.startedFunction

def Board.startedFunction (b : Board) (f : FunctionDefinition) : FunctionDefinition

A function, with the core’s startup run before its body when it is main.

arduino.Board.started

def Board.started (b : Board) (items : List Item) : List Item

Items whose main (a test’s own, run on the board’s items without the core’s entry) first runs what the core’s entry runs before the sketch: the board as a sketch’s setup sees it.

arduino.Board.avr

def Board.avr : Target

AVR’s target: 16-bit int, a 32-bit double and long double (avr-gcc’s as the Arduino core builds it: both are float).

arduino.Board.esp

def Board.esp : Target

The target of the ESP32 and the ESP8266: 32-bit int and long, a 64-bit double and long double (the Xtensa GCC’s).

arduino.Board.itemsFor

def Board.itemsFor (header : List Item) (core : List Item) : List Item

A board’s items: its header, the pins, then its core (with the core’s String, Print and Serial).

arduino.Board.of

def Board.of (name : String) (header : List Item) (core : List Item) (entry : CoreEntry) (target : Target) (libraries : List HeaderLibrary) : Board

A board of a name, its header, core and the core’s entry, its target, and its libraries.

arduino.Board.headers

def Board.headers (seen : List String) (items : List Item) : List String

The headers a sketch includes, each once, in order.

arduino.LibraryPart.firsts

def LibraryPart.firsts (seen : List String) (parts : List LibraryPart) : List LibraryPart

The parts, each the first time its name comes (a part two headers bring is included once, as a header’s include guard does).

arduino.Board.included

def Board.included (b : Board) (items : List Item) : List Item

The items of the libraries a sketch includes that the board has: their parts in order, each once.

arduino.Board.avrCore

def Board.avrCore : List Item

The AVR core with its String, Print and Serial (Arduino.h includes WString.h: every sketch has String).

arduino.Board.esp32Serial

def Board.esp32Serial : List Item

The ESP32 core’s number formatting, String, Print, Serial and IPAddress (arduino-esp32 3.0.7’s; Arduino.h includes IPAddress.h).

arduino.Board.esp32WithTouch

def Board.esp32WithTouch : List Item

The ESP32 core with the first touch sensor’s touchRead (the ESP32).

arduino.Board.s3WithTouch

def Board.s3WithTouch : List Item

The ESP32 core with the second touch sensor’s touchRead (the ESP32-S3).

arduino.Board.c3Core

def Board.c3Core : List Item

The ESP32 core without a touch sensor (the ESP32-C3).

arduino.Board.esp8266Core

def Board.esp8266Core : List Item

The ESP8266 core with its number formatting, String, Print and Serial (esp8266/Arduino 3.1.2’s).

arduino.Board.makingWith

def Board.makingWith (libraries : BoardLibraries) : List (String * (Unit -> Board))

The boards, by the names the earlier model took (arduino is the Uno; the S3 CAM is an S3 to its core), with the libraries given for their processor: each name with how its board is made, so only the board asked for is built (a board’s items are its core’s whole library, and a program is checked against one board).

arduino.Board.headersOf

def Board.headersOf (libraries : BoardLibraries) : List String

The headers of every library the boards are given (libraries), which a board that lacks one reports as elsewhere.

arduino.Board.withElsewhere

def Board.withElsewhere (headers : List String) (b : Board) : Board

A board with the headers of the given libraries it does not have.

arduino.Board.missingHeader

def Board.missingHeader (b : Board) (items : List Item) : Option (NodeId * String)

The first include of a library other boards have and this one does not: its node and header.

arduino.Board.namedWith

def Board.namedWith (libraries : BoardLibraries) (name : String) : Option Board

The board of a name, with the libraries given (arduino gives all of them; a check that includes none gives BoardLibraries.none, and does not load the libraries’ modules).

arduino.Board.number

def Board.number (e : Expr) : Option Int

An integer an expression writes (a literal, or a literal converted).

arduino.Board.constant

def Board.constant (items : List Item) (name : String) : Option Int

The integer a global of the items is initialized with (a board’s constant: A0 is 14 on an Uno).

arduino.Board.pinText

def Board.pinText (b : Board) (written : String) : String

A pin as the host writes it (a number, or a board’s constant) as a number.

arduino.Board.deviceKey

def Board.deviceKey (names : List (DeclId * String)) (kind : String) (arg : String) : Option String

A device’s input as the host writes it (dht:room.temperature, the device by its variable’s name) as the headers read it: dht.temperature:@ and the declaration (the primitive finds the device’s number by the declaration it was shown named for); none when the argument has no field. A name no declaration has is kept as written (no device takes it).

arduino.Board.key

def Board.key (b : Board) (names : List (DeclId * String)) (key : String) : String

An input key as the host writes it (analog:A0, echo:7, dht:room.temperature) as the headers read it: the pin by number, echo as pulse, a device’s by its declaration (Board.deviceKey). A key without its argument (wifi, wifi:) is the first one’s (wifi:0).

arduino.Board.value

def Board.value (b : Board) (j : Json) : Either String Value

An input’s value: an integer, or a number with a fraction or an exponent (a sensor’s temperature) as the board’s double.

arduino.Board.input

def Board.input (b : Board) (names : List (DeclId * String)) (j : Json) : Either String TimedInput

One of the host’s inputs, {t, key, value} (milliseconds; an integer, or a number with a fraction), as the environment takes it; names are the program’s declarations (a device’s input names its variable).

arduino.Board.inputOf

def Board.inputOf (time : Either String Nat) (key : String) (value : Either String Value) : Either String TimedInput

An input at a time in milliseconds, as the environment’s (microseconds).

arduino.Board.objectCall

def Board.objectCall (e : Expr) : Expr

A call the earlier model wrote by an object’s name (Serial.begin): the member function called on the library’s object of that name.

arduino.Macro

record Macro

A function-like macro of a core (constrain(amt, low, high)): its name, its parameters, and the expression it stands for written with them.

arduino.Board.macroPrefix

def Board.macroPrefix : String

The name a core gives the template that shows clang a macro’s expansion (__cella_macro_constrain).

arduino.Board.returned

def Board.returned (body : Stmt) : Option Expr

The expression a function’s body returns, when the body is that one return.

arduino.Board.macroOf

def Board.macroOf (it : Item) : Option Macro

The macro a core’s item stands for: a template __cella_macro_<name> whose body returns the expansion.

arduino.Board.macros

def Board.macros (items : List Item) : List Macro

The macros a board’s items define.

arduino.Macro.substituted

def Macro.substituted (m : Macro) (args : List Expr) : Expr

A macro’s expansion for arguments: each mention of a parameter replaced by its argument, as the preprocessor does (an argument mentioned twice is evaluated twice).

arduino.Macro.takes

def Macro.takes (f : String) (count : Nat) (m : Macro) : Bool

Whether a macro is the one a call of a name with a number of arguments calls.

arduino.Board.expandedCall

def Board.expandedCall (macros : List Macro) (e : Expr) : Expr

A call of a macro (by its name, with as many arguments as it has parameters) expanded in place, its nodes renamed after the call’s (n#0, n#1…): the copies of an argument must not share nodes. Any other expression is kept.

arduino.Board.expanded

def Board.expanded (b : Board) (items : List Item) : List Item

A program’s items as they run on a board: the calls the earlier model wrote by an object’s name as member calls, and the core’s macros expanded (inner calls first: the rewriting is bottom-up).

arduino.Board.inputs

def Board.inputs (b : Board) (names : List (DeclId * String)) (j : Json) : Either String (List TimedInput)

The host’s inputs on a board, a JSON array.

arduino.Board.defines

def Board.defines (name : String) (items : List Item) : Bool

Whether items define a function of a name.

arduino.Board.describe

def Board.describe (r : CppReason) : ReasonDescription

Why a run on a board stops, as the Arduino core says it: a pin the board does not have (__cella_pin_on_board’s precondition) is undefined behavior of the core’s pin functions; anything else as C++ says.

arduino.Board.dialect

def Board.dialect (b : Board) (given : List TimedInput) : Dialect Cpp.constructs

C++ on a board’s target with the host’s inputs, its run starting at the core’s entry, its reasons as the Arduino core says them.

arduino.Board.query

def Board.query (b : Board) : QueryDialect Cpp.constructs

C++’s type query on a board: its target, its checking starting at the core’s entry.

arduino.Board.program

def Board.program (b : Board) (items : List Item) : Program

The program run for a program’s items on a board: the board’s items, the libraries it includes, the program’s (expanded), the core’s entry (its main.cpp, linked from the core’s archive only when the program does not define a function of the entry’s name: an AVR sketch’s own main replaces the core’s, which calls init()).

arduino.Board.shown

def Board.shown (env : Environment) (key : String) : Option Int

What the host was last shown for a key (mode:13).

arduino.Board.pinOf

def Board.pinOf (key : String) : Option Nat

The pin a key shows a pin’s state for (mode:13, level:13, pwm:13, tone:13).

arduino.Board.pins

def Board.pins (shown : List (String * Int)) (seen : List Nat) : List Nat

The pins the host was shown, in the order each was first shown.

arduino.Board.modeJson

def Board.modeJson (code : Option Int) : Json

A pin’s mode by name (as pinMode writes it), null before one was set.

arduino.Board.modeName

def Board.modeName (code : Int) : Json

A mode’s code (1 INPUT, 2 OUTPUT, 3 INPUT_PULLUP) by name; null for no mode.

arduino.Board.present

def Board.present (value : Option Int) (least : Int) : Json

A value the host was shown, null when it is not there or below the least (pwm -1 is no PWM; tone 0 is no sound).

arduino.Board.pinJson

def Board.pinJson (env : Environment) (pin : Nat) : Json

A pin’s state as the wiring panel reads it: {pin, mode, level, pwm, toneHz}.

arduino.Board.text

def Board.text (env : Environment) (key : String) : String

A text the host was shown for a key (“” when there is none).

arduino.Board.devices

def Board.devices (kind : String) (env : Environment) : List (String * DeclId)

The devices of a kind the host was shown names for (lcd:2), in the order each was attached.

arduino.Board.stateKey

def Board.stateKey (kind : String) (state : String) (named : String * DeclId) : String

The key of a device’s state (lcd.rows:2 for the second device’s rows), from its kind and its own key (lcd:2).

arduino.Board.deviceName

def Board.deviceName (names : List (DeclId * String)) (named : String * DeclId) : Json

The source name of a device’s declaration, with the elements of an array it is (arm[1]; “” for one allocated).

arduino.Board.displayJson

def Board.displayJson (names : List (DeclId * String)) (env : Environment) (named : String * DeclId) : Json

An LCD as the host reads it, from what its chip showed for its number: {name, lines}, the name its declaration has in the sketch (“” for one allocated) and each row of the module.

arduino.Board.servoJson

def Board.servoJson (names : List (DeclId * String)) (env : Environment) (named : String * DeclId) : Json

A servo as the host reads it: {name, pin, angle}, the angle of the last pulse its motor measured (null before any).

arduino.Board.hardware

def Board.hardware (names : List (DeclId * String)) (env : Environment) : String

The hardware at the end, as the earlier model’s showEnv: the clock, the loops, the pins, the servos, the LCDs (named by the sketch’s declarations), the EEPROM’s cells written ([address, byte], in the order first written).

arduino.Board.changeJson

def Board.changeJson (c : PinChange) : Json

A change of a pin’s value as the host reads it: {t, pin, value}, the time in milliseconds.

arduino.Board.run

def Board.run (b : Board) (given : List TimedInput) (fuel : Nat) (input : String) (items : List Item) : RunResult * List (String * Json)

A run of the sketch’s items on the board b with the host’s inputs given, on the input for at most fuel steps: the C++ branch’s verdict, and the fields a host reads, the verdict’s then the pins’ changes and the hardware at the end (only the verdict’s when the run did not finish: a program rejected while checking, or out of steps).

arduino.Board.verdict

def Board.verdict (b : Board) (given : List TimedInput) (fuel : Nat) (input : String) (items : List Item) : String

A run on a board as the host reads it (Board.run of the board b, the inputs given, the fuel, the input and the sketch’s items), as JSON.