Changeset 769


Ignore:
Timestamp:
Apr 22, 2011, 1:49:12 PM (9 years ago)
Author:
campbell
Message:

Update the Clight matita term printer.

File:
1 edited

Legend:

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

    r490 r769  
    158158  | Tfunction(args, res) -> "(Tfunction " ^ typelist args ^ " " ^ stype res ^ ")"
    159159  | Tstruct(name, fld) ->
    160       fieldlist "(Tstruct (succ_pos_of_nat " name fld
     160      fieldlist "(Tstruct (ident_of_nat " name fld
    161161  | Tunion(name, fld) ->
    162       fieldlist "(Tunion (succ_pos_of_nat " name fld
     162      fieldlist "(Tunion (ident_of_nat " name fld
    163163  | Tcomp_ptr (sp, name) ->
    164       "(Tcomp_ptr "^ sspace sp ^" (succ_pos_of_nat " ^ id_s name ^ "))"
     164      "(Tcomp_ptr "^ sspace sp ^" (ident_of_nat " ^ id_s name ^ "))"
    165165 and typelist l =
    166166    let b = Buffer.create 20 in
     
    183183        | [] -> Buffer.add_string b "Fnil"
    184184        | (id, ty)::tl ->
    185             Buffer.add_string b "(Fcons (succ_pos_of_nat ";
     185            Buffer.add_string b "(Fcons (ident_of_nat ";
    186186            Buffer.add_string b (id_s id);
    187187            Buffer.add_string b ") ";
     
    208208      fprintf p "(Econst_float %F)" f
    209209  | Evar id ->
    210       fprintf p "(Evar (succ_pos_of_nat %d))" (id_i id)
     210      fprintf p "(Evar (ident_of_nat %d))" (id_i id)
    211211  | Eunop(op, e1) ->
    212212      fprintf p "(Eunop %s %a)" (name_unop op) print_expr e1
     
    240240      fprintf p "(Esizeof %s)" (stype ty)
    241241  | Efield(e1, id) ->
    242       fprintf p "(Efield %a (succ_pos_of_nat %i))" print_expr e1 (id_i id)
     242      fprintf p "(Efield %a (ident_of_nat %i))" print_expr e1 (id_i id)
    243243
    244244let rec print_expr_list p (first, el) =
     
    300300      fprintf p "(Sreturn (Some expr %a))" print_expr e
    301301  | Slabel(lbl, s1) ->
    302       fprintf p "(Slabel (succ_pos_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
     302      fprintf p "(Slabel (ident_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
    303303  | Sgoto lbl ->
    304       fprintf p "(Sgoto (succ_pos_of_nat %i))" (id_i lbl)
     304      fprintf p "(Sgoto (ident_of_nat %i))" (id_i lbl)
    305305
    306306and print_cases p cases =
     
    321321      | (id, ty) :: rem ->
    322322          if not first then Buffer.add_string b "; ";
    323           Buffer.add_string b "〈succ_pos_of_nat ";
     323          Buffer.add_string b "〈ident_of_nat ";
    324324          Buffer.add_string b (id_s id);
    325325          Buffer.add_string b ", ";
     
    339339
    340340let print_fundef p (id, fd) =
    341   fprintf p "@[<v 2>〈succ_pos_of_nat %i (* %s *), " (id_i id) id;
     341  fprintf p "@[<v 2>〈ident_of_nat %i (* %s *), " (id_i id) id;
    342342  match fd with
    343343  | External(id', args, res) ->
    344       fprintf p "External (succ_pos_of_nat %i) %s %s〉@]" (id_i id) (typelist args) (stype res)
     344      fprintf p "CL_External (ident_of_nat %i) %s %s〉@]" (id_i id) (typelist args) (stype res)
    345345  | Internal f ->
    346       fprintf p "Internal (@ %a@;<0 -2>)〉@]" print_function f
     346      fprintf p "CL_Internal (@ %a@;<0 -2>)〉@]" print_function f
    347347
    348348let string_of_init id =
     
    370370  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
    371371  | Init_space n -> fprintf p "(Init_space %d)@ " n
    372   | Init_addrof(r, symb, ofs) -> fprintf p "(Init_addrof %s (succ_pos_of_nat %i) (repr %d))" (sspace r) (id_i symb) ofs
     372  | Init_addrof(r, symb, ofs) -> fprintf p "(Init_addrof %s (ident_of_nat %i) (repr %d))" (sspace r) (id_i symb) ofs
    373373
    374374let re_string_literal = Str.regexp "__stringlit_[0-9]+"
    375375
    376376let print_globvar p ((((id, init), sp), ty)) =
    377   fprintf p "@[<hov 2>〈〈〈succ_pos_of_nat %i (* %s *),@ %a〉,@ %s〉,@ %s〉@]"
     377  fprintf p "@[<hov 2>〈〈〈ident_of_nat %i (* %s *),@ %a〉,@ %s〉,@ %s〉@]"
    378378    (id_i id)
    379379    id
     
    474474  struct_unions := StructUnionSet.empty;
    475475  collect_program prog;
    476   fprintf p "include \"Animation.ma\".@\n@\n";
    477   fprintf p "@[<v 2>definition myprog := mk_program fundef type@ ";
     476  fprintf p "include \"Clight/Cexec.ma\".@\ninclude \"common/Animation.ma\".@\n@\n";
     477  fprintf p "@[<v 2>definition myprog := mk_program clight_fundef type@ ";
    478478(*  StructUnionSet.iter (declare_struct_or_union p) !struct_unions;
    479479  StructUnionSet.iter (print_struct_or_union p) !struct_unions;*)
    480480  print_list print_fundef p prog.prog_funct;
    481   fprintf p "@\n(succ_pos_of_nat %i)@\n" (id_i "main");
     481  fprintf p "@\n(ident_of_nat %i)@\n" (id_i "main");
    482482  print_list print_globvar p prog.prog_vars;
    483483  fprintf p "@;<0 -2>.@]@\n@\n";
    484   fprintf p "example exec: result ? (exec_up_to myprog 1000 [EVint (repr 0)]).@\n";
     484  fprintf p "example exec: result ? (exec_up_to clight_fullexec myprog 1000 [EVint (repr 0)]).@\n";
    485485  fprintf p "normalize  (* you can examine the result here *)@."
    486486
Note: See TracChangeset for help on using the changeset viewer.