Changeset 1226 for src/RTLabs
- Timestamp:
- Sep 16, 2011, 7:16:44 PM (9 years ago)
- Location:
- src/RTLabs
- Files:
-
- 1 added
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsMatitaPrinter.ml
r1157 r1226 312 312 313 313 let print_program p = 314 Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n (%s)\n%s\n%s\n).\n"314 Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n%s\n(%s)\n%s\n).\n" 315 315 (define_var_ids p.RTLabs.vars) 316 316 (print_fun_decls 2 p.RTLabs.functs) 317 317 (print_fun 2 p.RTLabs.functs) 318 (print_globals 2 p.RTLabs.vars) 318 319 (print_fun' 2 p.RTLabs.functs) 319 320 (print_main 2 p.RTLabs.main) 320 (print_globals 2 p.RTLabs.vars) -
src/RTLabs/test/search.RTLabs.ma
r1157 r1226 428 428 429 429 OK ? (mk_program ?? 430 (*globals:*) 431 [] 430 432 ( (pair ?? id_main f_main):: 431 433 (pair ?? id_search f_search):: … … 434 436 (nil ?)) 435 437 id_main 436 (*globals:*)437 []438 438 ). 439 440 example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).441 normalize (* you can examine the result here *)442 @refl qed.
Note: See TracChangeset
for help on using the changeset viewer.