Port fix-to-elim to Coq 8.11

.gitignore

@@ -1,3 +1,8 @@
+# Ignore autogenerated files
+plugin/src/fixtranslation.ml
+plugin/theories/Fixtoelim.vok
+plugin/theories/Fixtoelim.vos
+
 Makefile
 Makefile.conf
 *.d

plugin/Makefile.local

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

plugin/_CoqProject

@@ -86,7 +86,7 @@ src/automation/desugar.ml
 src/options.mli
 src/options.ml
 
-src/fixtranslation.ml4
+src/fixtranslation.mlg
 src/fixtoelim.mlpack
 
 theories/Fixtoelim.v

plugin/src/automation/desugar.ml

@@ -46,7 +46,7 @@ let decompose_indvect env ind_type sigma =
     with _ ->
       failwith "type passed to decompose_indvect must be an inductive type"
   in
-  let nparam = inductive_nparams (out_punivs pind) in
+  let nparam = inductive_nparams env (out_punivs pind) in
   let params, indices = Array.chop nparam args in
   sigma, (pind, params, indices)
 
@@ -129,7 +129,7 @@ let premise_of_case env ind_fam (ctxt, body) =
         let args = Array.append (Array.map shift indices) [|mkRel 1|] in
         let rec_type = prod_appvect (shift_by j fix_type) args in
         let fix_call = mkApp (mkRel j, args) in
-        mkLambda (fix_name, rec_type, abstract_subterm fix_call body)
+        mkLambda (get_rel_ctx_name fix_name, rec_type, abstract_subterm fix_call body)
       | _ ->
         body
     in mkLambda_or_LetIn decl body'
@@ -182,7 +182,7 @@ let expand_case env sigma case_term cons_sum =
  *)
 let configure_eliminator env sigma ind_fam typ =
   let ind, params = dest_ind_family ind_fam |> on_fst out_punivs in
-  let nb = inductive_nrealargs ind + 1 in
+  let nb = inductive_nrealargs env ind + 1 in
   let typ_ctxt, typ_body =
     let typ_ctxt, typ_body = decompose_prod_n_assum nb typ in
     let ind_sort = get_arity env ind_fam |> snd in
@@ -194,7 +194,7 @@ let configure_eliminator env sigma ind_fam typ =
   let sigma, elim =
     let typ_env = Environ.push_rel_context typ_ctxt env in
     let sigma, typ_sort = infer_sort typ_env sigma typ_body in
-    let elim_trm = Indrec.lookup_eliminator ind typ_sort in
+    let elim_trm = Indrec.lookup_eliminator env ind typ_sort in
     new_global sigma elim_trm
   in
   let motive = recompose_lam_assum typ_ctxt typ_body in
@@ -324,7 +324,7 @@ let desugar_constr env sigma trm =
         | Fix (([|fix_pos|], 0), ([|fix_name|], [|fix_type|], [|fix_term|])) ->
            aux
              env
-             (desugar_fixpoint env sigma fix_pos fix_name fix_type fix_term)
+             (desugar_fixpoint env sigma fix_pos fix_name.binder_name fix_type fix_term)
         | Fix _ ->
            user_err "desugar" err_mutual_recursion [try_opaque] [cool_feature]
         | CoFix _ ->
@@ -342,8 +342,9 @@ let desugar_constr env sigma trm =
       trm
   in
   let sigma, trm' = aux env (sigma, trm) in
+  let eterm = EConstr.of_constr trm' in
   try
-    let _ = Typing.e_type_of env (ref sigma) (EConstr.of_constr trm') in
+    let (sigma, _) = Typing.type_of ~refresh:false env sigma eterm (* might be able to set refresh to false *) in
     sigma, trm'
   with PretypeError (env, sigma, err) ->
     user_err

plugin/src/automation/desugar.mli

@@ -1,7 +1,3 @@
-open Environ
-open Constr
-open Evd
-
 (*
  * Translate the given term into an equivalent, bisimulative (i.e., homomorpic
  * reduction behavior) version using eliminators instead of match or fix

plugin/src/fixtoelim.mlpack

@@ -14,8 +14,8 @@ Sigmautils
 Idutils
 
 Stateutils
-Envutils
 Contextutils
+Envutils
 
 Hofs
 Debruijn
@@ -28,9 +28,8 @@ Indutils
 
 Modutils
 
-Transform
-
 Printing
+Transform
 
 Preprocess_errors
 

plugin/src/fixtranslation.ml4 → plugin/src/fixtranslation.mlg

@@ -1,5 +1,6 @@
 DECLARE PLUGIN "fixtoelim"
 
+{ 
 open Stdarg
 open Desugar
 open Names
@@ -17,8 +18,8 @@ open Declarations
 open Preprocess_errors
 open Options
 
-module Globmap = Globnames.Refmap
-module Globset = Globnames.Refset
+module Globmap = GlobRef.Map
+module Globset = GlobRef.Set
 module DPset = Set.Make(DirPath)
 
 (*
@@ -193,18 +194,19 @@ let do_desugar_module ?(opaques=[]) ?(transparents=[]) ident mod_ref =
   in
   let consts = all_transitive_constants env m exceptions exception_mods in
   let init () = List.fold_left include_constant Globmap.empty consts in
-  ignore (transform_module_structure ~init ~opaques ident desugar_constr m)
+  ignore (transform_module_structure env ~init ~opaques ident desugar_constr m)
+}
 
 (* --- Commands --- *)
 
 (* Desugar any/all fix/match subterms into eliminator applications *)
 VERNAC COMMAND EXTEND TranslateMatch CLASSIFIED AS SIDEFF
 | [ "Preprocess" reference(const_ref) "as" ident(id) ] ->
-  [ do_desugar_constant id const_ref ]
+  { do_desugar_constant id const_ref }
 | [ "Preprocess" "Module" reference(mod_ref) "as" ident(id) ] ->
-  [ do_desugar_module id mod_ref ]
+  { do_desugar_module id mod_ref }
 | [ "Preprocess" "Module" reference(mod_ref) "as" ident(id) "{" "opaque" ne_reference_list(opaq_refs) "}" ] ->
-  [ do_desugar_module ~opaques:opaq_refs id mod_ref ]
+  { do_desugar_module ~opaques:opaq_refs id mod_ref }
 | [ "Preprocess" "Module" reference(mod_ref) "as" ident(id) "{" "transparent" ne_reference_list(transp_refs) "}" ] ->
-  [ do_desugar_module ~transparents:transp_refs id mod_ref ]
+  { do_desugar_module ~transparents:transp_refs id mod_ref }
 END

plugin/test.sh

@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
+set -euxo pipefail
 coqc coq/Preprocess.v
 coqc coq/PreprocessModule.v
 coqc coq/DefaultOpaque.v