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.

File:
1 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 =
Note: See TracChangeset for help on using the changeset viewer.