Changeset 1379 for src/LIN/LIN.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/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.
Note: See TracChangeset for help on using the changeset viewer.