Changeset 2250


Ignore:
Timestamp:
Jul 24, 2012, 7:40:20 PM (7 years ago)
Author:
campbell
Message:

Tidy up Clight to Cminor pass a bit.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r2249 r2250  
    11441144    ]
    11451145| Ssequence s1 s2 ⇒
    1146     do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
    1147     do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
     1146    do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
     1147    do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;
    11481148    OK ? «〈fgens2, St_seq s1' s2'〉, ?»
    11491149| Sifthenelse e1 s1 s2 ⇒
     
    11511151    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    11521152    [ ASTint _ _ ⇒ λe1'.
    1153          do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1;
    1154          do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2;
     1153         do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;
     1154         do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;
    11551155        OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?»
    11561156    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    11601160    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    11611161    [ ASTint _ _ ⇒ λe1'.         
    1162          (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    1163          match mklabels ul with
    1164          [ mk_Sig result Hmklabels =>
    1165               let 〈labels, ul1〉 as E1 ≝ result in
    1166               let 〈entry, exit〉 as E2 ≝ labels in
    1167               do «fgens2, s1',H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
    1168               let converted_loop ≝
    1169                St_label entry
    1170                (St_seq
    1171                  (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
    1172                  (St_label exit St_skip))
    1173               in         
    1174               OK ? «〈fgens2, converted_loop〉, ?»
    1175          ]
     1162        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     1163        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
     1164        let 〈entry, exit〉 as E2 ≝ labels in
     1165        do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;
     1166        let converted_loop ≝
     1167          St_label entry
     1168          (St_seq
     1169            (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip)
     1170            (St_label exit St_skip))
     1171        in         
     1172          OK ? «〈fgens2, converted_loop〉, ?»
    11761173    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    11771174    ] e1'
     
    11801177    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    11811178    [ ASTint _ _ ⇒ λe1'.
    1182          match mklabels ul with
    1183          [ mk_Sig result Hmklabels ⇒
    1184               let 〈labels, ul1〉 as E1 ≝ result in
    1185               let 〈entry, exit〉 as E2 ≝ labels in             
    1186               do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1;
    1187               let converted_loop ≝
    1188                St_label entry
    1189                  (St_seq
    1190                    (St_seq
    1191                      s1'
    1192                      (St_ifthenelse ?? e1' (St_goto entry) St_skip)
    1193                    )
    1194                    (St_label exit St_skip))
    1195               in
    1196               (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    1197               OK ? «〈fgens2, converted_loop〉, ?»
    1198          ]
     1179        let 〈labels, ul1〉 as E1 ≝ mklabels ul in
     1180        let 〈entry, exit〉 as E2 ≝ labels in             
     1181        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;
     1182        let converted_loop ≝
     1183          St_label entry
     1184           (St_seq
     1185             (St_seq
     1186               s1'
     1187               (St_ifthenelse ?? e1' (St_goto entry) St_skip)
     1188             )
     1189             (St_label exit St_skip))
     1190        in
     1191        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     1192        OK ? «〈fgens2, converted_loop〉, ?»
    11991193    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    12001194    ] e1'
     
    12031197    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    12041198    [ ASTint _ _ ⇒ λe1'.
    1205          match mklabels ul with
    1206          [ mk_Sig result Hmklabels ⇒
    1207               let 〈labels, ul1〉 as E ≝ result in
    1208               let 〈entry, exit〉 as E2 ≝ labels in                           
    1209               do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» flag s1;
    1210               do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) «lbls, ?» (ConvertTo entry exit) s2;
    1211               do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) «lbls, ?» (ConvertTo entry exit) s3;
    1212               (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    1213               let converted_loop ≝
    1214                 St_seq
    1215                  s1'
    1216                  (St_label entry
    1217                    (St_seq
    1218                      (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
    1219                      (St_label exit St_skip)
    1220                     ))
    1221               in
    1222              OK ? «〈fgens4, converted_loop〉, ?»
    1223         ]
     1199        let 〈labels, ul1〉 as E ≝ mklabels ul in
     1200        let 〈entry, exit〉 as E2 ≝ labels in                           
     1201        do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag s1;
     1202        do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) s2;
     1203        do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) s3;
     1204        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
     1205        let converted_loop ≝
     1206          St_seq
     1207            s1'
     1208            (St_label entry
     1209              (St_seq
     1210                (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip)
     1211                (St_label exit St_skip)
     1212            ))
     1213        in
     1214          OK ? «〈fgens4, converted_loop〉, ?»
    12241215    | _ ⇒ λ_.Error ? (msg TypeMismatch)
    12251216    ] e1'
Note: See TracChangeset for help on using the changeset viewer.