From 571f8dedeb24015e60d918c3c4edabcadc8114bb Mon Sep 17 00:00:00 2001 From: gares Date: Thu, 28 Nov 2024 21:14:49 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20LPCIC/co?= =?UTF-8?q?q-elpi@2d729c70c9f561a47a4af4198f6359ca9f8142f6=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- stlc.html | 382 ------------------- stlc.txt | 669 +++++++++++++++++++++++++++++++++ tutorial_coq_elpi_HOAS.html | 120 +++--- tutorial_coq_elpi_command.html | 142 +++---- tutorial_coq_elpi_tactic.html | 153 ++++---- tutorial_elpi_lang.html | 467 +++++++++++++---------- 6 files changed, 1168 insertions(+), 765 deletions(-) delete mode 100644 stlc.html create mode 100644 stlc.txt diff --git a/stlc.html b/stlc.html deleted file mode 100644 index d78537d73..000000000 --- a/stlc.html +++ /dev/null @@ -1,382 +0,0 @@ - - - - - /home/runner/work/coq-elpi/coq-elpi/_build/default/examples/stlc.html - - - - - - - -

/home/runner/work/coq-elpi/coq-elpi/_build/default/examples/stlc.html

- -

Filter predicate:

-
File "elpi-builtin.elpi", line 9, column 0, character 89:
true
-
File "elpi-builtin.elpi", line 28, column 0, character 296:
A
(A ; 
_)
-
File "elpi-builtin.elpi", line 30, column 0, character 311:
B
(_ ; 
B)
-
File "elpi-builtin.elpi", line 52, column 0, character 609:
X,
!,
fail
not X
-
File "elpi-builtin.elpi", line 54, column 0, character 631:
not _
-
File "elpi-builtin.elpi", line 67, column 0, character 974:
halt
stop
-
File "elpi-builtin.elpi", line 73, column 0, character 1031:
calc Y X
X is 
Y
-
File "elpi-builtin.elpi", line 173, column 0, character 2867:
gt_ X Y
> X Y
-
File "elpi-builtin.elpi", line 175, column 0, character 2888:
lt_ X Y
X < 
Y
-
File "elpi-builtin.elpi", line 177, column 0, character 2909:
le_ X Y
=< X Y
-
File "elpi-builtin.elpi", line 179, column 0, character 2930:
ge_ X Y
>= X Y
-
File "elpi-builtin.elpi", line 183, column 0, character 3002:
lt_ X Y
i< X Y
-
File "elpi-builtin.elpi", line 185, column 0, character 3023:
gt_ X Y
i> X Y
-
File "elpi-builtin.elpi", line 187, column 0, character 3044:
le_ X Y
i=< X Y
-
File "elpi-builtin.elpi", line 189, column 0, character 3065:
ge_ X Y
i>= X Y
-
File "elpi-builtin.elpi", line 193, column 0, character 3141:
lt_ X Y
r< X Y
-
File "elpi-builtin.elpi", line 195, column 0, character 3162:
gt_ X Y
r> X Y
-
File "elpi-builtin.elpi", line 197, column 0, character 3183:
le_ X Y
r=< X Y
-
File "elpi-builtin.elpi", line 199, column 0, character 3204:
ge_ X Y
r>= X Y
-
File "elpi-builtin.elpi", line 203, column 0, character 3282:
lt_ X Y
s< X Y
-
File "elpi-builtin.elpi", line 205, column 0, character 3303:
gt_ X Y
s> X Y
-
File "elpi-builtin.elpi", line 207, column 0, character 3324:
le_ X Y
s=< X Y
-
File "elpi-builtin.elpi", line 209, column 0, character 3345:
ge_ X Y
s>= X Y
-
File "elpi-builtin.elpi", line 230, column 0, character 3755:
fst (pr A _) A
-
File "elpi-builtin.elpi", line 234, column 0, character 3800:
snd (pr _ B) B
-
File "elpi-builtin.elpi", line 262, column 0, character 4438:
trace.counter C N
counter C N
-
File "elpi-builtin.elpi", line 293, column 0, character 5594:
rex.match Rx S
rex_match Rx S
-
File "elpi-builtin.elpi", line 297, column 0, character 5716:
rex.replace Rx R S O
rex_replace Rx R S O
-
File "elpi-builtin.elpi", line 301, column 0, character 5841:
rex.split Rx S L
rex_split Rx S L
-
File "elpi-builtin.elpi", line 335, column 0, character 7069:
same_term X Y
== X Y
-
File "elpi-builtin.elpi", line 369, column 0, character 8255:
is_cdata X (ctype S)
primitive? X S
-
File "elpi-builtin.elpi", line 399, column 0, character 9284:
B,
!,
T
if B T _
-
File "elpi-builtin.elpi", line 400, column 0, character 9305:
E
if _ _ E
-
File "elpi-builtin.elpi", line 404, column 0, character 9448:
G1,
!,
P1
if2 G1 P1 _ _ _
-
File "elpi-builtin.elpi", line 405, column 0, character 9480:
G2,
!,
P2
if2 _ _ G2 P2 _
-
File "elpi-builtin.elpi", line 406, column 0, character 9512:
E
if2 _ _ _ _ E
-
File "builtin_stdlib.elpi: default-fatal-error", line 16, column 0, character 659:
halt Msg
std.fatal-error Msg
-
File "builtin_stdlib.elpi: default-fatal-error-w-data", line 20, column 0, character 756:
halt Msg : Data
std.fatal-error-w-data Msg Data
-
File "builtin_stdlib.elpi: default-debug-print", line 24, column 0, character 874:
print Msg Data
std.debug-print Msg Data
-
File "builtin_stdlib.elpi", line 30, column 0, character 1007:
P,
!
std.ignore-failure! P
-
File "builtin_stdlib.elpi", line 31, column 0, character 1034:
std.ignore-failure! _
-
File "builtin_stdlib.elpi", line 34, column 0, character 1072:
P,
!
std.once P
-
File "builtin_stdlib.elpi", line 38, column 0, character 1190:
(Cond ; 
std.fatal-error-w-data Msg Cond),
!
std.assert! Cond Msg
-
File "builtin_stdlib.elpi", line 43, column 0, character 1441:
Cond Diagnostic,
!,
(Diagnostic = 
ok ; 
Diagnostic = 
(error S),
std.fatal-error-w-data Msg S),
!
std.assert-ok! Cond Msg
-
File "builtin_stdlib.elpi", line 44, column 0, character 1555:
std.fatal-error-w-data Msg no diagnostic returned
std.assert-ok! _ Msg
-
File "builtin_stdlib.elpi", line 48, column 0, character 1717:
trace.counter run NR,
if (not
(NR = 
0))
(std.debug-print run= NR) true,
std.debug-print ----<<---- enter: P,
P,
std.debug-print ---->>---- exit: P
std.spy P
-
File "builtin_stdlib.elpi", line 52, column 0, character 1898:
std.debug-print ---->>---- fail: P,
fail
std.spy P
-
File "builtin_stdlib.elpi", line 56, column 0, character 2036:
trace.counter run NR,
if (not
(NR = 
0))
(std.debug-print run= NR) true,
std.debug-print ----<<---- enter: P,
P,
std.debug-print ---->>---- exit: P,
!
std.spy! P
-
File "builtin_stdlib.elpi", line 60, column 0, character 2221:
std.debug-print ---->>---- fail: P,
fail
std.spy! P
-
File "builtin_stdlib.elpi", line 64, column 0, character 2330:
std.unsafe-cast X X
-
File "builtin_stdlib.elpi", line 69, column 0, character 2402:
std.length L N1,
N is 
N1 + 
1
std.length
[
_ | L
]
N
-
File "builtin_stdlib.elpi", line 70, column 0, character 2446:
std.length [] 0
-
File "builtin_stdlib.elpi", line 73, column 0, character 2492:
std.rev.aux L [] RL
std.rev L RL
-
File "builtin_stdlib.elpi", line 76, column 0, character 2567:
std.rev.aux XS
[
X | ACC
]
R
std.rev.aux
[
X | XS
]
ACC R
-
File "builtin_stdlib.elpi", line 77, column 0, character 2613:
std.rev.aux [] L L
-
File "builtin_stdlib.elpi", line 80, column 0, character 2655:
std.fatal-error last on empty list
std.last [] _
-
File "builtin_stdlib.elpi", line 81, column 0, character 2702:
!
std.last
[
X
]
X
-
File "builtin_stdlib.elpi", line 82, column 0, character 2719:
std.last XS R
std.last
[
_ | XS
]
R
-
File "builtin_stdlib.elpi", line 85, column 0, character 2790:
std.append XS L L1
std.append
[
X | XS
]
L
[
X | L1
]
-
File "builtin_stdlib.elpi", line 86, column 0, character 2833:
std.append [] L L
-
File "builtin_stdlib.elpi", line 89, column 0, character 2893:
std.appendR [] L L
-
File "builtin_stdlib.elpi", line 90, column 0, character 2909:
std.appendR XS L L1
std.appendR
[
X | XS
]
L
[
X | L1
]
-
File "builtin_stdlib.elpi", line 93, column 0, character 2991:
!
std.take 0 _ []
-
File "builtin_stdlib.elpi", line 94, column 0, character 3009:
N1 is 
- N 1,
std.take N1 XS L
std.take N
[
X | XS
]
[
X | L
]
-
File "builtin_stdlib.elpi", line 95, column 0, character 3062:
std.fatal-error take run out of list items
std.take _ _ _
-
File "builtin_stdlib.elpi", line 98, column 0, character 3161:
std.length L M,
D is 
- M N,
std.drop D L R
std.take-last N L R
-
File "builtin_stdlib.elpi", line 104, column 0, character 3260:
!
std.drop 0 L L
-
File "builtin_stdlib.elpi", line 105, column 0, character 3277:
N1 is 
- N 1,
std.drop N1 XS L
std.drop N
[
_ | XS
]
L
-
File "builtin_stdlib.elpi", line 106, column 0, character 3326:
std.fatal-error drop run out of list items
std.drop _ _ _
-
File "builtin_stdlib.elpi", line 109, column 0, character 3425:
std.length L M,
I is 
- M N,
std.take I L R
std.drop-last N L R
-
File "builtin_stdlib.elpi", line 113, column 0, character 3534:
!
std.split-at 0 L [] L
-
File "builtin_stdlib.elpi", line 114, column 0, character 3558:
N1 is 
- N 1,
std.split-at N1 XS LN LM
std.split-at N
[
X | XS
]
[
X | LN
]
LM
-
File "builtin_stdlib.elpi", line 115, column 0, character 3627:
std.fatal-error split-at run out of list items
std.split-at _ _ _ _
-
File "builtin_stdlib.elpi", line 118, column 0, character 3749:
std.fold [] A _ A
-
File "builtin_stdlib.elpi", line 119, column 0, character 3764:
F X A A1,
std.fold XS A1 F R
std.fold
[
X | XS
]
A F R
-
File "builtin_stdlib.elpi", line 122, column 0, character 3873:
std.fold-right [] A _ A
-
File "builtin_stdlib.elpi", line 123, column 0, character 3894:
std.fold-right XS A F A',
F X A' R
std.fold-right
[
X | XS
]
A F R
-
File "builtin_stdlib.elpi", line 126, column 0, character 4025:
std.fatal-error fold2 on lists of different length
std.fold2 []
[
_ | _
]
_ _ _
-
File "builtin_stdlib.elpi", line 127, column 0, character 4099:
std.fatal-error fold2 on lists of different length
std.fold2
[
_ | _
]
[] _ _ _
-
File "builtin_stdlib.elpi", line 128, column 0, character 4173:
std.fold2 [] [] A _ A
-
File "builtin_stdlib.elpi", line 129, column 0, character 4192:
F X Y A A1,
std.fold2 XS YS A1 F R
std.fold2
[
X | XS
]
[
Y | YS
]
A F R
-
File "builtin_stdlib.elpi", line 132, column 0, character 4303:
std.map [] _ []
-
File "builtin_stdlib.elpi", line 133, column 0, character 4316:
F X Y,
std.map XS F YS
std.map
[
X | XS
]
F
[
Y | YS
]
-
File "builtin_stdlib.elpi", line 136, column 0, character 4418:
std.map-i.aux L 0 F R
std.map-i L F R
-
File "builtin_stdlib.elpi", line 137, column 0, character 4452:
std.map-i.aux [] _ _ []
-
File "builtin_stdlib.elpi", line 138, column 0, character 4473:
F N X Y,
M is 
N + 
1,
std.map-i.aux XS M F YS
std.map-i.aux
[
X | XS
]
N F
[
Y | YS
]
-
File "builtin_stdlib.elpi", line 141, column 0, character 4603:
std.map-filter [] _ []
-
File "builtin_stdlib.elpi", line 142, column 0, character 4623:
F X Y,
!,
std.map-filter XS F YS
std.map-filter
[
X | XS
]
F
[
Y | YS
]
-
File "builtin_stdlib.elpi", line 143, column 0, character 4683:
std.map-filter XS F YS
std.map-filter
[
_ | XS
]
F YS
-
File "builtin_stdlib.elpi", line 147, column 0, character 4807:
std.fatal-error map2 on lists of different length
std.map2 []
[
_ | _
]
_ _
-
File "builtin_stdlib.elpi", line 148, column 0, character 4877:
std.fatal-error map2 on lists of different length
std.map2
[
_ | _
]
[] _ _
-
File "builtin_stdlib.elpi", line 149, column 0, character 4947:
std.map2 [] [] _ []
-
File "builtin_stdlib.elpi", line 150, column 0, character 4964:
F X Y Z,
std.map2 XS YS F ZS
std.map2
[
X | XS
]
[
Y | YS
]
F
[
Z | ZS
]
-
File "builtin_stdlib.elpi", line 153, column 0, character 5094:
std.fatal-error map2-filter on lists of different length
std.map2-filter []
[
_ | _
]
_ _
-
File "builtin_stdlib.elpi", line 154, column 0, character 5178:
std.fatal-error map2-filter on lists of different length
std.map2-filter
[
_ | _
]
[] _ _
-
File "builtin_stdlib.elpi", line 155, column 0, character 5262:
std.map2-filter [] [] _ []
-
File "builtin_stdlib.elpi", line 156, column 0, character 5286:
F X Y Z,
!,
std.map2-filter XS YS F ZS
std.map2-filter
[
X | XS
]
[
Y | YS
]
F
[
Z | ZS
]
-
File "builtin_stdlib.elpi", line 157, column 0, character 5360:
std.map2-filter XS YS F ZS
std.map2-filter
[
_ | XS
]
[
_ | YS
]
F ZS
-
File "builtin_stdlib.elpi", line 160, column 0, character 5499:
P X Y S0,
if
(S0 = 
ok)
(std.map-ok L P YS S)
(S = 
S0)
std.map-ok
[
X | L
]
P
[
Y | YS
]
S
-
File "builtin_stdlib.elpi", line 161, column 0, character 5577:
std.map-ok [] _ [] ok
-
File "builtin_stdlib.elpi", line 164, column 0, character 5671:
std.fold-map [] A _ [] A
-
File "builtin_stdlib.elpi", line 165, column 0, character 5693:
F X A Y A1,
std.fold-map XS A1 F YS A2
std.fold-map
[
X | XS
]
A F
[
Y | YS
]
A2
-
File "builtin_stdlib.elpi", line 168, column 0, character 5817:
std.omap none _ none
-
File "builtin_stdlib.elpi", line 169, column 0, character 5835:
F X Y
std.omap (some X) F (some Y)
-
File "builtin_stdlib.elpi", line 173, column 0, character 5975:
X = 
R
std.nth 0
[
X | _
]
R
-
File "builtin_stdlib.elpi", line 174, column 0, character 6003:
> N 0,
!,
N1 is 
- N 1,
std.nth N1 XS R
std.nth N
[
_ | XS
]
R
-
File "builtin_stdlib.elpi", line 175, column 0, character 6057:
N < 
0,
!,
std.fatal-error nth got a negative index
std.nth N _ _
-
File "builtin_stdlib.elpi", line 176, column 0, character 6120:
std.fatal-error nth run out of list items
std.nth _ _ _
-
File "builtin_stdlib.elpi", line 180, column 0, character 6261:
std.lookup
[
pr X Y | _
]
X Y
-
File "builtin_stdlib.elpi", line 181, column 0, character 6284:
std.lookup LS X Y
std.lookup
[
_ | LS
]
X Y
-
File "builtin_stdlib.elpi", line 185, column 0, character 6443:
!
std.lookup!
[
pr X Y | _
]
X Y
-
File "builtin_stdlib.elpi", line 186, column 0, character 6472:
std.lookup! LS X Y
std.lookup!
[
_ | LS
]
X Y
-
File "builtin_stdlib.elpi", line 190, column 0, character 6591:
!
std.mem!
[
X | _
]
X
-
File "builtin_stdlib.elpi", line 191, column 0, character 6610:
std.mem! L X
std.mem!
[
_ | L
]
X
-
File "builtin_stdlib.elpi", line 195, column 0, character 6715:
std.mem
[
X | _
]
X
-
File "builtin_stdlib.elpi", line 196, column 0, character 6728:
std.mem L X
std.mem
[
_ | L
]
X
-
File "builtin_stdlib.elpi", line 199, column 0, character 6790:
P X
std.exists
[
X | _
]
P
-
File "builtin_stdlib.elpi", line 200, column 0, character 6813:
std.exists L P
std.exists
[
_ | L
]
P
-
File "builtin_stdlib.elpi", line 203, column 0, character 6897:
std.fatal-error exists2 on lists of different length
std.exists2 []
[
_ | _
]
_
-
File "builtin_stdlib.elpi", line 204, column 0, character 6971:
std.fatal-error exists2 on lists of different length
std.exists2
[
_ | _
]
[] _
-
File "builtin_stdlib.elpi", line 205, column 0, character 7045:
P X Y
std.exists2
[
X | _
]
[
Y | _
]
P
-
File "builtin_stdlib.elpi", line 206, column 0, character 7077:
std.exists2 L M P
std.exists2
[
_ | L
]
[
_ | M
]
P
-
File "builtin_stdlib.elpi", line 209, column 0, character 7155:
std.forall [] _
-
File "builtin_stdlib.elpi", line 210, column 0, character 7168:
P X,
std.forall L P
std.forall
[
X | L
]
P
-
File "builtin_stdlib.elpi", line 213, column 0, character 7272:
P X S0,
if
(S0 = 
ok)
(std.forall-ok L P S)
(S = 
S0)
std.forall-ok
[
X | L
]
P S
-
File "builtin_stdlib.elpi", line 214, column 0, character 7344:
std.forall-ok [] _ ok
-
File "builtin_stdlib.elpi", line 217, column 0, character 7417:
std.fatal-error forall2 on lists of different length
std.forall2 []
[
_ | _
]
_
-
File "builtin_stdlib.elpi", line 218, column 0, character 7491:
std.fatal-error forall2 on lists of different length
std.forall2
[
_ | _
]
[] _
-
File "builtin_stdlib.elpi", line 219, column 0, character 7565:
P X Y,
std.forall2 XS YS P
std.forall2
[
X | XS
]
[
Y | YS
]
P
-
File "builtin_stdlib.elpi", line 220, column 0, character 7616:
std.forall2 [] [] _
-
File "builtin_stdlib.elpi", line 223, column 0, character 7681:
std.filter [] _ []
-
File "builtin_stdlib.elpi", line 224, column 0, character 7700:
if (P X)
(R = 
[
X | L1
]
)
(R = 
L1),
std.filter L P L1
std.filter
[
X | L
]
P R
-
File "builtin_stdlib.elpi", line 227, column 0, character 7817:
std.fatal-error zip on lists of different length
std.zip
[
_ | _
]
[] _
-
File "builtin_stdlib.elpi", line 228, column 0, character 7883:
std.fatal-error zip on lists of different length
std.zip []
[
_ | _
]
_
-
File "builtin_stdlib.elpi", line 229, column 0, character 7949:
std.zip LX LY LR
std.zip
[
X | LX
]
[
Y | LY
]
[
pr X Y | LR
]
-
File "builtin_stdlib.elpi", line 230, column 0, character 7996:
std.zip [] [] []
-
File "builtin_stdlib.elpi", line 233, column 0, character 8061:
std.unzip [] [] []
-
File "builtin_stdlib.elpi", line 234, column 0, character 8077:
std.unzip L LX LY
std.unzip
[
pr X Y | L
]
[
X | LX
]
[
Y | LY
]
-
File "builtin_stdlib.elpi", line 237, column 0, character 8167:
std.flatten LS LS',
std.append X LS' R
std.flatten
[
X | LS
]
R
-
File "builtin_stdlib.elpi", line 238, column 0, character 8219:
std.flatten [] []
-
File "builtin_stdlib.elpi", line 241, column 0, character 8259:
std.null []
-
File "builtin_stdlib.elpi", line 244, column 0, character 8298:
std.iota.aux 0 N L
std.iota N L
-
File "builtin_stdlib.elpi", line 245, column 0, character 8326:
!
std.iota.aux X X []
-
File "builtin_stdlib.elpi", line 246, column 0, character 8348:
M is 
N + 
1,
std.iota.aux M X R
std.iota.aux N X
[
N | R
]
-
File "builtin_stdlib.elpi", line 251, column 0, character 8500:
std.intersperse _ [] []
-
File "builtin_stdlib.elpi", line 252, column 0, character 8521:
!
std.intersperse _
[
X
]
[
X
]
-
File "builtin_stdlib.elpi", line 253, column 0, character 8549:
std.intersperse Sep XS YS
std.intersperse Sep
[
X | XS
]
[
X,
Sep | YS
]
-
File "builtin_stdlib.elpi", line 258, column 0, character 8665:
P Y X
std.flip P X Y
-
File "builtin_stdlib.elpi", line 261, column 0, character 8714:
gettimeofday Before,
P,
gettimeofday After,
T is 
- After Before
std.time P T
-
File "builtin_stdlib.elpi", line 264, column 0, character 8814:
std.do! []
-
File "builtin_stdlib.elpi", line 265, column 0, character 8822:
P,
!,
std.do! PS
std.do!
[
P | PS
]
-
File "builtin_stdlib.elpi", line 269, column 0, character 8918:
std.do-ok! ok []
-
File "builtin_stdlib.elpi", line 270, column 0, character 8932:
P S0,
!,
if
(S0 = 
ok)
(std.do-ok! S PS)
(S = 
S0)
std.do-ok! S
[
P | PS
]
-
File "builtin_stdlib.elpi", line 273, column 0, character 9043:
(P,
R = 
ok ; 
R = 
(error Msg))
std.lift-ok P Msg R
-
File "builtin_stdlib.elpi", line 276, column 0, character 9117:
std.map L
λx1.
λx2.
x2 = 
(std.spy x1)
L1,
std.do! L1
std.spy-do! L
-
File "builtin_stdlib.elpi", line 279, column 0, character 9240:
std.while-ok-do!
(error _ as 
E)
_ E
-
File "builtin_stdlib.elpi", line 280, column 0, character 9273:
std.while-ok-do! ok [] ok
-
File "builtin_stdlib.elpi", line 281, column 0, character 9296:
P C,
!,
std.while-ok-do! C PS R
std.while-ok-do! ok
[
P | PS
]
R
-
File "builtin_stdlib.elpi", line 284, column 0, character 9386:
term_to_string X Y
std.any->string X Y
-
File "builtin_stdlib.elpi", line 287, column 0, character 9450:
>= N M,
!
std.max N M N
-
File "builtin_stdlib.elpi", line 288, column 0, character 9474:
std.max _ M M
-
File "builtin_stdlib.elpi", line 292, column 0, character 9597:
findall_solutions P L
std.findall P L
-
File "builtin_map.elpi", line 7, column 0, character 10158:
std.map.make Cmp (std.map std.map.private.empty Cmp)
-
File "builtin_map.elpi", line 11, column 0, character 10290:
std.map.private.find M Cmp K V
std.map.find K (std.map M Cmp) V
-
File "builtin_map.elpi", line 15, column 0, character 10439:
std.map.private.add M Cmp K V M1
std.map.add K V (std.map M Cmp) (std.map M1 Cmp)
-
File "builtin_map.elpi", line 19, column 0, character 10602:
std.map.private.remove M Cmp K M1
std.map.remove K (std.map M Cmp) (std.map M1 Cmp)
-
File "builtin_map.elpi", line 23, column 0, character 10785:
std.map.private.bindings M [] L
std.map.bindings (std.map M _) L
-
File "builtin_map.elpi", line 33, column 0, character 11028:
std.map.private.height std.map.private.empty 0
-
File "builtin_map.elpi", line 34, column 0, character 11044:
std.map.private.height (std.map.private.node _ _ _ _ H) H
-
File "builtin_map.elpi", line 37, column 0, character 11127:
std.map.private.height L Spilled1,
std.map.private.height R Spilled2,
std.max Spilled1 Spilled2 Spilled3,
H is 
Spilled3 + 
1
std.map.private.create L K V R (std.map.private.node L K V R H)
-
File "builtin_map.elpi", line 40, column 0, character 11257:
std.map.private.height L HL,
std.map.private.height R HR,
HL2 is 
HL + 
2,
HR2 is 
HR + 
2,
std.map.private.bal.aux HL HR HL2 HR2 L K V R T
std.map.private.bal L K V R T
-
File "builtin_map.elpi", line 47, column 0, character 11374:
> HL HR2,
std.map.private.height LL Spilled2,
std.map.private.height LR Spilled3,
>= Spilled2 Spilled3,
!,
std.map.private.create LR X D R Spilled1,
std.map.private.create LL LV LD Spilled1 T
std.map.private.bal.aux HL _ _ HR2 (std.map.private.node LL LV LD LR _) X D R T
-
File "builtin_map.elpi", line 50, column 0, character 11507:
> HL HR2,
!,
std.map.private.create LL LV LD LRL Spilled1,
std.map.private.create LRR X D R Spilled2,
std.map.private.create Spilled1 LRV LRD Spilled2 T
std.map.private.bal.aux HL _ _ HR2 (std.map.private.node LL LV LD (std.map.private.node LRL LRV LRD LRR _) _) X D R T
-
File "builtin_map.elpi", line 53, column 0, character 11656:
> HR HL2,
std.map.private.height RR Spilled2,
std.map.private.height RL Spilled3,
>= Spilled2 Spilled3,
!,
std.map.private.create L X D RL Spilled1,
std.map.private.create Spilled1 RV RD RR T
std.map.private.bal.aux _ HR HL2 _ L X D (std.map.private.node RL RV RD RR _) T
-
File "builtin_map.elpi", line 56, column 0, character 11789:
> HR HL2,
!,
std.map.private.create L X D RLL Spilled1,
std.map.private.create RLR RV RD RR Spilled2,
std.map.private.create Spilled1 RLV RLD Spilled2 T
std.map.private.bal.aux _ HR HL2 _ L X D (std.map.private.node (std.map.private.node RLL RLV RLD RLR _) RV RD RR _) T
-
File "builtin_map.elpi", line 59, column 0, character 11938:
std.map.private.create L K V R T
std.map.private.bal.aux _ _ _ _ L K V R T
-
File "builtin_map.elpi", line 62, column 0, character 12054:
std.map.private.create std.map.private.empty K V std.map.private.empty T
std.map.private.add std.map.private.empty _ K V T
-
File "builtin_map.elpi", line 63, column 0, character 12101:
Cmp X1 X E,
std.map.private.add.aux E M Cmp X1 XD M1
std.map.private.add
(std.map.private.node _ X _ _ _ as 
M)
Cmp X1 XD M1
-
File "builtin_map.elpi", line 64, column 0, character 12181:
T = 
(std.map.private.node L X XD R H)
std.map.private.add.aux eq (std.map.private.node L _ _ R H) _ X XD T
-
File "builtin_map.elpi", line 65, column 0, character 12245:
std.map.private.add L Cmp X XD Spilled1,
std.map.private.bal Spilled1 V D R T
std.map.private.add.aux lt (std.map.private.node L V D R _) Cmp X XD T
-
File "builtin_map.elpi", line 66, column 0, character 12317:
std.map.private.add R Cmp X XD Spilled1,
std.map.private.bal L V D Spilled1 T
std.map.private.add.aux gt (std.map.private.node L V D R _) Cmp X XD T
-
File "builtin_map.elpi", line 69, column 0, character 12448:
Cmp K K1 E,
std.map.private.find.aux E Cmp L R V1 K V
std.map.private.find (std.map.private.node L K1 V1 R _) Cmp K V
-
File "builtin_map.elpi", line 70, column 0, character 12522:
std.map.private.find.aux eq _ _ _ V _ V
-
File "builtin_map.elpi", line 71, column 0, character 12549:
std.map.private.find L Cmp K V
std.map.private.find.aux lt Cmp L _ _ K V
-
File "builtin_map.elpi", line 72, column 0, character 12594:
std.map.private.find R Cmp K V
std.map.private.find.aux gt Cmp _ R _ K V
-
File "builtin_map.elpi", line 75, column 0, character 12686:
!
std.map.private.remove-min-binding (std.map.private.node std.map.private.empty _ _ R _) R
-
File "builtin_map.elpi", line 76, column 0, character 12734:
std.map.private.remove-min-binding L Spilled1,
std.map.private.bal Spilled1 V D R X
std.map.private.remove-min-binding (std.map.private.node L V D R _) X
-
File "builtin_map.elpi", line 79, column 0, character 12850:
!
std.map.private.min-binding (std.map.private.node std.map.private.empty V D _ _) V D
-
File "builtin_map.elpi", line 80, column 0, character 12893:
std.map.private.min-binding L V D
std.map.private.min-binding (std.map.private.node L _ _ _ _) V D
-
File "builtin_map.elpi", line 83, column 0, character 12993:
!
std.map.private.merge std.map.private.empty X X
-
File "builtin_map.elpi", line 84, column 0, character 13015:
!
std.map.private.merge X std.map.private.empty X
-
File "builtin_map.elpi", line 85, column 0, character 13037:
std.map.private.min-binding M2 X D,
std.map.private.remove-min-binding M2 Spilled1,
std.map.private.bal M1 X D Spilled1 R
std.map.private.merge M1 M2 R
-
File "builtin_map.elpi", line 90, column 0, character 13183:
!
std.map.private.remove std.map.private.empty _ _ std.map.private.empty
-
File "builtin_map.elpi", line 91, column 0, character 13212:
Cmp X V E,
std.map.private.remove.aux E Cmp L R V D X M
std.map.private.remove (std.map.private.node L V D R _) Cmp X M
-
File "builtin_map.elpi", line 92, column 0, character 13288:
std.map.private.merge L R M
std.map.private.remove.aux eq _ L R _ _ _ M
-
File "builtin_map.elpi", line 93, column 0, character 13334:
std.map.private.remove L Cmp X Spilled1,
std.map.private.bal Spilled1 V D R M
std.map.private.remove.aux lt Cmp L R V D X M
-
File "builtin_map.elpi", line 94, column 0, character 13397:
std.map.private.remove R Cmp X Spilled1,
std.map.private.bal L V D Spilled1 M
std.map.private.remove.aux gt Cmp L R V D X M
-
File "builtin_map.elpi", line 97, column 0, character 13524:
std.map.private.bindings std.map.private.empty X X
-
File "builtin_map.elpi", line 98, column 0, character 13544:
std.map.private.bindings R X Spilled1,
std.map.private.bindings L
[
pr V D | Spilled1
]
X1
std.map.private.bindings (std.map.private.node L V D R _) X X1
-
File "builtin_set.elpi", line 7, column 0, character 22315:
std.set.make Cmp (std.set std.set.private.empty Cmp)
-
File "builtin_set.elpi", line 11, column 0, character 22412:
std.set.private.mem M Cmp E
std.set.mem E (std.set M Cmp)
-
File "builtin_set.elpi", line 15, column 0, character 22527:
std.set.private.add M Cmp E M1
std.set.add E (std.set M Cmp) (std.set M1 Cmp)
-
File "builtin_set.elpi", line 19, column 0, character 22669:
std.set.private.remove M Cmp E M1
std.set.remove E (std.set M Cmp) (std.set M1 Cmp)
-
File "builtin_set.elpi", line 23, column 0, character 22826:
std.set.private.cardinal M N
std.set.cardinal (std.set M _) N
-
File "builtin_set.elpi", line 26, column 0, character 22914:
std.set.private.elements M [] L
std.set.elements (std.set M _) L
-
File "builtin_set.elpi", line 36, column 0, character 23134:
std.set.private.height std.set.private.empty 0
-
File "builtin_set.elpi", line 37, column 0, character 23150:
std.set.private.height (std.set.private.node _ _ _ H) H
-
File "builtin_set.elpi", line 40, column 0, character 23220:
std.set.private.height L Spilled1,
std.set.private.height R Spilled2,
std.max Spilled1 Spilled2 Spilled3,
H is 
Spilled3 + 
1
std.set.private.create L E R (std.set.private.node L E R H)
-
File "builtin_set.elpi", line 43, column 0, character 23335:
std.set.private.height L HL,
std.set.private.height R HR,
HL2 is 
HL + 
2,
HR2 is 
HR + 
2,
std.set.private.bal.aux HL HR HL2 HR2 L E R T
std.set.private.bal L E R T
-
File "builtin_set.elpi", line 50, column 0, character 23448:
> HL HR2,
std.set.private.height LL Spilled2,
std.set.private.height LR Spilled3,
>= Spilled2 Spilled3,
!,
std.set.private.create LR X R Spilled1,
std.set.private.create LL LV Spilled1 T
std.set.private.bal.aux HL _ _ HR2 (std.set.private.node LL LV LR _) X R T
-
File "builtin_set.elpi", line 53, column 0, character 23571:
> HL HR2,
!,
std.set.private.create LL LV LRL Spilled1,
std.set.private.create LRR X R Spilled2,
std.set.private.create Spilled1 LRV Spilled2 T
std.set.private.bal.aux HL _ _ HR2 (std.set.private.node LL LV (std.set.private.node LRL LRV LRR _) _) X R T
-
File "builtin_set.elpi", line 56, column 0, character 23702:
> HR HL2,
std.set.private.height RR Spilled2,
std.set.private.height RL Spilled3,
>= Spilled2 Spilled3,
!,
std.set.private.create L X RL Spilled1,
std.set.private.create Spilled1 RV RR T
std.set.private.bal.aux _ HR HL2 _ L X (std.set.private.node RL RV RR _) T
-
File "builtin_set.elpi", line 59, column 0, character 23825:
> HR HL2,
!,
std.set.private.create L X RLL Spilled1,
std.set.private.create RLR RV RR Spilled2,
std.set.private.create Spilled1 RLV Spilled2 T
std.set.private.bal.aux _ HR HL2 _ L X (std.set.private.node (std.set.private.node RLL RLV RLR _) RV RR _) T
-
File "builtin_set.elpi", line 62, column 0, character 23956:
std.set.private.create L E R T
std.set.private.bal.aux _ _ _ _ L E R T
-
File "builtin_set.elpi", line 65, column 0, character 24059:
std.set.private.create std.set.private.empty E std.set.private.empty T
std.set.private.add std.set.private.empty _ E T
-
File "builtin_set.elpi", line 66, column 0, character 24102:
Cmp X1 X E,
std.set.private.add.aux E Cmp L R X X1 H S
std.set.private.add (std.set.private.node L X R H) Cmp X1 S
-
File "builtin_set.elpi", line 67, column 0, character 24173:
std.set.private.add.aux eq _ L R X _ H (std.set.private.node L X R H)
-
File "builtin_set.elpi", line 68, column 0, character 24212:
std.set.private.add L Cmp X Spilled1,
std.set.private.bal Spilled1 E R T
std.set.private.add.aux lt Cmp L R E X _ T
-
File "builtin_set.elpi", line 69, column 0, character 24267:
std.set.private.add R Cmp X Spilled1,
std.set.private.bal L E Spilled1 T
std.set.private.add.aux gt Cmp L R E X _ T
-
File "builtin_set.elpi", line 72, column 0, character 24373:
Cmp E K O,
std.set.private.mem.aux O Cmp L R E
std.set.private.mem (std.set.private.node L K R _) Cmp E
-
File "builtin_set.elpi", line 73, column 0, character 24433:
std.set.private.mem.aux eq _ _ _ _
-
File "builtin_set.elpi", line 74, column 0, character 24453:
std.set.private.mem L Cmp E
std.set.private.mem.aux lt Cmp L _ E
-
File "builtin_set.elpi", line 75, column 0, character 24490:
std.set.private.mem R Cmp E
std.set.private.mem.aux gt Cmp _ R E
-
File "builtin_set.elpi", line 78, column 0, character 24570:
!
std.set.private.remove-min-binding (std.set.private.node std.set.private.empty _ R _) R
-
File "builtin_set.elpi", line 79, column 0, character 24616:
std.set.private.remove-min-binding L Spilled1,
std.set.private.bal Spilled1 E R X
std.set.private.remove-min-binding (std.set.private.node L E R _) X
-
File "builtin_set.elpi", line 82, column 0, character 24721:
!
std.set.private.min-binding (std.set.private.node std.set.private.empty E _ _) E
-
File "builtin_set.elpi", line 83, column 0, character 24760:
std.set.private.min-binding L E
std.set.private.min-binding (std.set.private.node L _ _ _) E
-
File "builtin_set.elpi", line 86, column 0, character 24848:
!
std.set.private.merge std.set.private.empty X X
-
File "builtin_set.elpi", line 87, column 0, character 24870:
!
std.set.private.merge X std.set.private.empty X
-
File "builtin_set.elpi", line 88, column 0, character 24892:
std.set.private.min-binding M2 X,
std.set.private.remove-min-binding M2 Spilled1,
std.set.private.bal M1 X Spilled1 R
std.set.private.merge M1 M2 R
-
File "builtin_set.elpi", line 93, column 0, character 25030:
std.set.private.remove std.set.private.empty _ _ std.set.private.empty
-
File "builtin_set.elpi", line 94, column 0, character 25054:
Cmp X E O,
std.set.private.remove.aux O Cmp L R E X M
std.set.private.remove (std.set.private.node L E R _) Cmp X M
-
File "builtin_set.elpi", line 95, column 0, character 25126:
std.set.private.merge L R M
std.set.private.remove.aux eq _ L R _ _ M
-
File "builtin_set.elpi", line 96, column 0, character 25170:
std.set.private.remove L Cmp X Spilled1,
std.set.private.bal Spilled1 E R M
std.set.private.remove.aux lt Cmp L R E X M
-
File "builtin_set.elpi", line 97, column 0, character 25229:
std.set.private.remove R Cmp X Spilled1,
std.set.private.bal L E Spilled1 M
std.set.private.remove.aux gt Cmp L R E X M
-
File "builtin_set.elpi", line 100, column 0, character 25319:
std.set.private.cardinal std.set.private.empty 0
-
File "builtin_set.elpi", line 101, column 0, character 25337:
std.set.private.cardinal L Spilled1,
std.set.private.cardinal R Spilled2,
N is 
Spilled1 + 
1 + 
Spilled2
std.set.private.cardinal (std.set.private.node L _ R _) N
-
File "builtin_set.elpi", line 104, column 0, character 25448:
std.set.private.elements std.set.private.empty X X
-
File "builtin_set.elpi", line 105, column 0, character 25468:
std.set.private.elements R Acc Spilled1,
std.set.private.elements L
[
E | Spilled1
]
X
std.set.private.elements (std.set.private.node L E R _) Acc X
-
File "builtin_set.elpi", line 255, column 0, character 30599:
term_to_string T T1,
output S T1
printterm S T
-
File "builtin_set.elpi", line 259, column 0, character 30667:
flush std_out,
input_line std_in X,
string_to_term X S
read S
-
File "coq-builtin.elpi: default-declare-evar", line 268, column 0, character 10807:
declare_constraint (declare-evar Ctx RawEv Ty Ev)
[
RawEv
]
declare-evar Ctx RawEv Ty Ev
-
File "coq-builtin.elpi", line 277, column 0, character 11167:
declare_constraint (rm-evar X Y)
[
X,
Y
]
rm-evar
(uvar as 
X)
(uvar as 
Y)
-
File "coq-builtin.elpi", line 278, column 0, character 11244:
rm-evar _ _
-
File "coq-builtin.elpi", line 299, column 0, character 12024:
var S _ VL,
!,
prune T VL,
prune X VL,
declare_constraint (evar X T S)
[
X,
S
]
evar
(uvar as 
X)
T S
-
File "coq-builtin.elpi: default-assign-evar", line 302, column 0, character 12130:
evar _ _ _
-
File "coq-builtin.elpi", line 750, column 3, character 30772:
coq.warning elpi.deprecated elpi.const-opaque use coq.env.opaque? in place of coq.env.const-opaque?,
coq.env.opaque? C
coq.env.const-opaque? C
-
File "coq-builtin.elpi", line 757, column 3, character 31020:
coq.warning elpi.deprecated elpi.const-primitive use coq.env.primitive? in place of coq.env.const-primitive?,
coq.env.primitive? C
coq.env.const-primitive? C
-
File "coq-builtin.elpi", line 839, column 0, character 34362:
coq.env.begin-module-functor Name MP []
coq.env.begin-module Name MP
-
File "coq-builtin.elpi", line 852, column 0, character 34843:
coq.env.begin-module-type-functor Name []
coq.env.begin-module-type Name
-
File "coq-builtin.elpi", line 1231, column 0, character 49739:
coq.warning elpi.deprecated elpi.canonical-projections use coq.env.projections in place of coq.CS.canonical-projections,
coq.env.projections I L
coq.CS.canonical-projections I L
-
File "coq-builtin.elpi", line 1535, column 0, character 62545:
coq.warning elpi.deprecated elpi.cbv-whd-all use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all,
coq.reduction.cbv.norm T R
coq.reduction.cbv.whd_all T R
-
File "coq-builtin.elpi", line 1542, column 0, character 62823:
coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all,
coq.reduction.vm.norm T TY R
coq.reduction.vm.whd_all T TY R
-
File "coq-builtin.elpi", line 1549, column 0, character 63057:
get-option coq:redflags coq.redflags.all ⇒ 
coq.reduction.lazy.whd X Y
coq.reduction.lazy.whd_all X Y
-
File "coq-builtin.elpi", line 1666, column 0, character 67568:
coq.string->name S N
coq.id->name S N
-
File "coq-builtin.elpi", line 1768, column 0, character 71342:
coq.elpi.accumulate-clauses S N
[
C
]
coq.elpi.accumulate S N C
-
File "./examples/tutorial_elpi_lang.v", line 491, column 3, character 12653:
whd Hd (fun F),
!,
whd (F Arg) Reduct
whd (app Hd Arg) Reduct
-
File "./examples/tutorial_elpi_lang.v", line 495, column 3, character 12776:
Reduct = 
X
whd X Reduct
-
File "./examples/tutorial_elpi_lang.v", line 591, column 3, character 15201:
of Hd (arr A B),
of Arg A
of (app Hd Arg) B
-
File "./examples/tutorial_elpi_lang.v", line 596, column 3, character 15366:
∀x1.
of x1 A ⇒ 
of (F x1) B
of (fun F) (arr A B)
- \ No newline at end of file diff --git a/stlc.txt b/stlc.txt new file mode 100644 index 000000000..f0dd03ede --- /dev/null +++ b/stlc.txt @@ -0,0 +1,669 @@ +% File "elpi-builtin.elpi", line 11, column 0, characters 147-151: [1] +true :- . +% File "elpi-builtin.elpi", line 34, column 0, characters 373-385: [2] +A0 ; _ :- A0. +% File "elpi-builtin.elpi", line 36, column 0, characters 388-400: [3] +_ ; A0 :- A0. +% File "elpi-builtin.elpi", line 62, column 0, characters 759-778: [4] +not A0 :- A0, !, fail. +% File "elpi-builtin.elpi", line 64, column 0, characters 781-786: [5] +not _ :- . +% File "elpi-builtin.elpi", line 77, column 0, characters 1124-1136: [6] +stop :- halt. +% File "elpi-builtin.elpi", line 83, column 0, characters 1181-1199: [7] +A1 is A0 :- calc A0 A1. +% File "elpi-builtin.elpi", line 182, column 0, characters 2993-3009: [8] +A0 > A1 :- gt_ A0 A1. +% File "elpi-builtin.elpi", line 185, column 0, characters 3031-3047: [9] +A0 < A1 :- lt_ A0 A1. +% File "elpi-builtin.elpi", line 188, column 0, characters 3070-3087: [10] +A0 =< A1 :- le_ A0 A1. +% File "elpi-builtin.elpi", line 191, column 0, characters 3110-3127: [11] +A0 >= A1 :- ge_ A0 A1. +% File "elpi-builtin.elpi", line 194, column 0, characters 3154-3171: [12] +A0 i> A1 :- gt_ A0 A1. +% File "elpi-builtin.elpi", line 197, column 0, characters 3198-3215: [13] +A0 i< A1 :- lt_ A0 A1. +% File "elpi-builtin.elpi", line 200, column 0, characters 3243-3261: [14] +A0 i=< A1 :- le_ A0 A1. +% File "elpi-builtin.elpi", line 203, column 0, characters 3289-3307: [15] +A0 i>= A1 :- ge_ A0 A1. +% File "elpi-builtin.elpi", line 206, column 0, characters 3338-3355: [16] +A0 r> A1 :- gt_ A0 A1. +% File "elpi-builtin.elpi", line 209, column 0, characters 3386-3403: [17] +A0 r< A1 :- lt_ A0 A1. +% File "elpi-builtin.elpi", line 212, column 0, characters 3435-3453: [18] +A0 r=< A1 :- le_ A0 A1. +% File "elpi-builtin.elpi", line 215, column 0, characters 3485-3503: [19] +A0 r>= A1 :- ge_ A0 A1. +% File "elpi-builtin.elpi", line 218, column 0, characters 3536-3553: [20] +A0 s> A1 :- gt_ A0 A1. +% File "elpi-builtin.elpi", line 221, column 0, characters 3586-3603: [21] +A0 s< A1 :- lt_ A0 A1. +% File "elpi-builtin.elpi", line 224, column 0, characters 3637-3655: [22] +A0 s=< A1 :- le_ A0 A1. +% File "elpi-builtin.elpi", line 227, column 0, characters 3689-3707: [23] +A0 s>= A1 :- ge_ A0 A1. +% File "elpi-builtin.elpi", line 248, column 0, characters 4099-4113: [24] +fst (pr A0 _) A0 :- . +% File "elpi-builtin.elpi", line 252, column 0, characters 4144-4158: [25] +snd (pr _ A0) A0 :- . +% File "elpi-builtin.elpi", line 259, column 0, characters 4281-4306: [26] +triple_1 (triple A0 _ _) A0 :- . +% File "elpi-builtin.elpi", line 262, column 0, characters 4344-4369: [27] +triple_2 (triple _ A0 _) A0 :- . +% File "elpi-builtin.elpi", line 265, column 0, characters 4407-4432: [28] +triple_3 (triple _ _ A0) A0 :- . +% File "elpi-builtin.elpi", line 295, column 0, characters 5059-5091: [29] +counter A0 A1 :- trace.counter A0 A1. +% File "elpi-builtin.elpi", line 321, column 0, characters 5969-6001: [30] +rex_match A0 A1 :- rex.match A0 A1. +% File "elpi-builtin.elpi", line 325, column 0, characters 6091-6135: [31] +rex_replace A0 A1 A2 A3 :- rex.replace A0 A1 A2 A3. +% File "elpi-builtin.elpi", line 329, column 0, characters 6216-6252: [32] +rex_split A0 A1 A2 :- rex.split A0 A1 A2. +% File "elpi-builtin.elpi", line 359, column 0, characters 7377-7400: [33] +A0 == A1 :- same_term A0 A1. +% File "elpi-builtin.elpi", line 392, column 0, characters 8555-8585: [34] +primitive? A0 A1 :- is_cdata A0 A1. +% File "elpi-builtin.elpi", line 422, column 0, characters 9560-9579: [35] +if A0 A1 _ :- A0, !, A1. +% File "elpi-builtin.elpi", line 423, column 0, characters 9581-9594: [36] +if _ _ A0 :- A0. +% File "elpi-builtin.elpi", line 427, column 0, characters 9724-9754: [37] +if2 A0 A1 _ _ _ :- A0, !, A1. +% File "elpi-builtin.elpi", line 428, column 0, characters 9756-9786: [38] +if2 _ _ A0 A1 _ :- A0, !, A1. +% File "elpi-builtin.elpi", line 429, column 0, characters 9788-9813: [39] +if2 _ _ _ _ A0 :- !, A0. +% File "builtin_stdlib.elpi", line 17, column 0, characters 659-714: [40] default-fatal-error +std.fatal-error A0 :- halt A0. +% File "builtin_stdlib.elpi", line 21, column 0, characters 756-839: [41] default-fatal-error-w-data +std.fatal-error-w-data A0 A1 :- halt A0 : A1. +% File "builtin_stdlib.elpi", line 25, column 0, characters 874-940: [42] default-debug-print +std.debug-print A0 A1 :- print A0 A1. +% File "builtin_stdlib.elpi", line 31, column 0, characters 1007-1032: [43] +std.ignore-failure! A0 :- A0, !. +% File "builtin_stdlib.elpi", line 32, column 0, characters 1034-1051: [44] +std.ignore-failure! _ :- . +% File "builtin_stdlib.elpi", line 35, column 0, characters 1072-1086: [45] +std.once A0 :- A0, !. +% File "builtin_stdlib.elpi", line 39, column 0, characters 1190-1249: [46] +std.assert! A0 A1 :- A0 ; std.fatal-error-w-data A1 A0, !. +% File "builtin_stdlib.elpi", line 44, column 0, characters 1440-1552: [47] +std.assert-ok! A1 A3 :- A1 A0, !, + A0 = ok ; A0 = error A2 , std.fatal-error-w-data A3 A2, !. +% File "builtin_stdlib.elpi", line 45, column 0, characters 1554-1621: [48] +std.assert-ok! _ A0 :- std.fatal-error-w-data A0 no diagnostic returned. +% File "builtin_stdlib.elpi", line 49, column 0, characters 1716-1895: [49] +std.spy A1 :- trace.counter run A0, + if (not (A0 = 0)) (std.debug-print run= A0) true, + std.debug-print ----<<---- enter: A1, A1, + std.debug-print ---->>---- exit: A1. +% File "builtin_stdlib.elpi", line 53, column 0, characters 1897-1945: [50] +std.spy A0 :- std.debug-print ---->>---- fail: A0, fail. +% File "builtin_stdlib.elpi", line 57, column 0, characters 2035-2218: [51] +std.spy! A1 :- trace.counter run A0, + if (not (A0 = 0)) (std.debug-print run= A0) true, + std.debug-print ----<<---- enter: A1, A1, + std.debug-print ---->>---- exit: A1, !. +% File "builtin_stdlib.elpi", line 61, column 0, characters 2220-2269: [52] +std.spy! A0 :- std.debug-print ---->>---- fail: A0, fail. +% File "builtin_stdlib.elpi", line 65, column 0, characters 2329-2353: [53] +std.unsafe-cast A0 A0 :- . +% File "builtin_stdlib.elpi", line 70, column 0, characters 2410-2452: [54] +std.length [_ | A0] A2 :- std.length A0 A1, A2 is A1 + 1. +% File "builtin_stdlib.elpi", line 71, column 0, characters 2454-2468: [55] +std.length [] 0 :- . +% File "builtin_stdlib.elpi", line 74, column 0, characters 2500-2529: [56] +std.rev A0 A1 :- std.rev.aux A0 [] A1. +% File "builtin_stdlib.elpi", line 77, column 0, characters 2575-2619: [57] +std.rev.aux [A1 | A0] A2 A3 :- std.rev.aux A0 [A1 | A2] A3. +% File "builtin_stdlib.elpi", line 78, column 0, characters 2621-2635: [58] +std.rev.aux [] A0 A0 :- . +% File "builtin_stdlib.elpi", line 81, column 0, characters 2663-2708: [59] +std.last [] _ :- std.fatal-error last on empty list. +% File "builtin_stdlib.elpi", line 82, column 0, characters 2710-2725: [60] +std.last [A0] A0 :- !. +% File "builtin_stdlib.elpi", line 83, column 0, characters 2727-2753: [61] +std.last [_ | A0] A1 :- std.last A0 A1. +% File "builtin_stdlib.elpi", line 86, column 0, characters 2798-2838: [62] +std.append [A3 | A0] A1 [A3 | A2] :- std.append A0 A1 A2. +% File "builtin_stdlib.elpi", line 87, column 0, characters 2841-2854: [63] +std.append [] A0 A0 :- . +% File "builtin_stdlib.elpi", line 90, column 0, characters 2901-2915: [64] +std.appendR [] A0 A0 :- . +% File "builtin_stdlib.elpi", line 91, column 0, characters 2917-2959: [65] +std.appendR [A3 | A0] A1 [A3 | A2] :- std.appendR A0 A1 A2. +% File "builtin_stdlib.elpi", line 94, column 0, characters 2999-3015: [66] +std.take 0 _ [] :- !. +% File "builtin_stdlib.elpi", line 95, column 0, characters 3017-3068: [67] +std.take A1 [A4 | A2] [A4 | A3] :- !, A0 is A1 - 1, std.take A0 A2 A3. +% File "builtin_stdlib.elpi", line 96, column 0, characters 3070-3124: [68] +std.take _ _ _ :- std.fatal-error take run out of list items. +% File "builtin_stdlib.elpi", line 99, column 0, characters 3169-3228: [69] +std.take-last A3 A0 A4 :- std.length A0 A1, A2 is A1 - A3, std.drop A2 A0 A4. +% File "builtin_stdlib.elpi", line 105, column 0, characters 3268-3283: [70] +std.drop 0 A0 A0 :- !. +% File "builtin_stdlib.elpi", line 106, column 0, characters 3285-3332: [71] +std.drop A1 [_ | A2] A3 :- !, A0 is A1 - 1, std.drop A0 A2 A3. +% File "builtin_stdlib.elpi", line 107, column 0, characters 3334-3388: [72] +std.drop _ _ _ :- std.fatal-error drop run out of list items. +% File "builtin_stdlib.elpi", line 110, column 0, characters 3433-3488: [73] +std.drop-last A3 A0 A4 :- std.length A0 A1, A2 is A1 - A3, std.take A2 A0 A4. +% File "builtin_stdlib.elpi", line 114, column 0, characters 3542-3564: [74] +std.split-at 0 A0 [] A0 :- !. +% File "builtin_stdlib.elpi", line 115, column 0, characters 3566-3633: [75] +std.split-at A1 [A5 | A2] [A5 | A3] A4 :- !, A0 is A1 - 1, + std.split-at A0 A2 A3 A4. +% File "builtin_stdlib.elpi", line 116, column 0, characters 3635-3699: [76] +std.split-at _ _ _ _ :- std.fatal-error split-at run out of list items. +% File "builtin_stdlib.elpi", line 119, column 0, characters 3756-3769: [77] +std.fold [] A0 _ A0 :- . +% File "builtin_stdlib.elpi", line 120, column 0, characters 3771-3816: [78] +std.fold [A0 | A4] A1 A3 A5 :- A3 A0 A1 A2, std.fold A4 A2 A3 A5. +% File "builtin_stdlib.elpi", line 123, column 0, characters 3879-3898: [79] +std.fold-right [] A0 _ A0 :- . +% File "builtin_stdlib.elpi", line 124, column 0, characters 3900-3957: [80] +std.fold-right [A4 | A0] A1 A2 A5 :- std.fold-right A0 A1 A2 A3, A2 A4 A3 A5. +% File "builtin_stdlib.elpi", line 127, column 0, characters 4030-4102: [81] +std.fold2 [] [_ | _] _ _ _ :- std.fatal-error + fold2 on lists of different length. +% File "builtin_stdlib.elpi", line 128, column 0, characters 4104-4176: [82] +std.fold2 [_ | _] [] _ _ _ :- std.fatal-error + fold2 on lists of different length. +% File "builtin_stdlib.elpi", line 129, column 0, characters 4178-4195: [83] +std.fold2 [] [] A0 _ A0 :- . +% File "builtin_stdlib.elpi", line 130, column 0, characters 4197-4256: [84] +std.fold2 [A0 | A5] [A1 | A6] A2 A4 A7 :- A4 A0 A1 A2 A3, + std.fold2 A5 A6 A3 A4 A7. +% File "builtin_stdlib.elpi", line 133, column 0, characters 4307-4318: [85] +std.map [] _ [] :- . +% File "builtin_stdlib.elpi", line 134, column 0, characters 4320-4361: [86] +std.map [A0 | A3] A2 [A1 | A4] :- A2 A0 A1, std.map A3 A2 A4. +% File "builtin_stdlib.elpi", line 137, column 0, characters 4421-4453: [87] +std.map-i A0 A1 A2 :- std.map-i.aux A0 0 A1 A2. +% File "builtin_stdlib.elpi", line 140, column 0, characters 4524-4543: [88] +std.map-i.aux [] _ _ [] :- . +% File "builtin_stdlib.elpi", line 141, column 0, characters 4545-4616: [89] +std.map-i.aux [A1 | A5] A0 A3 [A2 | A6] :- A3 A0 A1 A2, A4 is A0 + 1, + std.map-i.aux A5 A4 A3 A6. +% File "builtin_stdlib.elpi", line 144, column 0, characters 4674-4692: [90] +std.map-filter [] _ [] :- . +% File "builtin_stdlib.elpi", line 145, column 0, characters 4694-4752: [91] +std.map-filter [A0 | A3] A2 [A1 | A4] :- A2 A0 A1, !, + std.map-filter A3 A2 A4. +% File "builtin_stdlib.elpi", line 146, column 0, characters 4754-4798: [92] +std.map-filter [_ | A0] A1 A2 :- std.map-filter A0 A1 A2. +% File "builtin_stdlib.elpi", line 150, column 0, characters 4877-4945: [93] +std.map2 [] [_ | _] _ _ :- std.fatal-error map2 on lists of different length. +% File "builtin_stdlib.elpi", line 151, column 0, characters 4947-5015: [94] +std.map2 [_ | _] [] _ _ :- std.fatal-error map2 on lists of different length. +% File "builtin_stdlib.elpi", line 152, column 0, characters 5017-5032: [95] +std.map2 [] [] _ [] :- . +% File "builtin_stdlib.elpi", line 153, column 0, characters 5034-5089: [96] +std.map2 [A0 | A4] [A1 | A5] A3 [A2 | A6] :- A3 A0 A1 A2, + std.map2 A4 A5 A3 A6. +% File "builtin_stdlib.elpi", line 156, column 0, characters 5163-5245: [97] +std.map2-filter [] [_ | _] _ _ :- std.fatal-error + map2-filter on lists of different length. +% File "builtin_stdlib.elpi", line 157, column 0, characters 5247-5329: [98] +std.map2-filter [_ | _] [] _ _ :- std.fatal-error + map2-filter on lists of different length. +% File "builtin_stdlib.elpi", line 158, column 0, characters 5331-5353: [99] +std.map2-filter [] [] _ [] :- . +% File "builtin_stdlib.elpi", line 159, column 0, characters 5355-5427: [100] +std.map2-filter [A0 | A4] [A1 | A5] A3 [A2 | A6] :- A3 A0 A1 A2, !, + std.map2-filter A4 A5 A3 A6. +% File "builtin_stdlib.elpi", line 160, column 0, characters 5429-5485: [101] +std.map2-filter [_ | A0] [_ | A1] A2 A3 :- std.map2-filter A0 A1 A2 A3. +% File "builtin_stdlib.elpi", line 163, column 0, characters 5567-5643: [102] +std.map-ok [A0 | A4] A3 [A1 | A5] A6 :- A3 A0 A1 A2, + if (A2 = ok) (std.map-ok A4 A3 A5 A6) (A6 = A2). +% File "builtin_stdlib.elpi", line 164, column 0, characters 5645-5662: [103] +std.map-ok [] _ [] ok :- . +% File "builtin_stdlib.elpi", line 167, column 0, characters 5738-5758: [104] +std.fold-map [] A0 _ [] A0 :- . +% File "builtin_stdlib.elpi", line 168, column 0, characters 5760-5827: [105] +std.fold-map [A0 | A5] A1 A4 [A2 | A6] A7 :- A4 A0 A1 A2 A3, + std.fold-map A5 A3 A4 A6 A7. +% File "builtin_stdlib.elpi", line 171, column 0, characters 5883-5899: [106] +std.omap none _ none :- . +% File "builtin_stdlib.elpi", line 172, column 0, characters 5901-5934: [107] +std.omap (some A0) A2 (some A1) :- A2 A0 A1. +% File "builtin_stdlib.elpi", line 176, column 0, characters 6041-6067: [108] +std.nth 0 [A0 | _] A1 :- !, A0 = A1. +% File "builtin_stdlib.elpi", line 177, column 0, characters 6069-6121: [109] +std.nth A0 [_ | A2] A3 :- A0 > 0, !, A1 is A0 - 1, std.nth A1 A2 A3. +% File "builtin_stdlib.elpi", line 178, column 0, characters 6123-6184: [110] +std.nth A0 _ _ :- A0 < 0, !, std.fatal-error nth got a negative index. +% File "builtin_stdlib.elpi", line 179, column 0, characters 6186-6238: [111] +std.nth _ _ _ :- std.fatal-error nth run out of list items. +% File "builtin_stdlib.elpi", line 183, column 0, characters 6327-6348: [112] +std.lookup [pr A0 A1 | _] A0 A1 :- . +% File "builtin_stdlib.elpi", line 184, column 0, characters 6350-6390: [113] +std.lookup [_ | A0] A1 A2 :- std.lookup A0 A1 A2. +% File "builtin_stdlib.elpi", line 188, column 0, characters 6509-6536: [114] +std.lookup! [pr A0 A1 | _] A0 A1 :- !. +% File "builtin_stdlib.elpi", line 189, column 0, characters 6538-6580: [115] +std.lookup! [_ | A0] A1 A2 :- std.lookup! A0 A1 A2. +% File "builtin_stdlib.elpi", line 193, column 0, characters 6657-6674: [116] +std.mem! [A0 | _] A0 :- !. +% File "builtin_stdlib.elpi", line 194, column 0, characters 6676-6700: [117] +std.mem! [_ | A0] A1 :- std.mem! A0 A1. +% File "builtin_stdlib.elpi", line 198, column 0, characters 6781-6792: [118] +std.mem [A0 | _] A0 :- . +% File "builtin_stdlib.elpi", line 199, column 0, characters 6794-6816: [119] +std.mem [_ | A0] A1 :- std.mem A0 A1. +% File "builtin_stdlib.elpi", line 202, column 0, characters 6855-6876: [120] +std.exists [A0 | _] A1 :- A1 A0. +% File "builtin_stdlib.elpi", line 203, column 0, characters 6878-6906: [121] +std.exists [_ | A0] A1 :- std.exists A0 A1. +% File "builtin_stdlib.elpi", line 206, column 0, characters 6961-7033: [122] +std.exists2 [] [_ | _] _ :- std.fatal-error + exists2 on lists of different length. +% File "builtin_stdlib.elpi", line 207, column 0, characters 7035-7107: [123] +std.exists2 [_ | _] [] _ :- std.fatal-error + exists2 on lists of different length. +% File "builtin_stdlib.elpi", line 208, column 0, characters 7109-7139: [124] +std.exists2 [A0 | _] [A1 | _] A2 :- A2 A0 A1. +% File "builtin_stdlib.elpi", line 209, column 0, characters 7141-7179: [125] +std.exists2 [_ | A0] [_ | A1] A2 :- std.exists2 A0 A1 A2. +% File "builtin_stdlib.elpi", line 212, column 0, characters 7218-7229: [126] +std.forall [] _ :- . +% File "builtin_stdlib.elpi", line 213, column 0, characters 7231-7264: [127] +std.forall [A0 | A2] A1 :- A1 A0, std.forall A2 A1. +% File "builtin_stdlib.elpi", line 216, column 0, characters 7334-7404: [128] +std.forall-ok [A0 | A3] A2 A4 :- A2 A0 A1, + if (A1 = ok) (std.forall-ok A3 A2 A4) (A4 = A1). +% File "builtin_stdlib.elpi", line 217, column 0, characters 7406-7423: [129] +std.forall-ok [] _ ok :- . +% File "builtin_stdlib.elpi", line 220, column 0, characters 7478-7550: [130] +std.forall2 [] [_ | _] _ :- std.fatal-error + forall2 on lists of different length. +% File "builtin_stdlib.elpi", line 221, column 0, characters 7552-7624: [131] +std.forall2 [_ | _] [] _ :- std.fatal-error + forall2 on lists of different length. +% File "builtin_stdlib.elpi", line 222, column 0, characters 7626-7675: [132] +std.forall2 [A0 | A3] [A1 | A4] A2 :- A2 A0 A1, std.forall2 A3 A4 A2. +% File "builtin_stdlib.elpi", line 223, column 0, characters 7677-7692: [133] +std.forall2 [] [] _ :- . +% File "builtin_stdlib.elpi", line 226, column 0, characters 7741-7758: [134] +std.filter [] _ [] :- . +% File "builtin_stdlib.elpi", line 227, column 0, characters 7760-7826: [135] +std.filter [A0 | A4] A1 A2 :- if (A1 A0) (A2 = [A0 | A3]) (A2 = A3), + std.filter A4 A1 A3. +% File "builtin_stdlib.elpi", line 230, column 0, characters 7877-7941: [136] +std.zip [_ | _] [] _ :- std.fatal-error zip on lists of different length. +% File "builtin_stdlib.elpi", line 231, column 0, characters 7943-8007: [137] +std.zip [] [_ | _] _ :- std.fatal-error zip on lists of different length. +% File "builtin_stdlib.elpi", line 232, column 0, characters 8009-8054: [138] +std.zip [A3 | A0] [A4 | A1] [pr A3 A4 | A2] :- std.zip A0 A1 A2. +% File "builtin_stdlib.elpi", line 233, column 0, characters 8056-8068: [139] +std.zip [] [] [] :- . +% File "builtin_stdlib.elpi", line 236, column 0, characters 8121-8135: [140] +std.unzip [] [] [] :- . +% File "builtin_stdlib.elpi", line 237, column 0, characters 8137-8184: [141] +std.unzip [pr A3 A4 | A0] [A3 | A1] [A4 | A2] :- std.unzip A0 A1 A2. +% File "builtin_stdlib.elpi", line 240, column 0, characters 8227-8277: [142] +std.flatten [A2 | A0] A3 :- std.flatten A0 A1, std.append A2 A1 A3. +% File "builtin_stdlib.elpi", line 241, column 0, characters 8279-8296: [143] +std.flatten [] [] :- . +% File "builtin_stdlib.elpi", line 244, column 0, characters 8319-8326: [144] +std.null [] :- . +% File "builtin_stdlib.elpi", line 248, column 0, characters 8417-8438: [145] +std.list.make 0 _ [] :- !. +% File "builtin_stdlib.elpi", line 249, column 0, characters 8440-8492: [146] +std.list.make A1 A2 [A2 | A3] :- A0 is A1 - 1, std.list.make A0 A2 A3. +% File "builtin_stdlib.elpi", line 253, column 0, characters 8588-8628: [147] +std.list.init A0 A1 A2 :- std.list.init.aux 0 A0 A1 A2. +% File "builtin_stdlib.elpi", line 256, column 0, characters 8695-8722: [148] +std.list.init.aux A0 A0 _ [] :- !. +% File "builtin_stdlib.elpi", line 257, column 0, characters 8724-8795: [149] +std.list.init.aux A0 A4 A2 [A1 | A5] :- A2 A0 A1, A3 is A0 + 1, + std.list.init.aux A3 A4 A2 A5. +% File "builtin_stdlib.elpi", line 260, column 0, characters 8827-8865: [150] +std.iota A0 A1 :- std.list.init A0 (c0 \ c1 \ c0 = c1) A1. +% File "builtin_stdlib.elpi", line 265, column 0, characters 8969-8988: [151] +std.intersperse _ [] [] :- . +% File "builtin_stdlib.elpi", line 266, column 0, characters 8990-9016: [152] +std.intersperse _ [A0] [A0] :- !. +% File "builtin_stdlib.elpi", line 267, column 0, characters 9018-9076: [153] +std.intersperse A0 [A3 | A1] [A3, A0 | A2] :- std.intersperse A0 A1 A2. +% File "builtin_stdlib.elpi", line 272, column 0, characters 9133-9152: [154] +std.flip A2 A1 A0 :- A2 A0 A1. +% File "builtin_stdlib.elpi", line 275, column 0, characters 9182-9257: [155] +std.time A1 A3 :- gettimeofday A0, A1, gettimeofday A2, A3 is A2 - A0. +% File "builtin_stdlib.elpi", line 278, column 0, characters 9282-9288: [156] +std.do! [] :- . +% File "builtin_stdlib.elpi", line 279, column 0, characters 9290-9316: [157] +std.do! [A0 | A1] :- A0, !, std.do! A1. +% File "builtin_stdlib.elpi", line 283, column 0, characters 9385-9397: [158] +std.do-ok! ok [] :- . +% File "builtin_stdlib.elpi", line 284, column 0, characters 9399-9462: [159] +std.do-ok! A2 [A1 | A3] :- A1 A0, !, + if (A0 = ok) (std.do-ok! A2 A3) (A2 = A0). +% File "builtin_stdlib.elpi", line 287, column 0, characters 9510-9555: [160] +std.lift-ok A0 A2 A1 :- A0 , A1 = ok ; A1 = error A2. +% File "builtin_stdlib.elpi", line 290, column 0, characters 9584-9629: [161] +std.spy-do! A0 :- std.map A0 (c0 \ c1 \ c1 = std.spy c0) A1, std.do! A1. +% File "builtin_stdlib.elpi", line 293, column 0, characters 9706-9737: [162] +std.while-ok-do! (as (error _) A0) _ A0 :- . +% File "builtin_stdlib.elpi", line 294, column 0, characters 9739-9760: [163] +std.while-ok-do! ok [] ok :- . +% File "builtin_stdlib.elpi", line 295, column 0, characters 9762-9817: [164] +std.while-ok-do! ok [A1 | A2] A3 :- A1 A0, !, std.while-ok-do! A0 A2 A3. +% File "builtin_stdlib.elpi", line 298, column 0, characters 9852-9889: [165] +std.any->string A0 A1 :- term_to_string A0 A1. +% File "builtin_stdlib.elpi", line 301, column 0, characters 9916-9938: [166] +std.max A0 A1 A0 :- A0 >= A1, !. +% File "builtin_stdlib.elpi", line 302, column 0, characters 9940-9949: [167] +std.max _ A0 A0 :- . +% File "builtin_stdlib.elpi", line 306, column 0, characters 10063-10099: [168] +std.findall A0 A1 :- findall_solutions A0 A1. +% File "builtin_map.elpi", line 8, column 0, characters 10432-10468: [169] +std.map.make A0 (std.map std.map.private.empty A0) :- . +% File "builtin_map.elpi", line 12, column 0, characters 10564-10614: [170] +std.map.find A2 (std.map A0 A1) A3 :- std.map.private.find A0 A1 A2 A3. +% File "builtin_map.elpi", line 16, column 0, characters 10713-10781: [171] +std.map.add A2 A3 (std.map A0 A1) (std.map A4 A1) :- std.map.private.add A0 + A1 A2 A3 A4. +% File "builtin_map.elpi", line 20, column 0, characters 10876-10946: [172] +std.map.remove A2 (std.map A0 A1) (std.map A3 A1) :- std.map.private.remove + A0 A1 A2 A3. +% File "builtin_map.elpi", line 24, column 0, characters 11059-11110: [173] +std.map.bindings (std.map A0 _) A1 :- std.map.private.bindings A0 [] A1. +% File "builtin_map.elpi", line 34, column 0, characters 11302-11316: [174] +std.map.private.height std.map.private.empty 0 :- . +% File "builtin_map.elpi", line 35, column 0, characters 11318-11343: [175] +std.map.private.height (std.map.private.node _ _ _ _ A0) A0 :- . +% File "builtin_map.elpi", line 38, column 0, characters 11401-11476: [176] +std.map.private.create A0 A6 A7 A2 (std.map.private.node A0 A6 A7 A2 A5) :- + std.map.private.height A0 A1, std.map.private.height A2 A3, + std.max A1 A3 A4, A5 is A4 + 1. +% File "builtin_map.elpi", line 41, column 0, characters 11531-11645: [177] +std.map.private.bal A0 A6 A7 A2 A8 :- std.map.private.height A0 A1, + std.map.private.height A2 A3, A4 is A1 + 2, A5 is A3 + 2, + std.map.private.bal.aux A1 A3 A4 A5 A0 A6 A7 A2 A8. +% File "builtin_map.elpi", line 49, column 0, characters 11732-11863: [178] +std.map.private.bal.aux A0 _ _ A1 (std.map.private.node A2 A10 A11 A4 _) A6 + A7 A8 A12 :- A0 > A1, std.map.private.height A2 A3, + std.map.private.height A4 A5, A3 >= A5, !, + std.map.private.create A4 A6 A7 A8 A9, + std.map.private.create A2 A10 A11 A9 A12. +% File "builtin_map.elpi", line 52, column 0, characters 11865-12012: [179] +std.map.private.bal.aux A0 _ _ A1 + (std.map.private.node A2 A3 A4 (std.map.private.node A5 A12 A13 A7 _) _) A8 + A9 A10 A14 :- A0 > A1, !, std.map.private.create A2 A3 A4 A5 A6, + std.map.private.create A7 A8 A9 A10 A11, + std.map.private.create A6 A12 A13 A11 A14. +% File "builtin_map.elpi", line 55, column 0, characters 12014-12145: [180] +std.map.private.bal.aux _ A0 A1 _ A6 A7 A8 + (std.map.private.node A4 A10 A11 A2 _) A12 :- A0 > A1, + std.map.private.height A2 A3, std.map.private.height A4 A5, A3 >= A5, !, + std.map.private.create A6 A7 A8 A4 A9, + std.map.private.create A9 A10 A11 A2 A12. +% File "builtin_map.elpi", line 58, column 0, characters 12147-12294: [181] +std.map.private.bal.aux _ A0 A1 _ A2 A3 A4 + (std.map.private.node (std.map.private.node A5 A12 A13 A7 _) A8 A9 A10 _) + A14 :- A0 > A1, !, std.map.private.create A2 A3 A4 A5 A6, + std.map.private.create A7 A8 A9 A10 A11, + std.map.private.create A6 A12 A13 A11 A14. +% File "builtin_map.elpi", line 61, column 0, characters 12296-12341: [182] +std.map.private.bal.aux _ _ _ _ A0 A1 A2 A3 A4 :- std.map.private.create A0 + A1 A2 A3 A4. +% File "builtin_map.elpi", line 64, column 0, characters 12411-12456: [183] +std.map.private.add std.map.private.empty _ A0 A1 A2 :- std.map.private.create + std.map.private.empty + A0 A1 + std.map.private.empty + A2. +% File "builtin_map.elpi", line 65, column 0, characters 12458-12536: [184] +std.map.private.add (as (std.map.private.node _ A1 _ _ _) A4) A3 A0 A5 A6 :- + A3 A0 A1 A2, std.map.private.add.aux A2 A4 A3 A0 A5 A6. +% File "builtin_map.elpi", line 68, column 0, characters 12617-12678: [185] +std.map.private.add.aux eq (std.map.private.node A1 _ _ A4 A5) _ A2 A3 A0 :- + A0 = std.map.private.node A1 A2 A3 A4 A5. +% File "builtin_map.elpi", line 69, column 0, characters 12681-12751: [186] +std.map.private.add.aux lt (std.map.private.node A0 A5 A6 A7 _) A1 A2 A3 A8 :- + std.map.private.add A0 A1 A2 A3 A4, std.map.private.bal A4 A5 A6 A7 A8. +% File "builtin_map.elpi", line 70, column 0, characters 12753-12823: [187] +std.map.private.add.aux gt (std.map.private.node A5 A6 A7 A0 _) A1 A2 A3 A8 :- + std.map.private.add A0 A1 A2 A3 A4, std.map.private.bal A5 A6 A7 A4 A8. +% File "builtin_map.elpi", line 73, column 0, characters 12883-12955: [188] +std.map.private.find (std.map.private.node A4 A1 A6 A5 _) A3 A0 A7 :- + A3 A0 A1 A2, std.map.private.find.aux A2 A3 A4 A5 A6 A0 A7. +% File "builtin_map.elpi", line 76, column 0, characters 13042-13067: [189] +std.map.private.find.aux eq _ _ _ A0 _ A0 :- . +% File "builtin_map.elpi", line 77, column 0, characters 13069-13112: [190] +std.map.private.find.aux lt A1 A0 _ _ A2 A3 :- std.map.private.find A0 A1 A2 + A3. +% File "builtin_map.elpi", line 78, column 0, characters 13114-13157: [191] +std.map.private.find.aux gt A1 _ A0 _ A2 A3 :- std.map.private.find A0 A1 A2 + A3. +% File "builtin_map.elpi", line 81, column 0, characters 13206-13252: [192] +std.map.private.remove-min-binding + (std.map.private.node std.map.private.empty _ _ A0 _) A0 :- !. +% File "builtin_map.elpi", line 82, column 0, characters 13254-13329: [193] +std.map.private.remove-min-binding (std.map.private.node A0 A2 A3 A4 _) A5 :- + std.map.private.remove-min-binding A0 A1, + std.map.private.bal A1 A2 A3 A4 A5. +% File "builtin_map.elpi", line 85, column 0, characters 13370-13411: [194] +std.map.private.min-binding + (std.map.private.node std.map.private.empty A0 A1 _ _) A0 A1 :- !. +% File "builtin_map.elpi", line 86, column 0, characters 13413-13466: [195] +std.map.private.min-binding (std.map.private.node A0 _ _ _ _) A1 A2 :- + std.map.private.min-binding A0 A1 A2. +% File "builtin_map.elpi", line 89, column 0, characters 13513-13533: [196] +std.map.private.merge std.map.private.empty A0 A0 :- !. +% File "builtin_map.elpi", line 90, column 0, characters 13535-13555: [197] +std.map.private.merge A0 std.map.private.empty A0 :- !. +% File "builtin_map.elpi", line 91, column 0, characters 13557-13634: [198] +std.map.private.merge A4 A0 A5 :- std.map.private.min-binding A0 A1 A2, + std.map.private.remove-min-binding A0 A3, + std.map.private.bal A4 A1 A2 A3 A5. +% File "builtin_map.elpi", line 96, column 0, characters 13702-13729: [199] +std.map.private.remove std.map.private.empty _ _ std.map.private.empty :- !. +% File "builtin_map.elpi", line 97, column 0, characters 13731-13805: [200] +std.map.private.remove (std.map.private.node A4 A1 A6 A5 _) A3 A0 A7 :- + A3 A0 A1 A2, std.map.private.remove.aux A2 A3 A4 A5 A1 A6 A0 A7. +% File "builtin_map.elpi", line 100, column 0, characters 13905-13949: [201] +std.map.private.remove.aux eq _ A0 A1 _ _ _ A2 :- std.map.private.merge A0 + A1 A2. +% File "builtin_map.elpi", line 101, column 0, characters 13951-14012: [202] +std.map.private.remove.aux lt A1 A0 A6 A4 A5 A2 A7 :- std.map.private.remove + A0 A1 A2 A3, + std.map.private.bal A3 A4 A5 A6 A7. +% File "builtin_map.elpi", line 102, column 0, characters 14014-14075: [203] +std.map.private.remove.aux gt A1 A4 A0 A5 A6 A2 A7 :- std.map.private.remove + A0 A1 A2 A3, + std.map.private.bal A4 A5 A6 A3 A7. +% File "builtin_map.elpi", line 105, column 0, characters 14141-14159: [204] +std.map.private.bindings std.map.private.empty A0 A0 :- . +% File "builtin_map.elpi", line 106, column 0, characters 14161-14234: [205] +std.map.private.bindings (std.map.private.node A3 A4 A5 A0 _) A1 A6 :- + std.map.private.bindings A0 A1 A2, + std.map.private.bindings A3 [pr A4 A5 | A2] A6. +% File "builtin_set.elpi", line 8, column 0, characters 22779-22815: [206] +std.set.make A0 (std.set std.set.private.empty A0) :- . +% File "builtin_set.elpi", line 12, column 0, characters 22876-22919: [207] +std.set.mem A2 (std.set A0 A1) :- std.set.private.mem A0 A1 A2. +% File "builtin_set.elpi", line 16, column 0, characters 22991-23055: [208] +std.set.add A2 (std.set A0 A1) (std.set A3 A1) :- std.set.private.add A0 A1 + A2 A3. +% File "builtin_set.elpi", line 20, column 0, characters 23133-23203: [209] +std.set.remove A2 (std.set A0 A1) (std.set A3 A1) :- std.set.private.remove + A0 A1 A2 A3. +% File "builtin_set.elpi", line 24, column 0, characters 23290-23338: [210] +std.set.cardinal (std.set A0 _) A1 :- std.set.private.cardinal A0 A1. +% File "builtin_set.elpi", line 27, column 0, characters 23378-23429: [211] +std.set.elements (std.set A0 _) A1 :- std.set.private.elements A0 [] A1. +% File "builtin_set.elpi", line 37, column 0, characters 23598-23612: [212] +std.set.private.height std.set.private.empty 0 :- . +% File "builtin_set.elpi", line 38, column 0, characters 23614-23637: [213] +std.set.private.height (std.set.private.node _ _ _ A0) A0 :- . +% File "builtin_set.elpi", line 41, column 0, characters 23684-23755: [214] +std.set.private.create A0 A6 A2 (std.set.private.node A0 A6 A2 A5) :- + std.set.private.height A0 A1, std.set.private.height A2 A3, + std.max A1 A3 A4, A5 is A4 + 1. +% File "builtin_set.elpi", line 44, column 0, characters 23799-23909: [215] +std.set.private.bal A0 A6 A2 A7 :- std.set.private.height A0 A1, + std.set.private.height A2 A3, A4 is A1 + 2, A5 is A3 + 2, + std.set.private.bal.aux A1 A3 A4 A5 A0 A6 A2 A7. +% File "builtin_set.elpi", line 52, column 0, characters 23985-24106: [216] +std.set.private.bal.aux A0 _ _ A1 (std.set.private.node A2 A9 A4 _) A6 A7 A10 :- + A0 > A1, std.set.private.height A2 A3, std.set.private.height A4 A5, + A3 >= A5, !, std.set.private.create A4 A6 A7 A8, + std.set.private.create A2 A9 A8 A10. +% File "builtin_set.elpi", line 55, column 0, characters 24108-24237: [217] +std.set.private.bal.aux A0 _ _ A1 + (std.set.private.node A2 A3 (std.set.private.node A4 A10 A6 _) _) A7 A8 A11 :- + A0 > A1, !, std.set.private.create A2 A3 A4 A5, + std.set.private.create A6 A7 A8 A9, std.set.private.create A5 A10 A9 A11. +% File "builtin_set.elpi", line 58, column 0, characters 24239-24360: [218] +std.set.private.bal.aux _ A0 A1 _ A6 A7 (std.set.private.node A4 A9 A2 _) A10 :- + A0 > A1, std.set.private.height A2 A3, std.set.private.height A4 A5, + A3 >= A5, !, std.set.private.create A6 A7 A4 A8, + std.set.private.create A8 A9 A2 A10. +% File "builtin_set.elpi", line 61, column 0, characters 24362-24491: [219] +std.set.private.bal.aux _ A0 A1 _ A2 A3 + (std.set.private.node (std.set.private.node A4 A10 A6 _) A7 A8 _) A11 :- + A0 > A1, !, std.set.private.create A2 A3 A4 A5, + std.set.private.create A6 A7 A8 A9, std.set.private.create A5 A10 A9 A11. +% File "builtin_set.elpi", line 64, column 0, characters 24493-24534: [220] +std.set.private.bal.aux _ _ _ _ A0 A1 A2 A3 :- std.set.private.create A0 A1 + A2 A3. +% File "builtin_set.elpi", line 67, column 0, characters 24595-24636: [221] +std.set.private.add std.set.private.empty _ A0 A1 :- std.set.private.create + std.set.private.empty + A0 + std.set.private.empty + A1. +% File "builtin_set.elpi", line 68, column 0, characters 24638-24707: [222] +std.set.private.add (std.set.private.node A4 A1 A5 A6) A3 A0 A7 :- A3 A0 A1 + A2, + std.set.private.add.aux A2 A3 A4 A5 A1 A0 A6 A7. +% File "builtin_set.elpi", line 71, column 0, characters 24800-24839: [223] +std.set.private.add.aux eq _ A0 A1 A2 _ A3 (std.set.private.node A0 A2 A1 A3) :- . +% File "builtin_set.elpi", line 72, column 0, characters 24841-24894: [224] +std.set.private.add.aux lt A1 A0 A5 A4 A2 _ A6 :- std.set.private.add A0 A1 + A2 A3, + std.set.private.bal A3 A4 A5 A6. +% File "builtin_set.elpi", line 73, column 0, characters 24896-24949: [225] +std.set.private.add.aux gt A1 A4 A0 A5 A2 _ A6 :- std.set.private.add A0 A1 + A2 A3, + std.set.private.bal A4 A5 A3 A6. +% File "builtin_set.elpi", line 76, column 0, characters 25001-25059: [226] +std.set.private.mem (std.set.private.node A4 A1 A5 _) A3 A0 :- A3 A0 A1 A2, + std.set.private.mem.aux A2 A3 A4 A5 A0. +% File "builtin_set.elpi", line 77, column 0, characters 25061-25079: [227] +std.set.private.mem.aux eq _ _ _ _ :- . +% File "builtin_set.elpi", line 80, column 0, characters 25151-25186: [228] +std.set.private.mem.aux lt A1 A0 _ A2 :- std.set.private.mem A0 A1 A2. +% File "builtin_set.elpi", line 81, column 0, characters 25188-25223: [229] +std.set.private.mem.aux gt A1 _ A0 A2 :- std.set.private.mem A0 A1 A2. +% File "builtin_set.elpi", line 84, column 0, characters 25268-25312: [230] +std.set.private.remove-min-binding + (std.set.private.node std.set.private.empty _ A0 _) A0 :- !. +% File "builtin_set.elpi", line 85, column 0, characters 25314-25385: [231] +std.set.private.remove-min-binding (std.set.private.node A0 A2 A3 _) A4 :- + std.set.private.remove-min-binding A0 A1, std.set.private.bal A1 A2 A3 A4. +% File "builtin_set.elpi", line 88, column 0, characters 25419-25456: [232] +std.set.private.min-binding + (std.set.private.node std.set.private.empty A0 _ _) A0 :- !. +% File "builtin_set.elpi", line 89, column 0, characters 25458-25505: [233] +std.set.private.min-binding (std.set.private.node A0 _ _ _) A1 :- std.set.private.min-binding + A0 A1. +% File "builtin_set.elpi", line 92, column 0, characters 25546-25566: [234] +std.set.private.merge std.set.private.empty A0 A0 :- !. +% File "builtin_set.elpi", line 93, column 0, characters 25568-25588: [235] +std.set.private.merge A0 std.set.private.empty A0 :- !. +% File "builtin_set.elpi", line 94, column 0, characters 25590-25663: [236] +std.set.private.merge A3 A0 A4 :- std.set.private.min-binding A0 A1, + std.set.private.remove-min-binding A0 A2, std.set.private.bal A3 A1 A2 A4. +% File "builtin_set.elpi", line 99, column 0, characters 25727-25749: [237] +std.set.private.remove std.set.private.empty _ _ std.set.private.empty :- . +% File "builtin_set.elpi", line 100, column 0, characters 25751-25821: [238] +std.set.private.remove (std.set.private.node A4 A1 A5 _) A3 A0 A6 :- + A3 A0 A1 A2, std.set.private.remove.aux A2 A3 A4 A5 A1 A0 A6. +% File "builtin_set.elpi", line 103, column 0, characters 25910-25952: [239] +std.set.private.remove.aux eq _ A0 A1 _ _ A2 :- std.set.private.merge A0 A1 + A2. +% File "builtin_set.elpi", line 104, column 0, characters 25954-26011: [240] +std.set.private.remove.aux lt A1 A0 A5 A4 A2 A6 :- std.set.private.remove A0 + A1 A2 A3, + std.set.private.bal A3 A4 A5 A6. +% File "builtin_set.elpi", line 105, column 0, characters 26013-26070: [241] +std.set.private.remove.aux gt A1 A4 A0 A5 A2 A6 :- std.set.private.remove A0 + A1 A2 A3, + std.set.private.bal A4 A5 A3 A6. +% File "builtin_set.elpi", line 108, column 0, characters 26103-26119: [242] +std.set.private.cardinal std.set.private.empty 0 :- . +% File "builtin_set.elpi", line 109, column 0, characters 26121-26186: [243] +std.set.private.cardinal (std.set.private.node A0 _ A2 _) A4 :- std.set.private.cardinal + A0 A1, + std.set.private.cardinal A2 A3, A4 is A1 + 1 + A3. +% File "builtin_set.elpi", line 112, column 0, characters 26232-26250: [244] +std.set.private.elements std.set.private.empty A0 A0 :- . +% File "builtin_set.elpi", line 113, column 0, characters 26252-26320: [245] +std.set.private.elements (std.set.private.node A3 A4 A0 _) A1 A5 :- std.set.private.elements + A0 A1 A2, + std.set.private.elements A3 [A4 | A2] A5. +% File "builtin_set.elpi", line 255, column 0, characters 31127-31176: [246] +printterm A2 A0 :- term_to_string A0 A1, output A2 A1. +% File "coq-builtin.elpi", line 269, column 0, characters 10824-10944: [247] default-declare-evar +declare-evar A0 A1 A2 A3 :- declare_constraint (declare-evar A0 A1 A2 A3) + [A1]. +% File "coq-builtin.elpi", line 278, column 0, characters 11184-11259: [248] +rm-evar (as uvar A0) (as uvar A1) :- !, + declare_constraint (rm-evar A0 A1) [A0, A1]. +% File "coq-builtin.elpi", line 279, column 0, characters 11261-11272: [249] +rm-evar _ _ :- . +% File "coq-builtin.elpi", line 300, column 0, characters 12041-12144: [250] +evar (as uvar A3) A2 A0 :- var A0 _ A1, !, prune A2 A1, prune A3 A1, + declare_constraint (evar A3 A2 A0) [A3, A0]. +% File "coq-builtin.elpi", line 303, column 0, characters 12147-12185: [251] default-assign-evar +evar _ _ _ :- . +% File "coq-builtin.elpi", line 751, column 3, characters 30685-30843: [252] +coq.env.const-opaque? A0 :- coq.warning elpi.deprecated elpi.const-opaque + use coq.env.opaque? in place of coq.env.const-opaque?, + coq.env.opaque? A0. +% File "coq-builtin.elpi", line 758, column 3, characters 30933-31106: [253] +coq.env.const-primitive? A0 :- coq.warning elpi.deprecated + elpi.const-primitive + use coq.env.primitive? in place of coq.env.const-primitive?, + coq.env.primitive? A0. +% File "coq-builtin.elpi", line 840, column 0, characters 34275-34346: [254] +coq.env.begin-module A0 A1 :- coq.env.begin-module-functor A0 A1 []. +% File "coq-builtin.elpi", line 853, column 0, characters 34756-34833: [255] +coq.env.begin-module-type A0 :- coq.env.begin-module-type-functor A0 []. +% File "coq-builtin.elpi", line 1232, column 0, characters 49508-49698: [256] +coq.CS.canonical-projections A0 A1 :- coq.warning elpi.deprecated + elpi.canonical-projections + use coq.env.projections in place of coq.CS.canonical-projections, + coq.env.projections A0 A1. +% File "coq-builtin.elpi", line 1536, column 0, characters 62266-62446: [257] +coq.reduction.cbv.whd_all A0 A1 :- coq.warning elpi.deprecated + elpi.cbv-whd-all + use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all, + coq.reduction.cbv.norm A0 A1. +% File "coq-builtin.elpi", line 1543, column 0, characters 62544-62725: [258] +coq.reduction.vm.whd_all A0 A1 A2 :- coq.warning elpi.deprecated + elpi.vm-whd-all + use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all, + coq.reduction.vm.norm A0 A1 A2. +% File "coq-builtin.elpi", line 1550, column 0, characters 62778-62871: [259] +coq.reduction.lazy.whd_all A0 A1 :- get-option coq:redflags coq.redflags.all + => coq.reduction.lazy.whd A0 A1. +% File "coq-builtin.elpi", line 1667, column 0, characters 67249-67289: [260] +coq.id->name A0 A1 :- coq.string->name A0 A1. +% File "coq-builtin.elpi", line 1769, column 0, characters 71023-71087: [261] +coq.elpi.accumulate A0 A1 A2 :- coq.elpi.accumulate-clauses A0 A1 [A2]. +% File "./examples/tutorial_elpi_lang.v", line 491, column 3, characters 12653-12720: [262] +whd (app A0 A2) A3 :- whd A0 (fun A1), !, whd (A1 A2) A3. +% File "./examples/tutorial_elpi_lang.v", line 495, column 3, characters 12776-12801: [263] +whd A1 A0 :- A0 = A1. +% File "./examples/tutorial_elpi_lang.v", line 591, column 3, characters 15201-15250: [264] +of (app A0 A3) A2 :- of A0 (arr A1 A2), of A3 A1. +% File "./examples/tutorial_elpi_lang.v", line 596, column 3, characters 15367-15421: [265] +of (fun A0) (arr A2 A1) :- pi c0 \ of c0 A2 => of (A0 c0) A1. diff --git a/tutorial_coq_elpi_HOAS.html b/tutorial_coq_elpi_HOAS.html index 9bf5a526e..ea63e5998 100644 --- a/tutorial_coq_elpi_HOAS.html +++ b/tutorial_coq_elpi_HOAS.html @@ -176,24 +176,30 @@

HOAS for Gallina

syntax tree of Coq terms.

Constructor global

-

Let's start with the gref data type (for global reference).

+

Let's start with the gref data type (for global reference).

 type const constant -> gref.
 type indt inductive -> gref.
 type indc constructor -> gref.
-

constant, inductive and constructor are Coq specific -data types that are opaque to Elpi. Still the gref data type lets you +

constant, inductive and constructor are Coq specific +data types that are opaque to Elpi. Still the gref data type lets you see what these names point to (a constant, and inductive type or a constructor).

-

The coq.locate API resolves a string to a gref.

+

The coq.locate API resolves a string to a gref.

Query assignments:
GRnat = indt «nat»
GRplus = const «Nat.add»
GRs = indc «S»

The coq.env.* family of APIs lets one access the +}}.

Toplevel input, characters 38-42 +GRnat is linear: name it _GRnat (discard) or GRnat_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 87-92 +GRplus is linear: name it _GRplus (discard) or GRplus_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 62-64 +GRs is linear: name it _GRs (discard) or GRs_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
GRnat = indt «nat»
GRplus = const «Nat.add»
GRs = indc «S»

The coq.env.* family of APIs lets one access the environment of well typed Coq terms that have a global name.

Definition x := 2.
 
@@ -210,16 +216,22 @@ 
Constructor 
   % constants may have a body, do have a type
   coq.env.const C (some Bo) TyC
 
-}}.
Query assignments:
Bo = app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]
C = «x»
GR = const «x»
Ty = global (indt «nat»)
TyC = global (indt «nat»)

An expression like indt «nat» is not a Coq term (or better a type) yet.

-

The global term constructor turns a gref into an -actual term.

+}}.
Toplevel input, characters 257-258 +Bo is linear: name it _Bo (discard) or Bo_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 119-120 +Ty is linear: name it _Ty (discard) or Ty_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 261-263 +TyC is linear: name it _TyC (discard) or TyC_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
Bo = app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]
C = «x»
GR = const «x»
Ty = global (indt «nat»)
TyC = global (indt «nat»)

An expression like indt «nat» is not a Coq term (or better a type) yet.

+

The global term constructor turns a gref into an +actual term.

 type global gref -> term.

Constructors app and fun

-

The app term constructor takes a list of terms and builds +

The app term constructor takes a list of terms and builds the (n-ary) application. The first term is the head, while the others are the arguments.

For example app [global (indc «S»), global (indc «O»)] is @@ -235,36 +247,40 @@

Constructors "f" (const C), coq.env.const C (some Bo) _ -}}.
Query assignments:
Bo = fun `x` (global (indt «nat»)) c0 \ c0
C = «f»

The fun constructor carries a pretty printing hint `x`, +}}.

Toplevel input, characters 106-107 +Bo is linear: name it _Bo (discard) or Bo_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
Bo = fun `x` (global (indt «nat»)) c0 \ c0
C = «f»

The fun constructor carries a pretty printing hint `x`, the type of the bound variable nat and a function describing the body:

 type fun  name -> term -> (term -> term) -> term.

Note

-

name is just for pretty printing: in spite of carrying +

name is just for pretty printing: in spite of carrying a value in the Coq world, it has no content in Elpi (like the unit type)

-

Elpi terms of type name are just identifiers +

Elpi terms of type name are just identifiers written between ` (backticks).

Query assignments:
B = X0
T = X1

API such as coq.name-suffix lets one craft a family of +}}.

Query assignments:
B = X0
T = X1

API such as coq.name-suffix lets one craft a family of names starting from one, eg coq.name-suffix `H` 1 N sets N to `H1`.

Constructors fix and match

-

The other binders prod (Coq's forall, AKA Π) and let are similar, -so let's rather focus on fix here.

+

The other binders prod (Coq's forall, AKA Π) and let are similar, +so let's rather focus on fix here.

Query assignments:
 Bo = fix `add` 0 
+}}.
Toplevel input, characters 74-75
+Bo is linear: name it _Bo (discard) or Bo_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
 Bo = fix `add` 0 
 (prod `n` (global (indt «nat»)) c0 \
   prod `m` (global (indt «nat»)) c1 \ global (indt «nat»)) c0 \
 fun `n` (global (indt «nat»)) c1 \
@@ -272,14 +288,14 @@ 
Constructors match c1 (fun `n` (global (indt «nat»)) c3 \ global (indt «nat»)) 
    [c2, 
     fun `p` (global (indt «nat»)) c3 \
-     app [global (indc «S»), app [c0, c3, c2]]]
C = «Nat.add»

The fix constructor carries a pretty printing hint, + app [global (indc «S»), app [c0, c3, c2]]]

C = «Nat.add»

The fix constructor carries a pretty printing hint, the number of the recursive argument (starting at 0), the type of the recursive function and finally the body where the recursive call is represented via a bound variable

 type fix   name -> int -> term -> (term -> term) -> term.
-

A match constructor carries the term being inspected, +

A match constructor carries the term being inspected, the return clause and a list of branches. Each branch is a Coq function expecting in input the arguments of the corresponding constructor. The order follows the @@ -311,13 +327,13 @@

Constructors global (indc «O»)]) c4 \ app [c1, c2]

Constructor sort

-

The last term constructor worth discussing is sort.

+

The last term constructor worth discussing is sort.

 type sort  universe -> term.
 type prop universe.
 type typ univ -> universe.
-

The opaque type univ is a universe level variable. Elpi holds a store of +

The opaque type univ is a universe level variable. Elpi holds a store of constraints among these variables and provides APIs named coq.univ.* to impose constraints.

Let's play a bit more with universe constraints using the -coq.typecheck API:

+coq.typecheck API:

The diagnostic data type is used by coq.typecheck to +

The diagnostic data type is used by coq.typecheck to tell if the term is well typed. The constructor ok signals success, while error carries an error message. In case of success universe constraints are added to the store.

@@ -541,7 +559,7 @@

Quotations and Antiquotations fun `b` (global (indt «nat»)) c1 \ app [global (indt «eq»), global (indt «nat»), c0, c1]
Query assignments:
T = fun `ax` (global (indt «nat»)) c0 \ fun `b` (global (indt «nat»)) c1 \ - app [global (indt «eq»), global (indt «nat»), c0, c1]
_uvk_1_ = c0 \ + app [global (indt «eq»), global (indt «nat»), c0, c1]
X1_ = c0 \ global (indt «nat»)
Universe constraints: UNIVERSES: {tutorial_coq_elpi_HOAS.11 tutorial_coq_elpi_HOAS.10} |= @@ -588,7 +606,7 @@

The context

In some sense Elpi's way of traversing a binder is similar to a Zipper. The context of Elpi must record the part of the Zipper context that is relevant for binders.

-

The two predicates decl and def are used +

The two predicates decl and def are used for that purpose:

 pred decl i:term, o:name, o:term.         % Var Name Ty
@@ -601,7 +619,7 @@ 
The context

   coq.typecheck T _ ok,
   T = fun N Ty Bo,
   pi x\
-    decl x N Ty =>
+    decl x N Ty ==>
       coq.typecheck (Bo x) _ ok
 
 }}.
Query assignments:
  Bo = c0 \
@@ -613,7 +631,7 @@ 
The context

   app [global (indc «S»), global (indc «O»)]]
Ty = global (indt «nat»)

In order to ease this task, Coq-Elpi provides a few commodity macros such as @pi-decl:

-macro @pi-decl N T F :- pi x\ decl x N T => F x.
+macro @pi-decl N T F :- pi x\ decl x N T ==> F x.

Note

@@ -636,9 +654,9 @@

The context

app [global (indc «S»), global (indc «O»)]]
Ty = global (indt «nat»)

Tip

-

@pi-decl N Ty x\ takes arguments in the same order of fun and -prod, while -@pi-def N Ty Bo x\ takes arguments in the same order of let.

+

@pi-decl N Ty x\ takes arguments in the same order of fun and +prod, while +@pi-def N Ty Bo x\ takes arguments in the same order of let.

@@ -672,7 +690,7 @@

The context

?X11 <-> X1 ELAB: ?X11 <-> X1 -
Query assignments:
T = X1
_uvk_4_ = X1
Syntactic constraints: +
Query assignments:
T = X1
X2_ = X1
Syntactic constraints: evar (X1) (global (indt «nat»)) (X1) /* suspended on X1 */
Universe constraints: UNIVERSES: {tutorial_coq_elpi_HOAS.12} |= @@ -685,7 +703,7 @@

The context

α7 := Type WEAK CONSTRAINTS: -

Before the call to coq.typecheck, coq.sigma.print +

Before the call to coq.typecheck, coq.sigma.print prints nothing interesting, while after the call it also prints the following syntactic constraint:

evar (X1) (global (indt «nat»)) (X1)  /* suspended on X1 */

which indicates that the hole X1 is linked to a Coq evar @@ -741,7 +759,7 @@

The context

?X13 <-> X1
Query assignments:
Bo = c0 \ app [global (const «Nat.add»), c0, X1 c0]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \ -app [global (const «Nat.add»), c0, X1 c0]
Ty = global (indt «nat»)
_uvk_9_ = c0 \ +app [global (const «Nat.add»), c0, X1 c0]
Ty = global (indt «nat»)
X3_ = c0 \ X1 c0
Syntactic constraints: {c0 c1} : decl c1 `x` (global (indt «nat»)) ?- evar (X1 c1) (global (indt «nat»)) (X1 c1) /* suspended on X1 */
Universe constraints: @@ -815,7 +833,11 @@

Outside the pattern fragment< % boom coq.typecheck Bo1 {{ nat }} ok. -}}.
Bo1 (not in pattern fragment) = +}}.
Toplevel input, characters 95-95 +N is linear: name it _N (discard) or N_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 97-98 +Ty is linear: name it _Ty (discard) or Ty_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Bo1 (not in pattern fragment) = app [global (const «Nat.add»), app [global (indc «S»), global (indc «O»)], @@ -833,7 +855,7 @@

Outside the pattern fragment< to be a special dummy constant, to be turned into an actual hole on the fly when needed.

This use case is perfectly legitimate and is supported by all APIs taking -terms in input thanks to the @holes! option.

+terms in input thanks to the @holes! option.

Note that after the call to coq.typecheck, X0 is assigned the +

Note that after the call to coq.typecheck, X0 is assigned the term _\ X1, that means that the offending argument has been pruned (discarded).

Note

-

All APIs taking a term support the @holes! option.

+

All APIs taking a term support the @holes! option.

-

In addition to the @holes! option, there is a class of APIs which can +

In addition to the @holes! option, there is a class of APIs which can deal with terms outside the pattern fragment. These APIs take in input a term -skeleton. A skeleton is not modified in place, as coq.typecheck +skeleton. A skeleton is not modified in place, as coq.typecheck does with its first argument, but is rather elaborated to a term related to it.

In some sense APIs taking a skeleton are more powerful, because they can modify the structure of the term, eg. insert a coercions, but are less @@ -894,14 +920,20 @@

Outside the pattern fragment< Bo1 = Bo {{ 1 }}, coq.elaborate-skeleton Bo1 {{ bool }} Bo2 ok -}}.
Query assignments:
Bo = c0 \ +}}.
Toplevel input, characters 221-223 +Bo2 is linear: name it _Bo2 (discard) or Bo2_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 152-152 +N is linear: name it _N (discard) or N_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Toplevel input, characters 154-155 +Ty is linear: name it _Ty (discard) or Ty_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
Query assignments:
Bo = c0 \ app [global (const «andb»), c0, X0 c0]
Bo1 = app [global (const «andb»), app [global (indc «S»), global (indc «O»)], X0 (app [global (indc «S»), global (indc «O»)])]
Bo2 = app [global (const «andb»), app [global (const «nat2bool»), - app [global (indc «S»), global (indc «O»)]], X1]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \ app [global (const «andb»), c0, X0 c0]
Ty = global (indt «nat»)
_uvk_21_ = X0
Syntactic constraints: + app [global (indc «S»), global (indc «O»)]], X1]
N = `x`
T = fun `x` (global (indt «nat»)) c0 \ app [global (const «andb»), c0, X0 c0]
Ty = global (indt «nat»)
X6_ = X0
Syntactic constraints: evar (X2) (global (indt «bool»)) X1 /* suspended on X2, X1 */

Here Bo2 is obtained by taking Bo1, considering all unification variables as holes and all {{ Type }} levels as fresh (the are none in this example), and running Coq's elaborator on it.

diff --git a/tutorial_coq_elpi_command.html b/tutorial_coq_elpi_command.html index e71c2ecad..2a230b43a 100644 --- a/tutorial_coq_elpi_command.html +++ b/tutorial_coq_elpi_command.html @@ -183,14 +183,13 @@

Defining commands

% main is, well, the entry point main Arguments :- coq.say "Hello" Arguments. -}}. -Elpi Typecheck.

The program declaration is made of 3 parts.

+}}.

The program declaration is made of 3 parts.

The first one Elpi Command hello. sets the current program to hello. Since it is declared as a Command some code is loaded automatically:

The second one Elpi Accumulate ... loads some extra code. @@ -204,10 +203,11 @@

Defining commands

Accumulating code via inline text or file is equivalent, the AST of code is stored in the .vo file (the external file does not need to be installed). We postpone the description of data bases to a dedicated section.

-

Once all the code is accumulated Elpi Typecheck verifies that the -code does not contain the most frequent kind of mistakes. This command -considers some mistakes minor and only warns about them. You can -pass -w +elpi.typecheck to coqc to turn these warnings into errors.

+

When some code is accumulated Elpi verifies that the +code does not contain the most frequent kind of mistakes, via some +type checking and linting. Some mistakes are minor and Elpi only warns about +them. You can pass -w +elpi.typecheck to coqc to turn these warnings into +errors.

We can now run our program!

Hello [str world!]

You should see the following output (hover the bubble next to the code if you are reading this online):

@@ -215,7 +215,7 @@

Defining commands

as (str "world!").

Note

-

coq.say won't print quotes around strings

+

coq.say won't print quotes around strings

@@ -264,7 +264,7 @@

Command arguments

the type of the record (which was omitted) defaults to Type. Finally note that the type of the second field sees c0 (the value of the first field).

-

See the argument data type +

See the argument data type for a detailed description of all the arguments a command can receive.

Processing raw arguments

@@ -282,8 +282,8 @@

Processing raw arguments

coq.say "The type of" T "is" Ty. }}. -Elpi Typecheck. +
The type of app [global (indt «eq»), global (indt «nat»), @@ -297,9 +297,9 @@

Processing raw arguments

"true" : "bool" The 3rd term has type "bool" which should be a subtype of "nat".

The command check_arg receives a term T and type checks it, then it prints the term and its type.

-

The coq.typecheck API has 3 arguments: a term, its type and a -diagnostic which can either be ok or (error Message). -The assert-ok! combinator checks if the diagnostic is ok, +

The coq.typecheck API has 3 arguments: a term, its type and a +diagnostic which can either be ok or (error Message). +The assert-ok! combinator checks if the diagnostic is ok, and if not it prints the error message and bails out.

The first invocation succeeds while the second one fails and prints the type checking error (given by Coq) following the string passed to @@ -315,10 +315,10 @@

Processing raw arguments

1 = true : Prop

The command still fails even if we told Coq how to inject booleans values into the natural numbers. Indeed the Check commands works.

-

The call to coq.typecheck modifies the term in place, it can assign +

The call to coq.typecheck modifies the term in place, it can assign implicit arguments (like the type parameter of eq) but it cannot modify the structure of the term. To do so, one has to use the -coq.elaborate-skeleton API.

+coq.elaborate-skeleton API.

#[arguments(raw)]
 Elpi Command elaborate_arg.
 Elpi Accumulate lp:{{
@@ -330,8 +330,8 @@ 
Processing raw arguments

     coq.say "Ty=" Ty.
 
 }}.
-Elpi Typecheck.
 
+
 
T= 
 app
  [global (indt «eq»), X0, app [global (indc «S»), global (indc «O»)], 
@@ -356,8 +356,8 @@ 
Examples

 
Synthesizing a term

 
Synthesizing a term typically involves reading an existing declaration
 and writing a new one. The relevant APIs are in the coq.env.* namespace
-and are named after the global reference they manipulate, eg coq.env.const
-for reading and coq.env.add-const for writing.

+and are named after the global reference they manipulate, eg coq.env.const
+for reading and coq.env.add-const for writing.

 
Here we implement a little command that given an inductive type name
 generates a term of type nat whose value is the number of constructors
 of the given inductive type.

@@ -377,8 +377,8 @@ 
Synthesizing a term

   coq.env.add-const Name Nnat _ _ _. % save it
 
 }}.
-Elpi Typecheck.
 
+
 Elpi constructors_num bool nK_bool.
 
nK_bool = 2
      : nat

@@ -389,20 +389,20 @@ 
Synthesizing a term

 
 
not an inductive type: coq.locate plus (indt X0)

 
Global reference not found: not_there

The command starts by locating the first argument and asserting it points to -an inductive type. This line is idiomatic: coq.locate aborts if +an inductive type. This line is idiomatic: coq.locate aborts if the string cannot be located, and if it relates it to a gref which is not -indt (for example const plus) assert! aborts with the given +indt (for example const plus) assert! aborts with the given error message.

-

coq.env.indt lets one access all the details of an inductive type, +

coq.env.indt lets one access all the details of an inductive type, here we just use the list of constructors. -The twin API coq.env.indt-decl lets +The twin API coq.env.indt-decl lets one access the declaration of the inductive in HOAS form, which might be easier to manipulate in other situations, like the next example.

Then the program crafts a natural number and declares a constant for it.

Abstracting an inductive

-

For the sake of introducing copy, the swiss army knife of λProlog, we +

For the sake of introducing copy, the swiss army knife of λProlog, we write a command which takes an inductive type declaration and builds a new one abstracting the former one on a given term. The new inductive has a parameter in place of the occurrences of that term.

@@ -427,11 +427,11 @@

Abstracting an inductive

% let's start to craft the new declaration by putting a % parameter A which has the type of P - NewDecl = parameter "A" explicit PTy Decl', + (NewDecl : indt-decl) = parameter "A" explicit PTy Decl', % let's make a copy, capturing all occurrences of P with a % (which stands for the parameter) - (pi a\ copy P a => copy-indt-decl Decl (Decl' a)), + (pi a\ copy P a ==> copy-indt-decl Decl (Decl' a)), % to avoid name clashes, we rename the type and its constructors % (we don't need to rename the parameters) @@ -447,8 +447,8 @@

Abstracting an inductive

coq.env.add-indt DeclRenamed _. }}. -Elpi Typecheck. + Inductive tree := leaf | node : tree -> option nat -> tree -> tree. Elpi abstract tree (option nat). @@ -459,7 +459,7 @@

Abstracting an inductive

Arguments tree' A%type_scope Arguments leaf' A%type_scope Arguments node' A%type_scope _ _ _

As expected tree' has a parameter A.

-

Now let's focus on copy. The standard +

Now let's focus on copy. The standard coq library (loaded by the command template) contains a definition of copy for terms and declarations.

An excerpt:

@@ -481,34 +481,34 @@

Abstracting an inductive

copy (app [global (indt «option»), global (indt «nat»)]) c0

and that rule masks the one for app when the sub-term being copied is -exactly option nat. The API copy-indt-decl copies an inductive +exactly option nat. The API copy-indt-decl copies an inductive declaration and calls copy on all the terms it contains (e.g. the type of the constructors).

-

The copy predicate is very flexible, but sometimes one needs to collect -some data along the way. The sibling API fold-map lets one do that.

+

The copy predicate is very flexible, but sometimes one needs to collect +some data along the way. The sibling API fold-map lets one do that.

An excerpt:

 fold-map (fun N T F) A (fun N T1 F1) A2 :-
   fold-map T A T1 A1, pi x\ fold-map (F x) A1 (F1 x) A2.
-

For example one can use fold-map to collect into a list all the occurrences +

For example one can use fold-map to collect into a list all the occurrences of inductive type constructors in a given term, then use the list to postulate -the right number of binders for them, and finally use copy to capture them.

+the right number of binders for them, and finally use copy to capture them.

Using DBs to store data across calls

A Db can be created with the command:

-
Elpi Db name.db lp:{{ some code. }}.

and a Db can be later extended via Elpi Accumulate. +

Elpi Db name.db lp:{{ pred some-pred. }}.

and a Db can be later extended via Elpi Accumulate. As a convention, we like Db names to end in a .db suffix.

A Db is pretty much like a regular program but can be shared among other programs and is accumulated by name. Since is a Db is accumulated when a program runs the current contents of the Db are used. Moreover the Db can be extended by Elpi programs themselves -thanks to the API coq.elpi.accumulate, enabling code to save a state +thanks to the API coq.elpi.accumulate, enabling code to save a state which is then visible at subsequent runs.

-

The initial contents of a Db, some code in the example +

The initial contents of a Db, pred some-pred. in the example above, is usually just the type declaration for the predicates part of the Db, and maybe a few default rules. Let's define a Db.

@@ -534,8 +534,8 @@

Using DBs to store data across ca coq.say Name "is" A "years old". }}. -Elpi Typecheck. +
I don't know who bob is!

Let's put some data in the Db. Given that the Db contains a catch-all rule, we need the new ones to be put before it.

Elpi Accumulate age.db lp:{{
@@ -547,7 +547,7 @@ 
Using DBs to store data across ca
 
 
bob is 24 years old

Extending data bases this way is fine, but requires the user of our command to be familiar with Elpi's syntax, which is not very nice. Instead, -we can write a new program that uses the coq.elpi.accumulate API +we can write a new program that uses the coq.elpi.accumulate API to extend the Db.

Elpi Command set_age.
 Elpi Accumulate Db age.db.
@@ -558,16 +558,16 @@ 
Using DBs to store data across ca
       (clause _ (before "age.fail") TheNewRule).
 
 }}.
-Elpi Typecheck.
 
+
 Elpi set_age "alice" 21.
 
alice is 21 years old

Additions to a Db are a Coq object, a bit like a Notation or a Type Class instance: these object live inside a Coq module (or a Coq file) and become active when that module is Imported.

Deciding to which Coq module these -extra rules belong is important and coq.elpi.accumulate provides +extra rules belong is important and coq.elpi.accumulate provides a few options to tune that. Here we passed _, that uses the default -setting. See the scope and clause data types for more info.

+setting. See the scope and clause data types for more info.

Inspecting a Db

So far we did query a Db but sometimes one needs to inspect the whole @@ -587,12 +587,12 @@

Using DBs to store data across ca print-rule (age P N) :- coq.say P "is" N "years old". }}. -Elpi Typecheck. -
bob is 24 years old
alice is 21 years old

The std.findall predicate gathers in a list all solutions to -a query, while std.forall iterates a predicate over a list. -It is important to notice that coq.error is a fatal error which + +

bob is 24 years old
alice is 21 years old

The std.findall predicate gathers in a list all solutions to +a query, while std.forall iterates a predicate over a list. +It is important to notice that coq.error is a fatal error which aborts an Elpi program. Here we shadow the catch all clause with a regular -failure so that std.findall can complete to list all the results.

+failure so that std.findall can complete to list all the results.

@@ -614,15 +614,15 @@

Attributes

This command does not support these attributes: more, this. [unsupported-attributes,parsing,default]
[attribute elpi.loc - (leaf-loc File "(stdin)", line 10, column 31, character 175:), + (leaf-loc File "(stdin)", line 10, column 31, characters 175-179:), attribute elpi.phase (leaf-str interp), attribute this (leaf-str ), attribute more (node [attribute stuff (leaf-str 33)])]

The first attribute, elpi.loc is always present and corresponds to the location in the source file of the command. Then we find an attribute for "this" holding the empty string and an attribute for "more.stuff" holding the string "33".

Attributes are usually validated (parsed) and turned into regular options -using coq.parse-attributes and a description of their types using -the attribute-type data type:

+using coq.parse-attributes and a description of their types using +the attribute-type data type:

Elpi Command parse_attr.
 Elpi Accumulate lp:{{
 
@@ -637,13 +637,13 @@ 
Attributes

       att "more.stuff" int,
     ] Opts,
     coq.say "options=" Opts,
-    Opts => some-code.
+    Opts ==> some-code.
 
 }}.
 
 
This command does not support these attributes: more,
 this. [unsupported-attributes,parsing,default]
options= 
-[get-option elpi.loc File "(stdin)", line 19, column 31, character 358:, 
+[get-option elpi.loc File "(stdin)", line 19, column 31, characters 359-369:, 
  get-option elpi.phase interp, get-option this tt, get-option more.stuff 33]
33 tt

 
This command does not support this attribute: unknown.
 [unsupported-attributes,parsing,default]
Attribute unknown is not supported

Note that get-option links a string with a datum of type any, which means @@ -660,8 +660,8 @@

Extending the command grammarElpi to invoke them.

Elpi Command Say.
 Elpi Accumulate lp:{{ main [str S] :- coq.say S. }}.
-Elpi Typecheck.
 
+
 Elpi Export Say. (* extend the Coq command grammar *)
 
 
That is all folks!

Not yet...

@@ -675,8 +675,8 @@

Extending the command grammar_ :- coq.error "Parse error! Use: go <from> => <to> / <via>". }}. -Elpi Typecheck. -Elpi Export Go. + +Elpi Export Go.
going from source to target via plane
Parse error! Use: go <from> => <to> / <via>

@@ -686,8 +686,8 @@

Reporting errors

as the previous one.

Elpi Command bad.
 Elpi Accumulate lp:{{ main []. }}.
-Elpi Typecheck.
-Elpi Export bad.
+
+Elpi Export bad.
 
 
The elpi tactic/command bad failed without giving a
 specific error message. Please report this
@@ -695,10 +695,10 @@ 
Reporting errors

 error:

 
The elpi tactic/command bad failed without giving a
 specific error message. Please report this
-inconvenience to the authors of the program.
You should use the coq.error API or the assert! one
-to abort a program. There is a dedicated coq.ltac.fail API to abort
+inconvenience to the authors of the program.

You should use the coq.error API or the assert! one +to abort a program. There is a dedicated coq.ltac.fail API to abort tactics.

-

Warnings can be reported using the coq.warning which lets you +

Warnings can be reported using the coq.warning which lets you pick a name and category. In turn these can be used to disable or make fatal your warnings (as any other Coq warning).

@@ -738,8 +738,8 @@

Parsing and Execution

Elpi Accumulate lp:{{ main [const-decl Name Body _] :- coq.say "interp" Name ":=" Body. }}. -Elpi Typecheck. +
synterp x := some _
interp x := some (app [global (indc «S»), app [global (indc «S»), global (indc «O»)]])

This simple command has no real synterp action, one could safely remove @@ -759,8 +759,8 @@

Parsing and Execution

coq.locate "w" (const GR), coq.env.const GR (some {{ 3 }}) _. }}. -Elpi Typecheck. +
The command did perform no (more) actions during the parsing phase (aka synterp), while during the execution phase (aka interp) it tried to perform a @@ -779,8 +779,8 @@

Parsing and Execution

coq.locate-module M MP, coq.env.import-module MP. }}. -Elpi Typecheck. + Elpi import_module Notations.

Elpi reports a descriptive error message if actions affecting the parser are not declared in the synterp code of the command.

The command did perform no (more) actions during the
@@ -821,15 +821,15 @@ 
Parsing and Execution

     coq.env.end-module MP,
     coq.say "The module is" MP.
 }}.
-Elpi Typecheck.
 
-
The module is «tutorial_coq_elpi_command.Module91»

If the only data to be passed to the interp phase is the list of + +

The module is «tutorial_coq_elpi_command.Module14»

If the only data to be passed to the interp phase is the list of synterp actions, then a few APIs can come in handy. -The synterp phase has access to the API coq.synterp-actions +The synterp phase has access to the API coq.synterp-actions that lists the actions performed so far. The interp phase can use -coq.replay-synterp-action and coq.next-synterp-action to +coq.replay-synterp-action and coq.next-synterp-action to replay an action or peek the next one to be performed.

-

An excerpt of the synterp-action.

+

An excerpt of the synterp-action.

 % Action executed during the parsing phase (aka synterp)
 kind synterp-action type.
@@ -862,8 +862,8 @@ 
Parsing and Execution

   replay-missing.
 }}.
 
-Elpi Typecheck.
-
+
+
 Elpi put_inside 4 Definition foo (n : nat) := n + 2.
 
 
Box.Box.Box.Box.foo =
@@ -900,8 +900,8 @@ 
Parsing and Execution

     replay-missing.
   replay-missing.
 }}.
-Elpi Typecheck.
 
+
 Elpi mk_next_module.
 Elpi mk_next_module.
 Elpi mk_next_module.
diff --git a/tutorial_coq_elpi_tactic.html b/tutorial_coq_elpi_tactic.html
index 4be9ad5f5..362ec1f8b 100644
--- a/tutorial_coq_elpi_tactic.html
+++ b/tutorial_coq_elpi_tactic.html
@@ -189,14 +189,13 @@ 
Defining tactics

   solve (goal Ctx _Trigger Type Proof _) _ :-
     coq.say "Goal:" Ctx "|-" Proof ":" Type.
 
-}}.
-Elpi Typecheck.

The tactic declaration is made of 3 parts.

+}}.

The tactic declaration is made of 3 parts.

The first one Elpi Tactic show. sets the current program to show. Since it is declared as a Tactic some code is loaded automatically:

The second one Elpi Accumulate ... loads some extra code. @@ -211,12 +210,13 @@

Defining tactics

is stored in the .vo file (the external file does not need to be installed). We invite the reader to look up the description of data bases in the tutorial about commands.

-

Once all the code is accumulated Elpi Typecheck verifies that the -code does not contain the most frequent kind of mistakes. This command -considers some mistakes minor and only warns about them. You can -pass -w +elpi.typecheck to coqc to turn these warnings into errors.

-

The entry point for tactics is called solve which maps a goal -into a list of sealed-goal (representing subgoals).

+

When some code is accumulated Elpi verifies that the +code does not contain the most frequent kind of mistakes, via some +type checking and linting. Some mistakes are minor and Elpi only warns about +them. You can pass -w +elpi.typecheck to coqc to turn these warnings into +errors.

+

The entry point for tactics is called solve which maps a goal +into a list of sealed-goal (representing subgoals).

Tactics written in Elpi can be invoked by prefixing its name with elpi.

x, y: nat
x + 1 = y

 
Goal: 
@@ -252,15 +252,15 @@ 
Defining tactics

 
The _Trigger component, which we did not print, is a variable that, when
 assigned, triggers the elaboration of its value against the type of the goal
 and obtains a value for Proof this way.

-
Keeping in mind that the solve predicate relates one goal to a list of
+
Keeping in mind that the solve predicate relates one goal to a list of
 subgoals, we implement our first tactic which blindly tries to solve the goal.

 
Elpi Tactic blind.
 Elpi Accumulate lp:{{
   solve (goal _ Trigger _ _ _) [] :- Trigger = {{0}}.
   solve (goal _ Trigger _ _ _) [] :- Trigger = {{I}}.
 }}.
-Elpi Typecheck.
 
+
 
(True * nat)%type

 Proof.
 
True
nat

@@ -278,20 +278,20 @@ 
Integration with Ltac

 
For a simple tactic like blind the list of subgoals is easy to write, since
 it is empty, but in general one should collect all the holes in
 the value of Proof (the checked proof term) and build goals out of them.

-
There is a family of APIs named after refine, the mother of all
+
There is a family of APIs named after refine, the mother of all
 tactics, in 
 elpi-ltac.elpi
 which does this job for you.

 
Usually a tactic builds a (possibly partial) term and calls
-refine on it.

+refine on it.

 
Let's rewrite the blind tactic using this schema.

 
Elpi Tactic blind2.
 Elpi Accumulate lp:{{
   solve G GL :- refine {{0}} G GL.
   solve G GL :- refine {{I}} G GL.
 }}.
-Elpi Typecheck.
 
+
 
(True * nat)%type

 Proof.
 
True
nat

@@ -330,8 +330,8 @@ 
Integration with Ltac

     % error that cannot be caught by Ltac combinators like repeat.
     coq.ltac.fail _ "not a conjunction".
 }}.
-Elpi Typecheck.
 
+
 
exists t : Prop, True /\ True /\ t

 Proof.
 
True /\ True /\ ?t

@@ -348,7 +348,7 @@ 
Integration with Ltac

 its type nat is not of sort Prop, so it backtracks and picks {{I}}.

 
Another common way to build an Elpi tactic is to synthesize a term and
 then call some Ltac piece of code finishing the work.

-
The API coq.ltac.call invokes some Ltac piece
+
The API coq.ltac.call invokes some Ltac piece
 of code passing to it the desired
 arguments. Then it builds the list of subgoals.

 
Here we pass an integer, which in turn is passed to fail, and a term,
@@ -362,8 +362,8 @@ 
Integration with Ltac

   solve _ _ :-
     coq.ltac.fail _ "not a conjunction".
 }}.
-Elpi Typecheck.
 
+
 
exists t : Prop, True /\ True /\ t

 Proof.
 
True /\ True /\ ?t

@@ -381,8 +381,8 @@ 
Arguments and Tactic Notation
 Elpi Accumulate lp:{{
   solve (goal _ _ _ _ Args) _ :- coq.say Args.
 }}.
-Elpi Typecheck.
 
+
 Lemma test_print_args : True.
 
[int 1, str x, str a b, 
  trm
@@ -396,13 +396,13 @@ 
Arguments and Tactic Notation
 
Important

 
terms are received in raw format, eg before elaboration

 
Indeed the type argument to eq is a variable.
-One can use APIs like coq.elaborate-skeleton to infer holes like
+One can use APIs like coq.elaborate-skeleton to infer holes like
 X0.

 

-
See the argument data type
+
See the argument data type
 for a detailed description of all the arguments a tactic can receive.

-
Now let's write a tactic which behaves pretty much like the refine
-one from Coq, but prints what it does using the API coq.term->string.

+
Now let's write a tactic which behaves pretty much like the refine
+one from Coq, but prints what it does using the API coq.term->string.

 
Elpi Tactic refine.
 Elpi Accumulate lp:{{
   solve (goal _ _ Ty _ [trm S] as G) GL :-
@@ -419,8 +419,8 @@ 
Arguments and Tactic Notation
     Msg is {coq.term->string S} ^ " does not fit",
     coq.ltac.fail _ Msg.
 }}.
-Elpi Typecheck.
 
+
 
P, Q: Prop
H: P -> Q
Q

 Proof.
 
Tactic failure: H does not fit.
P, Q: Prop
H: P -> Q
Q

@@ -464,14 +464,14 @@ 
Ltac arguments to Elpi arguments<
 

 

 
Failure

-
The coq.error aborts the execution of both
+
The coq.error aborts the execution of both
 Elpi and any enclosing Ltac context. This failure cannot be caught
 by Ltac.

-
On the contrary the coq.ltac.fail builtin can be used to
+
On the contrary the coq.ltac.fail builtin can be used to
 abort the execution of Elpi code in such a way that Ltac can catch it.
 This API takes an integer akin to Ltac's fail depth together with
 the error message to be displayed to the user.

-
Library functions of the assert! family call, by default, coq.error.
+
Library functions of the assert! family call, by default, coq.error.
 The flag @ltacfail! N can be set to alter this behavior and turn errors into
 calls to coq.ltac.fail N.

 
Elpi Tactic abort.
@@ -500,7 +500,7 @@ 
Examples

 
Let's code assumption in Elpi

 
assumption is a very simple tactic: we look up in the proof
 context for an hypothesis which unifies with the goal.
-Recall that Ctx is made of decl and def
+Recall that Ctx is made of decl and def
 (here, for simplicity, we ignore the latter case).

 
Elpi Tactic assumption.
 Elpi Accumulate lp:{{
@@ -511,8 +511,8 @@ 
Let's code _ _ :-
     coq.ltac.fail _ "no such hypothesis".
 }}.
-Elpi Typecheck.
 
+
 
P, Q: Prop
p: P
q: Q
P /\ id Q

 Proof.
 
P, Q: Prop
p: P
q: Q
P
P, Q: Prop
p: P
q: Q
id Q

@@ -522,9 +522,9 @@ 
Let's code Q but the goal has type id Q which is
 convertible (unifiable, for Coq's unification) to Q.

 
Let's improve our tactic by looking for an assumption which is unifiable with
-the goal, and not just alpha convertible. The coq.unify-leq
+the goal, and not just alpha convertible. The coq.unify-leq
 calls Coq's unification for types (on which cumulativity applies, hence the
--leq suffix). The std.mem utility, thanks to backtracking,
+-leq suffix). The std.mem utility, thanks to backtracking,
 eventually finds an hypothesis that satisfies the following predicate
 (ie unifies with the goal).

 
Elpi Tactic assumption2.
@@ -536,13 +536,13 @@ 
Let's code _ _ :-
     coq.ltac.fail _ "no such hypothesis".
 }}.
-Elpi Typecheck.
 
+
 
P, Q: Prop
p: P
q: Q
P /\ id Q

 Proof.
 
P, Q: Prop
p: P
q: Q
P
P, Q: Prop
p: P
q: Q
id Q

 all: elpi assumption2.
-Qed.
refine does unify the type of goal with the type of the term,
+Qed.
refine does unify the type of goal with the type of the term,
 hence we can simplify the code further. We obtain a
 tactic very similar to our initial blind tactic, which picks
 candidates from the context rather than from the program itself.

@@ -554,8 +554,8 @@ 
Let's code _ _ :-
     coq.ltac.fail _ "no such hypothesis".
 }}.
-Elpi Typecheck.
 
+
 
P, Q: Prop
p: P
q: Q
P /\ id Q

 Proof.
 
P, Q: Prop
p: P
q: Q
P
P, Q: Prop
p: P
q: Q
id Q

@@ -565,19 +565,19 @@ 
Let's code Let's code set in Elpi

 
The set tactic takes a term, possibly with holes, and
 makes a let-in out of it.

-
It gives us the occasion to explain the copy utility.

+
It gives us the occasion to explain the copy utility.

 
Elpi Tactic find.
 Elpi Accumulate lp:{{
 
 solve (goal _ _ T _ [trm X]) _ :-
   pi x\
-    copy X x => copy T (Tabs x),
+    (copy X x ==> copy T (Tabs x)),
     if (occurs x (Tabs x))
        (coq.say "found" {coq.term->string X})
        (coq.ltac.fail _ "not found").
 }}.
-Elpi Typecheck.
 
+
 
P, Q: Prop
P /\ P \/ P /\ Q

 Proof.
 
found P
P, Q: Prop
P /\ P \/ P /\ Q

@@ -585,7 +585,7 @@ 
Let's code 
found P /\ P
P, Q: Prop
P /\ P \/ P /\ Q

 Abort.
This first approximation only prints the term it found, or better the first
 instance of the given term.

-
Now lets focus on copy. An excerpt:

+
Now lets focus on copy. An excerpt:

 
 copy X X :- name X.     % checks X is a bound variable
 copy (global _ as C) C.
@@ -603,7 +603,7 @@ 
Let's code 
 copy (app [global (indt «andn»), sort prop, sort prop, c0, X0 c0 c1]) c2
 

-
and that rule masks the one for app when the 
+
and that rule masks the one for app when the 
 sub-term being copied matches (P /\ _). The first time this rule
 is used X0 is assigned, making the rule represent the term (P /\ P).

 
Now let's refine the tactic to build a let-in, and complain if the
@@ -613,7 +613,7 @@ 
Let's code _ _ T _ [str ID, trm X] as G) GL :-
   pi x\
-    copy X x => copy T (Tabs x),
+    (copy X x ==> copy T (Tabs x)),
     if (occurs x (Tabs x))
        (if (coq.ltac.id-free? ID G) true
            (coq.warn ID "is already taken, Elpi will make a name up"),
@@ -623,8 +623,8 @@ 
Let's code _ "not found").
 
 }}.
-Elpi Typecheck.
 
+
 
P, Q: Prop
P /\ P \/ P /\ Q

 Proof.
 
P, Q: Prop
x:= P: Prop
x /\ x \/ x /\ Q

@@ -650,8 +650,8 @@ 
Let's code }}.
-Elpi Typecheck.
 
+
 
x: nat
x + 1 = 0

 
Goal: [decl c0 `x` (global (indt «nat»))] |- X0 c0 : 
 app
@@ -720,9 +720,9 @@ 
Let's code X1 some procedure to
 turn that value into X0 is triggered. That procedure is called
 elaboration and it is currently implemented by calling the
-coq.elaborate-skeleton API.

+coq.elaborate-skeleton API.

 
Given this set up, it is impossible to use a term of the wrong type as a
-Proof. Let's rewrite the split tactic without using refine.

+Proof. Let's rewrite the split tactic without using refine.

 
Elpi Tactic split_ll.
 Elpi Accumulate lp:{{
   solve (goal Ctx Trigger {{ lp:A /\ lp:B }} Proof []) GL :- !,
@@ -734,8 +734,8 @@ 
Let's code _ _ :-
     coq.ltac.fail _ "not a conjunction".
 }}.
-Elpi Typecheck.
 
+
 
exists t : Prop, True /\ True /\ t

 Proof.
 
True /\ True /\ ?t

@@ -744,9 +744,9 @@ 
Let's code Qed.
Crafting by hand the list of subgoal is not easy.
 In particular here we did not set up the new trigger for Pa and Pb,
 nor seal the goals appropriately (we did not bind proof variables).

-
The coq.ltac.collect-goals API helps us doing this.

+
The coq.ltac.collect-goals API helps us doing this.

 
Elpi Tactic split_ll_bis.
-Elpi Accumulate lp:{{
+
At the light of that, refine is simply:

+Qed.
At the light of that, refine is simply:

 
 refine T (goal _ RawEv _ Ev _) GS :-
   RawEv = T, coq.ltac.collect-goals Ev GS _.
 

-
Now that we know the low level plumbing, we can use refine ;-)

+
Now that we know the low level plumbing, we can use refine ;-)

 
The only detail we still have to explain is what exactly a
-sealed-goal is. A sealed goal wraps into a single object all
+sealed-goal is. A sealed goal wraps into a single object all
 the proof variables and the assumptions about them, making this object easy
 (or better, sound) to pass around.

 

@@ -784,9 +787,9 @@ 
multi-goal tactics

 
  • if the tactic is a multi-goal one, it will receive all goals
    • 
 
 
    In Elpi you can implement a multi-goal tactic by providing a rule for
-the msolve predicate. Since such a tactic will need to manipulate
+the msolve predicate. Since such a tactic will need to manipulate
 multiple goals, potentially living in different proof context, it receives
-a list of sealed-goal, a data type which seals a goal and
+a list of sealed-goal, a data type which seals a goal and
 its proof context.
    
 
    Elpi Tactic ngoals.
 Elpi Accumulate lp:{{
@@ -796,8 +799,8 @@ 
    multi-goal tactics
    
     coq.say GL.
 
 }}.    
-    Elpi Typecheck.
 
+
 
    P, Q: Prop
    P /\ Q
    
     Proof.
 
    P, Q: Prop
    P
    P, Q: Prop
    Q
    
@@ -822,9 +825,9 @@ 
    multi-goal tactics
    
   nabla c1 \
    seal
     (goal [decl c1 `Q` (sort prop), decl c0 `P` (sort prop)] (X2 c0 c1) c1 
-      (X3 c0 c1) [])]
    nabla binds all proof variables, then seal
+      (X3 c0 c1) [])]
    nabla binds all proof variables, then seal
 holds a regular goal, which in turn carries the proof context.
    
-
    In order to operate inside a goal one can use the coq.ltac.open utility,
+
    In order to operate inside a goal one can use the coq.ltac.open utility,
 which postulates all proof variables using pi x\  and loads the proof
 context using =>.
    
 
    Operating on multiple goals at the same time is doable, but not easy.
@@ -833,7 +836,7 @@ 
    multi-goal tactics
    
 removing duplicates. As one can see, there is much room for improvement
 in the same-ctx predicate.
    
 
    Elpi Tactic undup.
-Elpi Accumulate lp:{{
+
-
    G2 is linear: name it _G2 (discard) or G2_ (fresh variable)
-[elpi.typecheck,elpi,default]
    G1 is linear: name it _G1 (discard) or G1_ (fresh variable)
-[elpi.typecheck,elpi,default]
    
+}}.
    Toplevel input, characters 252-253
+G1 is linear: name it _G1 (discard) or G1_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
    Toplevel input, characters 300-301
+G2 is linear: name it _G2 (discard) or G2_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
    
     
+
 
    P, Q: Prop
    p: P
    q: Q
    P /\ Q /\ P
    
     Proof.
 
    P, Q: Prop
    p: P
    q: Q
    P
    P, Q: Prop
    p: P
    q: Q
    Q
    P, Q: Prop
    p: P
    q: Q
    P
    
@@ -877,13 +882,13 @@ 
    multi-goal tactics
    
  conj ?Goal (conj ?Goal0 ?Goal1))
    
 
    P, Q: Prop
    p: P
    q: Q
    P
    P, Q: Prop
    p: P
    q: Q
    Q
    
 
    (fun (P Q : Prop) (p : P) (q : Q) =>
- conj ?Goal (conj ?Goal0 ?Goal))
    
+ conj ?Goal0 (conj ?Goal ?Goal0))
    P, Q: Prop
    p: P
    q: Q
    P
         apply p.
    P, Q: Prop
    p: P
    q: Q
    Q
         apply q. Qed.

    The two calls to show proof display, respectively:

    (fun (P Q : Prop) (p : P) (q : Q) =>
  conj ?Goal (conj ?Goal0 ?Goal1))
    (fun (P Q : Prop) (p : P) (q : Q) =>
- conj ?Goal (conj ?Goal0 ?Goal))

    the proof term is the same but for the fact that after the tactic the first + conj ?Goal0 (conj ?Goal ?Goal0))

    the proof term is the same but for the fact that after the tactic the first and last missing subterm (incomplete proof tree branch) are represented by the same hole ?Goal0. Indeed by solving one, we can also solve the other.

    @@ -897,7 +902,7 @@

    LCF tacticals

    A few tacticals can be found in the elpi-ltac.elpi file. -For example this is the code of try:

    +For example this is the code of try:

     pred try i:tactic, i:sealed-goal, o:list sealed-goal.
 try T G GS :- T G GS.
@@ -940,8 +945,8 @@ 
    Setting arguments for a tactic]) SG GL.
 
 }}.
-Elpi Typecheck.
 
+
 
    P: Prop
    P -> P
    
     Proof.
 elpi argpass.
@@ -950,9 +955,9 @@ 
    Setting arguments for a tactic
 thenl [ open (tac1 Datum), open (tac2 Datum) ]
    -

    but the binder structure of sealed-goal would prevent Datum +

    but the binder structure of sealed-goal would prevent Datum to mention proof variables, that would otherwise escape the sealing.

    -

    The utility set-goal-arguments:

    +

    The utility set-goal-arguments:

     coq.ltac.set-goal-arguments Args G G1 G1wArgs
    @@ -983,8 +988,8 @@

    Tactics in terms

    refine P G GL. }}. -Elpi Typecheck. -Elpi Export default. + +Elpi Export default. Definition foo : nat := default.
    foo = 46 @@ -1003,8 +1008,8 @@

    Tactics in terms

    default T MaxI P, refine P G GL. }}. -Elpi Typecheck. +
    [Loading ML file zify_plugin.cmxs (using legacy method) ... done]
    [Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
    [Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
    [Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
         Open Scope uint63_scope. diff --git a/tutorial_elpi_lang.html b/tutorial_elpi_lang.html index 6f489dd24..ab4a71ac1 100644 --- a/tutorial_elpi_lang.html +++ b/tutorial_elpi_lang.html @@ -174,7 +174,7 @@

    Tutorial on the Elpi programming language

  • Good old print
  • Printing entire programs
  • Common pitfalls @@ -218,8 +218,8 @@

    Logic programming

    is a mode declaration, which we will explain later (ignore it for now).

    Note

    -

    int is the built-in data type of integers

    -

    Integers come with usual arithmetic operators, see the calc built-in.

    +

    int is the built-in data type of integers

    +

    Integers come with usual arithmetic operators, see the calc built-in.

    In order to run our program we have to write a query, i.e. a predicate expression containing variables such as:

    @@ -247,14 +247,14 @@

    Logic programming

    age alice A, coq.say "The age of alice is" A -}}.
    The age of alice is 20
    Query assignments:
    A = 20

    coq.say is a built-in predicate provided by Coq-Elpi which +}}.

    The age of alice is 20
    Query assignments:
    A = 20

    coq.say is a built-in predicate provided by Coq-Elpi which prints its arguments. You can look at the output buffer of Coq to see the value for A or hover or toggle the little bubble after }}. if you are reading the tutorial with a web browser.

    Note

    -

    string is a built-in data type

    +

    string is a built-in data type

    Strings are delimited by double quotes and \ is the escape symbol.

    The predicate age represents a relation (in contrast to a function) @@ -541,7 +541,9 @@

    λ-abstraction

    Omega = app Delta Delta, whd Omega Hummm, coq.say "not going to happen" -}}.
    elpi run out of steps (1000)
     +}}.
    Toplevel input, characters 138-142 +Hummm is linear: name it _Hummm (discard) or Hummm_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
    elpi run out of steps (1000)
         Elpi Bound Steps 0.

    • pi x\ and =>

    @@ -569,15 +571,15 @@

    Hd (arr A B), of Arg A. % for lambda, instead of using a context (a list) of bound - % variables we use pi and => , explained below + % variables we use pi and ==> , explained below of (fun F) (arr A B) :- - pi x\ of x A => of (F x) B. + pi x\ of x A ==> of (F x) B. }}.

    The pi name\ code syntax is reserved, as well as -rule => code.

    +rule ==> code.

    Operationally pi x\ code introduces a fresh constant c for x and then runs code. -Operationally rule => code adds rule to +Operationally rule ==> code adds rule to the program and runs code. Such extra rule is said to be hypothetical. Both the constant for x and rule are @@ -627,7 +629,9 @@

    Delta = fun (x\ app x x), (of Delta Ty ; coq.say "Error:" Delta "has no type") -}}.
    Error: fun c0 \ app c0 c0 has no type
    Query assignments:
    Delta = fun c0 \ app c0 c0
    Ty = X0

    The ; infix operator stands for disjunction. Since we see the message +}}.

    Toplevel input, characters 59-60 +Ty is linear: name it _Ty (discard) or Ty_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
    Error: fun c0 \ app c0 c0 has no type
    Query assignments:
    Delta = fun c0 \ app c0 c0
    Ty = X0

    The ; infix operator stands for disjunction. Since we see the message of failed: the term fun (x\ app x x) is not well typed.

    First, the rule for elpi:fun is selected:

      @@ -687,7 +691,7 @@

      A rule like:

       of (fun F) (arr A B) :-
-  pi x\ of x A => of (F x) B.
+  pi x\ of x A ==> of (F x) B.

      reads, as a logical formula:

      @@ -749,7 +753,11 @@

      Modes and constraints

      order of the rules for add Elpi can either diverge or pick z as a value for X (that may not be what one wants)

      Elpi Bound Steps 100.
-
      elpi run out of steps (100)
      
+
      Toplevel input, characters 49-49
+X is linear: name it _X (discard) or X_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 57-57
+Y is linear: name it _Y (discard) or Y_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      elpi run out of steps (100)
      
       Elpi Bound Steps 0.

      Indeed the first rule for add can be applied forever. If one exchanges the two rules in the program, then Elpi terminates picking z for X.

      @@ -771,7 +779,11 @@

      Modes and constraints

      }}. -
      nothing matched but for this catch all clause!

      The query fails because no rule first argument matches X.

      +
      Toplevel input, characters 256-256 +X is linear: name it _X (discard) or X_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 264-264 +Y is linear: name it _Y (discard) or Y_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
      nothing matched but for this catch all clause!

      The query fails because no rule first argument matches X.

      Instead of failing we can suspend goals and turn them into syntactic constraints

      Elpi Program peano3 lp:{{
@@ -795,7 +807,11 @@ 
      Modes and constraints
      
 
 }}.      
       
-
      Query assignments:
      X = X0
      Z = X1
      Syntactic constraints:
+
      Toplevel input, characters 480-480
+X is linear: name it _X (discard) or X_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 488-488
+Z is linear: name it _Z (discard) or Z_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Query assignments:
      X = X0
      Z = X1
      Syntactic constraints:
  sum X0 (s z) X1  /* suspended on X0 */

      Syntactic constraints are resumed when the variable they are suspended on is assigned:

      Note

      variables (capital letters) can be used in types in order to describe ML-like polymorphism.

      @@ -920,26 +938,28 @@

      Spilling (relation composition)< make-palindrome2 [1,2,3] A -}}.
      Query assignments:
      A = [1, 2, 3, 3, 2, 1]

      The two versions of make-palindrome are equivalent. +}}.

      Toplevel input, characters 182-182 +A is linear: name it _A (discard) or A_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
      Query assignments:
      A = [1, 2, 3, 3, 2, 1]

      The two versions of make-palindrome are equivalent. Actually the latter is elaborated into the former.

      APIs for built-in data

      Functions about built-in data types are available via the -calc predicate or its infix version is. Example:

      +calc predicate or its infix version is. Example:

      result = 5
      Query assignments:
      X = result =
      Y = 5

      The calc predicate works nicely with spilling:

      -
      result = 5
      Query assignments:
      Spilled_1 = 5
      +}}.
      result = 5
      Query assignments:
      X = result =
      Y = 5

      The calc predicate works nicely with spilling:

      +
      result = 5
      Query assignments:
      %arg1 = 5

      Allocation of variables

      The language let's one use λ-abstraction also to write anonymous rules but one has to be wary of where variables are bound (allocated really).

      -

      In our example we use the higher order predicate std.map:

      +

      In our example we use the higher order predicate std.map:

       pred std.map i:list A, i:(A -> B -> prop), o:list B.
      @@ -982,8 +1002,14 @@

      Allocation of variables

      good [1,2,3] R2, good2 [1,2,3] R3 -}}.
      Query assignments:
      R1 = X0
      R2 = [2, 3, 4]
      R3 = [2, 3, 4]

      The problem with bad is that TMP is fresh each time the rule -is used, but not every time the anonymous rule passed to map +}}.

      Toplevel input, characters 401-402 +R1 is linear: name it _R1 (discard) or R1_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 421-422 +R2 is linear: name it _R2 (discard) or R2_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 441-442 +R3 is linear: name it _R3 (discard) or R3_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
      Query assignments:
      R1 = X0
      R2 = [2, 3, 4]
      R3 = [2, 3, 4]

      The problem with bad is that TMP is fresh each time the rule +is used, but not every time the anonymous rule passed to map is used. Technically TMP is quantified (allocated) where L and Result are.

      There are two ways to quantify TMP correctly, that is inside the @@ -1002,7 +1028,7 @@

      Allocation of variables

      pred good3 i:list int, o:list int. good3 L Result :- pi aux\ - (pi TMP X R\ aux X R :- TMP is X + 1, R = TMP) => + (pi TMP X R\ aux X R :- TMP is X + 1, R = TMP) ==> std.map L aux Result. }}. @@ -1011,7 +1037,9 @@

      Allocation of variables

      good3 [1,2,3] R -}}.
      Query assignments:
      R = [2, 3, 4]

      In this case the auxiliary predicate aux +}}.

      Toplevel input, characters 208-208 +R is linear: name it _R (discard) or R_ (fresh variable) +[elpi.linear-variable,elpi.typecheck,elpi,default]
      Query assignments:
      R = [2, 3, 4]

      In this case the auxiliary predicate aux is only visible inside good3. What is interesting to remark is that the quantifications are explicit in the hypothetical rule, and they indicate clearly that each and every @@ -1029,10 +1057,10 @@

      Allocation of variables

      Tip

      => can load more than one clause at once

      -

      It is sufficient to put a list on the left hand side, eg [ rule1, rule2 ] => code. +

      It is sufficient to put a list on the left hand side, eg [ rule1, rule2 ] ==> code. Moreover one can synthesize a rule before loading it, eg:

      -Rules = [ one-more-rule | ExtraRules ], Rules => code
+Rules = [ one-more-rule | ExtraRules ], Rules ==> code

      The last remark worth making is that bound variables are intimately related @@ -1070,7 +1098,7 @@

      Allocation of variables

      λ-abstraction:

       of (fun F) (arr A B) :-
-  pi x\ of x A => of (F x) B.
+  pi x\ of x A ==> of (F x) B.

      we can see that the only unification variable that sees the fresh x is F, because we pass x to F explicitly @@ -1143,90 +1171,90 @@

      Trace browser

      of (fun (x\ fun y\ x)) Ty, coq.say Ty }}.
      run 1 {{{ -
      rid:0 step:1 gid:6 user:curgoal = , +
      rid:0 step:1 gid:4 user:curgoal = , of (fun c0 \ fun c1 \ c0) X0 , coq.say X0 -
      rid:0 step:1 gid:6 user:rule = and -
      rid:0 step:1 gid:6 user:subgoal = 7 -
      rid:0 step:1 gid:7 user:newgoal = of (fun c0 \ fun c1 \ c0) X0 -
      rid:0 step:1 gid:6 user:subgoal = 8 -
      rid:0 step:1 gid:8 user:newgoal = coq.say X0 -
      rid:0 step:1 gid:6 user:rule:and = success -
      }}} -> (0.001s)
      run 2 {{{ -
      rid:0 step:2 gid:7 user:curgoal = of +
      rid:0 step:1 gid:4 user:rule = and +
      rid:0 step:1 gid:4 user:subgoal = 5 +
      rid:0 step:1 gid:5 user:newgoal = of (fun c0 \ fun c1 \ c0) X0 +
      rid:0 step:1 gid:4 user:subgoal = 6 +
      rid:0 step:1 gid:6 user:newgoal = coq.say X0 +
      rid:0 step:1 gid:4 user:rule:and = success +
      }}} -> (0.000s)
      run 2 {{{ +
      rid:0 step:2 gid:5 user:curgoal = of of (fun c0 \ fun c1 \ c0) X0 -
      rid:0 step:2 gid:7 user:rule = backchain -
      rid:0 step:2 gid:7 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, character 459: +
      rid:0 step:2 gid:5 user:rule = backchain +
      rid:0 step:2 gid:5 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, characters 460-514:
      }}} -> (0.000s)
      select 3 {{{ -
      rid:0 step:2 gid:7 user:rule:backchain:try = File "(stdin)", line 15, column 3, character 459: - (of (fun A0) (arr A1 A2)) :- ( +
      rid:0 step:2 gid:5 user:rule:backchain:try = File "(stdin)", line 15, column 3, characters 460-514: + (of (fun A0) (arr A2 A1)) :- ( pi (c0 \ - (of c0 A1 => of (A0 c0) A2))). + (of c0 A2 => of (A0 c0) A1))).
      rid:0 step:2 gid:0 user:assign = A0 := c0 \ fun c1 \ c0
      rid:0 step:2 gid:0 user:assign = X0 := arr X1 X2 -
      rid:0 step:2 gid:7 user:subgoal = 9 -
      rid:0 step:2 gid:9 user:newgoal = pi c0 \ of c0 X1 => of (fun c1 \ c0) X2 -
      rid:0 step:2 gid:9 user:rule:backchain = success +
      rid:0 step:2 gid:5 user:subgoal = 7 +
      rid:0 step:2 gid:7 user:newgoal = pi c0 \ of c0 X1 => of (fun c1 \ c0) X2 +
      rid:0 step:2 gid:7 user:rule:backchain = success
      }}} -> (0.000s)
      run 3 {{{ -
      rid:0 step:3 gid:9 user:curgoal = pi +
      rid:0 step:3 gid:7 user:curgoal = pi pi c0 \ of c0 X1 => of (fun c1 \ c0) X2 -
      rid:0 step:3 gid:9 user:rule = pi -
      rid:0 step:3 gid:9 user:subgoal = 10 -
      rid:0 step:3 gid:10 user:newgoal = of c0 X1 => of (fun c1 \ c0) X2 -
      rid:0 step:3 gid:10 user:rule:pi = success +
      rid:0 step:3 gid:7 user:rule = pi +
      rid:0 step:3 gid:7 user:subgoal = 8 +
      rid:0 step:3 gid:8 user:newgoal = of c0 X1 => of (fun c1 \ c0) X2 +
      rid:0 step:3 gid:8 user:rule:pi = success
      }}} -> (0.000s)
      run 4 {{{ -
      rid:0 step:4 gid:10 user:curgoal = => - of c0 X1 => of (fun c1 \ c0) X2 -
      rid:0 step:4 gid:10 user:rule = implication -
      rid:0 step:4 gid:10 user:subgoal = 11 -
      rid:0 step:4 gid:11 user:newgoal = of (fun c1 \ c0) X2 -
      rid:0 step:4 gid:11 user:rule:implication = success +
      rid:0 step:4 gid:8 user:curgoal = => + of c0 X1 => of (fun c1 \ c0) X2 +
      rid:0 step:4 gid:8 user:rule = implication +
      rid:0 step:4 gid:8 user:subgoal = 9 +
      rid:0 step:4 gid:9 user:newgoal = of (fun c1 \ c0) X2 +
      rid:0 step:4 gid:9 user:rule:implication = success
      }}} -> (0.000s)
      run 5 {{{ -
      rid:0 step:5 gid:11 user:curgoal = of - of (fun c1 \ c0) X2 -
      rid:0 step:5 gid:11 user:rule = backchain -
      rid:0 step:5 gid:11 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, character 459: +
      rid:0 step:5 gid:9 user:curgoal = of + of (fun c1 \ c0) X2 +
      rid:0 step:5 gid:9 user:rule = backchain +
      rid:0 step:5 gid:9 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, characters 460-514:
      }}} -> (0.000s)
      select 4 {{{ -
      rid:0 step:5 gid:11 user:rule:backchain:try = File "(stdin)", line 15, column 3, character 459: - (of (fun A0) (arr A1 A2)) :- ( - pi (c0 \ - (of c0 A1 => of (A0 c0) A2))). +
      rid:0 step:5 gid:9 user:rule:backchain:try = File "(stdin)", line 15, column 3, characters 460-514: + (of (fun A0) (arr A2 A1)) :- ( + pi (c0 \ + (of c0 A2 => of (A0 c0) A1))).
      rid:0 step:5 gid:0 user:assign = A0 := c1 \ c0
      rid:0 step:5 gid:0 user:assign = X2 := arr X3 X4 -
      rid:0 step:5 gid:11 user:subgoal = 12 -
      rid:0 step:5 gid:12 user:newgoal = pi c1 \ of c1 X3 => of c0 X4 -
      rid:0 step:5 gid:12 user:rule:backchain = success +
      rid:0 step:5 gid:9 user:subgoal = 10 +
      rid:0 step:5 gid:10 user:newgoal = pi c1 \ of c1 X3 => of c0 X4 +
      rid:0 step:5 gid:10 user:rule:backchain = success
      }}} -> (0.000s)
      run 6 {{{ -
      rid:0 step:6 gid:12 user:curgoal = pi +
      rid:0 step:6 gid:10 user:curgoal = pi pi c1 \ of c1 X3 => of c0 X4 -
      rid:0 step:6 gid:12 user:rule = pi -
      rid:0 step:6 gid:12 user:subgoal = 13 -
      rid:0 step:6 gid:13 user:newgoal = of c1 X3 => of c0 X4 -
      rid:0 step:6 gid:13 user:rule:pi = success +
      rid:0 step:6 gid:10 user:rule = pi +
      rid:0 step:6 gid:10 user:subgoal = 11 +
      rid:0 step:6 gid:11 user:newgoal = of c1 X3 => of c0 X4 +
      rid:0 step:6 gid:11 user:rule:pi = success
      }}} -> (0.000s)
      run 7 {{{ -
      rid:0 step:7 gid:13 user:curgoal = => +
      rid:0 step:7 gid:11 user:curgoal = => of c1 X3 => of c0 X4 -
      rid:0 step:7 gid:13 user:rule = implication -
      rid:0 step:7 gid:13 user:subgoal = 14 -
      rid:0 step:7 gid:14 user:newgoal = of c0 X4 -
      rid:0 step:7 gid:14 user:rule:implication = success +
      rid:0 step:7 gid:11 user:rule = implication +
      rid:0 step:7 gid:11 user:subgoal = 12 +
      rid:0 step:7 gid:12 user:newgoal = of c0 X4 +
      rid:0 step:7 gid:12 user:rule:implication = success
      }}} -> (0.000s)
      run 8 {{{ -
      rid:0 step:8 gid:14 user:curgoal = of +
      rid:0 step:8 gid:12 user:curgoal = of of c0 X4 -
      rid:0 step:8 gid:14 user:rule = backchain -
      rid:0 step:8 gid:14 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:0 step:8 gid:12 user:rule = backchain +
      rid:0 step:8 gid:12 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, characters 0-0:
      }}} -> (0.000s)
      select 5 {{{ -
      rid:0 step:8 gid:14 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:0 step:8 gid:12 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, characters 0-0: (of c0 X1) :- .
      rid:0 step:8 gid:0 user:assign = X1 := X4 -
      rid:0 step:8 gid:14 user:rule:backchain = success +
      rid:0 step:8 gid:12 user:rule:backchain = success
      }}} -> (0.000s)
      run 9 {{{ -
      rid:0 step:9 gid:8 user:curgoal = coq.say +
      rid:0 step:9 gid:6 user:curgoal = coq.say coq.say (arr X4 (arr X3 X4)) -
      rid:0 step:9 gid:8 user:rule = builtin -
      rid:0 step:9 gid:8 user:rule:builtin:name = coq.say -
      arr X4 (arr X3 X4)
      rid:0 step:9 gid:8 user:rule:builtin = success +
      rid:0 step:9 gid:6 user:rule = builtin +
      rid:0 step:9 gid:6 user:rule:builtin:name = coq.say +
      arr X4 (arr X3 X4)
      rid:0 step:9 gid:6 user:rule:builtin = success
      }}} -> (0.000s)
      Query assignments:
      Ty = arr X4 (arr X3 X4)
      run 1 {{{ -
      rid:1 step:1 gid:15 user:curgoal = , +
      rid:1 step:1 gid:13 user:curgoal = , of (fun c0 \ app c0 c0) X0 , coq.say X0 -
      rid:1 step:1 gid:15 user:rule = and -
      rid:1 step:1 gid:15 user:subgoal = 16 -
      rid:1 step:1 gid:16 user:newgoal = of (fun c0 \ app c0 c0) X0 -
      rid:1 step:1 gid:15 user:subgoal = 17 -
      rid:1 step:1 gid:17 user:newgoal = coq.say X0 -
      rid:1 step:1 gid:15 user:rule:and = success +
      rid:1 step:1 gid:13 user:rule = and +
      rid:1 step:1 gid:13 user:subgoal = 14 +
      rid:1 step:1 gid:14 user:newgoal = of (fun c0 \ app c0 c0) X0 +
      rid:1 step:1 gid:13 user:subgoal = 15 +
      rid:1 step:1 gid:15 user:newgoal = coq.say X0 +
      rid:1 step:1 gid:13 user:rule:and = success
      }}} -> (0.000s)
      run 2 {{{ -
      rid:1 step:2 gid:16 user:curgoal = of +
      rid:1 step:2 gid:14 user:curgoal = of of (fun c0 \ app c0 c0) X0 -
      rid:1 step:2 gid:16 user:rule = backchain -
      rid:1 step:2 gid:16 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, character 459: +
      rid:1 step:2 gid:14 user:rule = backchain +
      rid:1 step:2 gid:14 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, characters 460-514:
      }}} -> (0.000s)
      select 3 {{{ -
      rid:1 step:2 gid:16 user:rule:backchain:try = File "(stdin)", line 15, column 3, character 459: - (of (fun A0) (arr A1 A2)) :- ( +
      rid:1 step:2 gid:14 user:rule:backchain:try = File "(stdin)", line 15, column 3, characters 460-514: + (of (fun A0) (arr A2 A1)) :- ( pi (c0 \ - (of c0 A1 => of (A0 c0) A2))). + (of c0 A2 => of (A0 c0) A1))).
      rid:1 step:2 gid:0 user:assign = A0 := c0 \ app c0 c0
      rid:1 step:2 gid:0 user:assign = X0 := arr X1 X2 -
      rid:1 step:2 gid:16 user:subgoal = 18 -
      rid:1 step:2 gid:18 user:newgoal = pi c0 \ of c0 X1 => of (app c0 c0) X2 -
      rid:1 step:2 gid:18 user:rule:backchain = success +
      rid:1 step:2 gid:14 user:subgoal = 16 +
      rid:1 step:2 gid:16 user:newgoal = pi c0 \ of c0 X1 => of (app c0 c0) X2 +
      rid:1 step:2 gid:16 user:rule:backchain = success
      }}} -> (0.000s)
      run 3 {{{ -
      rid:1 step:3 gid:18 user:curgoal = pi +
      rid:1 step:3 gid:16 user:curgoal = pi pi c0 \ of c0 X1 => of (app c0 c0) X2 -
      rid:1 step:3 gid:18 user:rule = pi -
      rid:1 step:3 gid:18 user:subgoal = 19 -
      rid:1 step:3 gid:19 user:newgoal = of c0 X1 => of (app c0 c0) X2 -
      rid:1 step:3 gid:19 user:rule:pi = success +
      rid:1 step:3 gid:16 user:rule = pi +
      rid:1 step:3 gid:16 user:subgoal = 17 +
      rid:1 step:3 gid:17 user:newgoal = of c0 X1 => of (app c0 c0) X2 +
      rid:1 step:3 gid:17 user:rule:pi = success
      }}} -> (0.000s)
      run 4 {{{ -
      rid:1 step:4 gid:19 user:curgoal = => +
      rid:1 step:4 gid:17 user:curgoal = => of c0 X1 => of (app c0 c0) X2 -
      rid:1 step:4 gid:19 user:rule = implication -
      rid:1 step:4 gid:19 user:subgoal = 20 -
      rid:1 step:4 gid:20 user:newgoal = of (app c0 c0) X2 -
      rid:1 step:4 gid:20 user:rule:implication = success +
      rid:1 step:4 gid:17 user:rule = implication +
      rid:1 step:4 gid:17 user:subgoal = 18 +
      rid:1 step:4 gid:18 user:newgoal = of (app c0 c0) X2 +
      rid:1 step:4 gid:18 user:rule:implication = success
      }}} -> (0.000s)
      run 5 {{{ -
      rid:1 step:5 gid:20 user:curgoal = of +
      rid:1 step:5 gid:18 user:curgoal = of of (app c0 c0) X2 -
      rid:1 step:5 gid:20 user:rule = backchain -
      rid:1 step:5 gid:20 user:rule:backchain:candidates = File "(stdin)", line 10, column 3, character 294: +
      rid:1 step:5 gid:18 user:rule = backchain +
      rid:1 step:5 gid:18 user:rule:backchain:candidates = File "(stdin)", line 10, column 3, characters 294-343:
      }}} -> (0.000s)
      select 4 {{{ -
      rid:1 step:5 gid:20 user:rule:backchain:try = File "(stdin)", line 10, column 3, character 294: - (of (app A0 A1) A2) :- ( - of A0 (arr A3 A2)), - (of A1 A3). +
      rid:1 step:5 gid:18 user:rule:backchain:try = File "(stdin)", line 10, column 3, characters 294-343: + (of (app A0 A3) A2) :- ( + of A0 (arr A1 A2)), + (of A3 A1).
      rid:1 step:5 gid:0 user:assign = A0 := c0 -
      rid:1 step:5 gid:0 user:assign = A1 := c0 +
      rid:1 step:5 gid:0 user:assign = A3 := c0
      rid:1 step:5 gid:0 user:assign = A2 := X2 -
      rid:1 step:5 gid:20 user:subgoal = 21 -
      rid:1 step:5 gid:21 user:newgoal = of c0 (arr X3^1 X2) -
      rid:1 step:5 gid:21 user:subgoal = 22 -
      rid:1 step:5 gid:22 user:newgoal = of c0 X3^1 -
      rid:1 step:5 gid:21 user:rule:backchain = success +
      rid:1 step:5 gid:18 user:subgoal = 19 +
      rid:1 step:5 gid:19 user:newgoal = of c0 (arr X3^1 X2) +
      rid:1 step:5 gid:19 user:subgoal = 20 +
      rid:1 step:5 gid:20 user:newgoal = of c0 X3^1 +
      rid:1 step:5 gid:19 user:rule:backchain = success
      }}} -> (0.000s)
      run 6 {{{ -
      rid:1 step:6 gid:21 user:curgoal = of +
      rid:1 step:6 gid:19 user:curgoal = of of c0 (arr X3^1 X2) -
      rid:1 step:6 gid:21 user:rule = backchain -
      rid:1 step:6 gid:21 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:1 step:6 gid:19 user:rule = backchain +
      rid:1 step:6 gid:19 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, characters 0-0:
      }}} -> (0.000s)
      select 5 {{{ -
      rid:1 step:6 gid:21 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:1 step:6 gid:19 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, characters 0-0: (of c0 X1) :- .
      rid:1 step:6 gid:0 user:assign:expand = X3^1 := X4 c0
      rid:1 step:6 gid:0 user:assign:restrict = 0 X4 c0 := c0 \ .X5
      rid:1 step:6 gid:0 user:assign = X1 := arr X5 X2 -
      rid:1 step:6 gid:21 user:rule:backchain = success +
      rid:1 step:6 gid:19 user:rule:backchain = success
      }}} -> (0.000s)
      run 7 {{{ -
      rid:1 step:7 gid:22 user:curgoal = of +
      rid:1 step:7 gid:20 user:curgoal = of of c0 X5 -
      rid:1 step:7 gid:22 user:rule = backchain -
      rid:1 step:7 gid:22 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:1 step:7 gid:20 user:rule = backchain +
      rid:1 step:7 gid:20 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, characters 0-0:
      }}} -> (0.000s)
      select 6 {{{ -
      rid:1 step:7 gid:22 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:1 step:7 gid:20 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, characters 0-0: (of c0 (arr X5 X2)) :- . -
      rid:1 step:7 gid:22 user:backchain:fail-to = unify X5 with arr X5 X2 +
      rid:1 step:7 gid:20 user:backchain:fail-to = unify X5 with arr X5 X2
      }}} -> (0.000s)
      select 7 {{{ -
      rid:1 step:7 gid:22 user:rule:backchain = fail +
      rid:1 step:7 gid:20 user:rule:backchain = fail
      }}} -> (0.000s)
      The elpi tactic/command stlc failed without giving a specific error message. Please report this inconvenience to the authors of the program.

      The trace can be limited to a range of steps. Look at the @@ -1324,29 +1352,29 @@

      Trace browser

      of (fun (x\ fun y\ x)) Ty, coq.say Ty }}.
      run 6 {{{ -
      rid:2 step:6 gid:29 user:curgoal = pi +
      rid:2 step:6 gid:27 user:curgoal = pi pi c1 \ of c1 X0 => of c0 X1 -
      rid:2 step:6 gid:29 user:rule = pi -
      rid:2 step:6 gid:29 user:subgoal = 30 -
      rid:2 step:6 gid:30 user:newgoal = of c1 X0 => of c0 X1 -
      rid:2 step:6 gid:30 user:rule:pi = success +
      rid:2 step:6 gid:27 user:rule = pi +
      rid:2 step:6 gid:27 user:subgoal = 28 +
      rid:2 step:6 gid:28 user:newgoal = of c1 X0 => of c0 X1 +
      rid:2 step:6 gid:28 user:rule:pi = success
      }}} -> (0.000s)
      run 7 {{{ -
      rid:2 step:7 gid:30 user:curgoal = => +
      rid:2 step:7 gid:28 user:curgoal = => of c1 X0 => of c0 X1 -
      rid:2 step:7 gid:30 user:rule = implication -
      rid:2 step:7 gid:30 user:subgoal = 31 -
      rid:2 step:7 gid:31 user:newgoal = of c0 X1 -
      rid:2 step:7 gid:31 user:rule:implication = success +
      rid:2 step:7 gid:28 user:rule = implication +
      rid:2 step:7 gid:28 user:subgoal = 29 +
      rid:2 step:7 gid:29 user:newgoal = of c0 X1 +
      rid:2 step:7 gid:29 user:rule:implication = success
      }}} -> (0.000s)
      run 8 {{{ -
      rid:2 step:8 gid:31 user:curgoal = of +
      rid:2 step:8 gid:29 user:curgoal = of of c0 X1 -
      rid:2 step:8 gid:31 user:rule = backchain -
      rid:2 step:8 gid:31 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:2 step:8 gid:29 user:rule = backchain +
      rid:2 step:8 gid:29 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, characters 0-0:
      }}} -> (0.000s)
      select 5 {{{ -
      rid:2 step:8 gid:31 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, character 0: +
      rid:2 step:8 gid:29 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, characters 0-0: (of c0 X2) :- .
      rid:2 step:8 gid:0 user:assign = X2 := X1 -
      rid:2 step:8 gid:31 user:rule:backchain = success +
      rid:2 step:8 gid:29 user:rule:backchain = success
      }}} -> (0.000s)
      arr X1 (arr X0 X1)
      Query assignments:
      Ty = arr X1 (arr X0 X1)

      The trace can be limited to a (list of) predicates as follows:

      Elpi Trace "of".
 
      run 2 {{{  
-
      rid:3 step:2 gid:33 user:curgoal = of 
+
      rid:3 step:2 gid:31 user:curgoal = of 
                                    of (fun c0 \ fun c1 \ c0) X0 
-
      rid:3 step:2 gid:33 user:rule = backchain 
-
      rid:3 step:2 gid:33 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, character 459: 
+
      rid:3 step:2 gid:31 user:rule = backchain 
+
      rid:3 step:2 gid:31 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, characters 460-514: 
 
      }}} ->  (0.000s)
      select 3 {{{  
-
      rid:3 step:2 gid:33 user:rule:backchain:try = File "(stdin)", line 15, column 3, character 459: 
-                                              (of (fun A0) (arr A1 A2)) :- (
+
      rid:3 step:2 gid:31 user:rule:backchain:try = File "(stdin)", line 15, column 3, characters 460-514: 
+                                              (of (fun A0) (arr A2 A1)) :- (
                                                pi (c0 \
-                                                (of c0 A1 => of (A0 c0) A2))). 
+                                                (of c0 A2 => of (A0 c0) A1))). 
 
      rid:3 step:2 gid:0 user:assign = A0 := c0 \
                                  fun c1 \ c0 
 
      rid:3 step:2 gid:0 user:assign = X0 := arr X1 X2 
-
      rid:3 step:2 gid:33 user:subgoal = 35 
-
      rid:3 step:2 gid:35 user:newgoal = pi c0 \ of c0 X1 => of (fun c1 \ c0) X2 
-
      rid:3 step:2 gid:35 user:rule:backchain = success 
+
      rid:3 step:2 gid:31 user:subgoal = 33 
+
      rid:3 step:2 gid:33 user:newgoal = pi c0 \ of c0 X1 => of (fun c1 \ c0) X2 
+
      rid:3 step:2 gid:33 user:rule:backchain = success 
 
      }}} ->  (0.000s)
      run 5 {{{  
-
      rid:3 step:5 gid:37 user:curgoal = of 
+
      rid:3 step:5 gid:35 user:curgoal = of 
                                    of (fun c1 \ c0) X2 
-
      rid:3 step:5 gid:37 user:rule = backchain 
-
      rid:3 step:5 gid:37 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, character 459: 
+
      rid:3 step:5 gid:35 user:rule = backchain 
+
      rid:3 step:5 gid:35 user:rule:backchain:candidates = File "(stdin)", line 15, column 3, characters 460-514: 
 
      }}} ->  (0.000s)
      select 4 {{{  
-
      rid:3 step:5 gid:37 user:rule:backchain:try = File "(stdin)", line 15, column 3, character 459: 
-                                              (of (fun A0) (arr A1 A2)) :- (
+
      rid:3 step:5 gid:35 user:rule:backchain:try = File "(stdin)", line 15, column 3, characters 460-514: 
+                                              (of (fun A0) (arr A2 A1)) :- (
                                                pi (c0 \
-                                                (of c0 A1 => of (A0 c0) A2))). 
+                                                (of c0 A2 => of (A0 c0) A1))). 
 
      rid:3 step:5 gid:0 user:assign = A0 := c1 \
                                  c0 
 
      rid:3 step:5 gid:0 user:assign = X2 := arr X3 X4 
-
      rid:3 step:5 gid:37 user:subgoal = 38 
-
      rid:3 step:5 gid:38 user:newgoal = pi c1 \ of c1 X3 => of c0 X4 
-
      rid:3 step:5 gid:38 user:rule:backchain = success 
+
      rid:3 step:5 gid:35 user:subgoal = 36 
+
      rid:3 step:5 gid:36 user:newgoal = pi c1 \ of c1 X3 => of c0 X4 
+
      rid:3 step:5 gid:36 user:rule:backchain = success 
 
      }}} ->  (0.000s)
      run 8 {{{  
-
      rid:3 step:8 gid:40 user:curgoal = of 
+
      rid:3 step:8 gid:38 user:curgoal = of 
                                    of c0 X4 
-
      rid:3 step:8 gid:40 user:rule = backchain 
-
      rid:3 step:8 gid:40 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, character 0: 
+
      rid:3 step:8 gid:38 user:rule = backchain 
+
      rid:3 step:8 gid:38 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, characters 0-0: 
 
      }}} ->  (0.000s)
      select 5 {{{  
-
      rid:3 step:8 gid:40 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, character 0: 
+
      rid:3 step:8 gid:38 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, characters 0-0: 
                                               (of c0 X1) :- . 
 
      rid:3 step:8 gid:0 user:assign = X1 := X4 
-
      rid:3 step:8 gid:40 user:rule:backchain = success 
+
      rid:3 step:8 gid:38 user:rule:backchain = success 
 
      }}} ->  (0.000s)
      arr X4 (arr X3 X4)
      Query assignments:
      Ty = arr X4 (arr X3 X4)

      One can combine the range of steps with the predicate:

      Elpi Trace 6 8 "of".
 
      run 8 {{{  
-
      rid:4 step:8 gid:49 user:curgoal = of 
+
      rid:4 step:8 gid:47 user:curgoal = of 
                                    of c0 X0 
-
      rid:4 step:8 gid:49 user:rule = backchain 
-
      rid:4 step:8 gid:49 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, character 0: 
+
      rid:4 step:8 gid:47 user:rule = backchain 
+
      rid:4 step:8 gid:47 user:rule:backchain:candidates = File "(context step_id:4)", line 1, column 0, characters 0-0: 
 
      }}} ->  (0.000s)
      select 5 {{{  
-
      rid:4 step:8 gid:49 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, character 0: 
+
      rid:4 step:8 gid:47 user:rule:backchain:try = File "(context step_id:4)", line 1, column 0, characters 0-0: 
                                               (of c0 X1) :- . 
 
      rid:4 step:8 gid:0 user:assign = X1 := X0 
-
      rid:4 step:8 gid:49 user:rule:backchain = success 
+
      rid:4 step:8 gid:47 user:rule:backchain = success 
 
      }}} ->  (0.000s)
      arr X0 (arr X2 X0)
      Query assignments:
      Ty = arr X0 (arr X2 X0)

      To switch traces off:

      Elpi Trace Off.
      @@ -1436,12 +1464,13 @@

      Good old print

      Printing entire programs

      Given that programs are not written in a single place, but rather obtained by -accumulating code, Elpi is able to print a (full) program to an html file +accumulating code, Elpi is able to print a (full) program to an text file as follows. The obtained file provides a facility to filter rules by their -predicate.

      -
      Elpi Print stlc "elpi_examples/stlc".

      Look at the generated page -and type of in the filter.

      -

      Finally, one can bound the number of backchaining steps +predicate. Note that the first component of the path is a Coq Load Path (i.e. +coqc options -R and -Q), the text file will be placed in the directory +bound to it.

      +
      Elpi Print stlc "elpi_examples/stlc".

      Look at the generated page. +Finally, one can bound the number of backchaining steps performed by the interpreter:

      Elpi Query lp:{{ 0 = 0, 1 = 1 }}.
 Elpi Bound Steps 1.
@@ -1450,15 +1479,46 @@ 
      Printing entire programs
      
 
      Common pitfalls
      
 
      Well, no programming language is perfect.
      
-
      
-
      Precedence of , and =>
      
-
      The precedence of , and => can be surprising
      
+
      
+
      Precedence of ,, :e: ==> and =>
      
+
      In this tutorial we only used :e: ==> but Elpi also provides
+the standard λProlog implication =>. They have the same meaning
+but different precedences w.r.t. ,.
      
+
      The code a, c ==> d, e reads a, (c ==> (d,e)), that means that
+the rule c is available to both d and e.
      
+
      On the contrary the code a, c => d, e reads a, (c ==> d), e,
+making c only available to d.
      
+
      So, => binds stronger than ,, while ==> binds stronger only
+on the left.
      
+
      According to our experience the precedence of => is a common source
+of mistakes for beginners, if only because it is not stable by adding of
+debug prints, that is a => b and a => print "doing b", b have
+very different meaning (a becomes only available to print!).
      
+
      In this tutorial we only used ==> that was introduced in Elpi 2.0, but
+there is code out there using =>. Elpi 2.0 raises a warning if the
+right hand side of => is a conjenction with no parentheses.
      
+
      A concrete example:
      
 
      The elpi tactic/command stlc failed without giving a
+}}.
      Toplevel input, characters 43-58
+The standard λProlog infix operator for implication => has higher precedence
+than conjunction. This means that 'A => B, C' reads '(A => B), C'.
+This is a common mistake since it makes A only available to B (and not to C
+as many newcomers may expect).
+If this is really what you want write '(A => B), C' to silence this warning.
+Otherwise write 'A => (B, C)', or use the alternative implication operator ==>.
+Infix ==>  has lower precedence than conjunction, hence
+'A ==> B, C' reads 'A ==> (B, C)' and means the same as 'A => (B, C)'.
+[elpi.implication-precedence,elpi,default]
      Toplevel input, characters 48-48
+A is linear: name it _A (discard) or A_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 58-58
+B is linear: name it _B (discard) or B_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 66-66
+C is linear: name it _C (discard) or C_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      The elpi tactic/command stlc failed without giving a
 specific error message. Please report this
 inconvenience to the authors of the program.
      
 
@@ -1467,10 +1527,29 @@ 
      Precedence of pi x\
     of x A => (of x B, of x C) % both goals see of x A
 
-}}.
      Query assignments:
      A = X0
      B = X0
      C = X0
      
+}}.
      Toplevel input, characters 127-127
+A is linear: name it _A (discard) or A_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 138-138
+B is linear: name it _B (discard) or B_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 146-146
+C is linear: name it _C (discard) or C_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Query assignments:
      A = X0
      B = X0
      C = X0
      
+
+
      Toplevel input, characters 219-219
+A is linear: name it _A (discard) or A_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 230-230
+B is linear: name it _B (discard) or B_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Toplevel input, characters 238-238
+C is linear: name it _C (discard) or C_ (fresh variable)
+[elpi.linear-variable,elpi.typecheck,elpi,default]
      Query assignments:
      A = X0
      B = X0
      C = X0

      Backtracking

      -

      Backtracking can lead to weird execution traces. The std.do! predicate +

      Backtracking can lead to weird execution traces. The std.do! predicate should be used to write non-backtracking code.

       pred not-a-backtracking-one.
@@ -1483,8 +1562,8 @@ 
      Backtracking
      
 
      In the example above once condition holds we start a sequence of
 steps which we will not reconsider. Locally, backtracking is still
 available, e.g. between generate and test.
-See also the std.spy-do! predicate which prints each and every step,
-and the std.spy one which can be used to spy on a single one.
      
+See also the std.spy-do! predicate which prints each and every step,
+and the std.spy one which can be used to spy on a single one.