@cella-lang/arduino

Arduino, ESP32 and ESP8266 for the Cella proof checker, as a compiled module pack: C++17 on a board. The board is the program's environment: it decides the data model (the same int is 16 bits on an Uno and 32 bits on an ESP32), and its core and libraries are modeled from their C++ sources.

Depends on @cella-lang/cpp, @cella-lang/cfamily and @cella-lang/machine.

Programs

The JSON of @cella-lang/cfamily's syntax with "lang": {"k": "langCpp"} and a board: {"k": "prog", …, "board": "uno"}.

An unknown board makes the verdict invalid. A program with setup and loop and no main runs like a sketch: setup once, then loop until 5 simulated seconds. A program that defines its own entry (main on the AVR boards, app_main on the ESP32) runs that instead of the core's.

The core and the libraries

The core: pins, time, map, tone and noTone, pulseIn, the board's constants ({"k": "eConst", "name": "LED_BUILTIN"}), Serial, Serial1…, and String. As in a real sketch, a library's names come with its header ({"k": "iInclude", "header": "Servo.h"}): EEPROM.h, Servo.h, DHT.h, LiquidCrystal.h, LiquidCrystal_I2C.h, and on the ESP boards WiFi.h (WiFi.localIP() is an IPAddress, printed as a.b.c.d). Library objects are ordinary objects: declare them with tClass and call their methods with eMCall. The models follow the AVR core, arduino-esp32 3.0.7 and esp8266/Arduino 3.1.2. arduino.boardInfo "uno" lists what a sketch on a board can name: its constants, serial ports, global objects and library classes.

The environment's inputs

The program's JSON may carry the environment's inputs over time beside "board":

"inputs": [{"t": 1500, "key": "analog:A0", "value": 100}]

t is in milliseconds; an input applies once the simulated clock reaches it, and one that names a device waits until the device is declared. The keys:

Devices are named after the variable that declares them (s, lcd, an array's elements arm[0], arm[1]), in the keys and in env alike; an object with no variable (a member, a temporary) is dev<n>. The inputs are the run's environment, not the program's syntax: only this package's entries read them, and a C or C++ program without a board that carries them is invalid.

Verdicts

The verdict JSON of @cella-lang/cfamily, with what the hardware did:

• pins: each change of a pin's value, {t, pin, value} (the PWM duty when set, else the level); at most 1000, and pinsTruncated says when more were dropped;
• env: the hardware at the end: the clock, the loops run, each pin's mode, level, PWM and tone, the servos, the LCDs' rows and the EEPROM cells written.

Entries

• arduino.verdict src input fuel: the verdict; input is what Serial reads. A verdict proved by the kernels: kernel_verdict_in("arduino", "arduino.verdict", …) in cella-lang.
• arduino.types src candidates: the type query (format in @cella-lang/cfamily).
• arduino.boardInfo name: what a sketch on the board can name.
• arduino.withInputs src inputs: the program's JSON with inputs as its "inputs", for a host written in Cella (a JavaScript host sets the field).
• The debugger, for cella-lang/dap: load (applies the program's "inputs"), run, stopConf, stopKind, stopNode, stopOut, stopErr, stopDetail, divergences, feed, globals, frames, setVarErr, setVarConf, env (the hardware of a paused run, as the wiring panel shows it), setInput key value (an input changed while paused), clockMs (the simulated clock); and report input fuel session, a whole run with all the input given at once. cella-lang/dap records the inputs changed while debugging, and inputScript() gives them back as the "inputs" a verdict replays.

Loading

Load the packs into the cella-lang build named by index.json (checkerHash, cbfVersion; the peerDependencies pin it): the standard modules in index.requires["cella-lang"].modules, the packages in index.requires.packages (each the same way), then this package's modules in the order of index.modules.arduino.deps. cella-lang's README (Official packages) has the code.