Solved all typing problems, typechecker seems to be correct, but slow. Rethinking the instance checks since the code seems to be too complex, hinting at bugs. It also generates errors on the wrong spots, which should be fixable easily. Bootstrap accepts 30% of its own source, after which it stalls for unknown reasons.
12/25/09: Its the quadratic time typechecker. I gather type constraints in a simple bottom up pass over the term. It introduces a large number of variables and equalities where for each equality a linear number of substitutions are made on the sequent. Moreover, instantiation constraints also introduce type unknowns. On large terms, the prover run by an ocaml interpreter just stalls. I discard type equalities, for now, from the antecedents which should, almost, halve the running time.
In the end, I want to decorate variables in the AST with their derived types. The running time should be fixable by the introduction of two type unknowns: those unknowns which should be remembered, and unknowns for intermediates, where the former are stored separately in the sequent. A nice to have for now.
No comments:
Post a Comment