source: src/LTL/LTLToLIN.ma @ 2004

Last change on this file since 2004 was 1515, checked in by campbell, 10 years ago

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 3.6 KB
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3include "utilities/BitVectorTrieSet.ma".
4include alias "common/Graphs.ma".
5
6definition 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. *)
20let 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 mem_set … visited l 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 mem_set … visited' l1 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 *) ]
52qed.
53
54(* CSC: The branch compression (aka tunneling) optimization is not implemented
55   in Matita *)
56definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
57
58definition 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 mem_set … required' l then Some ? l else None ?,
74           x〉])
75    reversed.
76
77definition 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    ??.
88cases daemon (*CSC: XXXXXXXXX Dead code produced *)
89qed.
90
91definition ltl_to_lin : ltl_program → lin_program ≝
92 λp. transform_program … p (transf_fundef … (translate_int_fun …)).
Note: See TracBrowser for help on using the repository browser.