Diff of the two buildlogs: -- --- b1/build.log 2023-04-12 02:27:14.989829329 +0000 +++ b2/build.log 2023-04-12 02:33:04.438206268 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Tue Apr 11 14:20:26 -12 2023 -I: pbuilder-time-stamp: 1681266026 +I: Current time: Tue May 14 22:50:18 +14 2024 +I: pbuilder-time-stamp: 1715676618 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/bookworm-reproducible-base.tgz] I: copying local configuration @@ -16,7 +16,7 @@ I: copying [./coq-elpi_1.16.0.orig.tar.gz] I: copying [./coq-elpi_1.16.0-2.debian.tar.xz] I: Extracting source -gpgv: Signature made Tue Jan 24 18:46:59 2023 -12 +gpgv: Signature made Wed Jan 25 20:46:59 2023 +14 gpgv: using RSA key 812EEFD8A3FBA4ACE4DF114B04C53BD7FE030551 gpgv: issuer "jpuydt@debian.org" gpgv: Can't check signature: No public key @@ -29,11 +29,20 @@ dpkg-source: info: applying make_install.patch I: Not using root during the build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/29232/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/D01_modify_environment starting +debug: Running on codethink13-arm64. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +lrwxrwxrwx 1 root root 4 Jan 6 2023 /bin/sh -> dash +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/D02_print_environment starting I: set BUILDDIR='/build' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME='pbuilder2' BUILD_ARCH='arm64' DEBIAN_FRONTEND='noninteractive' DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=8' @@ -43,38 +52,38 @@ IFS=' ' LANG='C' - LANGUAGE='en_US:en' + LANGUAGE='nl_BE:nl' LC_ALL='C' MAIL='/var/mail/root' OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' + PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path' PBCURRENTCOMMANDLINEOPERATION='build' PBUILDER_OPERATION='build' PBUILDER_PKGDATADIR='/usr/share/pbuilder' PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' PBUILDER_SYSCONFDIR='/etc' - PPID='29232' + PPID='31020' PS1='# ' PS2='> ' PS4='+ ' PWD='/' SHELL='/bin/bash' SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.aVFef8rv/pbuilderrc_l7ZB --distribution bookworm --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.aVFef8rv/b1 --logfile b1/build.log coq-elpi_1.16.0-2.dsc' + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/r-b-build.aVFef8rv/pbuilderrc_3Tah --distribution bookworm --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/bookworm-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/r-b-build.aVFef8rv/b2 --logfile b2/build.log --extrapackages usrmerge coq-elpi_1.16.0-2.dsc' SUDO_GID='117' SUDO_UID='110' SUDO_USER='jenkins' TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' + TZ='/usr/share/zoneinfo/Etc/GMT-14' USER='root' USERNAME='root' _='/usr/bin/systemd-run' http_proxy='http://192.168.101.16:3128' I: uname -a - Linux codethink10-arm64 4.15.0-208-generic #220-Ubuntu SMP Mon Mar 20 14:28:12 UTC 2023 aarch64 GNU/Linux + Linux i-capture-the-hostname 4.15.0-208-generic #220-Ubuntu SMP Mon Mar 20 14:28:12 UTC 2023 aarch64 GNU/Linux I: ls -l /bin - lrwxrwxrwx 1 root root 7 Apr 10 22:26 /bin -> usr/bin -I: user script /srv/workspace/pbuilder/29232/tmp/hooks/D02_print_environment finished + lrwxrwxrwx 1 root root 7 May 14 06:48 /bin -> usr/bin +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -197,7 +206,7 @@ Get: 73 http://deb.debian.org/debian bookworm/main arm64 libppx-deriving-ocaml-dev arm64 5.2.1-1+b3 [800 kB] Get: 74 http://deb.debian.org/debian bookworm/main arm64 libre-ocaml-dev arm64 1.10.4-1 [892 kB] Get: 75 http://deb.debian.org/debian bookworm/main arm64 libelpi-ocaml-dev arm64 1.16.8-1+b2 [10.9 MB] -Fetched 368 MB in 28s (13.0 MB/s) +Fetched 368 MB in 6s (62.3 MB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libpython3.11-minimal:arm64. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 19616 files and directories currently installed.) @@ -513,8 +522,17 @@ Writing extended state information... Building tag database... -> Finished parsing the build-deps +Reading package lists... +Building dependency tree... +Reading state information... +usrmerge is already the newest version (35). +0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/coq-elpi-1.16.0/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-genchanges -S > ../coq-elpi_1.16.0-2_source.changes +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/A99_set_merged_usr starting +Re-configuring usrmerge... +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/A99_set_merged_usr finished +hostname: Temporary failure in name resolution +I: Running cd /build/coq-elpi-1.16.0/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-genchanges -S > ../coq-elpi_1.16.0-2_source.changes dpkg-buildpackage: info: source package coq-elpi dpkg-buildpackage: info: source version 1.16.0-2 dpkg-buildpackage: info: source distribution unstable @@ -681,7 +699,7 @@ app [global (indt «or»), global (indt «False»), global (indt «True»)] hit app [global (indt «or»), global (indt «False»), global (indt «True»)] -Finished transaction in 0.019 secs (0.018u,0.s) (successful) +Finished transaction in 0.019 secs (0.019u,0.s) (successful) ########################## building APPS ############################ make[3]: Entering directory '/build/coq-elpi-1.16.0/apps/derive' Using coq found in /usr/bin/, from COQBIN or PATH @@ -780,26 +798,50 @@ COQC tests/test_API_section.v COQC tests/test_API_TC_CS.v make[4]: Nothing to be done for 'real-all'. -make[2]: Leaving directory '/build/coq-elpi-1.16.0/apps/eltac' -make[2]: Entering directory '/build/coq-elpi-1.16.0/apps/NES' -Using coq found in /usr/bin/, from COQBIN or PATH ?r : Reflexive R : Reflexive R where ?r : [ |- Reflexive R] +make[2]: Leaving directory '/build/coq-elpi-1.16.0/apps/eltac' +make[2]: Entering directory '/build/coq-elpi-1.16.0/apps/NES' +Using coq found in /usr/bin/, from COQBIN or PATH make[4]: Nothing to be done for 'real-all'. make[2]: Leaving directory '/build/coq-elpi-1.16.0/apps/NES' make[2]: Entering directory '/build/coq-elpi-1.16.0/apps/locker' Using coq found in /usr/bin/, from COQBIN or PATH -make[4]: Nothing to be done for 'real-all'. -make[2]: Leaving directory '/build/coq-elpi-1.16.0/apps/locker' -########################## testing APPS ############################ -make[2]: Entering directory '/build/coq-elpi-1.16.0/apps/derive' -Using coq found in /usr/bin/, from COQBIN or PATH -Warning: ../../theories (used in -R or -Q) is not a subdirectory of the current directory +Query assignments: + E = fun `n` (global (indt «nat»)) c0 \ + fun `t` (app [global (const «T2»), c0]) c1 \ + fun `_` + (app [global (const «f3»), c0, app [global (const «h»), c0, c1]]) c2 \ + app + [global (const «g3»), c0, app [global (const «h»), c0, c1], + app + [global (indc «S»), + app + [global (indc «S»), app [global (indc «S»), global (indc «O»)]]]] + TY = prod `n` (global (indt «nat»)) c0 \ + prod `t` (app [global (const «T2»), c0]) c1 \ + prod `_` + (app [global (const «f3»), c0, app [global (const «h»), c0, c1]]) c2 \ + global (indt «nat») + _uvk_1_ = X0 +Universe constraints: +UNIVERSES: + {elpi.tests.test_API_elaborate.13 elpi.tests.test_API_elaborate.10 + elpi.tests.test_API_elaborate.9} |= + elpi.tests.test_API_elaborate.13 < elpi.tests.test_API_elaborate.9 + Set <= elpi.tests.test_API_elaborate.10 + Set <= elpi.tests.test_API_elaborate.13 + T2.u0 <= elpi.tests.test_API_elaborate.13 + f3.u0 <= elpi.tests.test_API_elaborate.13 +ALGEBRAIC UNIVERSES: + {elpi.tests.test_API_elaborate.10} +UNDEFINED UNIVERSES: + elpi.tests.test_API_elaborate.10 +WEAK CONSTRAINTS: + -COQDEP VFILES -COQC tests/test_derive_stdlib.v Query assignments: L = [gref (indt «Empty_set»), gref (const «Empty_set_rect»), gref (const «Empty_set_ind»), gref (const «Empty_set_rec»), @@ -859,43 +901,6 @@ eq_refl : e2 = 3 : e2 = 3 Query assignments: - GR = const «myi» -myi : Reflexive R - : Reflexive R -Query assignments: - E = fun `n` (global (indt «nat»)) c0 \ - fun `t` (app [global (const «T2»), c0]) c1 \ - fun `_` - (app [global (const «f3»), c0, app [global (const «h»), c0, c1]]) c2 \ - app - [global (const «g3»), c0, app [global (const «h»), c0, c1], - app - [global (indc «S»), - app - [global (indc «S»), app [global (indc «S»), global (indc «O»)]]]] - TY = prod `n` (global (indt «nat»)) c0 \ - prod `t` (app [global (const «T2»), c0]) c1 \ - prod `_` - (app [global (const «f3»), c0, app [global (const «h»), c0, c1]]) c2 \ - global (indt «nat») - _uvk_1_ = X0 -Universe constraints: -UNIVERSES: - {elpi.tests.test_API_elaborate.13 elpi.tests.test_API_elaborate.10 - elpi.tests.test_API_elaborate.9} |= - elpi.tests.test_API_elaborate.13 < elpi.tests.test_API_elaborate.9 - Set <= elpi.tests.test_API_elaborate.10 - Set <= elpi.tests.test_API_elaborate.13 - T2.u0 <= elpi.tests.test_API_elaborate.13 - f3.u0 <= elpi.tests.test_API_elaborate.13 -ALGEBRAIC UNIVERSES: - {elpi.tests.test_API_elaborate.10} -UNDEFINED UNIVERSES: - elpi.tests.test_API_elaborate.10 -WEAK CONSTRAINTS: - - -Query assignments: BO = fix `add` 0 (prod `n` (global (indt «nat»)) c0 \ prod `m` (global (indt «nat»)) c1 \ global (indt «nat»)) c0 \ @@ -914,6 +919,7 @@ MI = 16 P = 1 V = 8.16.1 +make[4]: Nothing to be done for 'real-all'. Query assignments: BO = fix `add` 0 (prod `n` (global (indt «nat»)) c0 \ @@ -931,6 +937,27 @@ Succ = global (indc «S») TY = prod `n` (global (indt «nat»)) c0 \ prod `m` (global (indt «nat»)) c1 \ global (indt «nat») +make[2]: Leaving directory '/build/coq-elpi-1.16.0/apps/locker' +########################## testing APPS ############################ +make[2]: Entering directory '/build/coq-elpi-1.16.0/apps/derive' +Using coq found in /usr/bin/, from COQBIN or PATH +Warning: ../../theories (used in -R or -Q) is not a subdirectory of the current directory + +Query assignments: + GR = const «myi» +myi : Reflexive R + : Reflexive R +COQDEP VFILES +Query assignments: + E = app + [global (const «bar»), + app + [global (indc «S»), + app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]], + global (const «xxx»)] + TY = prop + _uvk_4_ = X0 + _uvk_5_ = X1 elpi.tests.test_API_module.X.i [elpi, tests, test_API_module, X, Y] [elpi, tests, test_API_module, X, Y] @@ -951,6 +978,25 @@ XYr = «X.Y.i_rect» Xi = «X.i» Query assignments: + X = «x» +fx : nat -> nat + : nat -> nat +c2 +global (indt «nat») +z +nat +Query assignments: + Spilled_1 = c0 \ c1 \ c2 \ +nat + Spilled_2 = c0 \ c1 \ c2 \ +z + T = global (indt «nat») +hello world +Query assignments: + GR = «empty_nat» + TY = global (indt «nat») +COQC tests/test_derive_stdlib.v +Query assignments: L = [tc-instance (const «inverse_impl_rewrite_relation») 3, tc-instance (const «impl_rewrite_relation») 3, tc-instance (const «iff_rewrite_relation») 2, @@ -984,52 +1030,6 @@ tc-instance (const «PER_Symmetric») 3, tc-instance (const «iff_Symmetric») 0] Query assignments: - X = «x» -fx : nat -> nat - : nat -> nat -Query assignments: - E = app - [global (const «bar»), - app - [global (indc «S»), - app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]], - global (const «xxx»)] - TY = prop - _uvk_4_ = X0 - _uvk_5_ = X1 -c2 -global (indt «nat») -z -nat -Query assignments: - Spilled_1 = c0 \ c1 \ c2 \ -nat - Spilled_2 = c0 \ c1 \ c2 \ -z - T = global (indt «nat») -hello world -Query assignments: - GR = «empty_nat» - TY = global (indt «nat») -COQC tests/test_param2.v -Query assignments: - I = «Y.i» - ID = j - J = «Y.j» - MP = «elpi.tests.test_API_module.Y» - P = [elpi, tests, test_API_module, Y] -Query assignments: - GR = indt «RewriteRelation» - L = [tc-instance (const «inverse_impl_rewrite_relation») 3, - tc-instance (const «impl_rewrite_relation») 3, - tc-instance (const «iff_rewrite_relation») 2, - tc-instance (const «relation_equivalence_rewrite_relation») 0] -opaque_3 : nat - -opaque_3 is not universe polymorphic -opaque_3 is opaque -Expands to: Constant elpi.tests.test_API_section.opaque_3 -Query assignments: E = app [global (const «op»), global (const «c»), app @@ -1049,130 +1049,17 @@ WEAK CONSTRAINTS: -nth_R = -fun (T T0 : Type) (T1 : T -> T0 -> Type) (x0 : T) (x1 : T0) (x2 : T1 x0 x1) -=> -let - fix rec (n : nat) (l : list T) {struct n} : T := - match l with - | nil => x0 - | (x :: xs)%list => match n with - | 0 => x - | S m => rec m xs - end - end in -let - fix rec0 (n : nat) (l : list T0) {struct n} : T0 := - match l with - | nil => x1 - | (x :: xs)%list => match n with - | 0 => x - | S m => rec0 m xs - end - end in -fix rec1 (n n0 : nat) (n1 : nat_R n n0) {struct n1} : - forall (l : list T) (l0 : list T0), - list_R T T0 T1 l l0 -> T1 (rec n l) (rec0 n0 l0) := - match - n1 in (nat_R s1 s2) - return - (forall (l : list T) (l0 : list T0), - list_R T T0 T1 l l0 -> T1 (rec s1 l) (rec0 s2 l0)) - with - | O_R => - let K := O_R in - (fun (n2 n3 : nat) (n4 : nat_R n2 n3) (l : list T) - (l0 : list T0) (l1 : list_R T T0 T1 l l0) => - match - l1 in (list_R _ _ _ l2 l3) - return - (T1 - match l2 with - | nil => x0 - | (x :: xs)%list => - match n2 with - | 0 => x - | S m => rec m xs - end - end - match l3 with - | nil => x1 - | (x :: xs)%list => - match n3 with - | 0 => x - | S m => rec0 m xs - end - end) - with - | nil_R _ _ _ => x2 - | cons_R _ _ _ x x3 x4 xs xs0 xs1 => - match - n4 in (nat_R n5 n6) - return - (T1 match n5 with - | 0 => x - | S m => rec m xs - end match n6 with - | 0 => x3 - | S m => rec0 m xs0 - end) - with - | O_R => x4 - | S_R m m0 m1 => rec1 m m0 m1 xs xs0 xs1 - end - end) 0 0 K - | S_R x x3 x4 => - let K := S_R x x3 x4 in - (fun (n2 n3 : nat) (n4 : nat_R n2 n3) (l : list T) - (l0 : list T0) (l1 : list_R T T0 T1 l l0) => - match - l1 in (list_R _ _ _ l2 l3) - return - (T1 - match l2 with - | nil => x0 - | (x5 :: xs)%list => - match n2 with - | 0 => x5 - | S m => rec m xs - end - end - match l3 with - | nil => x1 - | (x5 :: xs)%list => - match n3 with - | 0 => x5 - | S m => rec0 m xs - end - end) - with - | nil_R _ _ _ => x2 - | cons_R _ _ _ x5 x6 x7 xs xs0 xs1 => - match - n4 in (nat_R n5 n6) - return - (T1 match n5 with - | 0 => x5 - | S m => rec m xs - end match n6 with - | 0 => x6 - | S m => rec0 m xs0 - end) - with - | O_R => x7 - | S_R m m0 m1 => rec1 m m0 m1 xs xs0 xs1 - end - end) (S x) (S x3) K - end - : forall (T T0 : Type) (T1 : T -> T0 -> Type) (x0 : T) (x1 : T0), - T1 x0 x1 -> - forall n n0 : nat, - nat_R n n0 -> - forall (l : list T) (l0 : list T0), - list_R T T0 T1 l l0 -> T1 (nth T x0 n l) (nth T0 x1 n0 l0) +opaque_3 : nat -Arguments nth_R (T T)%type_scope T%function_scope - x0 x0 x0 (n n)%nat_scope n (l l)%list_scope l +opaque_3 is not universe polymorphic +opaque_3 is opaque +Expands to: Constant elpi.tests.test_API_section.opaque_3 +Query assignments: + I = «Y.i» + ID = j + J = «Y.j» + MP = «elpi.tests.test_API_module.Y» + P = [elpi, tests, test_API_module, Y] c2 global (indt «nat») z @@ -1189,45 +1076,10 @@ GR3 = const «A» Query assignments: GR = indt «RewriteRelation» -Query assignments: - GRy = EXN PRINTING: Not_found - I = EXN PRINTING: Not_found - L = [gref (const «A.z»), gref (const «A.i»)] - MP = «elpi.tests.test_API_module.A» - MP_TA = «elpi.tests.test_API_module.TA» - type_1 = «elpi.tests.test_API_module.10» - type_2 = «elpi.tests.test_API_module.11» -Universe constraints: -UNIVERSES: - -ALGEBRAIC UNIVERSES: - {elpi.tests.test_API_module.11 A.i.u0} -UNDEFINED UNIVERSES: - elpi.tests.test_API_module.11 - elpi.tests.test_API_module.10 -WEAK CONSTRAINTS: - - -Module -A - : TA -:= Struct - Definition x - Module B - Definition z - Inductive i1 - Definition i1_rect - Definition i1_ind - Definition i1_rec - Definition i1_sind - Definition i - End - -A.z - : nat -A.i - : Type -*** [ A.i : Type ] + L = [tc-instance (const «inverse_impl_rewrite_relation») 3, + tc-instance (const «impl_rewrite_relation») 3, + tc-instance (const «iff_rewrite_relation») 2, + tc-instance (const «relation_equivalence_rewrite_relation») 0] raw: parameter A explicit (global (const «T1»)) c0 \ inductive ind1 tt @@ -1314,6 +1166,46 @@ (prod `x` c0 c1 \ app [global (indt «eq»), c0, c1, c1]) c1 \ end-record) forall x : ind3, x -> Prop : Type +COQC tests/test_param2.v +Query assignments: + GRy = EXN PRINTING: Not_found + I = EXN PRINTING: Not_found + L = [gref (const «A.z»), gref (const «A.i»)] + MP = «elpi.tests.test_API_module.A» + MP_TA = «elpi.tests.test_API_module.TA» + type_1 = «elpi.tests.test_API_module.10» + type_2 = «elpi.tests.test_API_module.11» +Universe constraints: +UNIVERSES: + +ALGEBRAIC UNIVERSES: + {elpi.tests.test_API_module.11 A.i.u0} +UNDEFINED UNIVERSES: + elpi.tests.test_API_module.11 + elpi.tests.test_API_module.10 +WEAK CONSTRAINTS: + + +Module +A + : TA +:= Struct + Definition x + Module B + Definition z + Inductive i1 + Definition i1_rect + Definition i1_ind + Definition i1_rec + Definition i1_sind + Definition i + End + +A.z + : nat +A.i + : Type +*** [ A.i : Type ] Illegal application (Non-functional construction): The expression "Prop" of type "Type" cannot be applied to the term @@ -1348,48 +1240,8 @@ Arguments add_equal (n m)%nat_scope add_equal is opaque Expands to: Constant elpi.tests.test_API_env.add_equal -pred_R = -fun (n n0 : nat) (n1 : nat_R n n0) => -match - n1 in (nat_R n2 n3) - return - (nat_R match n2 with - | 0 => n - | S u => u - end match n3 with - | 0 => n0 - | S u => u - end) -with -| O_R => n1 -| S_R _ _ u1 => u1 -end - : forall n n0 : nat, nat_R n n0 -> nat_R (Nat.pred n) (Nat.pred n0) - -Arguments pred_R (n n)%nat_scope n -pred_R : nat2nat_R Nat.pred Nat.pred - : nat2nat_R Nat.pred Nat.pred -predn_R : nat2nat_R predn predn - : nat2nat_R predn predn -add_R : nat2nat2nat_R Nat.add Nat.add - : nat2nat2nat_R Nat.add Nat.add Query assignments: - MP_TA = «elpi.tests.test_API_module.TA» - MP_TF = «elpi.tests.test_API_module.TF» - Spilled_1 = «elpi.tests.test_API_module.a» - Spilled_2 = const const EXN PRINTING: Not_found -Module -F - : Funsig (a:TA) Funsig (b:TA) TF -:= Functor (a:TA) Functor (b:TA) Struct Definition w : nat. End - -Module B : Sig Parameter w : nat. End := (F A A) - -*** [ B.w : nat ] -Query assignments: - GR = indt «True» -File "./tests/test_param2.v", line 85, characters 0-30: -Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] + GR = indt «RewriteRelation» Query assignments: E = app [global (const «op»), global (const «c»), @@ -1409,46 +1261,161 @@ WEAK CONSTRAINTS: -COQC tests/test_invert.v unknown_gref +nth_R = +fun (T T0 : Type) (T1 : T -> T0 -> Type) (x0 : T) (x1 : T0) (x2 : T1 x0 x1) +=> +let + fix rec (n : nat) (l : list T) {struct n} : T := + match l with + | nil => x0 + | (x :: xs)%list => match n with + | 0 => x + | S m => rec m xs + end + end in +let + fix rec0 (n : nat) (l : list T0) {struct n} : T0 := + match l with + | nil => x1 + | (x :: xs)%list => match n with + | 0 => x + | S m => rec0 m xs + end + end in +fix rec1 (n n0 : nat) (n1 : nat_R n n0) {struct n1} : + forall (l : list T) (l0 : list T0), + list_R T T0 T1 l l0 -> T1 (rec n l) (rec0 n0 l0) := + match + n1 in (nat_R s1 s2) + return + (forall (l : list T) (l0 : list T0), + list_R T T0 T1 l l0 -> T1 (rec s1 l) (rec0 s2 l0)) + with + | O_R => + let K := O_R in + (fun (n2 n3 : nat) (n4 : nat_R n2 n3) (l : list T) + (l0 : list T0) (l1 : list_R T T0 T1 l l0) => + match + l1 in (list_R _ _ _ l2 l3) + return + (T1 + match l2 with + | nil => x0 + | (x :: xs)%list => + match n2 with + | 0 => x + | S m => rec m xs + end + end + match l3 with + | nil => x1 + | (x :: xs)%list => + match n3 with + | 0 => x + | S m => rec0 m xs + end + end) + with + | nil_R _ _ _ => x2 + | cons_R _ _ _ x x3 x4 xs xs0 xs1 => + match + n4 in (nat_R n5 n6) + return + (T1 match n5 with + | 0 => x + | S m => rec m xs + end match n6 with + | 0 => x3 + | S m => rec0 m xs0 + end) + with + | O_R => x4 + | S_R m m0 m1 => rec1 m m0 m1 xs xs0 xs1 + end + end) 0 0 K + | S_R x x3 x4 => + let K := S_R x x3 x4 in + (fun (n2 n3 : nat) (n4 : nat_R n2 n3) (l : list T) + (l0 : list T0) (l1 : list_R T T0 T1 l l0) => + match + l1 in (list_R _ _ _ l2 l3) + return + (T1 + match l2 with + | nil => x0 + | (x5 :: xs)%list => + match n2 with + | 0 => x5 + | S m => rec m xs + end + end + match l3 with + | nil => x1 + | (x5 :: xs)%list => + match n3 with + | 0 => x5 + | S m => rec0 m xs + end + end) + with + | nil_R _ _ _ => x2 + | cons_R _ _ _ x5 x6 x7 xs xs0 xs1 => + match + n4 in (nat_R n5 n6) + return + (T1 match n5 with + | 0 => x5 + | S m => rec m xs + end match n6 with + | 0 => x6 + | S m => rec0 m xs0 + end) + with + | O_R => x7 + | S_R m m0 m1 => rec1 m m0 m1 xs xs0 xs1 + end + end) (S x) (S x3) K + end + : forall (T T0 : Type) (T1 : T -> T0 -> Type) (x0 : T) (x1 : T0), + T1 x0 x1 -> + forall n n0 : nat, + nat_R n n0 -> + forall (l : list T) (l0 : list T0), + list_R T T0 T1 l l0 -> T1 (nth T x0 n l) (nth T0 x1 n0 l0) + +Arguments nth_R (T T)%type_scope T%function_scope + x0 x0 x0 (n n)%nat_scope n (l l)%list_scope l Unable to unify "bool" with "nat". Query assignments: Msg = Unable to unify "bool" with "nat". +Query assignments: + MP_TA = «elpi.tests.test_API_module.TA» + MP_TF = «elpi.tests.test_API_module.TF» + Spilled_1 = «elpi.tests.test_API_module.a» + Spilled_2 = const const EXN PRINTING: Not_found +Module +F + : Funsig (a:TA) Funsig (b:TA) TF +:= Functor (a:TA) Functor (b:TA) Struct Definition w : nat. End + +Module B : Sig Parameter w : nat. End := (F A A) + +*** [ B.w : nat ] «myfalse» Query assignments: F = indt «False» GR = «myfalse» myfalse : False -test_inv : Type -> bool -> Type - : Type -> bool -> Type -K1_inv : forall (A : Type) (b : bool), b = true -> test_inv A b - : forall (A : Type) (b : bool), b = true -> test_inv A b -K2_inv -: -forall (A : Type) (b x : bool), -A -> test_inv A (negb x) -> b = negb (negb x) -> test_inv A b - : forall (A : Type) (b x : bool), - A -> test_inv A (negb x) -> b = negb (negb x) -> test_inv A b -Inductive listR_inv (A : Type) (PA : A -> Type) (idx0 : list A) : Type := - nilR_inv : idx0 = nil -> listR_inv A PA idx0 - | consR_inv : forall a : A, - PA a -> - forall xs : list A, - listR_inv A PA xs -> - idx0 = (a :: xs)%list -> listR_inv A PA idx0. - -Arguments listR_inv A%type_scope PA%function_scope idx0%list_scope -Arguments nilR_inv A%type_scope PA%function_scope idx0%list_scope _ -Arguments consR_inv A%type_scope PA%function_scope - idx0%list_scope a _ xs%list_scope _ _ -COQC tests/test_idx2inv.v Query assignments: - MP_TA = «elpi.tests.test_API_module.TA» -Module Type TB = Funsig (A:TA) Sig End + GR = indt «True» «elpi.tests.test_API_elaborate.52» «elpi.tests.test_API_elaborate.52» COQC tests/test_API_arguments.v Query assignments: + MP_TA = «elpi.tests.test_API_module.TA» +Module Type TB = Funsig (A:TA) Sig End +Query assignments: Cons = global (indc «cons») GRCons = indc «cons» GRList = indt «list» @@ -1482,6 +1449,31 @@ WEAK CONSTRAINTS: +pred_R = +fun (n n0 : nat) (n1 : nat_R n n0) => +match + n1 in (nat_R n2 n3) + return + (nat_R match n2 with + | 0 => n + | S u => u + end match n3 with + | 0 => n0 + | S u => u + end) +with +| O_R => n1 +| S_R _ _ u1 => u1 +end + : forall n n0 : nat, nat_R n n0 -> nat_R (Nat.pred n) (Nat.pred n0) + +Arguments pred_R (n n)%nat_scope n +pred_R : nat2nat_R Nat.pred Nat.pred + : nat2nat_R Nat.pred Nat.pred +predn_R : nat2nat_R predn predn + : nat2nat_R predn predn +add_R : nat2nat2nat_R Nat.add Nat.add + : nat2nat2nat_R Nat.add Nat.add parameter T X0 (sort (typ X1)) c0 \ record eq_class (sort (typ X2)) mk_eq_class (field [canonical ff, coercion regular] eq_f (global (indt «bool»)) c1 \ @@ -1489,6 +1481,8 @@ (app [global (indt «eq»), global (indt «bool»), c1, c1]) c2 \ end-record) Query assignments: +File "./tests/test_param2.v", line 85, characters 0-30: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] DECL = parameter T X0 (sort (typ «elpi.tests.test_API_env.1»)) c0 \ record eq_class (sort (typ «elpi.tests.test_API_env.2»)) mk_eq_class (field [canonical ff, coercion regular] eq_f (global (indt «bool»)) c1 \ @@ -1517,17 +1511,7 @@ fun x : eq_class nat => x : bool : eq_class nat -> bool p <- eq_proof ( xxx ) -is_list_to_is_list_inv -: -forall (A : Type) (PA : A -> Type) (l : list A), -is_list A PA l -> is_list_inv A PA l - : forall (A : Type) (PA : A -> Type) (l : list A), - is_list A PA l -> is_list_inv A PA l -COQC tests/test_lens.v -Query assignments: - GR = const «myc» -eq_op myc t t - : bool +COQC tests/test_invert.v foo : nat : nat bar : bool -> nat @@ -1538,7 +1522,34 @@ COQC tests/test_API_notations.v Query assignments: + GR = const «myc» +eq_op myc t t + : bool +test_inv : Type -> bool -> Type + : Type -> bool -> Type +K1_inv : forall (A : Type) (b : bool), b = true -> test_inv A b + : forall (A : Type) (b : bool), b = true -> test_inv A b +K2_inv +: +forall (A : Type) (b x : bool), +A -> test_inv A (negb x) -> b = negb (negb x) -> test_inv A b + : forall (A : Type) (b x : bool), + A -> test_inv A (negb x) -> b = negb (negb x) -> test_inv A b +Inductive listR_inv (A : Type) (PA : A -> Type) (idx0 : list A) : Type := + nilR_inv : idx0 = nil -> listR_inv A PA idx0 + | consR_inv : forall a : A, + PA a -> + forall xs : list A, + listR_inv A PA xs -> + idx0 = (a :: xs)%list -> listR_inv A PA idx0. + +Arguments listR_inv A%type_scope PA%function_scope idx0%list_scope +Arguments nilR_inv A%type_scope PA%function_scope idx0%list_scope _ +Arguments consR_inv A%type_scope PA%function_scope + idx0%list_scope a _ xs%list_scope _ _ +Query assignments: GR = «nat» +COQC tests/test_idx2inv.v Query assignments: DECL = parameter T X0 (sort (typ «elpi.tests.test_API_env.3»)) c0 \ record prim_eq_class (sort (typ «elpi.tests.test_API_env.4»)) @@ -1568,9 +1579,6 @@ r = {| prim_eq_f := r; prim_eq_proof := prim_eq_proof _ r |} (* {} |= prim_eq_class.u1 <= eq.u0 *) Query assignments: - L = [cs-instance (const «carrier») (cs-gref (const «W»)) (const «myc»), - cs-instance (const «eq_op») (cs-gref (const «Z»)) (const «myc»)] -Query assignments: Spilled_1 = «elpi.tests.test_API_module.IA» i : Type @@ -1581,20 +1589,20 @@ X2.imp is not universe polymorphic Arguments X2.imp T%type_scope x _ Expands to: Constant elpi.tests.test_API_arguments.X2.imp -_f1 : Lens fo_record fo_record peano peano - : Lens fo_record fo_record peano peano -_f2 : Lens fo_record fo_record unit unit - : Lens fo_record fo_record unit unit -@_f3 : forall A : Type, Lens (pa_record A) (pa_record A) peano peano - : forall A : Type, Lens (pa_record A) (pa_record A) peano peano -@_f4 : forall A : Type, Lens (pa_record A) (pa_record A) A A - : forall A : Type, Lens (pa_record A) (pa_record A) A A -@_pf3 : forall A : Type, Lens (pr_record A) (pr_record A) peano peano - : forall A : Type, Lens (pr_record A) (pr_record A) peano peano -@_pf4 : forall A : Type, Lens (pr_record A) (pr_record A) A A - : forall A : Type, Lens (pr_record A) (pr_record A) A A -ok -COQC tests/test_tag.v +Query assignments: + L = [cs-instance (const «carrier») (cs-gref (const «W»)) (const «myc»), + cs-instance (const «eq_op») (cs-gref (const «Z»)) (const «myc»)] +fun `r` (app [global (indt «prim_eq_class»), global (indt «nat»)]) c0 \ + app [primitive (proj elpi.tests.test_API_env.prim_eq_f 1), c0] +is_list_to_is_list_inv +: +forall (A : Type) (PA : A -> Type) (l : list A), +is_list A PA l -> is_list_inv A PA l + : forall (A : Type) (PA : A -> Type) (l : list A), + is_list A PA l -> is_list_inv A PA l +Query assignments: + Spilled_1 = «elpi.tests.test_API_module.TA» +Module Type ITA = Sig Parameter z : nat. Parameter i : Type. End global (indt «nat») Query assignments: T = global (indt «nat») @@ -1619,8 +1627,31 @@ WEAK CONSTRAINTS: -fun `r` (app [global (indt «prim_eq_class»), global (indt «nat»)]) c0 \ - app [primitive (proj elpi.tests.test_API_env.prim_eq_f 1), c0] +COQC tests/test_lens.v +Query assignments: + Spilled_1 = const «foo» +foo 3 + : nat +Query assignments: + C = «pc» +Query assignments: + GR = «Nat.add» + MP = «Coq.Init.Datatypes» +Query assignments: + F = «elpi.tests.test_API_module.R.F» + FT = «elpi.tests.test_API_module.R.FT» + L = [submodule «elpi.tests.test_API_module.R.S» [gref (const «R.S.x»)], + module-type «elpi.tests.test_API_module.R.P1», + module-type «elpi.tests.test_API_module.R.P2», + «elpi.tests.test_API_module.R.F» module-functor + [«elpi.tests.test_API_module.R.P1», «elpi.tests.test_API_module.R.P2»], + «elpi.tests.test_API_module.R.FT» module-type-functor + [«elpi.tests.test_API_module.R.P2», «elpi.tests.test_API_module.R.P1»], + gref (const «R.a»)] + P1 = «elpi.tests.test_API_module.R.P1» + P2 = «elpi.tests.test_API_module.R.P2» + R = «elpi.tests.test_API_module.R» + S = «elpi.tests.test_API_module.R.S» «elpi.tests.test_API_notations.abbr» Query assignments: A = «elpi.tests.test_API_notations.abbr» @@ -1643,20 +1674,26 @@ Expands to: Notation elpi.tests.test_API_notations.abbr 4 = 4 : Prop +COQC tests/test_HOAS.v +Query assignments: + Spilled_1 = const «f» + Spilled_2 = const «f» + Spilled_3 = const «f» + Spilled_4 = const «f» + Spilled_5 = const «f» +f : forall [S : Type], S -> Prop + +f is not universe polymorphic +Arguments f [S]%type_scope _ + (where some original arguments have been renamed) +f is transparent +Expands to: Constant elpi.tests.test_API_arguments.f +f (S:=bool * bool) + : bool * bool -> Prop Query assignments: I = «eq» P1 = «carrier» P2 = «eq_op» -Query assignments: - Spilled_1 = «elpi.tests.test_API_module.TA» -Module Type ITA = Sig Parameter z : nat. Parameter i : Type. End -Query assignments: - Spilled_1 = const «foo» -foo 3 - : nat -Query assignments: - GR = «Nat.add» - MP = «Coq.Init.Datatypes» «elpi.tests.test_API_typecheck.10» Query assignments: U = «elpi.tests.test_API_typecheck.10» @@ -1671,8 +1708,32 @@ WEAK CONSTRAINTS: +Universe constraints: +UNIVERSES: + +ALGEBRAIC UNIVERSES: + {myind.u0} +UNDEFINED UNIVERSES: + elpi.tests.test_API_env.5 +WEAK CONSTRAINTS: + + +myind true false : Prop + : Prop +K2 true : myind true true + : myind true true +myind1 true false : Prop + : Prop +K21 true : myind1 true true + : myind1 true true Query assignments: - C = «pc» + A = «elpi.tests.test_API.succ» + GR = «Nat.add» + MP = «Coq.Init.Datatypes» + X1 = [loc-gref (const «Nat.add»)] + X2 = [loc-gref (const «Nat.add»)] + X3 = [loc-abbreviation «elpi.tests.test_API.succ»] + X4 = [loc-modpath «Coq.Init.Datatypes»] Query assignments: _uvk_6_ = X0 _uvk_7_ = X1 @@ -1697,69 +1758,112 @@ GR = const «myc1» eq_op myc1 t1 t1 : bool + {c0} : decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0) + (prod `_` (global (indt «bool»)) c1 \ global (indt «True»)) + (X1 c0) /* suspended on X0, X1 */ +EVARS: + ?X2==[x |- bool -> True] (goal evar) {?Goal} + ?X1==[ |- nat -> bool -> True => fun x : nat => ?Goal] (goal evar) + +SHELF:|| +FUTURE GOALS STACK: + || + +Coq-Elpi mapping: +RAW: +?X2 <-> c0 \ X0 c0 +ELAB: +?X2 <-> X1 + + {c0} : decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0) + (prod `_` (global (indt «bool»)) c1 \ global (indt «True»)) + (X1 c0) /* suspended on X0, X1 */ Query assignments: - F = «elpi.tests.test_API_module.R.F» - FT = «elpi.tests.test_API_module.R.FT» - L = [submodule «elpi.tests.test_API_module.R.S» [gref (const «R.S.x»)], - module-type «elpi.tests.test_API_module.R.P1», - module-type «elpi.tests.test_API_module.R.P2», - «elpi.tests.test_API_module.R.F» module-functor - [«elpi.tests.test_API_module.R.P1», «elpi.tests.test_API_module.R.P2»], - «elpi.tests.test_API_module.R.FT» module-type-functor - [«elpi.tests.test_API_module.R.P2», «elpi.tests.test_API_module.R.P1»], - gref (const «R.a»)] - P1 = «elpi.tests.test_API_module.R.P1» - P2 = «elpi.tests.test_API_module.R.P2» - R = «elpi.tests.test_API_module.R» - S = «elpi.tests.test_API_module.R.S» -COQC tests/test_HOAS.v + type_6 = «elpi.tests.test_API_env.6» + type_7 = «elpi.tests.test_API_env.7» +Universe constraints: +UNIVERSES: + +ALGEBRAIC UNIVERSES: + {nuind.u1 nuind.u0} +UNDEFINED UNIVERSES: + elpi.tests.test_API_env.7 + elpi.tests.test_API_env.6 +WEAK CONSTRAINTS: + + +fun x : nuind nat 3 false => +match x in (nuind _ _ b) return (b = b) with +| k1 _ _ => eq_refl : true = true +| k2 _ _ x0 => (fun _ : nuind nat 1 false => eq_refl : false = false) x0 +end + : nuind nat 3 false -> false = false +Universe constraints: Query assignments: Spilled_1 = const «f» - Spilled_2 = const «f» - Spilled_3 = const «f» - Spilled_4 = const «f» - Spilled_5 = const «f» f : forall [S : Type], S -> Prop f is not universe polymorphic -Arguments f [S]%type_scope _ +Arguments f [S]%type_scope / _ (where some original arguments have been renamed) +The reduction tactics unfold f when applied to 1 argument f is transparent Expands to: Constant elpi.tests.test_API_arguments.f f (S:=bool * bool) : bool * bool -> Prop -Query assignments: - A = «elpi.tests.test_API.succ» - GR = «Nat.add» - MP = «Coq.Init.Datatypes» - X1 = [loc-gref (const «Nat.add»)] - X2 = [loc-gref (const «Nat.add»)] - X3 = [loc-abbreviation «elpi.tests.test_API.succ»] - X4 = [loc-modpath «Coq.Init.Datatypes»] + = fun x : bool => x = x + : bool -> Prop Unable to unify "Set" with "Prop" (universe inconsistency: Cannot enforce Set <= Prop). Query assignments: E = Unable to unify "Set" with "Prop" (universe inconsistency: Cannot enforce Set <= Prop). +Query assignments: + P = const «eq_op» COQC tests/test_arg_HOAS.v +COQC tests/test_quotation.v +_f1 : Lens fo_record fo_record peano peano + : Lens fo_record fo_record peano peano +_f2 : Lens fo_record fo_record unit unit + : Lens fo_record fo_record unit unit +@_f3 : forall A : Type, Lens (pa_record A) (pa_record A) peano peano + : forall A : Type, Lens (pa_record A) (pa_record A) peano peano +@_f4 : forall A : Type, Lens (pa_record A) (pa_record A) A A + : forall A : Type, Lens (pa_record A) (pa_record A) A A +@_pf3 : forall A : Type, Lens (pr_record A) (pr_record A) peano peano + : forall A : Type, Lens (pr_record A) (pr_record A) peano peano +@_pf4 : forall A : Type, Lens (pr_record A) (pr_record A) A A + : forall A : Type, Lens (pr_record A) (pr_record A) A A +ok +COQC tests/test_tag.v +H +[nabla c1 \ + seal + (goal + [decl c1 `H` + (prod `b` + (prod `b` (global (indt «bool»)) c2 \ + app [global (indt «eq»), global (indt «bool»), c2, c2]) c2 \ + global (indt «True»))] (X0 c1) + (prod `b` (global (indt «bool»)) c2 \ + app [global (indt «eq»), global (indt «bool»), c2, c2]) (X1 c1) [])] +c0 global (indt «nat») +Query assignments: + T = global (indt «nat») +Query assignments: + X = «elpi.tests.test_API.1» Universe constraints: UNIVERSES: - + {elpi.tests.test_API.1} |= ALGEBRAIC UNIVERSES: - {myind.u0} + {} UNDEFINED UNIVERSES: - elpi.tests.test_API_env.5 + WEAK CONSTRAINTS: -myind true false : Prop - : Prop -K2 true : myind true true - : myind true true -myind1 true false : Prop - : Prop -K21 true : myind1 true true - : myind1 true true fun `H` X0 c0 \ app [global (indt «eq»), X1 c0, fun `x` X2 c1 \ c1, fun `x` X2 c1 \ c1] Query assignments: @@ -1768,23 +1872,160 @@ app [global (indt «eq»), X1 c0, fun `x` X2 c1 \ c1, fun `x` X2 c1 \ c1] _uvk_11_ = X2 Query assignments: + W = const «W» +[str fun, str in, str as, int 4, str end, str match, str return, str =>, + str :, str :=, str {, str }, str ;, str ,, str |, str x, int 1, str H, + trm + (fun `x` (global (indt «False»)) c0 \ + match c0 (fun `y` (global (indt «False»)) c1 \ global (indt «nat»)) + [])] +Query assignments: + D = parameter A X0 (sort (typ «elpi.tests.test_API_env.10»)) c0 \ + inductive tx X1 + (parameter y X2 (global (indt «nat»)) c1 \ + arity + (prod `_` (global (indt «bool»)) c2 \ + sort (typ «elpi.tests.test_API_env.12»))) c1 \ + [constructor K1x + (parameter y X3 (global (indt «nat»)) c2 \ + arity + (prod `x` c0 c3 \ + prod `n` (global (indt «nat»)) c4 \ + prod `p` + (app + [global (indt «eq»), global (indt «nat»), + app [global (indc «S»), c4], c2]) c5 \ + prod `e` (app [c1, c4, global (indc «true»)]) c6 \ + app [c1, c2, global (indc «true»)])), + constructor K2x + (parameter y X4 (global (indt «nat»)) c2 \ + arity (app [c1, c2, global (indc «false»)]))] + type_8 = «elpi.tests.test_API_env.10» + type_9 = «elpi.tests.test_API_env.12» +Universe constraints: +UNIVERSES: + {elpi.tests.test_API_env.18 elpi.tests.test_API_env.17 + elpi.tests.test_API_env.16 elpi.tests.test_API_env.15 + elpi.tests.test_API_env.14 elpi.tests.test_API_env.13 + elpi.tests.test_API_env.11} |= + tx.u0 < elpi.tests.test_API_env.11 + tx.u1 < elpi.tests.test_API_env.13 + Set <= eq.u0 + Set <= elpi.tests.test_API_env.13 + Set <= elpi.tests.test_API_env.14 + Set <= elpi.tests.test_API_env.15 + Set <= elpi.tests.test_API_env.16 + Set <= elpi.tests.test_API_env.17 + Set <= elpi.tests.test_API_env.18 + tx.u0 <= elpi.tests.test_API_env.14 + tx.u1 <= elpi.tests.test_API_env.14 + elpi.tests.test_API_env.14 <= tx.u1 +ALGEBRAIC UNIVERSES: + {tx.u1 tx.u0} +UNDEFINED UNIVERSES: + elpi.tests.test_API_env.12 + elpi.tests.test_API_env.10 +WEAK CONSTRAINTS: + + +[cs-instance (const «eq_op») (cs-gref (const «Z1»)) (const «myc1»)] +Query assignments: + L = [cs-instance (const «eq_op») (cs-gref (const «Z1»)) (const «myc1»)] P = const «eq_op» + W = const «Z1» Query assignments: - Spilled_1 = const «f» -f : forall [S : Type], S -> Prop + Spilled_1 = «elpi.tests.test_API_notations.abbr2» +COQC tests/test_vernacular1.v +Query assignments: + T = sort (typ «elpi.tests.test_HOAS.3») + U = «elpi.tests.test_HOAS.3» +Query assignments: + X = typ «elpi.tests.test_API.2» + Y = typ «elpi.tests.test_API.3» +Universe constraints: +UNIVERSES: + {elpi.tests.test_API.3 elpi.tests.test_API.2} |= + elpi.tests.test_API.2 <= elpi.tests.test_API.3 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + +Query assignments: + P = const «eq_op» + W = indt «nat» +Query assignments: + D = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ + parameter a explicit c0 c1 \ + inductive ind1 tt + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ + parameter b explicit c2 c3 \ + arity + (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ + prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.26»))) c2 \ + [constructor k1 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + arity + (prod `bb` (app [global (indt «prod»), c3, c3]) c5 \ + prod `_` + (app + [c2, app [global (indt «prod»), c3, c3], c5, + global (indt «bool»), global (indc «true»)]) c6 \ + app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), + constructor k2 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + arity + (app + [c2, c3, c4, global (indt «nat»), + app [global (indc «S»), global (indc «O»)]]))] + D1 = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ + parameter a explicit c0 c1 \ + inductive ind1 tt + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ + parameter b explicit c2 c3 \ + arity + (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ + prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.26»))) c2 \ + [constructor k1 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + arity + (prod `bb` (app [global (indt «prod»), c3, c3]) c5 \ + prod `_` + (app + [c2, app [global (indt «prod»), c3, c3], c5, + global (indt «bool»), global (indc «true»)]) c6 \ + app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), + constructor k2 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + arity + (app + [c2, c3, c4, global (indt «nat»), + app [global (indc «S»), global (indc «O»)]]))] + I = «ind1» + U = «elpi.tests.test_API_env.26» + UA = «elpi.tests.test_API_env.20» + UB1 = «elpi.tests.test_API_env.21» + UB2 = «elpi.tests.test_API_env.21» + UB3 = «elpi.tests.test_API_env.21» + UC = «elpi.tests.test_API_env.22» +Universe constraints: +UNIVERSES: + {elpi.tests.test_API_env.26} |= + Set <= elpi.tests.test_API_env.26 + ind1.u1 <= elpi.tests.test_API_env.26 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + -f is not universe polymorphic -Arguments f [S]%type_scope / _ - (where some original arguments have been renamed) -The reduction tactics unfold f when applied to 1 argument -f is transparent -Expands to: Constant elpi.tests.test_API_arguments.f -f (S:=bool * bool) - : bool * bool -> Prop - = fun x : bool => x = x - : bool -> Prop -COQC tests/test_quotation.v -Universe constraints: empty_tag : tag empty : tag empty unit_tag : tag unit @@ -1827,95 +2068,7 @@ : forall p : peano, tag (ord2 p) val_tag : tag val : tag val -Query assignments: - Spilled_1 = «elpi.tests.test_API_notations.abbr2» -COQC tests/test_eqType_ast.v -COQC tests/test_vernacular1.v - {c0} : decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0) - (prod `_` (global (indt «bool»)) c1 \ global (indt «True»)) - (X1 c0) /* suspended on X0, X1 */ -EVARS: - ?X2==[x |- bool -> True] (goal evar) {?Goal} - ?X1==[ |- nat -> bool -> True => fun x : nat => ?Goal] (goal evar) - -SHELF:|| -FUTURE GOALS STACK: - || - -Coq-Elpi mapping: -RAW: -?X2 <-> c0 \ X0 c0 -ELAB: -?X2 <-> X1 - - {c0} : decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0) - (prod `_` (global (indt «bool»)) c1 \ global (indt «True»)) - (X1 c0) /* suspended on X0, X1 */ -Query assignments: - type_6 = «elpi.tests.test_API_env.6» - type_7 = «elpi.tests.test_API_env.7» -Universe constraints: -UNIVERSES: - -ALGEBRAIC UNIVERSES: - {nuind.u1 nuind.u0} -UNDEFINED UNIVERSES: - elpi.tests.test_API_env.7 - elpi.tests.test_API_env.6 -WEAK CONSTRAINTS: - - -fun x : nuind nat 3 false => -match x in (nuind _ _ b) return (b = b) with -| k1 _ _ => eq_refl : true = true -| k2 _ _ x0 => (fun _ : nuind nat 1 false => eq_refl : false = false) x0 -end - : nuind nat 3 false -> false = false -Query assignments: - W = const «W» test2 -test1 -str hello -test1 -too many arguments -test1 -str hello my -str Dear -test1 -too many arguments -Query assignments: - X = «elpi.tests.test_API.1» -Universe constraints: -UNIVERSES: - {elpi.tests.test_API.1} |= -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - -H -[nabla c1 \ - seal - (goal - [decl c1 `H` - (prod `b` - (prod `b` (global (indt «bool»)) c2 \ - app [global (indt «eq»), global (indt «bool»), c2, c2]) c2 \ - global (indt «True»))] (X0 c1) - (prod `b` (global (indt «bool»)) c2 \ - app [global (indt «eq»), global (indt «bool»), c2, c2]) (X1 c1) [])] -[cs-instance (const «eq_op») (cs-gref (const «Z1»)) (const «myc1»)] -Query assignments: - L = [cs-instance (const «eq_op») (cs-gref (const «Z1»)) (const «myc1»)] - P = const «eq_op» - W = const «Z1» -c0 global (indt «nat») -Query assignments: - T = global (indt «nat») Query assignments: BO = fix `add` 0 (prod `n` (global (indt «nat»)) c0 \ @@ -1929,6 +2082,16 @@ GR = «Nat.add» TY = prod `n` (global (indt «nat»)) c0 \ prod `m` (global (indt «nat»)) c1 \ global (indt «nat») +test1 +str hello +COQC tests/test_eqType_ast.v +test1 +too many arguments +test1 +str hello my +str Dear +test1 +too many arguments raw: parameter A1 maximal (sort (typ «elpi.tests.test_arg_HOAS.2»)) c0 \ parameter A2 explicit c0 c1 \ @@ -2003,6 +2166,76 @@ ?B1 : [ |- Type] ?B2 : [ |- Type] ?f : [ |- foo1 ?A2 (?B1 * ?B1) ?B2 3] +Query assignments: + D = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ + parameter a explicit c0 c1 \ + inductive ind1 tt + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ + parameter b explicit c2 c3 \ + arity + (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ + prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.27»))) c2 \ + [constructor k1 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + parameter bb implicit (app [global (indt «prod»), c3, c3]) c5 \ + arity + (prod `_` + (app + [c2, app [global (indt «prod»), c3, c3], c5, + global (indt «bool»), global (indc «true»)]) c6 \ + app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), + constructor k2 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + arity + (app + [c2, c3, c4, global (indt «nat»), + app [global (indc «S»), global (indc «O»)]]))] + D1 = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ + parameter a explicit c0 c1 \ + inductive ind1 tt + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ + parameter b explicit c2 c3 \ + arity + (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ + prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.27»))) c2 \ + [constructor k1 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + parameter bb implicit (app [global (indt «prod»), c3, c3]) c5 \ + arity + (prod `_` + (app + [c2, app [global (indt «prod»), c3, c3], c5, + global (indt «bool»), global (indc «true»)]) c6 \ + app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), + constructor k2 + (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ + parameter b explicit c3 c4 \ + arity + (app + [c2, c3, c4, global (indt «nat»), + app [global (indc «S»), global (indc «O»)]]))] + I = «ind1» + U = «elpi.tests.test_API_env.27» + UA = «elpi.tests.test_API_env.20» + UB1 = «elpi.tests.test_API_env.21» + UB2 = «elpi.tests.test_API_env.21» + UB3 = «elpi.tests.test_API_env.21» + UC = «elpi.tests.test_API_env.22» +Universe constraints: +UNIVERSES: + {elpi.tests.test_API_env.27} |= + Set <= elpi.tests.test_API_env.27 + ind1.u1 <= elpi.tests.test_API_env.27 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + raw: parameter A1 maximal X0 c0 \ parameter A2 explicit c0 c1 \ @@ -2078,12 +2311,12 @@ ?B2 : [ |- Type] ?f : [ |- foo1 ?A2 (?B1 * ?B1) ?B2 3] Query assignments: - X = typ «elpi.tests.test_API.2» - Y = typ «elpi.tests.test_API.3» + X = typ «elpi.tests.test_API.4» + Y = typ «elpi.tests.test_API.5» Universe constraints: UNIVERSES: - {elpi.tests.test_API.3 elpi.tests.test_API.2} |= - elpi.tests.test_API.2 <= elpi.tests.test_API.3 + {elpi.tests.test_API.5 elpi.tests.test_API.4} |= + elpi.tests.test_API.4 <= elpi.tests.test_API.5 ALGEBRAIC UNIVERSES: {} UNDEFINED UNIVERSES: @@ -2091,15 +2324,6 @@ WEAK CONSTRAINTS: -[str fun, str in, str as, int 4, str end, str match, str return, str =>, - str :, str :=, str {, str }, str ;, str ,, str |, str x, int 1, str H, - trm - (fun `x` (global (indt «False»)) c0 \ - match c0 (fun `y` (global (indt «False»)) c1 \ global (indt «nat»)) - [])] -Query assignments: - P = const «eq_op» - W = indt «nat» fix X0 0 (prod `n` (global (indt «nat»)) c0 \ prod `m` (global (indt «nat»)) c1 \ global (indt «nat»)) c0 \ @@ -2145,76 +2369,18 @@ Query assignments: - D = parameter A X0 (sort (typ «elpi.tests.test_API_env.10»)) c0 \ - inductive tx X1 - (parameter y X2 (global (indt «nat»)) c1 \ - arity - (prod `_` (global (indt «bool»)) c2 \ - sort (typ «elpi.tests.test_API_env.12»))) c1 \ - [constructor K1x - (parameter y X3 (global (indt «nat»)) c2 \ - arity - (prod `x` c0 c3 \ - prod `n` (global (indt «nat»)) c4 \ - prod `p` - (app - [global (indt «eq»), global (indt «nat»), - app [global (indc «S»), c4], c2]) c5 \ - prod `e` (app [c1, c4, global (indc «true»)]) c6 \ - app [c1, c2, global (indc «true»)])), - constructor K2x - (parameter y X4 (global (indt «nat»)) c2 \ - arity (app [c1, c2, global (indc «false»)]))] - type_8 = «elpi.tests.test_API_env.10» - type_9 = «elpi.tests.test_API_env.12» -Universe constraints: -UNIVERSES: - {elpi.tests.test_API_env.18 elpi.tests.test_API_env.17 - elpi.tests.test_API_env.16 elpi.tests.test_API_env.15 - elpi.tests.test_API_env.14 elpi.tests.test_API_env.13 - elpi.tests.test_API_env.11} |= - tx.u0 < elpi.tests.test_API_env.11 - tx.u1 < elpi.tests.test_API_env.13 - Set <= eq.u0 - Set <= elpi.tests.test_API_env.13 - Set <= elpi.tests.test_API_env.14 - Set <= elpi.tests.test_API_env.15 - Set <= elpi.tests.test_API_env.16 - Set <= elpi.tests.test_API_env.17 - Set <= elpi.tests.test_API_env.18 - tx.u0 <= elpi.tests.test_API_env.14 - tx.u1 <= elpi.tests.test_API_env.14 - elpi.tests.test_API_env.14 <= tx.u1 -ALGEBRAIC UNIVERSES: - {tx.u1 tx.u0} -UNDEFINED UNIVERSES: - elpi.tests.test_API_env.12 - elpi.tests.test_API_env.10 -WEAK CONSTRAINTS: - - -[attribute elpi.loc - (leaf-loc - File "./tests/test_vernacular1.v", line 48, column 5, character 947:), - attribute foo (leaf-str bar)] -[get-option elpi.loc - File "./tests/test_vernacular1.v", line 48, column 5, character 947:, - get-option foo bar] -[attribute elpi.loc - (leaf-loc - File "./tests/test_vernacular1.v", line 52, column 0, character 981:), - attribute foo (leaf-str bar), attribute poly (leaf-str )] -[get-option elpi.loc - File "./tests/test_vernacular1.v", line 52, column 0, character 981:, - get-option foo bar, get-option poly tt] -[attribute elpi.loc - (leaf-loc - File "./tests/test_vernacular1.v", line 53, column 0, character 1009:), - attribute foo (leaf-str bar), attribute poly (leaf-str ), - attribute suppa (node [attribute duppa (leaf-str )])] -[get-option elpi.loc - File "./tests/test_vernacular1.v", line 53, column 0, character 1009:, - get-option foo bar, get-option poly tt] + C1 = const «C1» + GR1 = const «c12» + GR2 = const «c1t» + GR3 = const «c1f» +fun x : C1 => x : C2 + : C1 -> C2 +fun (x : C1) (_ : x) => true + : forall x : C1, x -> bool +fun x : C1 => x 3 + : C1 -> nat +Query assignments: + U = «elpi.tests.test_HOAS.5» Query assignments: D = parameter A explicit (sort (typ «elpi.tests.test_arg_HOAS.79»)) c0 \ inductive t tt @@ -2309,12 +2475,14 @@ app [global (indt «eq»), c0, app [c2, c5, c5], c5]) c4 \ end-record) Query assignments: - X = typ «elpi.tests.test_API.4» - Y = typ «elpi.tests.test_API.5» + X = typ «elpi.tests.test_API.6» + Y = typ «elpi.tests.test_API.7» + Z = typ «elpi.tests.test_API.8» Universe constraints: UNIVERSES: - {elpi.tests.test_API.5 elpi.tests.test_API.4} |= - elpi.tests.test_API.4 <= elpi.tests.test_API.5 + {elpi.tests.test_API.8 elpi.tests.test_API.7 elpi.tests.test_API.6} |= + elpi.tests.test_API.6 <= elpi.tests.test_API.8 + elpi.tests.test_API.7 <= elpi.tests.test_API.8 ALGEBRAIC UNIVERSES: {} UNDEFINED UNIVERSES: @@ -2323,90 +2491,21 @@ Query assignments: - T = sort (typ «elpi.tests.test_HOAS.3») - U = «elpi.tests.test_HOAS.3» -Query assignments: - C1 = const «C1» - GR1 = const «c12» - GR2 = const «c1t» - GR3 = const «c1f» -fun x : C1 => x : C2 - : C1 -> C2 -fun (x : C1) (_ : x) => true - : forall x : C1, x -> bool -fun x : C1 => x 3 - : C1 -> nat -COQC examples/usage.v -Query assignments: - D = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ - parameter a explicit c0 c1 \ - inductive ind1 tt - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ - parameter b explicit c2 c3 \ - arity - (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ - prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.26»))) c2 \ - [constructor k1 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - arity - (prod `bb` (app [global (indt «prod»), c3, c3]) c5 \ - prod `_` - (app - [c2, app [global (indt «prod»), c3, c3], c5, - global (indt «bool»), global (indc «true»)]) c6 \ - app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), - constructor k2 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - arity - (app - [c2, c3, c4, global (indt «nat»), - app [global (indc «S»), global (indc «O»)]]))] - D1 = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ - parameter a explicit c0 c1 \ - inductive ind1 tt - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ - parameter b explicit c2 c3 \ - arity - (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ - prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.26»))) c2 \ - [constructor k1 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - arity - (prod `bb` (app [global (indt «prod»), c3, c3]) c5 \ - prod `_` - (app - [c2, app [global (indt «prod»), c3, c3], c5, - global (indt «bool»), global (indc «true»)]) c6 \ - app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), - constructor k2 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - arity - (app - [c2, c3, c4, global (indt «nat»), - app [global (indc «S»), global (indc «O»)]]))] - I = «ind1» - U = «elpi.tests.test_API_env.26» - UA = «elpi.tests.test_API_env.20» - UB1 = «elpi.tests.test_API_env.21» - UB2 = «elpi.tests.test_API_env.21» - UB3 = «elpi.tests.test_API_env.21» - UC = «elpi.tests.test_API_env.22» -Universe constraints: -UNIVERSES: - {elpi.tests.test_API_env.26} |= - Set <= elpi.tests.test_API_env.26 - ind1.u1 <= elpi.tests.test_API_env.26 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - + D = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ + parameter p explicit c0 c1 \ + record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 + (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ + field [coercion off, canonical ff] f2 + (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) + D1 = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ + parameter p explicit c0 c1 \ + record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 + (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ + field [coercion off, canonical ff] f2 + (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) + I = «r1» + UP = «elpi.tests.test_API_env.28» + UR = «elpi.tests.test_API_env.28» fun `v` (app [global (indt «Vector.t»), global (indt «nat»), @@ -2540,22 +2639,6 @@ Query assignments: - X = typ «elpi.tests.test_API.6» - Y = typ «elpi.tests.test_API.7» - Z = typ «elpi.tests.test_API.8» -Universe constraints: -UNIVERSES: - {elpi.tests.test_API.8 elpi.tests.test_API.7 elpi.tests.test_API.6} |= - elpi.tests.test_API.6 <= elpi.tests.test_API.8 - elpi.tests.test_API.7 <= elpi.tests.test_API.8 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - -Query assignments: I = «foo» raw: parameter A explicit X0 c0 \ @@ -2598,77 +2681,62 @@ app [global (indt «eq»), c0, app [c2, c5, c5], c5]) c4 \ end-record) Query assignments: + X = typ «elpi.tests.test_API.9» + Y = typ «elpi.tests.test_API.10» +Universe constraints: +UNIVERSES: + {elpi.tests.test_API.10 elpi.tests.test_API.9} |= + elpi.tests.test_API.9 < elpi.tests.test_API.10 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + +Query assignments: L = [coercion (const «c1t») 0 (const «C1») sortclass, coercion (const «c1f») 0 (const «C1») funclass, coercion (const «c12») 0 (const «C1») (grefclass (const «C2»))] -3 Query assignments: - X = 3 + D = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ + parameter p explicit c0 c1 \ + record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 + (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ + field [coercion regular, canonical ff] f2 + (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) + D1 = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ + parameter p explicit c0 c1 \ + record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 + (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ + field [coercion regular, canonical ff] f2 + (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) + I = «r1» + UP = «elpi.tests.test_API_env.28» + UR = «elpi.tests.test_API_env.28» +3 Query assignments: X = 3 Query assignments: - D = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ - parameter a explicit c0 c1 \ - inductive ind1 tt - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ - parameter b explicit c2 c3 \ - arity - (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ - prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.27»))) c2 \ - [constructor k1 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - parameter bb implicit (app [global (indt «prod»), c3, c3]) c5 \ - arity - (prod `_` - (app - [c2, app [global (indt «prod»), c3, c3], c5, - global (indt «bool»), global (indc «true»)]) c6 \ - app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), - constructor k2 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - arity - (app - [c2, c3, c4, global (indt «nat»), - app [global (indc «S»), global (indc «O»)]]))] - D1 = parameter A explicit (sort (typ «elpi.tests.test_API_env.20»)) c0 \ - parameter a explicit c0 c1 \ - inductive ind1 tt - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c2 \ - parameter b explicit c2 c3 \ - arity - (prod `C` (sort (typ «elpi.tests.test_API_env.22»)) c4 \ - prod `_` c4 c5 \ sort (typ «elpi.tests.test_API_env.27»))) c2 \ - [constructor k1 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - parameter bb implicit (app [global (indt «prod»), c3, c3]) c5 \ - arity - (prod `_` - (app - [c2, app [global (indt «prod»), c3, c3], c5, - global (indt «bool»), global (indc «true»)]) c6 \ - app [c2, c3, c4, global (indt «unit»), global (indc «tt»)])), - constructor k2 - (parameter B explicit (sort (typ «elpi.tests.test_API_env.21»)) c3 \ - parameter b explicit c3 c4 \ - arity - (app - [c2, c3, c4, global (indt «nat»), - app [global (indc «S»), global (indc «O»)]]))] - I = «ind1» - U = «elpi.tests.test_API_env.27» - UA = «elpi.tests.test_API_env.20» - UB1 = «elpi.tests.test_API_env.21» - UB2 = «elpi.tests.test_API_env.21» - UB3 = «elpi.tests.test_API_env.21» - UC = «elpi.tests.test_API_env.22» + X = c0 \ c1 \ c2 \ +X0 c0 c1 c2 + _uvk_19_ = global (indt «nat») +Syntactic constraints: + {c0 c1 c2 c3 c4 c5 c6} : + decl c6 `z` (app [global (const «N»), c5]), + decl c5 `x` (global (indt «nat»)), + decl c4 `a` (global (indt «bool»)) + ?- evar (X0 c4 c5 c6) (X1 c4 c5 c6) (X0 c4 c5 c6) /* suspended on X0 */ + {c0 c1 c2 c3 c4 c5 c6} : + decl c6 `z` (app [global (const «N»), c5]), + decl c5 `x` (global (indt «nat»)), + decl c4 `a` (global (indt «bool»)) + ?- evar (X2 c4 c5 c6) (sort (typ «elpi.tests.test_HOAS.9»)) + (X1 c4 c5 c6) /* suspended on X2, X1 */ Universe constraints: UNIVERSES: - {elpi.tests.test_API_env.27} |= - Set <= elpi.tests.test_API_env.27 - ind1.u1 <= elpi.tests.test_API_env.27 + {elpi.tests.test_HOAS.9 elpi.tests.test_HOAS.8} |= + Set <= elpi.tests.test_HOAS.8 ALGEBRAIC UNIVERSES: {} UNDEFINED UNIVERSES: @@ -2676,8 +2744,6 @@ WEAK CONSTRAINTS: -app [global (const «Nat.mul»), X0, X1] type -COQC tests/test_tactic.v Query assignments: I = «foo» x1 : forall P : Type, P -> nat -> nat @@ -2692,22 +2758,36 @@ : x1 = (fun (P : Type) (_ : P) (n : nat) => n + 1) y : nat -> Type : nat -> Type +COQC examples/usage.v +[attribute elpi.loc + (leaf-loc + File "./tests/test_vernacular1.v", line 48, column 5, character 947:), + attribute foo (leaf-str bar)] +[get-option elpi.loc + File "./tests/test_vernacular1.v", line 48, column 5, character 947:, + get-option foo bar] +[attribute elpi.loc + (leaf-loc + File "./tests/test_vernacular1.v", line 52, column 0, character 981:), + attribute foo (leaf-str bar), attribute poly (leaf-str )] +[get-option elpi.loc + File "./tests/test_vernacular1.v", line 52, column 0, character 981:, + get-option foo bar, get-option poly tt] +[attribute elpi.loc + (leaf-loc + File "./tests/test_vernacular1.v", line 53, column 0, character 1009:), + attribute foo (leaf-str bar), attribute poly (leaf-str ), + attribute suppa (node [attribute duppa (leaf-str )])] +[get-option elpi.loc + File "./tests/test_vernacular1.v", line 53, column 0, character 1009:, + get-option foo bar, get-option poly tt] +fun `x` X0 c0 \ app [X1, c0] Query assignments: - X = typ «elpi.tests.test_API.9» - Y = typ «elpi.tests.test_API.10» -Universe constraints: -UNIVERSES: - {elpi.tests.test_API.10 elpi.tests.test_API.9} |= - elpi.tests.test_API.9 < elpi.tests.test_API.10 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - -Query assignments: - U = «elpi.tests.test_HOAS.5» + X = X1 + Y = fun `x` X0 c0 \ app [X1, c0] + _uvk_34_ = X0 +File "coq-builtin.elpi", line 1470, characters 0-93: +Warning: constant get-option has no declared type. [elpi.typecheck,elpi] Query assignments: Spilled_1 = const «nuc» nuc : forall x : nat, C1 -> C3 x @@ -2716,80 +2796,40 @@ Arguments nuc x%nat_scope _ nuc is a reversible coercion Expands to: Constant elpi.tests.test_API_TC_CS.nuc -COQC tests/test_elaborator.v -more : (forall A : Type, A -> tickle A -> tickle A) - : forall A : Type, A -> tickle A -> tickle A -tickle.eqb - : (forall A : Type, (A -> A -> bool) -> tickle A -> tickle A -> bool) - : forall A : Type, (A -> A -> bool) -> tickle A -> tickle A -> bool -tickle.eqb_OK - : (forall (A : Type) (f : A -> A -> bool), - (forall x y : A, reflect (x = y) (f x y)) -> - forall x y : tickle A, reflect (x = y) (tickle.eqb A f x y)) - : forall (A : Type) (f : A -> A -> bool), - (forall x y : A, reflect (x = y) (f x y)) -> - forall x y : tickle A, reflect (x = y) (tickle.eqb A f x y) -tickle.map : (forall A B : Type, (A -> B) -> tickle A -> tickle B) - : forall A B : Type, (A -> B) -> tickle A -> tickle B -tickle.tickle_R - : (forall A B : Type, (A -> B -> Type) -> tickle A -> tickle B -> Type) - : forall A B : Type, (A -> B -> Type) -> tickle A -> tickle B -> Type -fun `x` X0 c0 \ app [X1, c0] +fun `r` (global (indt «nat»)) c0 \ + fun `p` + (prod `y` (global (indt «nat»)) c1 \ + app + [global (indt «eq»), global (indt «nat»), c1, global (indc «O»)]) + c1 \ + fun `q` (global (indt «bool»)) c2 \ + prod `y` (global (indt «nat»)) c3 \ + app + [global (indt «eq»), global (indt «nat»), c3, global (indc «O»)] Query assignments: - X = X1 - Y = fun `x` X0 c0 \ app [X1, c0] - _uvk_34_ = X0 -Starting module rtree -Declaring inductive -parameter A explicit (sort (typ «elpi.apps.derive.examples.usage.190»)) - c0 \ - inductive rtree tt - (arity (sort (typ «elpi.apps.derive.examples.usage.191»))) c1 \ - [constructor Leaf (arity (prod `_` c0 c2 \ c1)), - constructor Node - (arity (prod `_` (app [global (indt «tickle.tickle»), c1]) c2 \ c1))] -Deriving -Derivation map on indt «rtree» -Derivation map on indt «rtree» took 0.013942 -Derivation lens on indt «rtree» -Derivation lens on indt «rtree» failed, continuing -Derivation param1 on indt «rtree» -Derivation param1 on indt «rtree» took 0.034608 -Derivation param2 on indt «rtree» -Derivation param2 on indt «rtree» took 0.040975 -Derivation tag on indt «rtree» -File "coq-builtin.elpi", line 1470, characters 0-93: -Warning: constant get-option has no declared type. [elpi.typecheck,elpi] -Derivation tag on indt «rtree» took 0.007694 -Derivation eqType_ast on indt «rtree» -Derivation eqType_ast on indt «rtree» took 0.003808 -Derivation lens_laws on indt «rtree» -Derivation lens_laws on indt «rtree» took 0.002532 -Derivation param1_congr on indt «rtree» -Derivation param1_congr on indt «rtree» took 0.015718 -Derivation param1_inhab on indt «rtree» -Derivation param1_inhab on indt «rtree» took 0.013171 -Derivation param1_functor on indt «rtree» -Derivation param1_functor on indt «rtree» took 0.012810 -Derivation fields on indt «rtree» -Derivation fields on indt «rtree» took 0.147934 -Derivation param1_trivial on indt «rtree» + Spilled_1 = c0 \ c1 \ c2 \ +prod `y` (global (indt «nat»)) c3 \ + app [global (indt «eq»), global (indt «nat»), c3, global (indc «O»)] + X = fun `r` (global (indt «nat»)) c0 \ + fun `p` + (prod `y` (global (indt «nat»)) c1 \ + app + [global (indt «eq»), global (indt «nat»), c1, global (indc «O»)]) + c1 \ + fun `q` (global (indt «bool»)) c2 \ + prod `y` (global (indt «nat»)) c3 \ + app + [global (indt «eq»), global (indt «nat»), c3, global (indc «O»)] +fun u : nat => +{| val := oval u; Sub := Ord u; Sub_rect := inlined_sub_rect |} + : forall u : nat, is_SUB nat (fun x : nat => leq x u) (ord u) +COQC tests/test_tactic.v +{{ nat; S; }} +{{ nat; S; }} Query assignments: - D = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ - parameter p explicit c0 c1 \ - record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 - (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ - field [coercion off, canonical ff] f2 - (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) - D1 = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ - parameter p explicit c0 c1 \ - record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 - (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ - field [coercion off, canonical ff] f2 - (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) - I = «r1» - UP = «elpi.tests.test_API_env.28» - UR = «elpi.tests.test_API_env.28» + GR = const «Nat.add» + L = {{ nat; S; }} + S = {{ nat; S; }} parameter A1 maximal (sort (typ «elpi.tests.test_arg_HOAS.2»)) c0 \ parameter A2 explicit c0 c1 \ inductive foo1 tt @@ -2819,33 +2859,6 @@ (prod `_` c0 c5 \ app [c2, c3, c4, app [global (indc «S»), global (indc «O»)]]))] Query assignments: - X = c0 \ c1 \ c2 \ -X0 c0 c1 c2 - _uvk_19_ = global (indt «nat») -Syntactic constraints: - {c0 c1 c2 c3 c4 c5 c6} : - decl c6 `z` (app [global (const «N»), c5]), - decl c5 `x` (global (indt «nat»)), - decl c4 `a` (global (indt «bool»)) - ?- evar (X0 c4 c5 c6) (X1 c4 c5 c6) (X0 c4 c5 c6) /* suspended on X0 */ - {c0 c1 c2 c3 c4 c5 c6} : - decl c6 `z` (app [global (const «N»), c5]), - decl c5 `x` (global (indt «nat»)), - decl c4 `a` (global (indt «bool»)) - ?- evar (X2 c4 c5 c6) (sort (typ «elpi.tests.test_HOAS.9»)) - (X1 c4 c5 c6) /* suspended on X2, X1 */ -Universe constraints: -UNIVERSES: - {elpi.tests.test_HOAS.9 elpi.tests.test_HOAS.8} |= - Set <= elpi.tests.test_HOAS.8 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - -Query assignments: D = parameter A1 maximal (sort (typ «elpi.tests.test_arg_HOAS.2»)) c0 \ parameter A2 explicit c0 c1 \ inductive foo1 tt @@ -2883,30 +2896,6 @@ ?B1 : [ |- Type] ?B2 : [ |- Type] ?n : [ |- nat] -fun `r` (global (indt «nat»)) c0 \ - fun `p` - (prod `y` (global (indt «nat»)) c1 \ - app - [global (indt «eq»), global (indt «nat»), c1, global (indc «O»)]) - c1 \ - fun `q` (global (indt «bool»)) c2 \ - prod `y` (global (indt «nat»)) c3 \ - app - [global (indt «eq»), global (indt «nat»), c3, global (indc «O»)] -Query assignments: - Spilled_1 = c0 \ c1 \ c2 \ -prod `y` (global (indt «nat»)) c3 \ - app [global (indt «eq»), global (indt «nat»), c3, global (indc «O»)] - X = fun `r` (global (indt «nat»)) c0 \ - fun `p` - (prod `y` (global (indt «nat»)) c1 \ - app - [global (indt «eq»), global (indt «nat»), c1, global (indc «O»)]) - c1 \ - fun `q` (global (indt «bool»)) c2 \ - prod `y` (global (indt «nat»)) c3 \ - app - [global (indt «eq»), global (indt «nat»), c3, global (indc «O»)] a_k1 ?A2 ?B1 ?B2 3 ?f : foo1 ?A2 ?B1 ?B2 3 : foo1 ?A2 ?B1 ?B2 3 where @@ -2915,30 +2904,6 @@ ?B1 : [ |- Type] ?B2 : [ |- Type] ?f : [ |- foo1 ?A2 (?B1 * ?B1) ?B2 3] -fun u : nat => -{| val := oval u; Sub := Ord u; Sub_rect := inlined_sub_rect |} - : forall u : nat, is_SUB nat (fun x : nat => leq x u) (ord u) -Derivation param1_trivial on indt «rtree» took 0.290211 -Derivation induction on indt «rtree» -Derivation induction on indt «rtree» took 0.010367 -Derivation eqb on indt «rtree» -Derivation eqb on indt «rtree» took 0.071704 -Derivation eqbcorrect on indt «rtree» -Derivation eqbcorrect on indt «rtree» took 0.116500 -Derivation eqbOK on indt «rtree» -Derivation eqbOK on indt «rtree» took 0.008130 -Done -rtree.induction - : (forall (A : Type) (PA : A -> Type) (P : rtree A -> Type), - (forall a : A, PA a -> P (Leaf A a)) -> - (forall l : tickle (rtree A), - tickle.is_tickle (rtree A) P l -> P (Node A l)) -> - forall x : rtree A, rtree.is_rtree A PA x -> P x) - : forall (A : Type) (PA : A -> Type) (P : rtree A -> Type), - (forall a : A, PA a -> P (Leaf A a)) -> - (forall l : tickle (rtree A), - tickle.is_tickle (rtree A) P l -> P (Node A l)) -> - forall x : rtree A, rtree.is_rtree A PA x -> P x Query assignments: GR = indc «Ord» K = global (indc «Ord») @@ -3036,87 +3001,62 @@ WEAK CONSTRAINTS: -Starting module Box -Declaring inductive -parameter A explicit (sort (typ «elpi.apps.derive.examples.usage.379»)) - c0 \ - record Box (sort (typ «elpi.apps.derive.examples.usage.380»)) Build_Box - (field [coercion off, canonical tt] contents c0 c1 \ - field [coercion off, canonical tt] tag (global (indt «nat»)) c2 \ - end-record) -Deriving -Skipping derivation map on indt «Box» since the user did not select it -Derivation lens on indt «Box» -Derivation lens on indt «Box» took 0.020289 -Skipping derivation param1 on indt «Box» since the user did not select it -Skipping derivation param2 on indt «Box» since the user did not select it -Derivation tag on indt «Box» -File "./examples/usage.v", line 53, characters 0-84: -Warning: Global name tag is taken, using tag1 instead [elpi.renamed,elpi] -Derivation tag on indt «Box» took 0.007479 -Derivation eqType_ast on indt «Box» -Derivation eqType_ast on indt «Box» took 0.003322 -Derivation lens_laws on indt «Box» -Derivation lens_laws on indt «Box» took 0.056392 -Skipping derivation param1_congr on indt «Box» -since the user did not select it -Skipping derivation param1_inhab on indt «Box» -since the user did not select it -Skipping derivation param1_functor on indt «Box» -since the user did not select it -Derivation fields on indt «Box» -Derivation fields on indt «Box» took 0.024691 -Skipping derivation param1_trivial on indt «Box» -since the user did not select it -Skipping derivation induction on indt «Box» -since the user did not select it -Derivation eqb on indt «Box» -Derivation eqb on indt «Box» took 0.020257 -Skipping derivation eqbcorrect on indt «Box» -since the user did not select it -Skipping derivation eqbOK on indt «Box» since the user did not select it -Done -Box.eqb : (forall A : Type, (A -> A -> bool) -> Box A -> Box A -> bool) - : forall A : Type, (A -> A -> bool) -> Box A -> Box A -> bool -@Box._tag : (forall A : Type, Lens (Box A) (Box A) nat nat) - : forall A : Type, Lens (Box A) (Box A) nat nat -Box._tag_set_set - : (forall (A : Type) (r : Box A) (y x : nat), - set Box._tag x (set Box._tag y r) = set Box._tag x r) - : forall (A : Type) (r : Box A) (y x : nat), - set Box._tag x (set Box._tag y r) = set Box._tag x r -Box._tag_contents_exchange - : (forall (A : Type) (r : Box A) (x : nat) (y : A), - set Box._tag x (set Box._contents y r) = - set Box._contents y (set Box._tag x r)) - : forall (A : Type) (r : Box A) (x : nat) (y : A), - set Box._tag x (set Box._contents y r) = - set Box._contents y (set Box._tag x r) -nat_eqb_OK : (forall x y : nat, reflect (x = y) (nat_eqb x y)) - : forall x y : nat, reflect (x = y) (nat_eqb x y) +COQC tests/test_elaborator.v Query assignments: - D = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ - parameter p explicit c0 c1 \ - record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 - (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ - field [coercion regular, canonical ff] f2 - (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) - D1 = parameter P explicit (sort (typ «elpi.tests.test_API_env.28»)) c0 \ - parameter p explicit c0 c1 \ - record r1 (sort (typ «elpi.tests.test_API_env.28»)) mk_r1 - (field [coercion reversible, canonical tt] f1 (prod `_` c0 c2 \ c0) c2 \ - field [coercion regular, canonical ff] f2 - (app [global (indt «eq»), c0, c1, app [c2, c1]]) c3 \ end-record) - I = «r1» - UP = «elpi.tests.test_API_env.28» - UR = «elpi.tests.test_API_env.28» -Derivation map on indt «a» -Derivation map on indt «a» took 0.008149 -Derivation lens on indt «a» -Derivation lens on indt «a» failed, continuing -Derivation param1 on indt «a» -Derivation param1 on indt «a» took 0.017828 -Derivation param2 on indt «a» + X = 3 +app [global (const «Nat.mul»), X0, X1] type +COQC tests/test_ltac.v +{{ X.a; }} {{ X.a; Nat.add; nat; }} +{{ X.a; }} {{ X.a; Nat.add; nat; O; S; }} +Query assignments: + AllL = {{ X.a; Nat.add; nat; }} + AllS = {{ X.a; Nat.add; nat; O; S; }} + GR = const «X.b» + L = {{ X.a; }} + M = «elpi.tests.test_API_env.HOAS.X» + S = {{ X.a; }} + Spilled_1 = const «X.a» +---------------------------------- + {c0 c1} : decl c1 `a` (global (indt «bool»)) + ?- evar X0 (sort (typ «elpi.tests.test_HOAS.10»)) X1 /* suspended on X0, X1 */ + {c0 c1} : decl c1 `a` (global (indt «bool»)) ?- evar (X2 c1) X1 (X2 c1) /* suspended on X2 */ +EVARS: + ?X11==[a |- ?elpi_evar] (internal placeholder) {?elpi_evar0} + ?X10==[ |- Type] (internal placeholder) {?elpi_evar} + ?X9==[a |- ?elpi_evar => ?elpi_evar0] (internal placeholder) + ?X8==[a |- Type => ?elpi_evar] (internal placeholder) + +SHELF: +FUTURE GOALS STACK:?X11 +?X10 + +Coq-Elpi mapping: +RAW: +?X10 <-> X0 +?X11 <-> X2 +ELAB: +?X10 <-> X1 +?X11 <-> X2 + +X2 c0 : X1 +Query assignments: + TY = X1 + X = c0 \ c1 \ +X2 c0 +Syntactic constraints: + {c0 c1} : decl c1 `a` (global (indt «bool»)) + ?- evar X0 (sort (typ «elpi.tests.test_HOAS.10»)) X1 /* suspended on X0, X1 */ + {c0 c1} : decl c1 `a` (global (indt «bool»)) ?- evar (X2 c1) X1 (X2 c1) /* suspended on X2 */ +Universe constraints: +UNIVERSES: + {elpi.tests.test_HOAS.10} |= +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + Query assignments: I = «inductive_nup.r» R = parameter A explicit (sort (typ «elpi.tests.test_arg_HOAS.31»)) c0 \ @@ -3132,68 +3072,79 @@ Arguments R A%type_scope a f%function_scope g p raw: inductive X1 tt (arity (sort prop)) c0 \ [] typed: inductive X1 tt (arity (sort prop)) c0 \ [] -Derivation param2 on indt «a» took 0.019112 -Derivation tag on indt «a» -Derivation tag on indt «a» took 0.005460 -Derivation eqType_ast on indt «a» X1 : Prop X1 is not universe polymorphic Expands to: Inductive elpi.tests.test_arg_HOAS.X1 -Derivation eqType_ast on indt «a» took 0.003006 -Derivation lens_laws on indt «a» -Derivation lens_laws on indt «a» took 0.002462 -Derivation param1_congr on indt «a» -Derivation param1_congr on indt «a» took 0.003438 -Derivation param1_inhab on indt «a» -Derivation param1_inhab on indt «a» took 0.007707 -Derivation param1_functor on indt «a» -Derivation param1_functor on indt «a» took 0.007458 -Derivation fields on indt «a» -COQC tests/test_ltac.v -Derivation fields on indt «a» took 0.016582 -Derivation param1_trivial on indt «a» -Derivation param1_trivial on indt «a» took 0.009821 -Derivation induction on indt «a» -Derivation induction on indt «a» took 0.006118 -Derivation eqb on indt «a» -Derivation eqb on indt «a» took 0.013696 -Derivation eqbcorrect on indt «a» -Derivation eqbcorrect on indt «a» took 0.020632 -Derivation eqbOK on indt «a» -Derivation eqbOK on indt «a» took 0.004915 -Skipping derivation map on indt «b» since the user did not select it -Skipping derivation lens on indt «b» since the user did not select it -Derivation param1 on indt «b» -Derivation param1 on indt «b» took 0.019322 -Skipping derivation param2 on indt «b» since the user did not select it -Derivation tag on indt «b» -Derivation tag on indt «b» took 0.006224 -Derivation eqType_ast on indt «b» -Derivation eqType_ast on indt «b» took 0.003491 -Skipping derivation lens_laws on indt «b» since the user did not select it -Skipping derivation param1_congr on indt «b» -since the user did not select it -Derivation param1_inhab on indt «b» -Derivation param1_inhab on indt «b» took 0.008794 -Derivation param1_functor on indt «b» -Derivation param1_functor on indt «b» took 0.008190 -Derivation fields on indt «b» -Derivation fields on indt «b» took 0.018304 -Skipping derivation param1_trivial on indt «b» -since the user did not select it -Derivation induction on indt «b» -Derivation induction on indt «b» took 0.006737 -Derivation eqb on indt «b» -Derivation eqb on indt «b» took 0.015662 -Derivation eqbcorrect on indt «b» -Derivation eqbcorrect on indt «b» took 0.024567 -Derivation eqbOK on indt «b» -Derivation eqbOK on indt «b» took 0.005055 -a_eqb - : a -> a -> bool -b_eqb - : b -> b -> bool +more : (forall A : Type, A -> tickle A -> tickle A) + : forall A : Type, A -> tickle A -> tickle A +tickle.eqb + : (forall A : Type, (A -> A -> bool) -> tickle A -> tickle A -> bool) + : forall A : Type, (A -> A -> bool) -> tickle A -> tickle A -> bool +tickle.eqb_OK + : (forall (A : Type) (f : A -> A -> bool), + (forall x y : A, reflect (x = y) (f x y)) -> + forall x y : tickle A, reflect (x = y) (tickle.eqb A f x y)) + : forall (A : Type) (f : A -> A -> bool), + (forall x y : A, reflect (x = y) (f x y)) -> + forall x y : tickle A, reflect (x = y) (tickle.eqb A f x y) +tickle.map : (forall A B : Type, (A -> B) -> tickle A -> tickle B) + : forall A B : Type, (A -> B) -> tickle A -> tickle B +tickle.tickle_R + : (forall A B : Type, (A -> B -> Type) -> tickle A -> tickle B -> Type) + : forall A B : Type, (A -> B -> Type) -> tickle A -> tickle B -> Type +Starting module rtree +Declaring inductive +parameter A explicit (sort (typ «elpi.apps.derive.examples.usage.190»)) + c0 \ + inductive rtree tt + (arity (sort (typ «elpi.apps.derive.examples.usage.191»))) c1 \ + [constructor Leaf (arity (prod `_` c0 c2 \ c1)), + constructor Node + (arity (prod `_` (app [global (indt «tickle.tickle»), c1]) c2 \ c1))] +Deriving +Derivation map on indt «rtree» +Derivation map on indt «rtree» took 0.031083 +Derivation lens on indt «rtree» +Derivation lens on indt «rtree» failed, continuing +Derivation param1 on indt «rtree» +[foo (const «X»), foo (indt «nat»), foo (indt «bool»)] +Derivation param1 on indt «rtree» took 0.071434 +Derivation param2 on indt «rtree» +[foo (indt «nat»), foo (indt «bool»)] +Derivation param2 on indt «rtree» took 0.081062 +Derivation tag on indt «rtree» +[] +Derivation tag on indt «rtree» took 0.015707 +Derivation eqType_ast on indt «rtree» +Derivation eqType_ast on indt «rtree» took 0.011759 +Derivation lens_laws on indt «rtree» +Derivation lens_laws on indt «rtree» took 0.002712 +Derivation param1_congr on indt «rtree» +[foo (indt «nat»)] +File "./tests/test_HOAS.v", line 123, characters 0-34: +Warning: Use of “Require” inside a module is fragile. It is not recommended +to use this functionality in finished proof scripts. +[require-in-module,fragile] +Derivation param1_congr on indt «rtree» took 0.030091 +Derivation param1_inhab on indt «rtree» +Derivation param1_inhab on indt «rtree» took 0.028901 +Derivation param1_functor on indt «rtree» +Derivation param1_functor on indt «rtree» took 0.021122 +Derivation fields on indt «rtree» +Raw term: +app + [global (const «add»), primitive (uint63 2000000003333002), + primitive (uint63 1)] +Nice term: add 2000000003333002 1 +Red: +2000000003333003 +File "./tests/test_HOAS.v", line 127, characters 0-34: +Warning: Use of “Require” inside a module is fragile. It is not recommended +to use this functionality in finished proof scripts. +[require-in-module,fragile] +Derivation fields on indt «rtree» took 0.304666 +Derivation param1_trivial on indt «rtree» Query assignments: B = fix `add` 0 (prod `n` (global (indt «nat»)) c0 \ @@ -3273,54 +3224,12 @@ WEAK CONSTRAINTS: -COQC examples/readme.v ----------------------------------- - {c0 c1} : decl c1 `a` (global (indt «bool»)) - ?- evar X0 (sort (typ «elpi.tests.test_HOAS.10»)) X1 /* suspended on X0, X1 */ - {c0 c1} : decl c1 `a` (global (indt «bool»)) ?- evar (X2 c1) X1 (X2 c1) /* suspended on X2 */ -EVARS: - ?X11==[a |- ?elpi_evar] (internal placeholder) {?elpi_evar0} - ?X10==[ |- Type] (internal placeholder) {?elpi_evar} - ?X9==[a |- ?elpi_evar => ?elpi_evar0] (internal placeholder) - ?X8==[a |- Type => ?elpi_evar] (internal placeholder) - -SHELF: -FUTURE GOALS STACK:?X11 -?X10 - -Coq-Elpi mapping: -RAW: -?X10 <-> X0 -?X11 <-> X2 -ELAB: -?X10 <-> X1 -?X11 <-> X2 - -X2 c0 : X1 -Query assignments: - TY = X1 - X = c0 \ c1 \ -X2 c0 -Syntactic constraints: - {c0 c1} : decl c1 `a` (global (indt «bool»)) - ?- evar X0 (sort (typ «elpi.tests.test_HOAS.10»)) X1 /* suspended on X0, X1 */ - {c0 c1} : decl c1 `a` (global (indt «bool»)) ?- evar (X2 c1) X1 (X2 c1) /* suspended on X2 */ -Universe constraints: -UNIVERSES: - {elpi.tests.test_HOAS.10} |= -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - -{{ nat; S; }} -{{ nat; S; }} -Query assignments: - GR = const «Nat.add» - L = {{ nat; S; }} - S = {{ nat; S; }} +Raw term: +app + [global (const «add»), primitive (float64 24000000000000), + primitive (float64 1)] +Nice term: 24000000000000 + 1 +Red: 24000000000001 raw: inductive X3 tt (arity (sort (typ «elpi.tests.test_arg_HOAS.127»))) c0 \ [] upoly-decl [«elpi.tests.test_arg_HOAS.127»] tt [] tt @@ -3359,6 +3268,86 @@ X4 is universe polymorphic Expands to: Inductive elpi.tests.test_arg_HOAS.X4 +Derivation param1_trivial on indt «rtree» took 0.585728 +Derivation induction on indt «rtree» +Derivation induction on indt «rtree» took 0.018729 +Derivation eqb on indt «rtree» +z + : nat +Derivation eqb on indt «rtree» took 0.155222 +Derivation eqbcorrect on indt «rtree» +COQC tests/test_cache_async.v +Derivation eqbcorrect on indt «rtree» took 0.232399 +Derivation eqbOK on indt «rtree» +Derivation eqbOK on indt «rtree» took 0.012225 +Done +rtree.induction + : (forall (A : Type) (PA : A -> Type) (P : rtree A -> Type), + (forall a : A, PA a -> P (Leaf A a)) -> + (forall l : tickle (rtree A), + tickle.is_tickle (rtree A) P l -> P (Node A l)) -> + forall x : rtree A, rtree.is_rtree A PA x -> P x) + : forall (A : Type) (PA : A -> Type) (P : rtree A -> Type), + (forall a : A, PA a -> P (Leaf A a)) -> + (forall l : tickle (rtree A), + tickle.is_tickle (rtree A) P l -> P (Node A l)) -> + forall x : rtree A, rtree.is_rtree A PA x -> P x +Starting module Box +Declaring inductive +parameter A explicit (sort (typ «elpi.apps.derive.examples.usage.379»)) + c0 \ + record Box (sort (typ «elpi.apps.derive.examples.usage.380»)) Build_Box + (field [coercion off, canonical tt] contents c0 c1 \ + field [coercion off, canonical tt] tag (global (indt «nat»)) c2 \ + end-record) +Deriving +Skipping derivation map on indt «Box» since the user did not select it +Derivation lens on indt «Box» +Derivation lens on indt «Box» took 0.037278 +Skipping derivation param1 on indt «Box» since the user did not select it +Skipping derivation param2 on indt «Box» since the user did not select it +Derivation tag on indt «Box» +File "./examples/usage.v", line 53, characters 0-84: +Warning: Global name tag is taken, using tag1 instead [elpi.renamed,elpi] +Derivation tag on indt «Box» took 0.016004 +Derivation eqType_ast on indt «Box» +Derivation eqType_ast on indt «Box» took 0.003871 +Derivation lens_laws on indt «Box» +Query assignments: + GR = indt «X3» +Universe constraints: +UNIVERSES: + {elpi.tests.test_arg_HOAS.143} |= +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + elpi.tests.test_arg_HOAS.143 +WEAK CONSTRAINTS: + + +Derivation lens_laws on indt «Box» took 0.113705 +Skipping derivation param1_congr on indt «Box» +since the user did not select it +Skipping derivation param1_inhab on indt «Box» +since the user did not select it +Skipping derivation param1_functor on indt «Box» +since the user did not select it +Derivation fields on indt «Box» +Derivation fields on indt «Box» took 0.059481 +Skipping derivation param1_trivial on indt «Box» +since the user did not select it +Skipping derivation induction on indt «Box» +since the user did not select it +Derivation eqb on indt «Box» +Derivation eqb on indt «Box» took 0.044524 +Skipping derivation eqbcorrect on indt «Box» +since the user did not select it +Skipping derivation eqbOK on indt «Box» since the user did not select it +Done +Box.eqb : (forall A : Type, (A -> A -> bool) -> Box A -> Box A -> bool) + : forall A : Type, (A -> A -> bool) -> Box A -> Box A -> bool +@Box._tag : (forall A : Type, Lens (Box A) (Box A) nat nat) + : forall A : Type, Lens (Box A) (Box A) nat nat Query assignments: B = fun `n` (global (indt «nat»)) c0 \ app @@ -3462,320 +3451,21 @@ WEAK CONSTRAINTS: -z - : nat -COQC tests/test_cache_async.v -File "./tests/test_HOAS.v", line 123, characters 0-34: -Warning: Use of “Require” inside a module is fragile. It is not recommended -to use this functionality in finished proof scripts. -[require-in-module,fragile] -{{ X.a; }} {{ X.a; Nat.add; nat; }} -{{ X.a; }} {{ X.a; Nat.add; nat; O; S; }} -Query assignments: - AllL = {{ X.a; Nat.add; nat; }} - AllS = {{ X.a; Nat.add; nat; O; S; }} - GR = const «X.b» - L = {{ X.a; }} - M = «elpi.tests.test_API_env.HOAS.X» - S = {{ X.a; }} - Spilled_1 = const «X.a» -[foo (const «X»), foo (indt «nat»), foo (indt «bool»)] -Raw term: -app - [global (const «add»), primitive (uint63 2000000003333002), - primitive (uint63 1)] -Nice term: add 2000000003333002 1 -Red: -2000000003333003 -File "./tests/test_HOAS.v", line 127, characters 0-34: -Warning: Use of “Require” inside a module is fragile. It is not recommended -to use this functionality in finished proof scripts. -[require-in-module,fragile] -[foo (indt «nat»), foo (indt «bool»)] -[] -Query assignments: - GR = indt «X3» -Universe constraints: -UNIVERSES: - {elpi.tests.test_arg_HOAS.143} |= -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - elpi.tests.test_arg_HOAS.143 -WEAK CONSTRAINTS: - - -[foo (indt «nat»)] -Raw term: -app - [global (const «add»), primitive (float64 24000000000000), - primitive (float64 1)] -Nice term: 24000000000000 + 1 -Red: 24000000000001 -Notation peano := peano.peano -Inductive peano : Set := Zero : peano | Succ : peano -> peano. - = false - : bool -peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2) - -peano.eqb_OK is not universe polymorphic -Arguments peano.eqb_OK x1 x2 -peano.eqb_OK is opaque -Expands to: Constant elpi.apps.derive.examples.readme.peano.eqb_OK +Box._tag_set_set + : (forall (A : Type) (r : Box A) (y x : nat), + set Box._tag x (set Box._tag y r) = set Box._tag x r) + : forall (A : Type) (r : Box A) (y x : nat), + set Box._tag x (set Box._tag y r) = set Box._tag x r +Box._tag_contents_exchange + : (forall (A : Type) (r : Box A) (x : nat) (y : A), + set Box._tag x (set Box._contents y r) = + set Box._contents y (set Box._tag x r)) + : forall (A : Type) (r : Box A) (x : nat) (y : A), + set Box._tag x (set Box._contents y r) = + set Box._contents y (set Box._tag x r) COQC tests/test_COQ_ELPI_ATTRIBUTES.v -Derivation param1 on const «Nat.add» -Derivation param1 on const «Nat.add» took 0.019077 -Derivation param2 on const «Nat.add» -Derivation param2 on const «Nat.add» took 0.022964 -Derivation eqb-alias on const «Nat.add» -Derivation eqb-alias on const «Nat.add» failed, continuing -Derivation eqbcorrect-alias on const «Nat.add» -Derivation eqbcorrect-alias on const «Nat.add» failed, continuing -Derivation eqbOK-alias on const «Nat.add» -Derivation eqbOK-alias on const «Nat.add» failed, continuing -is_add - : forall n : nat, is_nat n -> forall m : nat, is_nat m -> is_nat (n + m) -COQC tests/test_projK.v -CHR: Uniqueness of typing of frozen--985 + [] <-> [] -1 |> [decl c0 `x` (uvar frozen--985 [])] |- frozen--985 [] : -sort (typ «elpi.tests.test_elaborator.40») -0 |> [] |- frozen--985 [] : sort (typ «elpi.tests.test_elaborator.39») -0 |> [] |- -unify-eq (sort (typ «elpi.tests.test_elaborator.40»)) - (sort (typ «elpi.tests.test_elaborator.39»)) - -Query assignments: - R = fun `x` X0 c0 \ c0 - T = prod `x` X0 c0 \ X0 - _uvk_87_ = X1 -Syntactic constraints: - {c0} : decl c0 `x` X0 - ?- evar X2 (sort (typ «elpi.tests.test_elaborator.40»)) X0 /* suspended on X2, X0 */ -Universe constraints: -UNIVERSES: - {elpi.tests.test_elaborator.42 elpi.tests.test_elaborator.41 - elpi.tests.test_elaborator.40 elpi.tests.test_elaborator.39} |= - elpi.tests.test_elaborator.39 <= elpi.tests.test_elaborator.41 - elpi.tests.test_elaborator.40 <= elpi.tests.test_elaborator.39 - elpi.tests.test_elaborator.40 <= elpi.tests.test_elaborator.41 - elpi.tests.test_elaborator.41 <= elpi.tests.test_elaborator.42 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - - {c0 c1 c2 c3} : - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) - ?- evar (X0 c0 c1 c2 c3) - (prod `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ - prod `j` (app [c1, c3]) c5 \ - app - [global (indt «ex»), app [c1, c3], - fun `a` (app [c1, c3]) c6 \ - app [global (indt «eq»), app [c1, c3], c6, c6]]) - (X1 c0 c1 c2 c3) /* suspended on X0, X1 */ -Goal: -[] - - -[decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] ------------- -prod `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ - prod `j` (app [c1, c3]) c5 \ - app - [global (indt «ex»), app [c1, c3], - fun `a` (app [c1, c3]) c6 \ - app [global (indt «eq»), app [c1, c3], c6, c6]] -x w = Type -> x w -> exists a : x w, a = a - {c0 c1 c2 c3} : - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) - ?- evar (X0 c0 c1 c2 c3) - (prod `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ - prod `j` (app [c1, c3]) c5 \ - app - [global (indt «ex»), app [c1, c3], - fun `a` (app [c1, c3]) c6 \ - app [global (indt «eq»), app [c1, c3], c6, c6]]) - (X1 c0 c1 c2 c3) /* suspended on X0, X1 */ -Goal: -[] - - -[decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] ------------- -prod `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ - prod `j` (app [c1, c3]) c5 \ - app - [global (indt «ex»), app [c1, c3], - fun `a` (app [c1, c3]) c6 \ - app [global (indt «eq»), app [c1, c3], c6, c6]] -x w = Type -> x w -> exists a : x w, a = a - {c0 c1 c2 c3 c4 c5} : - decl c5 `j` (app [c1, c3]), - decl c4 `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) - ?- evar (X0 c0 c1 c2 c3 c4 c5) (app [c1, c3]) (X1 c0 c1 c2 c3 c4 c5) /* suspended on X0, X1 */ - {c0 c1 c2 c3 c4 c5} : - decl c5 `j` (app [c1, c3]), - decl c4 `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) - ?- evar (X2 c0 c1 c2 c3 c4 c5) - (app - [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, - X1 c0 c1 c2 c3 c4 c5]) (X3 c0 c1 c2 c3 c4 c5) /* suspended on X2, X3 */ -Goal: -[] - - -Query assignments: - GR = indt «X4» -Universe constraints: -UNIVERSES: - {elpi.tests.test_arg_HOAS.144} |= -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - elpi.tests.test_arg_HOAS.144 -WEAK CONSTRAINTS: - - -[decl c5 `j` (app [c1, c3]), - decl c4 `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] ------------- -app - [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, - X1 c0 c1 c2 c3 c4 c5] ?elpi_evar = ?elpi_evar -raw: -inductive X5 tt (arity (sort (typ «elpi.tests.test_arg_HOAS.145»))) c0 \ [] -upoly-decl [«elpi.tests.test_arg_HOAS.145»] ff [] ff -Universe constraints: UNIVERSES: - {u3} |= - ALGEBRAIC UNIVERSES: - {} - UNDEFINED UNIVERSES: - elpi.tests.test_arg_HOAS.145 - WEAK CONSTRAINTS: - - - {c0 c1 c2 c3 c4 c5} : - decl c5 `j` (app [c1, c3]), - decl c4 `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) - ?- evar (X0 c0 c1 c2 c3 c4 c5) (app [c1, c3]) (X1 c0 c1 c2 c3 c4 c5) /* suspended on X0, X1 */ - {c0 c1 c2 c3 c4 c5} : - decl c5 `j` (app [c1, c3]), - decl c4 `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) - ?- evar (X2 c0 c1 c2 c3 c4 c5) - (app - [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, - X1 c0 c1 c2 c3 c4 c5]) (X3 c0 c1 c2 c3 c4 c5) /* suspended on X2, X3 */ -Goal: -[] - - -[decl c5 `j` (app [c1, c3]), - decl c4 `e` - (app - [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), - app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), - decl c3 `w` c0, - decl c2 `h` - (app - [global (indt «eq»), global (indt «nat»), global (const «o»), - global (const «m»)]), - decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), - decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] ------------- -app - [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, - X1 c0 c1 c2 c3 c4 c5] ?elpi_evar0 = ?elpi_evar0 -typed: -inductive X5 tt (arity (sort (typ «elpi.tests.test_arg_HOAS.145»))) c0 \ [] +nat_eqb_OK : (forall x y : nat, reflect (x = y) (nat_eqb x y)) + : forall x y : nat, reflect (x = y) (nat_eqb x y) Query assignments: C = «Nat.add» F = TODO @@ -3795,11 +3485,6 @@ [global (const «Nat.add»), app [global (indc «S»), global (indc «O»)], app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]] -X5@{u3} : Type@{u3} -(* u3 |= *) - -X5 is universe polymorphic -Expands to: Inductive elpi.tests.test_arg_HOAS.X5 T2 = app [fix `plus` 0 (prod `n` (global (indt «nat»)) c0 \ @@ -3825,6 +3510,102 @@ global (indt «nat») _uvk_41_ = c0 \ c1 \ c2 \ global (indt «nat») +Derivation map on indt «a» +Derivation map on indt «a» took 0.008351 +Derivation lens on indt «a» +Derivation lens on indt «a» failed, continuing +Derivation param1 on indt «a» +Derivation param1 on indt «a» took 0.017412 +Derivation param2 on indt «a» +Derivation param2 on indt «a» took 0.019394 +Derivation tag on indt «a» +Derivation tag on indt «a» took 0.005803 +Derivation eqType_ast on indt «a» +Derivation eqType_ast on indt «a» took 0.002836 +Derivation lens_laws on indt «a» +Derivation lens_laws on indt «a» took 0.002542 +Derivation param1_congr on indt «a» +Derivation param1_congr on indt «a» took 0.003772 +Derivation param1_inhab on indt «a» +Derivation param1_inhab on indt «a» took 0.007906 +Derivation param1_functor on indt «a» +Derivation param1_functor on indt «a» took 0.007620 +Derivation fields on indt «a» +Derivation fields on indt «a» took 0.015442 +Derivation param1_trivial on indt «a» +Derivation param1_trivial on indt «a» took 0.009680 +Derivation induction on indt «a» +Derivation induction on indt «a» took 0.006009 +Derivation eqb on indt «a» +Derivation eqb on indt «a» took 0.013404 +Derivation eqbcorrect on indt «a» +Derivation eqbcorrect on indt «a» took 0.020190 +Derivation eqbOK on indt «a» +Derivation eqbOK on indt «a» took 0.004871 +Skipping derivation map on indt «b» since the user did not select it +Skipping derivation lens on indt «b» since the user did not select it +Derivation param1 on indt «b» +Derivation param1 on indt «b» took 0.019005 +Skipping derivation param2 on indt «b» since the user did not select it +Derivation tag on indt «b» +Derivation tag on indt «b» took 0.006129 +Derivation eqType_ast on indt «b» +Derivation eqType_ast on indt «b» took 0.002973 +Skipping derivation lens_laws on indt «b» since the user did not select it +Skipping derivation param1_congr on indt «b» +since the user did not select it +Derivation param1_inhab on indt «b» +Derivation param1_inhab on indt «b» took 0.007830 +Derivation param1_functor on indt «b» +Derivation param1_functor on indt «b» took 0.007644 +Derivation fields on indt «b» +Derivation fields on indt «b» took 0.017364 +Skipping derivation param1_trivial on indt «b» +since the user did not select it +Derivation induction on indt «b» +Derivation induction on indt «b» took 0.006329 +Derivation eqb on indt «b» +Derivation eqb on indt «b» took 0.014825 +Derivation eqbcorrect on indt «b» +Derivation eqbcorrect on indt «b» took 0.023085 +Derivation eqbOK on indt «b» +Derivation eqbOK on indt «b» took 0.004822 +a_eqb + : a -> a -> bool +b_eqb + : b -> b -> bool +COQC examples/readme.v +Query assignments: + GR = indt «X4» +Universe constraints: +UNIVERSES: + {elpi.tests.test_arg_HOAS.144} |= +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + elpi.tests.test_arg_HOAS.144 +WEAK CONSTRAINTS: + + +raw: +inductive X5 tt (arity (sort (typ «elpi.tests.test_arg_HOAS.145»))) c0 \ [] +upoly-decl [«elpi.tests.test_arg_HOAS.145»] ff [] ff +Universe constraints: UNIVERSES: + {u3} |= + ALGEBRAIC UNIVERSES: + {} + UNDEFINED UNIVERSES: + elpi.tests.test_arg_HOAS.145 + WEAK CONSTRAINTS: + + +typed: +inductive X5 tt (arity (sort (typ «elpi.tests.test_arg_HOAS.145»))) c0 \ [] +X5@{u3} : Type@{u3} +(* u3 |= *) + +X5 is universe polymorphic +Expands to: Inductive elpi.tests.test_arg_HOAS.X5 raw: inductive X6 tt (arity (sort (typ «elpi.tests.test_arg_HOAS.154»))) c0 \ [constructor K @@ -3896,26 +3677,6 @@ f6 is transparent Expands to: Constant elpi.tests.test_arg_HOAS.f6 Query assignments: - R = fun `x` (global (indt «nat»)) c0 \ - app [global (const «Nat.add»), c0, global (indc «O»)] - T = prod `x` (global (indt «nat»)) c0 \ global (indt «nat») - _uvk_109_ = X0 -Universe constraints: -UNIVERSES: - {elpi.tests.test_elaborator.46 elpi.tests.test_elaborator.45 - elpi.tests.test_elaborator.44 elpi.tests.test_elaborator.43} |= - elpi.tests.test_elaborator.43 <= elpi.tests.test_elaborator.45 - elpi.tests.test_elaborator.44 <= elpi.tests.test_elaborator.45 - elpi.tests.test_elaborator.45 <= elpi.tests.test_elaborator.46 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - -COQC tests/perf_calls.v -Query assignments: C = «Nat.add» F = TODO T = app @@ -3987,27 +3748,39 @@ global (indt «nat») _uvk_52_ = c0 \ c1 \ c2 \ c3 \ global (indt «nat») -const-decl D - (some - (fun `i` (global (indt «I»)) c0 \ - fun `l` (app [global (indt «L»), c0]) c1 \ global (indt «True»))) - (parameter i maximal (global (indt «I»)) c0 \ - parameter l maximal (app [global (indt «L»), c0]) c1 \ arity (sort prop)) -const-decl D - (some - (fun `i` (global (indt «I»)) c0 \ - fun `H` (app [global (indt «L»), c0]) c1 \ global (indt «True»))) - (parameter i maximal (global (indt «I»)) c0 \ - parameter H maximal (app [global (indt «L»), c0]) c1 \ arity (sort prop)) -const-decl D - (some - (fun `i` (global (indt «I»)) c0 \ - fun `H` (app [global (indt «L»), c0]) c1 \ - fun `n` (global (indt «nat»)) c2 \ global (indt «True»))) - (parameter i maximal (global (indt «I»)) c0 \ - parameter H maximal (app [global (indt «L»), c0]) c1 \ - parameter n explicit (global (indt «nat»)) c2 \ arity (sort prop)) -COQC tests/test_ctx_cache.v +CHR: Uniqueness of typing of frozen--985 + [] <-> [] +1 |> [decl c0 `x` (uvar frozen--985 [])] |- frozen--985 [] : +sort (typ «elpi.tests.test_elaborator.40») +0 |> [] |- frozen--985 [] : sort (typ «elpi.tests.test_elaborator.39») +0 |> [] |- +unify-eq (sort (typ «elpi.tests.test_elaborator.40»)) + (sort (typ «elpi.tests.test_elaborator.39»)) + +Query assignments: + R = fun `x` X0 c0 \ c0 + T = prod `x` X0 c0 \ X0 + _uvk_87_ = X1 +Syntactic constraints: + {c0} : decl c0 `x` X0 + ?- evar X2 (sort (typ «elpi.tests.test_elaborator.40»)) X0 /* suspended on X2, X0 */ +Universe constraints: +UNIVERSES: + {elpi.tests.test_elaborator.42 elpi.tests.test_elaborator.41 + elpi.tests.test_elaborator.40 elpi.tests.test_elaborator.39} |= + elpi.tests.test_elaborator.39 <= elpi.tests.test_elaborator.41 + elpi.tests.test_elaborator.40 <= elpi.tests.test_elaborator.39 + elpi.tests.test_elaborator.40 <= elpi.tests.test_elaborator.41 + elpi.tests.test_elaborator.41 <= elpi.tests.test_elaborator.42 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + +File "./tests/test_API.v", line 204, characters 0-107: +Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] +COQC tests/perf_calls.v Query assignments: C = «Nat.add» F = TODO @@ -4070,12 +3843,70 @@ global (indt «nat») _uvk_61_ = c0 \ c1 \ c2 \ c3 \ global (indt «nat») -sort (typ X0) +const-decl D + (some + (fun `i` (global (indt «I»)) c0 \ + fun `l` (app [global (indt «L»), c0]) c1 \ global (indt «True»))) + (parameter i maximal (global (indt «I»)) c0 \ + parameter l maximal (app [global (indt «L»), c0]) c1 \ arity (sort prop)) +const-decl D + (some + (fun `i` (global (indt «I»)) c0 \ + fun `H` (app [global (indt «L»), c0]) c1 \ global (indt «True»))) + (parameter i maximal (global (indt «I»)) c0 \ + parameter H maximal (app [global (indt «L»), c0]) c1 \ arity (sort prop)) +const-decl D + (some + (fun `i` (global (indt «I»)) c0 \ + fun `H` (app [global (indt «L»), c0]) c1 \ + fun `n` (global (indt «nat»)) c2 \ global (indt «True»))) + (parameter i maximal (global (indt «I»)) c0 \ + parameter H maximal (app [global (indt «L»), c0]) c1 \ + parameter n explicit (global (indt «nat»)) c2 \ arity (sort prop)) +COQC tests/test_ctx_cache.v +Notation peano := peano.peano +Inductive peano : Set := Zero : peano | Succ : peano -> peano. + = false + : bool +peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2) + +peano.eqb_OK is not universe polymorphic +Arguments peano.eqb_OK x1 x2 +peano.eqb_OK is opaque +Expands to: Constant elpi.apps.derive.examples.readme.peano.eqb_OK +Derivation param1 on const «Nat.add» +Derivation param1 on const «Nat.add» took 0.019249 +Derivation param2 on const «Nat.add» +Derivation param2 on const «Nat.add» took 0.022591 +Derivation eqb-alias on const «Nat.add» +Derivation eqb-alias on const «Nat.add» failed, continuing +Derivation eqbcorrect-alias on const «Nat.add» +Derivation eqbcorrect-alias on const «Nat.add» failed, continuing +Derivation eqbOK-alias on const «Nat.add» +Derivation eqbOK-alias on const «Nat.add» failed, continuing +is_add + : forall n : nat, is_nat n -> forall m : nat, is_nat m -> is_nat (n + m) Query assignments: - type_1 = X0 -File "./tests/test_API.v", line 204, characters 0-107: -Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] -COQC tests/test_libobject_A.v + R = fun `x` (global (indt «nat»)) c0 \ + app [global (const «Nat.add»), c0, global (indc «O»)] + T = prod `x` (global (indt «nat»)) c0 \ global (indt «nat») + _uvk_109_ = X0 +Universe constraints: +UNIVERSES: + {elpi.tests.test_elaborator.46 elpi.tests.test_elaborator.45 + elpi.tests.test_elaborator.44 elpi.tests.test_elaborator.43} |= + elpi.tests.test_elaborator.43 <= elpi.tests.test_elaborator.45 + elpi.tests.test_elaborator.44 <= elpi.tests.test_elaborator.45 + elpi.tests.test_elaborator.45 <= elpi.tests.test_elaborator.46 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + +COQC tests/test_projK.v +hello [int 1, int 2, trm (global (indt «nat»)), str x] Query assignments: C = «Nat.add» F = TODO @@ -4089,47 +3920,8 @@ T2 = app [global (indc «S»), app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]] -hello [int 1, int 2, trm (global (indt «nat»)), str x] -Query assignments: - S = sort (typ «elpi.tests.test_elaborator.48») - T = sort (typ «elpi.tests.test_elaborator.47») - type_2 = «elpi.tests.test_elaborator.47» -Universe constraints: -UNIVERSES: - {elpi.tests.test_elaborator.48 elpi.tests.test_elaborator.47} |= - elpi.tests.test_elaborator.47 < elpi.tests.test_elaborator.48 -ALGEBRAIC UNIVERSES: - {elpi.tests.test_elaborator.47} -UNDEFINED UNIVERSES: - elpi.tests.test_elaborator.47 -WEAK CONSTRAINTS: - - -COQC tests/test_vernacular2.v -test1 -str hello -str x -test1 -too many arguments -File "./tests/test_vernacular2.v", line 6, characters 2-17: -Warning: This command does not support this attribute: fwd_compat_attr. -[unsupported-attributes,parsing] -File "./tests/test_vernacular2.v", line 7, characters 2-17: -Warning: This command does not support this attribute: fwd_compat_attr. -[unsupported-attributes,parsing] -File "./tests/test_vernacular2.v", line 8, characters 2-17: -Warning: This command does not support this attribute: fwd_compat_attr. -[unsupported-attributes,parsing] Query assignments: GR = const «Ranalysis5.derivable_pt_lim_CVU» -elpi.tests.test_HOAS.P.p1 1 global (const «P.x») -@P.p1 -X0 global (const «P.x») -P.p1 P.x -some - (fun `A` (sort (typ «elpi.tests.test_HOAS.11»)) c0 \ - fun `f` (app [global (indt «P.foo»), c0]) c1 \ - app [primitive (proj elpi.tests.test_HOAS.P.p1 1), c1]) S = {{ BinInt.Z.A'A_left; BinNat.N.A'A_right; PeanoNat.Nat.A'A_right; BinInt.Z.A'A_right; Field_theory.AF_1_neq_0; Field_theory.AF_AR; Field_theory.AFdiv_def; Field_theory.AFinv_l; Ring_theory.ARadd_0_l; @@ -5560,21 +5352,7 @@ Ring_polynom.PEpow; RMicromega.CInv; Field_theory.FEdiv; Tauto.EQ; RMicromega.COpp; Field_theory.FEpow; }} Spilled_1 = 3412 - T = 3.172966 -elpi.tests.test_HOAS.P.p2 2 global (const «P.x») -@P.p2 -X0 global (const «P.x») -P.p2 P.x -some - (fun `A` (sort (typ «elpi.tests.test_HOAS.11»)) c0 \ - fun `f` (app [global (indt «P.foo»), c0]) c1 \ - app [primitive (proj elpi.tests.test_HOAS.P.p1 1), c1]) - evar (X0) (global (indt «nat»)) X1 /* suspended on X0, X1 */ -X0 global (indt «nat») - evar (X2) (global (indt «nat»)) X3 /* suspended on X2, X3 */ -hello -eq_refl : one = 1 - : one = 1 + T = 4.894889 coq.pp.box (coq.pp.hv 2) [coq.pp.str Module, coq.pp.spc, coq.pp.str Foo, coq.pp.spc, coq.pp.str :=, coq.pp.brk 1 0, coq.pp.str body, coq.pp.spc, coq.pp.str End Foo.] @@ -5589,7 +5367,267 @@ | false => y end fix foo x y {struct x} := if x as x0 return ?e6@{x:=x0} then 3 else y -COQC tests/test_libobject_B.v +COQC tests/test_libobject_A.v + {c0 c1 c2 c3} : + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) + ?- evar (X0 c0 c1 c2 c3) + (prod `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ + prod `j` (app [c1, c3]) c5 \ + app + [global (indt «ex»), app [c1, c3], + fun `a` (app [c1, c3]) c6 \ + app [global (indt «eq»), app [c1, c3], c6, c6]]) + (X1 c0 c1 c2 c3) /* suspended on X0, X1 */ +Goal: +[] + + +[decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] +------------ +prod `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ + prod `j` (app [c1, c3]) c5 \ + app + [global (indt «ex»), app [c1, c3], + fun `a` (app [c1, c3]) c6 \ + app [global (indt «eq»), app [c1, c3], c6, c6]] +x w = Type -> x w -> exists a : x w, a = a + {c0 c1 c2 c3} : + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) + ?- evar (X0 c0 c1 c2 c3) + (prod `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ + prod `j` (app [c1, c3]) c5 \ + app + [global (indt «ex»), app [c1, c3], + fun `a` (app [c1, c3]) c6 \ + app [global (indt «eq»), app [c1, c3], c6, c6]]) + (X1 c0 c1 c2 c3) /* suspended on X0, X1 */ +Goal: +[] + + +[decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c4 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] +------------ +prod `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]) c4 \ + prod `j` (app [c1, c3]) c5 \ + app + [global (indt «ex»), app [c1, c3], + fun `a` (app [c1, c3]) c6 \ + app [global (indt «eq»), app [c1, c3], c6, c6]] +x w = Type -> x w -> exists a : x w, a = a +elpi.tests.test_HOAS.P.p1 1 global (const «P.x») +@P.p1 +X0 global (const «P.x») +P.p1 P.x +some + (fun `A` (sort (typ «elpi.tests.test_HOAS.11»)) c0 \ + fun `f` (app [global (indt «P.foo»), c0]) c1 \ + app [primitive (proj elpi.tests.test_HOAS.P.p1 1), c1]) +sort (typ X0) +Query assignments: + type_1 = X0 + {c0 c1 c2 c3 c4 c5} : + decl c5 `j` (app [c1, c3]), + decl c4 `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) + ?- evar (X0 c0 c1 c2 c3 c4 c5) (app [c1, c3]) (X1 c0 c1 c2 c3 c4 c5) /* suspended on X0, X1 */ + {c0 c1 c2 c3 c4 c5} : + decl c5 `j` (app [c1, c3]), + decl c4 `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) + ?- evar (X2 c0 c1 c2 c3 c4 c5) + (app + [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, + X1 c0 c1 c2 c3 c4 c5]) (X3 c0 c1 c2 c3 c4 c5) /* suspended on X2, X3 */ +Goal: +[] + + +[decl c5 `j` (app [c1, c3]), + decl c4 `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] +------------ +app + [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, + X1 c0 c1 c2 c3 c4 c5] ?elpi_evar = ?elpi_evar +elpi.tests.test_HOAS.P.p2 2 global (const «P.x») +@P.p2 +X0 global (const «P.x») +P.p2 P.x +some + (fun `A` (sort (typ «elpi.tests.test_HOAS.11»)) c0 \ + fun `f` (app [global (indt «P.foo»), c0]) c1 \ + app [primitive (proj elpi.tests.test_HOAS.P.p1 1), c1]) + {c0 c1 c2 c3 c4 c5} : + decl c5 `j` (app [c1, c3]), + decl c4 `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) + ?- evar (X0 c0 c1 c2 c3 c4 c5) (app [c1, c3]) (X1 c0 c1 c2 c3 c4 c5) /* suspended on X0, X1 */ + {c0 c1 c2 c3 c4 c5} : + decl c5 `j` (app [c1, c3]), + decl c4 `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»)) + ?- evar (X2 c0 c1 c2 c3 c4 c5) + (app + [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, + X1 c0 c1 c2 c3 c4 c5]) (X3 c0 c1 c2 c3 c4 c5) /* suspended on X2, X3 */ +Goal: +[] + + +[decl c5 `j` (app [c1, c3]), + decl c4 `e` + (app + [global (indt «eq»), sort (typ «elpi.tests.test_tactic.2»), + app [c1, c3], sort (typ «elpi.tests.test_tactic.3»)]), + decl c3 `w` c0, + decl c2 `h` + (app + [global (indt «eq»), global (indt «nat»), global (const «o»), + global (const «m»)]), + decl c1 `x` (prod `y` c0 c6 \ sort (typ «elpi.tests.test_tactic.2»)), + decl c0 `T` (sort (typ «elpi.tests.test_tactic.1»))] +------------ +app + [global (indt «eq»), app [c1, c3], X1 c0 c1 c2 c3 c4 c5, + X1 c0 c1 c2 c3 c4 c5] ?elpi_evar0 = ?elpi_evar0 +COQC tests/test_API2.v +Query assignments: + S = {{ Nat.add; eq; nat; O; }} + Spilled_1 = 4 + T = prod `x` (global (indt «nat»)) c0 \ + app + [global (indt «eq»), X0 c0, + app [global (const «Nat.add»), c0, global (indc «O»)], c0] + _uvk_9_ = c0 \ +X0 c0 +Syntactic constraints: + {c0} : decl c0 `x` (global (indt «nat»)) ?- evar (X0 c0) (X1 c0) (X0 c0) /* suspended on X0 */ + {c0} : decl c0 `x` (global (indt «nat»)) + ?- evar (X2 c0) (sort (typ «elpi.tests.test_API_env.30»)) (X1 c0) /* suspended on X2, X1 */ +Universe constraints: +UNIVERSES: + {elpi.tests.test_API_env.30} |= +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + +COQC tests/test_vernacular2.v +COQC tests/test_derive.v +File "./tests/test_API2.v", line 3, characters 0-27: +Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] +Query assignments: + S = sort (typ «elpi.tests.test_elaborator.48») + T = sort (typ «elpi.tests.test_elaborator.47») + type_2 = «elpi.tests.test_elaborator.47» +Universe constraints: +UNIVERSES: + {elpi.tests.test_elaborator.48 elpi.tests.test_elaborator.47} |= + elpi.tests.test_elaborator.47 < elpi.tests.test_elaborator.48 +ALGEBRAIC UNIVERSES: + {elpi.tests.test_elaborator.47} +UNDEFINED UNIVERSES: + elpi.tests.test_elaborator.47 +WEAK CONSTRAINTS: + + +test1 +str hello +str x +test1 +too many arguments +File "./tests/test_vernacular2.v", line 6, characters 2-17: +Warning: This command does not support this attribute: fwd_compat_attr. +[unsupported-attributes,parsing] +File "./tests/test_vernacular2.v", line 7, characters 2-17: +Warning: This command does not support this attribute: fwd_compat_attr. +[unsupported-attributes,parsing] +File "./tests/test_vernacular2.v", line 8, characters 2-17: +Warning: This command does not support this attribute: fwd_compat_attr. +[unsupported-attributes,parsing] Query assignments: S = sort (typ «elpi.tests.test_elaborator.50») T = sort (typ «elpi.tests.test_elaborator.49») @@ -5617,22 +5655,21 @@ File "./tests/test_vernacular2.v", line 10, characters 2-17: Warning: This command does not support this attribute: fwd_compat_attr. [unsupported-attributes,parsing] +some + (pglobal (const «toto») + «elpi.tests.test_HOAS.19 elpi.tests.test_HOAS.20») +prod `T1` (sort (typ «elpi.tests.test_HOAS.19»)) c0 \ + prod `T2` (sort (typ «elpi.tests.test_HOAS.20»)) c1 \ prod `x` c0 c2 \ c0 Query assignments: - S = {{ Nat.add; eq; nat; O; }} - Spilled_1 = 4 - T = prod `x` (global (indt «nat»)) c0 \ - app - [global (indt «eq»), X0 c0, - app [global (const «Nat.add»), c0, global (indc «O»)], c0] - _uvk_9_ = c0 \ -X0 c0 -Syntactic constraints: - {c0} : decl c0 `x` (global (indt «nat»)) ?- evar (X0 c0) (X1 c0) (X0 c0) /* suspended on X0 */ - {c0} : decl c0 `x` (global (indt «nat»)) - ?- evar (X2 c0) (sort (typ «elpi.tests.test_API_env.30»)) (X1 c0) /* suspended on X2, X1 */ + Body = some + (pglobal (const «toto») + «elpi.tests.test_HOAS.19 elpi.tests.test_HOAS.20») + C = «titi» + Term = prod `T1` (sort (typ «elpi.tests.test_HOAS.19»)) c0 \ + prod `T2` (sort (typ «elpi.tests.test_HOAS.20»)) c1 \ prod `x` c0 c2 \ c0 Universe constraints: UNIVERSES: - {elpi.tests.test_API_env.30} |= + {elpi.tests.test_HOAS.20 elpi.tests.test_HOAS.19} |= ALGEBRAIC UNIVERSES: {} UNDEFINED UNIVERSES: @@ -5640,15 +5677,16 @@ WEAK CONSTRAINTS: -COQC tests/test_API2.v +Query assignments: + X1 = «x1» + X2 = «x2» + X3 = «x3» Debug: Cannot enforce elpi.tests.test_elaborator.52 < elpi.tests.test_elaborator.52 because elpi.tests.test_elaborator.52 = elpi.tests.test_elaborator.52 Query assignments: X = sort (typ X0) type_5 = X0 -File "./tests/test_API2.v", line 3, characters 0-27: -Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] [attribute elpi.loc (leaf-loc File "./tests/test_vernacular2.v", line 11, column 24, character 361:), @@ -5657,39 +5695,29 @@ (leaf-loc File "./tests/test_vernacular2.v", line 12, column 0, character 366:), attribute fwd_compat_attr (leaf-str )] -COQC tests/test_libobject_C.v -[(c4 \ app [c1, c2]), (c4 \ app [c0, c2]), (c4 \ c4), (c4 \ - prod `x0` (app [c0, c2]) c5 \ - prod `x1` (global (indt «nat»)) c6 \ - sort (typ «elpi.tests.test_tactic.16»))] -[app - [global (indt «eq»), global (indt «nat»), c2, - app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]], - sort prop] -global (indc «O») -app - [global (indc «S»), - app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]] -COQC tests/test_derive.v -some - (pglobal (const «toto») - «elpi.tests.test_HOAS.19 elpi.tests.test_HOAS.20») -prod `T1` (sort (typ «elpi.tests.test_HOAS.19»)) c0 \ - prod `T2` (sort (typ «elpi.tests.test_HOAS.20»)) c1 \ prod `x` c0 c2 \ c0 Query assignments: - Body = some - (pglobal (const «toto») - «elpi.tests.test_HOAS.19 elpi.tests.test_HOAS.20») - C = «titi» - Term = prod `T1` (sort (typ «elpi.tests.test_HOAS.19»)) c0 \ - prod `T2` (sort (typ «elpi.tests.test_HOAS.20»)) c1 \ prod `x` c0 c2 \ c0 + M = [[mode-ground], [mode-input]] + evar (X0) (global (indt «nat»)) X1 /* suspended on X0, X1 */ +X0 global (indt «nat») + evar (X2) (global (indt «nat»)) X3 /* suspended on X2, X3 */ +hello +eq_refl : one = 1 + : one = 1 +pglobal (const «toto») X0 +pglobal (const «toto») «elpi.tests.test_HOAS.21 elpi.tests.test_HOAS.22» +toto +Query assignments: + Spilled_1 = toto + univ_inst_1 = X0 + univ_inst_2 = «elpi.tests.test_HOAS.23 elpi.tests.test_HOAS.24» Universe constraints: UNIVERSES: - {elpi.tests.test_HOAS.20 elpi.tests.test_HOAS.19} |= + {elpi.tests.test_HOAS.24 elpi.tests.test_HOAS.23} |= ALGEBRAIC UNIVERSES: - {} + {elpi.tests.test_HOAS.24 elpi.tests.test_HOAS.23} UNDEFINED UNIVERSES: - + elpi.tests.test_HOAS.24 + elpi.tests.test_HOAS.23 WEAK CONSTRAINTS: @@ -5708,34 +5736,8 @@ WEAK CONSTRAINTS: -Finished transaction in 4.644 secs (4.639u,0.004s) (successful) -1356 - : nat -this 3 app [c4, X0 c0 c1 c2 c3 c4] -app [c3, app [c1, c2], global (const «a»)] foo.bar -pglobal (const «toto») X0 -pglobal (const «toto») «elpi.tests.test_HOAS.21 elpi.tests.test_HOAS.22» -toto -Query assignments: - Spilled_1 = toto - univ_inst_1 = X0 - univ_inst_2 = «elpi.tests.test_HOAS.23 elpi.tests.test_HOAS.24» -Universe constraints: -UNIVERSES: - {elpi.tests.test_HOAS.24 elpi.tests.test_HOAS.23} |= -ALGEBRAIC UNIVERSES: - {elpi.tests.test_HOAS.24 elpi.tests.test_HOAS.23} -UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.24 - elpi.tests.test_HOAS.23 -WEAK CONSTRAINTS: - - -COQC tests/test_eq.v -Query assignments: - X1 = «x1» - X2 = «x2» - X3 = «x3» +1 +1.000000 Query assignments: D = X0 R = app @@ -5782,78 +5784,8 @@ WEAK CONSTRAINTS: -Query assignments: - M = [[mode-ground], [mode-input]] -Query assignments: - R = app - [global (indc «ex_intro»), global (indt «nat»), - fun `hd_beta_auto` (global (indt «nat»)) c0 \ - app [global (indt «eq»), global (indt «nat»), c0, c0], - global (indc «O»), global (const «p»)] - TY = app - [global (indt «ex»), global (indt «nat»), - fun `hd_beta_auto` (global (indt «nat»)) c0 \ - app [global (indt «eq»), global (indt «nat»), c0, c0]] - _uvk_158_ = X0 - _uvk_159_ = X1 -[trm c0, trm (app [global (const «Nat.add»), c0, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[trm c0, trm (app [global (const «Nat.add»), X0 c0 c1, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X1 c0 c1) (global (indt «nat»)) (X0 c0 c1) /* suspended on X1, X0 */ - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X2 c0 c1) (global (indt «True»)) (X3 c0 c1) /* suspended on X2, X3 */ -[trm c0, trm (app [global (const «Nat.add»), X0 c0 c1, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ -[trm c0, trm c1] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[trm (app [global (const «Nat.add»), c0, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X1 c0 c1) (global (indt «nat»)) (X0 c0 c1) /* suspended on X1, X0 */ - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X2 c0 c1) (global (indt «True»)) (X3 c0 c1) /* suspended on X2, X3 */ -[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ -[trm (app [global (indc «O»), global (indc «O»)])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[trm c0] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[int 1] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[int -1] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[str a] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[str a] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +Finished transaction in 6.435 secs (4.607u,0.007s) (successful) +COQC tests/test_libobject_B.v Query assignments: A4 = «elpi.tests.test_HOAS.36» A5 = «elpi.tests.test_HOAS.37» @@ -6034,62 +5966,30 @@ WEAK CONSTRAINTS: -[str x] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[trm (app [global (const «Nat.add»), c0, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ -[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ -[trm c0] - {c0 c1} : - decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) - ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ -1 -1.000000 Query assignments: R = app [global (indc «ex_intro»), global (indt «nat»), fun `hd_beta_auto` (global (indt «nat»)) c0 \ - app [global (indt «eq»), global (indt «nat»), c0, global (indc «O»)], + app [global (indt «eq»), global (indt «nat»), c0, c0], global (indc «O»), global (const «p»)] TY = app [global (indt «ex»), global (indt «nat»), - fun `n` (global (indt «nat»)) c0 \ - app [global (indt «eq»), global (indt «nat»), c0, global (indc «O»)]] - _uvk_168_ = X0 - _uvk_169_ = c0 \ -X1 c0 - _uvk_170_ = X2 - _uvk_171_ = X3 + fun `hd_beta_auto` (global (indt «nat»)) c0 \ + app [global (indt «eq»), global (indt «nat»), c0, c0]] + _uvk_158_ = X0 + _uvk_159_ = X1 +[(c4 \ app [c1, c2]), (c4 \ app [c0, c2]), (c4 \ c4), (c4 \ + prod `x0` (app [c0, c2]) c5 \ + prod `x1` (global (indt «nat»)) c6 \ + sort (typ «elpi.tests.test_tactic.16»))] +[app + [global (indt «eq»), global (indt «nat»), c2, + app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]], + sort prop] «elpi.tests.test_HOAS.68» parameter T explicit (sort (typ «elpi.tests.test_HOAS.68»)) c0 \ record F (sort (typ «elpi.tests.test_HOAS.68»)) Build_F (field [coercion off, canonical tt] t c0 c1 \ end-record) -Universe constraints: -UNIVERSES: - {elpi.tests.test_elaborator.58 elpi.tests.test_elaborator.57 - elpi.tests.test_elaborator.56 elpi.tests.test_elaborator.55} |= - Set <= elpi.tests.test_elaborator.55 - elpi.tests.test_elaborator.55 <= elpi.tests.test_elaborator.57 - elpi.tests.test_elaborator.56 <= elpi.tests.test_elaborator.57 - elpi.tests.test_elaborator.57 <= elpi.tests.test_elaborator.58 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - «elpi.tests.test_HOAS.68» parameter T explicit (sort (typ «elpi.tests.test_HOAS.68»)) c0 \ record F (sort (typ «elpi.tests.test_HOAS.68»)) Build_F @@ -6121,6 +6021,41 @@ WEAK CONSTRAINTS: +COQC tests/test_libobject_C.v +Query assignments: + R = app + [global (indc «ex_intro»), global (indt «nat»), + fun `hd_beta_auto` (global (indt «nat»)) c0 \ + app [global (indt «eq»), global (indt «nat»), c0, global (indc «O»)], + global (indc «O»), global (const «p»)] + TY = app + [global (indt «ex»), global (indt «nat»), + fun `n` (global (indt «nat»)) c0 \ + app [global (indt «eq»), global (indt «nat»), c0, global (indc «O»)]] + _uvk_168_ = X0 + _uvk_169_ = c0 \ +X1 c0 + _uvk_170_ = X2 + _uvk_171_ = X3 +Universe constraints: +UNIVERSES: + {elpi.tests.test_elaborator.58 elpi.tests.test_elaborator.57 + elpi.tests.test_elaborator.56 elpi.tests.test_elaborator.55} |= + Set <= elpi.tests.test_elaborator.55 + elpi.tests.test_elaborator.55 <= elpi.tests.test_elaborator.57 + elpi.tests.test_elaborator.56 <= elpi.tests.test_elaborator.57 + elpi.tests.test_elaborator.57 <= elpi.tests.test_elaborator.58 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + +global (indc «O») +app + [global (indc «S»), + app [global (indc «S»), app [global (indc «S»), global (indc «O»)]]] «elpi.tests.test_HOAS.70» «elpi.tests.test_HOAS.71» Universe constraints: UNIVERSES: {elpi.tests.test_HOAS.71 elpi.tests.test_HOAS.70} |= @@ -6159,6 +6094,11 @@ WEAK CONSTRAINTS: +COQC tests/test_eq.v +1356 + : nat +this 3 app [c4, X0 c0 c1 c2 c3 c4] +app [c3, app [c1, c2], global (const «a»)] foo.bar Query assignments: R = app [global (indc «ex_intro»), global (indt «nat»), @@ -6189,45 +6129,6 @@ WEAK CONSTRAINTS: -empty_eq : eq_test empty - : eq_test empty -unit_eq : eq_test unit - : eq_test unit -peano_eq : eq_test peano - : eq_test peano -option_eq : forall A : Type, eq_test A -> eq_test (option A) - : forall A : Type, eq_test A -> eq_test (option A) -pair_eq -: -forall A : Type, -eq_test A -> forall B : Type, eq_test B -> eq_test (pair A B) - : forall A : Type, - eq_test A -> forall B : Type, eq_test B -> eq_test (pair A B) -seq_eq : forall A : Type, eq_test A -> eq_test (seq A) - : forall A : Type, eq_test A -> eq_test (seq A) -rose_eq : forall A : Type, eq_test A -> eq_test (rose A) - : forall A : Type, eq_test A -> eq_test (rose A) -vect_eq : forall A : Type, eq_test A -> forall i : peano, eq_test (vect A i) - : forall A : Type, eq_test A -> forall i : peano, eq_test (vect A i) -zeta_eq : forall A : Type, eq_test A -> eq_test (zeta A) - : forall A : Type, eq_test A -> eq_test (zeta A) -beta_eq : forall A : Type, eq_test A -> eq_test (beta A) - : forall A : Type, eq_test A -> eq_test (beta A) -large_eq : eq_test large - : eq_test large -prim_int_eq : eq_test prim_int - : eq_test prim_int -prim_float_eq : eq_test prim_float - : eq_test prim_float -fo_record_eq : eq_test fo_record - : eq_test fo_record -pa_record_eq : forall A : Type, eq_test A -> eq_test (pa_record A) - : forall A : Type, eq_test A -> eq_test (pa_record A) -pr_record_eq : forall A : Type, eq_test A -> eq_test (pr_record A) - : forall A : Type, eq_test A -> eq_test (pr_record A) -enum_eq : eq_test enum - : eq_test enum -COQC tests/test_isK.v «elpi.tests.test_HOAS.72» «» Universe constraints: UNIVERSES: {elpi.tests.test_HOAS.72} |= @@ -6264,9 +6165,22 @@ WEAK CONSTRAINTS: -[attribute elpi.loc - (leaf-loc - File "./tests/test_tactic.v", line 300, column 10, character 6470:)] +Query assignments: + GRF = indt «F» + I1 = «elpi.tests.test_HOAS.73» + I2 = «elpi.tests.test_HOAS.73» + U = «elpi.tests.test_HOAS.73» + UL1 = [«elpi.tests.test_HOAS.73»] +Universe constraints: +UNIVERSES: + {elpi.tests.test_HOAS.73} |= +ALGEBRAIC UNIVERSES: + {elpi.tests.test_HOAS.73} +UNDEFINED UNIVERSES: + elpi.tests.test_HOAS.73 +WEAK CONSTRAINTS: + + Query assignments: A = tt B = 0 @@ -6275,22 +6189,282 @@ E = [«true», «false»] F = [global (indt «bool»), global (indt «bool»)] GR = «bool» +derive.param1_trivial: wrong shape is_nest +. It does not look like a unary parametricity translation of an inductive with no indexes. +File "./tests/test_API2.v", line 114, characters 0-16: +Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] +Cannot enforce elpi.tests.test_HOAS.74 = elpi.tests.test_HOAS.75 because +elpi.tests.test_HOAS.75 < elpi.tests.test_HOAS.75 = elpi.tests.test_HOAS.74 Query assignments: + E = Cannot enforce elpi.tests.test_HOAS.74 = elpi.tests.test_HOAS.75 because +elpi.tests.test_HOAS.75 < elpi.tests.test_HOAS.75 = elpi.tests.test_HOAS.74 GRF = indt «F» - I1 = «elpi.tests.test_HOAS.73» - I2 = «elpi.tests.test_HOAS.73» - U = «elpi.tests.test_HOAS.73» - UL1 = [«elpi.tests.test_HOAS.73»] + I1 = «elpi.tests.test_HOAS.74» + I2 = «elpi.tests.test_HOAS.75» + L1 = «elpi.tests.test_HOAS.74» + L2 = «elpi.tests.test_HOAS.75» + U1 = «elpi.tests.test_HOAS.74» + U2 = «elpi.tests.test_HOAS.75» Universe constraints: UNIVERSES: - {elpi.tests.test_HOAS.73} |= + {elpi.tests.test_HOAS.75 elpi.tests.test_HOAS.74} |= + elpi.tests.test_HOAS.74 < elpi.tests.test_HOAS.75 ALGEBRAIC UNIVERSES: - {elpi.tests.test_HOAS.73} + {elpi.tests.test_HOAS.75 elpi.tests.test_HOAS.74} UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.73 + elpi.tests.test_HOAS.75 + elpi.tests.test_HOAS.74 WEAK CONSTRAINTS: +File "./tests/test_API2.v", line 122, characters 0-14: +Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] +derive.param1_trivial: wrong shape is_vect A PA +. It does not look like a unary parametricity translation of an inductive with no indexes. +Universe constraints: UNIVERSES: + {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} |= + elpi.tests.test_HOAS.78 < elpi.tests.test_HOAS.79 + ALGEBRAIC UNIVERSES: + {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} + UNDEFINED UNIVERSES: + elpi.tests.test_HOAS.79 + elpi.tests.test_HOAS.78 + WEAK CONSTRAINTS: + + +Query assignments: + GRF = indt «F2» + I1 = «elpi.tests.test_HOAS.78» + I2 = «elpi.tests.test_HOAS.79» + L1 = «elpi.tests.test_HOAS.78» + L2 = «elpi.tests.test_HOAS.79» + U1 = «elpi.tests.test_HOAS.78» + U2 = «elpi.tests.test_HOAS.79» +Universe constraints: +UNIVERSES: + {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} |= + elpi.tests.test_HOAS.78 < elpi.tests.test_HOAS.79 + elpi.tests.test_HOAS.78 <= elpi.tests.test_HOAS.79 +ALGEBRAIC UNIVERSES: + {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} +UNDEFINED UNIVERSES: + elpi.tests.test_HOAS.79 + elpi.tests.test_HOAS.78 +WEAK CONSTRAINTS: + + +Query assignments: + F = app [global (const «nat_of_bool»), global (indc «true»)] +[trm c0, trm (app [global (const «Nat.add»), c0, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[trm c0, trm (app [global (const «Nat.add»), X0 c0 c1, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X1 c0 c1) (global (indt «nat»)) (X0 c0 c1) /* suspended on X1, X0 */ + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X2 c0 c1) (global (indt «True»)) (X3 c0 c1) /* suspended on X2, X3 */ +[trm c0, trm (app [global (const «Nat.add»), X0 c0 c1, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ +[trm c0, trm c1] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[trm (app [global (const «Nat.add»), c0, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X1 c0 c1) (global (indt «nat»)) (X0 c0 c1) /* suspended on X1, X0 */ + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X2 c0 c1) (global (indt «True»)) (X3 c0 c1) /* suspended on X2, X3 */ +[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ +[trm (app [global (indc «O»), global (indc «O»)])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[trm c0] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[int 1] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[int -1] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[str a] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[str a] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[str x] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[trm (app [global (const «Nat.add»), c0, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ +[trm (app [global (const «Nat.add»), X0 c0 c1, c1])] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X1 c0 c1) (global (indt «True»)) (X2 c0 c1) /* suspended on X1, X2 */ +[trm c0] + {c0 c1} : + decl c1 `y` (global (indt «nat»)), decl c0 `x` (global (indt «nat»)) + ?- evar (X0 c0 c1) (global (indt «True»)) (X1 c0 c1) /* suspended on X0, X1 */ +c0 \ app [global (const «nat_of_bool»), c0] +Query assignments: + Res = app + [global (const «map»), global (indt «bool»), global (indt «nat»), + fun `x` (global (indt «bool»)) c0 \ + app [global (const «nat_of_bool»), c0], + app + [global (indc «cons»), global (indt «bool»), global (indc «true»), + app [global (indc «nil»), global (indt «bool»)]]] + _uvk_232_ = X0 + _uvk_233_ = X1 +Universe constraints: UNIVERSES: + {elpi.tests.test_HOAS.81 elpi.tests.test_HOAS.80} |= + elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 + ALGEBRAIC UNIVERSES: + {elpi.tests.test_HOAS.81} + UNDEFINED UNIVERSES: + elpi.tests.test_HOAS.81 + elpi.tests.test_HOAS.80 + WEAK CONSTRAINTS: + + +Cannot enforce elpi.tests.test_HOAS.81 = elpi.tests.test_HOAS.80 because +elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 +Query assignments: + E = Cannot enforce elpi.tests.test_HOAS.81 = elpi.tests.test_HOAS.80 because +elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 + GRF = indt «F» + I1 = «elpi.tests.test_HOAS.80» + I2 = «elpi.tests.test_HOAS.81» + L1 = «elpi.tests.test_HOAS.80» + L2 = «elpi.tests.test_HOAS.81» + U1 = «elpi.tests.test_HOAS.80» + U2 = «elpi.tests.test_HOAS.81» +Universe constraints: +UNIVERSES: + {elpi.tests.test_HOAS.81 elpi.tests.test_HOAS.80} |= + elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 +ALGEBRAIC UNIVERSES: + {elpi.tests.test_HOAS.81} +UNDEFINED UNIVERSES: + elpi.tests.test_HOAS.81 + elpi.tests.test_HOAS.80 +WEAK CONSTRAINTS: + + +empty_eq : eq_test empty + : eq_test empty +unit_eq : eq_test unit + : eq_test unit +peano_eq : eq_test peano + : eq_test peano +option_eq : forall A : Type, eq_test A -> eq_test (option A) + : forall A : Type, eq_test A -> eq_test (option A) +pair_eq +: +forall A : Type, +eq_test A -> forall B : Type, eq_test B -> eq_test (pair A B) + : forall A : Type, + eq_test A -> forall B : Type, eq_test B -> eq_test (pair A B) +seq_eq : forall A : Type, eq_test A -> eq_test (seq A) + : forall A : Type, eq_test A -> eq_test (seq A) +rose_eq : forall A : Type, eq_test A -> eq_test (rose A) + : forall A : Type, eq_test A -> eq_test (rose A) +vect_eq : forall A : Type, eq_test A -> forall i : peano, eq_test (vect A i) + : forall A : Type, eq_test A -> forall i : peano, eq_test (vect A i) +zeta_eq : forall A : Type, eq_test A -> eq_test (zeta A) + : forall A : Type, eq_test A -> eq_test (zeta A) +beta_eq : forall A : Type, eq_test A -> eq_test (beta A) + : forall A : Type, eq_test A -> eq_test (beta A) +large_eq : eq_test large + : eq_test large +prim_int_eq : eq_test prim_int + : eq_test prim_int +prim_float_eq : eq_test prim_float + : eq_test prim_float +fo_record_eq : eq_test fo_record + : eq_test fo_record +pa_record_eq : forall A : Type, eq_test A -> eq_test (pa_record A) + : forall A : Type, eq_test A -> eq_test (pa_record A) +pr_record_eq : forall A : Type, eq_test A -> eq_test (pr_record A) + : forall A : Type, eq_test A -> eq_test (pr_record A) +enum_eq : eq_test enum + : eq_test enum +COQC tests/test_isK.v +Query assignments: + C1 = «Nat.add» + C2 = «times» + X1 = tt + X2 = ff +Query assignments: + GR = indt «nat» +Query assignments: + Res = app + [global (const «Z_of_nat»), + app [global (const «nat_of_bool»), global (indc «true»)]] +Query assignments: + C1 = «x» +Query assignments: + GR = indt «F» + I = «elpi.tests.test_HOAS.82» +Universe constraints: +UNIVERSES: + {elpi.tests.test_HOAS.82} |= +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + elpi.tests.test_HOAS.82 +WEAK CONSTRAINTS: + + +[attribute elpi.loc + (leaf-loc + File "./tests/test_tactic.v", line 300, column 10, character 6470:)] +c0 \ +app [global (const «Z_of_nat»), app [global (const «nat_of_bool»), c0]] +Query assignments: + Res = app + [global (const «map»), global (indt «bool»), global (const «Z»), + fun `x` (global (indt «bool»)) c0 \ + app + [global (const «Z_of_nat»), app [global (const «nat_of_bool»), c0]], + app + [global (indc «cons»), global (indt «bool»), global (indc «true»), + app [global (indc «nil»), global (indt «bool»)]]] + _uvk_268_ = X0 + _uvk_269_ = X1 +Query assignments: + C1 = «x» + M = «elpi.tests.test_API2.xx» +Query assignments: + GR = indt «F» Entry constr is [ LEFTA [ "@"; global; univ_annot @@ -6467,33 +6641,51 @@ [attribute elpi.loc (leaf-loc File "./tests/test_tactic.v", line 332, column 7, character 7186:)] Query assignments: - F = app [global (const «nat_of_bool»), global (indc «true»)] -Cannot enforce elpi.tests.test_HOAS.74 = elpi.tests.test_HOAS.75 because -elpi.tests.test_HOAS.75 < elpi.tests.test_HOAS.75 = elpi.tests.test_HOAS.74 + R = prod `r` (global (const «ring»)) c0 \ + prod `x` (app [global (const «carr»), c0]) c1 \ + app [global (indt «eq»), app [global (const «carr»), c0], c1, c1] + T = sort (typ «elpi.tests.test_elaborator.75») + _uvk_304_ = c0 \ c1 \ +X0 c0 c1 +Universe constraints: +UNIVERSES: + {elpi.tests.test_elaborator.75 elpi.tests.test_elaborator.74 + elpi.tests.test_elaborator.73 elpi.tests.test_elaborator.72 + elpi.tests.test_elaborator.70} |= + ring.u0 <= elpi.tests.test_elaborator.70 + elpi.tests.test_elaborator.70 <= elpi.tests.test_elaborator.75 + elpi.tests.test_elaborator.73 <= elpi.tests.test_elaborator.74 + elpi.tests.test_elaborator.74 <= elpi.tests.test_elaborator.75 +ALGEBRAIC UNIVERSES: + {} +UNDEFINED UNIVERSES: + +WEAK CONSTRAINTS: + + +Debug: Cannot enforce elpi.apps.derive.tests.test_derive.3312 <= Set Query assignments: - E = Cannot enforce elpi.tests.test_HOAS.74 = elpi.tests.test_HOAS.75 because -elpi.tests.test_HOAS.75 < elpi.tests.test_HOAS.75 = elpi.tests.test_HOAS.74 - GRF = indt «F» - I1 = «elpi.tests.test_HOAS.74» - I2 = «elpi.tests.test_HOAS.75» - L1 = «elpi.tests.test_HOAS.74» - L2 = «elpi.tests.test_HOAS.75» - U1 = «elpi.tests.test_HOAS.74» - U2 = «elpi.tests.test_HOAS.75» + C1 = «x» + M = «elpi.tests.test_API2.xx2» +pglobal (indt «F») «elpi.tests.test_HOAS.84» +«elpi.tests.test_HOAS.84» +pglobal (indc «Build_F») «elpi.tests.test_HOAS.84» +Query assignments: + GR = indt «F» + GR1 = indc «Build_F» + I = «elpi.tests.test_HOAS.84» + Spilled_1 = pglobal (indc «Build_F») «elpi.tests.test_HOAS.84» + Spilled_2 = pglobal (indt «F») «elpi.tests.test_HOAS.84» Universe constraints: UNIVERSES: - {elpi.tests.test_HOAS.75 elpi.tests.test_HOAS.74} |= - elpi.tests.test_HOAS.74 < elpi.tests.test_HOAS.75 + {elpi.tests.test_HOAS.84} |= ALGEBRAIC UNIVERSES: - {elpi.tests.test_HOAS.75 elpi.tests.test_HOAS.74} + {} UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.75 - elpi.tests.test_HOAS.74 + elpi.tests.test_HOAS.84 WEAK CONSTRAINTS: -File "./tests/test_API2.v", line 114, characters 0-16: -Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] H goal [] (X0) (global (indt «True»)) X1 [trm (global (const «H»))] goal [] (X0) (global (indt «True»)) X1 @@ -6503,88 +6695,34 @@ global (const «H»)])] goal [] (X0) (global (indt «True»)) X1 [trm (global (const «H»))] COQC tests/test_param1.v -Universe constraints: UNIVERSES: - {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} |= - elpi.tests.test_HOAS.78 < elpi.tests.test_HOAS.79 - ALGEBRAIC UNIVERSES: - {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} - UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.79 - elpi.tests.test_HOAS.78 - WEAK CONSTRAINTS: - - +«elpi.tests.test_HOAS.85 elpi.tests.test_HOAS.85» Query assignments: - GRF = indt «F2» - I1 = «elpi.tests.test_HOAS.78» - I2 = «elpi.tests.test_HOAS.79» - L1 = «elpi.tests.test_HOAS.78» - L2 = «elpi.tests.test_HOAS.79» - U1 = «elpi.tests.test_HOAS.78» - U2 = «elpi.tests.test_HOAS.79» + I = «elpi.tests.test_HOAS.85 elpi.tests.test_HOAS.85» + U = «elpi.tests.test_HOAS.85» Universe constraints: UNIVERSES: - {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} |= - elpi.tests.test_HOAS.78 < elpi.tests.test_HOAS.79 - elpi.tests.test_HOAS.78 <= elpi.tests.test_HOAS.79 + {elpi.tests.test_HOAS.85} |= ALGEBRAIC UNIVERSES: - {elpi.tests.test_HOAS.79 elpi.tests.test_HOAS.78} + {} UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.79 - elpi.tests.test_HOAS.78 -WEAK CONSTRAINTS: - -File "./tests/test_API2.v", line 122, characters 0-14: -Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] -c0 \ app [global (const «nat_of_bool»), c0] -Query assignments: - Res = app - [global (const «map»), global (indt «bool»), global (indt «nat»), - fun `x` (global (indt «bool»)) c0 \ - app [global (const «nat_of_bool»), c0], - app - [global (indc «cons»), global (indt «bool»), global (indc «true»), - app [global (indc «nil»), global (indt «bool»)]]] - _uvk_232_ = X0 - _uvk_233_ = X1 -Universe constraints: UNIVERSES: - {elpi.tests.test_HOAS.81 elpi.tests.test_HOAS.80} |= - elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 - ALGEBRAIC UNIVERSES: - {elpi.tests.test_HOAS.81} - UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.81 - elpi.tests.test_HOAS.80 - WEAK CONSTRAINTS: - - -Cannot enforce elpi.tests.test_HOAS.81 = elpi.tests.test_HOAS.80 because -elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 -Query assignments: - E = Cannot enforce elpi.tests.test_HOAS.81 = elpi.tests.test_HOAS.80 because -elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 - GRF = indt «F» - I1 = «elpi.tests.test_HOAS.80» - I2 = «elpi.tests.test_HOAS.81» - L1 = «elpi.tests.test_HOAS.80» - L2 = «elpi.tests.test_HOAS.81» - U1 = «elpi.tests.test_HOAS.80» - U2 = «elpi.tests.test_HOAS.81» -Universe constraints: -UNIVERSES: - {elpi.tests.test_HOAS.81 elpi.tests.test_HOAS.80} |= - elpi.tests.test_HOAS.80 < elpi.tests.test_HOAS.81 -ALGEBRAIC UNIVERSES: - {elpi.tests.test_HOAS.81} -UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.81 - elpi.tests.test_HOAS.80 WEAK CONSTRAINTS: -derive.param1_trivial: wrong shape is_nest -. It does not look like a unary parametricity translation of an inductive with no indexes. +Skipping derivation map on indt «nat» since it has been already run +Derivation lens on indt «nat» +Derivation lens on indt «nat» failed, continuing +Skipping derivation param1 on indt «nat» since it has been already run +Skipping derivation param2 on indt «nat» since it has been already run +Skipping derivation tag on indt «nat» since it has been already run +Skipping derivation eqType_ast on indt «nat» since it has been already run +Derivation projK on indt «nat» +Derivation projK on indt «nat» took 0.011865 +Derivation isK on indt «nat» +Derivation isK on indt «nat» took 0.026658 +Derivation eq on indt «nat» +Derivation eq on indt «nat» took 0.025115 +Derivation invert on indt «nat» unit_is_tt : unit -> bool : unit -> bool peano_is_Zero : peano -> bool @@ -6605,8 +6743,18 @@ : forall A : Type, rose A -> bool rose_is_Node : forall A : Type, rose A -> bool : forall A : Type, rose A -> bool +Derivation invert on indt «nat» took 0.032244 +Skipping derivation lens_laws on indt «nat» since it has been already run +Skipping derivation param1_congr on indt «nat» +since it has been already run +Skipping derivation param1_inhab on indt «nat» +since it has been already run +Skipping derivation param1_functor on indt «nat» +since it has been already run nest_is_NilN : forall A : Type, nest A -> bool : forall A : Type, nest A -> bool +Skipping derivation fields on indt «nat» since it has been already run +Derivation bcongr on indt «nat» nest_is_ConsN : forall A : Type, nest A -> bool : forall A : Type, nest A -> bool w_is_via : forall A : Type, w A -> bool @@ -6637,75 +6785,107 @@ : forall A : Type, pa_record A -> bool pr_record_is_Build_pr_record : forall A : Type, pr_record A -> bool : forall A : Type, pr_record A -> bool -Query assignments: - Res = app - [global (const «Z_of_nat»), - app [global (const «nat_of_bool»), global (indc «true»)]] enum_is_E1 : enum -> bool : enum -> bool +Derivation bcongr on indt «nat» took 0.031738 +Derivation idx2inv on indt «nat» +Derivation idx2inv on indt «nat» failed, continuing +Skipping derivation param1_trivial on indt «nat» +since it has been already run +Skipping derivation induction on indt «nat» since it has been already run +Skipping derivation eqb on indt «nat» since it has been already run +Derivation eqK on indt «nat» +Derivation eqK on indt «nat» took 0.024860 +Skipping derivation eqbcorrect on indt «nat» since it has been already run +Derivation eqcorrect on indt «nat» +Derivation eqcorrect on indt «nat» took 0.007106 +Skipping derivation eqbOK on indt «nat» since it has been already run +Derivation eqOK on indt «nat» +Derivation eqOK on indt «nat» took 0.005839 +nat_eqb : nat -> nat -> bool + : nat -> nat -> bool +is_nat : nat -> Type + : nat -> Type +is_nat_inhab : (forall x : nat, is_nat x) + : forall x : nat, is_nat x +is_nat_functor : (forall x : nat, is_nat x -> is_nat x) + : forall x : nat, is_nat x -> is_nat x COQC tests/test_map.v -Query assignments: - GR = indt «nat» -derive.param1_trivial: wrong shape is_vect A PA -. It does not look like a unary parametricity translation of an inductive with no indexes. -Query assignments: - C1 = «Nat.add» - C2 = «times» - X1 = tt - X2 = ff -c0 \ -app [global (const «Z_of_nat»), app [global (const «nat_of_bool»), c0]] -Query assignments: - Res = app - [global (const «map»), global (indt «bool»), global (const «Z»), - fun `x` (global (indt «bool»)) c0 \ - app - [global (const «Z_of_nat»), app [global (const «nat_of_bool»), c0]], - app - [global (indc «cons»), global (indt «bool»), global (indc «true»), - app [global (indc «nil»), global (indt «bool»)]]] - _uvk_268_ = X0 - _uvk_269_ = X1 -Query assignments: - GR = indt «F» - I = «elpi.tests.test_HOAS.82» -Universe constraints: -UNIVERSES: - {elpi.tests.test_HOAS.82} |= -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.82 -WEAK CONSTRAINTS: - - -Query assignments: - C1 = «x» -Query assignments: - GR = indt «F» -Query assignments: - R = prod `r` (global (const «ring»)) c0 \ - prod `x` (app [global (const «carr»), c0]) c1 \ - app [global (indt «eq»), app [global (const «carr»), c0], c1, c1] - T = sort (typ «elpi.tests.test_elaborator.75») - _uvk_304_ = c0 \ c1 \ -X0 c0 c1 -Universe constraints: -UNIVERSES: - {elpi.tests.test_elaborator.75 elpi.tests.test_elaborator.74 - elpi.tests.test_elaborator.73 elpi.tests.test_elaborator.72 - elpi.tests.test_elaborator.70} |= - ring.u0 <= elpi.tests.test_elaborator.70 - elpi.tests.test_elaborator.70 <= elpi.tests.test_elaborator.75 - elpi.tests.test_elaborator.73 <= elpi.tests.test_elaborator.74 - elpi.tests.test_elaborator.74 <= elpi.tests.test_elaborator.75 -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - +nat_induction + : (forall P : nat -> Type, + P 0 -> + (forall n : nat, P n -> P (S n)) -> forall x : nat, is_nat x -> P x) + : forall P : nat -> Type, + P 0 -> + (forall n : nat, P n -> P (S n)) -> forall x : nat, is_nat x -> P x +nat_tag : nat -> BinNums.positive + : nat -> BinNums.positive +nat_fields_t : BinNums.positive -> Type + : BinNums.positive -> Type +nat_fields : (forall n : nat, nat_fields_t (nat_tag n)) + : forall n : nat, nat_fields_t (nat_tag n) +nat_construct : (forall p : BinNums.positive, nat_fields_t p -> option nat) + : forall p : BinNums.positive, nat_fields_t p -> option nat +nat_constructP + : (forall n : nat, nat_construct (nat_tag n) (nat_fields n) = Some n) + : forall n : nat, nat_construct (nat_tag n) (nat_fields n) = Some n +nat_eqb : nat -> nat -> bool + : nat -> nat -> bool +nat_eqb_correct + : forall x : nat, eqb_correct_on nat_eqb x +nat_eqb_refl + : forall x : nat, eqb_refl_on nat_eqb x +list_map : (forall A B : Type, (A -> B) -> list A -> list B) + : forall A B : Type, (A -> B) -> list A -> list B +is_nil : (forall (A : Type) (P : A -> Type), is_list A P nil) + : forall (A : Type) (P : A -> Type), is_list A P nil +is_cons + : (forall (A : Type) (P : A -> Type) (x : A), + P x -> forall tl : list A, is_list A P tl -> is_list A P (x :: tl)) + : forall (A : Type) (P : A -> Type) (x : A), + P x -> forall tl : list A, is_list A P tl -> is_list A P (x :: tl) +is_list_functor + : (forall (A : Type) (P Q : A -> Type), + (forall x : A, P x -> Q x) -> + forall l : list A, is_list A P l -> is_list A Q l) + : forall (A : Type) (P Q : A -> Type), + (forall x : A, P x -> Q x) -> + forall l : list A, is_list A P l -> is_list A Q l +list_induction + : (forall (A : Type) (PA : A -> Type) (P : list A -> Type), + P nil -> + (forall x : A, PA x -> forall xs : list A, P xs -> P (x :: xs)%list) -> + forall l : list A, is_list A PA l -> P l) + : forall (A : Type) (PA : A -> Type) (P : list A -> Type), + P nil -> + (forall x : A, PA x -> forall xs : list A, P xs -> P (x :: xs)%list) -> + forall l : list A, is_list A PA l -> P l +list_tag : (forall A : Type, list A -> BinNums.positive) + : forall A : Type, list A -> BinNums.positive +list_fields_t : Type -> BinNums.positive -> Type + : Type -> BinNums.positive -> Type +list_fields + : (forall (A : Type) (l : list A), list_fields_t A (list_tag A l)) + : forall (A : Type) (l : list A), list_fields_t A (list_tag A l) +list_construct + : (forall (A : Type) (p : BinNums.positive), + list_fields_t A p -> option (list A)) + : forall (A : Type) (p : BinNums.positive), + list_fields_t A p -> option (list A) +list_constructP + : (forall (A : Type) (l : list A), + list_construct A (list_tag A l) (list_fields A l) = Some l) + : forall (A : Type) (l : list A), + list_construct A (list_tag A l) (list_fields A l) = Some l +list_eqb : (forall A : Type, (A -> A -> bool) -> list A -> list A -> bool) + : forall A : Type, (A -> A -> bool) -> list A -> list A -> bool +list_eqb_correct + : forall (a : Type) (eqA : a -> a -> bool), + eqb_correct eqA -> + forall x : list a, eqb_correct_on (list_eqb a eqA) x +list_eqb_refl + : forall (a : Type) (eqA : a -> a -> bool), + eqb_reflexive eqA -> forall x : list a, eqb_refl_on (list_eqb a eqA) x projSucc1 : peano -> peano -> peano : peano -> peano -> peano projSome1 : forall A : Type, A -> option A -> A @@ -6774,6 +6954,9 @@ | Zero => peano | Succ _ => unit end -> iota -> peano +Query assignments: + C1 = «x» + M = «elpi.tests.test_API2.xx3» projWhy2 : forall n : peano, @@ -6807,193 +6990,6 @@ : forall A : Type, peano -> A -> pa_record A -> A projBuild_pr_record2 : forall A : Type, peano -> A -> pr_record A -> A : forall A : Type, peano -> A -> pr_record A -> A -COQC tests/test_lens_laws.v -Query assignments: - C1 = «x» - M = «elpi.tests.test_API2.xx» -empty_map : map empty - : map empty -unit_map : map unit - : map unit -peano_map : map peano - : map peano -option_map : map1 option - : map1 option -pair_map -: -forall A B : Type, -(A -> B) -> forall C D : Type, (C -> D) -> pair A C -> pair B D - : forall A B : Type, - (A -> B) -> forall C D : Type, (C -> D) -> pair A C -> pair B D -seq_map : map1 seq - : map1 seq -rose_map : map1 rose - : map1 rose -vect_map -: -forall A B : Type, (A -> B) -> forall i : peano, vect A i -> vect B i - : forall A B : Type, (A -> B) -> forall i : peano, vect A i -> vect B i -dyn_map : map dyn - : map dyn -zeta_map : map1 zeta - : map1 zeta -iota_map : map iota - : map iota -large_map : map large - : map large -prim_int_map : map prim_int - : map prim_int -prim_float_map : map prim_float - : map prim_float -pa_record_map : map1 pa_record - : map1 pa_record -pr_record_map : map1 pr_record - : map1 pr_record -pglobal (indt «F») «elpi.tests.test_HOAS.84» -«elpi.tests.test_HOAS.84» -pglobal (indc «Build_F») «elpi.tests.test_HOAS.84» -Query assignments: - GR = indt «F» - GR1 = indc «Build_F» - I = «elpi.tests.test_HOAS.84» - Spilled_1 = pglobal (indc «Build_F») «elpi.tests.test_HOAS.84» - Spilled_2 = pglobal (indt «F») «elpi.tests.test_HOAS.84» -Universe constraints: -UNIVERSES: - {elpi.tests.test_HOAS.84} |= -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - elpi.tests.test_HOAS.84 -WEAK CONSTRAINTS: - - -COQC tests/test_fields.v -is_empty : pred empty - : pred empty -is_unit : pred unit - : pred unit -is_peano : pred peano - : pred peano -is_option : forall A : Type, pred A -> pred (option A) - : forall A : Type, pred A -> pred (option A) -is_pair -: -forall A : Type, pred A -> forall B : Type, pred B -> pred (pair A B) - : forall A : Type, pred A -> forall B : Type, pred B -> pred (pair A B) -is_seq : forall A : Type, pred A -> pred (seq A) - : forall A : Type, pred A -> pred (seq A) -is_rose : forall A : Type, pred A -> pred (rose A) - : forall A : Type, pred A -> pred (rose A) -is_nest : forall A : Type, pred A -> pred (nest A) - : forall A : Type, pred A -> pred (nest A) -is_w : forall A : Type, pred A -> pred (w A) - : forall A : Type, pred A -> pred (w A) -is_vect -: -forall A : Type, pred A -> forall i : peano, is_peano i -> pred (vect A i) - : forall A : Type, - pred A -> forall i : peano, is_peano i -> pred (vect A i) -is_dyn : pred dyn - : pred dyn -is_zeta : forall A : Type, pred A -> pred (zeta A) - : forall A : Type, pred A -> pred (zeta A) -is_beta : forall A : Type, pred A -> pred (beta A) - : forall A : Type, pred A -> pred (beta A) -is_iota : pred iota - : pred iota -is_large : pred large - : pred large -is_prim_int : pred prim_int - : pred prim_int -is_prim_float : pred prim_float - : pred prim_float -is_fo_record : pred fo_record - : pred fo_record -is_pa_record : forall A : Type, pred A -> pred (pa_record A) - : forall A : Type, pred A -> pred (pa_record A) -is_pr_record : forall A : Type, pred A -> pred (pr_record A) - : forall A : Type, pred A -> pred (pr_record A) -is_enum : pred enum - : pred enum -is_ord : forall p : peano, is_peano p -> pred (ord p) - : forall p : peano, is_peano p -> pred (ord p) -is_ord2 : forall p : peano, is_peano p -> pred (ord2 p) - : forall p : peano, is_peano p -> pred (ord2 p) -is_val : pred val - : pred val -Query assignments: - C1 = «x» - M = «elpi.tests.test_API2.xx2» -«elpi.tests.test_HOAS.85 elpi.tests.test_HOAS.85» -Query assignments: - I = «elpi.tests.test_HOAS.85 elpi.tests.test_HOAS.85» - U = «elpi.tests.test_HOAS.85» -Universe constraints: -UNIVERSES: - {elpi.tests.test_HOAS.85} |= -ALGEBRAIC UNIVERSES: - {} -UNDEFINED UNIVERSES: - -WEAK CONSTRAINTS: - - -Query assignments: - T = global (const «int») - X = primitive (uint63 99) -_f1_view_set : view_set _f1 - : view_set _f1 -_f2_view_set : view_set _f2 - : view_set _f2 -_f3_view_set : forall A : Type, view_set _f3 - : forall A : Type, view_set _f3 -_f4_view_set : forall A : Type, view_set _f4 - : forall A : Type, view_set _f4 -_pf3_view_set : forall A : Type, view_set _pf3 - : forall A : Type, view_set _pf3 -_pf4_view_set : forall A : Type, view_set _pf4 - : forall A : Type, view_set _pf4 -_f1_set_set : set_set _f1 - : set_set _f1 -_f2_set_set : set_set _f2 - : set_set _f2 -_f3_set_set : forall A : Type, set_set _f3 - : forall A : Type, set_set _f3 -_f4_set_set : forall A : Type, set_set _f4 - : forall A : Type, set_set _f4 -_pf3_set_set : forall A : Type, set_set _pf3 - : forall A : Type, set_set _pf3 -_pf4_set_set : forall A : Type, set_set _pf4 - : forall A : Type, set_set _pf4 -_f1_set_view : set_view _f1 - : set_view _f1 -_f2_set_view : set_view _f2 - : set_view _f2 -_f3_set_view : forall A : Type, set_view _f3 - : forall A : Type, set_view _f3 -_f4_set_view : forall A : Type, set_view _f4 - : forall A : Type, set_view _f4 -_pf3_set_view : forall A : Type, set_view _pf3 - : forall A : Type, set_view _pf3 -_pf4_set_view : forall A : Type, set_view _pf4 - : forall A : Type, set_view _pf4 -_f1_f2_exchange : exchange _f1 _f2 - : exchange _f1 _f2 -_f2_f1_exchange : exchange _f2 _f1 - : exchange _f2 _f1 -_f3_f4_exchange : forall A : Type, exchange _f3 _f4 - : forall A : Type, exchange _f3 _f4 -_f4_f3_exchange : forall A : Type, exchange _f4 _f3 - : forall A : Type, exchange _f4 _f3 -_pf3_pf4_exchange : forall A : Type, exchange _pf3 _pf4 - : forall A : Type, exchange _pf3 _pf4 -_pf4_pf3_exchange : forall A : Type, exchange _pf4 _pf3 - : forall A : Type, exchange _pf4 _pf3 -COQC tests/test_bcongr.v -Query assignments: - C1 = «x» - M = «elpi.tests.test_API2.xx3» Universe constraints: ------------------ Universe constraints: UNIVERSES: @@ -7047,10 +7043,10 @@ : Type@{elpi.tests.test_HOAS.88} (* {elpi.tests.test_HOAS.88} |= Set < elpi.tests.test_HOAS.88 *) Box not a defined object. -Debug: Cannot enforce elpi.apps.derive.tests.test_derive.3312 <= Set Query assignments: - T = global (const «float») - X = primitive (float64 993000) + T = global (const «int») + X = primitive (uint63 99) +COQC tests/test_lens_laws.v sort (typ «Set») Query assignments: U = «elpi.tests.test_HOAS.89» @@ -7071,128 +7067,9 @@ Arguments tree A%type_scope Arguments leaf A%type_scope _ Arguments node A%type_scope _ _%list_scope -Skipping derivation map on indt «nat» since it has been already run -Derivation lens on indt «nat» -Derivation lens on indt «nat» failed, continuing -Skipping derivation param1 on indt «nat» since it has been already run -Skipping derivation param2 on indt «nat» since it has been already run -Skipping derivation tag on indt «nat» since it has been already run -Skipping derivation eqType_ast on indt «nat» since it has been already run -Derivation projK on indt «nat» -Derivation projK on indt «nat» took 0.008066 -Derivation isK on indt «nat» -Derivation isK on indt «nat» took 0.015145 -Derivation eq on indt «nat» -Derivation eq on indt «nat» took 0.013717 -Derivation invert on indt «nat» -Derivation invert on indt «nat» took 0.016040 -Skipping derivation lens_laws on indt «nat» since it has been already run -Skipping derivation param1_congr on indt «nat» -since it has been already run -Skipping derivation param1_inhab on indt «nat» -since it has been already run -Skipping derivation param1_functor on indt «nat» -since it has been already run -Skipping derivation fields on indt «nat» since it has been already run -Derivation bcongr on indt «nat» -Derivation bcongr on indt «nat» took 0.017537 -Derivation idx2inv on indt «nat» -Derivation idx2inv on indt «nat» failed, continuing -Skipping derivation param1_trivial on indt «nat» -since it has been already run -Skipping derivation induction on indt «nat» since it has been already run -Skipping derivation eqb on indt «nat» since it has been already run -Derivation eqK on indt «nat» -Derivation eqK on indt «nat» took 0.020508 -Skipping derivation eqbcorrect on indt «nat» since it has been already run -Derivation eqcorrect on indt «nat» -Derivation eqcorrect on indt «nat» took 0.007197 -Skipping derivation eqbOK on indt «nat» since it has been already run -Derivation eqOK on indt «nat» -Derivation eqOK on indt «nat» took 0.005641 -nat_eqb : nat -> nat -> bool - : nat -> nat -> bool -is_nat : nat -> Type - : nat -> Type -is_nat_inhab : (forall x : nat, is_nat x) - : forall x : nat, is_nat x -is_nat_functor : (forall x : nat, is_nat x -> is_nat x) - : forall x : nat, is_nat x -> is_nat x -nat_induction - : (forall P : nat -> Type, - P 0 -> - (forall n : nat, P n -> P (S n)) -> forall x : nat, is_nat x -> P x) - : forall P : nat -> Type, - P 0 -> - (forall n : nat, P n -> P (S n)) -> forall x : nat, is_nat x -> P x -nat_tag : nat -> BinNums.positive - : nat -> BinNums.positive -nat_fields_t : BinNums.positive -> Type - : BinNums.positive -> Type -nat_fields : (forall n : nat, nat_fields_t (nat_tag n)) - : forall n : nat, nat_fields_t (nat_tag n) -nat_construct : (forall p : BinNums.positive, nat_fields_t p -> option nat) - : forall p : BinNums.positive, nat_fields_t p -> option nat -nat_constructP - : (forall n : nat, nat_construct (nat_tag n) (nat_fields n) = Some n) - : forall n : nat, nat_construct (nat_tag n) (nat_fields n) = Some n -nat_eqb : nat -> nat -> bool - : nat -> nat -> bool -nat_eqb_correct - : forall x : nat, eqb_correct_on nat_eqb x -nat_eqb_refl - : forall x : nat, eqb_refl_on nat_eqb x -list_map : (forall A B : Type, (A -> B) -> list A -> list B) - : forall A B : Type, (A -> B) -> list A -> list B -is_nil : (forall (A : Type) (P : A -> Type), is_list A P nil) - : forall (A : Type) (P : A -> Type), is_list A P nil -is_cons - : (forall (A : Type) (P : A -> Type) (x : A), - P x -> forall tl : list A, is_list A P tl -> is_list A P (x :: tl)) - : forall (A : Type) (P : A -> Type) (x : A), - P x -> forall tl : list A, is_list A P tl -> is_list A P (x :: tl) -is_list_functor - : (forall (A : Type) (P Q : A -> Type), - (forall x : A, P x -> Q x) -> - forall l : list A, is_list A P l -> is_list A Q l) - : forall (A : Type) (P Q : A -> Type), - (forall x : A, P x -> Q x) -> - forall l : list A, is_list A P l -> is_list A Q l -list_induction - : (forall (A : Type) (PA : A -> Type) (P : list A -> Type), - P nil -> - (forall x : A, PA x -> forall xs : list A, P xs -> P (x :: xs)%list) -> - forall l : list A, is_list A PA l -> P l) - : forall (A : Type) (PA : A -> Type) (P : list A -> Type), - P nil -> - (forall x : A, PA x -> forall xs : list A, P xs -> P (x :: xs)%list) -> - forall l : list A, is_list A PA l -> P l -list_tag : (forall A : Type, list A -> BinNums.positive) - : forall A : Type, list A -> BinNums.positive -list_fields_t : Type -> BinNums.positive -> Type - : Type -> BinNums.positive -> Type -list_fields - : (forall (A : Type) (l : list A), list_fields_t A (list_tag A l)) - : forall (A : Type) (l : list A), list_fields_t A (list_tag A l) -list_construct - : (forall (A : Type) (p : BinNums.positive), - list_fields_t A p -> option (list A)) - : forall (A : Type) (p : BinNums.positive), - list_fields_t A p -> option (list A) -list_constructP - : (forall (A : Type) (l : list A), - list_construct A (list_tag A l) (list_fields A l) = Some l) - : forall (A : Type) (l : list A), - list_construct A (list_tag A l) (list_fields A l) = Some l -list_eqb : (forall A : Type, (A -> A -> bool) -> list A -> list A -> bool) - : forall A : Type, (A -> A -> bool) -> list A -> list A -> bool -list_eqb_correct - : forall (a : Type) (eqA : a -> a -> bool), - eqb_correct eqA -> - forall x : list a, eqb_correct_on (list_eqb a eqA) x -list_eqb_refl - : forall (a : Type) (eqA : a -> a -> bool), - eqb_reflexive eqA -> forall x : list a, eqb_refl_on (list_eqb a eqA) x +Query assignments: + T = global (const «float») + X = primitive (float64 993000) parameter A explicit (sort (typ «elpi.tests.test_HOAS.98»)) c0 \ inductive tree tt (arity (sort (typ «elpi.tests.test_HOAS.99»))) c1 \ [constructor leaf (arity (prod `_` c0 c2 \ c1)), @@ -7253,8 +7130,56 @@ WEAK CONSTRAINTS: -Query assignments: - Y = global (indc «is_O») +_f1_view_set : view_set _f1 + : view_set _f1 +_f2_view_set : view_set _f2 + : view_set _f2 +_f3_view_set : forall A : Type, view_set _f3 + : forall A : Type, view_set _f3 +COQC tests/test_fields.v +_f4_view_set : forall A : Type, view_set _f4 + : forall A : Type, view_set _f4 +_pf3_view_set : forall A : Type, view_set _pf3 + : forall A : Type, view_set _pf3 +_pf4_view_set : forall A : Type, view_set _pf4 + : forall A : Type, view_set _pf4 +_f1_set_set : set_set _f1 + : set_set _f1 +_f2_set_set : set_set _f2 + : set_set _f2 +_f3_set_set : forall A : Type, set_set _f3 + : forall A : Type, set_set _f3 +_f4_set_set : forall A : Type, set_set _f4 + : forall A : Type, set_set _f4 +_pf3_set_set : forall A : Type, set_set _pf3 + : forall A : Type, set_set _pf3 +_pf4_set_set : forall A : Type, set_set _pf4 + : forall A : Type, set_set _pf4 +_f1_set_view : set_view _f1 + : set_view _f1 +_f2_set_view : set_view _f2 + : set_view _f2 +_f3_set_view : forall A : Type, set_view _f3 + : forall A : Type, set_view _f3 +_f4_set_view : forall A : Type, set_view _f4 + : forall A : Type, set_view _f4 +_pf3_set_view : forall A : Type, set_view _pf3 + : forall A : Type, set_view _pf3 +_pf4_set_view : forall A : Type, set_view _pf4 + : forall A : Type, set_view _pf4 +_f1_f2_exchange : exchange _f1 _f2 + : exchange _f1 _f2 +_f2_f1_exchange : exchange _f2 _f1 + : exchange _f2 _f1 +_f3_f4_exchange : forall A : Type, exchange _f3 _f4 + : forall A : Type, exchange _f3 _f4 +_f4_f3_exchange : forall A : Type, exchange _f4 _f3 + : forall A : Type, exchange _f4 _f3 +_pf3_pf4_exchange : forall A : Type, exchange _pf3 _pf4 + : forall A : Type, exchange _pf3 _pf4 +_pf4_pf3_exchange : forall A : Type, exchange _pf4 _pf3 + : forall A : Type, exchange _pf4 _pf3 +COQC tests/test_bcongr.v Query assignments: _uvk_1_ = X0 _uvk_2_ = X1 @@ -7280,6 +7205,114 @@ For any goal -> For xeq -> exact xxx(level 0, pattern 0 = _, id 0) +empty_map : map empty + : map empty +unit_map : map unit + : map unit +peano_map : map peano + : map peano +option_map : map1 option + : map1 option +pair_map +: +forall A B : Type, +(A -> B) -> forall C D : Type, (C -> D) -> pair A C -> pair B D + : forall A B : Type, + (A -> B) -> forall C D : Type, (C -> D) -> pair A C -> pair B D +seq_map : map1 seq + : map1 seq +rose_map : map1 rose + : map1 rose +vect_map +: +forall A B : Type, (A -> B) -> forall i : peano, vect A i -> vect B i + : forall A B : Type, (A -> B) -> forall i : peano, vect A i -> vect B i +dyn_map : map dyn + : map dyn +zeta_map : map1 zeta + : map1 zeta +iota_map : map iota + : map iota +large_map : map large + : map large +prim_int_map : map prim_int + : map prim_int +prim_float_map : map prim_float + : map prim_float +pa_record_map : map1 pa_record + : map1 pa_record +pr_record_map : map1 pr_record + : map1 pr_record +Query assignments: + type_1 = «elpi.tests.test_API2.7» +Universe constraints: +UNIVERSES: + +ALGEBRAIC UNIVERSES: + {elpi.tests.test_API2.7} +UNDEFINED UNIVERSES: + elpi.tests.test_API2.7 +WEAK CONSTRAINTS: + + +is_empty : pred empty + : pred empty +is_unit : pred unit + : pred unit +is_peano : pred peano + : pred peano +is_option : forall A : Type, pred A -> pred (option A) + : forall A : Type, pred A -> pred (option A) +is_pair +: +forall A : Type, pred A -> forall B : Type, pred B -> pred (pair A B) + : forall A : Type, pred A -> forall B : Type, pred B -> pred (pair A B) +is_seq : forall A : Type, pred A -> pred (seq A) + : forall A : Type, pred A -> pred (seq A) +is_rose : forall A : Type, pred A -> pred (rose A) + : forall A : Type, pred A -> pred (rose A) +is_nest : forall A : Type, pred A -> pred (nest A) + : forall A : Type, pred A -> pred (nest A) +is_w : forall A : Type, pred A -> pred (w A) + : forall A : Type, pred A -> pred (w A) +is_vect +: +forall A : Type, pred A -> forall i : peano, is_peano i -> pred (vect A i) + : forall A : Type, + pred A -> forall i : peano, is_peano i -> pred (vect A i) +is_dyn : pred dyn + : pred dyn +is_zeta : forall A : Type, pred A -> pred (zeta A) + : forall A : Type, pred A -> pred (zeta A) +is_beta : forall A : Type, pred A -> pred (beta A) + : forall A : Type, pred A -> pred (beta A) +is_iota : pred iota + : pred iota +is_large : pred large + : pred large +is_prim_int : pred prim_int + : pred prim_int +is_prim_float : pred prim_float + : pred prim_float +is_fo_record : pred fo_record + : pred fo_record +is_pa_record : forall A : Type, pred A -> pred (pa_record A) + : forall A : Type, pred A -> pred (pa_record A) +is_pr_record : forall A : Type, pred A -> pred (pr_record A) + : forall A : Type, pred A -> pred (pr_record A) +is_enum : pred enum + : pred enum +is_ord : forall p : peano, is_peano p -> pred (ord p) + : forall p : peano, is_peano p -> pred (ord p) +is_ord2 : forall p : peano, is_peano p -> pred (ord2 p) + : forall p : peano, is_peano p -> pred (ord2 p) +is_val : pred val + : pred val +Query assignments: + _uvk_317_ = X0 +Query assignments: + GR = const const EXN PRINTING: Not_found + T = «elpi.tests.test_API2.T» unit_bcongr_tt : reflect (tt = tt) true : reflect (tt = tt) true peano_bcongr_Zero : reflect (Zero = Zero) true @@ -7328,10 +7361,6 @@ reflect (x = y) b -> reflect (Leaf A x = Leaf A y) b : forall (A : Type) (x y : A) (b : bool), reflect (x = y) b -> reflect (Leaf A x = Leaf A y) b -Query assignments: - Y = app - [global (indc «is_S»), app [global (indc «S»), global (indc «O»)], - app [global (indc «is_S»), global (indc «O»), global (indc «is_O»)]] rose_bcongr_Node : forall (A : Type) (l1 l2 : seq (rose A)) (b : bool), @@ -7432,40 +7461,22 @@ : reflect (E2 = E2) true enum_bcongr_E3 : reflect (E3 = E3) true : reflect (E3 = E3) true -Query assignments: - _uvk_317_ = X0 COQC tests/test_eqK.v -is_pred = -fun (n : nat) (Pn : is_nat n) => -match - Pn in (is_nat n0) return (is_nat match n0 with - | 0 => n - | S u => u - end) -with -| is_O => Pn -| is_S _ Pu => Pu -end - : forall n : nat, is_nat n -> is_nat (Nat.pred n) +«elpi.tests.test_API2.G» +Query assignments: + F = «elpi.tests.test_API2.F» + G = «elpi.tests.test_API2.G» + X = «elpi.tests.test_API2.X» +Module G : Sig Definition id : X.T -> X.T. End := (F X) -Arguments is_pred n%nat_scope Pn -is_pred : is_nat2nat Nat.pred - : is_nat2nat Nat.pred -is_predn : is_nat2nat predn - : is_nat2nat predn -is_add : is_nat2nat2nat Nat.add - : is_nat2nat2nat Nat.add Query assignments: - type_1 = «elpi.tests.test_API2.7» -Universe constraints: -UNIVERSES: - -ALGEBRAIC UNIVERSES: - {elpi.tests.test_API2.7} -UNDEFINED UNIVERSES: - elpi.tests.test_API2.7 -WEAK CONSTRAINTS: - + Y = global (indc «is_O») +«elpi.tests.test_API2.H» +Query assignments: + F = «elpi.tests.test_API2.F» + H = «elpi.tests.test_API2.H» + X = «elpi.tests.test_API2.X» +Module H : Sig Definition id : nat -> nat. End := (F X) empty_fields_t : positive -> Type : positive -> Type @@ -7672,14 +7683,6 @@ : forall l : sigma_bool, sigma_bool_fields_t (sigma_bool_tag l) : forall l : sigma_bool, sigma_bool_fields_t (sigma_bool_tag l) -Inductive is_bla : forall H : nat, is_nat H -> bla H -> Type := - is_Bla : forall H : nat, is_nat H -> is_bla 0 is_O (Bla H) - | is_Blu : forall (n : nat) (Pn : is_nat n) (H : bla n), - is_bla n Pn H -> is_bla 1 (is_S 0 is_O) (Blu n H). - -Arguments is_bla _%nat_scope P_ s1 -Arguments is_Bla _%nat_scope P_ -Arguments is_Blu n%nat_scope Pn _ P_ sigma_bool_construct : forall p : positive, sigma_bool_fields_t p -> Datatypes.option sigma_bool @@ -7736,10 +7739,295 @@ forall v : val, val_construct (val_tag v) (val_fields v) = Datatypes.Some v : forall v : val, val_construct (val_tag v) (val_fields v) = Datatypes.Some v +Query assignments: + Y = app + [global (indc «is_S»), app [global (indc «S»), global (indc «O»)], + app [global (indc «is_S»), global (indc «O»), global (indc «is_O»)]] +Skipping derivation map on indt «nat» since the user did not select it +Skipping derivation lens on indt «nat» since the user did not select it +Skipping derivation param1 on indt «nat» since it has been already run +Skipping derivation param2 on indt «nat» since the user did not select it +Skipping derivation tag on indt «nat» since the user did not select it +Skipping derivation eqType_ast on indt «nat» +since the user did not select it +Skipping derivation projK on indt «nat» since it has been already run +Skipping derivation isK on indt «nat» since it has been already run +Skipping derivation eq on indt «nat» since it has been already run +Skipping derivation invert on indt «nat» since the user did not select it +Skipping derivation lens_laws on indt «nat» +since the user did not select it +Skipping derivation param1_congr on indt «nat» +since it has been already run +Skipping derivation param1_inhab on indt «nat» +since it has been already run +Skipping derivation param1_functor on indt «nat» +since it has been already run +Skipping derivation fields on indt «nat» since the user did not select it +Skipping derivation bcongr on indt «nat» since it has been already run +Skipping derivation idx2inv on indt «nat» since the user did not select it +Skipping derivation param1_trivial on indt «nat» +since it has been already run +Skipping derivation induction on indt «nat» since it has been already run +Skipping derivation eqb on indt «nat» since the user did not select it +Skipping derivation eqK on indt «nat» since it has been already run +Skipping derivation eqbcorrect on indt «nat» +since the user did not select it +Skipping derivation eqcorrect on indt «nat» since it has been already run +Skipping derivation eqbOK on indt «nat» since the user did not select it +Skipping derivation eqOK on indt «nat» since it has been already run +is_pred = +fun (n : nat) (Pn : is_nat n) => +match + Pn in (is_nat n0) return (is_nat match n0 with + | 0 => n + | S u => u + end) +with +| is_O => Pn +| is_S _ Pu => Pu +end + : forall n : nat, is_nat n -> is_nat (Nat.pred n) + +Arguments is_pred n%nat_scope Pn +is_pred : is_nat2nat Nat.pred + : is_nat2nat Nat.pred COQC tests/test_eqb.v +is_predn : is_nat2nat predn + : is_nat2nat predn +is_add : is_nat2nat2nat Nat.add + : is_nat2nat2nat Nat.add +Inductive is_bla : forall H : nat, is_nat H -> bla H -> Type := + is_Bla : forall H : nat, is_nat H -> is_bla 0 is_O (Bla H) + | is_Blu : forall (n : nat) (Pn : is_nat n) (H : bla n), + is_bla n Pn H -> is_bla 1 (is_S 0 is_O) (Blu n H). + +Arguments is_bla _%nat_scope P_ s1 +Arguments is_Bla _%nat_scope P_ +Arguments is_Blu n%nat_scope Pn _ P_ Query assignments: GR = const const EXN PRINTING: Not_found T = «elpi.tests.test_API2.T» +Module Type FT = Funsig (P:T) Sig Parameter idT : P.T -> P.T. End +derive.param1_trivial: wrong shape is_t A PA +. It does not look like a unary parametricity translation of an inductive with no indexes. +Vector.t_eq + : (forall A : Type, + (A -> A -> bool) -> forall n : nat, Vector.t A n -> Vector.t A n -> bool) + : forall A : Type, + (A -> A -> bool) -> + forall n : nat, Vector.t A n -> Vector.t A n -> bool +Vector.t_isk_nil : (forall (A : Type) (n : nat), Vector.t A n -> bool) + : forall (A : Type) (n : nat), Vector.t A n -> bool +Vector.t_isk_cons : (forall (A : Type) (n : nat), Vector.t A n -> bool) + : forall (A : Type) (n : nat), Vector.t A n -> bool +Vector.t_map + : (forall A B : Type, + (A -> B) -> forall n : nat, Vector.t A n -> Vector.t B n) + : forall A B : Type, + (A -> B) -> forall n : nat, Vector.t A n -> Vector.t B n +Vector.t_getk_cons1 + : (forall (A : Type) (n : nat), + A -> forall m : nat, Vector.t A m -> Vector.t A n -> A) + : forall (A : Type) (n : nat), + A -> forall m : nat, Vector.t A m -> Vector.t A n -> A +Vector.t_getk_cons2 + : (forall (A : Type) (n : nat), + A -> forall m : nat, Vector.t A m -> Vector.t A n -> nat) + : forall (A : Type) (n : nat), + A -> forall m : nat, Vector.t A m -> Vector.t A n -> nat +Vector.t_getk_cons3 + : (forall (A : Type) (n : nat), + A -> + forall m : nat, Vector.t A m -> Vector.t A n -> {k : nat & Vector.t A k}) + : forall (A : Type) (n : nat), + A -> + forall m : nat, + Vector.t A m -> Vector.t A n -> {k : nat & Vector.t A k} +Vector.is_t + : (forall A : Type, + (A -> Type) -> forall n : nat, is_nat n -> Vector.t A n -> Type) + : forall A : Type, + (A -> Type) -> forall n : nat, is_nat n -> Vector.t A n -> Type +Vector.is_nil + : (forall (A : Type) (PA : A -> Type), + Vector.is_t A PA 0 is_O (Vector.nil A)) + : forall (A : Type) (PA : A -> Type), + Vector.is_t A PA 0 is_O (Vector.nil A) +Vector.is_cons + : (forall (A : Type) (PA : A -> Type) (a : A), + PA a -> + forall (n : nat) (Pn : is_nat n) (H : Vector.t A n), + Vector.is_t A PA n Pn H -> + Vector.is_t A PA (S n) (is_S n Pn) (Vector.cons A a n H)) + : forall (A : Type) (PA : A -> Type) (a : A), + PA a -> + forall (n : nat) (Pn : is_nat n) (H : Vector.t A n), + Vector.is_t A PA n Pn H -> + Vector.is_t A PA (S n) (is_S n Pn) (Vector.cons A a n H) +Vector.is_t_functor + : (forall (A : Type) (PA QA : A -> Type), + (forall x : A, PA x -> QA x) -> + forall (n : nat) (nR : is_nat n) (v : Vector.t A n), + Vector.is_t A PA n nR v -> Vector.is_t A QA n nR v) + : forall (A : Type) (PA QA : A -> Type), + (forall x : A, PA x -> QA x) -> + forall (n : nat) (nR : is_nat n) (v : Vector.t A n), + Vector.is_t A PA n nR v -> Vector.is_t A QA n nR v +Vector.t_induction + : (forall (A : Type) (PA : A -> Type) + (P : forall n : nat, is_nat n -> Vector.t A n -> Type), + P 0 is_O (Vector.nil A) -> + (forall a : A, + PA a -> + forall (m : nat) (mR : is_nat m) (v : Vector.t A m), + P m mR v -> P (S m) (is_S m mR) (Vector.cons A a m v)) -> + forall (n : nat) (nR : is_nat n) (v : Vector.t A n), + Vector.is_t A PA n nR v -> P n nR v) + : forall (A : Type) (PA : A -> Type) + (P : forall n : nat, is_nat n -> Vector.t A n -> Type), + P 0 is_O (Vector.nil A) -> + (forall a : A, + PA a -> + forall (m : nat) (mR : is_nat m) (v : Vector.t A m), + P m mR v -> P (S m) (is_S m mR) (Vector.cons A a m v)) -> + forall (n : nat) (nR : is_nat n) (v : Vector.t A n), + Vector.is_t A PA n nR v -> P n nR v +Vector.t_tag + : (forall (A : Type) (i : nat), Vector.t A i -> BinNums.positive) + : forall (A : Type) (i : nat), Vector.t A i -> BinNums.positive +W_tag : (forall A : Type, W A -> BinNums.positive) + : forall A : Type, W A -> BinNums.positive +«elpi.tests.test_API2.GT» +Query assignments: + F = «elpi.tests.test_API2.FT» + G = «elpi.tests.test_API2.GT» + X = «elpi.tests.test_API2.X» +Module Type GT = Sig Parameter idT : X.T -> X.T. End +eq_axiom_tt : eq_axiom_at unit unit_eq tt + : eq_axiom_at unit unit_eq tt +eq_axiom_Zero : eq_axiom_at peano peano_eq Zero + : eq_axiom_at peano peano_eq Zero +eq_axiom_Succ +: +forall y : peano, +eq_axiom_at peano peano_eq y -> eq_axiom_at peano peano_eq (Succ y) + : forall y : peano, + eq_axiom_at peano peano_eq y -> eq_axiom_at peano peano_eq (Succ y) +eq_axiom_None +: +forall (A : Type) (f : eq_test A), +eq_axiom_at (option A) (option_eq A f) (None A) + : forall (A : Type) (f : eq_test A), + eq_axiom_at (option A) (option_eq A f) (None A) +eq_axiom_Some +: +forall (A : Type) (f : eq_test A) (x : A), +eq_axiom_at A f x -> eq_axiom_at (option A) (option_eq A f) (Some A x) + : forall (A : Type) (f : eq_test A) (x : A), + eq_axiom_at A f x -> eq_axiom_at (option A) (option_eq A f) (Some A x) +eq_axiom_Comma +: +forall (A : Type) (f : eq_test A) (B : Type) (g : eq_test B) (x : A), +eq_axiom_at A f x -> +forall y : B, +eq_axiom_at B g y -> eq_axiom_at (pair A B) (pair_eq A f B g) (Comma A B x y) + : forall (A : Type) (f : eq_test A) (B : Type) (g : eq_test B) (x : A), + eq_axiom_at A f x -> + forall y : B, + eq_axiom_at B g y -> + eq_axiom_at (pair A B) (pair_eq A f B g) (Comma A B x y) +eq_axiom_Nil +: +forall (A : Type) (f : eq_test A), eq_axiom_at (seq A) (seq_eq A f) (Nil A) + : forall (A : Type) (f : eq_test A), + eq_axiom_at (seq A) (seq_eq A f) (Nil A) +eq_axiom_Cons +: +forall (A : Type) (f : eq_test A) (x : A), +eq_axiom_at A f x -> +forall xs : seq A, +eq_axiom_at (seq A) (seq_eq A f) xs -> +eq_axiom_at (seq A) (seq_eq A f) (Cons A x xs) + : forall (A : Type) (f : eq_test A) (x : A), + eq_axiom_at A f x -> + forall xs : seq A, + eq_axiom_at (seq A) (seq_eq A f) xs -> + eq_axiom_at (seq A) (seq_eq A f) (Cons A x xs) +eq_axiom_Leaf +: +forall (A : Type) (f : eq_test A) (a : A), +eq_axiom_at A f a -> eq_axiom_at (rose A) (rose_eq A f) (Leaf A a) + : forall (A : Type) (f : eq_test A) (a : A), + eq_axiom_at A f a -> eq_axiom_at (rose A) (rose_eq A f) (Leaf A a) +eq_axiom_Node +: +forall (A : Type) (f : eq_test A) (l : seq (rose A)), +eq_axiom_at (seq (rose A)) (seq_eq (rose A) (rose_eq A f)) l -> +eq_axiom_at (rose A) (rose_eq A f) (Node A l) + : forall (A : Type) (f : eq_test A) (l : seq (rose A)), + eq_axiom_at (seq (rose A)) (seq_eq (rose A) (rose_eq A f)) l -> + eq_axiom_at (rose A) (rose_eq A f) (Node A l) +eq_axiom_Envelope + : forall (Sender : Type) (f : eq_test Sender) (x : Sender), + eq_axiom_at Sender f x -> + forall x0 : Sender, + eq_axiom_at Sender f x0 -> + forall x1 : zeta Sender, + eq_axiom_on (zeta Sender) (zeta_eq Sender f) (Envelope Sender x x0) x1 +eq_axiom_Redex + : forall (A : Type) (f : eq_test A) (x : A), + eq_axiom_at A f x -> + forall x0 : beta A, eq_axiom_on (beta A) (beta_eq A f) (Redex A x) x0 +eq_axiom_PI + : forall x : PrimInt63.int, + eq_axiom_at PrimInt63.int PrimInt63.eqb x -> + forall x0 : prim_int, eq_axiom_on prim_int prim_int_eq (PI x) x0 +eq_axiom_PF + : forall x : PrimFloat.float, + eq_axiom_at PrimFloat.float PrimFloat.eqb x -> + forall x0 : prim_float, eq_axiom_on prim_float prim_float_eq (PF x) x0 +eq_axiom_Build_fo_record +: +forall x : peano, +eq_axiom_at peano peano_eq x -> +forall y : unit, +eq_axiom_at unit unit_eq y -> +eq_axiom_at fo_record fo_record_eq {| f1 := x; f2 := y |} + : forall x : peano, + eq_axiom_at peano peano_eq x -> + forall y : unit, + eq_axiom_at unit unit_eq y -> + eq_axiom_at fo_record fo_record_eq {| f1 := x; f2 := y |} +eq_axiom_Build_pa_record +: +forall (A : Type) (f : eq_test A) (x : peano), +eq_axiom_at peano peano_eq x -> +forall y : A, +eq_axiom_at A f y -> +eq_axiom_at (pa_record A) (pa_record_eq A f) {| f3 := x; f4 := y |} + : forall (A : Type) (f : eq_test A) (x : peano), + eq_axiom_at peano peano_eq x -> + forall y : A, + eq_axiom_at A f y -> + eq_axiom_at (pa_record A) (pa_record_eq A f) {| f3 := x; f4 := y |} +eq_axiom_Build_pr_record +: +forall (A : Type) (f : eq_test A) (x : peano), +eq_axiom_at peano peano_eq x -> +forall y : A, +eq_axiom_at A f y -> +eq_axiom_at (pr_record A) (pr_record_eq A f) {| pf3 := x; pf4 := y |} + : forall (A : Type) (f : eq_test A) (x : peano), + eq_axiom_at peano peano_eq x -> + forall y : A, + eq_axiom_at A f y -> + eq_axiom_at (pr_record A) (pr_record_eq A f) {| pf3 := x; pf4 := y |} +eq_axiom_E1 : eq_axiom_at enum enum_eq E1 + : eq_axiom_at enum enum_eq E1 +eq_axiom_E2 : eq_axiom_at enum enum_eq E2 + : eq_axiom_at enum enum_eq E2 +eq_axiom_E3 : eq_axiom_at enum enum_eq E3 + : eq_axiom_at enum enum_eq E3 Query assignments: PDb = [tc-instance (const «reali_is_fin_length») 0, tc-instance (const «reali_is_vec_length») 0, @@ -7887,153 +8175,89 @@ Spilled_1 = indt «reali_db» File "./tests/test_param1.v", line 158, characters 0-30: Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] -eq_axiom_tt : eq_axiom_at unit unit_eq tt - : eq_axiom_at unit unit_eq tt -eq_axiom_Zero : eq_axiom_at peano peano_eq Zero - : eq_axiom_at peano peano_eq Zero -eq_axiom_Succ -: -forall y : peano, -eq_axiom_at peano peano_eq y -> eq_axiom_at peano peano_eq (Succ y) - : forall y : peano, - eq_axiom_at peano peano_eq y -> eq_axiom_at peano peano_eq (Succ y) -eq_axiom_None -: -forall (A : Type) (f : eq_test A), -eq_axiom_at (option A) (option_eq A f) (None A) - : forall (A : Type) (f : eq_test A), - eq_axiom_at (option A) (option_eq A f) (None A) -eq_axiom_Some -: -forall (A : Type) (f : eq_test A) (x : A), -eq_axiom_at A f x -> eq_axiom_at (option A) (option_eq A f) (Some A x) - : forall (A : Type) (f : eq_test A) (x : A), - eq_axiom_at A f x -> eq_axiom_at (option A) (option_eq A f) (Some A x) -eq_axiom_Comma -: -forall (A : Type) (f : eq_test A) (B : Type) (g : eq_test B) (x : A), -eq_axiom_at A f x -> -forall y : B, -eq_axiom_at B g y -> eq_axiom_at (pair A B) (pair_eq A f B g) (Comma A B x y) - : forall (A : Type) (f : eq_test A) (B : Type) (g : eq_test B) (x : A), - eq_axiom_at A f x -> - forall y : B, - eq_axiom_at B g y -> - eq_axiom_at (pair A B) (pair_eq A f B g) (Comma A B x y) -eq_axiom_Nil -: -forall (A : Type) (f : eq_test A), eq_axiom_at (seq A) (seq_eq A f) (Nil A) - : forall (A : Type) (f : eq_test A), - eq_axiom_at (seq A) (seq_eq A f) (Nil A) -eq_axiom_Cons -: -forall (A : Type) (f : eq_test A) (x : A), -eq_axiom_at A f x -> -forall xs : seq A, -eq_axiom_at (seq A) (seq_eq A f) xs -> -eq_axiom_at (seq A) (seq_eq A f) (Cons A x xs) - : forall (A : Type) (f : eq_test A) (x : A), - eq_axiom_at A f x -> - forall xs : seq A, - eq_axiom_at (seq A) (seq_eq A f) xs -> - eq_axiom_at (seq A) (seq_eq A f) (Cons A x xs) -eq_axiom_Leaf -: -forall (A : Type) (f : eq_test A) (a : A), -eq_axiom_at A f a -> eq_axiom_at (rose A) (rose_eq A f) (Leaf A a) - : forall (A : Type) (f : eq_test A) (a : A), - eq_axiom_at A f a -> eq_axiom_at (rose A) (rose_eq A f) (Leaf A a) -eq_axiom_Node -: -forall (A : Type) (f : eq_test A) (l : seq (rose A)), -eq_axiom_at (seq (rose A)) (seq_eq (rose A) (rose_eq A f)) l -> -eq_axiom_at (rose A) (rose_eq A f) (Node A l) - : forall (A : Type) (f : eq_test A) (l : seq (rose A)), - eq_axiom_at (seq (rose A)) (seq_eq (rose A) (rose_eq A f)) l -> - eq_axiom_at (rose A) (rose_eq A f) (Node A l) -eq_axiom_Envelope - : forall (Sender : Type) (f : eq_test Sender) (x : Sender), - eq_axiom_at Sender f x -> - forall x0 : Sender, - eq_axiom_at Sender f x0 -> - forall x1 : zeta Sender, - eq_axiom_on (zeta Sender) (zeta_eq Sender f) (Envelope Sender x x0) x1 -eq_axiom_Redex - : forall (A : Type) (f : eq_test A) (x : A), - eq_axiom_at A f x -> - forall x0 : beta A, eq_axiom_on (beta A) (beta_eq A f) (Redex A x) x0 -eq_axiom_PI - : forall x : PrimInt63.int, - eq_axiom_at PrimInt63.int PrimInt63.eqb x -> - forall x0 : prim_int, eq_axiom_on prim_int prim_int_eq (PI x) x0 -eq_axiom_PF - : forall x : PrimFloat.float, - eq_axiom_at PrimFloat.float PrimFloat.eqb x -> - forall x0 : prim_float, eq_axiom_on prim_float prim_float_eq (PF x) x0 -eq_axiom_Build_fo_record -: -forall x : peano, -eq_axiom_at peano peano_eq x -> -forall y : unit, -eq_axiom_at unit unit_eq y -> -eq_axiom_at fo_record fo_record_eq {| f1 := x; f2 := y |} - : forall x : peano, - eq_axiom_at peano peano_eq x -> - forall y : unit, - eq_axiom_at unit unit_eq y -> - eq_axiom_at fo_record fo_record_eq {| f1 := x; f2 := y |} -eq_axiom_Build_pa_record -: -forall (A : Type) (f : eq_test A) (x : peano), -eq_axiom_at peano peano_eq x -> -forall y : A, -eq_axiom_at A f y -> -eq_axiom_at (pa_record A) (pa_record_eq A f) {| f3 := x; f4 := y |} - : forall (A : Type) (f : eq_test A) (x : peano), - eq_axiom_at peano peano_eq x -> - forall y : A, - eq_axiom_at A f y -> - eq_axiom_at (pa_record A) (pa_record_eq A f) {| f3 := x; f4 := y |} -eq_axiom_Build_pr_record -: -forall (A : Type) (f : eq_test A) (x : peano), -eq_axiom_at peano peano_eq x -> -forall y : A, -eq_axiom_at A f y -> -eq_axiom_at (pr_record A) (pr_record_eq A f) {| pf3 := x; pf4 := y |} - : forall (A : Type) (f : eq_test A) (x : peano), - eq_axiom_at peano peano_eq x -> - forall y : A, - eq_axiom_at A f y -> - eq_axiom_at (pr_record A) (pr_record_eq A f) {| pf3 := x; pf4 := y |} -eq_axiom_E1 : eq_axiom_at enum enum_eq E1 - : eq_axiom_at enum enum_eq E1 -eq_axiom_E2 : eq_axiom_at enum enum_eq E2 - : eq_axiom_at enum enum_eq E2 -eq_axiom_E3 : eq_axiom_at enum enum_eq E3 - : eq_axiom_at enum enum_eq E3 -«elpi.tests.test_API2.G» +XXX.rtree_tag : (forall A : Type, rtree A -> BinNums.positive) + : forall A : Type, rtree A -> BinNums.positive +XXX.rtree_fields_t : Type -> BinNums.positive -> Type + : Type -> BinNums.positive -> Type +XXX.rtree_fields + : (forall (A : Type) (l : rtree A), + XXX.rtree_fields_t A (XXX.rtree_tag A l)) + : forall (A : Type) (l : rtree A), + XXX.rtree_fields_t A (XXX.rtree_tag A l) +XXX.rtree_construct + : (forall (A : Type) (p : BinNums.positive), + XXX.rtree_fields_t A p -> option (rtree A)) + : forall (A : Type) (p : BinNums.positive), + XXX.rtree_fields_t A p -> option (rtree A) +XXX.rtree_constructP + : (forall (A : Type) (l : rtree A), + XXX.rtree_construct A (XXX.rtree_tag A l) (XXX.rtree_fields A l) = + Some l) + : forall (A : Type) (l : rtree A), + XXX.rtree_construct A (XXX.rtree_tag A l) (XXX.rtree_fields A l) = + Some l +XXX.rtree_eqb + : (forall A : Type, (A -> A -> bool) -> rtree A -> rtree A -> bool) + : forall A : Type, (A -> A -> bool) -> rtree A -> rtree A -> bool +«elpi.tests.test_API2.HT» Query assignments: - F = «elpi.tests.test_API2.F» - G = «elpi.tests.test_API2.G» + F = «elpi.tests.test_API2.FT» + H = «elpi.tests.test_API2.HT» X = «elpi.tests.test_API2.X» -Module G : Sig Definition id : X.T -> X.T. End := (F X) - -«elpi.tests.test_API2.H» +Module Type HT = Sig Parameter idT : nat -> nat. End +derive.param1_trivial: wrong shape is_triv +. It does not look like a unary parametricity translation of an inductive with no indexes. +triv.induction + : (forall P : forall H : Coverage.unit, is_unit H -> triv H -> Prop, + (forall (t : Coverage.unit) (Pt : is_unit t), P t Pt (one t)) -> + (forall (x : Coverage.unit) (Px : is_unit x), P x Px (more x)) -> + forall (u : Coverage.unit) (p : is_unit u) (s : triv u), + triv.is_triv u p s -> P u p s) + : forall P : forall H : Coverage.unit, is_unit H -> triv H -> Prop, + (forall (t : Coverage.unit) (Pt : is_unit t), P t Pt (one t)) -> + (forall (x : Coverage.unit) (Px : is_unit x), P x Px (more x)) -> + forall (u : Coverage.unit) (p : is_unit u) (s : triv u), + triv.is_triv u p s -> P u p s +Debug: Cannot enforce elpi.apps.derive.tests.test_derive.4294 <= Set Query assignments: - F = «elpi.tests.test_API2.F» - H = «elpi.tests.test_API2.H» - X = «elpi.tests.test_API2.X» -Module H : Sig Definition id : nat -> nat. End := (F X) + L = [«elpi.tests.test_API2.8», «elpi.tests.test_API2.9»] + S = {{ elpi.tests.test_API2.8; elpi.tests.test_API2.9; }} + U = «elpi.tests.test_API2.8» + UV = «elpi.tests.test_API2.8» + V = «elpi.tests.test_API2.9» + VV = «elpi.tests.test_API2.9» +Universe constraints: +UNIVERSES: + {elpi.tests.test_API2.9 elpi.tests.test_API2.8} |= +ALGEBRAIC UNIVERSES: + {elpi.tests.test_API2.9 elpi.tests.test_API2.8} +UNDEFINED UNIVERSES: + elpi.tests.test_API2.9 + elpi.tests.test_API2.8 +WEAK CONSTRAINTS: + -File "./tests/test_param1.v", line 176, characters 0-66: -Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] -COQC tests/test_param1_functor.v -COQC tests/test_param1_congr.v -Query assignments: - GR = const const EXN PRINTING: Not_found - T = «elpi.tests.test_API2.T» -Module Type FT = Funsig (P:T) Sig Parameter idT : P.T -> P.T. End +COQC tests/test_require_bad_order.v +derive.param1_trivial: wrong shape is_Pred +. It does not look like a unary parametricity translation of an inductive with no indexes. +Pred.Pred_to_Predinv : (forall T : RoseTree, Pred T -> Pred.Predinv T) + : forall T : RoseTree, Pred T -> Pred.Predinv T +File "./tests/test_require_bad_order.v", line 2, characters 0-28: +Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] +wimpls.wimpls : forall {A : Type}, rtree A -> Type + +wimpls.wimpls is not universe polymorphic +Arguments wimpls.wimpls {A}%type_scope {rtree0} +Expands to: Inductive elpi.apps.derive.tests.test_derive.wimpls.wimpls +wimpls.Kwi : forall {A : Type} {rtree0 : rtree A} (x : A), x = x -> wimpls + +wimpls.Kwi is not universe polymorphic +Arguments wimpls.Kwi {A}%type_scope {rtree0} x _ +Expands to: Constructor elpi.apps.derive.tests.test_derive.wimpls.Kwi +Kwi 3 eq_refl + : wimpls +where +?rtree0 : [ |- rtree nat] empty_eqb : eq_test2 empty empty : eq_test2 empty empty unit_eqb : eq_test2 unit unit @@ -8080,158 +8304,10 @@ : eq_test2 val val alias_eqb : eq_test2 alias alias : eq_test2 alias alias -«elpi.tests.test_API2.GT» -Query assignments: - F = «elpi.tests.test_API2.FT» - G = «elpi.tests.test_API2.GT» - X = «elpi.tests.test_API2.X» -Module Type GT = Sig Parameter idT : X.T -> X.T. End -«elpi.tests.test_API2.HT» -Query assignments: - F = «elpi.tests.test_API2.FT» - H = «elpi.tests.test_API2.HT» - X = «elpi.tests.test_API2.X» -Module Type HT = Sig Parameter idT : nat -> nat. End -Skipping derivation map on indt «nat» since the user did not select it -Skipping derivation lens on indt «nat» since the user did not select it -Skipping derivation param1 on indt «nat» since it has been already run -Skipping derivation param2 on indt «nat» since the user did not select it -Skipping derivation tag on indt «nat» since the user did not select it -Skipping derivation eqType_ast on indt «nat» -since the user did not select it -Skipping derivation projK on indt «nat» since it has been already run -Skipping derivation isK on indt «nat» since it has been already run -Skipping derivation eq on indt «nat» since it has been already run -Skipping derivation invert on indt «nat» since the user did not select it -Skipping derivation lens_laws on indt «nat» -since the user did not select it -Skipping derivation param1_congr on indt «nat» -since it has been already run -Skipping derivation param1_inhab on indt «nat» -since it has been already run -Skipping derivation param1_functor on indt «nat» -since it has been already run -Skipping derivation fields on indt «nat» since the user did not select it -Skipping derivation bcongr on indt «nat» since it has been already run -Skipping derivation idx2inv on indt «nat» since the user did not select it -Skipping derivation param1_trivial on indt «nat» -since it has been already run -Skipping derivation induction on indt «nat» since it has been already run -Skipping derivation eqb on indt «nat» since the user did not select it -Skipping derivation eqK on indt «nat» since it has been already run -Skipping derivation eqbcorrect on indt «nat» -since the user did not select it -Skipping derivation eqcorrect on indt «nat» since it has been already run -Skipping derivation eqbOK on indt «nat» since the user did not select it -Skipping derivation eqOK on indt «nat» since it has been already run -derive.param1_trivial: wrong shape is_t A PA -. It does not look like a unary parametricity translation of an inductive with no indexes. -Vector.t_eq - : (forall A : Type, - (A -> A -> bool) -> forall n : nat, Vector.t A n -> Vector.t A n -> bool) - : forall A : Type, - (A -> A -> bool) -> - forall n : nat, Vector.t A n -> Vector.t A n -> bool -Vector.t_isk_nil : (forall (A : Type) (n : nat), Vector.t A n -> bool) - : forall (A : Type) (n : nat), Vector.t A n -> bool -Vector.t_isk_cons : (forall (A : Type) (n : nat), Vector.t A n -> bool) - : forall (A : Type) (n : nat), Vector.t A n -> bool -Vector.t_map - : (forall A B : Type, - (A -> B) -> forall n : nat, Vector.t A n -> Vector.t B n) - : forall A B : Type, - (A -> B) -> forall n : nat, Vector.t A n -> Vector.t B n -Vector.t_getk_cons1 - : (forall (A : Type) (n : nat), - A -> forall m : nat, Vector.t A m -> Vector.t A n -> A) - : forall (A : Type) (n : nat), - A -> forall m : nat, Vector.t A m -> Vector.t A n -> A -Vector.t_getk_cons2 - : (forall (A : Type) (n : nat), - A -> forall m : nat, Vector.t A m -> Vector.t A n -> nat) - : forall (A : Type) (n : nat), - A -> forall m : nat, Vector.t A m -> Vector.t A n -> nat -Vector.t_getk_cons3 - : (forall (A : Type) (n : nat), - A -> - forall m : nat, Vector.t A m -> Vector.t A n -> {k : nat & Vector.t A k}) - : forall (A : Type) (n : nat), - A -> - forall m : nat, - Vector.t A m -> Vector.t A n -> {k : nat & Vector.t A k} -Vector.is_t - : (forall A : Type, - (A -> Type) -> forall n : nat, is_nat n -> Vector.t A n -> Type) - : forall A : Type, - (A -> Type) -> forall n : nat, is_nat n -> Vector.t A n -> Type -Vector.is_nil - : (forall (A : Type) (PA : A -> Type), - Vector.is_t A PA 0 is_O (Vector.nil A)) - : forall (A : Type) (PA : A -> Type), - Vector.is_t A PA 0 is_O (Vector.nil A) -Vector.is_cons - : (forall (A : Type) (PA : A -> Type) (a : A), - PA a -> - forall (n : nat) (Pn : is_nat n) (H : Vector.t A n), - Vector.is_t A PA n Pn H -> - Vector.is_t A PA (S n) (is_S n Pn) (Vector.cons A a n H)) - : forall (A : Type) (PA : A -> Type) (a : A), - PA a -> - forall (n : nat) (Pn : is_nat n) (H : Vector.t A n), - Vector.is_t A PA n Pn H -> - Vector.is_t A PA (S n) (is_S n Pn) (Vector.cons A a n H) -Vector.is_t_functor - : (forall (A : Type) (PA QA : A -> Type), - (forall x : A, PA x -> QA x) -> - forall (n : nat) (nR : is_nat n) (v : Vector.t A n), - Vector.is_t A PA n nR v -> Vector.is_t A QA n nR v) - : forall (A : Type) (PA QA : A -> Type), - (forall x : A, PA x -> QA x) -> - forall (n : nat) (nR : is_nat n) (v : Vector.t A n), - Vector.is_t A PA n nR v -> Vector.is_t A QA n nR v -Vector.t_induction - : (forall (A : Type) (PA : A -> Type) - (P : forall n : nat, is_nat n -> Vector.t A n -> Type), - P 0 is_O (Vector.nil A) -> - (forall a : A, - PA a -> - forall (m : nat) (mR : is_nat m) (v : Vector.t A m), - P m mR v -> P (S m) (is_S m mR) (Vector.cons A a m v)) -> - forall (n : nat) (nR : is_nat n) (v : Vector.t A n), - Vector.is_t A PA n nR v -> P n nR v) - : forall (A : Type) (PA : A -> Type) - (P : forall n : nat, is_nat n -> Vector.t A n -> Type), - P 0 is_O (Vector.nil A) -> - (forall a : A, - PA a -> - forall (m : nat) (mR : is_nat m) (v : Vector.t A m), - P m mR v -> P (S m) (is_S m mR) (Vector.cons A a m v)) -> - forall (n : nat) (nR : is_nat n) (v : Vector.t A n), - Vector.is_t A PA n nR v -> P n nR v -Vector.t_tag - : (forall (A : Type) (i : nat), Vector.t A i -> BinNums.positive) - : forall (A : Type) (i : nat), Vector.t A i -> BinNums.positive -Query assignments: - L = [«elpi.tests.test_API2.8», «elpi.tests.test_API2.9»] - S = {{ elpi.tests.test_API2.8; elpi.tests.test_API2.9; }} - U = «elpi.tests.test_API2.8» - UV = «elpi.tests.test_API2.8» - V = «elpi.tests.test_API2.9» - VV = «elpi.tests.test_API2.9» -Universe constraints: -UNIVERSES: - {elpi.tests.test_API2.9 elpi.tests.test_API2.8} |= -ALGEBRAIC UNIVERSES: - {elpi.tests.test_API2.9 elpi.tests.test_API2.8} -UNDEFINED UNIVERSES: - elpi.tests.test_API2.9 - elpi.tests.test_API2.8 -WEAK CONSTRAINTS: - - -COQC tests/test_require_bad_order.v -W_tag : (forall A : Type, W A -> BinNums.positive) - : forall A : Type, W A -> BinNums.positive +File "./tests/test_param1.v", line 176, characters 0-66: +Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints] +COQC tests/test_param1_functor.v +COQC tests/test_param1_congr.v congr_is_tt : is_tt = is_tt : is_tt = is_tt congr_is_Zero : is_Zero = is_Zero @@ -8360,6 +8436,7 @@ is_Build_pr_record A pr n p1 b q1 = is_Build_pr_record A pr n p2 b q2 congr_is_E1 : is_E1 = is_E1 : is_E1 = is_E1 +COQC tests/test_param1_trivial.v is_empty_functor : func is_empty : func is_empty is_unit_functor : func is_unit @@ -8412,66 +8489,7 @@ : forall (n : peano) (pn : is_peano n), func (is_ord2 n pn) is_val_functor : func is_val : func is_val -COQC tests/test_param1_trivial.v COQC tests/test_induction.v -File "./tests/test_require_bad_order.v", line 2, characters 0-28: -Warning: Option Foo Bar is deprecated [deprecated-option,deprecated] -XXX.rtree_tag : (forall A : Type, rtree A -> BinNums.positive) - : forall A : Type, rtree A -> BinNums.positive -XXX.rtree_fields_t : Type -> BinNums.positive -> Type - : Type -> BinNums.positive -> Type -XXX.rtree_fields - : (forall (A : Type) (l : rtree A), - XXX.rtree_fields_t A (XXX.rtree_tag A l)) - : forall (A : Type) (l : rtree A), - XXX.rtree_fields_t A (XXX.rtree_tag A l) -XXX.rtree_construct - : (forall (A : Type) (p : BinNums.positive), - XXX.rtree_fields_t A p -> option (rtree A)) - : forall (A : Type) (p : BinNums.positive), - XXX.rtree_fields_t A p -> option (rtree A) -XXX.rtree_constructP - : (forall (A : Type) (l : rtree A), - XXX.rtree_construct A (XXX.rtree_tag A l) (XXX.rtree_fields A l) = - Some l) - : forall (A : Type) (l : rtree A), - XXX.rtree_construct A (XXX.rtree_tag A l) (XXX.rtree_fields A l) = - Some l -XXX.rtree_eqb - : (forall A : Type, (A -> A -> bool) -> rtree A -> rtree A -> bool) - : forall A : Type, (A -> A -> bool) -> rtree A -> rtree A -> bool -derive.param1_trivial: wrong shape is_triv -. It does not look like a unary parametricity translation of an inductive with no indexes. -triv.induction - : (forall P : forall H : Coverage.unit, is_unit H -> triv H -> Prop, - (forall (t : Coverage.unit) (Pt : is_unit t), P t Pt (one t)) -> - (forall (x : Coverage.unit) (Px : is_unit x), P x Px (more x)) -> - forall (u : Coverage.unit) (p : is_unit u) (s : triv u), - triv.is_triv u p s -> P u p s) - : forall P : forall H : Coverage.unit, is_unit H -> triv H -> Prop, - (forall (t : Coverage.unit) (Pt : is_unit t), P t Pt (one t)) -> - (forall (x : Coverage.unit) (Px : is_unit x), P x Px (more x)) -> - forall (u : Coverage.unit) (p : is_unit u) (s : triv u), - triv.is_triv u p s -> P u p s -Debug: Cannot enforce elpi.apps.derive.tests.test_derive.4294 <= Set -derive.param1_trivial: wrong shape is_Pred -. It does not look like a unary parametricity translation of an inductive with no indexes. -Pred.Pred_to_Predinv : (forall T : RoseTree, Pred T -> Pred.Predinv T) - : forall T : RoseTree, Pred T -> Pred.Predinv T -wimpls.wimpls : forall {A : Type}, rtree A -> Type - -wimpls.wimpls is not universe polymorphic -Arguments wimpls.wimpls {A}%type_scope {rtree0} -Expands to: Inductive elpi.apps.derive.tests.test_derive.wimpls.wimpls -wimpls.Kwi : forall {A : Type} {rtree0 : rtree A} (x : A), x = x -> wimpls - -wimpls.Kwi is not universe polymorphic -Arguments wimpls.Kwi {A}%type_scope {rtree0} x _ -Expands to: Constructor elpi.apps.derive.tests.test_derive.wimpls.Kwi -Kwi 3 eq_refl - : wimpls -where -?rtree0 : [ |- rtree nat] Inductive elpi.apps.derive.tests.test_param1.Coverage.is_unit Inductive elpi.apps.derive.tests.test_param1.OtherTests.is_unit (shorter name to refer to it in current context is OtherTests.is_unit) @@ -9368,7 +9386,8 @@ : full val is_val COQC tests/test_eqOK.v COQC tests/test_eqbcorrect.v -Finished transaction in 46.324 secs (46.321u,0.s) (successful) +Finished transaction in 56.895 secs (46.024u,0.073s) (successful) +Finished transaction in 1.037 secs (1.036u,0.s) (successful) empty_eq_OK : ok empty empty_eq : ok empty empty_eq unit_eq_OK : ok unit unit_eq @@ -9429,7 +9448,6 @@ ok A f -> ok (pr_record A) (pr_record_eq A f) enum_eq_OK : ok enum enum_eq : ok enum enum_eq -Finished transaction in 0.843 secs (0.843u,0.s) (successful) dlist_eqOK : forall (A : Type) (f : A -> A -> bool), ok A f -> ok (dlist A) (dlist_eq A f) @@ -9488,15 +9506,15 @@ COQC tests/test_discriminate.v COQC tests/test_injection.v COQC tests/test_case.v -trying i = i d : nat -trying elpi_ctx_entry_2_ = elpi_ctx_entry_2_ COQC tests/test_generalize.v +trying i = i +trying elpi_ctx_entry_2_ = elpi_ctx_entry_2_ COQC tests/test_cycle.v -COQC examples/usage_eltac.v trying elpi_ctx_entry_1_ = elpi_ctx_entry_1_ /\ p0 = p0 trying elpi_ctx_entry_1_ = elpi_ctx_entry_1_ /\ p0 = p0 +COQC examples/usage_eltac.v make[2]: Leaving directory '/build/coq-elpi-1.16.0/apps/eltac' make[2]: Entering directory '/build/coq-elpi-1.16.0/apps/NES' Using coq found in /usr/bin/, from COQBIN or PATH @@ -9513,23 +9531,23 @@ : nat Foo.x2 = 4 : nat +eq_refl : Foo.x = 5 + : Foo.x = 5 This.Is.A.Long.Namespace.stuff = 1 : nat = 1 : nat -eq_refl : Foo.x = 5 - : Foo.x = 5 This.Is.A.Long.Namespace.stuff = 2 : nat = 1 : nat -stuff = 2 - : nat A.B.c : nat A.B.c is not universe polymorphic A.B.c is transparent Expands to: Constant elpi.apps.NES.tests.test_NES.A_aux_4.A.B.c +stuff = 2 + : nat default nat_def : nat : nat A1.B1.d : nat @@ -9886,12 +9904,14 @@ dpkg-buildpackage: info: binary-only upload (no source included) dpkg-genchanges: info: not including original source code in upload I: copying local configuration +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/31020/tmp/hooks/B01_cleanup finished I: unmounting dev/ptmx filesystem I: unmounting dev/pts filesystem I: unmounting dev/shm filesystem I: unmounting proc filesystem I: unmounting sys filesystem I: cleaning the build env -I: removing directory /srv/workspace/pbuilder/29232 and its subdirectories -I: Current time: Tue Apr 11 14:25:58 -12 2023 -I: pbuilder-time-stamp: 1681266358 +I: removing directory /srv/workspace/pbuilder/31020 and its subdirectories +I: Current time: Tue May 14 22:56:03 +14 2024 +I: pbuilder-time-stamp: 1715676963