Changeset 2745 for src/ASM


Ignore:
Timestamp:
Feb 27, 2013, 10:46:05 PM (7 years ago)
Author:
sacerdot
Message:
  1. Complexity of policy computation lowered from O(n2) to O(n)
  2. Computational daemon in compiler.ma implemented
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2700 r2745  
    2222  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
    2323  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
    24   | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     24  | S m ⇒ λp.
     25          let res ≝ pi1 ?? (jump_expansion_internal program m) in
     26          let 〈no_ch,z〉 as p1 ≝ res in
    2527          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
    2628          [ None    ⇒ λp2.〈false,None ?〉
    2729          | Some op ⇒ λp2.if no_ch
    28             then pi1 ?? (jump_expansion_internal program m)
     30            then res
    2931            else pi1 ?? (jump_expansion_step program (pi1 ?? labels) «op,?»)
    3032          ] (refl … z)
     
    5557    ]
    5658  ]
    57 | cases (jump_expansion_internal program m) in p1;
     59| whd in match res in p1;
     60  cases (jump_expansion_internal program m) in p1;
    5861  #p cases p -p #p #r cases r normalize nodelta
    5962  [ #_ >p2 #ABS destruct (ABS)
Note: See TracChangeset for help on using the changeset viewer.