Changeset 1226


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
Files:
3 added
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/clightPrintMatita.ml

    r1157 r1226  
    466466  collect_program prog;
    467467  fprintf p "include \"Clight/Cexec.ma\".@\ninclude \"common/Animation.ma\".@\n@\n";
    468   fprintf p "@[<v 2>definition myprog := mk_program clight_fundef ((list init_data) × type)@ ";
     468  fprintf p "@[<v 2>definition myprog := mk_program (\\lambda _. clight_fundef) ((list init_data) × type)@ ";
    469469(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
    470470  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
     471  print_list print_globvar p prog.prog_vars;
    471472  print_list print_fundef p prog.prog_funct;
    472473  fprintf p "@\n(ident_of_nat %i)@\n" (id_i "main");
    473   print_list print_globvar p prog.prog_vars;
    474   fprintf p "@;<0 -2>.@]@\n@\n";
     474  fprintf p "@;<0 -2>.@]@\n@\n(*@\n";
    475475  fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).@\n";
    476   fprintf p "normalize  (* you can examine the result here *)@."
     476  fprintf p "normalize  (* you can examine the result here *)@\n";
     477  fprintf p "*)@."
    477478
    478479let print_program prog =
  • src/Clight/test/sum.c.ma

    r1198 r1226  
    22include "common/Animation.ma".
    33
    4 definition myprog := mk_program clight_fundef (list init_data × type)
    5   [〈ident_of_nat 0 (* main *), CL_Internal (
    6      mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 1, (Tint I32 Signed  )〉 ; 〈ident_of_nat 2, (Tint I8 Unsigned )〉 ]
     4definition myprog := mk_program (\lambda _. clight_fundef) ((list init_data) × type)
     5  [〈〈ident_of_nat 0 (* src *), Any〉,
     6     〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
     7        (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
     8        (Init_int8 (repr I8 4)) ], (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     9  [〈ident_of_nat 1 (* main *), CL_Internal (
     10     mk_function (Tint I32 Signed  ) [] [〈ident_of_nat 2, (Tint I32 Signed  )〉 ; 〈ident_of_nat 3, (Tint I8 Unsigned )〉 ]
    711       (Ssequence
    8        (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     12       (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    913         (Expr (Ecast (Tint I8 Unsigned )
    1014           (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1115           (Tint I8 Unsigned )))
    1216       (Ssequence
    13        (Sfor (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     17       (Sfor (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    1418               (Expr (Econst_int I32 (repr ? 0)) (Tint I32 Signed  )))
    1519         (Expr (Ebinop Olt
    1620           (Expr (Ecast (Tint I32 Unsigned)
    17              (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
     21             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    1822             (Tint I32 Unsigned))
    1923           (Expr (Esizeof (Tarray Any (Tint I8 Unsigned ) 5))
    2024             (Tint I32 Unsigned))) (Tint I32 Signed  ))
    21          (Sassign (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     25         (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    2226           (Expr (Ebinop Oadd
    23              (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  ))
     27             (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  ))
    2428             (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed  )))
    2529             (Tint I32 Signed  )))
    26          (Sassign (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned ))
     30         (Sassign (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned ))
    2731           (Expr (Ecast (Tint I8 Unsigned )
    2832             (Expr (Ebinop Oadd
    2933               (Expr (Ecast (Tint I32 Signed  )
    30                  (Expr (Evar (ident_of_nat 2)) (Tint I8 Unsigned )))
     34                 (Expr (Evar (ident_of_nat 3)) (Tint I8 Unsigned )))
    3135                 (Tint I32 Signed  ))
    3236               (Expr (Ecast (Tint I32 Signed  )
    3337                 (Expr (Ederef
    3438                   (Expr (Ebinop Oadd
    35                      (Expr (Evar (ident_of_nat 3))
     39                     (Expr (Evar (ident_of_nat 0))
    3640                       (Tarray Any (Tint I8 Unsigned ) 5))
    37                      (Expr (Evar (ident_of_nat 1)) (Tint I32 Signed  )))
     41                     (Expr (Evar (ident_of_nat 2)) (Tint I32 Signed  )))
    3842                     (Tpointer Any (Tint I8 Unsigned ))))
    3943                   (Tint I8 Unsigned ))) (Tint I32 Signed  )))
     
    4145       )
    4246       (Sreturn (Some expr (Expr (Ecast (Tint I32 Signed  )
    43                              (Expr (Evar (ident_of_nat 2))
     47                             (Expr (Evar (ident_of_nat 3))
    4448                               (Tint I8 Unsigned ))) (Tint I32 Signed  ))))))
    4549     
     
    4751     
    4852   )〉]
    49   (ident_of_nat 0)
    50   [〈〈ident_of_nat 3 (* src *), Any〉,
    51      〈[(Init_int8 (repr I8 28)) ; (Init_int8 (repr I8 17)) ;
    52      (Init_int8 (repr I8 17)) ; (Init_int8 (repr I8 8)) ;
    53      (Init_int8 (repr I8 4)) ],
    54      (Tarray Any (Tint I8 Unsigned ) 5)〉〉]
     53  (ident_of_nat 1)
     54 
    5555.
    5656
    57 example exec: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec myprog 1000 [ ]).
     57(*
     58example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint I32 (repr I32 0)]).
    5859normalize  (* you can examine the result here *)
    59 @refl
    60 qed.
    61 
    62 include "Clight/SimplifyCasts.ma".
    63 
    64 example es: finishes_with (repr I32 74) ? (exec_up_to clight_fullexec (simplify_program myprog) 1000 [ ]).
    65 normalize  (* you can examine the result here *)
    66 @refl
    67 qed.
    68 
    69 include "Clight/toCminor.ma".
    70 include "Cminor/semantics.ma".
    71 
    72 example e1: finishes_with (repr I32 74) ? (do p ← clight_to_cminor (simplify_program myprog); exec_up_to Cminor_fullexec p 1000 [ ]).
    73 normalize
    74 @refl
    75 qed.
    76 
    77 include "Cminor/toRTLabs.ma".
    78 include "RTLabs/semantics.ma".
    79 
    80 example e2: finishes_with (repr I32 74) ? (
    81 do p1 ← clight_to_cminor (simplify_program myprog);
    82 do p2 ← cminor_to_rtlabs p1;
    83  exec_up_to RTLabs_fullexec p2 1000 [ ]).
    84 normalize
    85 @refl
    86 qed.
     60*)
  • 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 
  • 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.