Algebraic universes everywhere

.gitignore

@@ -301,6 +301,7 @@ test-suite/plugin-demo/Makefile.plugin
 template-rocq/Makefile.plugin-e
 template-rocq/Makefile.template-e
 template-rocq/src/g_template_coq.ml
+template-rocq/src/g_template_rocq.ml
 pcuic/Makefile.plugin-e
 erasure/Makefile.plugin-e
 safechecker/Makefile.plugin-e
@@ -413,3 +414,7 @@ template-rocq/_TemplateRocqProject
 .gitignore
 template-rocq/_PluginProject
 template-rocq/_RocqProject
+template-coq/extraction_clauses/clauses.ml
+template-coq/extraction_clauses/clauses.mli
+template-coq/extraction_clauses/loop_checking.mli
+template-coq/extraction_clauses/loop_checking.ml

.nix/rocq-overlays/metarocq/default.nix

@@ -34,11 +34,11 @@ let
       "safechecker"
       "template-pcuic"
     ];
-    "quotation" = [
-      "template-rocq"
-      "pcuic"
-      "template-pcuic"
-    ];
+    # "quotation" = [
+    #   "template-rocq"
+    #   "pcuic"
+    #   "template-pcuic"
+    # ];
     "safechecker-plugin" = [
       "template-pcuic"
       "safechecker"
@@ -52,7 +52,7 @@ let
       "safechecker-plugin"
       "erasure-plugin"
       "translations"
-      "quotation"
+      # "quotation"
     ];
   };
 
@@ -111,7 +111,7 @@ let
                   (lib.elem package [
                     "erasure"
                     "template-pcuic"
-                    "quotation"
+                    # "quotation"
                     "safechecker-plugin"
                     "erasure-plugin"
                     "translations"

.vscode/metarocq.code-workspace

@@ -8,86 +8,94 @@
 
 	// A list of arguments to send to coqtop. Use seperate elements instead of spaces to seperate each argument, especially when a flag expects another trailing argument, e.g. `["-I","./bin"]` instead of `["-I ./bin"]`
 	"coqtop.args": [
+
 		// "-bt", // get backtraces from Rocq on errors
-		"-R", "utils/theories", "MetaRocq.Utils",
-		"-R", "common/theories", "MetaRocq.Common",
-		"-R", "template-rocq/theories", "MetaRocq.Template",
+		"-Q", "utils/theories", "MetaRocq.Utils",
+		"-Q", "common/theories", "MetaRocq.Common",
+		"-Q", "template-rocq/theories", "MetaRocq.Template",
 		"-I", "template-rocq",
 		"-I", "template-rocq/src",
-		"-R", "pcuic/theories", "MetaRocq.PCUIC",
+		"-Q", "pcuic/theories", "MetaRocq.PCUIC",
 		"-I", "pcuic",
 		"-I", "pcuic/src",
-		"-R", "template-pcuic/theories", "MetaRocq.TemplatePCUIC",
-		"-R", "safechecker/theories", "MetaRocq.SafeChecker",
-		"-R", "safechecker-plugin/theories", "MetaRocq.SafeCheckerPlugin",
+		"-Q", "template-pcuic/theories", "MetaRocq.TemplatePCUIC",
+		"-Q", "safechecker/theories", "MetaRocq.SafeChecker",
+		"-Q", "safechecker-plugin/theories", "MetaRocq.SafeCheckerPlugin",
 		"-I", "safechecker-plugin",
 		"-I", "safechecker-plugin/src",
-		"-R", "erasure/theories", "MetaRocq.Erasure",
-		"-R", "erasure-plugin/theories", "MetaRocq.ErasurePlugin",
+		"-Q", "erasure/theories", "MetaRocq.Erasure",
+		"-Q", "erasure-plugin/theories", "MetaRocq.ErasurePlugin",
 		"-I", "erasure-plugin",
 		"-I", "erasure-plugin/src",
-		"-R", "translations", "MetaRocq.Translations",
-		"-R", "quotation/theories", "MetaRocq.Quotation",
-		"-R", "test-suite", "MetaRocq.TestSuite",
-		"-R", "test-suite/plugin-demo/theories", "MetaRocq.ExtractedPluginDemo",
+		"-Q", "translations", "MetaRocq.Translations",
+		"-Q", "quotation/theories", "MetaRocq.Quotation",
+		"-Q", "test-suite", "MetaRocq.TestSuite",
+		"-Q", "test-suite/plugin-demo/theories", "MetaRocq.ExtractedPluginDemo",
 		"-I", "test-suite/plugin-demo",
 		"-I", "test-suite/plugin-demo/src",
-		"-R", "examples", "MetaRocq.Examples",
+		"-Q", "test-suite/loop-checking/theories", "MetaRocq.LoopChecking",
+		"-I", "test-suite/loop-checking/src",
+		"-Q", "examples", "MetaRocq.Examples",
 	    ],
 		"vscoq.args": [
+
 		// "-bt", // get backtraces from Rocq on errors
-		"-R", "utils/theories", "MetaRocq.Utils",
-		"-R", "common/theories", "MetaRocq.Common",
-		"-R", "template-rocq/theories", "MetaRocq.Template",
+		"-Q", "utils/theories", "MetaRocq.Utils",
+		"-Q", "common/theories", "MetaRocq.Common",
+		"-Q", "template-rocq/theories", "MetaRocq.Template",
 		"-I", "template-rocq",
 		"-I", "template-rocq/src",
-		"-R", "pcuic/theories", "MetaRocq.PCUIC",
+		"-Q", "pcuic/theories", "MetaRocq.PCUIC",
 		"-I", "pcuic",
 		"-I", "pcuic/src",
-		"-R", "template-pcuic/theories", "MetaRocq.TemplatePCUIC",
-		"-R", "safechecker/theories", "MetaRocq.SafeChecker",
-		"-R", "safechecker-plugin/theories", "MetaRocq.SafeCheckerPlugin",
+		"-Q", "template-pcuic/theories", "MetaRocq.TemplatePCUIC",
+		"-Q", "safechecker/theories", "MetaRocq.SafeChecker",
+		"-Q", "safechecker-plugin/theories", "MetaRocq.SafeCheckerPlugin",
 		"-I", "safechecker-plugin",
 		"-I", "safechecker-plugin/src",
-		"-R", "erasure/theories", "MetaRocq.Erasure",
-		"-R", "erasure-plugin/theories", "MetaRocq.ErasurePlugin",
+		"-Q", "erasure/theories", "MetaRocq.Erasure",
+		"-Q", "erasure-plugin/theories", "MetaRocq.ErasurePlugin",
 		"-I", "erasure-plugin",
 		"-I", "erasure-plugin/src",
-		"-R", "translations", "MetaRocq.Translations",
-		"-R", "quotation/theories", "MetaRocq.Quotation",
-		"-R", "test-suite", "MetaRocq.TestSuite",
-		"-R", "test-suite/plugin-demo/theories", "MetaRocq.ExtractedPluginDemo",
+		"-Q", "translations", "MetaRocq.Translations",
+		"-Q", "quotation/theories", "MetaRocq.Quotation",
+		"-Q", "test-suite", "MetaRocq.TestSuite",
+		"-Q", "test-suite/plugin-demo/theories", "MetaRocq.ExtractedPluginDemo",
 		"-I", "test-suite/plugin-demo",
 		"-I", "test-suite/plugin-demo/src",
-		"-R", "examples", "MetaRocq.Examples",
+		"-Q", "examples", "MetaRocq.Examples",
 	    ],
 	    "coq-lsp.args": [
-		// "-bt", // get backtraces from Rocq on errors
-		"-R", "utils/theories,MetaRocq.Utils",
-		"-R", "common/theories,MetaRocq.Common",
-		"-R", "template-rocq/theories,MetaRocq.Template",
-		"-I", "template-rocq",
-		"-I", "template-rocq/src",
-		"-R", "pcuic/theories,MetaRocq.PCUIC",
-		"-I", "pcuic",
-		"-I", "pcuic/src",
-		"-R", "template-pcuic/theories,MetaRocq.TemplatePCUIC",
-		"-R", "safechecker/theories,MetaRocq.SafeChecker",
-		"-R", "safechecker-plugin/theories,MetaRocq.SafeCheckerPlugin",
-		"-I", "safechecker-plugin",
-		"-I", "safechecker-plugin/src",
-		"-R", "erasure/theories,MetaRocq.Erasure",
-		"-R", "erasure-plugin/theories,MetaRocq.ErasurePlugin",
-		"-I", "erasure-plugin",
-		"-I", "erasure-plugin/src",
-		"-R", "translations,MetaRocq.Translations",
-		"-R", "quotation/theories,MetaRocq.Quotation",
-		"-R", "test-suite,MetaRocq.TestSuite",
-		"-R", "test-suite/plugin-demo/theories,MetaRocq.ExtractedPluginDemo",
-		"-I", "test-suite/plugin-demo",
-		"-I", "test-suite/plugin-demo/src",
-		"-R", "examples,MetaRocq.Examples",
-	    ],
+				"-Q",
+				"utils/theories,MetaRocq.Utils",
+				"-Q",
+				"common/theories,MetaRocq.Common",
+				"-Q",
+				"template-rocq/theories,MetaRocq.Template",
+				"-Q",
+				"pcuic/theories,MetaRocq.PCUIC",
+				"-Q",
+				"template-pcuic/theories,MetaRocq.TemplatePCUIC",
+				"-Q",
+				"safechecker/theories,MetaRocq.SafeChecker",
+				"-Q",
+				"safechecker-plugin/theories,MetaRocq.SafeCheckerPlugin",
+				"-Q",
+				"erasure/theories,MetaRocq.Erasure",
+				"-Q",
+				"erasure-plugin/theories,MetaRocq.ErasurePlugin",
+				"-Q",
+				"translations,MetaRocq.Translations",
+				"-Q",
+				"quotation/theories,MetaRocq.Quotation",
+				"-Q",
+				"test-suite,MetaRocq.TestSuite",
+				"-Q",
+				"test-suite/plugin-demo/theories,MetaRocq.ExtractedPluginDemo",
+				"-Q",
+				"examples,MetaRocq.Examples",
+				"--ocamlpath=template-rocq,template-rocq/src,pcuic/src,safechecker-plugin/src,erasure-plugin/src,test-suite/plugin-demo/src"
+			],
 	 // When enabled, will trim trailing whitespace when saving a file.
 	"files.trimTrailingWhitespace": true,
 	"vscoq.path": "_opam/bin/vscoqtop",
@@ -101,13 +109,53 @@
 		"**/.git": true,
 		"**/.svn": true,
 		"**/.hg": true,
-		"**/CVS": true,
 		"**/.DS_Store": true,
-		"**/Thumbs.db": true
+		"**/Thumbs.db": true,
+		"**/CVS": true
 	},
 	"coq-lsp.check_only_on_request": true,
 	"coqtop.binPath": "_opam/bin",
 	"coqtop.coqtopExe": "coqtop",
 	"coqtop.coqidetopExe": "coqidetop",
+	"cSpell.enabledFileTypes": {
+		"coq": false
+	},
+	"coq-lsp.show_universes_on_hover": false,
+	"coq-lsp.pp_type": 1,
+	"coq-lsp.heatmap.enabled": true,
+	"coq-lsp.goal_after_tactic": false,
+	"coq-lsp.messages_follow_goal": false,
+	"coq-lsp.send_perf_data": false,
+	"coq-lsp.admit_on_bad_qed": false,
+	"coq-lsp.max_errors": 1,
+	"vsrocq.args": [
+
+		// "-bt", // get backtraces from Rocq on errors
+		"-Q", "utils/theories", "MetaRocq.Utils",
+		"-Q", "common/theories", "MetaRocq.Common",
+		"-Q", "template-rocq/theories", "MetaRocq.Template",
+		"-I", "template-rocq",
+		"-I", "template-rocq/src",
+		"-Q", "pcuic/theories", "MetaRocq.PCUIC",
+		"-I", "pcuic",
+		"-I", "pcuic/src",
+		"-Q", "template-pcuic/theories", "MetaRocq.TemplatePCUIC",
+		"-Q", "safechecker/theories", "MetaRocq.SafeChecker",
+		"-Q", "safechecker-plugin/theories", "MetaRocq.SafeCheckerPlugin",
+		"-I", "safechecker-plugin",
+		"-I", "safechecker-plugin/src",
+		"-Q", "erasure/theories", "MetaRocq.Erasure",
+		"-Q", "erasure-plugin/theories", "MetaRocq.ErasurePlugin",
+		"-I", "erasure-plugin",
+		"-I", "erasure-plugin/src",
+		"-Q", "translations", "MetaRocq.Translations",
+		"-Q", "quotation/theories", "MetaRocq.Quotation",
+		"-Q", "test-suite", "MetaRocq.TestSuite",
+		"-Q", "test-suite/plugin-demo/theories", "MetaRocq.ExtractedPluginDemo",
+		"-I", "test-suite/plugin-demo",
+		"-I", "test-suite/plugin-demo/src",
+		"-Q", "examples", "MetaRocq.Examples",
+	],
+	"vsrocq.completion.enable": true,
   }
 }

Makefile

@@ -1,5 +1,5 @@
 
-all: printconf template-rocq pcuic safechecker erasure erasure-plugin safechecker-plugin quotation
+all: printconf template-rocq pcuic safechecker erasure erasure-plugin safechecker-plugin
 
 -include Makefile.conf
 
@@ -33,7 +33,7 @@ install: all
 	$(MAKE) -C pcuic install
 	$(MAKE) -C safechecker install
 	$(MAKE) -C template-pcuic install
-	$(MAKE) -C quotation install
+# 	$(MAKE) -C quotation install
 	$(MAKE) -C safechecker-plugin install
 	$(MAKE) -C erasure install
 	$(MAKE) -C erasure-plugin install
@@ -45,7 +45,7 @@ uninstall:
 	$(MAKE) -C pcuic uninstall
 	$(MAKE) -C safechecker uninstall
 	$(MAKE) -C template-pcuic uninstall
-	$(MAKE) -C quotation uninstall
+# 	$(MAKE) -C quotation uninstall
 	$(MAKE) -C safechecker-plugin uninstall
 	$(MAKE) -C erasure uninstall
 	$(MAKE) -C erasure-plugin uninstall
@@ -65,7 +65,6 @@ html: all
 		-R safechecker-plugin/theories MetaRocq.SafeCheckerPlugin \
 		-R erasure/theories MetaRocq.Erasure \
 		-R erasure-plugin/theories MetaRocq.ErasurePlugin \
-		-R quotation/theories MetaRocq.Quotation \
 		-R translations MetaRocq.Translations \
 		-R examples MetaRocq.Examples \
 		-d html */theories/*.v */theories/*/*.v translations/*.v examples/*.v
@@ -80,7 +79,7 @@ clean:
 	$(MAKE) -C safechecker clean
 	$(MAKE) -C safechecker-plugin clean
 	$(MAKE) -C template-pcuic clean
-	$(MAKE) -C quotation clean
+# 	$(MAKE) -C quotation clean
 	$(MAKE) -C erasure clean
 	$(MAKE) -C erasure-plugin clean
 	$(MAKE) -C examples clean
@@ -95,7 +94,7 @@ vos:
 	$(MAKE) -C safechecker vos
 	$(MAKE) -C safechecker-plugin vos
 	$(MAKE) -C template-pcuic vos
-	$(MAKE) -C quotation vos
+# 	$(MAKE) -C quotation vos
 	$(MAKE) -C erasure vos
 	$(MAKE) -C erasure-plugin vos
 	$(MAKE) -C translations vos
@@ -108,7 +107,7 @@ quick:
 	$(MAKE) -C safechecker quick
 	$(MAKE) -C safechecker-plugin quick
 	$(MAKE) -C template-pcuic quick
-	$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent
+# 	$(MAKE) -C quotation vos # quick # we cannot unset universe checking in 8.16 due to COQBUG(https://github.com/coq/coq/issues/17361), and quick does not buy much in quotation anyway, where almost everything is transparent
 	$(MAKE) -C erasure quick
 	$(MAKE) -C erasure-plugin quick
 	$(MAKE) -C translations quick
@@ -121,7 +120,7 @@ mrproper:
 	$(MAKE) -C safechecker mrproper
 	$(MAKE) -C safechecker-plugin mrproper
 	$(MAKE) -C template-pcuic mrproper
-	$(MAKE) -C quotation mrproper
+# 	$(MAKE) -C quotation mrproper
 	$(MAKE) -C erasure mrproper
 	$(MAKE) -C erasure-plugin mrproper
 	$(MAKE) -C examples mrproper
@@ -136,7 +135,7 @@ mrproper:
 	$(MAKE) -C safechecker .merlin
 	$(MAKE) -C safechecker-plugin .merlin
 	$(MAKE) -C template-pcuic .merlin
-	$(MAKE) -C quotation .merlin
+# 	$(MAKE) -C quotation .merlin
 	$(MAKE) -C erasure .merlin
 	$(MAKE) -C erasure-plugin .merlin
 
@@ -158,8 +157,8 @@ safechecker: pcuic
 template-pcuic: template-rocq pcuic
 	$(MAKE) -C template-pcuic
 
-quotation: template-rocq pcuic template-pcuic
-	$(MAKE) -C quotation
+# quotation: template-rocq pcuic template-pcuic
+# 	$(MAKE) -C quotation
 
 safechecker-plugin: safechecker template-pcuic
 	$(MAKE) -C safechecker-plugin
@@ -207,7 +206,9 @@ ci-quick:
 
 ci-opam:
 # Use -v so that regular output is produced
-	opam install --with-test -v -y .
+	rm -f rocq-metarocq-quotation.opam
+	opam pin add -y .
+	opam install --with-test -v -y rocq-metarocq
 	opam remove -y rocq-metarocq rocq-metarocq-template
 
 checktodos:

common/_RocqProject.in

@@ -1,7 +1,7 @@
 -R theories MetaRocq.Common
 
 theories/Primitive.v
-theories/uGraph.v
+theories/UnivConstraintType.v
 theories/config.v
 theories/Kernames.v
 theories/Universes.v
@@ -14,3 +14,15 @@ theories/EnvironmentTyping.v
 theories/EnvironmentReflect.v
 theories/EnvMap.v
 theories/Transform.v
+
+theories/LoopChecking/Common.v
+theories/LoopChecking/Interfaces.v
+theories/LoopChecking/InitialSemilattice.v
+theories/LoopChecking/HornClauses.v
+theories/LoopChecking/HornSemilatticeEquiv.v
+theories/LoopChecking/Model.v
+theories/LoopChecking/Models.v
+theories/LoopChecking/PartialLoopChecking.v
+theories/LoopChecking/Deciders.v
+theories/LoopChecking/UnivLoopChecking.v
+theories/uGraph.v