Changes between Version 6 and Version 7 of Commentary/Compiler/TypeNatSolver


Ignore:
Timestamp:
Dec 9, 2012 5:26:32 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/TypeNatSolver

    v6 v7  
    129129constraints only interact with other givens.
    130130
     131=== Wanted Constraints ===
     132
     133The main purpose of the solver is to discharge ``wanted`` constraints
     134(the purpose of processing given and derived constraints is to help
     135solve existing wanted goals).   When we encounter a new wanted goals
     136we proceed as follows:
     137
     138    1. Try to solve the goal, using a few different strategies:
     139        1. Try to see if it matches the conclusion of an iff rule (`solveIff`). Aassumptions of rule become new wanted work.
     140        2. Try to see if it matches an axiom exactly (`solve`)
     141        3. Try the ordering solver for `<=` goals (`solveLeq`)
     142        4. Try to use a (possibly synthesized) assumption
     143
     144    2. If that didn't work:
     145      1. Wanted is added to the inert set
     146      2. Check to see if any of the existing wanteds in the inert set can be solved in terms of the new goal (`reExamineWanteds`)
     147      3. Generate new derived facts.
    131148
    132149
     
    136153
    137154
     155
     156
     157