git.megacz.com Git - coq-hetmet.git/shortlog

2011-08-30	gentzen	update baked in CoqPass.hs coq-extraction-baked-in	commit \| commitdiff \| tree \| snapshot
2011-08-30	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-08-30	Adam Megacz	NaturalDeductionContext: more permutation proofs	commit \| commitdiff \| tree \| snapshot
2011-08-29	Adam Megacz	General: add ilist_ins	commit \| commitdiff \| tree \| snapshot
2011-08-29	Adam Megacz	NaturalDeductionContext: add arrangePullback	commit \| commitdiff \| tree \| snapshot
2011-08-29	Adam Megacz	HaskStrongTypes: add TBool and TInt for convenience	commit \| commitdiff \| tree \| snapshot
2011-07-04	Adam Megacz	HaskTyCons: add Int and Bool	commit \| commitdiff \| tree \| snapshot
2011-07-04	Adam Megacz	addErrorMessage: put blank lines between messages	commit \| commitdiff \| tree \| snapshot
2011-06-24	Adam Megacz	allow quantification over any tyvar in the environment...	commit \| commitdiff \| tree \| snapshot
2011-06-24	Adam Megacz	HaskFlattener: use pga_kappa a bit more, but not everyw...	commit \| commitdiff \| tree \| snapshot
2011-06-24	Adam Megacz	General.v: add list_{ins,del,take,drop}	commit \| commitdiff \| tree \| snapshot
2011-06-22	Adam Megacz	Add "atomic" component during optimization	commit \| commitdiff \| tree \| snapshot
2011-06-21	Adam Megacz	GArrowTikZ: add ability to omit rendering of assoc...	commit \| commitdiff \| tree \| snapshot
2011-06-21	Adam Megacz	GArrowSkeleton: improve optimizations	commit \| commitdiff \| tree \| snapshot
2011-06-21	Adam Megacz	update Demo.hs	commit \| commitdiff \| tree \| snapshot
2011-06-21	Adam Megacz	add crude support for flattening with LetRec and Case...	commit \| commitdiff \| tree \| snapshot
2011-06-20	Adam Megacz	update for GHC.HetMet package renaming	commit \| commitdiff \| tree \| snapshot
2011-06-19	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-06-19	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-06-19	Adam Megacz	remove magic flatten/unflatten identifiers	commit \| commitdiff \| tree \| snapshot
2011-06-19	Adam Megacz	use CoreM monad to acquire known-to-compiler identifiers	commit \| commitdiff \| tree \| snapshot
2011-06-15	Adam Megacz	Makefile: use -f when doing git pull for baked-in branch	commit \| commitdiff \| tree \| snapshot
2011-06-15	Adam Megacz	move to new normalization-based optimizer, add GArrowSk...	commit \| commitdiff \| tree \| snapshot
2011-06-15	Adam Megacz	pull baked-in branch automatically if correct coq versi...	commit \| commitdiff \| tree \| snapshot
2011-06-15	Adam Megacz	clean up demo code	commit \| commitdiff \| tree \| snapshot
2011-06-14	Adam Megacz	GArrowTikZ: support ga_loopl	commit \| commitdiff \| tree \| snapshot
2011-06-14	Adam Megacz	GArrowTikZ: draw input wires before first box, output...	commit \| commitdiff \| tree \| snapshot
2011-06-14	Adam Megacz	GArrowTikZ: render more of the structural stuff in...	commit \| commitdiff \| tree \| snapshot
2011-06-06	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-06-05	Adam Megacz	merge	commit \| commitdiff \| tree \| snapshot
2011-06-04	Adam Megacz	Unify.hs: propagate errors through the unifier	commit \| commitdiff \| tree \| snapshot
2011-06-04	Adam Megacz	GArrowPortShape: add Show instance, use new Unify.hs	commit \| commitdiff \| tree \| snapshot
2011-06-04	Adam Megacz	fix bugs in Unify.hs, store unifiers in fully-resolved...	commit \| commitdiff \| tree \| snapshot
2011-06-02	Adam Megacz	very rudimentary support for feedback in GArrowTikZ	commit \| commitdiff \| tree \| snapshot
2011-06-02	Adam Megacz	add support for flattening recursive-let	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	fix bugs in BiGArrow	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	update for new GHC coercion representation	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	remove RLet and RWhere	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	let RCut take a left environment as well	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	use -fsimpleopt-before-flatten in sanity checks	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	remove RJoin rule	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	better error reporting in coreTypeToWeakType; dont...	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	Makefile: use a for-loop to compile sanity checks	commit \| commitdiff \| tree \| snapshot
2011-05-31	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	fix bugs in BiGArrow	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	update for new GHC coercion representation	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	remove RLet and RWhere	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	let RCut take a left environment as well	commit \| commitdiff \| tree \| snapshot
2011-05-31	Adam Megacz	use -fsimpleopt-before-flatten in sanity checks	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	remove RJoin rule	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	better error reporting in coreTypeToWeakType; dont...	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	Makefile: use a for-loop to compile sanity checks	commit \| commitdiff \| tree \| snapshot
2011-05-30	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	add "sanity" target to Makefile	commit \| commitdiff \| tree \| snapshot
2011-05-30	Adam Megacz	add -fflatten and -funsafe-skolemize flags	commit \| commitdiff \| tree \| snapshot
2011-05-29	Adam Megacz	add RCut, RLeft, RRight rules	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	rename constructors of Arrange to start with A instead...	commit \| commitdiff \| tree \| snapshot
2011-05-28	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	move more arrange routines into NaturalDeductionContext	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	move Arrange into NaturalDeductionContext	commit \| commitdiff \| tree \| snapshot
2011-05-28	Adam Megacz	migrate HaskStrong away from using LeveledHaskType	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	HaskProof: make the succedent level part of the judgment	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	update Demo.hs	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	add commented-out/incomplete implementation of simplify...	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	General.v: add boolean and/or functions	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	rename variables to avoid Coq pickiness during extraction	commit \| commitdiff \| tree \| snapshot
2011-05-27	Adam Megacz	partial support for LetRec in flattener	commit \| commitdiff \| tree \| snapshot
2011-05-26	Adam Megacz	fix types of GAS_loop{l,r}	commit \| commitdiff \| tree \| snapshot
2011-05-26	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-05-26	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-05-26	Adam Megacz	add new Where rule, eliminate unnecessary ga_swaps...	commit \| commitdiff \| tree \| snapshot
2011-05-26	Adam Megacz	note to self in HaskWeak	commit \| commitdiff \| tree \| snapshot
2011-05-23	Adam Megacz	NaturalDeduction: add nd_exch	commit \| commitdiff \| tree \| snapshot
2011-05-16	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	HaskFlattener: support escapifying multi-leaf contexts	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	complete rewrite of GArrowTikZ, update examples	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	GArrowSkeleton: add some more optimization cases	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	GArrowPortShape: add detectShape	commit \| commitdiff \| tree \| snapshot
2011-05-16	Adam Megacz	Unify.hs: commenting fix	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add begin/end{preview} to tex output	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	GArrowTikZ: improve pdf page cropping	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	update demo for new more-efficient encoding of functions	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	more efficient encoding of function types	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add an identity production for Arrange	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	update demo	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add GArrowPortShape	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	add GArrowSkeleton	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	fix bug in flattener, make extensionality axiom explicit	commit \| commitdiff \| tree \| snapshot
2011-05-15	gentzen	update baked in CoqPass.hs	commit \| commitdiff \| tree \| snapshot
2011-05-15	Adam Megacz	Merge branch 'coq-extraction-baked-in' of /afs/megacz...	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	update examples	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	integrate skolemization pass with flattening	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	improve detection of type function kinds, mainly their...	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	add split_list to General.v	commit \| commitdiff \| tree \| snapshot
2011-05-14	Adam Megacz	add ToString instance for lists	commit \| commitdiff \| tree \| snapshot
2011-05-13	Adam Megacz	first draft of skolemization pass	commit \| commitdiff \| tree \| snapshot
next

Coq proofs and code accompanying the HetMet extensions for GHC

RSS Atom