Adam Megacz [Sun, 24 Apr 2011 09:03:40 +0000 (02:03 -0700)]
remove all admits from ProgrammingLanguage.v
Adam Megacz [Sun, 24 Apr 2011 07:04:13 +0000 (00:04 -0700)]
NaturalDeduction: add nd_swap, nd_prod_split, and some tactics
Adam Megacz [Sun, 24 Apr 2011 07:03:22 +0000 (00:03 -0700)]
add examples targets to Makefile
Adam Megacz [Sun, 24 Apr 2011 02:39:52 +0000 (19:39 -0700)]
add Unify.hs to examples
Adam Megacz [Mon, 18 Apr 2011 23:59:00 +0000 (16:59 -0700)]
speed up builds by removing some dependencies from ExtractionMain
Adam Megacz [Sat, 16 Apr 2011 22:14:58 +0000 (15:14 -0700)]
fix erroneous conclusion to penultimate lemma
Adam Megacz [Mon, 11 Apr 2011 21:46:23 +0000 (14:46 -0700)]
use the $(MAKE) variable so -j2 works
Adam Megacz [Mon, 11 Apr 2011 21:45:49 +0000 (14:45 -0700)]
Merge branches 'master' and 'master' of git.megacz.com/coq-hetmet
Adam Megacz [Mon, 11 Apr 2011 07:24:23 +0000 (07:24 +0000)]
unbreak lots more stuff
Adam Megacz [Mon, 11 Apr 2011 00:09:26 +0000 (00:09 +0000)]
uncomment some code in ProgrammingLanguage.v
Adam Megacz [Sun, 10 Apr 2011 23:34:48 +0000 (23:34 +0000)]
remove the very last admit (missing proof) from GeneralizedArrowFromReification
Adam Megacz [Sun, 10 Apr 2011 19:59:38 +0000 (19:59 +0000)]
add skeleton of GArrowTikZ
Adam Megacz [Sun, 10 Apr 2011 19:53:11 +0000 (19:53 +0000)]
separate CoqPass.hs from All.v in Makefile
Adam Megacz [Sun, 10 Apr 2011 19:51:27 +0000 (19:51 +0000)]
fix bug in GeneralizedArrowFromReification
Adam Megacz [Sun, 10 Apr 2011 19:37:59 +0000 (19:37 +0000)]
All.v: uncomment things
Adam Megacz [Sun, 10 Apr 2011 19:37:53 +0000 (19:37 +0000)]
bugfix in ReificationsIsomorphicToGeneralizedArrows
Adam Megacz [Sun, 10 Apr 2011 19:37:36 +0000 (19:37 +0000)]
add commented-out definitions for analytic proofs and cut elimination
Adam Megacz [Sun, 10 Apr 2011 11:22:43 +0000 (11:22 +0000)]
fill in lots of missing proofs
Adam Megacz [Sun, 10 Apr 2011 04:04:51 +0000 (04:04 +0000)]
update to new coq-categories, base ND_Relation on inert sequences
Adam Megacz [Sat, 9 Apr 2011 08:54:24 +0000 (08:54 +0000)]
remove notations from Preamble that come from coq-categories
Adam Megacz [Mon, 4 Apr 2011 02:53:27 +0000 (02:53 +0000)]
update to account for coq-categories changes
Adam Megacz [Sat, 2 Apr 2011 22:53:42 +0000 (22:53 +0000)]
fix Makefile bug
Adam Megacz [Sat, 2 Apr 2011 22:49:20 +0000 (15:49 -0700)]
update submodule pointer, account for changes upstream
Adam Megacz [Sat, 2 Apr 2011 22:48:01 +0000 (15:48 -0700)]
ExtractionMain: better pdflatex code output
Adam Megacz [Sat, 2 Apr 2011 20:16:22 +0000 (13:16 -0700)]
re-arrange ProgrammingLanguage
Adam Megacz [Sat, 2 Apr 2011 08:07:55 +0000 (01:07 -0700)]
add extra targets to Makefile
Adam Megacz [Sat, 2 Apr 2011 08:07:39 +0000 (01:07 -0700)]
split HaskProofCategory into two files
Adam Megacz [Fri, 1 Apr 2011 01:28:38 +0000 (18:28 -0700)]
remove unproven step1_lemma (it has a proof now)
Adam Megacz [Tue, 29 Mar 2011 18:03:35 +0000 (11:03 -0700)]
formatting fixes
Adam Megacz [Tue, 29 Mar 2011 17:52:53 +0000 (17:52 +0000)]
remove stale import from ExtractionMain
Adam Megacz [Tue, 29 Mar 2011 16:46:52 +0000 (09:46 -0700)]
lots of cleanup
Adam Megacz [Tue, 29 Mar 2011 11:20:41 +0000 (04:20 -0700)]
tweak comments in examples
Adam Megacz [Tue, 29 Mar 2011 11:15:27 +0000 (04:15 -0700)]
reorganized examples directory
Adam Megacz [Tue, 29 Mar 2011 11:13:13 +0000 (04:13 -0700)]
reorganize flattening code
Adam Megacz [Tue, 29 Mar 2011 08:05:29 +0000 (01:05 -0700)]
HaskProofCategory: more work
Adam Megacz [Tue, 29 Mar 2011 08:05:18 +0000 (01:05 -0700)]
swap the order of the hypotheses of RLet
Adam Megacz [Tue, 29 Mar 2011 08:04:22 +0000 (01:04 -0700)]
NaturalDeduction: remove unnecessary scnd_leaf, add (s)cnd_property
Adam Megacz [Mon, 28 Mar 2011 08:44:16 +0000 (01:44 -0700)]
add pushcheck
Adam Megacz [Mon, 28 Mar 2011 08:44:04 +0000 (01:44 -0700)]
replace UJudg with Arrange
Adam Megacz [Mon, 28 Mar 2011 07:17:10 +0000 (00:17 -0700)]
checkpoint
Adam Megacz [Mon, 28 Mar 2011 04:49:57 +0000 (21:49 -0700)]
checkpoint
Adam Megacz [Mon, 28 Mar 2011 00:24:18 +0000 (17:24 -0700)]
fix typo
Adam Megacz [Mon, 28 Mar 2011 00:22:44 +0000 (17:22 -0700)]
ProgrammingLanguage: more implementation
Adam Megacz [Mon, 28 Mar 2011 00:22:25 +0000 (17:22 -0700)]
HaskProofCategory: implement more
Adam Megacz [Mon, 28 Mar 2011 00:22:10 +0000 (17:22 -0700)]
remove old code from WeakFunctorCategory
Adam Megacz [Mon, 28 Mar 2011 00:21:41 +0000 (17:21 -0700)]
ReificationsIsomorphicToGeneralizedArrows: use EqDep
Adam Megacz [Mon, 28 Mar 2011 00:21:22 +0000 (17:21 -0700)]
NaturalDeduction: allow multi-rule implementations for SequentExpansion and TreeStructuralRules
Adam Megacz [Mon, 28 Mar 2011 00:20:22 +0000 (17:20 -0700)]
Merge branch 'master' of git.megacz.com/coq-hetmet
Conflicts:
src/Extraction-prefix.hs
Adam Megacz [Mon, 28 Mar 2011 00:19:42 +0000 (17:19 -0700)]
organize Extraction-prefix.hs a bit
Adam Megacz [Mon, 28 Mar 2011 00:18:07 +0000 (00:18 +0000)]
fallback plan: turn all CoreSyn coercions into unsafeCoerce
Adam Megacz [Sun, 27 Mar 2011 20:32:20 +0000 (13:32 -0700)]
change name of string-extraction placeholder
Adam Megacz [Sun, 27 Mar 2011 20:25:20 +0000 (13:25 -0700)]
remove PreCategory
Adam Megacz [Sun, 27 Mar 2011 19:37:04 +0000 (19:37 +0000)]
Merge branch 'master' of git.megacz.com/coq-hetmet
Adam Megacz [Sun, 27 Mar 2011 19:36:52 +0000 (19:36 +0000)]
uncomment more of the tutorial
Adam Megacz [Sun, 27 Mar 2011 19:27:57 +0000 (12:27 -0700)]
update submodule pointer
Adam Megacz [Sun, 27 Mar 2011 19:27:50 +0000 (12:27 -0700)]
almost finished with main theorem
Adam Megacz [Sun, 27 Mar 2011 19:21:45 +0000 (12:21 -0700)]
fix -dont-load-proofs option in Makefile
Adam Megacz [Sun, 27 Mar 2011 08:06:40 +0000 (01:06 -0700)]
checkpoint
Adam Megacz [Sun, 27 Mar 2011 04:14:45 +0000 (21:14 -0700)]
get rid of vec_{fst,snd} axioms
Adam Megacz [Sun, 27 Mar 2011 02:26:01 +0000 (19:26 -0700)]
improve error message
Adam Megacz [Sun, 27 Mar 2011 02:13:26 +0000 (19:13 -0700)]
update submodule pointer
Adam Megacz [Sun, 27 Mar 2011 02:12:46 +0000 (19:12 -0700)]
remove unnecessary comments
Adam Megacz [Sun, 27 Mar 2011 02:12:36 +0000 (19:12 -0700)]
use WeakFunctorCategory to prove GArrow/Reification isomorphism
Adam Megacz [Sat, 26 Mar 2011 09:31:25 +0000 (02:31 -0700)]
temporarily comment out
Adam Megacz [Sat, 26 Mar 2011 09:26:53 +0000 (02:26 -0700)]
more bugfixes
Adam Megacz [Sat, 26 Mar 2011 09:13:02 +0000 (02:13 -0700)]
fix {Reification,GeneralizedArrow}Category
Adam Megacz [Sat, 26 Mar 2011 09:09:35 +0000 (02:09 -0700)]
improvements to ProgrammingLanguage
Adam Megacz [Sat, 26 Mar 2011 08:40:46 +0000 (01:40 -0700)]
ProgrammingLanguage.v: add definitions for TypesL_{first,second}
Adam Megacz [Sat, 26 Mar 2011 08:40:21 +0000 (01:40 -0700)]
finish definitions for SequentCalculus, CutRule, SequentExpansion
Adam Megacz [Sat, 26 Mar 2011 08:39:46 +0000 (01:39 -0700)]
note that REmptyGroup and RLit are flat
Adam Megacz [Sat, 26 Mar 2011 08:39:15 +0000 (01:39 -0700)]
update submodule pointer
Adam Megacz [Sat, 26 Mar 2011 07:06:41 +0000 (00:06 -0700)]
update submodule pointer
Adam Megacz [Sat, 26 Mar 2011 07:02:29 +0000 (00:02 -0700)]
re-arrange NaturalDeduction
Adam Megacz [Sat, 26 Mar 2011 07:01:32 +0000 (00:01 -0700)]
change fst_zip/snd_zip to axioms
Adam Megacz [Sat, 26 Mar 2011 02:18:09 +0000 (19:18 -0700)]
fix proof that Judgments(L) is Cartesian
Adam Megacz [Fri, 25 Mar 2011 22:09:55 +0000 (15:09 -0700)]
add Concatenable, LatexMath, and fix HaskProofToLatex
Adam Megacz [Fri, 25 Mar 2011 18:22:04 +0000 (11:22 -0700)]
add ToLatex instance for TyCon/TyFun
Adam Megacz [Fri, 25 Mar 2011 18:18:04 +0000 (11:18 -0700)]
update categories submodule pointer
Adam Megacz [Fri, 25 Mar 2011 18:17:55 +0000 (11:17 -0700)]
split Extraction.v so most can be compiled with -dont-load-proofs
Adam Megacz [Fri, 25 Mar 2011 18:17:28 +0000 (11:17 -0700)]
HaskProofToLatex improvements
Adam Megacz [Fri, 25 Mar 2011 18:17:15 +0000 (11:17 -0700)]
HaskProofCategory: add commented-out-code
Adam Megacz [Fri, 25 Mar 2011 18:16:55 +0000 (11:16 -0700)]
use apply tactic in ReificationFromGeneralizedArrow; not sure why this is required
Adam Megacz [Fri, 25 Mar 2011 18:16:24 +0000 (11:16 -0700)]
ProgrammingLanguage: significant cleanups
Adam Megacz [Fri, 25 Mar 2011 18:16:00 +0000 (11:16 -0700)]
add LetRec case to Rule_Flat
Adam Megacz [Fri, 25 Mar 2011 18:15:33 +0000 (11:15 -0700)]
NaturalDeductionCategory: cleanup, add SequentCalculus and CutRule
Adam Megacz [Fri, 25 Mar 2011 18:15:01 +0000 (11:15 -0700)]
add ToLatex instance parameter to HaskStrong
Adam Megacz [Fri, 25 Mar 2011 18:14:04 +0000 (11:14 -0700)]
remove unnecessary instance from HaskStrongTypes
Adam Megacz [Fri, 25 Mar 2011 18:12:22 +0000 (11:12 -0700)]
change import order in HaskWeakVars
Adam Megacz [Fri, 25 Mar 2011 18:12:03 +0000 (11:12 -0700)]
change import order in HaskCoreToWeak
Adam Megacz [Fri, 25 Mar 2011 18:10:10 +0000 (11:10 -0700)]
add n-ary form of nd_weak
Adam Megacz [Fri, 25 Mar 2011 18:09:55 +0000 (11:09 -0700)]
add ndr_void_proofs_irrelevant
Adam Megacz [Fri, 25 Mar 2011 18:09:10 +0000 (11:09 -0700)]
move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons
Adam Megacz [Fri, 25 Mar 2011 17:07:38 +0000 (10:07 -0700)]
add kindToLatex in HaskKinds
Adam Megacz [Fri, 25 Mar 2011 17:07:20 +0000 (10:07 -0700)]
add ToLatex class, move machinery to General.v
Adam Megacz [Fri, 25 Mar 2011 17:05:34 +0000 (10:05 -0700)]
add machinery to create merged Coq script GArrow.v
Adam Megacz [Tue, 22 Mar 2011 01:27:07 +0000 (18:27 -0700)]
update categories submodule pointer
Adam Megacz [Tue, 22 Mar 2011 01:26:58 +0000 (18:26 -0700)]
proofs that Types/Judgments form an enrichment
Adam Megacz [Tue, 22 Mar 2011 01:26:27 +0000 (18:26 -0700)]
update tutorial for new GArrow classes
Adam Megacz [Mon, 21 Mar 2011 22:14:15 +0000 (15:14 -0700)]
add distinctT, InT to General
Adam Megacz [Mon, 21 Mar 2011 01:57:32 +0000 (18:57 -0700)]
add HaskXXXXCategory, generalized arrows, and reifications