Changeset 1379 for src/LIN/LINToASM.ma


Ignore:
Timestamp:
Oct 14, 2011, 7:44:46 PM (9 years ago)
Author:
sacerdot
Message:

Invariant on LIN code removed. In Paris it was decided that a simpler invariant
(to be added later) holds: every function in graph format starts with a
label that is equal to the name of the funciton.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1282 r1379  
    5151    set_union ? labels (statement_labels globals statement).
    5252
    53 
    5453(* dpm: A = Identifier *)
    5554definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
     
    6059  match fun_def return λ_. BitVectorTrieSet ? with
    6160  [ Internal stmts ⇒
    62       foldl ? ? (function_labels_internal globals) (set_empty ?) (pi1 … (joint_if_code ?? stmts))
     61      foldl ? ? (function_labels_internal globals) (set_empty ?) (joint_if_code ?? stmts)
    6362  | External _ ⇒ set_empty ?
    6463  ].
     
    263262  λcode: list (lin_statement globals_old).
    264263    map ? ? (build_translated_statement globals globals_old prf) code.
    265    
    266 lemma translate_code_preserves_WellFormedP:
    267   ∀globals, globals_old, prf, code.
    268     well_formed_P ? ? code → well_formed_P ? ? (translate_code globals globals_old prf code).
    269   #G #GO #P #C
    270   elim C
    271   [ normalize
    272     //
    273   | #G2 #G02 #IH (* CSC: understand here *)
    274     whd in ⊢ (% → %) whd in match build_translated_statement normalize nodelta
    275     cases (\fst G2) normalize // ]
    276 qed.
    277264
    278265definition translate_fun_def ≝
     
    284271    match def with
    285272    [ Internal int ⇒
    286       let code_proof ≝ joint_if_code … (lin_params globals_old) int in
    287       match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
    288       [ nil ⇒ λprf2.
    289       | cons hd tl ⇒ λ_.
     273      let code ≝ joint_if_code … (lin_params globals_old) int in
     274      match translate_code globals globals_old prf code with
     275      [ nil ⇒
     276      | cons hd tl ⇒
    290277        let rest ≝ 〈Some ? id, \snd hd〉 :: tl in
    291278          map ? ? (
     
    295282            | None ⇒ 〈None ?, \snd r〉
    296283            ]) rest
    297       ] (translate_code_preserves_WellFormedP globals globals_old prf (pi1 ?? code_proof) (pi2 ?? code_proof))
     284      ]
    298285    | External _ ⇒ [ ]
    299286    ].
    300 @prf2
     287cases daemon (*CSC: XXX will be fixed by an invariant later *)
    301288qed.
    302289   
Note: See TracChangeset for help on using the changeset viewer.