Commits on Dec 10, 2007
  1. @amiddelk

    Prepared gadt-branch for merge with trunk.

    A.k.a. made sure that the gadt changes do not break the main pipeline of 
    (can take a while due to regression tests)
    amiddelk committed Dec 10, 2007
Commits on Nov 14, 2007
  1. @amiddelk

    Solved some performance issues with the GADT stuff. It is still not

    fast: it takes 23 seconds to compile a derived version of the code of 
    Arthur and Doaitse. But I'm not sure anymore if the time is in the CHR 
    stuff because EHC itself takes quite some time on that kind of code as 
    well (have to do some profiling again).
    amiddelk committed Nov 14, 2007
Commits on Nov 6, 2007
  1. @amiddelk

    No commit message

    amiddelk committed Nov 6, 2007
Commits on Nov 1, 2007
  1. @amiddelk

    Thanks to a change by Atze, forward and backward reasoning (needed fo…

    …r an example in the left-corner paper of Atze and Doaitse) now seems to work (although slow :( )
    amiddelk committed Nov 1, 2007
Commits on Oct 19, 2007
  1. @amiddelk

    * Adapted the heuristics to deal with the equality reductions.

    * Direct cycles in the reduction graph are now properly handled in general; indirect cyles can only be created by the equality CHRs and are properly handled by the heuristic.
    * Added an erasure for evidence resulting from an equality proof.
    * Changed my set of rules to properly deal with scoping.
    * Disassembled the entire CHR pipeline and reconstructed a simpler pipeline just for some tests (src/chr-experiment/Main.hs)
    * Added a todo item on my whiteboard to document the CHR pipeline now I have some more knowledge of it ;-)
    And last but not least:
    * Changed the chr machinery of EH16 such that it now uses my new rules for equality proofs
    Now *all* my gadt examples type check that should type check, and minor variations on them that shouldn't indeed fail with unresolved overloading.
    So... it's finished?!
    (well... I still need to integrate it with EH versions > 16 and also think about performance because the graphs can get huge...)
    amiddelk committed Oct 19, 2007
Commits on Oct 18, 2007
  1. @amiddelk

    CHR/GADT: Generic congruence rule (using fitsIn)

    * did not have to modify the CHR machinery for that (higher-order predicates and a guard can be used as 'foreign function interface')
    It now generates the proper reduction graph for:
    Ass. A = B
    Ass. B = C
    Ass. C1 = (C2 -> A, Int)
    Prv. (C2 -> ({! i !} -> C), Int) = C1
    (using symmetry, transitivity, congruence, and a rule that assumes that left-over implicit vars can be removed)
    Todo: adapt the graph heuristics because there are now new types of reductions in the graph.
    amiddelk committed Oct 18, 2007
Commits on Oct 17, 2007
  1. @amiddelk

    * Created a plain Haskell file to experiment with the CHR machinery (…

        ** ambitions for later: turn it into an extensive test suite
    * Created a reduction rule to deal with Impl_Tail constructs 
        ** it is a bit too ad-hoc at the moment, but can deal with that later (proof of concept)
        ** still have to adapt the heuristics to deal with this specific reduction
             (maybe the heuristic can also take in account that the assumption we made on the
              context still holds)
    * Commited other changes as a precaution for changes I'm about to make.
    amiddelk committed Oct 17, 2007
Commits on Sep 17, 2007
  1. @amiddelk

    * Fixed symmetry rule, with my previous implementation it could prove…

    … any Prove equality constraint (for some reason)
    * New implementation to bring Assume equality constraints in scope (based on fitsIn)
    One issue, how to solve in combination with implicit variables:
    Assume (c_bla = C_bla)
    Prove (c_bla = i_bla -> C_bla)
    amiddelk committed Sep 17, 2007
Commits on Sep 14, 2007
  1. @amiddelk

    The three gadt examples in test/regress/16 now work.

      (changed the heuristics to select a scope rule above the symmetry rule)
    Simplified the implementation a bit.
    amiddelk committed Sep 14, 2007
  2. @amiddelk

    More work on the CHR part of the GADT implementation after obtaining …

    …a lot of information about the CHR machinery from Atze.
    Some tests:
    * test/regress/16/ crashes (multiple reductions for the same prove-constraint, have to look into that)
    * test/regress/16/ compiles (still have to check if the output is as expected)
    * test/regress/16/ compiles after adding a required signature
    amiddelk committed Sep 14, 2007
  3. @amiddelk

    First working GADT test:

    -- -------------------------
    let data Bool = True | False
        data D a = C1 a,a=Int
                 | C2 a,a=Bool
     in let x1 = C1 3
            x2 = C2 True
         in let f :: D a -> a
                f = \z -> case z of
                            C1 _ -> 3
                            C2 _ -> True
             in let y1 = f x1
                    y2 = f x2
                 in (y1,y2)
    (type signature is required)
    amiddelk committed Sep 14, 2007
  4. @amiddelk

    GADTs + CHR

    amiddelk committed Sep 14, 2007
Commits on Sep 11, 2007
  1. @amiddelk

    * Generates equality prove obligations when a match with a fixed type…

    … variable fails (either a Ty_Var
    Fixed or a TyCon "C_...")
    Last step: add CHR rules to the CHR machinery to satisfy the generated prove equalities from the 
    generated assume equalities.
    amiddelk committed Sep 11, 2007
  2. @amiddelk
  3. @amiddelk

    * Parser + abstract syntax for GADTs.

    * Generation of the appropriate type signatures of constructor/deconstructor functions for GADTs.
    * Static checks on GADT definition (kinds, cyclic definitions, etc)
    Next step: introduction of assume-equality constraints during pattern matching.
    amiddelk committed Sep 11, 2007
Commits on Sep 3, 2007
  1. @amiddelk
Commits on Aug 28, 2007
  1. @JeroenFokker

    IFL paper - submitted

    JeroenFokker committed Aug 28, 2007
Commits on Aug 27, 2007
  1. @JeroenFokker

    IFL paper: processed comments of Stefan, and some of my own.

    In particular, had a hard job to squeeze it back to 16 pages after it grow to full 17 because LNCS prohibits the use of the Times font.
    JeroenFokker committed Aug 27, 2007
Commits on Aug 14, 2007
  1. @JeroenFokker
  2. @atzedijkstra
  3. @atzedijkstra

    shuffle driven generation of agc generation of multiple modules (for …

    …less memory consuming ghc compilation), for variant 100 only, requires latest AGC
    atzedijkstra committed Aug 14, 2007
Commits on Aug 13, 2007
  1. @JeroenFokker
  2. @atzedijkstra

    literature references

    atzedijkstra committed Aug 13, 2007
  3. @atzedijkstra

    literature references

    atzedijkstra committed Aug 13, 2007
  4. @atzedijkstra

    literature references

    atzedijkstra committed Aug 13, 2007
  5. @atzedijkstra

    literature references

    atzedijkstra committed Aug 13, 2007
  6. @atzedijkstra

    literature references

    atzedijkstra committed Aug 13, 2007
  7. @atzedijkstra

    work on paper

    atzedijkstra committed Aug 13, 2007
  8. @atzedijkstra
  9. @atzedijkstra
Commits on Aug 10, 2007
  1. @JeroenFokker
  2. @JeroenFokker
  3. @atzedijkstra

    more paper last words

    atzedijkstra committed Aug 10, 2007
  4. @JeroenFokker
Commits on Aug 9, 2007
  1. @JeroenFokker