From 2a917de6d837dd259868f5dc067c0e2cff213b8e Mon Sep 17 00:00:00 2001
From: Karolin Varner <karo@cupdev.net>
Date: Thu, 23 Feb 2023 20:16:54 +0100
Subject: [PATCH] add marzipan, a dialect of proverif

---
 marzipan/marzipan.awk                       | 121 ++++++++++++++++++++
 marzipan/marzipan.vim/ftdetect/marzipan.vim |   1 +
 marzipan/marzipan.vim/ftplugin/marzipan.vim |   3 +
 marzipan/marzipan.vim/syntax/marzipan.vim   |   8 ++
 4 files changed, 133 insertions(+)
 create mode 100644 marzipan/marzipan.awk
 create mode 100644 marzipan/marzipan.vim/ftdetect/marzipan.vim
 create mode 100644 marzipan/marzipan.vim/ftplugin/marzipan.vim
 create mode 100644 marzipan/marzipan.vim/syntax/marzipan.vim

diff --git a/marzipan/marzipan.awk b/marzipan/marzipan.awk
new file mode 100644
index 0000000..c73b1ab
--- /dev/null
+++ b/marzipan/marzipan.awk
@@ -0,0 +1,121 @@
+# Extensions to the proverif/cryptoverif language
+
+BEGIN {
+  buf=""
+  module = ""
+  err = 0
+  long_alias_name = ""
+  long_alias_value = ""
+}
+
+/^@module/ {
+  module=$2
+  for (k in aliases)
+    delete aliases[k];
+  $0=""
+}
+
+/^@alias/ {
+  for (i=2; i<=NF; i++) {
+    split($i, tok, "=");
+    aliases[tok[1]] = tok[2];
+  }
+  $0=""
+}
+
+/^@long-alias-end/ && !long_alias_name {
+  print(\
+    FILENAME ":" NR ": " \
+    "Long alias not started") > "/dev/stderr"
+  err = 1;
+  exit(1);
+}
+
+/^@long-alias-end/ {
+  gsub(/  */, " ", long_alias_value);
+  aliases[long_alias_name] = long_alias_value;
+  $0 = long_alias_name = long_alias_value = "";
+}
+
+/^@long-alias/ {
+  long_alias_name=$2;
+  long_alias_value="";
+  $0="";
+}
+
+/PRIVATE__/ {
+  print(\
+    FILENAME ":" NR ": " \
+    "Used private variable without ~:\n\n" \
+    "    " NR " > " $0) > "/dev/stderr"
+  err = 1;
+  exit(1);
+}
+
+/@(query|reachable|lemma)/ {
+  if (match($0, /@(query|reachable|lemma)\s+"[^"]*"/) == 0) {
+    print(\
+      FILENAME ":" NR ": " \
+      "@query or @reachable statement without parameter:\n\n" \
+      "    " NR " > " $0) > "/dev/stderr"
+    err = 1;
+    exit(1);
+  }
+  pre   = substr($0, 1, RSTART-1);
+  mat   = substr($0, RSTART, RLENGTh)
+  post  = substr($0, RSTART+RLENGTH)
+
+  gsub(/./, " ", mat);
+  $0 = pre mat post;
+}
+
+function istok(c) {
+  return c ~ /[0-9a-zA-Z_\']/;
+}
+
+{
+  gsub("~", "PRIVATE__" module "__", $0);
+}
+
+{
+  orig=$0;
+  minibuf="";
+  for (i=1; i<length($0); i+=1) {
+    a=substr($0, i, 1); # previous character
+    c=substr($0, i+1, 1); # this character
+    if (i > 1 && istok(a)) continue; # We are inside a token
+    if (!istok(c))         continue; # This is not the start of a token
+    # ==> We are at a token boundary
+
+    for (k in aliases) {
+      t=substr($0, i+1, length(k)); # The potential token that equals the alias
+      z=substr($0, i+length(k)+1, 1); # The char after the potential token
+      if (t != k) continue; # Alias does not match
+      if (istok(z)) continue; # Alias matches but is a prefix
+      # ==> ALIAS MATCH
+
+      val = aliases[k];
+      prefix = substr($0, 0, i);
+      suffix = substr($0, i+1+length(k));
+
+      minibuf = minibuf prefix val;
+      $0=suffix;
+      i=1;
+    }
+  }
+  $0 = minibuf $0;
+}
+
+long_alias_name {
+  long_alias_value=long_alias_value $0 " ";
+  $0=""
+}
+
+{
+  buf=buf $0 "\n";
+}
+
+END {
+  if (err == 0)
+    print(buf)
+}
diff --git a/marzipan/marzipan.vim/ftdetect/marzipan.vim b/marzipan/marzipan.vim/ftdetect/marzipan.vim
new file mode 100644
index 0000000..deed8ca
--- /dev/null
+++ b/marzipan/marzipan.vim/ftdetect/marzipan.vim
@@ -0,0 +1 @@
+autocmd BufNewFile,BufRead *.mpv setfiletype marzipan
diff --git a/marzipan/marzipan.vim/ftplugin/marzipan.vim b/marzipan/marzipan.vim/ftplugin/marzipan.vim
new file mode 100644
index 0000000..10e2f29
--- /dev/null
+++ b/marzipan/marzipan.vim/ftplugin/marzipan.vim
@@ -0,0 +1,3 @@
+setlocal commentstring=(*%s*),/*%s*/,//
+" (letters), single quotes (`'`), underscores (`_`), accented letters from the ISO Latin 1 character set
+setlocal isident=a-z,A-Z,_,',48-57,192-214,216-246,248-255
diff --git a/marzipan/marzipan.vim/syntax/marzipan.vim b/marzipan/marzipan.vim/syntax/marzipan.vim
new file mode 100644
index 0000000..5c8fc98
--- /dev/null
+++ b/marzipan/marzipan.vim/syntax/marzipan.vim
@@ -0,0 +1,8 @@
+if exists("b:current_syntax")
+  finish
+endif
+
+runtime syntax/c.vim
+unlet b:current_syntax
+runtime syntax/proverif.vim
+let b:current_syntax = "marzipan"