Changeset 2593


Ignore:
Timestamp:
Jan 29, 2013, 12:13:39 PM (6 years ago)
Author:
mckinna
Message:

Finally chased down wicked failure to close case 1.1: of trace_compute_paid_trace_cl_other, arising from change to type of as_classify in common/StructuredTraces.ma.

Pointless case analysis on instruction in 1.1 thereby also avoided.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2575 r2593  
    229229      in
    230230        current_instruction_cost + tail_trace_cost
    231   | _ ⇒ ? (* XXX *)
     231  | _ ⇒ ? (* XXX Paolo ??? *)
    232232  ].
    233233  cases daemon
     
    362362        #costlabel #Some_lookup_opt_assm normalize nodelta #ignore
    363363        generalize in match recursive_assm;
    364         cases classifier_assm
     364        cases classifier_assm -classifier_assm #classifier_assm
    365365        [2:
    366           -classifier_assm #classifier_assm
    367366          lapply (execute_1_and_program_counter_after_other_in_lockstep … classifier_assm)
    368367          <FETCH normalize nodelta #rewrite_assm >rewrite_assm in Some_lookup_opt_assm;
     
    377376            <plus_n_O %
    378377          ]
    379         |1:
    380           whd in ⊢ (% → ?);
    381           whd in ⊢ (??%? → ?);
     378        |1:
     379                (* JHM: wicked failure because Some prevent previous unfolding of ASM_classify here *)
     380                @⊥
     381                (* *** (* previously: unnecessary case analysis on instruction *)
     382          change with ((Some ? (ASM_classify0 ?) = ?) → ?);
    382383          whd in match (current_instruction code_memory' status_start);
    383384          <FETCH generalize in match classify_assm;
     
    391392          try(#addr normalize nodelta #ignore #absurd destruct(absurd))
    392393          normalize in ignore; destruct(ignore)
    393           (* JHM: at this point previously, all the instruction-case-split-induced goals were discharged, but now... they are left outstanding? *)
    394           cases daemon (* XXX *)
    395   (* NTactic error: unify
    396      NCicUnification failure: Can't unify Or with eq
    397      in response to
    398      
    399   change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;
    400 
    401   (*change with (ASM_classify0 ? = ?) in classifier_assm;*)
    402   whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    403   whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    404   <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    405   *)
     394                *** *)
    406395        ]
    407396      ]
     
    411400  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
    412401  <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd)
    413  
    414402qed.
    415403
Note: See TracChangeset for help on using the changeset viewer.