coq-hetmet.git
13 years agoNaturalDeduction: remove unnecessary scnd_leaf, add (s)cnd_property
Adam Megacz [Tue, 29 Mar 2011 08:04:22 +0000 (01:04 -0700)]
NaturalDeduction: remove unnecessary scnd_leaf, add (s)cnd_property

13 years agoadd pushcheck
Adam Megacz [Mon, 28 Mar 2011 08:44:16 +0000 (01:44 -0700)]
add pushcheck

13 years agoreplace UJudg with Arrange
Adam Megacz [Mon, 28 Mar 2011 08:44:04 +0000 (01:44 -0700)]
replace UJudg with Arrange

13 years agocheckpoint
Adam Megacz [Mon, 28 Mar 2011 07:17:10 +0000 (00:17 -0700)]
checkpoint

13 years agocheckpoint
Adam Megacz [Mon, 28 Mar 2011 04:49:57 +0000 (21:49 -0700)]
checkpoint

13 years agofix typo
Adam Megacz [Mon, 28 Mar 2011 00:24:18 +0000 (17:24 -0700)]
fix typo

13 years agoProgrammingLanguage: more implementation
Adam Megacz [Mon, 28 Mar 2011 00:22:44 +0000 (17:22 -0700)]
ProgrammingLanguage: more implementation

13 years agoHaskProofCategory: implement more
Adam Megacz [Mon, 28 Mar 2011 00:22:25 +0000 (17:22 -0700)]
HaskProofCategory: implement more

13 years agoremove old code from WeakFunctorCategory
Adam Megacz [Mon, 28 Mar 2011 00:22:10 +0000 (17:22 -0700)]
remove old code from WeakFunctorCategory

13 years agoReificationsIsomorphicToGeneralizedArrows: use EqDep
Adam Megacz [Mon, 28 Mar 2011 00:21:41 +0000 (17:21 -0700)]
ReificationsIsomorphicToGeneralizedArrows: use EqDep

13 years agoNaturalDeduction: allow multi-rule implementations for SequentExpansion and TreeStruc...
Adam Megacz [Mon, 28 Mar 2011 00:21:22 +0000 (17:21 -0700)]
NaturalDeduction: allow multi-rule implementations for SequentExpansion and TreeStructuralRules

13 years agoMerge branch 'master' of http://git.megacz.com/coq-hetmet
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

13 years agoorganize Extraction-prefix.hs a bit
Adam Megacz [Mon, 28 Mar 2011 00:19:42 +0000 (17:19 -0700)]
organize Extraction-prefix.hs a bit

13 years agofallback plan: turn all CoreSyn coercions into unsafeCoerce
Adam Megacz [Mon, 28 Mar 2011 00:18:07 +0000 (00:18 +0000)]
fallback plan: turn all CoreSyn coercions into unsafeCoerce

13 years agochange name of string-extraction placeholder
Adam Megacz [Sun, 27 Mar 2011 20:32:20 +0000 (13:32 -0700)]
change name of string-extraction placeholder

13 years agoremove PreCategory
Adam Megacz [Sun, 27 Mar 2011 20:25:20 +0000 (13:25 -0700)]
remove PreCategory

13 years agoMerge branch 'master' of http://git.megacz.com/coq-hetmet
Adam Megacz [Sun, 27 Mar 2011 19:37:04 +0000 (19:37 +0000)]
Merge branch 'master' of git.megacz.com/coq-hetmet

13 years agouncomment more of the tutorial
Adam Megacz [Sun, 27 Mar 2011 19:36:52 +0000 (19:36 +0000)]
uncomment more of the tutorial

13 years agoupdate submodule pointer
Adam Megacz [Sun, 27 Mar 2011 19:27:57 +0000 (12:27 -0700)]
update submodule pointer

13 years agoalmost finished with main theorem
Adam Megacz [Sun, 27 Mar 2011 19:27:50 +0000 (12:27 -0700)]
almost finished with main theorem

13 years agofix -dont-load-proofs option in Makefile
Adam Megacz [Sun, 27 Mar 2011 19:21:45 +0000 (12:21 -0700)]
fix -dont-load-proofs option in Makefile

13 years agocheckpoint
Adam Megacz [Sun, 27 Mar 2011 08:06:40 +0000 (01:06 -0700)]
checkpoint

13 years agoget rid of vec_{fst,snd} axioms
Adam Megacz [Sun, 27 Mar 2011 04:14:45 +0000 (21:14 -0700)]
get rid of vec_{fst,snd} axioms

13 years agoimprove error message
Adam Megacz [Sun, 27 Mar 2011 02:26:01 +0000 (19:26 -0700)]
improve error message

13 years agoupdate submodule pointer
Adam Megacz [Sun, 27 Mar 2011 02:13:26 +0000 (19:13 -0700)]
update submodule pointer

13 years agoremove unnecessary comments
Adam Megacz [Sun, 27 Mar 2011 02:12:46 +0000 (19:12 -0700)]
remove unnecessary comments

13 years agouse WeakFunctorCategory to prove GArrow/Reification isomorphism
Adam Megacz [Sun, 27 Mar 2011 02:12:36 +0000 (19:12 -0700)]
use WeakFunctorCategory to prove GArrow/Reification isomorphism

13 years agotemporarily comment out
Adam Megacz [Sat, 26 Mar 2011 09:31:25 +0000 (02:31 -0700)]
temporarily comment out

13 years agomore bugfixes
Adam Megacz [Sat, 26 Mar 2011 09:26:53 +0000 (02:26 -0700)]
more bugfixes

13 years agofix {Reification,GeneralizedArrow}Category
Adam Megacz [Sat, 26 Mar 2011 09:13:02 +0000 (02:13 -0700)]
fix {Reification,GeneralizedArrow}Category

13 years agoimprovements to ProgrammingLanguage
Adam Megacz [Sat, 26 Mar 2011 09:09:35 +0000 (02:09 -0700)]
improvements to ProgrammingLanguage

13 years agoProgrammingLanguage.v: add definitions for TypesL_{first,second}
Adam Megacz [Sat, 26 Mar 2011 08:40:46 +0000 (01:40 -0700)]
ProgrammingLanguage.v: add definitions for TypesL_{first,second}

13 years agofinish definitions for SequentCalculus, CutRule, SequentExpansion
Adam Megacz [Sat, 26 Mar 2011 08:40:21 +0000 (01:40 -0700)]
finish definitions for SequentCalculus, CutRule, SequentExpansion

13 years agonote that REmptyGroup and RLit are flat
Adam Megacz [Sat, 26 Mar 2011 08:39:46 +0000 (01:39 -0700)]
note that REmptyGroup and RLit are flat

13 years agoupdate submodule pointer
Adam Megacz [Sat, 26 Mar 2011 08:39:15 +0000 (01:39 -0700)]
update submodule pointer

13 years agoupdate submodule pointer
Adam Megacz [Sat, 26 Mar 2011 07:06:41 +0000 (00:06 -0700)]
update submodule pointer

13 years agore-arrange NaturalDeduction
Adam Megacz [Sat, 26 Mar 2011 07:02:29 +0000 (00:02 -0700)]
re-arrange NaturalDeduction

13 years agochange fst_zip/snd_zip to axioms
Adam Megacz [Sat, 26 Mar 2011 07:01:32 +0000 (00:01 -0700)]
change fst_zip/snd_zip to axioms

13 years agofix proof that Judgments(L) is Cartesian
Adam Megacz [Sat, 26 Mar 2011 02:18:09 +0000 (19:18 -0700)]
fix proof that Judgments(L) is Cartesian

13 years agoadd Concatenable, LatexMath, and fix HaskProofToLatex
Adam Megacz [Fri, 25 Mar 2011 22:09:55 +0000 (15:09 -0700)]
add Concatenable, LatexMath, and fix HaskProofToLatex

13 years agoadd ToLatex instance for TyCon/TyFun
Adam Megacz [Fri, 25 Mar 2011 18:22:04 +0000 (11:22 -0700)]
add ToLatex instance for TyCon/TyFun

13 years agoupdate categories submodule pointer
Adam Megacz [Fri, 25 Mar 2011 18:18:04 +0000 (11:18 -0700)]
update categories submodule pointer

13 years agosplit Extraction.v so most can be compiled with -dont-load-proofs
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

13 years agoHaskProofToLatex improvements
Adam Megacz [Fri, 25 Mar 2011 18:17:28 +0000 (11:17 -0700)]
HaskProofToLatex improvements

13 years agoHaskProofCategory: add commented-out-code
Adam Megacz [Fri, 25 Mar 2011 18:17:15 +0000 (11:17 -0700)]
HaskProofCategory: add commented-out-code

13 years agouse apply tactic in ReificationFromGeneralizedArrow; not sure why this is required
Adam Megacz [Fri, 25 Mar 2011 18:16:55 +0000 (11:16 -0700)]
use apply tactic in ReificationFromGeneralizedArrow; not sure why this is required

13 years agoProgrammingLanguage: significant cleanups
Adam Megacz [Fri, 25 Mar 2011 18:16:24 +0000 (11:16 -0700)]
ProgrammingLanguage: significant cleanups

13 years agoadd LetRec case to Rule_Flat
Adam Megacz [Fri, 25 Mar 2011 18:16:00 +0000 (11:16 -0700)]
add LetRec case to Rule_Flat

13 years agoNaturalDeductionCategory: cleanup, add SequentCalculus and CutRule
Adam Megacz [Fri, 25 Mar 2011 18:15:33 +0000 (11:15 -0700)]
NaturalDeductionCategory: cleanup, add SequentCalculus and CutRule

13 years agoadd ToLatex instance parameter to HaskStrong
Adam Megacz [Fri, 25 Mar 2011 18:15:01 +0000 (11:15 -0700)]
add ToLatex instance parameter to HaskStrong

13 years agoremove unnecessary instance from HaskStrongTypes
Adam Megacz [Fri, 25 Mar 2011 18:14:04 +0000 (11:14 -0700)]
remove unnecessary instance from HaskStrongTypes

13 years agochange import order in HaskWeakVars
Adam Megacz [Fri, 25 Mar 2011 18:12:22 +0000 (11:12 -0700)]
change import order in HaskWeakVars

13 years agochange import order in HaskCoreToWeak
Adam Megacz [Fri, 25 Mar 2011 18:12:03 +0000 (11:12 -0700)]
change import order in HaskCoreToWeak

13 years agoadd n-ary form of nd_weak
Adam Megacz [Fri, 25 Mar 2011 18:10:10 +0000 (11:10 -0700)]
add n-ary form of nd_weak

13 years agoadd ndr_void_proofs_irrelevant
Adam Megacz [Fri, 25 Mar 2011 18:09:55 +0000 (11:09 -0700)]
add ndr_void_proofs_irrelevant

13 years agomove ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons
Adam Megacz [Fri, 25 Mar 2011 18:09:10 +0000 (11:09 -0700)]
move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons

13 years agoadd kindToLatex in HaskKinds
Adam Megacz [Fri, 25 Mar 2011 17:07:38 +0000 (10:07 -0700)]
add kindToLatex in HaskKinds

13 years agoadd ToLatex class, move machinery to General.v
Adam Megacz [Fri, 25 Mar 2011 17:07:20 +0000 (10:07 -0700)]
add ToLatex class, move machinery to General.v

13 years agoadd machinery to create merged Coq script GArrow.v
Adam Megacz [Fri, 25 Mar 2011 17:05:34 +0000 (10:05 -0700)]
add machinery to create merged Coq script GArrow.v

13 years agoupdate categories submodule pointer
Adam Megacz [Tue, 22 Mar 2011 01:27:07 +0000 (18:27 -0700)]
update categories submodule pointer

13 years agoproofs that Types/Judgments form an enrichment
Adam Megacz [Tue, 22 Mar 2011 01:26:58 +0000 (18:26 -0700)]
proofs that Types/Judgments form an enrichment

13 years agoupdate tutorial for new GArrow classes
Adam Megacz [Tue, 22 Mar 2011 01:26:27 +0000 (18:26 -0700)]
update tutorial for new GArrow classes

13 years agoadd distinctT, InT to General
Adam Megacz [Mon, 21 Mar 2011 22:14:15 +0000 (15:14 -0700)]
add distinctT, InT to General

13 years agoadd HaskXXXXCategory, generalized arrows, and reifications
Adam Megacz [Mon, 21 Mar 2011 01:57:32 +0000 (18:57 -0700)]
add HaskXXXXCategory, generalized arrows, and reifications

13 years agoadd coq-categories as a submodule
Adam Megacz [Mon, 21 Mar 2011 01:57:07 +0000 (18:57 -0700)]
add coq-categories as a submodule

13 years agocomment out portions of the tutorial which do not yet work due to GHC.Prim.Any
Adam Megacz [Mon, 21 Mar 2011 00:31:03 +0000 (17:31 -0700)]
comment out portions of the tutorial which do not yet work due to GHC.Prim.Any

13 years agoMakefile update
Adam Megacz [Mon, 21 Mar 2011 00:30:40 +0000 (17:30 -0700)]
Makefile update

13 years agomake StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch
Adam Megacz [Mon, 21 Mar 2011 00:30:30 +0000 (17:30 -0700)]
make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch

13 years agoremove vec2list_injective
Adam Megacz [Sun, 20 Mar 2011 10:13:36 +0000 (03:13 -0700)]
remove vec2list_injective

13 years agoget rid of a bunch of admits in HaskStrongToProof
Adam Megacz [Sun, 20 Mar 2011 09:44:20 +0000 (02:44 -0700)]
get rid of a bunch of admits in HaskStrongToProof

13 years agorequire all branches of LetRec be at the same level in HaskProof
Adam Megacz [Sun, 20 Mar 2011 06:10:41 +0000 (23:10 -0700)]
require all branches of LetRec be at the same level in HaskProof

13 years agoadd mapOptionTree_extensional, leaves_unleaves, mapleaves
Adam Megacz [Sun, 20 Mar 2011 06:05:31 +0000 (23:05 -0700)]
add mapOptionTree_extensional, leaves_unleaves, mapleaves

13 years agoadd distinct_decidable, in_decidable to General.v
Adam Megacz [Sun, 20 Mar 2011 06:05:18 +0000 (23:05 -0700)]
add distinct_decidable, in_decidable to General.v

13 years agocheckpoint
Adam Megacz [Sat, 19 Mar 2011 23:23:03 +0000 (16:23 -0700)]
checkpoint

13 years agoimprove HaskProofToStrong, although its messier now
Adam Megacz [Sat, 19 Mar 2011 21:15:34 +0000 (14:15 -0700)]
improve HaskProofToStrong, although its messier now

13 years agoadd tracing support to Extraction-prefix.hs
Adam Megacz [Sat, 19 Mar 2011 21:15:19 +0000 (14:15 -0700)]
add tracing support to Extraction-prefix.hs

13 years agoadd mapleaves to General.v
Adam Megacz [Sat, 19 Mar 2011 21:15:18 +0000 (14:15 -0700)]
add mapleaves to General.v

13 years agochange LetRec rule to allow only a single expression in the body
Adam Megacz [Sat, 19 Mar 2011 21:15:17 +0000 (14:15 -0700)]
change LetRec rule to allow only a single expression in the body

13 years agoadd ToString instance for HaskStrong
Adam Megacz [Sat, 19 Mar 2011 21:15:15 +0000 (14:15 -0700)]
add ToString instance for HaskStrong

13 years agoadd closedNDtoNormalND to NaturalDeduction
Adam Megacz [Sat, 19 Mar 2011 21:15:14 +0000 (14:15 -0700)]
add closedNDtoNormalND to NaturalDeduction

13 years agoadd UniqMonad
Adam Megacz [Sat, 19 Mar 2011 21:15:12 +0000 (14:15 -0700)]
add UniqMonad

13 years agoadd itmap and itree_to_tree
Adam Megacz [Sat, 19 Mar 2011 21:15:11 +0000 (14:15 -0700)]
add itmap and itree_to_tree

13 years agoadd treeToString method to General
Adam Megacz [Sat, 19 Mar 2011 21:15:09 +0000 (14:15 -0700)]
add treeToString method to General

13 years agomove Prelude_error to General.v
Adam Megacz [Sat, 19 Mar 2011 21:15:05 +0000 (14:15 -0700)]
move Prelude_error to General.v

13 years agoexpand tutorial.hs, include justification for scoping changes
Adam Megacz [Wed, 16 Mar 2011 09:45:03 +0000 (02:45 -0700)]
expand tutorial.hs, include justification for scoping changes

13 years agocheck for Case that uses its binder, which we do not support
Adam Megacz [Wed, 16 Mar 2011 09:27:52 +0000 (02:27 -0700)]
check for Case that uses its binder, which we do not support

13 years agoMakefile fixes: ignore emacs droppings
Adam Megacz [Wed, 16 Mar 2011 08:55:22 +0000 (01:55 -0700)]
Makefile fixes: ignore emacs droppings

13 years agofix broken sortAlts implementation
Adam Megacz [Wed, 16 Mar 2011 08:55:07 +0000 (01:55 -0700)]
fix broken sortAlts implementation

13 years agomajor overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial
Adam Megacz [Wed, 16 Mar 2011 08:54:16 +0000 (01:54 -0700)]
major overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial

13 years agobetter variable names in HaskWeakToCore
Adam Megacz [Wed, 16 Mar 2011 08:53:36 +0000 (01:53 -0700)]
better variable names in HaskWeakToCore

13 years agorestrict RNote to one hypothesis, major additions to ProofToStrong
Adam Megacz [Wed, 16 Mar 2011 08:53:16 +0000 (01:53 -0700)]
restrict RNote to one hypothesis, major additions to ProofToStrong

13 years agoadd EGlobal/RGlobal for CoreVars whose binder we cannot see
Adam Megacz [Wed, 16 Mar 2011 08:52:39 +0000 (01:52 -0700)]
add EGlobal/RGlobal for CoreVars whose binder we cannot see

13 years agoadd crude Monad type class
Adam Megacz [Wed, 16 Mar 2011 08:50:06 +0000 (01:50 -0700)]
add crude Monad type class

13 years agofinal batch of fixups before enabling -fcoqpass
Adam Megacz [Tue, 15 Mar 2011 02:09:24 +0000 (19:09 -0700)]
final batch of fixups before enabling -fcoqpass

13 years agofix spellings in Extraction-prefix.hs, minor tweaks
Adam Megacz [Tue, 15 Mar 2011 02:02:30 +0000 (19:02 -0700)]
fix spellings in Extraction-prefix.hs, minor tweaks

13 years agoformatting
Adam Megacz [Tue, 15 Mar 2011 01:50:20 +0000 (18:50 -0700)]
formatting

13 years agochange names of Kind constructors to be more informative
Adam Megacz [Tue, 15 Mar 2011 01:27:32 +0000 (18:27 -0700)]
change names of Kind constructors to be more informative

13 years agoreshuffle definitions in an attempt to iron out inter-file dependenceies
Adam Megacz [Tue, 15 Mar 2011 00:40:24 +0000 (17:40 -0700)]
reshuffle definitions in an attempt to iron out inter-file dependenceies

13 years agoadd support for CSP in HaskCore+HaskWeak
Adam Megacz [Mon, 14 Mar 2011 23:56:06 +0000 (16:56 -0700)]
add support for CSP in HaskCore+HaskWeak

13 years agoremove dead code from HaskWeak
Adam Megacz [Mon, 14 Mar 2011 23:52:55 +0000 (16:52 -0700)]
remove dead code from HaskWeak