v1.1.4

Small fixes about "fst", "snd", and "pair" functions.
New logo.
Comments in the code.

v1.1.0

New checks

• Checks wether all variables in the right part of a macro are in the left part or public.
• Checks wether all variable in the right part of an equation are in the left part.
• Provides a quick fix for function names again with editing distance.
• Checks wether built-ins are imported to use corresponding functions or symbols (provides a quick fix to import the right built-in).

Fixes

• Editing distance is now used to display all close tokens (distance < 3) and not the first one only.
• diff is considered as a reserved function symbol so that there is no error while using it.
• Functions with arity 0 may be used without parenthesis.

v1.0.1

Release fixes

Package.json fix

v1.0.0

Tamarin Visual Studio Code extension

A Visual Studio Code extension for Tamarin files (.spthy) based on giclu-3's extension and using Tamarin's tree-sitter grammar.

Features:

• Enhances giclu-3's syntax highlighting.

• Adds comprehensive syntax error detection based on the grammar with MISSING or ERROR messages.

• Provides various wellformedness checks:

  • Checks position and usage of reserved facts (Fr, Out, In, K, KD, KU).
  • Checks whether variable are used consistly inside a rule, i.e., using the same capitalization and sort.
  • Spellcheck on facts (must start with an uppercase letter).
  • Checks whether all variables in the conclusion of a rule appear in the premises (except public variables).
  • Checks the arity of facts and functions.
  • Checks whether a lemma uses free terms.
  • Checks whether all facts in the premises of the rules appear in the conclusion of some (other) rule (provides a quick fix by using the closest exisiting fact, based on editing distance).

  This is a subset of the checks performed by Tamarin. For more details on Tamarin's wellformedness checks, see the corresponding Tamarin Prover manual section.

• Use right click and Rename on an indentifier to rename all occurences of it inside a rule or a lemma.

• Use right click and Search Definition on facts or function names and press CTRL+TAB to navigate through all occurences.