Changeset 490


Ignore:
Timestamp:
Feb 9, 2011, 6:22:34 PM (6 years ago)
Author:
campbell
Message:

Update syntax of Matita Clight term printer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.3/8051-memoryspaces-branch/src/clight/clightPrintMatita.ml

    r489 r490  
    321321      | (id, ty) :: rem ->
    322322          if not first then Buffer.add_string b "; ";
    323           Buffer.add_string b "mk_pair ident type (succ_pos_of_nat ";
     323          Buffer.add_string b "succ_pos_of_nat ";
    324324          Buffer.add_string b (id_s id);
    325           Buffer.add_string b ") ";
     325          Buffer.add_string b ", ";
    326326          Buffer.add_string b (stype ty);
     327          Buffer.add_string b "〉 ";
    327328          add_params false rem in
    328329      add_params true params;
     
    338339
    339340let print_fundef p (id, fd) =
    340   fprintf p "@[<v 2>mk_pair ident fundef (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
     341  fprintf p "@[<v 2>〈succ_pos_of_nat %i (* %s *), " (id_i id) id;
    341342  match fd with
    342343  | External(id', args, res) ->
    343       fprintf p "(External (succ_pos_of_nat %i) %s %s)@]" (id_i id) (typelist args) (stype res)
     344      fprintf p "External (succ_pos_of_nat %i) %s %s〉@]" (id_i id) (typelist args) (stype res)
    344345  | Internal f ->
    345       fprintf p "(Internal (@ %a@;<0 -2>))@]" print_function f
     346      fprintf p "Internal (@ %a@;<0 -2>)〉@]" print_function f
    346347
    347348let string_of_init id =
     
    374375
    375376let print_globvar p ((((id, init), sp), ty)) =
    376   fprintf p "@[<hov 2>(mk_pair ?? (mk_pair ?? (mk_pair ?? (succ_pos_of_nat %i (* %s *))@ %a)@ %s)@ %s)@]"
     377  fprintf p "@[<hov 2>〈〈〈succ_pos_of_nat %i (* %s *),@ %a〉,@ %s〉,@ %s〉@]"
    377378    (id_i id)
    378379    id
     
    473474  struct_unions := StructUnionSet.empty;
    474475  collect_program prog;
    475   fprintf p "include \"Csyntax.ma\".@\n@\n";
    476   fprintf p "@[<v 2>ndefinition myprog := mk_program fundef type@ ";
     476  fprintf p "include \"Animation.ma\".@\n@\n";
     477  fprintf p "@[<v 2>definition myprog := mk_program fundef type@ ";
    477478(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
    478479  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
     
    480481  fprintf p "@\n(succ_pos_of_nat %i)@\n" (id_i "main");
    481482  print_list print_globvar p prog.prog_vars;
    482   fprintf p "@;<0 -2>.@]@."
    483 
    484 
     483  fprintf p "@;<0 -2>.@]@\n@\n";
     484  fprintf p "example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).@\n";
     485  fprintf p "normalize  (* you can examine the result here *)@."
     486
     487
     488
Note: See TracChangeset for help on using the changeset viewer.