Changeset 2771 for src/ASM


Ignore:
Timestamp:
Mar 3, 2013, 11:46:51 PM (7 years ago)
Author:
sacerdot
Message:

Some speed up in Policy.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2763 r2771  
    167167   #Sno_ch #So cases So
    168168   [ normalize nodelta #HS #SEQ @I
    169    | #Spol normalize nodelta #HS #SEQ #Hj
    170      whd in match (jump_expansion_internal program (S n)) in SEQ; (*80s*)
     169   | #Spol normalize nodelta #HS #SEQ #Hj whd in SEQ:(??%?);
    171170     >NEQ in SEQ; normalize nodelta cases Nno_ch in HN;
    172171     [ #HN normalize nodelta #SEQ >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? SEQ))))
     
    182181   ]
    183182 ]
    184 qed.     
     183qed.   
    185184
    186185lemma pe_step: ∀program:(Σl:list labelled_instruction.S (|l|) < 2^16 ∧ is_well_labelled_p l).
     
    193192 [ #H #Hj lapply (step_none program n) >Hj #Hn lapply (Hn (refl ??) 1) <plus_n_Sm <plus_n_O
    194193   #HSeq >HSeq lapply (Hn (refl ??) 2) <plus_n_Sm <plus_n_Sm <plus_n_O #HSSeq >HSSeq / by /
    195  | -pol #pol #Hpol #Hn >Hn in Heq; whd in match (policy_equal_opt ???);
     194 | -pol #pol #Hpol #Hn >Hn in Heq; whd in ⊢ (% → ?);
    196195   lapply (refl ? (jump_expansion_internal program (S n)))
    197196   whd in match (jump_expansion_internal program (S n)) in ⊢ (???% → ?); >Hn
     
    202201   | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
    203202     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
    204      normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq ⊢ ?; (*320s*)
     203     normalize nodelta #Teq >Teq -Teq
     204     cases (jump_expansion_step program ??) in Heq Seq ⊢ ?; (*320s*)
    205205     #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
    206206     [ normalize nodelta #HSn #Heq #Seq cases Heq
     
    536536                    lapply (measure_special program «Xp,?»)
    537537                    [ @HXp
    538                     | lapply Seq whd in match (jump_expansion_internal program (S x)); (*340s*)
     538                    | lapply Seq whd in ⊢ (??%? → ?);
    539539                      >Xeq normalize nodelta cases Xno_ch in HXp Xeq; #HXp #Xeq
    540540                      [ normalize nodelta #EQ
     
    576576            #i #Hi
    577577            inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)))
    578             [1,3: #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
     578            [1,3: #Hj whd in Geq:(??%?);
    579579              >Feq in Geq; normalize nodelta cases Fno_ch
    580580              [1,3: normalize nodelta #Heq
Note: See TracChangeset for help on using the changeset viewer.