From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Fri, 25 Mar 2011 17:05:34 +0000 (-0700)
Subject: add machinery to create merged Coq script GArrow.v
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=2202d864c3a2779a33f3f7d6c411d2d16770073e

add machinery to create merged Coq script GArrow.v
---

diff --git a/Makefile b/Makefile
index 9c73d49..b8851aa 100644
--- 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
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
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.