Changeset 1246


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.

Location:
src
Files:
5 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.
  • src/LTL/LTL.ma

    r1233 r1246  
    11include "joint/Joint.ma".
    2 include "common/Graphs.ma".
     2include alias "common/Graphs.ma".
    33
    4 definition ltl_params: params
    5  mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label.
     4definition ltl_params_: params_
     5 mk_params_ (mk_params__ unit unit unit unit registers_move Register False unit unit unit) label.
    66
    7 definition ltl_statement ≝ joint_statement ltl_params.
     7definition ltl_statement ≝ joint_statement ltl_params_.
    88
    9 (*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
    10  λglobals.
    11   mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)
     9definition ltl_params: ∀globals. params globals ≝
     10 λglobals. mk_params globals ltl_params_ (graph (ltl_statement globals)) (lookup …).
    1211
    1312definition ltl_program ≝ joint_program ltl_params.
  • src/LTL/LTLToLIN.ma

    r1236 r1246  
    22include "LIN/LIN.ma".
    33include "utilities/BitVectorTrieSet.ma".
    4 include "utilities/lists.ma".
     4include alias "common/Graphs.ma".
    55
    6 definition translate_statement: ∀globals. ltl_statement globals → lin_statement globals ≝
     6definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
    77  λglobals: list ident.
    88  λs: ltl_statement globals.
     
    1111  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
    1212  | joint_st_goto l ⇒ joint_st_goto … l
    13   | joint_st_extension ext ⇒ joint_st_extension lin_params … ext
     13  | joint_st_extension ext ⇒ joint_st_extension lin_params_ … ext
    1414  ].
    1515
     
    2222  (globals: list ident) (g: label → option (ltl_statement globals))
    2323  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    24   (generated: list ((option label) × (lin_statement globals))) (l: label) (n: nat)
    25     on n: BitVectorTrieSet 16 × (list ((option label) × (lin_statement globals))) ≝
     24  (generated: list (lin_statement globals)) (l: label) (n: nat)
     25    on n: BitVectorTrieSet 16 × (list (lin_statement globals)) ≝
    2626  match n with
    2727  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
     
    6161definition translate_graph:
    6262 ∀globals. label → nat →
    63   (label → option (ltl_statement globals)) → (label → option (lin_statement globals))
     63  (label → option (ltl_statement globals)) → codeT … (lin_params globals)
    6464
    6565 λglobals,entry,labels_upper_bound,g.
     
    7777          〈if set_member … (word_of_identifier … l) required' then Some ? l else None ?,
    7878           x〉])
    79     reversed in
    80   λl.
    81    find ?? (λs. let 〈l',x〉 ≝ s in
    82     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) final.
     79    reversed
     80  in
     81   dp … final ?.
     82(*CSC: XXXXXXX missing proof of well formedness here; but it seems false! *)
     83cases daemon
     84qed.
    8385
    8486definition translate_int_fun:
    8587 ∀globals.
    86   joint_internal_function ltl_params globals
    87    joint_internal_function lin_params globals
     88  joint_internal_function … (ltl_params globals)
     89   joint_internal_function … (lin_params globals)
    8890
    8991 λglobals,f.
    90   mk_joint_internal_function lin_params globals
     92  mk_joint_internal_function globals (lin_params globals)
    9193   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
    9294    (translate_graph globals (joint_if_entry ?? f) (nat_of_bitvector … (next_identifier … (joint_if_luniverse … f)))
    93      (joint_if_lookup ?? f))
     95     (lookup ?? (joint_if_code … f)))
    9496    ??.
    9597cases daemon (*CSC: XXXXXXXXX Dead code produced *)
  • src/joint/Joint.ma

    r1245 r1246  
    55include "common/Graphs.ma".
    66
    7 record params_: Type[1] ≝
     7record params__: Type[1] ≝
    88 { acc_a_reg: Type[0]
    99 ; acc_b_reg: Type[0]
     
    2020 }.
    2121
    22 record params: Type[1] ≝
    23  { pars_:> params_
     22record params_: Type[1] ≝
     23 { pars__:> params__
    2424 ; succ: Type[0]
    2525 }.
    2626
    27 inductive joint_instruction (p:params_) (globals: list ident): Type[0] ≝
     27inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
    2828  | joint_instr_comment: String → joint_instruction p globals
    2929  | joint_instr_cost_label: costlabel → joint_instruction p globals
     
    4343  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
    4444
    45 inductive joint_statement (p:params) (globals: list ident): Type[0] ≝
     45inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    4646  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    4747  | joint_st_goto: label → joint_statement p globals
     
    4949  | joint_st_extension: extend_statements p → joint_statement p globals.
    5050
    51 record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
     51record params (globals: list ident): Type[1] ≝
     52 { pars_:> params_
     53 ; codeT: Type[0]
     54 ; lookup: codeT → label → option (joint_statement pars_ globals)
     55 }.
     56
     57record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
    5258{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    5359  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     
    5864(*CSC: XXXXX stacksize unused for LTL-...*)
    5965  joint_if_stacksize: nat;
    60   joint_if_lookup   : label → option (joint_statement p globals);
     66  joint_if_code     : codeT … p;
    6167(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
    62   joint_if_entry    : Σl: label. joint_if_lookup l ≠ None ?;
     68  joint_if_entry    : Σl: label. lookup … joint_if_code l ≠ None ?;
    6369(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
    64   joint_if_exit     : Σl: label. joint_if_lookup l ≠ None ?
     70  joint_if_exit     : Σl: label. lookup … joint_if_code l ≠ None ?
    6571}.
    6672
     
    7076  λexit: label.
    7177  λp: joint_internal_function pars globals.
    72   λprf: joint_if_lookup … p exit ≠ None ?.
     78  λprf: lookup … (joint_if_code … p) exit ≠ None ?.
    7379   mk_joint_internal_function pars globals
    7480    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    7581    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    76     (joint_if_lookup … p) (joint_if_entry … p) (dp … exit prf).
    77 
     82    (joint_if_code … p) (joint_if_entry … p) (dp … exit prf).
    7883
    7984definition set_luniverse ≝
    80   λp:params.
    8185  λglobals  : list ident.
    82   λint_fun  : joint_internal_function p globals.
     86  λp:params globals.
     87  λint_fun  : joint_internal_function globals p.
    8388  λluniverse: universe LabelTag.
    8489  let runiverse ≝ joint_if_runiverse … int_fun in
     
    8792  let result    ≝ joint_if_result … int_fun in
    8893  let stacksize ≝ joint_if_stacksize … int_fun in
    89   let lookup    ≝ joint_if_lookup … int_fun in
     94  let code      ≝ joint_if_code … int_fun in
    9095  let entry     ≝ joint_if_entry … int_fun in
    9196  let exit      ≝ joint_if_exit … int_fun in
    92     mk_joint_internal_function … globals
     97    mk_joint_internal_function globals p
    9398      luniverse runiverse result params locals
    94       stacksize lookup entry exit.
     99      stacksize code entry exit.
    95100
    96101definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
    97102
    98 definition joint_program ≝ λp:params. program (joint_function p) nat.
     103definition joint_program ≝
     104 λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat.
    99105
    100106(****************************************************************************)
  • src/joint/semantics.ma

    r1233 r1246  
    206206axiom BadFunction : String.
    207207
    208 (*CSC: move elsewhere *)
     208(*CSC: move elsewhere, also in LIN.ma *)
    209209definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    210210 λA,P,c. match c with [ dp w _ ⇒ w ].
Note: See TracChangeset for help on using the changeset viewer.