Changeset 1226 for src/RTLabs


Ignore:
Timestamp:
Sep 16, 2011, 7:16:44 PM (8 years ago)
Author:
campbell
Message:

Adjust pretty printers for change in program records, try a test of each.

Location:
src/RTLabs
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r1157 r1226  
    312312
    313313let 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"
    315315    (define_var_ids p.RTLabs.vars)
    316316    (print_fun_decls 2 p.RTLabs.functs)
    317317    (print_fun 2 p.RTLabs.functs)
     318    (print_globals 2 p.RTLabs.vars)
    318319    (print_fun' 2 p.RTLabs.functs)
    319320    (print_main 2 p.RTLabs.main)
    320     (print_globals 2 p.RTLabs.vars)
  • src/RTLabs/test/search.RTLabs.ma

    r1157 r1226  
    428428
    429429OK ? (mk_program ??
     430  (*globals:*)
     431  []
    430432(  (pair ?? id_main f_main)::
    431433  (pair ?? id_search f_search)::
     
    434436(nil ?))
    435437  id_main
    436   (*globals:*)
    437   []
    438438).
    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.