• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
          • Vls-commands
            • Vls-command-args-to-eformals
            • Vls-commandinfo-p
            • Vls-success
            • Vls-commandinfolist-p
            • Commands-table
            • Define-vls-command-fn
            • Vls-fail-fn
            • Vls-fail
            • Vls-command-arg-to-eformal
            • Vls-commandtype-p
            • Get-vls-commands
          • Vl-descriptionlist-summaries
          • Vls-transdb
          • File-layout
          • Vls-data-p
          • Ts-queue
          • Vls-showloc
          • Vls-get-plainsrc
          • Vl-description->warnings
          • Vl-describe
          • Vls-port-table
          • Vls-describe
          • Vls-data-from-translation
          • Vl-find-description-insensitive
          • Vls-get-warnings
          • Vls-get-summary
          • Vls-get-origsrc
          • Vls-data-origname-reportcard
          • Vls-get-parents
          • Vls-get-children
          • Vls-get-summaries
          • Vl-ppc-description
          • Vls-get-desctypes
          • Vl-description-summary
          • Start
          • Vl-descalist->descriptions/types
          • Stop
        • Kit
        • Printer
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Server

Vls-commands

A simple command format for interfacing between Lisp and Javascript.

Introduction

The VL server makes many Lisp functions available for use by the Javascript code that runs the module browser. To make interfacing between Javascript and Lisp simpler, we adopt certain conventions for how these commands work.

A few of VL server operations, such as those for selecting models, are special and do not follow the normal conventions. However, for the most part, we are generally wanting to deal with commands where:

  • The command is a get operation that affects no state except perhaps for implicit state like memoization tables, hons spaces, etc. We'll arrange so that the memo tables and hons spaces are set up correctly before invoking the command.
  • The model has already been selected. We'll arrange so that the server code will access the proper model, and invoke our Lisp command function with the selected vls-data-p structure as one of its arguments.
  • The command may need other arguments. To keep the command format regular, we'll require the Lisp function to take any extra arguments as strings, and it will be responsible for parsing these as necessary, e.g., to convert line numbers from "5" into 5.
  • The command may produce JSON or HTML formatted output.

JSON Commands

Most commands need to dive down into part of the model and retrieve some information. This process might fail or succeed. For uniformity on the Javascript side, we will expect each JSON-producing command to signal its failure by producing a JSON-encoded error message of the form:

{":ERROR": "Couldn't do such and so..."}

This can be done by calling vls-fail. Meanwhile, every JSON-producing command that succeeds should produce a result of the form:

{":ERROR": false,
 ":VALUE": ...actual result goes here...}
}

This can be done by calling vls-success.

HTML Commands

HTML producing commands are assumed to never fail. Their content is generally intended to be sent directly to the web browser and not processed further. An HTML-producing command can generally produce a simple error message in HTML format.

Subtopics

Vls-command-args-to-eformals
(vls-command-args-to-eformals x) maps vls-command-arg-to-eformal across a list.
Vls-commandinfo-p
Vls-success
Create a "standard", JSON-encoded successful return value for a VL server command.
Vls-commandinfolist-p
(vls-commandinfolist-p x) recognizes lists where every element satisfies vls-commandinfo-p.
Commands-table
A list of registered vls-commands.
Define-vls-command-fn
Vls-fail-fn
Vls-fail
Create a "standard", JSON-encoded error message for a VL server command.
Vls-command-arg-to-eformal
Vls-commandtype-p
Get-vls-commands