Changeset 1226 for src/Cminor


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

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

Location:
src/Cminor
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/cminorMatitaPrinter.ml

    r1157 r1226  
    352352
    353353let print_program p =
    354   Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [\n%s\n]%s\n[%s]\n.\n"
     354  Printf.sprintf "include \"Cminor/semantics.ma\".\ninclude \"common/Animation.ma\".\n\n%s\n\n%s\n\ndefinition myprog : Cminor_program :=\nmk_program ?? [%s] [\n%s\n]%s\n.\n"
    355355    (define_var_ids p.Cminor.vars)
    356356    (print_functs p.Cminor.functs)
     357    (print_vars 2 p.Cminor.vars)
    357358    (print_fun' 2 p.Cminor.functs)
    358359    (print_main 2 p.Cminor.main)
    359     (print_vars 2 p.Cminor.vars)
    360 
     360
  • src/Cminor/test/search.Cminor.ma

    r1157 r1226  
    281281
    282282definition myprog : Cminor_program :=
    283 mk_program ?? [
     283mk_program ?? [] [
    284284  (pair ?? id__div32u f__div32u);
    285285  (pair ?? id__div32s f__div32s);
     
    287287  (pair ?? id_main f_main)
    288288]  id_main
    289 []
    290289.
    291 
    292    example exec: finishes_with (repr 3) ? (exec_up_to Cminor_fullexec myprog 1000 [ ]).
    293    normalize  (* you can examine the result here *)
    294    @refl qed.
    295 
    296 
    297 include "Cminor/toRTLabs.ma".
    298 include "RTLabs/semantics.ma".
    299 
    300 example execRTL: finishes_with (repr 3) ? (do myprog' ← cminor_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [ ]).
    301 normalize  (* you can examine the result here *)
    302 @refl
    303 qed.
    304 
    305 
Note: See TracChangeset for help on using the changeset viewer.