1409 you can still safely apply the simplifier. |
1409 you can still safely apply the simplifier. |
1410 |
1410 |
1411 \footnote{\bf FIXME: show rewriting of cterms} |
1411 \footnote{\bf FIXME: show rewriting of cterms} |
1412 |
1412 |
1413 There is one restriction you have to keep in mind when using the simplifier: |
1413 There is one restriction you have to keep in mind when using the simplifier: |
1414 it can only deal with rewriting rules that are higher order pattern |
1414 it can only deal with rewriting rules whose left-hand sides are higher order |
1415 (see Section \ref{sec:univ} on unification). If a rule is not a pattern, |
1415 pattern (see Section \ref{sec:univ} on unification). Whether a term is a pattern |
1416 then you have to use simprocs or conversions, which we shall describe in |
1416 or not can be tested with the function @{ML_ind pattern in Pattern} from |
1417 the next section. |
1417 the structure @{ML_struct Pattern}. If a rule is not a pattern and you want |
|
1418 to use it for rewriting, then you have to use simprocs or conversions, both |
|
1419 of which we shall describe in the next section. |
1418 |
1420 |
1419 When using the simplifier, the crucial information you have to provide is |
1421 When using the simplifier, the crucial information you have to provide is |
1420 the simpset. If this information is not handled with care, then, as |
1422 the simpset. If this information is not handled with care, then, as |
1421 mentioned above, the simplifier can easily run into a loop. Therefore a good |
1423 mentioned above, the simplifier can easily run into a loop. Therefore a good |
1422 rule of thumb is to use simpsets that are as minimal as possible. It might |
1424 rule of thumb is to use simpsets that are as minimal as possible. It might |