source: src/Clight/test/factorial.ma @ 717

Last change on this file since 717 was 717, checked in by campbell, 11 years ago

Clean up Clight examples; better temporary definition of multiply.

File size: 2.0 KB
RevLine 
[717]1include "Clight/Animation.ma".
[415]2
[717]3definition myprog := mk_program fundef type
4  [〈succ_pos_of_nat 0 (* get_input *), External (succ_pos_of_nat 0) Tnil (Tint I32 Signed  )〉;
5  〈succ_pos_of_nat 1 (* main *), Internal (
6    mk_function (Tint I32 Signed  ) [] [〈succ_pos_of_nat 2, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 3, (Tint I32 Signed  )〉 ; 〈succ_pos_of_nat 4, (Tint I32 Signed  )〉 ]
[415]7      (Ssequence
[717]8      (Scall (Some expr (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
9        (Expr (Evar (succ_pos_of_nat 0))
[415]10          (Tfunction Tnil (Tint I32 Signed  )))
11        [])
12      (Ssequence
[717]13      (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
[415]14        (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
15      (Ssequence
[717]16      (Ssequence
17      (Sfor (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
[415]18              (Expr (Econst_int (repr 2)) (Tint I32 Signed  )))
19        (Expr (Ebinop Ole
[717]20          (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
21          (Expr (Evar (succ_pos_of_nat 2)) (Tint I32 Signed  )))
[415]22          (Tint I32 Signed  ))
[717]23        (Sassign (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
[415]24          (Expr (Ebinop Oadd
[717]25            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  ))
[415]26            (Expr (Econst_int (repr 1)) (Tint I32 Signed  )))
27            (Tint I32 Signed  )))
[717]28        (Sassign (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
[415]29          (Expr (Ebinop Omul
[717]30            (Expr (Evar (succ_pos_of_nat 3)) (Tint I32 Signed  ))
31            (Expr (Evar (succ_pos_of_nat 4)) (Tint I32 Signed  )))
[415]32            (Tint I32 Signed  )))
33      )
[717]34      Sskip)
35      (Sreturn (Some expr (Expr (Evar (succ_pos_of_nat 3))
36                            (Tint I32 Signed  )))))))
[415]37   
38   
39   
[717]40  )〉]
41  (succ_pos_of_nat 1)
[415]42  []
43.
44
[717]45example exec:
46  (do 〈t,s〉 ← exec_up_to myprog 1000 [EVint (repr 5)]; OK ? (is_final s)) = OK ? (Some ? (repr 120)).
47normalize  (* you can examine the result here *)
48@refl qed.
Note: See TracBrowser for help on using the repository browser.