Ignore:
Timestamp:
Jun 15, 2011, 4:15:57 PM (9 years ago)
Author:
campbell
Message:

Update Cminor pretty printer and some examples.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/test/null-op.Cminor.ma

    r898 r966  
    1616  []
    1717  [pair ?? id_main_p (ASTptr Any); pair ?? id_main_q (ASTptr Any)]
    18   4 (
     18  1 (
    1919  St_cost C_cost4 (
    2020  St_seq (
    21     St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst (repr 0))))
     21    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    2222  ) (
    2323  St_seq (
    24     St_assign (ASTptr Any) id_main_q (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack (repr 0))) (Cst (ASTint I32 Unsigned) (Ointconst (repr 0))))
     24    St_assign (ASTptr Any) id_main_q (Op2 (ASTptr Any) (ASTint I32 Unsigned) (ASTptr Any) Oaddp (Cst (ASTptr Any) (Oaddrstack 0)) (Cst (ASTint I32 Unsigned) (Ointconst I32 (repr ? 0))))
    2525  ) (
    2626  St_seq (
    2727    St_ifthenelse I32 Signed (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_q)) (
    2828      St_cost C_cost2 (
    29       St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 0))))))
     29      St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
    3030      )
    3131    ) (
     
    3535  ) (
    3636  St_seq (
    37     St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) Osubpp (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_p)) (Cst (ASTint I32 Signed) (Ointconst (repr 0)))) (
     37    St_ifthenelse I32 Signed (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) (Ocmp Cgt) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Osubpp I32) (Id (ASTptr Any) id_main_p) (Id (ASTptr Any) id_main_p)) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))) (
    3838      St_cost C_cost0 (
    39       St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) Ocast8signed (Cst (ASTint I8 Signed) (Ointconst (repr 0))))))
     39      St_return (Some ? (dp ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint Signed I32) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
    4040      )
    4141    ) (
     
    4545  ) (
    4646  St_seq (
    47     St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 0))) (Cst (ASTint I8 Signed) (Ointconst (repr 1)))))
     47    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
    4848  ) (
    4949  St_seq (
    50     St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 0))) (Cst (ASTint I8 Signed) (Ointconst (repr 1)))))
     50    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
    5151  ) (
    5252  St_seq (
    53     St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst (repr 0))) (Cst (ASTint I8 Signed) (Ointconst (repr 1)))))
     53    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I8 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (Op2 (ASTint I8 Signed) (ASTint I8 Signed) (ASTint I8 Signed) Omul (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
    5454  ) (
    55   St_return (Some ? (dp ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst (repr 0)))))))
     55  St_return (Some ? (dp ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0)))))))
    5656  )
    5757  )
     
    7474.
    7575
    76 example exec: finishes_with (repr 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
     76example exec: finishes_with (repr I32 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
    7777normalize  (* you can examine the result here *)
    7878@refl
     
    8686@refl
    8787qed.
     88
Note: See TracChangeset for help on using the changeset viewer.