# string-diagram

tool & library to visualize, edit and perform graphical rewriting steps in string diagrams

homepage: https://perso.ens-lyon.fr/damien.pous/string-diagrams/
companion Rocq library: https://github.com/damien-pous/categories/

# build instructions

opam install dune cairo2-gtk otfm vg
make

+ brr & js_of_ocaml-ppx to compile the web applet
(comment the relevant lines in bin/dune if installing these optional dependencies is problematic)


# using the program

make run

enter your favorite goal in the text box,
or use Ctrl-O to open one of the .sd files in the toplevel directory


# syntax

the syntax is designed to be permissive, several tokens are mapped to the same behaviour.
for instance, both
- "*", "⊗" and "\otimes" denote the tensor product
- ".", "·" and "\cdot" denote its application to morphisms
- "=", "≡" ant "≡'" denote equality
- "~>" and "->" denote arrow
- composition can be written forward (";", "\;",  ";;") or backward ("°", "∘",  "∘∘")

see *.sd files for examples, and files lib/lexer.mll and lib/parser.mly for a complete description

when copy-pasting a Rocq goal, remove irrelevant hypotheses, including the declaration of the ambiant monoidal category and the object declarations.


# keys

1..n    rewrite box using matching hypothesis
u       unbox or unfold node
t       toggle node labels
-/+     shrink/enlarge element
f       release fixed element
l       toggle labels printing
c       toggle contours printing
=       fit screen
r       redraw picture
e       toggle link edition mode
d       remove node
n       create node (give name afterward)
t       export term to clipboard
p/g     export diagram as pdf/svg
R       export Rocq script to clipboard
->/<-   undo/redo
SPACE   pause/start animation
ESC     abort current action
Ctrl-O  open file
Ctrl-S  save file
Ctrl-E  save as file
Ctrl-V  load from clipboard
Ctrl-F  toggle fullscreen


# modules

## lib
Misc:        miscellaneous utilities

Set:         finite sets
MSet:        finite multisets
Seq:         finite sequences, index starting at 1, usually duplicate-free
Perm:        finite support permutations
Inj:         finite support injections
ISeq:        increasing sequences
Stack:       lists with insertion capabilities at a designated position

Types:       shared class & module types (no implementation)
Graph_type:  graph class types (no implementation)

Constants:   constants for drawing graphs
Info:        informations about vertices & edges

Lexer:       lexer
Parser:      parser (produces raw terms)

Canvas:      canvas for drawing pictures
Polygon:     utilities about polygons
Geometry:    geometric utilities to draw edges
Arena: 	     canvas + viewport

Graph:       string diagrams (often called graphs in the implementation) and associated functions 

Place:       placing graphs

File:        SD files and functions to manipulate them

Program:     UI-independent main program

GArena:	     GTK arena


## bin
Sd:          GTK main program
Applet:      javascript web applet
Check:	     text mode program to check .sd files

## tests
Sanity:      sanity checks