Changeset 1246 for src/LIN


Ignore:
Timestamp:
Sep 22, 2011, 2:50:44 AM (8 years ago)
Author:
sacerdot
Message:

Yet another change to Joint.ma to accomodate all passes.
The concrete memory representation for the code of internal functions is
back, at the price of more complexity in the definition of the parameters.

Note: I do not understand any more the well_formed_P invariant for LIN code.
Moreover, the invariant does not seem to hold for code produced using LTLToLin.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1236 r1246  
    11include "joint/Joint.ma".
     2include "utilities/lists.ma".
    23
    3 definition lin_params: params
    4  mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit.
     4definition lin_params_: params_
     5 mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) unit.
    56
    6 definition lin_statement ≝ joint_statement lin_params.
     7definition pre_lin_statement ≝ joint_statement lin_params_.
    78
    89definition well_formed_P ≝
     
    1617      | None ⇒ True]].
    1718
    18 (*
    19 definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
     19definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
     20
     21(*CSC: move elsewhere, also in joint/semantics.ma *)
     22definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
     23 λA,P,c. match c with [ dp w _ ⇒ w ].
     24coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
     25
     26definition lin_params: ∀globals. params globals ≝
    2027 λglobals.
    21   mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?.
    22 (*CSC: lookup function to be implemented *)
    23 cases daemon
    24 qed.
    25 *)
     28  mk_params globals lin_params_ (Σcode:list (lin_statement globals). well_formed_P … code)
     29   (λcode:Σcode.?. λl.
     30    find ?? (λs. let 〈l',x〉 ≝ s in
     31     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
    2632
    2733definition lin_program ≝ joint_program lin_params.
Note: See TracChangeset for help on using the changeset viewer.