Merge pull request #293 from LPCIC/coq-v8.14

Coq v8.14

.github/workflows/doc.yml

@@ -28,6 +28,7 @@ jobs:
       run: |
         export OPAMYES=true
         opam repo add coq https://coq.inria.fr/opam/released
+        opam repo add coq-dev https://coq.inria.fr/opam/core-dev
         opam update
         opam install coq-serapi .
         sudo apt-get update

.github/workflows/main.yml

@@ -16,7 +16,7 @@ jobs:
     strategy:
       matrix:
         coq_version:
-          - '8.13'
+          - '8.14'
         ocaml_version:
           - '4.07-flambda'
           - '4.11-flambda'

Changelog.md

@@ -1,5 +1,15 @@
 # Changelog
 
+## [1.11.2] - 24-09-2021
+
+Requires Elpi 1.13.6 and Coq 8.14.
+
+### API
+- Change `coq.bind-ind-arity` preserves `let`
+- New `coq.bind-ind-arity-no-let` to reduce `let`, used in `coq.build-match`
+- Fix `coq.build-match` putting `let` bindings in `match` return type
+- Change `coq.map-under-fun` preserves `let`
+
 ## [1.11.1] - 24-09-2021
 
 Requires Elpi 1.13.6 and Coq 8.13.

Makefile.coq.local

@@ -1,4 +1,4 @@
-CAMLPKGS+= -package elpi
+CAMLPKGS+= -package elpi,stdlib-shims
 CAMLFLAGS+= -bin-annot -g
 
 src/coq_elpi_builtins_HOAS.ml: elpi/coq-HOAS.elpi Makefile.coq.local

apps/derive/tests/test_projK.v

@@ -47,7 +47,9 @@ Check projVCons3 : forall A i, A -> forall j, vect A j -> vect A i -> { w & vect
 Check projbox1 : forall T, T -> dyn -> Type.
 Check projbox2 : forall T, T -> dyn -> { T : Type & T }.
 Check projEnvelope1 : forall A, A -> A -> zeta A -> A.
+Check eq_refl 0 : projEnvelope1 nat 1 1 (Envelope nat 0 1) = 0.
 Check projEnvelope2 : forall A, A -> A -> zeta A -> A.
+Check eq_refl 0 : projEnvelope2 nat 1 1 (Envelope nat 1 0) = 0.
 Check projRedex1 : forall A, A -> beta A -> A.
 Check projWhy1 : forall n : peano, match n with 
                     | Zero => peano

apps/derive/theories/derive/eq.v

@@ -6,7 +6,7 @@
 From Coq Require Export Bool.
 From elpi Require Export elpi.
 
-Register Coq.Numbers.Cyclic.Int63.Int63.eqb as elpi.derive.eq_unit63.
+Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
 Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64.
 
 Elpi Db derive.eq.db lp:{{

apps/derive/theories/derive/eqcorrect.v

@@ -6,11 +6,11 @@
 From elpi Require Export elpi.
 From elpi.apps Require Export  derive.eq derive.map derive.induction derive.eqK.
 
-From Coq Require Import ssreflect.
+From Coq Require Import ssreflect Int63.
 
-Lemma uint63_eq_correct i : is_uint63 i -> eq_axiom_at Int63.int Int63.eqb i.
+Lemma uint63_eq_correct i : is_uint63 i -> eq_axiom_at PrimInt63.int PrimInt63.eqb i.
 Proof.
-move=> _ j; case: (Int63.eqb_spec i j); case: Int63.eqb => [-> // _|_ abs];
+move=> _ j; case: (Int63.eqb_spec i j); case: PrimInt63.eqb => [-> // _|_ abs];
   [ by constructor | by constructor=> /abs ].
 Qed.
 Register uint63_eq_correct as elpi.derive.uint63_eq_correct.

apps/derive/theories/derive/param1.v

@@ -36,7 +36,7 @@ Class reali {X : Type} {XR : X -> Type} (x : X) (xR : XR x) := Reali {}.
 
 Register store_reali as param1.store_reali.
 
-Inductive is_uint63 : Int63.int -> Type := uint63 (i : Int63.int) : is_uint63 i.
+Inductive is_uint63 : PrimInt63.int -> Type := uint63 (i : PrimInt63.int) : is_uint63 i.
 Register is_uint63 as elpi.derive.is_uint63.
 
 Inductive is_float64 : PrimFloat.float -> Type := float64 (f : PrimFloat.float ) : is_float64 f.

apps/derive/theories/derive/param1_trivial.v

@@ -7,7 +7,7 @@
 From elpi Require Export elpi.
 From elpi.apps Require Export derive.param1 derive.param1_congr derive.param1_inhab.
 
-Definition is_uint63_trivial : trivial Int63.int is_uint63 :=
+Definition is_uint63_trivial : trivial PrimInt63.int is_uint63 :=
   fun x => contracts _ is_uint63 x (is_uint63_witness x)
     (fun y => match y with uint63 i => eq_refl end).
 Register is_uint63_trivial as elpi.derive.is_uint63_trivial.

coq-builtin.elpi

@@ -105,7 +105,7 @@ type primitive primitive-value -> term.
 %      fun `n` (indt "nat) n\
 %       fun `i` (app[indt "i", indt "bool", a n) i\ ..
 %   Such spine of fun cannot be omitted; else elpi cannot read the term back.
-%   See also coq.bind-ind-arity in coq-lib.elpi, that builds such spine for you,
+%   See also coq.bind-ind-arity-no-let in coq-lib.elpi, that builds such spine for you,
 %   or the higher level api coq.build-match (same file) that also takes
 %   care of breanches.
 % - Branches is a list of terms, the order is the canonical one (the order

coq-elpi.opam

@@ -15,8 +15,8 @@ install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "stdlib-shims"
   "elpi" {>= "1.13.6" & < "1.14.0~"}
-  "coq" {>= "8.13" & < "8.14~" }
-  ]
+  "coq" {>= "8.14" & < "8.15~" }
+]
 tags: [ "logpath:elpi" ]
 synopsis: "Elpi extension language for Coq"
 description: """

elpi/coq-HOAS.elpi

@@ -90,7 +90,7 @@ type primitive primitive-value -> term.
 %      fun `n` (indt "nat) n\
 %       fun `i` (app[indt "i", indt "bool", a n) i\ ..
 %   Such spine of fun cannot be omitted; else elpi cannot read the term back.
-%   See also coq.bind-ind-arity in coq-lib.elpi, that builds such spine for you,
+%   See also coq.bind-ind-arity-no-let in coq-lib.elpi, that builds such spine for you,
 %   or the higher level api coq.build-match (same file) that also takes
 %   care of breanches.
 % - Branches is a list of terms, the order is the canonical one (the order

elpi/coq-lib.elpi

@@ -424,8 +424,8 @@ pred coq.map-under-fun i:term,
 coq.map-under-fun T F R :- map-under-fun.aux T [] [] F R.
 map-under-fun.aux (fun N T B) AccT AccTy F (fun N T R) :- !,
   @pi-decl N T x\ map-under-fun.aux (B x) [x|AccT] [T|AccTy] F (R x).
-map-under-fun.aux (let _ _ X B) AccT AccTy F R :- !,
-  map-under-fun.aux (B X) AccT AccTy F R.
+map-under-fun.aux (let N T X B) AccT AccTy F (let N T X R) :- !,
+  @pi-def N T X x\ map-under-fun.aux (B x) AccT AccTy F (R x).
 map-under-fun.aux End AccT AccTy F R :- F End {rev AccT} {rev AccTy} R.
 
 pred coq.iter-under-fun i:term,
@@ -455,10 +455,11 @@ coq.build-match T Tty RtyF BranchF (match T Rty Bs) :-
   coq.mk-app (global (indt GR)) LArgs IndtLArgs,
   % Rty
   coq.subst-prod LArgs Arity ArityArgs,
-  coq.bind-ind-arity IndtLArgs ArityArgs RtyF Rty,
+  coq.bind-ind-arity-no-let IndtLArgs ArityArgs RtyF Rty,
   % Bs
   map Kt (coq.subst-prod LArgs) KtArgs,
-  map KtArgs coq.prod->fun KtArgsLam,
+  map KtArgs hd-beta-zeta-reduce KtArgsNorm,
+  map KtArgsNorm coq.prod->fun KtArgsLam,
   map Kn (k\ coq.mk-app (global (indc k)) LArgs) KnArgs,
   map2 KnArgs KtArgsLam (k\t\coq.map-under-fun t (BranchF k)) Bs.
 
@@ -470,13 +471,20 @@ pred coq.bind-ind-arity % calls K under (fun Arity (x : Ity Arity) =>..)
   o:term. %
 bind-ind-arity.aux (prod N T B) (fun N T F) AccT AccTy IT K :- !,
   @pi-decl N T x\ bind-ind-arity.aux (B x) (F x) [x|AccT] [T|AccTy] IT K.
-bind-ind-arity.aux (let _ _ X B) F AccT AccTy IT K :- !,
-  bind-ind-arity.aux (B X) F AccT AccTy IT K.
+bind-ind-arity.aux (let N T X B) (let N T X F) AccT AccTy IT K :- !,
+  @pi-def N T X x\ bind-ind-arity.aux (B x) (F x) AccT AccTy IT K.
 bind-ind-arity.aux (sort _ as Sort) (fun `i` ITy F) AccT AccTy IT K :-
   rev AccT Vars,
   coq.mk-app IT Vars ITy,
   @pi-decl `i` ITy x\ K Sort {append Vars [x]} {rev [ITy|AccTy]} (F x).
 coq.bind-ind-arity IT Arity F R :- bind-ind-arity.aux Arity R [] [] IT F.
+% As above but let-ins are reduced
+pred coq.bind-ind-arity-no-let i:term, i:term, i:(term -> list term -> list term -> term -> prop), o:term.
+coq.bind-ind-arity-no-let IT Arity F R :-
+  (pi N T X B F AccT AccTy IT K\
+    bind-ind-arity.aux (let N T X B) F AccT AccTy IT K :- !,
+      bind-ind-arity.aux (B X) F AccT AccTy IT K) =>
+  bind-ind-arity.aux Arity R [] [] IT F.
 
 % coq.with-TC Class Instance->Clause Code: runs Code under a context augmented with
 % all instances for Class transformed by Instance->Clause.