source: src/LTL/LTLToLIN.ma @ 1783

Last change on this file since 1783 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
RevLine 
[714]1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
[728]3include "utilities/BitVectorTrieSet.ma".
[1246]4include alias "common/Graphs.ma".
[714]5
[1246]6definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
[757]7  λglobals: list ident.
8  λs: ltl_statement globals.
[1166]9  match s with
[1282]10  [ RETURN ⇒ RETURN ??
11  | sequential instr lbl ⇒ sequential … instr it
12  | GOTO l ⇒ GOTO lin_params_ globals l
[1166]13  ].
[728]14
[1233]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. *)
[1110]20let rec visit
[1236]21  (globals: list ident) (g: label → option (ltl_statement globals))
[1515]22  (required: identifier_set LabelTag) (visited: identifier_set LabelTag)
[1246]23  (generated: list (lin_statement globals)) (l: label) (n: nat)
[1515]24    on n: identifier_set LabelTag × (list (lin_statement globals)) ≝
[728]25  match n with
[1233]26  [ O ⇒ ⊥ (* CSC: Case to be made impossible; use dummy value? *)
[728]27  | S n' ⇒
[1515]28    if mem_set … visited l then
29     〈add_set ? required l, 〈None …, GOTO … globals l〉 :: generated〉
[1233]30    else
[1515]31     let visited' ≝ add_set ? visited l in
32     match g l with
[1233]33     [ None ⇒ ⊥ (* Case to be made impossible with more dependent types *)
34     | Some statement ⇒
35       let translated_statement ≝ translate_statement globals statement in
[1236]36       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
[1233]37       match statement with
[1282]38       [ sequential instr l2 ⇒
[1233]39         match instr with
[1282]40         [ COND acc_a_reg l1 ⇒
[1233]41            let 〈required', generated''〉 ≝
42             visit globals g required visited' generated' l2 n' in
[1515]43            let required'' ≝ add_set ? required' l1 in
44             if mem_set … visited' l1 then
[1233]45               〈required', generated''〉
46             else
47               visit globals g required'' visited' generated'' l1 n'
48         | _ ⇒ visit globals g required visited' generated' l2 n']
[1282]49     | RETURN ⇒ 〈required, generated'〉
50     | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
[1250]51[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
[1233]52qed.
[728]53
[1233]54(* CSC: The branch compression (aka tunneling) optimization is not implemented
55   in Matita *)
[1236]56definition branch_compress ≝ λglobals.λa:label → option (ltl_statement globals).a.
[1233]57
[1236]58definition translate_graph:
59 ∀globals. label → nat →
[1246]60  (label → option (ltl_statement globals)) → codeT … (lin_params globals)
[1236]61
62 λglobals,entry,labels_upper_bound,g.
63  let g ≝ branch_compress ? g in
[1515]64  let visited ≝ ∅ in
65  let required ≝ { (entry) } in
[1236]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 ⇒
[1515]73          〈if mem_set … required' l then Some ? l else None ?,
[1236]74           x〉])
[1379]75    reversed.
[1236]76
77definition translate_int_fun:
78 ∀globals.
[1246]79  joint_internal_function … (ltl_params globals) →
80   joint_internal_function … (lin_params globals)
[1236]81
82 λglobals,f.
[1246]83  mk_joint_internal_function globals (lin_params globals)
[1236]84   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f) it it it (joint_if_stacksize ?? f)
[1515]85    (translate_graph globals (joint_if_entry ?? f) (nat_of_pos … (next_identifier … (joint_if_luniverse … f)))
[1246]86     (lookup ?? (joint_if_code … f)))
[1236]87    ??.
88cases daemon (*CSC: XXXXXXXXX Dead code produced *)
89qed.
90
91definition ltl_to_lin : ltl_program → lin_program ≝
[1282]92 λp. transform_program … p (transf_fundef … (translate_int_fun …)).
Note: See TracBrowser for help on using the repository browser.