add machinery to create merged Coq script GArrow.v

diff --git a/Makefile b/Makefile
index 9c73d49..b8851aa 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,16 @@ src/categories/src:
 clean:
        rm -rf build
 
+merged:
+       mkdir -p .temp
+       cd src; for A in *.v; do cat $$A  | grep -v '^Require Import' > ../.temp/`echo $$A | sed s_\\\\.v_._`; done
+       cd src/categories/src; for A in *.v; do cat $$A  | grep -v '^Require Import' > ../../../.temp/`echo $$A | sed s_\\\\.v_._`; done
+       cp src/Banner.v .temp/GArrows.v
+       cd .temp; grep '^Require Import ' ../src/All.v | sed 's_Require Import _echo;echo;echo;echo;echo;cat _' | bash >> GArrows.v
+       cd .temp; time $(coqc) -dont-load-proofs -verbose GArrows.v
+       echo
+       echo COMPILATION OK
+       echo
 
 
 # this is for Adam's use only!

diff --git a/src/All.v b/src/All.v
new file mode 100644 (file)
index 0000000..52bfa4a
--- /dev/null
+++ b/src/All.v
@@ -0,0 +1,86 @@
+Require Import Preamble.
+Require Import General.
+
+Require Import HaskKinds.
+Require Import HaskLiteralsAndTyCons.
+
+Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
+Require Import HaskCore.
+
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskWeak.
+
+Require Import HaskCoreToWeak.
+
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+
+Require Import NaturalDeduction.
+Require Import NaturalDeductionToLatex.
+
+Require Import HaskProof.
+
+Require Import HaskProofToStrong.
+Require Import HaskStrongToWeak.
+Require Import HaskWeakToCore.
+(*Require Import HaskWeakToStrong.*)
+Require Import HaskStrongToProof.
+(*Require Import HaskProofToLatex.*)
+
+(*Require Import HaskStrongCategory.*)
+(*Require Import Extraction.*)
+
+Require Import Categories_ch1_3.
+Require Import Functors_ch1_4.
+Require Import Isomorphisms_ch1_5.
+Require Import ProductCategories_ch1_6_1.
+Require Import OppositeCategories_ch1_6_2.
+Require Import SliceCategories_ch1_6_4.
+
+Require Import EpicMonic_ch2_1.
+Require Import InitialTerminal_ch2_2.
+Require Import SectionRetract_ch2_4.
+
+Require Import Equalizers_ch3_3.
+Require Import CoEqualizers_ch3_4.
+
+Require Import Algebras_ch4.
+
+Require Import NaturalTransformations_ch7_4.
+Require Import NaturalIsomorphisms_ch7_5.
+Require Import FunctorCategories_ch7_7.
+
+Require Import Subcategories_ch7_1.
+
+Require Import Coherence_ch7_8.
+Require Import MonoidalCategories_ch7_8.
+
+Require Import Enrichment_ch2_8.
+Require Import RepresentableStructure_ch7_2.
+
+Require Import Yoneda_ch8.
+(*Require Import Exponentials_ch6.*)
+
+(*Require Import CategoryOfCategories_ch7_1.*)
+(*Require Import Adjoints_ch9.*)
+
+Require Import NaturalDeductionCategory.
+
+Require Import Reification.
+Require Import GeneralizedArrow.
+Require Import GeneralizedArrowFromReification.
+Require Import ReificationFromGeneralizedArrow.
+Require Import ReificationCategory.
+Require Import GeneralizedArrowCategory.
+Require Import ReificationsEquivalentToGeneralizedArrows.
+
+Require Import HaskProofCategory.
+Require Import ProgrammingLanguage.
+
+(* very slow! *)
+Require Import FreydCategories.
+Require Import Arrows.
+
+

diff --git a/src/Banner.v b/src/Banner.v
new file mode 100644 (file)
index 0000000..675d5b0
--- /dev/null
+++ b/src/Banner.v
@@ -0,0 +1,33 @@
+(***********************************************************************************************************************************
+ *
+ * This is the Coq development accompanying
+ *
+ *   __Multi-Level Programs are Generalized Arrows__
+ *
+ * Best viewed on a 132-character-wide display (use the first line of this file to size your window)
+ *
+ * This file makes extensive use of Unicode (UTF-8); please make sure your text editor supports it.
+ *
+ * Here is the version of Coq I used:
+ * 
+ *   megacz@skolem:~$ coqc -v
+ *   The Coq Proof Assistant, version 8.3pl1 (March 2011)
+ *   compiled on Mar 17 2011 21:07:25 with OCaml 3.11.2
+ *
+ * Warning: this script may take a half-hour or more to typecheck, even on a very fast machine.
+ *          It also needs about 1.5GB of ram; if you have less than that it will run unbearably slowly.
+ *
+ *  I recommend checking it using the following command:
+ *
+ *    coqc -noglob -dont-load-proofs GArrows.v
+ *
+ **********************************************************************************************************************************)
+
+Require Import Coq.Unicode.Utf8.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
+Require Setoid.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Omega.