Port coq-plugin-lib to Coq 8.11

.gitignore

@@ -23,3 +23,4 @@ plugin/Makefile
 plugin/.merlin
 *.out
 _opam
+src/plibrary.ml

Makefile.local

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

_CoqProject

@@ -91,7 +91,7 @@ src/coq/devutils/printing.ml
 src/coq/decompiler/decompiler.mli
 src/coq/decompiler/decompiler.ml
 
-src/plibrary.ml4
+src/plibrary.mlg
 src/plib.mlpack
 
 theories/Plib.v

src/coq/constants/equtils.ml

@@ -14,7 +14,7 @@ let coq_init_logic =
 
 (* equality *)
 let eq : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "eq")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "eq")), 0)
 
 (* Constructor for quality *)
 let eq_refl : types =

src/coq/constants/idutils.ml

@@ -4,7 +4,6 @@
 
 open Constr
 open Names
-open Environ
 open Evd
 
 let coq_init_datatypes =

src/coq/constants/produtils.ml

@@ -14,7 +14,7 @@ let coq_init_data =
 
 (* prod types *)
 let prod : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_data (Label.make "prod")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_data (Label.make "prod")), 0)
 
 (* Introduction for sigma types *)
 let pair : constr =

src/coq/constants/proputils.ml

@@ -4,7 +4,6 @@
 
 open Constr
 open Names
-open Apputils
 
 let coq_init_logic =
   ModPath.MPfile
@@ -14,7 +13,7 @@ let coq_init_logic =
 
 (* Logical or *)
 let logical_or : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "or")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "or")), 0)
 
 (* left constructor of \/ *)
 let or_introl : types =
@@ -27,7 +26,7 @@ let or_intror : types =
 
 (* Logical and *)
 let logical_and : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_logic (Label.make "and")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_logic (Label.make "and")), 0)
 
 (* constructor of /\ *)
 let conj : types =

src/coq/constants/sigmautils.ml

@@ -14,7 +14,7 @@ let coq_init_specif =
 
 (* sigma types *)
 let sigT : types =
-  mkInd (MutInd.make1 (KerName.make2 coq_init_specif (Label.make "sigT")), 0)
+  mkInd (MutInd.make1 (Names.KerName.make coq_init_specif (Label.make "sigT")), 0)
 
 (* Introduction for sigma types *)
 let existT : types =

src/coq/decompiler/decompiler.ml

@@ -36,11 +36,11 @@ let parse_tac_str (s : string) : unit Proofview.tactic =
 (* Run a coq tactic against a given goal, returning generated subgoals *)
 let run_tac env sigma (tac : unit Proofview.tactic) (goal : constr)
     : Goal.goal list * Evd.evar_map =
-  let p = Proof.start sigma [(env, EConstr.of_constr goal)] in
-  let (p', _) = Proof.run_tactic env tac p in
-  let (subgoals, _, _, _, sigma) = Proof.proof p' in
-  subgoals, sigma
-    
+  let p = Proof.start ~name:(destVar goal) ~poly:true sigma [(env, EConstr.of_constr goal)] in
+  let (p', _, _) = Proof.run_tactic env tac p in
+  let compact_p = Proof.data (Proof.compact p') in
+  (compact_p.goals, compact_p.sigma)
+
 (* Returns true if the given tactic solves the goal. *)
 let solves env sigma (tac : unit Proofview.tactic) (goal : constr) : bool state =
   try
@@ -476,7 +476,7 @@ and apply_in (n, valu, typ, body) (env, sigma, opts) : tactical option =
 
 (* Last resort decompile let-in as a pose.  *)
 and pose (n, valu, t, body) (env, sigma, opts) : tactical option =
-  let n' = fresh_name env n in
+  let n' = fresh_name env n.binder_name in
   let env' = push_let_in (Name n', valu, t) env in
   let decomp_body = first_pass env' sigma opts body in
   (* If the binding is NEVER used, just skip this. *)

src/coq/devutils/printing.ml

@@ -24,7 +24,7 @@ module CRD = Context.Rel.Declaration
 let pr_global_as_constr gref =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  pr_constr_env env sigma (Universes.constr_of_global gref)
+  pr_constr_env env sigma (UnivGen.constr_of_monomorphic_global gref)
 
 (* Using pp, prints directly to a string *)
 let print_to_string (pp : formatter -> 'a -> unit) (trm : 'a) : string =
@@ -66,11 +66,12 @@ let sort_as_string s =
 
 (* Prints a term *)
 let rec term_as_string (env : env) (trm : types) =
+  let open Context in
   match kind trm with
   | Rel i ->
      (try
        let (n, _, _) = CRD.to_tuple @@ lookup_rel i env in
-       Printf.sprintf "(%s [Rel %d])" (name_as_string n) i
+       Printf.sprintf "(%s [Rel %d])" (name_as_string n.binder_name) i
      with
        Not_found -> Printf.sprintf "(Unbound_Rel %d)" i)
   | Var v ->
@@ -84,22 +85,22 @@ let rec term_as_string (env : env) (trm : types) =
   | Prod (n, t, b) ->
      Printf.sprintf
        "(Π (%s : %s) . %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env t)
-       (term_as_string (push_local (n, t) env) b)
+       (term_as_string (push_local (n.binder_name, t) env) b)
   | Lambda (n, t, b) ->
      Printf.sprintf
        "(λ (%s : %s) . %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env t)
-       (term_as_string (push_local (n, t) env) b)
+       (term_as_string (push_local (n.binder_name, t) env) b)
   | LetIn (n, trm, typ, e) ->
      Printf.sprintf
        "(let (%s : %s) := %s in %s)"
-       (name_as_string n)
+       (name_as_string n.binder_name)
        (term_as_string env typ)
        (term_as_string env trm)
-       (term_as_string (push_let_in (n, trm, typ) env) e)
+       (term_as_string (push_let_in (n.binder_name, trm, typ) env) e)
   | App (f, xs) ->
      Printf.sprintf
        "(%s %s)"
@@ -119,14 +120,15 @@ let rec term_as_string (env : env) (trm : types) =
      let name_id = (ind_bodies.(i_index)).mind_typename in
      Id.to_string name_id
   | Fix ((is, i), (ns, ts, ds)) ->
-     let env_fix = push_rel_context (bindings_for_fix ns ds) env in
+     let ns_binder_name = Array.map (fun x -> x.binder_name) ns in
+     let env_fix = push_rel_context (bindings_for_fix ns_binder_name ds) env in
      String.concat
        " with "
        (map3
           (fun n t d ->
             Printf.sprintf
              "(Fix %s : %s := %s)"
-             (name_as_string n)
+             (name_as_string n.binder_name)
              (term_as_string env t)
              (term_as_string env_fix d))
           (Array.to_list ns)
@@ -180,7 +182,7 @@ let env_as_string (env : env) : string =
          let (n, b, t) = CRD.to_tuple @@ lookup_rel i env in
          Printf.sprintf
            "%s (Rel %d): %s"
-           (name_as_string n)
+           (name_as_string n.binder_name)
            i
            (term_as_string (pop_rel_context i env) t))
        all_relis)

src/coq/devutils/printing.mli

@@ -8,7 +8,7 @@ open Evd
 (* --- Coq terms --- *)
 
 (* Pretty-print a `global_reference` with fancy `constr` coloring. *)
-val pr_global_as_constr : global_reference -> Pp.t
+val pr_global_as_constr : Globnames.global_reference -> Pp.t
 
 (* Gets a name as a string *)
 val name_as_string : Name.t -> string

src/coq/logicutils/contexts/contextutils.ml

@@ -20,7 +20,8 @@ module CND = Context.Named.Declaration
 let is_rel_assum = CRD.is_local_assum
 
 (* Is the rel declaration a local definition? *)
-let is_rel_defin = CRD.is_local_def
+(* let is_rel_defin x = CRD.is_local_def (get_rel_ctx_name x) *)
+let is_rel_defin x = CRD.is_local_def x
 
 (* Is the named declaration an assumption? *)
 let is_named_assum = CND.is_local_assum
@@ -47,14 +48,25 @@ let named_value decl = CND.get_value decl
 
 (* Get the type of a named declaration *)
 let named_type decl = CND.get_type decl
-
+
+(* --- Context manipulation tools --- *)
+
+(* Get relative context for a name *)
+let get_rel_ctx_name name = 
+  match name with (* handle if anon or not *)
+  | Anonymous -> Context.anonR
+  | Name idt -> Context.nameR idt
+
+(* Get relative context for a declaration *)
+let get_rel_ctx decl = get_rel_ctx_name (rel_name decl)
+
 (* --- Constructing declarations --- *)
 
 (* Make the rel declaration for a local assumption *)
-let rel_assum (name, typ) = CRD.LocalAssum (name, typ)
+let rel_assum (name, typ) = CRD.LocalAssum (get_rel_ctx_name name, typ)
 
 (* Make the rel declaration for a local definition *)
-let rel_defin (name, def, typ) = CRD.LocalDef (name, def, typ)
+let rel_defin (name, def, typ) = CRD.LocalDef (get_rel_ctx_name name, def, typ)
 
 (* Make the named declaration for a local assumption *)
 let named_assum (id, typ) = CND.LocalAssum (id, typ)
@@ -104,7 +116,7 @@ let smash_prod_assum ctxt body =
     (fun body decl ->
        match rel_value decl with
        | Some defn -> Vars.subst1 defn body
-       | None -> mkProd (rel_name decl, rel_type decl, body))
+       | None -> mkProd (get_rel_ctx decl, rel_type decl, body))
     ~init:body
     ctxt
 
@@ -117,7 +129,7 @@ let smash_lam_assum ctxt body =
     (fun body decl ->
        match rel_value decl with
        | Some defn -> Vars.subst1 defn body
-       | None -> mkLambda (rel_name decl, rel_type decl, body))
+       | None -> mkLambda (get_rel_ctx decl, rel_type decl, body))
     ~init:body
     ctxt
 
@@ -127,39 +139,41 @@ let smash_lam_assum ctxt body =
  *)
 let decompose_prod_n_zeta n term =
   assert (n >= 0);
+  let open Context in
   let rec aux n ctxt body =
     if n > 0 then
       match Constr.kind body with
       | Prod (name, param, body) ->
-        aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body
+        aux (n - 1) (Rel.add (rel_assum (name.binder_name, param)) ctxt) body
       | LetIn (name, def_term, def_type, body) ->
         aux n ctxt (Vars.subst1 def_term body)
       | _ ->
         invalid_arg "decompose_prod_n_zeta: not enough products"
     else
       ctxt, body
   in
-  aux n Context.Rel.empty term
+  aux n Rel.empty term
 
 (*
  * Decompose the first n lambda bindings, zeta-reducing let bindings to reveal
  * further lambda bindings when necessary.
  *)
 let decompose_lam_n_zeta n term =
   assert (n >= 0);
+  let open Context in
   let rec aux n ctxt body =
     if n > 0 then
       match Constr.kind body with
       | Lambda (name, param, body) ->
-        aux (n - 1) (Context.Rel.add (rel_assum (name, param)) ctxt) body
+        aux (n - 1) (Rel.add (rel_assum (name.binder_name, param)) ctxt) body
       | LetIn (name, def_term, def_type, body) ->
         Vars.subst1 def_term body |> aux n ctxt
       | _ ->
         invalid_arg "decompose_lam_n_zeta: not enough lambdas"
     else
       ctxt, body
   in
-  aux n Context.Rel.empty term
+  aux n Rel.empty term
 
 (* Bind the declarations of a local context as product/let-in bindings *)
 let recompose_prod_assum decls term =
@@ -200,8 +214,8 @@ let bindings_for_inductive env mutind_body ind_bodies : rel_declaration list =
        (fun i ind_body ->
          let name_id = ind_body.mind_typename in
          let typ = type_of_inductive env i mutind_body in
-         CRD.LocalAssum (Name name_id, typ))
-       ind_bodies)
+         CRD.LocalAssum (Context.nameR name_id, typ))
+       mutind_body.mind_packets)
 
 (*
  * Fixpoints
@@ -210,7 +224,8 @@ let bindings_for_fix (names : name array) (typs : types array) : rel_declaration
   Array.to_list
     (CArray.map2_i
        (fun i name typ -> CRD.LocalAssum (name, Vars.lift i typ))
-       names typs)
+       (Array.map get_rel_ctx_name names)
+       typs)
 
 (* --- Combining contexts --- *)
 

src/coq/logicutils/contexts/contextutils.mli

@@ -35,8 +35,18 @@ val define_rel_decl :
 (*
  * Construct a named assumption/definition
  *)
+val named_assum : Id.t Context.binder_annot * 'types -> ('constr, 'types) CND.pt
+val named_defin : Id.t Context.binder_annot * 'constr * 'types -> ('constr, 'types) CND.pt
+
+(* Old version, breaking change. TODO: make sure this doesn't affect any downstream plugins
 val named_assum : Id.t * 'types -> ('constr, 'types) CND.pt
 val named_defin : Id.t * 'constr * 'types -> ('constr, 'types) CND.pt
+*)
+
+(* Context name/decl manipulation *)
+val get_rel_ctx_name : Names.name -> Names.Name.t Context.binder_annot
+
+val get_rel_ctx : ('constr, 'types) CRD.pt -> Names.Name.t Context.binder_annot
 
 (* --- Questions about declarations --- *)
 

src/coq/logicutils/contexts/envutils.ml

@@ -6,8 +6,6 @@ open Utilities
 open Environ
 open Constr
 open Declarations
-open Decl_kinds
-open Constrextern
 open Contextutils
 open Evd
 open Names
@@ -33,15 +31,15 @@ let lookup_all_rels (env : env) : rel_declaration list =
 (* Return a name-type pair from the given rel_declaration. *)
 let rel_name_type rel : Name.t * types =
   match rel with
-  | CRD.LocalAssum (n, t) -> (n, t)
-  | CRD.LocalDef (n, _, t) -> (n, t)
+  | CRD.LocalAssum (n, t) -> (n.binder_name, t)
+  | CRD.LocalDef (n, _, t) -> (n.binder_name, t)
 
 
 (* Push a local binding to an environment *)
-let push_local (n, t) = push_rel CRD.(LocalAssum (n, t))
+let push_local (n, t) = push_rel CRD.(LocalAssum (get_rel_ctx_name n, t))
 
 (* Push a let-in definition to an environment *)
-let push_let_in (n, e, t) = push_rel CRD.(LocalDef(n, e, t))
+let push_let_in (n, e, t) = push_rel CRD.(LocalDef(get_rel_ctx_name n, e, t))
 
 (* Lookup n rels and remove then *)
 let lookup_pop (n : int) (env : env) =
@@ -53,7 +51,7 @@ let force_constant_body const_body =
   | Def const_def ->
     Mod_subst.force_constr const_def
   | OpaqueDef opaq ->
-    Opaqueproof.force_proof (Global.opaque_tables ()) opaq
+    fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) opaq)
   | _ ->
     CErrors.user_err ~hdr:"force_constant_body"
       (Pp.str "An axiom has no defining term")