Skip to content

Commit

Permalink
refactor: Color let, letfun, set
Browse files Browse the repository at this point in the history
  • Loading branch information
@famoser
famoser committed Mar 2, 2024
1 parent 59e6d19 commit cc4b5eb
Show file tree
Hide file tree
Showing 2 changed files with 144 additions and 63 deletions.
4 changes: 4 additions & 0 deletions docs/sample.pv
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,10 @@ channel public2.
letfun no_conversion(key: key_t) = key.
let publish(key: key_t or fail) = out(public, key).

set attacker = passive.
set reconstructTrace = 2.
set privateCommOnPublicTerms = false.

equation forall key,key':key_t;
key = key'.

Expand Down
203 changes: 140 additions & 63 deletions syntaxes/pv.tmLanguage.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,8 +107,8 @@
]
},
{
"//comment" : "Declaration of let and letfun",
"begin": "(\\b(let|letfun)\\b)",
"//comment" : "Declaration of let",
"begin": "(\\b(let)\\b)",
"end": "(?=\\.)",
"beginCaptures": {
"1": { "name": "keyword.control.proverif" }
Expand All @@ -126,30 +126,55 @@
{ "include": "#fun_ident" }
]
},


{
"//comment" : "Declaration of channels",
"begin" : "(channel)\\s+",
"//comment" : "Declaration of letfun",
"begin": "(\\b(letfun)\\b)",
"end": "(?=\\.)",
"beginCaptures": { "1": { "name": "keyword.control.proverif" } },
"beginCaptures": {
"1": { "name": "keyword.control.proverif" }
},
"patterns": [
{ "include": "#comments" },
{ "include": "#variable_ident" }
{
"begin": "=",
"end": "(?=\\.)",
"patterns": [
{ "include": "#pterm" }
]
},
{ "include": "#parenthesis_nevartypeorfail" },
{ "include": "#fun_ident" }
]
},
{
"//comment": "Declaration of set parameters",
"begin" : "(set)\\s+(\\w+)",
"end": "\\.",
"begin" : "(\\b(set)\\b)",
"end": "(?=\\.)",
"beginCaptures": {
"1": { "name": "keyword.control.proverif" },
"2": { "name": "storage.modifier" }
"1": { "name": "keyword.control.proverif" }
},
"patterns": [
{ "include": "#comments" },
{ "include": "#boolean"},
{ "include": "#nat"}
{
"begin": "=",
"end": "(?=\\.)",
"patterns": [
{ "include": "#settings" }
]
},
{ "include": "#storage_ident"}
]
},


{
"//comment" : "Declaration of channels",
"begin" : "(channel)\\s+",
"end": "(?=\\.)",
"beginCaptures": { "1": { "name": "keyword.control.proverif" } },
"patterns": [
{ "include": "#comments" },
{ "include": "#variable_ident" }
]
},
{
Expand Down Expand Up @@ -230,7 +255,7 @@
},
{
"//comment" : "Declaration of def",
"begin": "(def)\\s+([a-zA-Z'0-9_]*)",
"begin": "(def)\\s+([a-zA-Z'0-9_]+)",
"end": "(?={)",
"beginCaptures": {
"1": { "name": "keyword.control.proverif" },
Expand All @@ -244,22 +269,20 @@
],
"repository": {
"type_ident": {
"match" : "([a-zA-Z'0-9_]*)",
"captures": {
"1": { "name": "entity.name.type.proverif" }
}
"match" : "([a-zA-Z'0-9_]+)",
"name": "entity.name.type.proverif"
},
"fun_ident": {
"match" : "([a-zA-Z'0-9_]*)",
"captures": {
"1": { "name": "entity.name.function.proverif" }
}
"match" : "([a-zA-Z'0-9_]+)",
"name": "entity.name.function.proverif"
},
"variable_ident": {
"match" : "([a-zA-Z'0-9_]*)",
"captures": {
"1": { "name": "variable.other.proverif" }
}
"match" : "([a-zA-Z'0-9_]+)",
"name": "variable.other.proverif"
},
"storage_ident": {
"match" : "([a-zA-Z'0-9_]+)",
"name": "storage.modifier.proverif"
},
"parenthesis_funseq": {
"begin" : "\\(",
Expand Down Expand Up @@ -300,7 +323,7 @@
"patterns": [
{ "include": "#comments"},
{
"match": "[a-zA-Z'0-9_]*",
"match": "[a-zA-Z'0-9_]+",
"name": "entity.name.tag.proverif"
}
]
Expand All @@ -311,7 +334,7 @@
"patterns": [
{ "include": "#comments"},
{
"match": "[a-zA-Z'0-9_]*",
"match": "[a-zA-Z'0-9_]+",
"name": "variable.other.proverif"
}
]
Expand All @@ -329,6 +352,26 @@
{ "include": "#term" }
]
},
"settings": {
"patterns": [
{
"match": "(\\b(true|false)\\b)",
"name": "constant.language.proverif"
},
{
"match": "-",
"name": "keyword.operator.arithmetic.proverif"
},
{
"match": "(\\b([0-9]+)\\b)",
"name": "constant.numeric.proverif"
},
{
"match" : "([a-zA-Z'0-9_]+)",
"name": "support.constant.proverif"
}
]
},
"term": {
"patterns": [
{
Expand All @@ -353,6 +396,35 @@
}
]
},
"pterm": {
"patterns": [
{
"match": "(\\b(if|then|let|suchthat|event|insert|get)\\b)",
"name": "keyword.control.proverif"
},
{
"match": "(\\b(choice|diff|not)\\b)",
"name": "keyword.operator.proverif"
},
{
"match": "(\\b(true|false)\\b)",
"name": "constant.language.proverif"
},
{
"match": "(-|\\+)",
"name": "keyword.operator.arithmetic.proverif"
},
{
"match": "(<|>|<=|>=|=|<>|\\|\\||&&)",
"name": "keyword.operator.comparison.proverif"
},
{
"match": "(\\b([0-9]+)\\b)",
"name": "constant.numeric.proverif"
},
{ "include": "#new_decl" }
]
},
"forallvartype": {
"begin": "(forall)",
"end": ";",
Expand Down Expand Up @@ -381,11 +453,15 @@
"patterns": [
{ "include": "#comments" },
{ "include": "#new_decl" },
{ "include": "#one_var_decl" },
{ "include": "#letinsimple" },
{ "include": "#keywords" },
{ "include": "#boolean" },
{ "include": "#nat" },
{
"match": "(\\b(foreach|yield|if|then|in|out|let|suchthat|insert|get|event|phase|sync)\\b)",
"name": "keyword.control.proverif"
},
{
"match": "!",
"name": "keyword.control.proverif"
},
{ "include": "#pterm" },
{ "include": "#options" }
]
},
Expand All @@ -405,6 +481,31 @@
"4": { "name": "keyword.control.proverif" }
}
},
"new_decl": {
"begin": "(\\b(new)\\b)",
"end": "(?=;)",
"captures": {
"1": { "name": "keyword.control.proverif" }
},
"patterns": [
{ "include": "#comments"},
{
"begin": ":",
"end": "(?=;)",
"patterns": [
{ "include": "#comments"},
{ "include": "#options" },
{ "include": "#type_ident" }
]
},
{ "include": "#variable_ident" },
{ "include": "#vars_options" }
]
},





"forall_mayfail": {
"begin": "(forall)",
Expand All @@ -413,12 +514,12 @@
"patterns": [
{ "include": "#comments" },
{
"match": "([\\s,a-zA-Z0-9'_]*)(:)\\s*([a-zA-Z'0-9_]*)(\\s+(or)\\s+(fail))?",
"match": "([\\s,a-zA-Z0-9'_]*)(:)\\s*([a-zA-Z'0-9_]+)(\\s+(or)\\s+(fail))?",
"captures":{
"1": {
"patterns": [
{
"match": "[a-zA-Z'0-9_]*",
"match": "[a-zA-Z'0-9_]+",
"name": "variable.other.proverif"
}
]
Expand Down Expand Up @@ -492,7 +593,7 @@
]
},
"letinsimple": {
"begin": "(let)\\s+([a-zA-Z'0-9_]*)\\s+(=)",
"begin": "(let)\\s+([a-zA-Z'0-9_]+)\\s+(=)",
"end": "(\\s|^)(in)(\\s|\\n)",
"beginCaptures": {
"1": { "name": "keyword.control.proverif" },
Expand All @@ -511,7 +612,7 @@
]
},
"letinsimple_query": {
"begin": "(let)\\s+([a-zA-Z'0-9_]*)\\s+(=)",
"begin": "(let)\\s+([a-zA-Z'0-9_]+)\\s+(=)",
"end": "(\\s|^)(in)(\\s|\\n)",
"beginCaptures": {
"1": { "name": "keyword.control.proverif" },
Expand All @@ -528,37 +629,13 @@
]
},
"one_var_decl": {
"match": "([a-zA-Z_][a-zA-Z0-9'_]*)(:)\\s*([a-zA-Z0-9'_]*)",
"match": "([a-zA-Z0-9'_]*)(:)\\s*([a-zA-Z0-9'_]*)",
"captures":{
"1": { "name": "variable.other.proverif" },
"2": { "name": "keyword.control.proverif" },
"3": { "name": "entity.name.type.proverif" }
}
},
"new_decl": {
"begin": "(new)(\\n|\\s)",
"end": "(?=;)",
"captures": {
"1": { "name": "keyword.control.proverif" }
},
"patterns": [
{ "include": "#comments"},
{
"begin": "(:)",
"end": "(?=;)",
"captures": {
"1": { "name": "keyword.control.proverif" }
},
"patterns": [
{ "include": "#comments"},
{ "include": "#options" },
{ "include": "#type_ident" }
]
},
{ "include": "#variable_ident" },
{ "include": "#vars_options" }
]
},
"keywords": {
"patterns": [
{
Expand Down

0 comments on commit cc4b5eb

Please sign in to comment.