Changeset 2286 for src/LTL/LTLToLIN.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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)).
Note: See TracChangeset for help on using the changeset viewer.