| 2011-06-19 |
Adam Megacz | use CoreM monad to acquire known-to-compiler identifiers
|
commit | commitdiff | tree |
| 2011-06-15 |
Adam Megacz | Makefile: use -f when doing git pull for baked-in branch
|
commit | commitdiff | tree |
| 2011-06-15 |
Adam Megacz | move to new normalization-based optimizer, add GArrowSkeleto...
|
commit | commitdiff | tree |
| 2011-06-15 |
Adam Megacz | pull baked-in branch automatically if correct coq version...
|
commit | commitdiff | tree |
| 2011-06-15 |
Adam Megacz | clean up demo code
|
commit | commitdiff | tree |
| 2011-06-14 |
Adam Megacz | GArrowTikZ: support ga_loopl
|
commit | commitdiff | tree |
| 2011-06-14 |
Adam Megacz | GArrowTikZ: draw input wires before first box, output...
|
commit | commitdiff | tree |
| 2011-06-14 |
Adam Megacz | GArrowTikZ: render more of the structural stuff in...
|
commit | commitdiff | tree |
| 2011-06-04 |
Adam Megacz | Unify.hs: propagate errors through the unifier
|
commit | commitdiff | tree |
| 2011-06-04 |
Adam Megacz | GArrowPortShape: add Show instance, use new Unify.hs
|
commit | commitdiff | tree |
| 2011-06-04 |
Adam Megacz | fix bugs in Unify.hs, store unifiers in fully-resolved...
|
commit | commitdiff | tree |
| 2011-06-02 |
Adam Megacz | very rudimentary support for feedback in GArrowTikZ
|
commit | commitdiff | tree |
| 2011-06-02 |
Adam Megacz | add support for flattening recursive-let
|
commit | commitdiff | tree |
| 2011-05-31 |
Adam Megacz | fix bugs in BiGArrow
|
commit | commitdiff | tree |
| 2011-05-31 |
Adam Megacz | update for new GHC coercion representation
|
commit | commitdiff | tree |
| 2011-05-31 |
Adam Megacz | remove RLet and RWhere
|
commit | commitdiff | tree |
| 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 |
| next |
projects / coq-hetmet.git / search