summaryrefslogtreecommitdiffstats
path: root/tests/snippets/elpi
diff options
context:
space:
mode:
Diffstat (limited to 'tests/snippets/elpi')
-rw-r--r--tests/snippets/elpi/test_catastrophic_backtracking.txt6
-rw-r--r--tests/snippets/elpi/test_chr.txt54
-rw-r--r--tests/snippets/elpi/test_clause.txt67
-rw-r--r--tests/snippets/elpi/test_namespace.txt35
-rw-r--r--tests/snippets/elpi/test_pred.txt60
-rw-r--r--tests/snippets/elpi/test_type.txt112
6 files changed, 334 insertions, 0 deletions
diff --git a/tests/snippets/elpi/test_catastrophic_backtracking.txt b/tests/snippets/elpi/test_catastrophic_backtracking.txt
new file mode 100644
index 0000000..a14a054
--- /dev/null
+++ b/tests/snippets/elpi/test_catastrophic_backtracking.txt
@@ -0,0 +1,6 @@
+---input---
+aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
+
+---tokens---
+'aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa' Text
+'\n' Text.Whitespace
diff --git a/tests/snippets/elpi/test_chr.txt b/tests/snippets/elpi/test_chr.txt
new file mode 100644
index 0000000..75291a3
--- /dev/null
+++ b/tests/snippets/elpi/test_chr.txt
@@ -0,0 +1,54 @@
+---input---
+constraint foo, bar {
+
+ :name "myrule"
+ rule (odd X) \ (even X) | true <=> fail.
+
+}
+rule. % not a kwd
+
+---tokens---
+'constraint' Keyword.Declaration
+' ' Text.Whitespace
+'foo, bar ' Name.Function
+'{' Text
+'\n\n ' Text.Whitespace
+':name' Keyword.Mode
+' ' Text.Whitespace
+'"' Literal.String.Double
+'myrule' Literal.String.Double
+'"' Literal.String.Double
+'\n ' Text.Whitespace
+'rule' Keyword.Declaration
+' ' Text.Whitespace
+'(' Text
+'odd' Text
+' ' Text.Whitespace
+'X' Name.Variable
+')' Operator
+' ' Text.Whitespace
+'\\' Keyword.Declaration
+' ' Text.Whitespace
+'(' Text
+'even' Text
+' ' Text.Whitespace
+'X' Name.Variable
+')' Operator
+' ' Text.Whitespace
+'|' Keyword.Declaration
+' ' Text.Whitespace
+'true' Text
+' ' Text.Whitespace
+'<=>' Keyword.Declaration
+' ' Text.Whitespace
+'fail' Text
+'.' Operator
+'\n\n' Text.Whitespace
+
+'}' Text
+'\n' Text.Whitespace
+
+'rule' Text
+'.' Operator
+' ' Text.Whitespace
+'% not a kwd\n' Comment
diff --git a/tests/snippets/elpi/test_clause.txt b/tests/snippets/elpi/test_clause.txt
new file mode 100644
index 0000000..e485753
--- /dev/null
+++ b/tests/snippets/elpi/test_clause.txt
@@ -0,0 +1,67 @@
+---input---
+true.
+stop :- !.
+of (fun F) :- pi x\ of x => of (F x).
+match (uvar as Y) :- print Y.
+
+---tokens---
+'true' Text
+'.' Operator
+'\n' Text.Whitespace
+
+'stop' Text
+' ' Text.Whitespace
+':-' Keyword.Declaration
+' ' Text.Whitespace
+'!' Keyword.Declaration
+'.' Operator
+'\n' Text.Whitespace
+
+'of' Text
+' ' Text.Whitespace
+'(' Text
+'fun' Text
+' ' Text.Whitespace
+'F' Name.Variable
+')' Operator
+' ' Text.Whitespace
+':-' Keyword.Declaration
+' ' Text.Whitespace
+'pi' Keyword.Declaration
+' ' Text.Whitespace
+'x' Name.Variable
+'\\' Text
+' ' Text.Whitespace
+'of' Text
+' ' Text.Whitespace
+'x' Text
+' ' Text.Whitespace
+'=>' Keyword.Declaration
+' ' Text.Whitespace
+'of' Text
+' ' Text.Whitespace
+'(' Text
+'F' Name.Variable
+' ' Text.Whitespace
+'x' Text
+')' Operator
+'.' Operator
+'\n' Text.Whitespace
+
+'match' Text
+' ' Text.Whitespace
+'(' Text
+'uvar' Keyword.Declaration
+' ' Text.Whitespace
+'as' Keyword.Declaration
+' ' Text.Whitespace
+'Y' Name.Variable
+')' Operator
+' ' Text.Whitespace
+':-' Keyword.Declaration
+' ' Text.Whitespace
+'print' Text
+' ' Text.Whitespace
+'Y' Name.Variable
+'.' Operator
+'\n' Text.Whitespace
diff --git a/tests/snippets/elpi/test_namespace.txt b/tests/snippets/elpi/test_namespace.txt
new file mode 100644
index 0000000..98a35b0
--- /dev/null
+++ b/tests/snippets/elpi/test_namespace.txt
@@ -0,0 +1,35 @@
+---input---
+namespace foo.bar {
+ baz :- std.do! [].
+}
+shorten foo. { bar }.
+
+---tokens---
+'namespace' Keyword.Declaration
+' ' Text.Whitespace
+'foo.bar' Text
+' ' Text.Whitespace
+'{\n' Text
+
+' ' Text.Whitespace
+'baz' Text
+' ' Text.Whitespace
+':-' Keyword.Declaration
+' ' Text.Whitespace
+'std.do!' Text
+' ' Text.Whitespace
+'[]' Keyword.Declaration
+'.' Operator
+'\n' Text.Whitespace
+
+'}\n' Text
+
+'shorten' Keyword.Declaration
+' ' Text.Whitespace
+'foo.' Text
+' ' Text.Whitespace
+'{ ' Text
+'bar' Text
+' ' Text.Whitespace
+'}.' Text
+'\n' Text.Whitespace
diff --git a/tests/snippets/elpi/test_pred.txt b/tests/snippets/elpi/test_pred.txt
new file mode 100644
index 0000000..657c8fd
--- /dev/null
+++ b/tests/snippets/elpi/test_pred.txt
@@ -0,0 +1,60 @@
+---input---
+pred p1.
+pred p2 i:int, o:list A.
+pred p3 i:(bool -> prop).
+:index(_ 2) pred p4 i:int, i:A.
+
+---tokens---
+'pred' Keyword.Declaration
+' ' Text.Whitespace
+'p1' Name.Function
+'.' Text
+'\n' Text.Whitespace
+
+'pred' Keyword.Declaration
+' ' Text.Whitespace
+'p2' Name.Function
+' ' Text.Whitespace
+'i:' Keyword.Mode
+'int' Keyword.Type
+',' Text
+' ' Text.Whitespace
+'o:' Keyword.Mode
+'list' Keyword.Type
+' ' Text.Whitespace
+'A' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+'pred' Keyword.Declaration
+' ' Text.Whitespace
+'p3' Name.Function
+' ' Text.Whitespace
+'i:' Keyword.Mode
+'(' Keyword.Type
+'bool' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'prop' Keyword.Type
+')' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+':index' Keyword.Mode
+'(' Text.Whitespace
+'_ 2' Literal.Number.Integer
+')' Text
+' ' Text.Whitespace
+'pred' Keyword.Declaration
+' ' Text.Whitespace
+'p4' Name.Function
+' ' Text.Whitespace
+'i:' Keyword.Mode
+'int' Keyword.Type
+',' Text
+' ' Text.Whitespace
+'i:' Keyword.Mode
+'A' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
diff --git a/tests/snippets/elpi/test_type.txt b/tests/snippets/elpi/test_type.txt
new file mode 100644
index 0000000..8a506ce
--- /dev/null
+++ b/tests/snippets/elpi/test_type.txt
@@ -0,0 +1,112 @@
+---input---
+kind list type -> type.
+type nil list A.
+type cons A -> list A -> list A.
+kind tm type.
+type fun (tm -> tm) -> tm.
+type app tm -> tm -> tm.
+pred foo i:(tm -> tm), o:tm.
+
+---tokens---
+'kind' Keyword.Declaration
+' ' Text.Whitespace
+'list' Name.Function
+' ' Text.Whitespace
+'type' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'type' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+'type' Keyword.Declaration
+' ' Text.Whitespace
+'nil' Name.Function
+' ' Text.Whitespace
+'list' Keyword.Type
+' ' Text.Whitespace
+'A' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+'type' Keyword.Declaration
+' ' Text.Whitespace
+'cons' Name.Function
+' ' Text.Whitespace
+'A' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'list' Keyword.Type
+' ' Text.Whitespace
+'A' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'list' Keyword.Type
+' ' Text.Whitespace
+'A' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+'kind' Keyword.Declaration
+' ' Text.Whitespace
+'tm' Name.Function
+' ' Text.Whitespace
+'type' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+'type' Keyword.Declaration
+' ' Text.Whitespace
+'fun' Name.Function
+' ' Text.Whitespace
+'(' Keyword.Type
+'tm' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'tm' Keyword.Type
+')' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'tm' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+'type' Keyword.Declaration
+' ' Text.Whitespace
+'app' Name.Function
+' ' Text.Whitespace
+'tm' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'tm' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'tm' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
+
+'pred' Keyword.Declaration
+' ' Text.Whitespace
+'foo' Name.Function
+' ' Text.Whitespace
+'i:' Keyword.Mode
+'(' Keyword.Type
+'tm' Keyword.Type
+' ' Text.Whitespace
+'->' Keyword.Type
+' ' Text.Whitespace
+'tm' Keyword.Type
+')' Keyword.Type
+',' Text
+' ' Text.Whitespace
+'o:' Keyword.Mode
+'tm' Keyword.Type
+'.' Text
+'\n' Text.Whitespace
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-06 20:09:17 +0000