Changeset 2392


Ignore:
Timestamp:
Oct 10, 2012, 5:18:15 PM (7 years ago)
Author:
campbell
Message:
Labelling translations of && and
need a lot of cost labelling to meet

criteria.

Location:
src/Clight
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2391 r2392  
    103103    〈Econdition e' e1 e2, costgen〉
    104104(* andbool and orbool are changed to conditionals to capture their
    105    short-circuiting cost difference; note that we have to return 0 or 1 *)
     105   short-circuiting cost difference; note that we have to return 0 or 1, and
     106   we get rather more cost labels than I'd like *)
    106107| Eandbool e1 e2 ⇒
    107108    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    108109    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    109     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
     110    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
     111    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
     112    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
    110113    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    111114    〈Econdition e1 e2 ef, costgen〉
    112115| Eorbool e1 e2 ⇒
    113116    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     117    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    114118    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    115     let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    116     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
     119    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
     120    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     121    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    117122    〈Econdition e1 et e2, costgen〉
    118123
  • src/Clight/labelSimulation.ma

    r2391 r2392  
    158158  normalize % // @twel_app // <(E0_right tr2) @twel_app /2/
    159159| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
    160   cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    161   cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
     160  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
     161  cases (bind_inversion ????? EX) -EX * * #EXguard #EX
    162162  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    163163  @label_gen_elim #u2
     
    165165  @add_cost_expr_elim #u4 #l4
    166166  @add_cost_expr_elim #u5 #l5
    167   [ cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    168     cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
    169     -EX1rem -EXguardrem -EX2rem
     167  @add_cost_expr_elim #u6 #l6
     168  @add_cost_expr_elim #u7 #l7
     169  [ cases (bind_inversion ????? EX) -EX * #v2 #tr2 * #EX2 #EX
     170    cases (bind_inversion ????? EX) -EX * * #EX3 #EX
    170171    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    171172    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
    172     %{(tr1'⧺(tr2'⧺E0)⧺Echarge l4)}
     173    [ %{(tr1'⧺(tr2'⧺Echarge l4)⧺Echarge l6)} | %{(tr1'⧺(tr2'⧺Echarge l5)⧺Echarge l6)} ]
    173174    whd in ⊢ (?(??%?)?); >EX1'
    174175    whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
     
    176177    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    177178    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    178     whd in EX3rem:(??%%) ⊢ %; destruct % [ 1,3: @refl | *: @twel_app // <(E0_right tr2) @twel_app /2/ ]
     179    whd in EX:(??%%) ⊢ %; destruct % [ 1,3: normalize @refl | *: @twel_app // <(E0_right tr2) @twel_app [1,3: <(E0_right tr2) @twel_app ] /2/ ]
    179180  | cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    180     %{(tr1'⧺E0⧺Echarge l5)}
     181    %{(tr1'⧺E0⧺Echarge l7)}
    181182    whd in ⊢ (?(??%?)?); >EX1'
    182183    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    183     whd in EXguardrem:(??%%); destruct % // <(E0_right tr) @twel_app /2/
     184    whd in EX:(??%%); destruct % normalize // <(E0_right tr) @twel_app /2/
    184185  ]
    185186| #ty #e1 #e2 #IH1 #IH2 #v #tr #EX #u
    186   cases (bind_inversion ????? EX) * #v1 #tr1 * #EX1 #EX1rem
    187   cases (bind_inversion ????? EX1rem) * * #EXguard #EXguardrem
     187  cases (bind_inversion ????? EX) -EX * #v1 #tr1 * #EX1 #EX
     188  cases (bind_inversion ????? EX) -EX * * #EXguard #EX
    188189  >shift_fst whd in ⊢ (??(λ_.?(??(????(?(???%)?))?)?));
    189190  @label_gen_elim #u2
     191  @label_gen_elim #u3
    190192  @add_cost_expr_elim #u4 #l4
    191   @label_gen_elim #u3
    192193  @add_cost_expr_elim #u5 #l5
     194  @add_cost_expr_elim #u6 #l6
     195  @add_cost_expr_elim #u7 #l7
    193196  [ cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    194     %{(tr1'⧺Echarge l4)}
     197    %{(tr1'⧺Echarge l7)}
    195198    whd in ⊢ (?(??%?)?); >EX1'
    196199    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    197     whd in EXguardrem:(??%%) ⊢ %; destruct % // <(E0_right tr) /3/
    198   | cases (bind_inversion ????? EXguardrem) * #v2 #tr2 * #EX2 #EX2rem
    199     cases (bind_inversion ????? EX2rem) * * #EX3 #EX3rem
     200    whd in EX:(??%%) ⊢ %; destruct normalize % // <(E0_right tr) /3/
     201  | cases (bind_inversion ????? EX) -EX * #v2 #tr2 * #EX2 #EX
     202    cases (bind_inversion ????? EX) -EX * * #EX3 #EX
    200203    cases (IH1 … EX1 u) #tr1' * #EX1' #twel1
    201     cases (IH2 … EX2 u4) #tr2' * #EX2' #twel2
    202     %{(tr1'⧺(tr2'⧺E0)⧺Echarge l5)}
     204    cases (IH2 … EX2 u2) #tr2' * #EX2' #twel2
     205    [ %{(tr1'⧺(tr2'⧺Echarge l4)⧺Echarge l6)} | %{(tr1'⧺(tr2'⧺Echarge l5)⧺Echarge l6)} ]
    203206    whd in ⊢ (?(??%?)?); >EX1'
    204     whd in ⊢ (?(??%?)?); >label_expr_type >EX2' >EXguard
     207    whd in ⊢ (?(??%?)?); >label_expr_type >EXguard
    205208    whd in ⊢ (?(??%?)?); whd in ⊢ (?(??(match % with [_⇒?|_⇒?])?)?);
    206209    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >EX2'
    207210    whd in ⊢ (?(??(match (match % with [_⇒?|_⇒?]) with [_⇒?|_⇒?])?)?); >label_expr_type >EX3
    208     whd in EX3rem:(??%%) ⊢ %; destruct % // @twel_app // <(E0_right tr2) @twel_app /2/
     211    whd in EX:(??%%) ⊢ %; destruct normalize % // @twel_app // <(E0_right tr2) @twel_app [1,3:<(E0_right tr2) @twel_app] /2/
    209212  ]
    210213| #ty #ty' #v #tr normalize /3/
Note: See TracChangeset for help on using the changeset viewer.