Changeset 2317 for src/ASM/Policy.ma


Ignore:
Timestamp:
Sep 3, 2012, 11:36:43 AM (7 years ago)
Author:
boender
Message:
  • small changes to make things compile
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2316 r2317  
    566566        ]
    567567        | @(equal_compact_unsafe_compact ? Fp)
    568           [ lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
    569             #H @H #i #Hi
     568          [1,2:
     569            [1: lapply (jump_pc_equal program (2*(|program|))) >Feq >Geq normalize nodelta
     570            #H @H ]
     571            #i #Hi
    570572            inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))
    571             [ #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
     573            [1,3: #Hj whd in match (jump_expansion_internal program (S (2*|program|))) in Geq; (*85s*)
    572574              >Feq in Geq; normalize nodelta cases Fno_ch
    573               [ normalize nodelta #Heq
     575              [1,3: normalize nodelta #Heq
    574576                >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) %
    575               | normalize nodelta cases (jump_expansion_step ???)
     577              |2,4: normalize nodelta cases (jump_expansion_step ???)
    576578                #x cases x -x #stch #sto normalize nodelta cases sto
    577                 [ normalize nodelta #_ #X destruct (X)
    578                 | -sto #stp normalize nodelta #Hst #Heq
     579                [1,3: normalize nodelta #_ #X destruct (X)
     580                |2,4: -sto #stp normalize nodelta #Hst #Heq
    579581                   <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq))))
    580582                   lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi))
    581                    lapply (Hfull i Hi ?) [>Hj %]
     583                   lapply (Hfull i Hi ?) [1,3: >Hj %]
    582584                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉)
    583585                   #fp #fj #Hfj >Hfj normalize nodelta
    584586                   cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉)
    585587                   #stp #stj cases stj normalize nodelta
    586                    [1,2: #H cases H #H2 cases H2 destruct (H2)
    587                    |3: #_ @refl
     588                   [1,2,4,5: #H cases H #H2 cases H2 destruct (H2)
     589                   |3,6: #_ @refl
    588590                   ]
    589                  ]
    590                ]
    591              | #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2:>Hj %]
    592                 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2:>Hj] %
     591                ]
    593592              ]
    594             | cases daemon (* true, but have to add to properties in some way *)
    595             | @(proj2 ?? (proj1 ?? HGp))
     593            |2,4: #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2,4:>Hj %]
     594              >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2,4:>Hj] %
    596595            ]
    597           ]
    598           | @(proj2 ?? HGp)
     596          | cases daemon (* true, but have to add to properties in some way *)
     597          | cases daemon
     598          | @(proj2 ?? (proj1 ?? HGp))
    599599          ]
    600600        ]
     601        | @(proj2 ?? HGp)
     602        ]
    601603      ]
    602604    ]
    603   | #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
    604     #x cases x -x #nch #npol normalize nodelta #Hnpol
    605     #x cases x -x #Sch #Spol normalize nodelta #HSpol
    606     cases npol in Hnpol; cases Spol in HSpol;
    607     [ #Hnpol #HSpol %1 //
    608     |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
    609       #H destruct (H)
    610     |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
    611         cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
    612         #x1 #x2
    613         cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
    614         #y1 #y2 normalize nodelta
    615         @dec_eq_jump_length
    616     ]
    617   ]
     605  ]
     606| #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n))
     607  #x cases x -x #nch #npol normalize nodelta #Hnpol
     608  #x cases x -x #Sch #Spol normalize nodelta #HSpol
     609  cases npol in Hnpol; cases Spol in HSpol;
     610  [ #Hnpol #HSpol %1 //
     611  |2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); //
     612    #H destruct (H)
     613  |4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m
     614      cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉)
     615      #x1 #x2
     616      cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉)
     617      #y1 #y2 normalize nodelta
     618      @dec_eq_jump_length
     619  ]
     620]
    618621qed.
    619622
Note: See TracChangeset for help on using the changeset viewer.