[commit: ghc] wip/ext-solver: An operational version of SMT integration for solving linear constraints. (7879bcb)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/ext-solver
Link       : http://ghc.haskell.org/trac/ghc/changeset/7879bcb0311b4fa808f681121b9d5be23e290f01/ghc

>---------------------------------------------------------------

commit 7879bcb0311b4fa808f681121b9d5be23e290f01
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Sat May 3 18:17:32 2014 -0700

    An operational version of SMT integration for solving linear constraints.
    
    This commit implements the missing "improvement" stage.
    
    It also refactors the code in two ways:
      - Most of the work is now done in module TcTypeNats
      - It removes the intermediate `Expr` type: now we go from GHC's `Ct`
        directly to SmtLib2 s-expressions (represented by type `SExpr`).


>---------------------------------------------------------------

7879bcb0311b4fa808f681121b9d5be23e290f01
 compiler/typecheck/TcInteract.lhs |   57 ++---
 compiler/typecheck/TcSMonad.lhs   |   12 +-
 compiler/typecheck/TcTypeNats.hs  |  472 ++++++++++++++++++++++---------------
 3 files changed, 301 insertions(+), 240 deletions(-)

Diff suppressed because of size. To see it, use:

    git diff-tree --root --patch-with-stat --no-color --find-copies-harder --ignore-space-at-eol --cc 7879bcb0311b4fa808f681121b9d5be23e290f01