fix test-suite

Makefile

@@ -57,8 +57,8 @@ html: all
 		-R pcuic/theories MetaCoq.PCUIC \
 		-R safechecker/theories MetaCoq.SafeChecker \
 		-R template-pcuic/theories MetaCoq.TemplatePCUIC \
-		-R safechecker-plugin/theories MetaCoq.SafeCheckerPlugin \
 		-R erasure/theories MetaCoq.Erasure \
+		-R erasure-plugin/theories MetaCoq.ErasurePlugin \
 		-R translations MetaCoq.Translations \
 		-R examples MetaCoq.Examples \
 		-d html */theories/*.v */theories/*/*.v translations/*.v examples/*.v
@@ -70,8 +70,8 @@ clean:
 	$(MAKE) -C pcuic clean
 	$(MAKE) -C safechecker clean
 	$(MAKE) -C template-pcuic clean
-	$(MAKE) -C safechecker-plugin clean
 	$(MAKE) -C erasure clean
+	$(MAKE) -C erasure-plugin clean
 	$(MAKE) -C examples clean
 	$(MAKE) -C test-suite clean
 	$(MAKE) -C translations clean
@@ -83,8 +83,8 @@ vos:
 	$(MAKE) -C pcuic vos
 	$(MAKE) -C safechecker vos
 	$(MAKE) -C template-pcuic vos
-	$(MAKE) -C safechecker-plugin vos
 	$(MAKE) -C erasure vos
+	$(MAKE) -C erasure-plugin vos
 	$(MAKE) -C translations vos
 
 quick:
@@ -94,8 +94,8 @@ quick:
 	$(MAKE) -C pcuic quick 
 	$(MAKE) -C safechecker quick
 	$(MAKE) -C template-pcuic quick 
-	$(MAKE) -C safechecker-plugin quick
 	$(MAKE) -C erasure quick
+	$(MAKE) -C erasure-plugin quick
 	$(MAKE) -C translations quick
 
 mrproper:
@@ -105,8 +105,8 @@ mrproper:
 	$(MAKE) -C pcuic mrproper
 	$(MAKE) -C safechecker mrproper
 	$(MAKE) -C template-pcuic mrproper
-	$(MAKE) -C safechecker-plugin mrproper
 	$(MAKE) -C erasure mrproper
+	$(MAKE) -C erasure-plugin mrproper
 	$(MAKE) -C examples mrproper
 	$(MAKE) -C test-suite mrproper
 	$(MAKE) -C translations mrproper
@@ -118,8 +118,8 @@ mrproper:
 	$(MAKE) -C pcuic .merlin
 	$(MAKE) -C safechecker .merlin
 	$(MAKE) -C template-pcuic .merlin
-	$(MAKE) -C safechecker-plugin .merlin
 	$(MAKE) -C erasure .merlin
+	$(MAKE) -C erasure-plugin .merin
 
 utils:
 	$(MAKE) -C utils
@@ -146,7 +146,7 @@ erasure: safechecker
 	$(MAKE) -C erasure
 
 erasure-plugin: erasure template-pcuic
-	$(MAKE) -C safechecker-plugin
+	$(MAKE) -C erasure-plugin
 
 examples: safechecker-plugin erasure-plugin
 	$(MAKE) -C examples

configure.sh

@@ -26,9 +26,9 @@ then
         ERASURE_DEPS="-R ../safechecker/theories MetaCoq.SafeChecker"
         ERASURE_PLUGIN_DEPS="-R ../template-pcuic/theories MetaCoq.TemplatePCUIC -R ../erasure/theories MetaCoq.Erasure  -I ../template-coq"
         TRANSLATIONS_DEPS="-R ../template-coq/theories MetaCoq.Template -I ../template-coq"
-        EXAMPLES_DEPS="-R ../safechecker-plugin/theories MetaCoq.SafecheckerPlugin -R ../erasure-plugin/theories MetaCoq.ErasurePlugin"
-        TEST_SUITE_DEPS="-R ../safechecker-plugin/theories MetaCoq.SafecheckerPlugin -R ../erasure-plugin/theories MetaCoq.ErasurePlugin"
-        PLUGIN_DEMO_DEPS="-R ../../template-coq/theories MetaCoq.Template -I ../../template-coq/"
+        EXAMPLES_DEPS="-R ../safechecker-plugin/theories MetaCoq.SafeCheckerPlugin -R ../erasure-plugin/theories MetaCoq.ErasurePlugin -I ../erasure-plugin/src -I ../safechecker-plugin/src/"
+        TEST_SUITE_DEPS="-R ../safechecker-plugin/theories MetaCoq.SafeCheckerPlugin -R ../erasure-plugin/theories MetaCoq.ErasurePlugin -I ../erasure-plugin/src -I ../safechecker-plugin/src/"
+        PLUGIN_DEMO_DEPS="-R ../../utils/theories MetaCoq.Utils -R ../../common/theories MetaCoq.Common -R ../../template-coq/theories MetaCoq.Template -I ../../template-coq/  -I ../../erasure-plugin/src -I ../../safechecker-plugin/src/"
         echo "METACOQ_CONFIG = local" > Makefile.conf
     else
         echo "Building MetaCoq globally (default)"

examples/metacoq_tour.v

@@ -61,7 +61,7 @@ Check PCUICSR.subject_reduction.
 (** Verified conversion and type-checking *)
 
 From MetaCoq.SafeChecker Require Import PCUICErrors PCUICWfEnv PCUICWfEnvImpl PCUICTypeChecker PCUICSafeChecker PCUICSafeRetyping.
-From MetaCoq.SafecheckerPlugin Require Import Loader.
+From MetaCoq.SafeCheckerPlugin Require Import Loader.
 Check PCUICSafeConversion.isconv_term_sound.
 Check PCUICSafeConversion.isconv_term_complete.
 

safechecker-plugin/_CoqProject.in

@@ -1,4 +1,4 @@
--R theories MetaCoq.SafecheckerPlugin
+-R theories MetaCoq.SafeCheckerPlugin
 
 
 theories/SafeTemplateChecker.v

safechecker-plugin/_PluginProject.in

@@ -1,7 +1,7 @@
-src/META.coq-metacoq-safecheckerplugin
+src/META.coq-metacoq-safechecker
 -I src
--Q src MetaCoq.SafecheckerPlugin
--R theories MetaCoq.SafecheckerPlugin
+-Q src MetaCoq.SafeCheckerPlugin
+-R theories MetaCoq.SafeCheckerPlugin
 
 # src/classes0.mli
 # src/classes0.ml

safechecker-plugin/theories/Extraction.v

@@ -2,7 +2,7 @@
 From Coq Require Import OrdersTac Ascii ExtrOcamlBasic ExtrOCamlInt63 ExtrOCamlFloats.
 From MetaCoq.Utils Require Import utils.
 From MetaCoq.SafeChecker Require Import PCUICWfEnvImpl PCUICSafeChecker PCUICSafeConversion.
-From MetaCoq.SafecheckerPlugin Require Import SafeTemplateChecker.
+From MetaCoq.SafeCheckerPlugin Require Import SafeTemplateChecker.
 
 (** * Extraction setup for the safechecker phase of MetaCoq.
 

safechecker-plugin/theories/Loader.v

@@ -1,4 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
+From MetaCoq.Template Require ExtractableLoader.
 From MetaCoq.Template Require Import Loader.
 From MetaCoq.TemplatePCUIC.PCUICTemplateMonad Require Core.
 From MetaCoq.TemplatePCUIC Require Import TemplateMonadToPCUIC.
@@ -13,3 +14,5 @@ Notation "<% x %>" := (match monad_trans return _ with monad_trans => ltac:(let
 Notation "<# x #>" := (match PCUICTemplateMonad.Core.tmQuoteRec x return _ with qx => ltac:(let p y := exact y in run_template_program qx p) end)
   (only parsing).
 Set Warnings "+notation-overridden".
+
+Declare ML Module "coq-metacoq-safechecker.plugin".

test-suite/castprop.v

@@ -1,4 +1,5 @@
-Require Import MetaCoq.Template.Loader MetaCoq.Template.utils.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import Loader.
 Require Import String.
 Set Template Cast Propositions.
 

test-suite/erasure_live_test.v

@@ -1,14 +1,16 @@
 From Coq Require Import Recdef.
 From MetaCoq.Template Require Import TemplateMonad Loader.
 (* From MetaCoq.SafeChecker Require Import SafeTemplateChecker. *)
-From MetaCoq.PCUIC Require Import PCUICEquality PCUICAst PCUICReflect PCUICSafeLemmata PCUICTyping PCUICNormal PCUICAstUtils PCUICSN TemplateToPCUIC PCUICToTemplate.
+From MetaCoq.PCUIC Require Import PCUICEquality PCUICAst PCUICReflect PCUICSafeLemmata PCUICTyping PCUICNormal PCUICAstUtils PCUICSN.
+From MetaCoq.TemplatePCUIC Require Import TemplateToPCUIC PCUICToTemplate.
 
-From MetaCoq.Erasure Require Import Erasure.
+From MetaCoq.ErasurePlugin Require Import Erasure.
 
 From Coq Require Import String.
 Local Open Scope string_scope.
 
-From MetaCoq.Template Require Import utils config.
+From MetaCoq.Utils Require Import utils bytestring.
+From MetaCoq.Common Require Import config.
 Import MCMonadNotation.
 Unset MetaCoq Debug.
 (* We're doing erasure assuming no Prop <= Type rule and lets can appear in constructor types. *)
@@ -337,7 +339,8 @@ Time Definition P_provedCopyx := Eval lazy in (test_fast cbv_provedCopyx).
 (* We don't run this one every time as it is really expensive *)
 (*Time Definition P_provedCopyxvm := Eval vm_compute in (test p_provedCopyx).*)
 
-From MetaCoq.Erasure Require Import Loader.
+From MetaCoq.ErasurePlugin Require Import Loader.
+
 MetaCoq Erase provedCopyx.
 (* 0.2s purely in the bytecode VM *)
 (*Time Definition P_provedCopyxvm' := Eval vm_compute in (test p_provedCopyx). *)

test-suite/erasure_test.v

@@ -1,4 +1,4 @@
-From MetaCoq.Erasure Require Import Loader.
+From MetaCoq.ErasurePlugin Require Import Loader.
 From MetaCoq.Template Require Import Loader.
 Set MetaCoq Timing.
 Local Open Scope string_scope.

test-suite/extractable.v

@@ -1,7 +1,11 @@
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
+From MetaCoq.Common Require Import
+     BasicAst.
 From MetaCoq.Template Require Import
-     BasicAst Ast Loader utils.
+     Ast Loader.
+From MetaCoq.Utils Require Import
+     utils.
 From MetaCoq.Template.TemplateMonad Require Import
      Common Extractable.
 

test-suite/issue28.v

@@ -1,4 +1,4 @@
-Require Import MetaCoq.Template.All MetaCoq.Template.utils.bytestring MetaCoq.Template.Pretty.
+Require Import MetaCoq.Template.All MetaCoq.Utils.bytestring MetaCoq.Template.Pretty.
 Require Export List.
 Open Scope bs_scope.
 Import ListNotations.

test-suite/modules_sections.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Template Require Import All.
+From MetaCoq.Utils Require Import utils.
 Import MCMonadNotation.
 
 

test-suite/order_rec.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 
 MetaCoq Quote Recursively Definition plus_syntax := plus.
 

test-suite/plugin-demo/theories/MyPlugin.v

@@ -1,10 +1,9 @@
 Require Import Coq.Lists.List.
-From MetaCoq.Template Require Import
-     bytestring Ast
-     Loader
-     TemplateMonad.Extractable.
+From MetaCoq.Utils Require Import bytestring.
+From MetaCoq.Common Require Import BasicAst.
+From MetaCoq.Template Require Import Ast Loader TemplateMonad.Extractable.
 Import TemplateMonad.Extractable.
-From MetaCoq Require Import Template.BasicAst Template.AstUtils Ast.
+From MetaCoq Require Import Template.AstUtils Ast.
 
 Open Scope bs_scope.
 
@@ -61,7 +60,6 @@ Definition tmResolve (nm : String.t) : TM (option kername) :=
 
 Require Import MetaCoq.ExtractedPluginDemo.Lens.
 
-
 Set Primitive Projections.
 Set Universe Polymorphism.
 

test-suite/proj.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 
 Set Primitive Projections.
 

test-suite/quotation_notations.v

@@ -1,5 +1,5 @@
 (* Some tests for the notations of quoting *)
-From MetaCoq.Template Require Import utils.bytestring.
+From MetaCoq.Utils Require Import bytestring.
 From MetaCoq.Template Require Loader.
 Local Open Scope bs_scope.
 Local Open Scope nat_scope.
@@ -19,10 +19,10 @@ Module template.
    *)
 End template.
 
-From MetaCoq.PCUIC Require Loader.
+From MetaCoq.SafeCheckerPlugin Require Loader.
 
 Module pcuic.
-  Import PCUIC.Loader.
+  Import SafeCheckerPlugin.Loader.
   Time Definition zero : nat := 0. (* 0. secs (0.u,0.s) *)
   Time Definition qzero : PCUIC.PCUICAst.term := <% zero %>. (* 0.001 secs (0.001u,0.s) *)
   Time Definition qzero_rec : PCUICProgram.pcuic_program := <# zero #>. (* 0.008 secs (0.008u,0.s) *)

test-suite/reduction_test.v

@@ -1,11 +1,15 @@
 From Coq Require Import Recdef.
-From MetaCoq.Template Require Import TemplateMonad bytestring Loader.
+From MetaCoq.Utils Require Import bytestring.
+From MetaCoq.Template Require Import TemplateMonad Loader.
 (* From MetaCoq.SafeChecker Require Import SafeTemplateChecker. *)
-From MetaCoq.PCUIC Require Import PCUICEquality PCUICAst PCUICReflect PCUICSafeLemmata PCUICTyping PCUICNormal PCUICAstUtils PCUICSN TemplateToPCUIC PCUICToTemplate.
+From MetaCoq.PCUIC Require Import PCUICEquality PCUICAst PCUICReflect PCUICSafeLemmata PCUICTyping PCUICNormal PCUICAstUtils PCUICSN.
+From MetaCoq.TemplatePCUIC Require Import TemplateToPCUIC PCUICToTemplate.
 From Coq Require Import String.
 Local Open Scope string_scope.
 
-From MetaCoq.Template Require Import utils config.
+From MetaCoq.Utils Require Import utils bytestring.
+From MetaCoq.Common Require Import config.
+
 Import MCMonadNotation.
 Unset MetaCoq Debug.
 (* We're doing erasure assuming no Prop <= Type rule and lets can appear in constructor types. *)
@@ -15,7 +19,8 @@ From MetaCoq.TestSuite Require hott_example.
 
 (* MetaCoq Quote Recursively Definition qequiv_adjointify := @isequiv_adjointify. *)
 
-From MetaCoq.SafeChecker Require Import PCUICEqualityDec PCUICWfReduction PCUICErrors PCUICSafeReduce PCUICTypeChecker PCUICSafeChecker PCUICWfEnv PCUICWfEnvImpl SafeTemplateChecker PCUICSafeConversion.
+From MetaCoq.SafeChecker Require Import PCUICEqualityDec PCUICWfReduction PCUICErrors PCUICSafeReduce PCUICTypeChecker PCUICSafeChecker PCUICWfEnv PCUICWfEnvImpl PCUICSafeConversion.
+From MetaCoq.SafeCheckerPlugin Require Import SafeTemplateChecker.
 
 #[local,program] Instance fake_abstract_guard_impl : PCUICWfEnvImpl.abstract_guard_impl :=
   {

test-suite/run_in_tactic.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 Import MCMonadNotation.
 
 Goal True.

test-suite/safechecker_test.v

@@ -1,6 +1,6 @@
 From MetaCoq.Template Require Import Loader.
-From MetaCoq.SafeChecker Require Import Loader.
-Require Import MetaCoq.SafeChecker.SafeTemplateChecker.
+From MetaCoq.SafeCheckerPlugin Require Import Loader.
+Require Import MetaCoq.SafeCheckerPlugin.SafeTemplateChecker.
 
 Local Open Scope string_scope.
 

test-suite/tmExistingInstance.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 Import MCMonadNotation.
 
 MetaCoq Run (tmLocate1 "I" >>= tmDefinition "qI").

test-suite/tmQuoteModule.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import bytestring Loader All.
+From MetaCoq.Utils Require Import bytestring.
+From MetaCoq.Template Require Import Loader All.
 Import MCMonadNotation.
 Module Foo.
     Inductive bar : Set := .

test-suite/tmVariable.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 Import MCMonadNotation.
 
 Section test.

test-suite/unfold.v

@@ -1,4 +1,5 @@
-From MetaCoq.Template Require Import utils All.
+From MetaCoq.Utils Require Import utils.
+From MetaCoq.Template Require Import All.
 Import MCMonadNotation.
 
 MetaCoq Test Quote negb.

test-suite/univ.v

@@ -149,7 +149,7 @@ Polymorphic Inductive foo3@{i j k l} (A : Type@{i}) (B : Type@{j}) : Type@{k} :=
 MetaCoq Quote Recursively Definition qfoo3 := foo3.
 Compute qfoo3.
 
-Require Import MetaCoq.Template.monad_utils. Import MCMonadNotation.
+Require Import MetaCoq.Utils.monad_utils. Import MCMonadNotation.
 Require Import MetaCoq.Template.TemplateMonad.Core.
 
 MetaCoq Run (tmQuoteInductive (cp "foo") >>= tmPrint).
@@ -162,7 +162,7 @@ MetaCoq Quote Recursively Definition qTT := TT.
 Polymorphic Inductive TT2@{i j} : Type@{j} := tt2 : Type@{i} -> TT2.
 MetaCoq Quote Recursively Definition qTT2 := TT2.
 
-Require Import MetaCoq.Template.utils.
+Require Import MetaCoq.Utils.utils.
 Require Import List. Import ListNotations.
 
 Module toto.