| 2011-05-31 |
Adam Megacz | let RCut take a left environment as well
|
commit | commitdiff | tree |
| 2011-05-31 |
Adam Megacz | use -fsimpleopt-before-flatten in sanity checks
|
commit | commitdiff | tree |
| 2011-05-31 |
Adam Megacz | remove RJoin rule
|
commit | commitdiff | tree |
| 2011-05-31 |
Adam Megacz | better error reporting in coreTypeToWeakType; dont...
|
commit | commitdiff | tree |
| 2011-05-31 |
Adam Megacz | Makefile: use a for-loop to compile sanity checks
|
commit | commitdiff | tree |
| 2011-05-30 |
Adam Megacz | add "sanity" target to Makefile
|
commit | commitdiff | tree |
| 2011-05-30 |
Adam Megacz | add -fflatten and -funsafe-skolemize flags
|
commit | commitdiff | tree |
| 2011-05-29 |
Adam Megacz | add RCut, RLeft, RRight rules
|
commit | commitdiff | tree |
| 2011-05-28 |
Adam Megacz | rename constructors of Arrange to start with A instead...
|
commit | commitdiff | tree |
| 2011-05-28 |
Adam Megacz | move more arrange routines into NaturalDeductionContext
|
commit | commitdiff | tree |
| 2011-05-28 |
Adam Megacz | move Arrange into NaturalDeductionContext
|
commit | commitdiff | tree |
| 2011-05-28 |
Adam Megacz | migrate HaskStrong away from using LeveledHaskType
|
commit | commitdiff | tree |
| 2011-05-27 |
Adam Megacz | HaskProof: make the succedent level part of the judgment
|
commit | commitdiff | tree |
| 2011-05-27 |
Adam Megacz | update Demo.hs
|
commit | commitdiff | tree |
| 2011-05-27 |
Adam Megacz | add commented-out/incomplete implementation of simplifyWeakExpr
|
commit | commitdiff | tree |
| 2011-05-27 |
Adam Megacz | General.v: add boolean and/or functions
|
commit | commitdiff | tree |
| 2011-05-27 |
Adam Megacz | rename variables to avoid Coq pickiness during extraction
|
commit | commitdiff | tree |
| 2011-05-27 |
Adam Megacz | partial support for LetRec in flattener
|
commit | commitdiff | tree |
| 2011-05-26 |
Adam Megacz | fix types of GAS_loop{l,r}
|
commit | commitdiff | tree |
| 2011-05-26 |
Adam Megacz | add new Where rule, eliminate unnecessary ga_swaps...
|
commit | commitdiff | tree |
| 2011-05-26 |
Adam Megacz | note to self in HaskWeak
|
commit | commitdiff | tree |
| 2011-05-23 |
Adam Megacz | NaturalDeduction: add nd_exch
|
commit | commitdiff | tree |
| 2011-05-16 |
Adam Megacz | HaskFlattener: support escapifying multi-leaf contexts
|
commit | commitdiff | tree |
| 2011-05-16 |
Adam Megacz | complete rewrite of GArrowTikZ, update examples
|
commit | commitdiff | tree |
| 2011-05-16 |
Adam Megacz | GArrowSkeleton: add some more optimization cases
|
commit | commitdiff | tree |
| 2011-05-16 |
Adam Megacz | GArrowPortShape: add detectShape
|
commit | commitdiff | tree |
| 2011-05-16 |
Adam Megacz | Unify.hs: commenting fix
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | add begin/end{preview} to tex output
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | GArrowTikZ: improve pdf page cropping
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | update demo for new more-efficient encoding of functions
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | more efficient encoding of function types
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | add an identity production for Arrange
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | update demo
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | add GArrowPortShape
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | add GArrowSkeleton
|
commit | commitdiff | tree |
| 2011-05-15 |
Adam Megacz | fix bug in flattener, make extensionality axiom explicit
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | update examples
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | integrate skolemization pass with flattening
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | improve detection of type function kinds, mainly their...
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | add split_list to General.v
|
commit | commitdiff | tree |
| 2011-05-14 |
Adam Megacz | add ToString instance for lists
|
commit | commitdiff | tree |
| 2011-05-13 |
Adam Megacz | first draft of skolemization pass
|
commit | commitdiff | tree |
| 2011-05-13 |
Adam Megacz | add EqDecidable instances for option and Tree
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | swap order of hypotheses in RApp to match RLet
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | rewrite {take,drop}_arg_types to avoid use of equality...
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskFlattener: represent first-order abstraction using...
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskFlattener: use ga_mk_raw
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | update PCF.v for new ECKind
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskFlattener: simplify the flattener
|
commit | commitdiff | tree |
| 2011-05-12 |
Adam Megacz | HaskStrongTypes: add {take,drop}_arg_types
|
commit | commitdiff | tree |
| 2011-05-11 |
Adam Megacz | HaskFLattener: formatting fixes and refactoring
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | start using type-family-based GArrow classes
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | have Makefile check for coq 8.3pl2-tracer
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | add examples/.build to gitignore
|
commit | commitdiff | tree |
| 2011-05-10 |
Adam Megacz | add support for flattening non-recursive Let bindings
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | move general-purpose routines from HaskFlattener to...
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | split HaskLiteralsAndTyCons into two files
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add support for hetmet_unflatten
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add Demo.hs
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | make GArrowTikZ into a module rather than a standalone...
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add support for hetmet_flatten casting variable
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | allow -fcoqpass to change the type of top-level bindings
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | use the "debug" version of Outputable for ToString...
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | change ECKind to *=>*=>*
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | abstract out the kind of environment classifiers (ECKind)
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | major improvements to flattener; almost finished now
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | allow rank-1 polymorphic types for globals
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | add PairTyCon and UnitTyCon
|
commit | commitdiff | tree |
| 2011-05-09 |
Adam Megacz | minor cleanups to Extraction-prefix.hs to eliminate...
|
commit | commitdiff | tree |
| 2011-05-05 |
Adam Megacz | further improvements to flattener
|
commit | commitdiff | tree |
| 2011-05-03 |
Adam Megacz | separate HaskProofStratified into PCF.v, HaskProgrammingLang...
|
commit | commitdiff | tree |
| 2011-04-30 |
Adam Megacz | reorganize HaskProof files
|
commit | commitdiff | tree |
| 2011-04-30 |
Adam Megacz | clean up hints for NaturalDeduction, split ProgrammingLangua...
|
commit | commitdiff | tree |
| 2011-04-29 |
Adam Megacz | remove many [[admit]]s from HaskProofFlattener.v
|
commit | commitdiff | tree |
| 2011-04-27 |
Adam Megacz | Merge branch 'master' of http://git.megacz.com/coq...
|
commit | commitdiff | tree |
| 2011-04-27 |
Adam Megacz | prove all [admit]ted lemmas in HaskStrongToProof (not...
|
commit | commitdiff | tree |
| 2011-04-26 |
Adam Megacz | add Makefile target for tikz demo
|
commit | commitdiff | tree |
| 2011-04-26 |
Adam Megacz | add examples/Makefile
|
commit | commitdiff | tree |
| 2011-04-25 |
Adam Megacz | add -fno-warn-unused-{binds,patterns} to Coq extraction
|
commit | commitdiff | tree |
| 2011-04-25 |
Adam Megacz | update GArrowTikZ.hs; still not finished, though
|
commit | commitdiff | tree |
| 2011-04-25 |
Adam Megacz | remove ClosedSIND (use "SIND []" instead)
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | remove all admits from ProgrammingLanguage.v
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | NaturalDeduction: add nd_swap, nd_prod_split, and some...
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | add examples targets to Makefile
|
commit | commitdiff | tree |
| 2011-04-24 |
Adam Megacz | add Unify.hs to examples
|
commit | commitdiff | tree |
| 2011-04-18 |
Adam Megacz | speed up builds by removing some dependencies from...
|
commit | commitdiff | tree |
| 2011-04-16 |
Adam Megacz | fix erroneous conclusion to penultimate lemma
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | use the $(MAKE) variable so -j2 works
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | Merge branches 'master' and 'master' of http://git...
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | unbreak lots more stuff
|
commit | commitdiff | tree |
| 2011-04-11 |
Adam Megacz | uncomment some code in ProgrammingLanguage.v
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | remove the very last admit (missing proof) from GeneralizedA...
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | add skeleton of GArrowTikZ
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | separate CoqPass.hs from All.v in Makefile
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | fix bug in GeneralizedArrowFromReification
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | All.v: uncomment things
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | bugfix in ReificationsIsomorphicToGeneralizedArrows
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | add commented-out definitions for analytic proofs and...
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | fill in lots of missing proofs
|
commit | commitdiff | tree |
| 2011-04-10 |
Adam Megacz | update to new coq-categories, base ND_Relation on inert...
|
commit | commitdiff | tree |
| next |
projects / coq-hetmet.git / search