diff --git a/Makefile b/Makefile index 2d2c7f2c4..48b2bba14 100644 --- a/Makefile +++ b/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 diff --git a/configure.sh b/configure.sh index 898633368..8c1006be8 100755 --- a/configure.sh +++ b/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)" diff --git a/examples/metacoq_tour.v b/examples/metacoq_tour.v index fa2d4a876..2f56ce470 100644 --- a/examples/metacoq_tour.v +++ b/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. diff --git a/safechecker-plugin/_CoqProject.in b/safechecker-plugin/_CoqProject.in index ddd32850c..d640410eb 100644 --- a/safechecker-plugin/_CoqProject.in +++ b/safechecker-plugin/_CoqProject.in @@ -1,4 +1,4 @@ --R theories MetaCoq.SafecheckerPlugin +-R theories MetaCoq.SafeCheckerPlugin theories/SafeTemplateChecker.v diff --git a/safechecker-plugin/_PluginProject.in b/safechecker-plugin/_PluginProject.in index 6a21a2999..5a2c45cb5 100644 --- a/safechecker-plugin/_PluginProject.in +++ b/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 diff --git a/safechecker-plugin/theories/Extraction.v b/safechecker-plugin/theories/Extraction.v index 4c0bcc278..6dd465243 100644 --- a/safechecker-plugin/theories/Extraction.v +++ b/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. diff --git a/safechecker-plugin/theories/Loader.v b/safechecker-plugin/theories/Loader.v index 26f40952f..66da095c8 100644 --- a/safechecker-plugin/theories/Loader.v +++ b/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". \ No newline at end of file diff --git a/test-suite/castprop.v b/test-suite/castprop.v index 185108656..f1514c150 100644 --- a/test-suite/castprop.v +++ b/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. diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v index e188f8a4c..20c37520e 100644 --- a/test-suite/erasure_live_test.v +++ b/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). *) diff --git a/test-suite/erasure_test.v b/test-suite/erasure_test.v index 143c4ae19..e9cd59265 100644 --- a/test-suite/erasure_test.v +++ b/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. diff --git a/test-suite/extractable.v b/test-suite/extractable.v index a48b86cd0..bfde3e025 100644 --- a/test-suite/extractable.v +++ b/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. diff --git a/test-suite/issue28.v b/test-suite/issue28.v index 84e7b90c3..4ed97ca0c 100644 --- a/test-suite/issue28.v +++ b/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. diff --git a/test-suite/modules_sections.v b/test-suite/modules_sections.v index 9300bec4f..2217491b8 100644 --- a/test-suite/modules_sections.v +++ b/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. diff --git a/test-suite/order_rec.v b/test-suite/order_rec.v index 827767405..b079608db 100644 --- a/test-suite/order_rec.v +++ b/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. diff --git a/test-suite/plugin-demo/theories/MyPlugin.v b/test-suite/plugin-demo/theories/MyPlugin.v index de9c9dc78..e0d3babef 100644 --- a/test-suite/plugin-demo/theories/MyPlugin.v +++ b/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. diff --git a/test-suite/proj.v b/test-suite/proj.v index cab6ec885..0273b99b5 100644 --- a/test-suite/proj.v +++ b/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. diff --git a/test-suite/quotation_notations.v b/test-suite/quotation_notations.v index 4f4ca6a4b..4696e5e23 100644 --- a/test-suite/quotation_notations.v +++ b/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) *) diff --git a/test-suite/reduction_test.v b/test-suite/reduction_test.v index ca452ee71..4e967f19b 100644 --- a/test-suite/reduction_test.v +++ b/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 := { diff --git a/test-suite/run_in_tactic.v b/test-suite/run_in_tactic.v index d5508a2cf..67ce25de0 100644 --- a/test-suite/run_in_tactic.v +++ b/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. diff --git a/test-suite/safechecker_test.v b/test-suite/safechecker_test.v index 863b120af..a506cd694 100644 --- a/test-suite/safechecker_test.v +++ b/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. diff --git a/test-suite/tmExistingInstance.v b/test-suite/tmExistingInstance.v index d1a0f099e..3992574e3 100644 --- a/test-suite/tmExistingInstance.v +++ b/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"). diff --git a/test-suite/tmQuoteModule.v b/test-suite/tmQuoteModule.v index b9cac9c10..df92ead19 100644 --- a/test-suite/tmQuoteModule.v +++ b/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 := . diff --git a/test-suite/tmVariable.v b/test-suite/tmVariable.v index f47d2e84e..80c9a1a45 100644 --- a/test-suite/tmVariable.v +++ b/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. diff --git a/test-suite/unfold.v b/test-suite/unfold.v index f5eb695c5..56513b90c 100644 --- a/test-suite/unfold.v +++ b/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. diff --git a/test-suite/univ.v b/test-suite/univ.v index 991a80ef3..c12e69a95 100644 --- a/test-suite/univ.v +++ b/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.