Changeset 1071 for src/RTLabs


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (8 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1068 r1071  
    22include "RTL/RTL.ma".
    33include "common/AssocList.ma".
     4include "common/FrontEndOps.ma".
    45include "common/Graphs.ma".
    5 include "common/FrontEndOps.ma".
     6
     7axiom graph_add_lookup:
     8  ∀g: graph rtl_statement.
     9  ∀l: label.
     10  ∀s: rtl_statement.
     11  ∀to_insert: label.
     12    lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?.
    613
    714definition add_graph ≝
     
    2027    mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
    2128                             rtl_if_params' rtl_if_params' rtl_if_locals'
    22                              rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
    23                              rtl_if_exit'.
     29                             rtl_if_stacksize' rtl_if_graph' ? ?.
     30  [1: cases(rtl_if_entry')
     31      #LABEL #HYP
     32      %
     33      [1: @LABEL
     34      |2: cases(HYP)
     35          #STMT
     36          #FRST_PRF
     37          %
     38          [1: @STMT
     39          |2: <FRST_PRF @(graph_add_lookup (rtl_if_graph p) LABEL stmt)
     40          ]
     41      ]
     42 
    2443     
    2544definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
     
    316335  λsrcrs: list register.
    317336  λstart_lbl: label.
    318     match reduce_strong register destrs srcrs with
     337    match reduce_strong register register destrs srcrs with
    319338    [ dp crl_crr len_proof ⇒
    320339      let commonl ≝ \fst (\fst crl_crr) in
     
    399418      translate_move destrs srcrs
    400419    else
    401       match reduce_strong ? destrs srcrs with
     420      match reduce_strong register register destrs srcrs with
    402421      [ dp crl len_proof ⇒
    403422        let commonl ≝ \fst (\fst crl) in
     
    510529  λdest_lbl.
    511530  λdef.
    512   match reduce_strong ? srcrs1 srcrs2 with
     531  match reduce_strong register register srcrs1 srcrs2 with
    513532  [ dp reduced first_reduced_proof ⇒
    514533    let srcrsl_common ≝ \fst (\fst reduced) in
     
    517536    let srcrsr_rest ≝ \snd (\snd reduced) in
    518537    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
    519     match reduce_strong ? destrs srcrsl_common with
     538    match reduce_strong register register destrs srcrsl_common with
    520539    [ dp reduced second_reduced_proof ⇒
    521540      let destrs_common ≝ \fst (\fst reduced) in
    522541      let destrs_rest ≝ \snd (\fst reduced) in
    523       match reduce_strong ? destrs_rest srcrs_rest with
     542      match reduce_strong register register destrs_rest srcrs_rest with
    524543      [ dp reduced third_reduced_proof ⇒
    525544        let destrs_cted ≝ \fst (\fst reduced) in
     
    704723    let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
    705724    let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
    706     match reduce_strong ? tmp_srcrs1 tmp_srcrs2 with
     725    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    707726    [ dp crl their_proof ⇒
    708727      let commonl ≝ \fst (\fst crl) in
  • src/RTLabs/syntax.ma

    r1070 r1071  
    3535; f_stacksize : nat
    3636; f_graph     : graph statement
    37 ; f_entry     : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
    38 ; f_exit      : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
     37; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
     38; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
    3939}.
    4040
Note: See TracChangeset for help on using the changeset viewer.