Changeset 1226 for src/RTLabs

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:

• RTLabsMatitaPrinter.ml (modified) (1 diff)
• test/search.RTLabs.ma (modified) (2 diffs)
• test/search.test.ma (added)

src/RTLabs/RTLabsMatitaPrinter.ml

@@ -312 +312 @@
 
 let print_program p =
-  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"
+  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"
     (define_var_ids p.RTLabs.vars)
     (print_fun_decls 2 p.RTLabs.functs)
     (print_fun 2 p.RTLabs.functs)
+    (print_globals 2 p.RTLabs.vars)
     (print_fun' 2 p.RTLabs.functs)
     (print_main 2 p.RTLabs.main)
-    (print_globals 2 p.RTLabs.vars)

src/RTLabs/test/search.RTLabs.ma

@@ -428 +428 @@
 
 OK ? (mk_program ??
+  (*globals:*)
+  []
 (  (pair ?? id_main f_main)::
   (pair ?? id_search f_search)::
@@ -434 +436 @@
 (nil ?))
   id_main
-  (*globals:*)
-  []
 ).
-
-   example exec: finishes_with (repr I32 3) ? (do p ← prog; do r ← exec_up_to RTLabs_fullexec p 1000 [ ]; OK ? r).
-   normalize  (* you can examine the result here *)
-   @refl qed.