Changeset 1379 for src/LIN


Ignore:
Timestamp:
Oct 14, 2011, 7:44:46 PM (8 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.

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1378 r1379  
    55
    66definition pre_lin_statement ≝ joint_statement lin_params_.
    7 
    8 definition well_formed_P ≝
    9   λA, B: Type[0].
    10   λcode: list (option A × B).
    11     match code with
    12     [ nil ⇒ False
    13     | cons hd tl ⇒
    14       match \fst hd with
    15       [ Some lbl ⇒ False
    16       | None ⇒ True]].
    17 
    18 definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
     7definition lin_statement≝ λglobals.(option label) × (pre_lin_statement globals).
    198
    209definition lin_params: ∀globals. params globals ≝
    2110 λglobals.
    22   mk_params globals unit ltl_lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code)
    23    (λcode:Σcode.?. λl.
     11  mk_params globals unit ltl_lin_params1 (list (lin_statement globals))
     12   (λcode. λl.
    2413    find ?? (λs. let 〈l',x〉 ≝ s in
    2514     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
    2615
    2716definition lin_function ≝ λglobals. joint_function … (lin_params globals).
    28 
    2917definition lin_program ≝ joint_program lin_params.
  • 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.