Ported the plugin to Coq 8.13

.gitignore

@@ -23,3 +23,5 @@ plugin/Makefile
 plugin/.merlin
 *.out
 _opam
+*.vok
+*.vos

.gitmodules

@@ -1,6 +1,8 @@
 [submodule "plugin/src/coq-plugin-lib"]
 	path = plugin/src/coq-plugin-lib
-	url = https://github.com/uwplse/coq-plugin-lib.git
+	url = https://github.com/agrarpan/coq-plugin-lib.git
+	branch = coq-8.13
 [submodule "plugin/deps/fix-to-elim"]
 	path = plugin/deps/fix-to-elim
-	url = https://github.com/uwplse/fix-to-elim.git
+	url = https://github.com/agrarpan/fix-to-elim.git
+	branch = coq-8.13

plugin/Makefile.local

@@ -0,0 +1 @@
+OCAMLWARN=-warn-error +a-3-8-40-32-28-33-60

plugin/_CoqProject

@@ -19,7 +19,8 @@
 -I src/automation/search
 -I src/automation/lift
 -I src
--R theories Ornamental
+-Q theories Ornamental
+-R coq Foo
 
 src/coq-plugin-lib/src/utilities/utilities.ml
 src/coq-plugin-lib/src/utilities/utilities.mli
@@ -148,12 +149,12 @@ src/automation/lift/lift.mli
 
 src/frontend.ml
 src/frontend.mli
-src/ornamental.ml4
+src/ornamental.mlg
 src/ornaments.mlpack
 
 theories/Adjoint.v
 theories/Unpack.v
 theories/Prod.v
 theories/Eliminators.v
 theories/Equivalences.v
-theories/Ornaments.v
+theories/Ornaments.v

plugin/build.sh

@@ -1,12 +1,13 @@
 #!/usr/bin/env bash
 git submodule init
 git submodule update
+echo "making makefile and cleaning"
+make uninstall
+make clean
+coq_makefile -f _CoqProject -o Makefile
 echo "building dependencies"
 cd deps/fix-to-elim/plugin
 ./build.sh
 cd ../../..
 echo "building DEVOID"
-
-coq_makefile -f _CoqProject -o Makefile
-make clean && make && make install
-
+make && make install

plugin/coq/Indtype.v

@@ -1,7 +1,6 @@
-Add LoadPath "coq".
 Require Import Ornamental.Ornaments.
 Require Import List Sorting.Permutation.
-Require Import Test TestLift.
+Require Import Foo.Test Foo.TestLift.
 
 Notation "( x ; y )" := (existT _ x y) (no associativity).
 Notation "p .1" := (projT1 p) (left associativity, at level 8, format "p .1").

plugin/coq/NoSmartCache.v

@@ -1,7 +1,6 @@
-Add LoadPath "coq".
 Require Import Ornamental.Ornaments.
 Require Import List.
-Require Import minimal_records.
+Require Import Foo.minimal_records.
 Require Import Coq.Bool.Bool.
 
 Set DEVOID search prove equivalence. (* <-- Correctness proofs for search *)
@@ -11,20 +10,20 @@ Unset DEVOID smart cache. (* <-- Disable the smart cache! *)
 
 Module leb.
 
-Lemma leb_implb : forall b1 b2, leb b1 b2 -> implb b1 b2 = true.
+Lemma leb_implb : forall b1 b2, Bool.le b1 b2 -> implb b1 b2 = true.
 Proof.
-  apply leb_implb.
+  apply Bool.le_implb.
 Qed.
 
 End leb.
 
-Preprocess Module leb as leb' { opaque Bool.leb_implb }.
+Preprocess Module leb as leb' { opaque Bool.le_implb }.
 Definition leb_implb := leb'.leb_implb.
 
-Definition f (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H) := ifb (eqb (negb (andb b1 (orb b2 (xorb b3 b4)))) true) false b4.
-Definition g (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb b1 (andb b2 (xorb b3 b4)))) true) false b4.
-Definition h (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb (andb b1 b2) (xorb b3 b4))) true) false b4.
-Definition i (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (andb (orb b1 b2) (xorb b3 b4))) true) false b4.
+Definition f (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H) := ifb (eqb (negb (andb b1 (orb b2 (xorb b3 b4)))) true) false b4.
+Definition g (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb b1 (andb b2 (xorb b3 b4)))) true) false b4.
+Definition h (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb (andb b1 b2) (xorb b3 b4))) true) false b4.
+Definition i (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (andb (orb b1 b2) (xorb b3 b4))) true) false b4.
 
 Time Lift Generated'.output Handwritten'.output in f as f'.
 Time Lift Generated'.output Handwritten'.output in g as g'.

plugin/coq/SmartCache.v

@@ -1,7 +1,6 @@
-Add LoadPath "coq".
 Require Import Ornamental.Ornaments.
 Require Import List.
-Require Import minimal_records.
+Require Import Foo.minimal_records.
 Require Import Coq.Bool.Bool.
 
 Set DEVOID search prove equivalence. (* <-- Correctness proofs for search *)
@@ -11,20 +10,20 @@ Set DEVOID smart cache.
 
 Module leb.
 
-Lemma leb_implb : forall b1 b2, leb b1 b2 -> implb b1 b2 = true.
+Lemma leb_implb : forall b1 b2, Bool.le b1 b2 -> implb b1 b2 = true.
 Proof.
-  apply leb_implb.
+  apply Bool.le_implb.
 Qed.
 
 End leb.
 
-Preprocess Module leb as leb' { opaque Bool.leb_implb }.
+Preprocess Module leb as leb' { opaque Bool.le_implb }.
 Definition leb_implb := leb'.leb_implb.
 
-Definition f (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H) := ifb (eqb (negb (andb b1 (orb b2 (xorb b3 b4)))) true) false b4.
-Definition g (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb b1 (andb b2 (xorb b3 b4)))) true) false b4.
-Definition h (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb (andb b1 b2) (xorb b3 b4))) true) false b4.
-Definition i (b1 b2 b3 b4 : bool) (H : leb true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (andb (orb b1 b2) (xorb b3 b4))) true) false b4.
+Definition f (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H) := ifb (eqb (negb (andb b1 (orb b2 (xorb b3 b4)))) true) false b4.
+Definition g (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb b1 (andb b2 (xorb b3 b4)))) true) false b4.
+Definition h (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (orb (andb b1 b2) (xorb b3 b4))) true) false b4.
+Definition i (b1 b2 b3 b4 : bool) (H : Bool.le true false) (H0 : leb_implb true false H = leb_implb true false H)  := ifb (eqb (negb (andb (orb b1 b2) (xorb b3 b4))) true) false b4.
 
 Time Lift Generated'.output Handwritten'.output in f as f'.
 Time Lift Generated'.output Handwritten'.output in g as g'.

plugin/coq/Swap.v

@@ -46,7 +46,8 @@ opaque (* ignore these, just for speed *)
   Nat.lt_irrefl
   Nat.le_refl
   Nat.bi_induction
-  Nat.central_induction;
+  Nat.central_induction
+  Nat.sub_succ;
 hint (* some tacic hints for better scripts *)
   "auto"
 }.

plugin/coq/TestFindLift.v

@@ -1,4 +1,3 @@
-Add LoadPath "coq".
 Require Import List.
 Require Import Ornamental.Ornaments.
 

plugin/coq/TestLift.v

@@ -1,8 +1,7 @@
-Add LoadPath "coq".
 Require Import List.
 Require Import Ornamental.Ornaments.
-Require Import Test.
-Require Import Infrastructure.
+Require Import Foo.Test.
+Require Import Foo.Infrastructure.
 
 (*
  * Test lifting directly

plugin/coq/TestUnpack.v

@@ -2,13 +2,12 @@
  * Basic lifting tests for unpack, building on TestLift.v
  *)
 
-Add LoadPath "coq".
 Require Import Vector.
 Require Import List.
-Require Import Test.
-Require Import TestLift.
+Require Import Foo.Test.
+Require Import Foo.TestLift.
 Require Import Ornamental.Ornaments.
-Require Import Infrastructure.
+Require Import Foo.Infrastructure.
 
 Set DEVOID lift type.
 

plugin/coq/examples/Assumptions.v

@@ -10,7 +10,6 @@
  * See issue #37 for the status of lifting restrictions that Search makes.
  *)
 
-Add LoadPath "coq/examples".
 Require Import Ornamental.Ornaments.
 Require Import List ZArith Nat.
 Require Import Search.

plugin/coq/examples/Example.v

@@ -6,7 +6,6 @@
  * take a look at the state of this file in the ITP release.
  *)
 
-Add LoadPath "coq/examples".
 Require Import Vector.
 Require Import List.
 Require Import Ornamental.Ornaments.
@@ -309,7 +308,7 @@ Configure Lift packed vector { opaque Eqdep_dec.UIP_dec Nat.eq_dec }.
 (*
  * Then we repair (lifting hs_to_coqV_p first makes this faster and makes the result prettier):
  *)
-Lift Module packed vector in hs_to_coqV_p as hs_to_coqV_u.
+Lift Module packed vector in hs_to_coqV_p as hs_to_coqV_u {opaque hs_to_coqV_p.list_to_t_adjunction}.
 Repair Module packed vector in packed_vector as uf.
 
 (* We are done. Here are our final types: *)

plugin/coq/examples/Lift.v

@@ -2,7 +2,6 @@
  * Walkthrough of lifting for Section 4
  *)
 
-Add LoadPath "coq/examples".
 Require Import Vector.
 Require Import List.
 Require Import Ornamental.Ornaments.

plugin/coq/examples/LiftSpec.v

@@ -2,7 +2,6 @@
  * Section 3.2 Examples
  *)
 
-Add LoadPath "coq/examples".
 Require Import Vector.
 Require Import List.
 Require Import Ornamental.Ornaments.

plugin/coq/examples/Search.v

@@ -2,7 +2,6 @@
  * Walkthrough of search for Section 4
  *)
 
-Add LoadPath "coq/examples".
 Require Import Vector.
 Require Import List.
 Require Import Ornamental.Ornaments.

plugin/coq/prod_rect.v

@@ -1,5 +1,5 @@
 From Ornamental Require Import Ornaments.
-Require Import Infrastructure.
+Require Import Foo.Infrastructure.
 
 Set DEVOID search prove equivalence.
 Set DEVOID lift type.

plugin/src/automation/depelim.ml

@@ -8,6 +8,7 @@ open Nameops
 open Declarations
 open Apputils
 open Sigmautils
+open Contextutils
 
 (*
  * Given a relative context quantifying an inductive family's indices, assemble
@@ -85,16 +86,16 @@ let eta_guard_motive ncons nindex typ =
         in
         let { index_type; packer } = dest_sigT domain in
         let packed_type = Reduction.beta_app (Vars.lift 1 packer) (mkRel 1) in
-        let name_1 = Name.map (fun id -> add_suffix id "_1") name in
-        let name_2 = Name.map (fun id -> add_suffix id "_2") name in
+        let name_1 = Name.map (fun id -> add_suffix id "_1") (Context.binder_name name) in
+        let name_2 = Name.map (fun id -> add_suffix id "_2") (Context.binder_name name) in
         mkApp
           (sigT_rect,
            [|index_type; packer;
              mkLambda (name, domain, codomain);
-             mkLambda (name_1, index_type,
-                       mkLambda (name_2, packed_type, body))|])
+             mkLambda (get_rel_ctx_name name_1, index_type,
+                       mkLambda (get_rel_ctx_name name_2, packed_type, body))|])
       else
-        mkLambda (name, domain, body)
+        mkLambda ( name, domain, body)
   in
   Vars.lift (ncons + nindex + 1) typ |> aux 0
 

plugin/src/automation/lift/lift.ml

@@ -19,6 +19,7 @@ open Promotion
 open Liftconfig
 open Liftrules
 open Evd
+open Record
 
 (*
  * The top-level lifting algorithm
@@ -144,13 +145,13 @@ let lift_evar c env trm lift_rec sigma =
       match info.evar_body with
       | Evar_empty -> sigma, Evar_empty
       | Evar_defined bod ->
-         let bod = EConstr.to_constr sigma bod in
+         let bod = EConstr.to_constr ~abort_on_undefined_evars:false sigma bod in
          let sigma, lifted_bod = lift_rec env sigma c bod in
          sigma, Evar_defined (EConstr.of_constr lifted_bod)
     in
     let sigma, evar_candidates =
       if Option.has_some info.evar_candidates then
-        let candidates = List.map (EConstr.to_constr sigma) (Option.get info.evar_candidates) in
+        let candidates = List.map (EConstr.to_constr ~abort_on_undefined_evars:false sigma) (Option.get info.evar_candidates) in
         let sigma, lifted_candidates = map_rec_args_list lift_rec env sigma c candidates in
         sigma, Some (List.map EConstr.of_constr lifted_candidates)
       else
@@ -201,28 +202,28 @@ let lift_core env c trm sigma =
         | Prod (n, t, b) ->
            (* PROD *)
            let sigma, t' = lift_rec en sigma c t in
-           let en_b = push_local (n, t) en in
+           let en_b = push_local (n.binder_name, t) en in
            let sigma, b' = lift_rec en_b sigma (zoom c) b in
            (sigma, mkProd (n, t', b'))
         | Lambda (n, t, b) ->
            (* LAMBDA *)
            let sigma, t' = lift_rec en sigma c t in
-           let en_b = push_local (n, t) en in
+           let en_b = push_local (n.binder_name, t) en in
            let sigma, b' = lift_rec en_b sigma (zoom c) b in
            (sigma, mkLambda (n, t', b'))
         | LetIn (n, trm, typ, e) ->
            (* LETIN *)
            let sigma, trm' = lift_rec en sigma c trm in
            let sigma, typ' = lift_rec en sigma c typ in
-           let en_e = push_let_in (n, trm, typ) en in
+           let en_e = push_let_in (n.binder_name, trm, typ) en in
            let sigma, e' = lift_rec en_e sigma (zoom c) e in
            (sigma, mkLetIn (n, trm', typ', e'))
-        | Case (ci, ct, m, bs) ->
+        | Case (ci, ct, iv, m, bs) ->
            (* CASE (will not work if this destructs over A; preprocess first) *)
            let sigma, ct' = lift_rec en sigma c ct in
            let sigma, m' = lift_rec en sigma c m in
            let sigma, bs' = map_rec_args lift_rec en sigma c bs in
-           (sigma, mkCase (ci, ct', m', bs'))
+           (sigma, mkCase (ci, ct', iv, m', bs'))
         | Fix ((is, i), (ns, ts, ds)) ->
            (* FIX (will not work if this destructs over A; preprocess first) *)
            let sigma, ts' = map_rec_args lift_rec en sigma c ts in
@@ -272,17 +273,17 @@ let define_lifted_eliminator ?(suffix="_sigT") l ind0 ind sort =
       let raw_ident = Indrec.make_elimination_ident ind_name sort in
       Nameops.add_suffix raw_ident suffix
     in
-    let elim0 = Indrec.lookup_eliminator ind0 sort in
-    let elim = Indrec.lookup_eliminator ind sort in
+    let elim0 = Indrec.lookup_eliminator env ind0 sort in
+    let elim = Indrec.lookup_eliminator env ind sort in
     let sigma, (eta_term, eta_type) =
       let sigma, term = Evarutil.new_global (Evd.from_env env) elim in
       let sigma, typ = Typing.type_of env sigma term in
       let typ = Reductionops.nf_betaiotazeta env sigma typ in
       let term, typ = EConstr.(to_constr sigma term, to_constr sigma typ) in
       sigma, Depelim.eta_guard_eliminator mind_specif term typ
     in
-    let elim' = UnivGen.constr_of_global (Defutils.define_term ~typ:eta_type ident sigma eta_term true) in
-    let elim0 = UnivGen.constr_of_global elim0 in
+    let elim' = UnivGen.constr_of_monomorphic_global (Defutils.define_term ~typ:eta_type ident sigma eta_term) in
+    let elim0 = UnivGen.constr_of_monomorphic_global elim0 in
     save_lifting (lift_to l, lift_back l, elim0) elim';
     save_lifting (lift_back l, lift_to l, elim') elim0
 
@@ -314,7 +315,7 @@ let do_lift_ind env sigma l typename suffix ind ignores is_lift_module =
   else
     let _ = check_inductive_supported mind_body in
     let env, univs, arity, constypes = open_inductive ~global:true env mind_specif in
-    let sigma = Evd.update_sigma_env sigma env in
+    let sigma = Evd.update_sigma_univs (Global.universes ()) sigma in
     let nparam = mind_body.mind_nparams_rec in
     let sigma, arity' = do_lift_term env sigma l arity ignores in
     let sigma, constypes' = map_state (fun trm sigma -> do_lift_term env sigma l trm ignores) constypes sigma in
@@ -325,7 +326,7 @@ let do_lift_ind env sigma l typename suffix ind ignores is_lift_module =
     let ind' =
       declare_inductive typename consnames is_template univs nparam arity' constypes'
     in
-    List.iter (define_lifted_eliminator l ind ind') ind_body.mind_kelim;
+    List.iter (define_lifted_eliminator l ind ind') (Inductiveops.sorts_below ind_body.mind_kelim);
     declare_inductive_liftings l ind ind' (List.length constypes);
     (* Lift record projections *)
     try
@@ -350,14 +351,14 @@ let do_lift_ind env sigma l typename suffix ind ignores is_lift_module =
                let c = mkConst p in
                let sigma, p_lifted = do_lift_term env sigma l c ignores in
                let n = Names.Label.to_id (Names.Constant.label p) in
-               let def = Defutils.define_term n sigma p_lifted true in
+               let def = Defutils.define_term n sigma p_lifted in
                Feedback.msg_info
                  (Pp.str (Printf.sprintf "DEVOID generated %s" (Names.Id.to_string n)));
                def))
           r.s_PROJ
       in
       (try
-         declare_structure (ind', (ind', 1), pks, ps);
+         Record.Internal.declare_structure_entry {s_CONST = (ind',1); s_EXPECTEDPARAM = r.s_EXPECTEDPARAM; s_PROJKIND = pks; s_PROJ = ps};
          ind'
        with _ ->
          Feedback.msg_warning