RESTful Interface

Till Mossakowski edited this page Nov 8, 2017 · 15 revisions

This is a RESTful Interface for communicating with Hets.

general idea

the interface

  • GET /version. Show version of hets. (example http://rest.hets.eu/version)

  • GET /filetype/coded-iri. Determine in a lightweight and fast way the file type of coded-iri. (example http://rest.hets.eu/filetype/https%3a%2f%2fsvn-agbkb.informatik.uni-bremen.de%2fHets-lib%2ftrunk%2fBasic%2fNumbers.casl)

  • GET /dg/coded-iri/command-list?options. Output the DG as DGXML, considering the DG commands or command line flags in command-list. The DGXML contains IRIs for the individual specs and symbols. (For HetCASL, the IRIs should be library-iri?spec-name resp. library-iri?spec-name?symbol-name but they are still simple names.) For DOL, IRIs are determined by DOL's prefixing mechanism. All the subsequent methods also use the parameters coded-iri, command-list, and option in a similar way to set up a DG.

  • Commands or flags in command-list are separated by slashes. The possible commands are those listed under "commands:" for http://rest.hets.eu/Basic/Numbers.casl

    • auto
    • glob-decomp
    • global-subsume
    • loc-decomp
    • local-infer
    • comp
    • comp-new
    • cons
    • hide-thm
    • thm-hide
    • compute-colimit
    • compute-normal-form
    • triangle-cons
    • freeness
    • importing
    • disjoint-union
    • renaming
    • hiding
    • heterogeneity
    • qualify-all-names
  • The possible flags in command-list are those from the command line. This feature may be deprecated in the future since flags can also be given as part of the query string in options (separated by "&").

    • just-structured
    • unlit
    • relative-positions
    • full-signatures
    • full-theories
    • recursive (does not make much sense)
    • (apply-automatic-rule) prefer command "auto"
    • (normal-form) prefer command "compute-normal-form"
  • The possible options are the long options from the command line (see "hets --help"). Several options are separated by ampersands. An option argument is given (as on the command line) following the equal sign (i.e. ?access-token=TOKEN). The leading two dashes of long options must be omitted in query strings. For simple options it is possible to write i.e. "full-theories=on", but "=on" should be omitted as it is not possible to switch off a flag. Not all options make sense and will be ignored or are forbidden. A particular case is "translation" that is ignored as option but used in queries for prover invocations. (The order of value pairs in query strings does not matter.)

  • from hets version 1407264924 onwards the option ?format=json is supported (example http://rest.hets.eu/dg/https%3a%2f%2fsvn-agbkb.informatik.uni-bremen.de%2fHets-lib%2ftrunk%2fBasic%2fNumbers.casl?format=json)

  • GET /translations/coded-iri/command-list?options&node=iri. Get comorphisms for the node iri (or all nodes' translations, if no iri is given). We have no command to actually only translations one or all nodes yet (without proving or consistency-checking). (NOTE: The command translations was translate in previous versions of Hets)

  • GET /provers/coded-iri/command-list?options&node=iri&translation=iri. Get provers for the node iri (or all nodes' provers, if no iri is given). If translation is given, give those provers available after translation.

  • POST /prove/coded-iri/command-list with the following options in the request body:

  • the above-mentioned options

  • node an IRI

  • theorems a list of goals to prove. If given, this requires node to be set.

  • axioms a list of axioms to use for the proof

  • translation the comorphism to use to translate to the target logic

  • prover the prover to use

  • timeout in seconds

  • include (with value true or false) to include previously proven theorems as axioms for further theorems in the same request

  • includeDetails (default: true) boolean to include the proof details in the response

  • includeProof (default: true) boolean to include the prover output in the response

The request body is expected to have the json format. Some sample requests are:

curl -X POST -H "Content-Type: application/json" -d '{"format": "xml"}' http://localhost:8000/prove/http%3A%2F%2Fdevelop.ontohub.org%2Fdefault%2Fpartial_order%3Fstrict_partial_order
curl -X POST -H "Content-Type: application/json" -d '{"format": "json", "axioms": ["irreflexive", "transitive"], "theorems": ["asymmetric"], "node": "strict_partial_order", "includeProof": "false"}' http://localhost:8000/prove/http%3A%2F%2Fdevelop.ontohub.org%2Fdefault%2Fpartial_order%3Fstrict_partial_order

The response is either formatted in XML (default) or JSON and contains

  • information on each node with proven theorems

    • node name
    • proof goals that hets worked on
      • goal name
      • result of the proof attempt
      • details (optional)
      • used prover
      • used tactic script
      • the proof tree
      • time taken on the proof (different formats)
      • axioms used
      • the prover output (optional)
  • GET /consistency-checkers/coded-iri/command-list?options&node=iri&translation=iri. Get consistency checkers for the node iri (or all nodes' consistency checkers, if no iri is given). If translation is given, give those consistency checkers available after translation.

  • GET /consistency-check/coded-iri/command-list?options&node=iri&consistency-checker=name&translation=iri&timeout=secs. Call the given consistency checker (or the first one if not given) on the given node (or all nodes, if non is given) using the given (or first) comorphism and the other optional parameters.

old interface

  • GET /dir/dir. List folder dir from repository. Returns a list of filenames for use with graph
  • GET /hets-lib/file?format. Get the development graph of file file. Returns the graph as svg, xml or dot (depending on format), where all nodes and edges have been annotated with their ids. (Also class names or other information needs to be added to SVG). A special format is also "session" that is just a number to access the graph later.
  • GET /libraries/coded-iri/development_graph?format=f. Two output formats: (1) just list of nodes and links with their IRIs, (2) whole DG. For now, the interface is synchronous; later on, also an asynchronous answer may be given "please call later". There is no session id. The DG contains IRIs for the individual specs and symbols. for HetCASL, the IRI is library-iri?spec-name resp. library-iri?spec-name?symbol-name. For DOL, IRIs are determined by DOL's prefixing mechanism. Optionally, rettrieve DG for a specific session
  • POST /libraries/coded-iri/sessions create a new proof session for development graph of coded-iri, like current GET command, answer: 201 and location header (=path on server) including the session id.
  • GET /sessions/id?format=f get proof state of session id as a DG
  • efficiency: Hets is provided with caching option, namely one caching location in the file system. The file system should be used as a cache for IRIs, e.g. path-to-cache/sha256sum-of-iri. Clients of Hets should use the same caching mechanism.
  • GET /menus. Get menu structure. Returns a list of triples (XQuery, displayname, action). Actions are node, theory, edge, proveform... and correspond to actions in the Hets development graph menus, and also to actions in this interface. Generally, these should be actions of type GET file?action_name&id=id, that is, the parameters are always the current file and the current (node or edge) id. XQuery can also be "" to denote a global action or "/" to be a menu entry global to the current development graph.
  • GET /nodes/coded-iri?library=coded-iri&session=id. Returns info for the node coded-iri (corresponds to show node info). Optionally, a library where the node resides and a proof session can be specified.
  • GET /nodes/coded-iri/theory?library=coded-iri&session=id. Returns theory (for now as ASCII text) of the node coded-iri (corresponds to show theory).
  • GET /edges/coded-iri?library=coded-iri&session=id. Returns info for the edge coded-iri (corresponds to show edge info).

The development graph calculus interface (stateful with sessions)

  • PUT /libraries/coded-iri/proofs/id/command execute command for session id
  • PUT /sessions/id/command?node=iri&edge=iri. Call command on session id, e.g. applying a development graph calculus rule. Returns a success/failure state. (A returned session id is unchanged.). Only one of node and edge may be provided.
  • GET /sessions/id/provers?node=iri&translation=iri. Get provers for the node iri (or all nodes' provers, if no iri is given). If translation is given, give those provers available after translation.
  • GET /sessions/id/translations?node=iri. Get comorphisms for the node iri (or all nodes' translations, if no iri is given)
  • PUT /sessions/id/prove?node=iri?prover=name&translation=iri&timeout=secs&include=true. Call the given prover (or the first one if not given) on the given node (or all nodes, if non is given) using the given (or first) comorphism and the other optional parameters. Previously proven theorems are not included by default as axioms, unless include=true is specified.
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.