[experiment] Use ext-lib monads

.github/workflows/nix-action-rocq-9.1.yml

@@ -52,11 +52,11 @@ jobs:
         status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: rocq-core'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "rocq-core"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "coq"
   metarocq:
     needs:
@@ -111,35 +111,39 @@ jobs:
         status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "coq"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: equations'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "equations"
+    - if: steps.stepCheck.outputs.status != 'fetched'
+      name: 'Building/fetching previous CI target: ExtLib'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
+        "rocq-9.1" --argstr job "ExtLib"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: stdlib'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "stdlib"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: metarocq-safechecker-plugin'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "metarocq-safechecker-plugin"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: metarocq-erasure-plugin'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "metarocq-erasure-plugin"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: metarocq-translations'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "metarocq-translations"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: 'Building/fetching previous CI target: metarocq-quotation'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "metarocq-quotation"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "metarocq"
   rocq-core:
     needs: []
@@ -193,24 +197,20 @@ jobs:
         status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
         "rocq-9.1" --argstr job "rocq-core"
 name: Nix CI for bundle rocq-9.1
 on:
   pull_request:
     paths:
     - .github/workflows/nix-action-rocq-9.1.yml
-    branches:
-    - '9.1'
   pull_request_target:
     paths-ignore:
     - .github/workflows/nix-action-rocq-9.1.yml
     types:
     - opened
     - synchronize
     - reopened
-    branches:
-    - '9.1'
   push:
     branches:
     - '9.1'

.gitignore

@@ -21,8 +21,8 @@ Makefile.rocq.conf
 *.d
 .merlin
 html/*.html
-.lia.cache
-*/.nia.cache
+**/.lia.cache
+**/.nia.cache
 .hidden
 _opam/
 .vscode/settings.json

.nix/config.nix

@@ -46,17 +46,20 @@
     # rocqPackages.stdlib.override.version = "9.0.0";
     coqPackages.equations.override.version = "v1.3.1-9.1";
     coqPackages.equations.job = false;
+    coqPackages.ExtLib.override.version = "0.13.0";
+    coqPackages.ExtLib.job = false;
     coqPackages.coq.override.version = "9.1";
     coqPackages.stdlib.override.version = "9.0.0";
     coqPackages.stdlib.job = false;
-    
+
     push-branches = ["9.1"];
   };
 
   bundles."rocq-dev" = {
     rocqPackages.rocq-core.override.version = "master";
     rocqPackages.stdlib.override.version = "master";
     coqPackages.equations.override.version = "main";
+    coqPackages.ExtLib.override.version = "master";
     coqPackages.coq.override.version = "master";
     coqPackages.stdlib.override.version = "master";
 

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"3a71d8318b495d464d04ac8bca80b38320448436"
+"f8f9d2623ff780116adc0531f702bc081f21fb1b"

.nix/coq-overlays/metacoq/default.nix

@@ -4,6 +4,7 @@
   single ? false,
   coq,
   equations,
+  ExtLib,
   stdlib,
   version ? null,
 }@args:
@@ -85,6 +86,7 @@ let
             mlPlugin = true;
             propagatedBuildInputs = [
               equations
+              ExtLib
               stdlib
               coq.ocamlPackages.zarith
               coq.ocamlPackages.stdlib-shims

.nix/coq-overlays/metarocq/default.nix

@@ -4,6 +4,7 @@
   coq,
   single ? false,
   equations,
+  ExtLib,
   stdlib,
   version ? null,
 }@args:
@@ -79,6 +80,7 @@ let
             mlPlugin = true;
             propagatedBuildInputs = [
               equations
+              ExtLib
               stdlib
               # rocq-core.ocamlPackages.zarith
               # rocq-core.ocamlPackages.stdlib-shims

common/theories/MonadBasicAst.v

@@ -2,7 +2,7 @@
 From MetaRocq.Utils Require Import utils monad_utils MRList.
 From MetaRocq.Common Require Import BasicAst.
 
-Import MRMonadNotation.
+Import MonadNotation.
 Local Set Universe Polymorphism.
 Local Unset Universe Minimization ToSet.
 

common/theories/UniversesDec.v

@@ -618,7 +618,7 @@ Lemma consistent_extension_on_iff_subgraph_helper cs cstr G G'
   (HG' : gc_of_uctx (lvls, cstr') = Some G')
   : subgraph (make_graph G) (make_graph G').
 Proof.
-  repeat first [ progress cbv [gc_of_uctx monad_utils.bind monad_utils.ret monad_utils.option_monad] in *
+  repeat first [ progress cbv [gc_of_uctx Monad.bind Monad.ret OptionMonad.Monad_option] in *
                | progress cbn [fst snd] in *
                | progress subst
                | progress destruct ?
@@ -699,7 +699,7 @@ Proof.
                  | [ |- _ <-> is_true true ]
                    => split; [ reflexivity | intros _ ]
                  end
-               | progress cbv [uGraph.is_graph_of_uctx monad_utils.bind monad_utils.ret monad_utils.option_monad] in *
+               | progress cbv [uGraph.is_graph_of_uctx Monad.bind Monad.ret OptionMonad.Monad_option] in *
                | progress cbn [MROption.on_Some fst snd] in *
                | rewrite <- uGraph.is_consistent_spec2
                | progress subst
@@ -819,7 +819,7 @@ Proof.
   { specialize_under_binders_by reflexivity.
     destruct uGraph.check_constraints_gen; specialize_by reflexivity; auto. }
   { rewrite uGraph.gc_consistent_iff in *.
-    cbv [uGraph.gc_of_uctx monad_utils.bind monad_utils.ret monad_utils.option_monad MROption.on_Some] in *; cbn [fst snd] in *.
+    cbv [uGraph.gc_of_uctx Monad.bind Monad.ret OptionMonad.Monad_option MROption.on_Some] in *; cbn [fst snd] in *.
     destruct ?.
     all: try congruence.
     all: exfalso; assumption. }

common/theories/uGraph.v

@@ -4,9 +4,10 @@ From MetaRocq.Utils Require Import utils wGraph.
 From MetaRocq.Common Require Import config Universes.
 From Equations.Prop Require Import DepElim.
 From Equations Require Import Equations.
+From ExtLib Require Import Monads.
 Import ConstraintType.
 
-Import MRMonadNotation.
+Import MonadNotation.
 
 
 Arguments Z.add : simpl nomatch.

erasure-plugin/theories/Extraction.v

@@ -10,7 +10,7 @@ From MetaRocq.Utils Require Import utils.
 
 Extraction Blacklist Classes config uGraph Universes Ast String List Nat Int
            UnivSubst Typing Checker Retyping OrderedType Logic Common ws_cumul_pb Classes Numeral
-           Uint63 Induction.
+           Uint63 Induction Monad.
 Set Warnings "-extraction-opaque-accessed".
 Set Warnings "-extraction-reserved-identifier".
 
@@ -42,4 +42,3 @@ Set Extraction Output Directory "src".
 Separate Extraction ErasureFunction.erase Erasure
          (* The following directives ensure separate extraction does not produce name clashes *)
          Stdlib.Strings.String utils Template.UnivSubst ELiftSubst EGlobalEnv.
-

erasure/_RocqProject.in

@@ -60,7 +60,6 @@ theories/Typed/ExtractionCorrectness.v
 theories/Typed/OptimizeCorrectness.v
 theories/Typed/OptimizePropDiscr.v
 theories/Typed/Optimize.v
-theories/Typed/ResultMonad.v
 theories/Typed/Transform.v
 theories/Typed/TypeAnnotations.v
 theories/Typed/Utils.v

erasure/theories/ECoInductiveToInductive.v

@@ -16,7 +16,7 @@ Import MRList (map_InP, map_InP_elim, map_InP_spec).
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.

erasure/theories/EConstructorsAsBlocks.v

@@ -8,7 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EAriti
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.

erasure/theories/EDeps.v

@@ -1,13 +1,13 @@
 From Stdlib Require Import Arith List.
 From Equations Require Import Equations.
+From MetaRocq.Utils Require Import utils.
 From MetaRocq.PCUIC Require Import
      PCUICPrimitive PCUICAst PCUICAstUtils PCUICTyping PCUICInversion PCUICWeakeningEnv PCUICWeakeningEnvTyp.
 Set Warnings "-notation-overridden".
 From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils ECSubst EInduction
   ELiftSubst EGlobalEnv EWcbvEval Extract ESubstitution.
 From MetaRocq.Erasure Require EExtends.
 Set Warnings "+notation-overridden".
-From MetaRocq.Utils Require Import utils.
 From MetaRocq.Common Require Import config.
 
 Derive NoConfusion for term.

erasure/theories/EEnvMap.v

@@ -3,7 +3,7 @@ From Equations Require Import Equations.
 From MetaRocq.Utils Require Import utils.
 From MetaRocq.Common Require Import Kernames EnvMap BasicAst.
 From MetaRocq.Erasure Require Import EAst EGlobalEnv EAstUtils EGlobalEnv EAstUtils.
-Import MRMonadNotation.
+Import MonadNotation.
 
 Lemma fresh_globals_cons_inv {Σ : global_context} {d} : EnvMap.fresh_globals (d :: Σ) -> EnvMap.fresh_globals Σ.
 Proof. intros H; now depelim H. Qed.

erasure/theories/EEtaExpanded.v

@@ -9,7 +9,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EGloba
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.

erasure/theories/EEtaExpandedFix.v

@@ -213,7 +213,7 @@ Qed.
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.
@@ -2054,4 +2054,4 @@ Proof using.
     destruct (expanded_head_viewc u) => //.
     bool.
     eapply isEtaExp_mkApps_intro; eauto. solve_all.
-Qed.
+Qed.

erasure/theories/EGenericGlobalMap.v

@@ -8,7 +8,7 @@ From MetaRocq.Erasure Require Import EAst EAstUtils EInduction EArities
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.
@@ -418,4 +418,4 @@ Proof.
   cbn. eapply gen_transform_wellformed_irrel => //. now eapply gen_transform_wellformed.
 Qed. *)
 
-End sec.
+End sec.

erasure/theories/EGenericMapEnv.v

@@ -8,7 +8,7 @@ From MetaRocq.Erasure Require Import EAst EAstUtils EInduction EArities
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.
@@ -360,4 +360,4 @@ Proof.
   cbn. eapply gen_transform_wellformed_irrel => //. now eapply gen_transform_wellformed.
 Qed. *)
 
-End sec.
+End sec.

erasure/theories/EGlobalEnv.v

@@ -4,7 +4,7 @@ From MetaRocq.Utils Require Import utils.
 From MetaRocq.Common Require Import config BasicAst Reflect.
 From MetaRocq.Erasure Require Import EAst EAstUtils ELiftSubst EReflect ECSubst.
 From Stdlib Require Import ssreflect.
-Import MRMonadNotation.
+Import MonadNotation.
 
 (** * Global environments
 

erasure/theories/EImplementBox.v

@@ -8,7 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EAriti
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.

erasure/theories/EInlineProjections.v

@@ -8,7 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EExtends
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.

erasure/theories/EInlining.v

@@ -8,7 +8,7 @@ From MetaRocq.Utils Require Import MRList bytestring utils monad_utils.
 From MetaRocq.Erasure Require Import EPrimitive EAst EEnvMap EInduction EGlobalEnv.
 
 Import Kernames.
-Import MRMonadNotation.
+Import MonadNotation.
 
 (* Inlining hints *)
 Definition inlining := KernameSet.t.
@@ -173,4 +173,3 @@ Proof.
   intros ? ? [[] ?] [[] ?]; cbn.
   now rewrite /extends_inlined_eprogram /extends_eprogram /=.
 Qed.
-

erasure/theories/EOptimizePropDiscr.v

@@ -13,7 +13,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EDeps EExtends
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.

erasure/theories/ERemapInductives.v

@@ -9,7 +9,7 @@ From MetaRocq.Erasure Require Import EEnvMap EProgram EPrimitive EAst ESpineView
   EAstUtils ELiftSubst EWellformed ECSubst EWcbvEval.
 
 Import Kernames.
-Import MRMonadNotation.
+Import MonadNotation.
 
 Lemma lookup_declared_constructor {Σ id mdecl idecl cdecl} :
   lookup_constructor Σ id.1 id.2 = Some (mdecl, idecl, cdecl) ->

erasure/theories/ERemoveParams.v

@@ -8,7 +8,7 @@ From MetaRocq.Erasure Require Import EPrimitive EAst EAstUtils EInduction EAriti
 
 Local Open Scope string_scope.
 Set Asymmetric Patterns.
-Import MRMonadNotation.
+Import MonadNotation.
 
 From Equations Require Import Equations.
 Set Equations Transparent.