Changeset 2286 for src/LTL


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (7 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

Location:
src/LTL
Files:
3 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1378 r2286  
    11include "LIN/joint_LTL_LIN.ma".
    22
    3 definition ltl_params_ : params_ ≝ graph_params_ ltl_lin_params__.
    4 definition ltl_params: ∀globals. params globals ≝ graph_params ltl_lin_params1.
     3definition LTL ≝ mk_graph_params LTL_LIN.
    54
    6 definition ltl_statement ≝ joint_statement ltl_params_.
    7 definition ltl_program ≝ joint_program ltl_params.
     5(* aid unification *)
     6unification hint 0 ≔
     7(*---------------*) ⊢
     8acc_a_reg LTL ≡ unit.
     9unification hint 0 ≔
     10(*---------------*) ⊢
     11acc_a_arg LTL ≡ unit.
     12unification hint 0 ≔
     13(*---------------*) ⊢
     14acc_b_reg LTL ≡ unit.
     15unification hint 0 ≔
     16(*---------------*) ⊢
     17acc_a_arg LTL ≡ unit.
     18unification hint 0 ≔
     19(*---------------*) ⊢
     20snd_arg LTL ≡ hdw_argument.
     21unification hint 0 ≔
     22(*---------------*) ⊢
     23ext_seq LTL ≡ ltl_lin_seq.
     24unification hint 0 ≔
     25(*---------------*) ⊢
     26pair_move LTL ≡ registers_move.
    827
    9 definition ltl_internal_function ≝
    10  λglobals. joint_internal_function … (ltl_params globals).
     28definition ltl_program ≝ joint_program LTL.
     29
     30coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝
     31  hdw_argument_from_byte on _b : Byte to snd_arg LTL.
     32coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝
     33  hdw_argument_from_reg on _r : Register to snd_arg LTL.
  • src/LTL/LTLToLIN.ma

    r2205 r2286  
     1include "joint/linearise.ma".
    12include "LTL/LTL.ma".
    23include "LIN/LIN.ma".
    3 include "utilities/BitVectorTrieSet.ma".
    4 include alias "common/Graphs.ma".
    5 
    6 definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
    7   λglobals: list ident.
    8   λs: ltl_statement globals.
    9   match s with
    10   [ RETURN ⇒ RETURN ??
    11   | sequential instr lbl ⇒ sequential … instr it
    12   | GOTO l ⇒ GOTO lin_params_ globals l
    13   ].
    14 
    15 (* Invariant: l has not been visited yet the very first time the
    16    function is called and in the true branch of a conditional call.
    17    This avoid useless gotos.
    18    
    19    Note: the OCaml code contains some useful explanatory comments. *)
    20 let rec visit
    21   (globals: list ident) (g: label → option (ltl_statement globals))
    22   (required: identifier_set LabelTag) (visited: identifier_set LabelTag)
    23   (generated: list (lin_statement globals)) (l: label) (n: nat)
    24     on n: identifier_set LabelTag × (list (lin_statement globals)) ≝
    25   match n with
    26   [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
    27   | S n' ⇒
    28     if l∈visited then
    29      〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
    30     else
    31      let visited' ≝ add_set ? visited l in
    32      match g l with
    33      [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
    34      | Some statement ⇒
    35        let translated_statement ≝ translate_statement globals statement in
    36        let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
    37        match statement with
    38        [ sequential instr l2 ⇒
    39          match instr with
    40          [ COND acc_a_reg l1 ⇒
    41             let 〈required', generated''〉 ≝
    42              visit globals g required visited' generated' l2 n' in
    43             let required'' ≝ add_set ? required' l1 in
    44              if l1 ∈ visited' then
    45                〈required', generated''〉
    46              else
    47                visit globals g required'' visited' generated'' l1 n'
    48          | _ ⇒ visit globals g required visited' generated' l2 n']
    49      | RETURN ⇒ 〈required, generated'〉
    50      | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
    51 [1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
    52 qed.
    53 
    54 (* CSC: The branch compression (aka tunneling) optimization is not implemented
    55    in Matita *)
    56 definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
    57 
    58 definition translate_graph:
    59  ∀globals. label → nat →
    60   (label → option (ltl_statement globals)) → codeT … (lin_params globals)
    61 
    62  λglobals,entry,labels_upper_bound,g.
    63   let g ≝ branch_compress ? g in
    64   let visited ≝ ∅ in
    65   let required ≝ { (entry) } in
    66   let 〈required', translated〉 ≝ visit globals g required visited [ ] entry labels_upper_bound in
    67   let reversed ≝ rev ? translated in
    68    map ??
    69     (λs. let 〈l,x〉 ≝ s in
    70       match l with
    71        [ None ⇒ 〈None …,x〉
    72        | Some l ⇒
    73           〈if l ∈ required' then Some ? l else None ?,
    74            x〉])
    75     reversed.
    76 
    77 definition translate_int_fun:
    78  ∀globals.
    79   joint_internal_function … (ltl_params globals) →
    80    joint_internal_function … (lin_params globals)
    81 
    82  λglobals,f.
    83   mk_joint_internal_function globals (lin_params globals)
    84    (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
    85     (translate_graph globals (joint_if_entry ?? f) (nat_of_pos … (next_identifier … (joint_if_luniverse … f)))
    86      (lookup ?? (joint_if_code … f)))
    87     ??.
    88 cases daemon (*CSC: XXXXXXXXX Dead code produced *)
    89 qed.
    904
    915definition ltl_to_lin : ltl_program → lin_program ≝
    92  λp. transform_program … p (λvarnames. transf_fundef … (translate_int_fun varnames)).
     6 λp. transform_program … p (λvarnames. transf_fundef … (linearise_int_fun LTL_LIN varnames)).
  • src/LTL/semantics.ma

    r1451 r2286  
    22include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition ltl_fullexec : fullexec io_out io_in ≝
    5  ltl_lin_fullexec … graph_succ_p (graph_fetch_statement … (ltl_lin_sem_params …))
    6   (graph_pointer_of_label …).
     4definition LTL_semantics : sem_params ≝
     5  make_sem_graph_params LTL (LTL_LIN_semantics ?).
Note: See TracChangeset for help on using the changeset viewer.