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


Ignore:
Timestamp:
Dec 9, 2012 5:26:32 PM (17 months 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