Ignore:
Timestamp:
Jan 4, 2012, 7:19:09 PM (8 years ago)
Author:
campbell
Message:

Update Cminor pretty printer and examples.

File:
1 edited

Legend:

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

    r966 r1633  
    11include "Cminor/semantics.ma".
    22include "common/Animation.ma".
     3
     4definition label_of_nat : nat -> identifier Label := identifier_of_nat ?.
    35
    46
     
    1517  (Some ? (ASTint I32 Signed))
    1618  []
    17   [pair ?? id_main_p (ASTptr Any); pair ?? id_main_q (ASTptr Any)]
    18   1 (
     19  [mk_Prod ?? id_main_p (ASTptr Any); mk_Prod ?? id_main_q (ASTptr Any)]
     20  (match daemon in False with [ ])
     211 (
    1922  St_cost C_cost4 (
    2023  St_seq (
    21     St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
     24    St_assign (ASTptr Any) id_main_p (Op1 (ASTint I8 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))
    2225  ) (
    2326  St_seq (
     
    2730    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)) (
    2831      St_cost C_cost2 (
    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))))))
     32      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
    3033      )
    3134    ) (
     
    3740    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)))) (
    3841      St_cost C_cost0 (
    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))))))
     42      St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op1 (ASTint I8 Signed) (ASTint I32 Signed) (Ocastint ????) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 0))))))
    4043      )
    4144    ) (
     
    4548  ) (
    4649  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 I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
     50    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    4851  ) (
    4952  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 I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
     53    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Oaddp (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    5154  ) (
    5255  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 I8 (repr ? 0))) (Cst (ASTint I8 Signed) (Ointconst I8 (repr ? 1)))))
     56    St_assign (ASTptr Any) id_main_p (Op2 (ASTptr Any) (ASTint I32 Signed) (ASTptr Any) Osubpi (Id (ASTptr Any) id_main_p) (Op2 (ASTint I32 Signed) (ASTint I32 Signed) (ASTint I32 Signed) Omul (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0))) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 1)))))
    5457  ) (
    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)))))))
     58  St_return (Some ? (mk_DPair ?? (ASTint I32 Signed) (Op2 (ASTptr Any) (ASTptr Any) (ASTint I32 Signed) (Ocmpp Ceq) (Id (ASTptr Any) id_main_p) (Op1 (ASTint I32 Signed) (ASTptr Any) (Optrofint ?? Any) (Cst (ASTint I32 Signed) (Ointconst I32 (repr ? 0)))))))
    5659  )
    5760  )
     
    6366  )
    6467
    65 )).
     68) (match daemon in False with [ ])).
    6669
    6770
    6871
    6972definition myprog : Cminor_program :=
    70 mk_program ?? [
    71   (pair ?? id_main f_main)
     73mk_program ?? [] [
     74  (mk_Prod ?? id_main f_main)
    7275]  id_main
    73 []
    7476.
    75 
    76 example exec: finishes_with (repr I32 1) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
    77 normalize  (* you can examine the result here *)
    78 @refl
    79 qed.
    80 
    81 include "Cminor/toRTLabs.ma".
    82 include "RTLabs/semantics.ma".
    83 
    84 example execRTL: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
    85 normalize  (* you can examine the result here *)
    86 @refl
    87 qed.
    88 
Note: See TracChangeset for help on using the changeset viewer.