Wenn ich es richtig verstehe (hauptsächlich aus der Existenz der applyTactic Funktion), ist es möglich, benutzerdefinierte Taktiken für den Theorembeweiser in Idris zu schreiben. Was (oder wo) sind Beispiele dafür, wie ich das lernen könnte?Custom Prover Taktik in Idris
Es gibt zwei Mechanismen zum Schreiben von benutzerdefinierten Taktiken in Idris: High-Level und Low-Level-Reflexion.
Mithilfe von High-Level-Reflektion schreiben Sie eine Funktion, die auf Syntax anstatt auf ausgewerteten Daten ausgeführt wird - es wird sein Argument nicht reduzieren. Diese Funktionen geben eine neue Taktik zurück, die mit den bereits bestehenden Taktiken in Idris definiert wurde. Wenn Sie einen Prüfterm direkt zurückgeben möchten, können Sie einfach Exact verwenden. Ein Beispiel für diese Art der Reflexion findet sich in the effects library. High-Level-Reflektionstaktiken werden unter Verwendung von byReflection im Proof-Modus aufgerufen.
In der Low-Level-Reflektion arbeiten Sie direkt mit zitierten Termen aus der Kerntyptheorie von Idris. Eine Taktik ist dann eine Funktion in TT -> List (TTName, TT) -> Tactic, wobei das erste Argument der Zieltyp ist, das zweite der lokale Proofkontext und das Rückgabeergebnis dasselbe wie bei der Hochreflexion. Dies ist, was laughadelic mit above verbunden ist. Diese werden unter Verwendung von applyTactic im Proof-Modus aufgerufen.
Ich weiß nichts darüber, wie man es schreibt und benutzt, aber ich habe kürzlich gesehen [ein Beispiel für benutzerdefinierte Taktik] (https://github.com/idris-lang/Idris-dev/blob/master /libs/base/Data/Vect.idr#L18-L22) und [ein Beispiel für die Verwendung] (https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/ HVect.idr # L57). Hoffe, das wird helfen. – laughedelic
Es tut, danke. –
Die obigen Links sind nicht mehr gültig, da sie sich auf den HEAD des Repos beziehen. Bitte sehen Sie stattdessen hier: [erste] (https://github.com/idris-lang/Idris-dev/blob/10ef56b8c1629347ab213e97bfff551ee27e11d0/libs/base/Data/Vect.idr#L18-L22), [zweite] (https: //github.com/idris-lang/Idris-dev/blob/fb6a0ed1ad5e3acc3795d7ab674977bdb419129a/libs/base/Data/HVect.idr#L57) –