Playground ========== This page is used to test hooks in order to run ``elpi`` on code snippets and inject its output within ``sphinx`` documentation sources. Prerequisites ------------- Before running the hooks, make sure to have ``elpi`` built locally: .. code-block:: console eval $(opam env) make build It doesn't hurt to check that ``dune`` runs the locally built ``elpi`` correctly: .. code-block:: console dune exec elpi -- -h Syntax ------ Elpi code blocks to be evaluated and which output is to be injected from ``docs/base`` to ``docs/source`` are conventionally denoted in ``reStructuredText`` as ``.. elpi:: FILE``. .. literalinclude:: ../../tests/sources/chr.elpi :linenos: :language: elpi The injection engine: * Retrieves all ``.. elpi::`` directives * Changes them into ``literalinclude`` in the generated source with relevant options * Runs ``dune exec elpi -- -test FILE`` on the ``FILE`` containing the ``elpi`` snippet, test or example. * Captures its output (``stdout``) * Creates a ``code-block:: console`` just after it to inject the captured console output * Captures its output (``stderr``) * Creates a ``code-block:: console`` just after it to inject the captured console erros * In case of an assertion option for the ``elpi`` directive, the output is injected only if matched Result should look as follows: .. code-block:: console Parsing time: 0.000 Compilation time: 0.004 File "/home/jwintz/Development/elpi/tests/sources/chr.elpi", line 7, column 60, character 133: Warning: constant term has no declared type. File "/home/jwintz/Development/elpi/tests/sources/chr.elpi", line 11, column 8, character 319: Warning: constant len has no declared type. Did you mean std.length ? File "/home/jwintz/Development/elpi/tests/sources/chr.elpi", line 28, column 28, character 761: Warning: constant compatible has no declared type. Typechecking time: 0.154 compat [term c1 (uvar frozen--501 []), term c0 (uvar frozen--502 [])] |- frozen--494 [ c1, c0] arr (uvar frozen--495 [c0, c1]) (arr (uvar frozen--496 [c0, c1]) (uvar frozen--497 [])) , [ term c3 (uvar frozen--499 []), term c2 (uvar frozen--498 [])] |- frozen--494 [ c2, c3] arr (uvar frozen--498 []) (arr (uvar frozen--499 []) (uvar frozen--500 [])) NEW [X0 = X1, X2 = X3] arr (X4 c0 c1) (arr (X5 c0 c1) X6) = arr X1 (arr X3 X7) 1 compat [term c0 bool] |- frozen--507 [c0] uvar frozen--508 [] , [term c1 (uvar frozen--509 [])] |- frozen--507 [c1] nat NEW [bool = X8] X9 = nat 2 compat [term c0 bool] |- frozen--514 [c0] uvar frozen--515 [] , [term c1 (uvar frozen--515 [])] |- frozen--514 [c1] nat NEW [bool = X10] X10 = nat compat [term c0 bool] |- frozen--520 [c0] uvar frozen--521 [] , [term c1 nat] |- frozen--520 [c1] nat NEW [bool = nat] X11 = nat Success: Time: 0.001 Constraints: {c0} : term c0 bool ?- term (X12 c0) nat /* suspended on X12 */ {c0 c1} : term c1 X13, term c0 X13 ?- term (X14 c1 c0) (arr X13 (arr X13 X6)) /* suspended on X14 */ State: Regexp Matching --------------- This ``elpi`` directive should pass validation: .. code-block:: console .. elpi:: ./a.elpi :assert: V = s \(.*\) **./a.elpi :** .. literalinclude:: ./a.elpi :linenos: :language: elpi .. code-block:: console V = s (s (s (s (s (s (s (s (s (s (s (s (s zero)))))))))))) .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.060 Success: Time: 0.000 Constraints: State: This one should fail validation, only a message stating the regexp matching error will be printed: .. code-block:: console .. elpi:: ./a.elpi :assert: /(?!)/ **./a.elpi :** .. literalinclude:: ./a.elpi :linenos: :language: elpi .. raw:: html 
Injection failure: result did not pass regexp check (/(?!)/)
Test Bed -------- **../../tests/sources/accumulate_twice1.elpi :** .. literalinclude:: ../../tests/sources/accumulate_twice1.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.055 **../../tests/sources/accumulate_twice2.elpi :** .. literalinclude:: ../../tests/sources/accumulate_twice2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/accumulate_twice2.elpi", line 4, column 0, character 87: Warning: constant other.doomed has no declared type. .. code-block:: console Parsing time: 0.001 Compilation time: 0.001 Typechecking time: 0.060 **../../tests/sources/accumulated.elpi :** .. literalinclude:: ../../tests/sources/accumulated.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/accumulated.elpi", line 1, column 0, character 0: Warning: constant doomed has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.061 **../../tests/sources/ackermann.elpi :** .. literalinclude:: ../../tests/sources/ackermann.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/ackermann.elpi", line 13, column 0, character 530: Warning: constant zero has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/ackermann.elpi", line 13, column 0, character 530: Warning: constant s has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.set.make std.set.mem std.set.add std.set.remove std.set.cardinal std.set.elements std.spy std.spy! std.split-at std.spy-do! rex.split random.self_init std.string.concat std.string.map std.string.map.empty std.string.map.mem std.string.map.add std.string.map.remove std.string.map.find std.string.map.bindings std.string.set std.string.set.empty std.string.set.mem std.string.set.add std.string.set.remove std.string.set.union std.string.set.inter std.string.set.diff std.string.set.equal std.string.set.subset std.string.set.elements std.string.set.cardinal std.int.set std.int.set.empty std.int.set.mem std.int.set.add std.int.set.remove std.int.set.union std.int.set.inter std.int.set.diff std.int.set.equal std.int.set.subset std.int.set.elements std.int.set.cardinal std.loc.set std.loc.set.empty std.loc.set.mem std.loc.set.add std.loc.set.remove std.loc.set.union std.loc.set.inter std.loc.set.diff std.loc.set.equal std.loc.set.subset std.loc.set.elements std.loc.set.cardinal std.set std.set gc.set gc.stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/ackermann.elpi", line 13, column 0, character 530: Warning: constant ack has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/ackermann.elpi", line 19, column 0, character 676: Warning: V is linear: name it _V (discard) or V_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.075 Success: Time: 0.000 Constraints: State: **../../tests/sources/asclause.elpi :** .. literalinclude:: ../../tests/sources/asclause.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/asclause.elpi", line 5, column 0, character 36: Warning: constant simple has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/asclause.elpi", line 2, column 0, character 1: Warning: constant lam has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/asclause.elpi", line 2, column 0, character 1: Warning: constant hard has no declared type. 1 lam c0 \ c0 .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.064 Success: Time: 0.000 Constraints: State: **../../tests/sources/beta.elpi :** .. literalinclude:: ../../tests/sources/beta.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/beta.elpi", line 1, column 0, character 0: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/beta.elpi", line 1, column 0, character 0: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/beta.elpi", line 1, column 0, character 0: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.063 Success: Time: 0.000 Constraints: State: **../../tests/sources/block.elpi :** .. literalinclude:: ../../tests/sources/block.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Fatal error: File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/block.elpi", line 1, column 0, character 0:matching } is missing **../../tests/sources/chr.elpi :** .. literalinclude:: ../../tests/sources/chr.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr.elpi", line 7, column 0, character 133: Warning: constant term has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr.elpi", line 11, column 0, character 319: Warning: constant len has no declared type. Did you mean std.length ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr.elpi", line 28, column 0, character 761: Warning: constant compatible has no declared type. compat [term c1 (uvar frozen--501 []), term c0 (uvar frozen--502 [])] |- frozen--494 [c1, c0] arr (uvar frozen--495 [c0, c1]) (arr (uvar frozen--496 [c0, c1]) (uvar frozen--497 [])) , [term c3 (uvar frozen--499 []), term c2 (uvar frozen--498 [])] |- frozen--494 [c2, c3] arr (uvar frozen--498 []) (arr (uvar frozen--499 []) (uvar frozen--500 [])) NEW [X0 = X1, X2 = X3] arr (X4 c0 c1) (arr (X5 c0 c1) X6) = arr X1 (arr X3 X7) 1 compat [term c0 bool] |- frozen--507 [c0] uvar frozen--508 [] , [term c1 (uvar frozen--509 [])] |- frozen--507 [c1] nat NEW [bool = X8] X9 = nat 2 compat [term c0 bool] |- frozen--514 [c0] uvar frozen--515 [] , [term c1 (uvar frozen--515 [])] |- frozen--514 [c1] nat NEW [bool = X10] X10 = nat compat [term c0 bool] |- frozen--520 [c0] uvar frozen--521 [] , [term c1 nat] |- frozen--520 [c1] nat NEW [bool = nat] X11 = nat .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.071 Success: Time: 0.001 Constraints: {c0} : term c0 bool ?- term (X12 c0) nat /* suspended on X12 */ {c0 c1} : term c1 X13, term c0 X13 ?- term (X14 c1 c0) (arr X13 (arr X13 X6)) /* suspended on X14 */ State: **../../tests/sources/chrGCD.elpi :** .. literalinclude:: ../../tests/sources/chrGCD.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chrGCD.elpi", line 6, column 0, character 74: Warning: constant gcd has no declared type. group 1 solved group 2 solved .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.058 Success: Time: 0.000 Constraints: State: **../../tests/sources/chrLEQ.elpi :** .. literalinclude:: ../../tests/sources/chrLEQ.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chrLEQ.elpi", line 7, column 0, character 238: Warning: constant ltn has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chrLEQ.elpi", line 2, column 0, character 16: Warning: constant leq has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.062 Success: Time: 0.001 Constraints: ltn X0 X1 /* suspended on X0, X1 */ leq X0 X1 /* suspended on X0, X1 */ leq X2 X1 /* suspended on X2, X1 */ ltn X0 X2 /* suspended on X0, X2 */ leq X0 X2 /* suspended on X0, X2 */ State: **../../tests/sources/chr_nokey.elpi :** .. literalinclude:: ../../tests/sources/chr_nokey.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.059 Success: Time: 0.000 Constraints: test 1 /* suspended on X0 */ State: **../../tests/sources/chr_nokey2.elpi :** .. literalinclude:: ../../tests/sources/chr_nokey2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr_nokey2.elpi", line 1, column 0, character 0: Warning: constant foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr_nokey2.elpi", line 1, column 0, character 0: Warning: constant bar has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.061 Success: Time: 0.000 Constraints: bar true /* suspended on */ foo /* suspended on */ State: **../../tests/sources/chr_not_clique.elpi :** .. literalinclude:: ../../tests/sources/chr_not_clique.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Fatal error: CHR rule File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr_not_clique.elpi", line 3, column 3, character 19:: matches b which is not a constraint on which it is applied. Check the list of predicates after the "constraint" keyword. **../../tests/sources/chr_sem.elpi :** .. literalinclude:: ../../tests/sources/chr_sem.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr_sem.elpi", line 1, column 0, character 0: Warning: constant d has no declared type. Did you mean std.debug-print std.drop std.drop-last std.do! std.do-ok! std.string.set.diff std.int.set.diff std.loc.set.diff ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr_sem.elpi", line 1, column 0, character 0: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/chr_sem.elpi", line 1, column 0, character 0: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? c .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.069 Success: Time: 0.000 Constraints: c /* suspended on X0 */ d /* suspended on X0 */ a /* suspended on X0 */ State: **../../tests/sources/conj2.elpi :** .. literalinclude:: ../../tests/sources/conj2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/conj2.elpi", line 1, column 0, character 0: Warning: constant test2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/conj2.elpi", line 1, column 0, character 0: Warning: constant test1 has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.065 Success: Time: 0.000 Constraints: State: **../../tests/sources/ctx_loading.elpi :** .. literalinclude:: ../../tests/sources/ctx_loading.elpi :linenos: :language: elpi .. code-block:: console [a, b, c] [a, b, c] [a, b, c] .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.057 Success: Time: 0.000 Constraints: State: **../../tests/sources/cut.elpi :** .. literalinclude:: ../../tests/sources/cut.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 6, column 0, character 100: Warning: constant two has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 8, column 0, character 108: Warning: constant three has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 2, column 0, character 60: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 5, column 0, character 79: Warning: constant ko has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 9, column 0, character 117: Warning: constant four has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 5, column 0, character 79: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 5, column 0, character 79: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut.elpi", line 2, column 0, character 60: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.079 Success: Time: 0.000 Constraints: State: **../../tests/sources/cut2.elpi :** .. literalinclude:: ../../tests/sources/cut2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 7, column 0, character 198: Warning: constant x has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 11, column 0, character 240: Warning: constant two has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 7, column 0, character 198: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 10, column 0, character 233: Warning: constant one has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 15, column 0, character 260: Warning: constant ko2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 13, column 0, character 248: Warning: constant ko1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 7, column 0, character 198: Warning: constant e has no declared type. Did you mean std.set.private.empty std.set.private.elements std.set.elements std.map.private.empty std.exists std.exists2 std.string.map.empty std.int.map.empty std.loc.map.empty std.string.set.empty std.string.set.equal std.string.set.elements std.int.set.empty std.int.set.equal std.int.set.elements std.loc.set.empty std.loc.set.equal std.loc.set.elements ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut2.elpi", line 7, column 0, character 198: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.079 Success: Time: 0.000 Constraints: State: **../../tests/sources/cut3.elpi :** .. literalinclude:: ../../tests/sources/cut3.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut3.elpi", line 3, column 0, character 36: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut3.elpi", line 5, column 0, character 57: Warning: constant ko has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut3.elpi", line 3, column 0, character 36: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut3.elpi", line 3, column 0, character 36: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut3.elpi", line 3, column 0, character 36: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.068 Success: Time: 0.000 Constraints: State: **../../tests/sources/cut4.elpi :** .. literalinclude:: ../../tests/sources/cut4.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.054 Success: Time: 0.000 Constraints: State: **../../tests/sources/cut5.elpi :** .. literalinclude:: ../../tests/sources/cut5.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 6, column 0, character 108: Warning: constant two has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 8, column 0, character 116: Warning: constant three has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 2, column 0, character 60: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 5, column 0, character 79: Warning: constant ko has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 9, column 0, character 125: Warning: constant four has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 5, column 0, character 79: Warning: constant d has no declared type. Did you mean std.debug-print std.drop std.drop-last std.do! std.do-ok! std.string.set.diff std.int.set.diff std.loc.set.diff ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 5, column 0, character 79: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 5, column 0, character 79: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 2, column 0, character 60: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut5.elpi", line 5, column 0, character 79: Warning: Y is linear: name it _Y (discard) or Y_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.081 Success: Time: 0.000 Constraints: State: **../../tests/sources/cut6.elpi :** .. literalinclude:: ../../tests/sources/cut6.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut6.elpi", line 3, column 0, character 25: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut6.elpi", line 9, column 0, character 75: Warning: constant ko has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut6.elpi", line 6, column 0, character 53: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut6.elpi", line 4, column 0, character 40: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/cut6.elpi", line 3, column 0, character 25: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.070 Success: Time: 0.000 Constraints: State: **../../tests/sources/deep_indexing.elpi :** .. literalinclude:: ../../tests/sources/deep_indexing.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.058 Success: Time: 0.000 Constraints: State: **../../tests/sources/discard.elpi :** .. literalinclude:: ../../tests/sources/discard.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/discard.elpi", line 1, column 0, character 0: Warning: constant foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/discard.elpi", line 1, column 0, character 0: Warning: constant bar has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.066 Success: Time: 0.000 Constraints: State: **../../tests/sources/elpi_only_llam.elpi :** .. literalinclude:: ../../tests/sources/elpi_only_llam.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/elpi_only_llam.elpi", line 1, column 0, character 0: Warning: constant x has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/elpi_only_llam.elpi", line 1, column 0, character 0: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/elpi_only_llam.elpi", line 1, column 0, character 0: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.067 Fatal error: Unification problem outside the pattern fragment. ((Data.Term.App (f, (Data.Term.Const x), [])) == (Data.Term.AppUVar ( { Data.Term.contents = please extend this printer; uid_private = 41116 }, 0, [(Data.Term.UVar ( { Data.Term.contents = please extend this printer; uid_private = 41115 }, 0, 0)) ] ))) Pass -delay-problems-outside-pattern-fragment (elpi command line utility) or set delay_outside_fragment to true (Elpi_API) in order to delay (deprecated, for Teyjus compatibility). **../../tests/sources/end_comment.elpi :** .. literalinclude:: ../../tests/sources/end_comment.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.055 Success: Time: 0.000 Constraints: State: **../../tests/sources/eta.elpi :** .. literalinclude:: ../../tests/sources/eta.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta.elpi", line 7, column 0, character 129: Warning: constant k2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta.elpi", line 6, column 0, character 116: Warning: constant k1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta.elpi", line 6, column 0, character 116: Warning: constant g has no declared type. Did you mean gc.get ? c2 \ c2 c2 \ c2 c1 .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.064 Success: Time: 0.000 Constraints: State: **../../tests/sources/eta_as.elpi :** .. literalinclude:: ../../tests/sources/eta_as.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: constant u has no declared type. Did you mean std.unsafe-cast std.unzip std.string.set.union std.int.set.union std.loc.set.union ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: constant tests-uvar has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 59, column 0, character 1639: Warning: constant tests-as has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 73, column 0, character 2170: Warning: constant test-unif has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 89, column 0, character 2567: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 17, column 0, character 237: Warning: constant bar has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 59, column 0, character 1639: Error: (bar u) has type any but is applied to c3 File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 97, column 0, character 2760: Error: 1 has type int but is used with type (X24 c1 -> X25) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 97, column 0, character 2760: Error: 1 has type int but is used with type (X26 c1 -> X27) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 23, column 0, character 700: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 33, column 0, character 1023: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 34, column 0, character 1040: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X5 is linear: name it _X5 (discard) or X5_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X4 is linear: name it _X4 (discard) or X4_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X3 is linear: name it _X3 (discard) or X3_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X2 is linear: name it _X2 (discard) or X2_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X1 is linear: name it _X1 (discard) or X1_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X01 is linear: name it _X01 (discard) or X01_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X0 is linear: name it _X0 (discard) or X0_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 37, column 0, character 1064: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 59, column 0, character 1639: Warning: X0 is linear: name it _X0 (discard) or X0_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 73, column 0, character 2170: Warning: X5 is linear: name it _X5 (discard) or X5_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 73, column 0, character 2170: Warning: X4 is linear: name it _X4 (discard) or X4_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 73, column 0, character 2170: Warning: X3 is linear: name it _X3 (discard) or X3_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 73, column 0, character 2170: Warning: X2 is linear: name it _X2 (discard) or X2_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 73, column 0, character 2170: Warning: X1 is linear: name it _X1 (discard) or X1_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/eta_as.elpi", line 73, column 0, character 2170: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.081 Type error. To ignore it, pass -no-tc. **../../tests/sources/even-odd.elpi :** .. literalinclude:: ../../tests/sources/even-odd.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/even-odd.elpi", line 19, column 0, character 395: Warning: Z is linear: name it _Z (discard) or Z_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.056 Success: Time: 0.000 Constraints: odd X0 /* suspended on X0 */ State: **../../tests/sources/findall.elpi :** .. literalinclude:: ../../tests/sources/findall.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 26, column 0, character 577: Warning: constant test5 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 16, column 0, character 281: Warning: constant test4 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 8, column 0, character 159: Warning: constant test3 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 7, column 0, character 95: Warning: constant test2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 6, column 0, character 43: Warning: constant test1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 6, column 0, character 43: Warning: B is linear: name it _B (discard) or B_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 6, column 0, character 43: Warning: A is linear: name it _A (discard) or A_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/findall.elpi", line 26, column 0, character 577: Warning: Z is linear: name it _Z (discard) or Z_ (fresh variable) 1 2 3 4 5 .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.073 Success: Time: 0.000 Constraints: State: **../../tests/sources/fragment_exit.elpi :** .. literalinclude:: ../../tests/sources/fragment_exit.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit.elpi", line 1, column 0, character 0: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit.elpi", line 1, column 0, character 0: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit.elpi", line 5, column 0, character 25: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.063 Success: Time: 0.000 Constraints: State: **../../tests/sources/fragment_exit2.elpi :** .. literalinclude:: ../../tests/sources/fragment_exit2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit2.elpi", line 1, column 0, character 0: Warning: constant ignore has no declared type. Did you mean std.ignore-failure! ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit2.elpi", line 2, column 0, character 10: Warning: constant d has no declared type. Did you mean std.debug-print std.drop std.drop-last std.do! std.do-ok! std.string.set.diff std.int.set.diff std.loc.set.diff ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit2.elpi", line 2, column 0, character 10: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.062 Success: Time: 0.000 Constraints: State: **../../tests/sources/fragment_exit3.elpi :** .. literalinclude:: ../../tests/sources/fragment_exit3.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit3.elpi", line 1, column 0, character 0: Warning: constant ignore has no declared type. Did you mean std.ignore-failure! ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit3.elpi", line 2, column 0, character 10: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/fragment_exit3.elpi", line 2, column 0, character 10: Warning: constant d has no declared type. Did you mean std.debug-print std.drop std.drop-last std.do! std.do-ok! std.string.set.diff std.int.set.diff std.loc.set.diff ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.063 Success: Time: 0.000 Constraints: State: **../../tests/sources/general_case.elpi :** .. literalinclude:: ../../tests/sources/general_case.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case.elpi", line 3, column 0, character 20: Warning: constant ignore has no declared type. Did you mean std.ignore-failure! ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case.elpi", line 4, column 0, character 30: Warning: constant foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case.elpi", line 2, column 0, character 17: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case.elpi", line 1, column 0, character 0: Warning: constant app has no declared type. Did you mean std.append std.appendR ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case.elpi", line 5, column 0, character 55: Warning: G is linear: name it _G (discard) or G_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.066 Success: Time: 0.000 Constraints: State: **../../tests/sources/general_case2.elpi :** .. literalinclude:: ../../tests/sources/general_case2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case2.elpi", line 3, column 0, character 20: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case2.elpi", line 1, column 0, character 0: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case2.elpi", line 1, column 0, character 0: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.071 Success: Time: 0.000 Constraints: State: **../../tests/sources/general_case3.elpi :** .. literalinclude:: ../../tests/sources/general_case3.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/general_case3.elpi", line 1, column 0, character 0: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.057 Success: Time: 0.000 Constraints: State: **../../tests/sources/hc_interp.elpi :** .. literalinclude:: ../../tests/sources/hc_interp.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 61, column 0, character 1823: Warning: constant xnil has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 42, column 0, character 1152: Warning: constant xcons has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 40, column 0, character 1103: Warning: constant try_clause has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 20, column 0, character 574: Warning: constant tru has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 65, column 0, character 2013: Warning: constant test2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 61, column 0, character 1823: Warning: constant test1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 27, column 0, character 633: Warning: constant subst has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 21, column 0, character 588: Warning: constant perp has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 14, column 0, character 396: Warning: constant or has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 40, column 0, character 1103: Warning: constant memb has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 68, column 0, character 2077: Warning: [suppressing 12 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 34, column 0, character 817: Warning: T is linear: name it _T (discard) or T_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 43, column 0, character 1172: Warning: Y is linear: name it _Y (discard) or Y_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 50, column 0, character 1381: Warning: T is linear: name it _T (discard) or T_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hc_interp.elpi", line 51, column 0, character 1445: Warning: Cs is linear: name it _Cs (discard) or Cs_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.089 Success: Time: 0.000 Constraints: State: **../../tests/sources/hdclause.elpi :** .. literalinclude:: ../../tests/sources/hdclause.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.055 Success: Time: 0.000 Constraints: State: **../../tests/sources/heap_discard.elpi :** .. literalinclude:: ../../tests/sources/heap_discard.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/heap_discard.elpi", line 1, column 0, character 0: Warning: Y is linear: name it _Y (discard) or Y_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.056 Success: Time: 0.000 Constraints: State: **../../tests/sources/ho.elpi :** .. literalinclude:: ../../tests/sources/ho.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/ho.elpi", line 3, column 0, character 67: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/ho.elpi", line 5, column 0, character 79: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.060 Success: Time: 0.000 Constraints: State: **../../tests/sources/hollight.elpi :** .. literalinclude:: ../../tests/sources/hollight.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hollight.elpi", line 231, column 18, character 8433: Malformed mode declaration. Example: mode (foo i i o). **../../tests/sources/hollight_legacy.elpi :** .. literalinclude:: ../../tests/sources/hollight_legacy.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/hollight_legacy.elpi", line 3, column 0, character 24: Mixfix directives are not supported by this parser. The parser is based on token families. A family is identified by some starting characters, for example a token '+-->' belongs to the family of '+'. There is no need to declare it. All the tokens of a family are parsed with the same precedence and associativity, for example 'x +--> y *--> z' is parsed as 'x +--> (y *--> z)' since the family of '*' has higher precedence than the family of '+'. Here the table of tokens and token families. Token families are represented by the start symbols followed by '..'. Tokens of families marked with [*] cannot end with the starting symbol, eg `foo` is not an infix, while `foo is. The listing is ordered by increasing precedence. fixity | tokens / token families -------------------------- + ----------------------------------- Infix not associative | :- ?- Infix right associative | ; Infix right associative | , & Infix right associative | -> Infix right associative | => Infix not associative | = == =< r< i< s< r=< i=< s=< <.. r> i> s> r>= i>= s>= >.. is Infix right associative | :: Infix not associative | '.. [*] Infix left associative | ^.. r+ i+ s+ +.. - r- i- s- Infix left associative | r* i* s* *.. / div mod Infix right associative | --.. Infix not associative | `.. [*] Infix right associative | ==.. Infix right associative | ||.. Infix right associative | &&.. Infix left associative | #.. Prefix not associative | r~ i~ ~.. Postfix not associative | ?.. If the token is a valid mixfix, and you want the file to stay compatible with Teyjus, you can ask Elpi to skip the directive. Eg: % elpi:skip 2 // skips the next two lines infixr ==> 120. infixr || 120. As a debugging facility one can ask Elpi to print the AST in order to verify how the text was parsed. Eg: echo 'MyFormula = a || b ==> c && d' | elpi -parse-term **../../tests/sources/hyp_uvar.elpi :** .. literalinclude:: ../../tests/sources/hyp_uvar.elpi :linenos: :language: elpi .. code-block:: console ok .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.059 Success: Time: 0.000 Constraints: State: **../../tests/sources/impl.elpi :** .. literalinclude:: ../../tests/sources/impl.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl.elpi", line 3, column 0, character 31: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl.elpi", line 3, column 0, character 31: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl.elpi", line 3, column 0, character 31: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl.elpi", line 5, column 0, character 62: Warning: constant ko has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl.elpi", line 3, column 0, character 31: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl.elpi", line 3, column 0, character 31: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.072 Success: Time: 0.000 Constraints: State: **../../tests/sources/impl2.elpi :** .. literalinclude:: ../../tests/sources/impl2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl2.elpi", line 3, column 0, character 19: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl2.elpi", line 3, column 0, character 19: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl2.elpi", line 3, column 0, character 19: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl2.elpi", line 3, column 0, character 19: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/impl2.elpi", line 3, column 0, character 19: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.069 Success: Time: 0.000 Constraints: State: **../../tests/sources/index2.elpi :** .. literalinclude:: ../../tests/sources/index2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/index2.elpi", line 111, column 0, character 2318: Warning: constant iter has no declared type. .. code-block:: console Parsing time: 0.001 Compilation time: 0.002 Typechecking time: 0.066 Success: Time: 1.267 Constraints: State: **../../tests/sources/io_colon.elpi :** .. literalinclude:: ../../tests/sources/io_colon.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/io_colon.elpi", line 1, column 0, character 0: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.066 Success: Time: 0.000 Constraints: State: **../../tests/sources/lambda.elpi :** .. literalinclude:: ../../tests/sources/lambda.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda.elpi", line 10, column 0, character 288: Warning: constant test has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda.elpi", line 7, column 0, character 186: Warning: constant of has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda.elpi", line 8, column 0, character 234: Warning: constant lam has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda.elpi", line 7, column 0, character 186: Warning: constant impl has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda.elpi", line 12, column 0, character 330: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda.elpi", line 7, column 0, character 186: Warning: constant appl has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda.elpi", line 12, column 0, character 330: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.080 Success: Time: 0.000 Constraints: State: **../../tests/sources/lambda2.elpi :** .. literalinclude:: ../../tests/sources/lambda2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda2.elpi", line 3, column 0, character 19: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda2.elpi", line 3, column 0, character 19: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda2.elpi", line 3, column 0, character 19: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda2.elpi", line 5, column 0, character 41: Warning: constant ko has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda2.elpi", line 5, column 0, character 41: Warning: constant g has no declared type. Did you mean gc.get ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.072 Success: Time: 0.000 Constraints: State: **../../tests/sources/lambda3.elpi :** .. literalinclude:: ../../tests/sources/lambda3.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 36, column 0, character 866: Warning: constant zero has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 7, column 0, character 178: Warning: constant xnil has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 6, column 0, character 122: Warning: constant xcons has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: constant x9 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: constant x8 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: constant x7 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: constant x6 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: constant x5 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: constant x4 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: constant x3 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 12, column 0, character 278: Warning: [suppressing 29 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 10, column 0, character 221: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 34, column 0, character 847: Warning: Z is linear: name it _Z (discard) or Z_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 36, column 0, character 866: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 42, column 0, character 959: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/lambda3.elpi", line 45, column 0, character 1020: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.097 Success: Time: 0.280 Constraints: State: **../../tests/sources/list_as_conj.elpi :** .. literalinclude:: ../../tests/sources/list_as_conj.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/list_as_conj.elpi", line 2, column 0, character 15: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? a b done .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.061 Success: Time: 0.000 Constraints: State: **../../tests/sources/list_comma.elpi :** .. literalinclude:: ../../tests/sources/list_comma.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.001 Typechecking time: 0.064 Success: Time: 0.000 Constraints: State: **../../tests/sources/llam.elpi :** .. literalinclude:: ../../tests/sources/llam.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 22, column 0, character 529: Warning: constant whatever has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 22, column 0, character 529: Warning: constant v has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 1, column 0, character 0: Warning: constant spy has no declared type. Did you mean std.spy std.spy! std.spy-do! ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 20, column 0, character 500: Warning: constant prune_arg3 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 19, column 0, character 476: Warning: constant prune_arg2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 18, column 0, character 459: Warning: constant prune_arg has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 22, column 0, character 529: Warning: constant h has no declared type. Did you mean std.set.private.height std.map.private.height ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 22, column 0, character 529: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 22, column 0, character 529: Warning: constant clause3 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 15, column 0, character 400: Warning: constant clause2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 14, column 0, character 383: Warning: [suppressing 2 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 18, column 0, character 459: Warning: F is linear: name it _F (discard) or F_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 19, column 0, character 476: Warning: F is linear: name it _F (discard) or F_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llam.elpi", line 20, column 0, character 500: Warning: F is linear: name it _F (discard) or F_ (fresh variable) 0 test pi c0 \ pi c1 \ X0 c1 c0 = c0 , X0 = (c0 \ c1 \ c1) 0 test pi c0 \ pi c1 \ c0 = X0 c1 c0 , X0 = (c0 \ c1 \ c1) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ c1 c3 c2 = c2 , c1 = (c2 \ c3 \ c3) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ c2 = c1 c3 c2 , c1 = (c2 \ c3 \ c3) ---------------------------------------- 0 test not (pi c0 \ pi c1 \ X1 c0 = c1) , X1 = whatever 0 test not (pi c0 \ pi c1 \ c1 = X1 c0) , X1 = whatever 0 test pi c0 \ sigma c1 \ not (pi c2 \ pi c3 \ c1 c2 = c3) , c1 = whatever 0 test pi c0 \ sigma c1 \ not (pi c2 \ pi c3 \ c3 = c1 c2) , c1 = whatever ---------------------------------------- 0 test pi c0 \ pi c1 \ X2 c1 c0 = r c2 \ h c2 c0 , X2 = (c0 \ c1 \ r c2 \ h c2 c1) 0 test pi c0 \ pi c1 \ r c2 \ h c2 c0 = X2 c1 c0 , X2 = (c0 \ c1 \ r c2 \ h c2 c1) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ c1 c3 c2 = r c4 \ h c4 c2 , c1 = (c2 \ c3 \ r c4 \ h c4 c3) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ r c4 \ h c4 c2 = c1 c3 c2 , c1 = (c2 \ c3 \ r c4 \ h c4 c3) ---------------------------------------- 0 test pi c0 \ pi c1 \ sigma c2 \ c2 = c0 , X3 c1 c0 = c2 , X3 = (c0 \ c1 \ c1) 0 test pi c0 \ pi c1 \ sigma c2 \ c2 = c0 , c2 = X3 c1 c0 , X3 = (c0 \ c1 \ c1) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ c4 = c2 , c1 c3 c2 = c4 , c1 = (c2 \ c3 \ c3) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ c4 = c2 , c4 = c1 c3 c2 , c1 = (c2 \ c3 \ c3) ---------------------------------------- 0 test not (pi c0 \ pi c1 \ sigma c2 \ c2 = c0 , X4 c2 = c1) , X4 = whatever 0 test not (pi c0 \ pi c1 \ sigma c2 \ c2 = c0 , c1 = X4 c2) , X4 = whatever 0 test pi c0 \ sigma c1 \ not (pi c2 \ pi c3 \ sigma c4 \ c4 = c2 , c1 c4 = c3) , c1 = whatever 0 test pi c0 \ sigma c1 \ not (pi c2 \ pi c3 \ sigma c4 \ c4 = c2 , c3 = c1 c4) , c1 = whatever ---------------------------------------- 0 test pi c0 \ pi c1 \ sigma c2 \ c2 = c0 , X5 c1 c0 = r c3 \ h c3 c2 , X5 = (c0 \ c1 \ r c2 \ h c2 c1) 0 test pi c0 \ pi c1 \ sigma c2 \ c2 = c0 , r c3 \ h c3 c2 = X5 c1 c0 , X5 = (c0 \ c1 \ r c2 \ h c2 c1) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ c4 = c2 , c1 c3 c2 = r c5 \ h c5 c4 , c1 = (c2 \ c3 \ r c4 \ h c4 c3) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ c4 = c2 , r c5 \ h c5 c4 = c1 c3 c2 , c1 = (c2 \ c3 \ r c4 \ h c4 c3) ---------------------------------------- 0 test pi c0 \ clause c1 \ c2 \ c1 0 test sigma c0 \ pi c1 \ pi c2 \ , (X6 c2 = r (c0 c2 c1)) (c0 c1 c1 = c1) (c0 c1 c2 = c1) , X6 = (c0 \ r c0) 0 test sigma c0 \ pi c1 \ pi c2 \ , (r (c0 c2 c1) = X6 c2) (c0 c1 c1 = c1) (c0 c1 c2 = c1) , X6 = (c0 \ r c0) 0 test pi c0 \ sigma c1 \ sigma c2 \ pi c3 \ pi c4 \ , (c1 c4 = r (c2 c4 c3)) (c2 c3 c3 = c3) (c2 c3 c4 = c3) , c1 = (c2 \ r c2) 0 test pi c0 \ sigma c1 \ sigma c2 \ pi c3 \ pi c4 \ , (r (c2 c4 c3) = c1 c4) (c2 c3 c3 = c3) (c2 c3 c4 = c3) , c1 = (c2 \ r c2) ---------------------------------------- 0 test pi c0 \ pi c1 \ sigma c2 \ pi c3 \ pi c4 \ , (X7 c1 = r (c2 c4)) (spy (c2 1 = c1)) (not (c2 2 = c0)) , X7 = (c0 \ r whatever) 0 test X8 c1 = c1 0 test pi c0 \ pi c1 \ sigma c2 \ pi c3 \ pi c4 \ , (r (c2 c4) = X7 c1) (spy (c2 1 = c1)) (not (c2 2 = c0)) , X7 = (c0 \ r whatever) 0 test X9 c1 = c1 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ pi c5 \ pi c6 \ , (c1 c3 = r (c4 c6)) (spy (c4 1 = c3)) (not (c4 2 = c2)) , c1 = (c2 \ r whatever) 0 test X10^1 c2 = c2 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ pi c5 \ pi c6 \ , (r (c4 c6) = c1 c3) (spy (c4 1 = c3)) (not (c4 2 = c2)) , c1 = (c2 \ r whatever) 0 test X11^1 c2 = c2 ---------------------------------------- 0 test pi c0 \ pi c1 \ sigma c2 \ pi c3 \ X12 c1 c0 = r (c2 c3) , c2 1 = f c0 c1 , X12 = (c0 \ c1 \ r (f c1 c0)) 0 test pi c0 \ pi c1 \ sigma c2 \ pi c3 \ r (c2 c3) = X12 c1 c0 , c2 1 = f c0 c1 , X12 = (c0 \ c1 \ r (f c1 c0)) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ pi c5 \ c1 c3 c2 = r (c4 c5) , c4 1 = f c2 c3 , c1 = (c2 \ c3 \ r (f c3 c2)) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ sigma c4 \ pi c5 \ r (c4 c5) = c1 c3 c2 , c4 1 = f c2 c3 , c1 = (c2 \ c3 \ r (f c3 c2)) ---------------------------------------- 0 test pi c0 \ pi c1 \ prune_arg (X13 c1 c0) , X13 = (c0 \ c1 \ r (v c0 c1)) 0 test pi c0 \ pi c1 \ prune_arg (X13 c1 c0) , X13 = (c0 \ c1 \ r (v c0 c1)) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ prune_arg (c1 c3 c2) , c1 = (c2 \ c3 \ r (v c2 c3)) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ prune_arg (c1 c3 c2) , c1 = (c2 \ c3 \ r (v c2 c3)) ---------------------------------------- 0 test pi c0 \ pi c1 \ prune_arg2 (X14 c1 c0) , X14 = (c0 \ c1 \ r c2 \ v c0 c1) 0 test pi c0 \ pi c1 \ prune_arg2 (X14 c1 c0) , X14 = (c0 \ c1 \ r c2 \ v c0 c1) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ prune_arg2 (c1 c3 c2) , c1 = (c2 \ c3 \ r c4 \ v c2 c3) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ prune_arg2 (c1 c3 c2) , c1 = (c2 \ c3 \ r c4 \ v c2 c3) ---------------------------------------- 0 test pi c0 \ pi c1 \ prune_arg3 (X15 c1 c0) , X15 = (c0 \ c1 \ r c2 \ c3 \ v c0 c1) 0 test pi c0 \ pi c1 \ prune_arg3 (X15 c1 c0) , X15 = (c0 \ c1 \ r c2 \ c3 \ v c0 c1) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ prune_arg3 (c1 c3 c2) , c1 = (c2 \ c3 \ r c4 \ c5 \ v c2 c3) 0 test pi c0 \ sigma c1 \ pi c2 \ pi c3 \ prune_arg3 (c1 c3 c2) , c1 = (c2 \ c3 \ r c4 \ c5 \ v c2 c3) ---------------------------------------- .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.095 Success: Time: 0.002 Constraints: State: **../../tests/sources/llamchr.elpi :** .. literalinclude:: ../../tests/sources/llamchr.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 8, column 0, character 216: Warning: constant zero has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 33, column 0, character 798: Warning: constant watch has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 3, column 0, character 18: Warning: constant term has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 9, column 0, character 231: Warning: constant succ has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 29, column 0, character 710: Warning: constant spy has no declared type. Did you mean std.spy std.spy! std.spy-do! ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 8, column 0, character 216: Warning: constant nat has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 4, column 0, character 66: Warning: constant lam has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 22, column 0, character 521: Warning: constant compatible has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 19, column 0, character 457: Warning: constant both_or_none has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 36, column 0, character 893: Warning: constant b2n has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 3, column 0, character 18: Warning: [suppressing 2 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/llamchr.elpi", line 30, column 0, character 751: Warning: P is linear: name it _P (discard) or P_ (fresh variable) X0 X1 X1 X0 nat | lam X0 c2 \ lam X1 c3 \ X2 c0 c2 c3 | lam X1 c2 \ lam X0 c3 \ X2 c0 c3 c2 [ (c2 \ c3 \ X2 c0 c2 c3) = (c2 \ c3 \ c2) ]ok nat X1 X1 nat nat | lam nat c2 \ lam X1 c3 \ c2 | lam X1 c2 \ lam nat c3 \ c3 [ term (app (lam X1 c2 \ lam nat c3 \ c3) false) _ ]ok nat bool bool nat nat | lam nat c2 \ lam bool c3 \ c2 | lam bool c2 \ lam nat c3 \ c3 .. code-block:: console Parsing time: 0.000 Compilation time: 0.003 Typechecking time: 0.094 Success: Time: 0.000 Constraints: State: **../../tests/sources/map.elpi :** .. literalinclude:: ../../tests/sources/map.elpi :linenos: :language: elpi .. code-block:: console 0.906139 + 0.038838 + 0.639453 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.057 Success: Time: 1.715 Constraints: State: **../../tests/sources/map_list.elpi :** .. literalinclude:: ../../tests/sources/map_list.elpi :linenos: :language: elpi .. code-block:: console 5.650392 + 3.082371 + 0.386618 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.064 Success: Time: 9.126 Constraints: State: **../../tests/sources/map_list_opt.elpi :** .. literalinclude:: ../../tests/sources/map_list_opt.elpi :linenos: :language: elpi .. code-block:: console 6.174692 + 3.324478 + 0.302949 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.086 Success: Time: 9.811 Constraints: State: **../../tests/sources/name_builtin.elpi :** .. literalinclude:: ../../tests/sources/name_builtin.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/name_builtin.elpi", line 1, column 0, character 0: Error: (c2) has type any but is applied to c3 c4 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.101 Type error. To ignore it, pass -no-tc. **../../tests/sources/named_clauses00.elpi :** .. literalinclude:: ../../tests/sources/named_clauses00.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Fatal error: File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/named_clauses00.elpi", line 4, column 0, character 19:a clause named name1 already exists at File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/named_clauses00.elpi", line 1, column 0, character 0: **../../tests/sources/named_clauses01.elpi :** .. literalinclude:: ../../tests/sources/named_clauses01.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Fatal error: File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/named_clauses01.elpi", line 2, column 0, character 1:unable to graft this clause: no clause named c **../../tests/sources/named_clauses02.elpi :** .. literalinclude:: ../../tests/sources/named_clauses02.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/named_clauses02.elpi", line 5, column 0, character 26: Warning: constant c has no declared type. Did you mean std.set.private.create std.set.private.cardinal std.set.cardinal std.map.private.create std.string.concat std.string.set.cardinal std.int.set.cardinal std.loc.set.cardinal trace.counter gc.compact ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.103 Success: Time: 0.000 Constraints: State: **../../tests/sources/namespaces00.elpi :** .. literalinclude:: ../../tests/sources/namespaces00.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces00.elpi", line 9, column 0, character 174: Warning: constant aux has no declared type. Did you mean rev.aux ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.092 Success: Time: 0.000 Constraints: State: **../../tests/sources/namespaces01.elpi :** .. literalinclude:: ../../tests/sources/namespaces01.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces01.elpi", line 1, column 0, character 0: Warning: constant toto has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces01.elpi", line 5, column 3, character 75: Warning: constant foo.baz has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces01.elpi", line 5, column 3, character 75: Warning: constant foo.bar has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.104 Success: Time: 0.000 Constraints: State: **../../tests/sources/namespaces02.elpi :** .. literalinclude:: ../../tests/sources/namespaces02.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces02.elpi", line 3, column 3, character 62: Warning: constant x.foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces00.elpi", line 9, column 0, character 174: Warning: constant x.acc.main has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces00.elpi", line 9, column 0, character 174: Warning: constant aux has no declared type. Did you mean x.acc.rev.aux ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.123 Success: Time: 0.000 Constraints: State: **../../tests/sources/namespaces03.elpi :** .. literalinclude:: ../../tests/sources/namespaces03.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces03.elpi", line 21, column 3, character 187: Warning: constant a.foo4 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces03.elpi", line 20, column 3, character 168: Warning: constant a.foo3 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces03.elpi", line 4, column 3, character 37: Warning: constant a.foo2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces03.elpi", line 3, column 3, character 18: Warning: constant a.foo1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces03.elpi", line 4, column 3, character 37: Warning: constant a.b.foo2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces03.elpi", line 4, column 3, character 37: Warning: constant a.b.foo1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/namespaces03.elpi", line 3, column 3, character 18: Warning: constant a.b.c.foo has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.153 Success: Time: 0.000 Constraints: State: **../../tests/sources/nil_cons.elpi :** .. literalinclude:: ../../tests/sources/nil_cons.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.096 Success: Time: 0.000 Constraints: State: **../../tests/sources/notation.elpi :** .. literalinclude:: ../../tests/sources/notation.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 13, column 0, character 122: Warning: constant ~z has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 15, column 0, character 132: Warning: constant z has no declared type. Did you mean std.zip ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 15, column 0, character 132: Warning: constant y has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 11, column 0, character 110: Warning: constant xx has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 13, column 0, character 122: Warning: constant x has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 15, column 0, character 132: Warning: constant w has no declared type. Did you mean std.while-ok-do! ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 11, column 0, character 110: Warning: constant uu has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 11, column 0, character 110: Warning: constant foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 17, column 0, character 151: Warning: constant e has no declared type. Did you mean std.set.private.empty std.set.private.elements std.set.elements std.map.private.empty std.exists std.exists2 std.string.map.empty std.int.map.empty std.loc.map.empty std.string.set.empty std.string.set.equal std.string.set.elements std.int.set.empty std.int.set.equal std.int.set.elements std.loc.set.empty std.loc.set.equal std.loc.set.elements ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 25, column 0, character 269: Warning: constant cd has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 17, column 0, character 151: Warning: [suppressing 5 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 9, column 0, character 101: Warning: D is linear: name it _D (discard) or D_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation.elpi", line 9, column 0, character 101: Warning: X is linear: name it _X (discard) or X_ (fresh variable) a a +x [b] +y d .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.160 Success: Time: 0.000 Constraints: State: **../../tests/sources/notation_error.elpi :** .. literalinclude:: ../../tests/sources/notation_error.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation_error.elpi", line 1, column 0, character 0: Mixfix directives are not supported by this parser. The parser is based on token families. A family is identified by some starting characters, for example a token '+-->' belongs to the family of '+'. There is no need to declare it. All the tokens of a family are parsed with the same precedence and associativity, for example 'x +--> y *--> z' is parsed as 'x +--> (y *--> z)' since the family of '*' has higher precedence than the family of '+'. Here the table of tokens and token families. Token families are represented by the start symbols followed by '..'. Tokens of families marked with [*] cannot end with the starting symbol, eg `foo` is not an infix, while `foo is. The listing is ordered by increasing precedence. fixity | tokens / token families -------------------------- + ----------------------------------- Infix not associative | :- ?- Infix right associative | ; Infix right associative | , & Infix right associative | -> Infix right associative | => Infix not associative | = == =< r< i< s< r=< i=< s=< <.. r> i> s> r>= i>= s>= >.. is Infix right associative | :: Infix not associative | '.. [*] Infix left associative | ^.. r+ i+ s+ +.. - r- i- s- Infix left associative | r* i* s* *.. / div mod Infix right associative | --.. Infix not associative | `.. [*] Infix right associative | ==.. Infix right associative | ||.. Infix right associative | &&.. Infix left associative | #.. Prefix not associative | r~ i~ ~.. Postfix not associative | ?.. If the token is a valid mixfix, and you want the file to stay compatible with Teyjus, you can ask Elpi to skip the directive. Eg: % elpi:skip 2 // skips the next two lines infixr ==> 120. infixr || 120. As a debugging facility one can ask Elpi to print the AST in order to verify how the text was parsed. Eg: echo 'MyFormula = a || b ==> c && d' | elpi -parse-term **../../tests/sources/notation_legacy.elpi :** .. literalinclude:: ../../tests/sources/notation_legacy.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/notation_legacy.elpi", line 3, column 10, character 24: Mixfix declaration expected (Teyjus compatibility, ignored by Elpi). Examples: infixl and 30. infixr ++ 45. prefix - 12. **../../tests/sources/patternunif.elpi :** .. literalinclude:: ../../tests/sources/patternunif.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/patternunif.elpi", line 2, column 0, character 30: Warning: constant s has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.set.make std.set.mem std.set.add std.set.remove std.set.cardinal std.set.elements std.spy std.spy! std.split-at std.spy-do! rex.split random.self_init std.string.concat std.string.map std.string.map.empty std.string.map.mem std.string.map.add std.string.map.remove std.string.map.find std.string.map.bindings std.string.set std.string.set.empty std.string.set.mem std.string.set.add std.string.set.remove std.string.set.union std.string.set.inter std.string.set.diff std.string.set.equal std.string.set.subset std.string.set.elements std.string.set.cardinal std.int.set std.int.set.empty std.int.set.mem std.int.set.add std.int.set.remove std.int.set.union std.int.set.inter std.int.set.diff std.int.set.equal std.int.set.subset std.int.set.elements std.int.set.cardinal std.loc.set std.loc.set.empty std.loc.set.mem std.loc.set.add std.loc.set.remove std.loc.set.union std.loc.set.inter std.loc.set.diff std.loc.set.equal std.loc.set.subset std.loc.set.elements std.loc.set.cardinal std.set std.set gc.set gc.stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/patternunif.elpi", line 2, column 0, character 30: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/patternunif.elpi", line 2, column 0, character 30: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/patternunif.elpi", line 2, column 0, character 30: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.119 Success: Time: 0.000 Constraints: State: **../../tests/sources/patternunif2.elpi :** .. literalinclude:: ../../tests/sources/patternunif2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/patternunif2.elpi", line 3, column 0, character 32: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/patternunif2.elpi", line 2, column 0, character 18: Warning: constant q has no declared type. Did you mean gc.quick-stat ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.093 Success: Time: 0.000 Constraints: State: **../../tests/sources/pi.elpi :** .. literalinclude:: ../../tests/sources/pi.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi.elpi", line 3, column 0, character 19: Warning: constant z has no declared type. Did you mean std.zip ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi.elpi", line 3, column 0, character 19: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi.elpi", line 3, column 0, character 19: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi.elpi", line 3, column 0, character 19: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi.elpi", line 5, column 0, character 62: Warning: constant ko has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.113 Success: Time: 0.000 Constraints: State: **../../tests/sources/pi3.elpi :** .. literalinclude:: ../../tests/sources/pi3.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi3.elpi", line 3, column 0, character 31: Warning: constant z has no declared type. Did you mean std.zip ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi3.elpi", line 3, column 0, character 31: Warning: constant q has no declared type. Did you mean gc.quick-stat ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.096 Success: Time: 0.000 Constraints: State: **../../tests/sources/pi5.elpi :** .. literalinclude:: ../../tests/sources/pi5.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi5.elpi", line 9, column 0, character 152: Warning: constant s has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.set.make std.set.mem std.set.add std.set.remove std.set.cardinal std.set.elements std.spy std.spy! std.split-at std.spy-do! rex.split random.self_init std.string.concat std.string.map std.string.map.empty std.string.map.mem std.string.map.add std.string.map.remove std.string.map.find std.string.map.bindings std.string.set std.string.set.empty std.string.set.mem std.string.set.add std.string.set.remove std.string.set.union std.string.set.inter std.string.set.diff std.string.set.equal std.string.set.subset std.string.set.elements std.string.set.cardinal std.int.set std.int.set.empty std.int.set.mem std.int.set.add std.int.set.remove std.int.set.union std.int.set.inter std.int.set.diff std.int.set.equal std.int.set.subset std.int.set.elements std.int.set.cardinal std.loc.set std.loc.set.empty std.loc.set.mem std.loc.set.add std.loc.set.remove std.loc.set.union std.loc.set.inter std.loc.set.diff std.loc.set.equal std.loc.set.subset std.loc.set.elements std.loc.set.cardinal std.set std.set gc.set gc.stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi5.elpi", line 8, column 0, character 122: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi5.elpi", line 7, column 0, character 85: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi5.elpi", line 3, column 0, character 33: Warning: constant of has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi5.elpi", line 5, column 0, character 56: Warning: constant lam has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pi5.elpi", line 4, column 0, character 42: Warning: constant bam has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.110 Success: Time: 0.000 Constraints: State: **../../tests/sources/pnf.elpi :** .. literalinclude:: ../../tests/sources/pnf.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 91, column 0, character 3225: Warning: constant test has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 25, column 0, character 688: Warning: constant termp has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 18, column 0, character 475: Warning: constant quant_free has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 36, column 0, character 855: Warning: constant prenex has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 37, column 0, character 891: Warning: constant merge has no declared type. Did you mean std.set.private.merge std.map.private.merge ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 20, column 0, character 508: Warning: constant atom has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 93, column 0, character 3271: Warning: F4 is linear: name it _F4 (discard) or F4_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 93, column 0, character 3271: Warning: F3 is linear: name it _F3 (discard) or F3_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 93, column 0, character 3271: Warning: F2 is linear: name it _F2 (discard) or F2_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/pnf.elpi", line 93, column 0, character 3271: Warning: F1 is linear: name it _F1 (discard) or F1_ (fresh variable) .. code-block:: console Parsing time: 0.001 Compilation time: 0.003 Typechecking time: 0.119 Success: Time: 0.000 Constraints: State: **../../tests/sources/polymorphic_variants.elpi :** .. literalinclude:: ../../tests/sources/polymorphic_variants.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 84, column 0, character 2748: Warning: constant union has no declared type. Did you mean std.string.set.union std.int.set.union std.loc.set.union ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 77, column 0, character 2542: Warning: constant propagate has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 33, column 0, character 1118: Warning: constant mem_ has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 30, column 0, character 1008: Warning: constant mem has no declared type. Did you mean std.set.private.mem std.set.mem std.mem! std.mem std.string.map.mem std.int.map.mem std.loc.map.mem std.string.set.mem std.int.set.mem std.loc.set.mem ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 129, column 0, character 3786: Warning: constant main2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 102, column 0, character 3251: Warning: constant main1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 28, column 0, character 958: Warning: constant is_subset_ has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 23, column 0, character 729: Warning: constant is_subset has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 88, column 0, character 2860: Warning: constant is_ground has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 80, column 0, character 2645: Warning: constant inter has no declared type. Did you mean std.intersperse std.string.set.inter std.int.set.inter std.loc.set.inter ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 23, column 0, character 729: Warning: [suppressing 18 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 35, column 0, character 1158: Warning: Y is linear: name it _Y (discard) or Y_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/polymorphic_variants.elpi", line 81, column 0, character 2697: Warning: X is linear: name it _X (discard) or X_ (fresh variable) Type-checking ok Type-inference ok ::: f : X0 -> X1 ::: g : X2 -> X3 mem X3 d /* suspended on X3 */ mem X3 c /* suspended on X3 */ X2 is_subset [a, b] /* suspended on X2 */ X3 is_subset X1 /* suspended on X3 */ mem X2 a /* suspended on X2 */ mem X1 a /* suspended on X1 */ X0 is_subset [a, b] /* suspended on X0 */ Type specialization ok ::: f : X0 -> X1 ::: g : [a] -> X3 mem X3 d /* suspended on X3 */ mem X3 c /* suspended on X3 */ X3 is_subset X1 /* suspended on X3 */ mem X1 a /* suspended on X1 */ X0 is_subset [a, b] /* suspended on X0 */ xxx failing xxx failed Type-inference ok ::: f : X4 -> X5 ::: g : X6 -> X7 ::: h1 : X8 -> X9 ::: h2 : X10 -> X11 .. code-block:: console Parsing time: 0.001 Compilation time: 0.002 Typechecking time: 0.158 Success: Time: 0.000 Constraints: mem X11 c /* suspended on X11 */ mem X11 b /* suspended on X11 */ mem X11 a /* suspended on X11 */ X10 is_subset [a, b, c] /* suspended on X10 */ mem X9 d /* suspended on X9 */ mem X9 b /* suspended on X9 */ mem X9 a /* suspended on X9 */ X8 is_subset [a, b, d] /* suspended on X8 */ mem X7 a /* suspended on X7 */ X6 is_subset [a] /* suspended on X6 */ X11 is_subset X5 /* suspended on X11 */ X7 is_subset X10 /* suspended on X7 */ mem X6 a /* suspended on X6 */ X9 is_subset X5 /* suspended on X9 */ X7 is_subset X8 /* suspended on X7 */ mem X6 a /* suspended on X6 */ mem X5 a /* suspended on X5 */ X4 is_subset [a, b, c] /* suspended on X4 */ State: **../../tests/sources/printer.elpi :** .. literalinclude:: ../../tests/sources/printer.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant || has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant x has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant g has no declared type. Did you mean gc.get ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: constant ==> has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: [suppressing 1 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Error: (r X) has type prop but is used with type int File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Error: (, (q X) (r x)) has type prop but is used with type (list prop) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: G is linear: name it _G (discard) or G_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/printer.elpi", line 1, column 0, character 0: Warning: B is linear: name it _B (discard) or B_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.123 Type error. To ignore it, pass -no-tc. **../../tests/sources/queens.elpi :** .. literalinclude:: ../../tests/sources/queens.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 14, column 0, character 189: Warning: constant zero has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 49, column 0, character 1240: Warning: constant xxx has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 24, column 0, character 348: Warning: constant xnil has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 27, column 0, character 431: Warning: constant xcons has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 27, column 0, character 431: Warning: constant select has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 15, column 0, character 204: Warning: constant s has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.set.make std.set.mem std.set.add std.set.remove std.set.cardinal std.set.elements std.spy std.spy! std.split-at std.spy-do! rex.split random.self_init std.string.concat std.string.map std.string.map.empty std.string.map.mem std.string.map.add std.string.map.remove std.string.map.find std.string.map.bindings std.string.set std.string.set.empty std.string.set.mem std.string.set.add std.string.set.remove std.string.set.union std.string.set.inter std.string.set.diff std.string.set.equal std.string.set.subset std.string.set.elements std.string.set.cardinal std.int.set std.int.set.empty std.int.set.mem std.int.set.add std.int.set.remove std.int.set.union std.int.set.inter std.int.set.diff std.int.set.equal std.int.set.subset std.int.set.elements std.int.set.cardinal std.loc.set std.loc.set.empty std.loc.set.mem std.loc.set.add std.loc.set.remove std.loc.set.union std.loc.set.inter std.loc.set.diff std.loc.set.equal std.loc.set.subset std.loc.set.elements std.loc.set.cardinal std.set std.set gc.set gc.stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 24, column 0, character 348: Warning: constant range has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 24, column 0, character 348: Warning: constant queens_aux has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 24, column 0, character 348: Warning: constant queens has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 52, column 0, character 1389: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 14, column 0, character 189: Warning: [suppressing 10 warnings] File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 34, column 0, character 649: Warning: DUMMY2 is linear: name it _DUMMY2 (discard) or DUMMY2_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 34, column 0, character 649: Warning: DUMMY1 is linear: name it _DUMMY1 (discard) or DUMMY1_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 54, column 0, character 1428: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 57, column 0, character 1471: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/queens.elpi", line 60, column 0, character 1532: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.135 Success: Time: 2.175 Constraints: State: **../../tests/sources/quote_syntax.elpi :** .. literalinclude:: ../../tests/sources/quote_syntax.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/quote_syntax.elpi", line 1, column 0, character 0: Warning: A is linear: name it _A (discard) or A_ (fresh variable) clause File "(quote_syntax): query", line 1, column 0, character 0: [] (const main) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.089 Success: Time: 0.016 Constraints: State: **../../tests/sources/random.elpi :** .. literalinclude:: ../../tests/sources/random.elpi :linenos: :language: elpi .. code-block:: console 3 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.079 Success: Time: 0.000 Constraints: State: **../../tests/sources/reduce_cbn.elpi :** .. literalinclude:: ../../tests/sources/reduce_cbn.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbn.elpi", line 7, column 0, character 285: Warning: constant subst has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbn.elpi", line 3, column 0, character 101: Warning: constant lam has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbn.elpi", line 2, column 0, character 49: Warning: constant copy has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbn.elpi", line 6, column 0, character 211: Warning: constant cbn has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbn.elpi", line 2, column 0, character 49: Warning: constant app has no declared type. Did you mean std.append std.appendR ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbn.elpi", line 14, column 0, character 563: Warning: NINE is linear: name it _NINE (discard) or NINE_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbn.elpi", line 14, column 0, character 563: Warning: TWELVE is linear: name it _TWELVE (discard) or TWELVE_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.106 Success: Time: 0.351 Constraints: State: **../../tests/sources/reduce_cbv.elpi :** .. literalinclude:: ../../tests/sources/reduce_cbv.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbv.elpi", line 2, column 0, character 52: Warning: constant lam has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbv.elpi", line 1, column 0, character 0: Warning: constant copy has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbv.elpi", line 4, column 0, character 115: Warning: constant cbv has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbv.elpi", line 5, column 0, character 186: Warning: constant beta has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbv.elpi", line 1, column 0, character 0: Warning: constant app has no declared type. Did you mean std.append std.appendR ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbv.elpi", line 15, column 0, character 351: Warning: NINE is linear: name it _NINE (discard) or NINE_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/reduce_cbv.elpi", line 15, column 0, character 351: Warning: TWELVE is linear: name it _TWELVE (discard) or TWELVE_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.106 Success: Time: 2.359 Constraints: State: **../../tests/sources/restriction.elpi :** .. literalinclude:: ../../tests/sources/restriction.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/restriction.elpi", line 3, column 0, character 21: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.077 **../../tests/sources/restriction3.elpi :** .. literalinclude:: ../../tests/sources/restriction3.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/restriction3.elpi", line 18, column 0, character 442: Warning: constant foo has no declared type. ----<<---- enter: X0 c0 = lam c1 \ lam c2 \ X1^1 c1 c2 ---->>---- exit: lam c1 \ lam c2 \ X1^1 c1 c2 = lam c1 \ lam c2 \ X1^1 c1 c2 ----<<---- enter: X2 = lam c1 \ lam c2 \ X3^1 c1 c2 ---->>---- exit: lam c1 \ lam c2 \ X4 c1 c2 = lam c1 \ lam c2 \ X4 c1 c2 ----<<---- enter: lam c1 \ lam c2 \ X1^1 c1 c2 = lam c1 \ lam c2 \ c1 ---->>---- exit: lam c1 \ lam c2 \ c1 = lam c1 \ lam c2 \ c1 ----<<---- enter: lam c1 \ lam c2 \ X4 c1 c2 = lam c1 \ lam c2 \ c1 ---->>---- exit: lam c1 \ lam c2 \ c1 = lam c1 \ lam c2 \ c1 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.088 Success: Time: 0.000 Constraints: State: **../../tests/sources/restriction4.elpi :** .. literalinclude:: ../../tests/sources/restriction4.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/restriction4.elpi", line 1, column 0, character 0: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/restriction4.elpi", line 1, column 0, character 0: Warning: X is linear: name it _X (discard) or X_ (fresh variable) ----<<---- enter: X0 c0 = f (X1^1 c1) c2 \ X2^1 c1 c2 ---->>---- exit: f (X3 c0) c2 \ X4 c0 c2 = f (X3 c0) c2 \ X4 c0 c2 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.080 Success: Time: 0.000 Constraints: State: **../../tests/sources/restriction5.elpi :** .. literalinclude:: ../../tests/sources/restriction5.elpi :linenos: :language: elpi .. code-block:: console ----<<---- enter: X0 c0 c1 = X0 c3 c4 ---->>---- exit: X1 = X1 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.079 Success: Time: 0.000 Constraints: State: **../../tests/sources/restriction6.elpi :** .. literalinclude:: ../../tests/sources/restriction6.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/restriction6.elpi", line 1, column 0, character 0: Warning: constant f has no declared type. Did you mean std.map.private.find std.map.find std.fatal-error std.fatal-error-w-data std.fold std.fold2 std.fold-map std.forall std.forall-ok std.forall2 std.filter std.flatten std.flip std.findall loc.fields std.string.map.find std.int.map.find std.loc.map.find gc.full ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/restriction6.elpi", line 1, column 0, character 0: Warning: X is linear: name it _X (discard) or X_ (fresh variable) ----<<---- enter: X0 c0 = f (X1^1 c1) c2 \ c3 \ X2^2 c3 ---->>---- exit: f (X3 c0) c2 \ c3 \ X4^1 c3 = f (X3 c0) c2 \ c3 \ X4^1 c3 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.077 Success: Time: 0.000 Constraints: State: **../../tests/sources/rev.elpi :** .. literalinclude:: ../../tests/sources/rev.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 40, column 0, character 1827: Warning: constant xnil has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 41, column 0, character 1857: Warning: constant xcons has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x9 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x8 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x7 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x6 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x5 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x4 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x3 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: constant x2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev.elpi", line 47, column 0, character 2004: Warning: [suppressing 17 warnings] .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.119 Fatal error: exception Stack overflow **../../tests/sources/rev14.elpi :** .. literalinclude:: ../../tests/sources/rev14.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 1, column 0, character 0: Warning: constant xnil has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 2, column 0, character 29: Warning: constant xcons has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x9 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x8 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x7 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x6 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x5 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x4 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x3 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: constant x2 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/rev14.elpi", line 8, column 0, character 171: Warning: [suppressing 17 warnings] .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.133 Fatal error: exception Stack overflow **../../tests/sources/same_term.elpi :** .. literalinclude:: ../../tests/sources/same_term.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.084 Success: Time: 0.000 Constraints: State: **../../tests/sources/self_assignment.elpi :** .. literalinclude:: ../../tests/sources/self_assignment.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/self_assignment.elpi", line 3, column 0, character 23: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/self_assignment.elpi", line 5, column 0, character 33: Warning: constant d has no declared type. Did you mean std.debug-print std.drop std.drop-last std.do! std.do-ok! std.string.set.diff std.int.set.diff std.loc.set.diff ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/self_assignment.elpi", line 3, column 0, character 23: Warning: A is linear: name it _A (discard) or A_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.087 Success: Time: 0.000 Constraints: State: **../../tests/sources/set.elpi :** .. literalinclude:: ../../tests/sources/set.elpi :linenos: :language: elpi .. code-block:: console 1.031358 + 0.051872 + 0.749295 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.082 Success: Time: 1.924 Constraints: State: **../../tests/sources/shorten.elpi :** .. literalinclude:: ../../tests/sources/shorten.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten.elpi", line 4, column 0, character 16: Warning: constant b.foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten.elpi", line 5, column 0, character 29: Warning: constant b.baz has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten.elpi", line 9, column 3, character 67: Warning: constant b.bar.baz has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten.elpi", line 23, column 3, character 177: Warning: constant a.main has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten.elpi", line 23, column 3, character 177: Warning: constant a.bar.baz has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.115 Success: Time: 0.000 Constraints: State: **../../tests/sources/shorten2.elpi :** .. literalinclude:: ../../tests/sources/shorten2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_aux2.elpi", line 1, column 0, character 0: Warning: constant foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_aux2.elpi", line 1, column 0, character 0: Warning: constant bar has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_aux.elpi", line 2, column 3, character 17: Warning: constant a.foo has no declared type. .. code-block:: console Parsing time: 0.001 Compilation time: 0.001 Typechecking time: 0.109 Success: Time: 0.000 Constraints: State: **../../tests/sources/shorten_aux.elpi :** .. literalinclude:: ../../tests/sources/shorten_aux.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_aux.elpi", line 2, column 3, character 17: Warning: constant a.foo has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.077 **../../tests/sources/shorten_aux2.elpi :** .. literalinclude:: ../../tests/sources/shorten_aux2.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_aux2.elpi", line 1, column 0, character 0: Warning: constant foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_aux2.elpi", line 1, column 0, character 0: Warning: constant bar has no declared type. .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.080 **../../tests/sources/shorten_builtin.elpi :** .. literalinclude:: ../../tests/sources/shorten_builtin.elpi :linenos: :language: elpi .. code-block:: console {{ }} .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.077 Success: Time: 0.000 Constraints: State: **../../tests/sources/shorten_trie.elpi :** .. literalinclude:: ../../tests/sources/shorten_trie.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_trie.elpi", line 3, column 0, character 44: Warning: constant std.string.escape has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_trie.elpi", line 2, column 0, character 18: Warning: constant std.string.concat1 has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_trie.elpi", line 1, column 0, character 0: Warning: constant std.list.map has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_trie.elpi", line 7, column 0, character 121: Warning: E is linear: name it _E (discard) or E_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_trie.elpi", line 7, column 0, character 121: Warning: AB is linear: name it _AB (discard) or AB_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/shorten_trie.elpi", line 7, column 0, character 121: Warning: F is linear: name it _F (discard) or F_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.093 Success: Time: 0.000 Constraints: State: **../../tests/sources/spill_and.elpi :** .. literalinclude:: ../../tests/sources/spill_and.elpi :linenos: :language: elpi .. code-block:: console lam c0 \ app t t .. code-block:: console Parsing time: 0.000 Compilation time: 0.003 Typechecking time: 0.094 Success: Time: 0.000 Constraints: State: **../../tests/sources/spill_impl.elpi :** .. literalinclude:: ../../tests/sources/spill_impl.elpi :linenos: :language: elpi .. code-block:: console lam c0 \ app t t .. code-block:: console Parsing time: 0.000 Compilation time: 0.004 Typechecking time: 0.088 Success: Time: 0.000 Constraints: State: **../../tests/sources/spill_lam.elpi :** .. literalinclude:: ../../tests/sources/spill_lam.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/spill_lam.elpi", line 2, column 0, character 25: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.073 Success: Time: 0.000 Constraints: State: **../../tests/sources/trace.elpi :** .. literalinclude:: ../../tests/sources/trace.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trace.elpi", line 2, column 0, character 1: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trace.elpi", line 6, column 0, character 60: Warning: Y is linear: name it _Y (discard) or Y_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trace.elpi", line 6, column 0, character 60: Warning: X is linear: name it _X (discard) or X_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.082 Success: Time: 0.000 Constraints: State: **../../tests/sources/trace2.elpi :** .. literalinclude:: ../../tests/sources/trace2.elpi :linenos: :language: elpi .. code-block:: console 1 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.077 Success: Time: 0.000 Constraints: State: **../../tests/sources/trace_chr.elpi :** .. literalinclude:: ../../tests/sources/trace_chr.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.080 Success: Time: 0.000 Constraints: odd X0 /* suspended on X0 */ State: **../../tests/sources/trace_cut.elpi :** .. literalinclude:: ../../tests/sources/trace_cut.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.085 Success: Time: 0.000 Constraints: State: **../../tests/sources/trace_findall.elpi :** .. literalinclude:: ../../tests/sources/trace_findall.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trace_findall.elpi", line 1, column 0, character 0: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? [p 1, p 2, p 3] .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.076 Success: Time: 0.000 Constraints: State: **../../tests/sources/trail.elpi :** .. literalinclude:: ../../tests/sources/trail.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trail.elpi", line 4, column 0, character 49: Warning: constant r has no declared type. Did you mean std.set.private.remove-min-binding std.set.private.remove std.set.remove std.map.private.remove-min-binding std.map.private.remove std.map.remove std.rev rex.replace std.string.map.remove std.int.map.remove std.loc.map.remove std.string.set.remove std.int.set.remove std.loc.set.remove ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trail.elpi", line 5, column 0, character 74: Warning: constant q has no declared type. Did you mean gc.quick-stat ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trail.elpi", line 4, column 0, character 49: Warning: constant p has no declared type. Did you mean std.set.private.set std.set.private.empty std.set.private.node std.set.private.height std.set.private.create std.set.private.bal std.set.private.add std.set.private.mem std.set.private.remove-min-binding std.set.private.min-binding std.set.private.merge std.set.private.remove std.set.private.cardinal std.set.private.elements std.map.private.map std.map.private.empty std.map.private.node std.map.private.height std.map.private.create std.map.private.bal std.map.private.add std.map.private.find std.map.private.remove-min-binding std.map.private.min-binding std.map.private.merge std.map.private.remove std.map.private.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trail.elpi", line 4, column 0, character 49: Warning: constant foo has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trail.elpi", line 7, column 0, character 110: Warning: constant b has no declared type. Did you mean std.set.private.bal std.map.private.bal std.map.private.bindings std.map.bindings std.string.map.bindings std.int.map.bindings std.loc.map.bindings ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/trail.elpi", line 6, column 0, character 105: Warning: constant a has no declared type. Did you mean std.set.private.add std.set.add std.map.private.add std.map.add std.assert! std.assert-ok! std.append std.appendR std.any->string std.string.map.add std.int.map.add std.loc.map.add std.string.set.add std.int.set.add std.loc.set.add ? .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.102 Success: Time: 0.000 Constraints: State: **../../tests/sources/typeabbrv.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.077 Success: Time: 0.000 Constraints: State: **../../tests/sources/typeabbrv1.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv1.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.003 Typechecking time: 0.076 Success: Time: 0.000 Constraints: State: **../../tests/sources/typeabbrv10.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv10.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv10.elpi", line 7, column 0, character 111: Error: 3 has type int but is used with type (foo X24) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv10.elpi", line 7, column 0, character 111: Error: 3 has type int but is used with type type File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv10.elpi", line 7, column 0, character 111: Error: 3 has type int but is used with type (std.map.private.map X26 X25) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv10.elpi", line 7, column 0, character 111: Error: 3 has type int but is used with type (foo X27) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv10.elpi", line 7, column 0, character 111: Error: 3 has type int but is used with type (std.map.private.map X29 X28) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.076 Type error. To ignore it, pass -no-tc. **../../tests/sources/typeabbrv11.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv11.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv11.elpi", line 4, column 0, character 31: Error: x has type string but is used with type int .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.090 Type error. To ignore it, pass -no-tc. **../../tests/sources/typeabbrv12.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv12.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv12.elpi", line 4, column 0, character 38: Error: x has type string but is used with type y .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.093 Type error. To ignore it, pass -no-tc. **../../tests/sources/typeabbrv2.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv2.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Fatal error: File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv2.elpi", line 6, column 0, character 39:duplicate type abbreviation for t1. Previous declaration: File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv2.elpi", line 1, column 0, character 0: **../../tests/sources/typeabbrv3.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv3.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.076 Success: Time: 0.000 Constraints: State: **../../tests/sources/typeabbrv4.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv4.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.072 Success: Time: 0.000 Constraints: State: **../../tests/sources/typeabbrv5.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv5.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Fatal error: exception Elpi__Compiler.CompileError(_, "looping while unfolding type abbreviation for x") **../../tests/sources/typeabbrv6.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv6.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Fatal error: File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/typeabbrv6.elpi", line 1, column 0, character 0:type abbreviation for x has unbound variables **../../tests/sources/typeabbrv7.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv7.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.072 Success: Time: 0.000 Constraints: State: **../../tests/sources/typeabbrv8.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv8.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.072 Success: Time: 0.000 Constraints: State: **../../tests/sources/typeabbrv9.elpi :** .. literalinclude:: ../../tests/sources/typeabbrv9.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.073 Success: Time: 0.000 Constraints: State: **../../tests/sources/uminus.elpi :** .. literalinclude:: ../../tests/sources/uminus.elpi :linenos: :language: elpi .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.079 Success: Time: 0.000 Constraints: State: **../../tests/sources/uvar_chr.elpi :** .. literalinclude:: ../../tests/sources/uvar_chr.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/uvar_chr.elpi", line 17, column 0, character 438: Warning: constant copy-list has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/uvar_chr.elpi", line 28, column 0, character 731: Warning: F is linear: name it _F (discard) or F_ (fresh variable) lam X0 lam c0 \ X0 c0 .. code-block:: console Parsing time: 0.000 Compilation time: 0.003 Typechecking time: 0.093 Success: Time: 0.000 Constraints: meta-copy (lam c0 \ X0 c0) (lam c0 \ X0 c0) /* suspended on */ State: **../../tests/sources/var.elpi :** .. literalinclude:: ../../tests/sources/var.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/var.elpi", line 1, column 0, character 0: Warning: X10 is linear: name it _X10 (discard) or X10_ (fresh variable) X0 , X1 , X2 , X3 , X4 , X4 c0 c1 .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.080 Success: Time: 0.000 Constraints: State: **../../tests/sources/variadic_declare_constraints.elpi :** .. literalinclude:: ../../tests/sources/variadic_declare_constraints.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/variadic_declare_constraints.elpi", line 3, column 0, character 36: Warning: Z is linear: name it _Z (discard) or Z_ (fresh variable) .. code-block:: console Parsing time: 0.000 Compilation time: 0.002 Typechecking time: 0.082 Success: Time: 0.000 Constraints: foo X0 X1 /* suspended on X0, X1, X2 */ State: **../../tests/sources/w.elpi :** .. literalinclude:: ../../tests/sources/w.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 76, column 0, character 1561: Warning: constant quantify has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 5, column 0, character 105: Warning: constant mem has no declared type. Did you mean std.set.private.mem std.set.mem std.mem! std.mem std.string.map.mem std.int.map.mem std.loc.map.mem std.string.set.mem std.int.set.mem std.loc.set.mem ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 76, column 0, character 1561: Warning: constant generalize has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 76, column 0, character 1561: Warning: constant free-ty has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 76, column 0, character 1561: Warning: constant free-gamma has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 82, column 0, character 1693: Warning: constant free has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 1, column 0, character 0: Warning: constant filter has no declared type. Did you mean std.filter ? File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 93, column 0, character 2038: Warning: constant copy-ty has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 93, column 0, character 2038: Warning: constant copy has no declared type. File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 91, column 0, character 2025: Warning: X is linear: name it _X (discard) or X_ (fresh variable) File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w.elpi", line 107, column 0, character 2408: Warning: TQ is linear: name it _TQ (discard) or TQ_ (fresh variable) Test 1 Typing let (lam c0 \ c0) X0 c0 \ app (app plus (app c0 one)) (app size (app c0 empty)) OK let (lam c0 \ c0) (all c0 \ mono (c0 ==> c0)) c0 \ app (app plus (app c0 one)) (app size (app c0 empty)) has type mono integer Test 2 Typing lam c0 \ let (lam c1 \ app (app comma c0) c1) X1 c1 \ app (app comma (app c1 one)) (app c1 c0) OK lam c0 \ let (lam c1 \ app (app comma c0) c1) (all c1 \ mono (c1 ==> pair # X2 # c1)) c1 \ app (app comma (app c1 one)) (app c1 c0) has type mono (X2 ==> pair # (pair # X2 # integer) # (pair # X2 # X2)) Test 3 Typing lam c0 \ app (app plus (app c0 one)) (app size (app c0 empty)) Error: c0 cannot have type all X3^1 Error: c0 cannot have type mono (X4^1 ==> list # X5^1) .. code-block:: console Parsing time: 0.001 Compilation time: 0.003 Typechecking time: 0.138 Success: Time: 0.001 Constraints: State: **../../tests/sources/w_legacy.elpi :** .. literalinclude:: ../../tests/sources/w_legacy.elpi :linenos: :language: elpi .. code-block:: console File "/home/jwintz/Development/elpi/docs/source/../../tests/sources/w_legacy.elpi", line 17, column 0, character 330: Mixfix directives are not supported by this parser. The parser is based on token families. A family is identified by some starting characters, for example a token '+-->' belongs to the family of '+'. There is no need to declare it. All the tokens of a family are parsed with the same precedence and associativity, for example 'x +--> y *--> z' is parsed as 'x +--> (y *--> z)' since the family of '*' has higher precedence than the family of '+'. Here the table of tokens and token families. Token families are represented by the start symbols followed by '..'. Tokens of families marked with [*] cannot end with the starting symbol, eg `foo` is not an infix, while `foo is. The listing is ordered by increasing precedence. fixity | tokens / token families -------------------------- + ----------------------------------- Infix not associative | :- ?- Infix right associative | ; Infix right associative | , & Infix right associative | -> Infix right associative | => Infix not associative | = == =< r< i< s< r=< i=< s=< <.. r> i> s> r>= i>= s>= >.. is Infix right associative | :: Infix not associative | '.. [*] Infix left associative | ^.. r+ i+ s+ +.. - r- i- s- Infix left associative | r* i* s* *.. / div mod Infix right associative | --.. Infix not associative | `.. [*] Infix right associative | ==.. Infix right associative | ||.. Infix right associative | &&.. Infix left associative | #.. Prefix not associative | r~ i~ ~.. Postfix not associative | ?.. If the token is a valid mixfix, and you want the file to stay compatible with Teyjus, you can ask Elpi to skip the directive. Eg: % elpi:skip 2 // skips the next two lines infixr ==> 120. infixr || 120. As a debugging facility one can ask Elpi to print the AST in order to verify how the text was parsed. Eg: echo 'MyFormula = a || b ==> c && d' | elpi -parse-term **../../tests/sources/zebra.elpi:** .. literalinclude:: ../../tests/sources/zebra.elpi :linenos: :language: elpi .. code-block:: console Fatal error: exception Failure("File /home/jwintz/Development/elpi/docs/source/../../tests/sources/zebra.elp not found in: /home/jwintz/Development/elpi/_build/default/../lib/, /home/jwintz/Development/elpi/_build/default/../lib/ocaml, /home/jwintz/Development/elpi/_build/install/default/lib, /home/jwintz/Development/elpi/_build/default")