source: src/LTL/LTLToLIN.ma @ 1783

Last change on this file since 1783 was 1515, checked in by campbell, 9 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.