Antra

Start

Die REPL: Code Stück für Stück auswerten

antra repl startet eine Sitzung, die ihren Zustand behält: Was du einmal definiert hast, steht in der nächsten Eingabe bereit. So kannst du eine Funktion schreiben, ausprobieren, ändern und wieder ausprobieren, ohne das ganze Programm neu zu starten — wie die REPL in Clojure oder Elixir.

Im Terminal#

$ antra repl
antra> fn sq(x) -> x * x
fn sq(x :- Number) :- Number
antra> sq(12)
val it :- Int = 144
antra> val xs = [1,
   ...   2, 3]
val xs :- [Int] = [1, 2, 3]
antra> map(xs, sq)
val it :- [Int] = [1, 4, 9]

Jede Antwort ist selbst gültiges Antra: eine Deklaration mit Typ und Wert. Der Wert eines Ausdrucks heißt it und ist in der nächsten Eingabe gebunden (map(it, sq)). Eine Funktion zeigt ihre Signatur, typedef sich selbst, package, protocol und impl ihren Namen. Strings stehen mit Quotes da ('hallo'). Was println ausgibt, erscheint vor der Antwort; ein Aufruf nur für die Ausgabe (println(...)) oder einer, der undef liefert, bekommt kein it.

Eine Eingabe geht über mehrere Zeilen, solange eine Klammer oder ein String offen ist oder die Zeile auf einen Operator, ein Komma oder -> endet. Eine leere Zeile schickt ab, was da ist, auch Unfertiges. Ctrl-D beendet die Sitzung, exit(n) ebenso, mit dem Status n. Eine Antwort über 2000 Zeichen wird im Terminal gekürzt (… (N more characters)), der Server schickt alles.

Bearbeiten und Verlauf#

Auf einem Terminal bearbeitest du die ganze Eingabe, auch über mehrere Zeilen, und die REPL färbt sie beim Tippen ein (dieselben Farben wie die VS-Code-Extension):

TasteWirkung
← →, Home EndCursor; Ctrl-A/Ctrl-E Zeilenanfang/-ende, Ctrl-B/Ctrl-F ein Zeichen
Alt-B Alt-F, Ctrl-← Ctrl-→ein Wort zurück/vor
Backspace DeleteZeichen löschen
Ctrl-K / Ctrl-Ubis Zeilenende / bis Zeilenanfang löschen
Ctrl-W, Alt-Backspace / Alt-DWort davor / dahinter löschen
↑ ↓in einer mehrzeiligen Eingabe die Zeile wechseln, an ihrem Rand durch den Verlauf
Ctrl-Rim Verlauf suchen; Ctrl-R erneut: älterer Treffer, Enter schickt ihn ab, eine andere Taste übernimmt ihn zum Bearbeiten, Ctrl-C bricht ab
Entereine fertige Eingabe abschicken, in einer unfertigen eine neue Zeile (eingerückt)
Alt-Enterimmer eine neue Zeile
TabNamen ergänzen (siehe unten); am Zeilenanfang oder nach einem Leerzeichen vier Leerzeichen
Ctrl-LBildschirm leeren
Ctrl-CEingabe verwerfen; während einer Auswertung: sie abbrechen (die Sitzung bleibt)
Ctrl-Dauf leerer Eingabe: Sitzung beenden; sonst Zeichen löschen

Vervollständigen mit Tab: Ergänzt wird das Wort vor dem Cursor aus dem, was die Sitzung kennt: eigene val/fn, Builtins, Schlüsselwörter, Paket-Aliase, nach einem Punkt die öffentlichen Funktionen eines importierten Pakets (Array.fi → Array.filter, Array.find, …) und am Zeilenanfang die Kommandos (:do → :doc). Ein Treffer wird eingesetzt, mehrere bis zu ihrem gemeinsamen Anfang; geht es nicht weiter, stehen die Treffer unter der Zeile.

Eine schließende Klammer am Zeilenanfang rückt wieder aus. Eingefügter Text wird so übernommen, wie er ist: ein mehrzeiliges Stück Code aus dem Editor wird nicht Zeile für Zeile abgeschickt, sondern wartet auf Enter.

Der Verlauf hält jede Eingabe als einen Eintrag (auch mehrzeilige) und überdauert die Sitzung: er steht in ~/.antra_history, eine Eingabe pro Zeile (Zeilenumbrüche als \n), die letzten 1000 Einträge. ANTRA_HISTORY nennt eine andere Datei, leer gesetzt schaltet es den Verlauf ab.

Farben gibt es nur auf einem Terminal; NO_COLOR schaltet sie ab, FORCE_COLOR erzwingt sie. Ohne Terminal (stdin aus einer Datei oder Pipe) oder mit TERM=dumb liest die REPL einfach Zeilen, ohne Editor und ohne Farben.

Typen in den Antworten#

Die Typen kommen vom statischen Checker (antra --check), wie in F# Interactive. Die Sitzung merkt sich dafür, was definiert ist, und prüft jede Eingabe im Zusammenhang damit, bevor sie läuft:

antra> %{name: "Ada", born: 1815}
val it :- %{name :- String, born :- Int} = %{ :born => 1815, :name => 'Ada' }
antra> val [a, b] = ["x", 2]
val a :- String = 'x'
val b :- Int = 2
antra> fn get[Key, Val](m :- Map[Key, Val], k :- Key) :- Val -> m[k]
fn get[Key, Val](m :- Map[Key, Val], k :- Key) :- Val

Weiß der Checker zu wenig (Any allein, etwa bei einem Wert aus einer Bibliothek ohne Annotationen, oder _), steht der Typ da, den der Wert selbst zeigt: [Int], %{name :- String}, %Ok[Int]. Bei Werten aus Destructuring gilt das immer. Ein geschriebenes [Any] bleibt stehen.

Annotationen werden im REPL immer auch beim Ausführen geprüft (wie mit --check-types). Der Checker lässt Any überall durch, die Werte aber sind da:

antra> my xs :- [Any] = [4, 9, "x"]
my xs :- [Any] = [4, 9, 'x']
antra> my ys :- [Int] = xs
RUNTIME ERROR (line 2): Type error: 'ys' must be [Int], got [4, 9, 'x'] (annotation at line 2)

Findet der Checker einen Fehler, erscheint er vor der Antwort, mit der Zeile der Eingabe:

antra> val bad = "a" + 1
type error (line 14): '+' takes numbers, got String; join strings with <> [operand-type]
RUNTIME ERROR (line 14): Type error: String cannot be used with '+' — use num() for explicit conversion

Die Eingabe läuft trotzdem — der Checker ist schrittweise und kann sich irren. Mit :strict on läuft sie nicht (wie in F#). Warnungen erscheinen ebenfalls (warning (line 1): … [annotation-spacing]), ohne die unused-*-Warnungen, die in einer REPL fast jedes val träfe; der Server liefert sie in diagnostics.

Kommandos#

Eine Zeile, die mit : beginnt, ist ein Kommando:

KommandoWirkung
:t ausdrucknur der Typ, ohne Auswertung (:t map(xs, sq) → map(xs, sq) :- [Int]; ein Funktionsname zeigt die Signatur)
:doc nameSignatur und Doku-Kommentare (#:) einer Funktion oder eines Pakets: :doc Array.map, :doc Array; mehrere Stelligkeiten je eine Zeile (:doc Array.count), ein Re-Export ohne eigene Doku nennt seine Herkunft; eingebaute Funktionen sind in Kapitel 13 beschrieben
:types on|offTypen in den Antworten (an); aus: val it = 9
:strict on|offEingaben mit einem Checker-Fehler nicht ausführen (aus)
:time on|offnach jeder Antwort die Laufzeit (time: 0.109 ms) (aus)
:helpdie Liste
:quitSitzung beenden (auch Ctrl-D, exit())

Neu definieren#

In einem Skript ist ein Name, der schon gebunden ist, ein Fehler. In der REPL ist das Neuauswerten der Normalfall: Eine Definition ersetzt die frühere.

Definitionin der REPL erneut ausgewertet
fn f(...)ersetzt f (zu Klauseln siehe unten)
val, my, constbindet den Namen neu
impl P for Tersetzt das frühere impl (kein Duplicate-Fehler)
typedef, package, protocolgelten in der neuen Fassung

Bei Funktionen mit mehreren Klauseln entscheidet die Reihenfolge der Eingaben:

  • Klauseln direkt nacheinander bilden eine Funktion, wie im Skript, ob in einer Eingabe oder in mehreren:

    antra> fn fib(n) when n < 2 -> n
    fn fib(n :- Number) :- Number
    antra> fn fib(n) -> fib(n - 1) + fib(n - 2)
    fn fib(n :- Number) :- Number
    antra> fib(10)
    val it :- Int = 55
  • Kam dazwischen etwas anderes, beginnt fn fib(...) die Funktion neu; die alten Klauseln sind weg.

  • Eine Klausel mit denselben Patterns und demselben Guard wie eine vorhandene ist eine Korrektur: Sie ersetzt genau diese Klausel an ihrer Stelle, die anderen bleiben. Innerhalb einer Eingabe bleibt das wie im Skript ein Fehler (duplicate unguarded clause).

Wer fib schon an anderer Stelle hält (ein Lambda, eine Map), sieht die neue Fassung: ersetzt wird die Funktion selbst, nicht nur der Name.

Die Datei der Sitzung#

antra repl examples/trees.ant

Die Datei wird nicht ausgeführt. Sie bestimmt den Suchpfad für import wie bei antra datei.ant (ihr Verzeichnis, lib/ daneben, die Projektwurzel) und den Namen in Fehlermeldungen. Ohne Datei gilt das aktuelle Verzeichnis. -I dir und --no-prelude gehen wie beim normalen Aufruf, vor repl: antra -I lib repl.

Für Editoren: --server#

antra repl --server [datei.ant] ist dieselbe Sitzung für Programme: Auf stdin und stdout steht je ein JSON-Objekt pro Zeile. Zuerst meldet sich der Server:

{"ready": true, "version": "0.9.0"}

Dann wertet er jede Anfrage aus und antwortet mit derselben id:

{"id": 1, "code": "fib(20)", "line": 12}
{"id": 1, "value": "6765", "type": "Int", "display": "val it :- Int = 6765", "out": "", "error": null, "diagnostics": [], "evaluated": true, "ms": 0.699}

Anfrage:

FeldBedeutung
idbeliebiger JSON-Wert, kommt unverändert zurück
codeeine oder mehrere Anweisungen
line(optional) die Dateizeile, in der code beginnt; Fehler und Diagnosen nennen dann Zeilen der Datei
file(optional) wechselt die Datei für Fehlermeldungen
op(optional) "eval" (Standard), "type": nur typisieren, wie :t; "complete": die Namen, die code ergänzen; "doc": wie :doc code
strict(optional) true: bei einem Checker-Fehler nicht ausführen

Antwort:

FeldBedeutung
valueder Wert der letzten Anweisung als Literal; null bei einem Fehler
typesein Typ (bei einer Definition der des Definierten)
displaydie Antwortzeilen wie im Terminal, durch \n getrennt
outwas die Auswertung mit print/println ausgegeben hat
errordie Fehlermeldung (Laufzeit- oder Parse-Fehler, exit(n)), sonst null
diagnosticsFehler und Warnungen des Checkers: line, col, endCol, severity, code, message
evaluatedfalse: nicht ausgeführt (op: "type", strict, Parse-Fehler)
msLaufzeit der Auswertung in Millisekunden

"op": "complete" antwortet {"id": …, "candidates": ["Array.filter", …]}, "op": "doc" antwortet {"id": …, "lines": ["fn Array.filter(…) :- [T]", …]} (die erste Zeile die Signatur, Code aus der Doku mit vier Leerzeichen).

Ein Fehler beendet nur die Anfrage; auch exit(n) lässt die Sitzung weiter laufen. Der Server endet, wenn stdin endet.

Grenzen#

  • Der Editor zählt jedes Zeichen als eine Spalte; breite Zeichen (CJK, viele Emoji) verschieben den Cursor. Unter Windows ist er gebaut, aber noch nicht in einer echten Konsole ausprobiert.
  • Im Server-Modus ist stdin der Kanal der Anfragen: Code, der von stdin liest (IO.prompt, File.read_line(IO.stdin())), liest das Protokoll.
  • Was nicht über print/println geht (ein Kindprozess, ein natives Modul, das direkt schreibt), landet im Server-Modus auf stdout zwischen den Antworten.
  • Der Checker läuft bei jeder Eingabe über alles, was die Sitzung definiert hat: bei einigen hundert Definitionen kostet das wenige Millisekunden pro Eingabe, bei über tausend um 20 ms.
  • Für einen Wert speichert die Sitzung nur seinen Typ, nicht wie er entstand; Typen von Werten aus Destructuring kommen immer aus dem Wert.

Quelle dieser Seite