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

Pointer fixes for the temporary version of the compiler that can output matita
terms.

File:
1 edited

Legend:

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

    r461 r489  
    136136  | Tunion(name, fld) ->
    137137      name ^ name_optid id
    138   | Tcomp_ptr name ->
     138  | Tcomp_ptr (_,name) ->
    139139      name ^ " *" ^ id
    140140
     
    161161  | Tunion(name, fld) ->
    162162      fieldlist "(Tunion (succ_pos_of_nat " name fld
    163   | Tcomp_ptr name ->
    164       "(Tcomp_ptr (succ_pos_of_nat " ^ id_s name ^ "))"
     163  | Tcomp_ptr (sp, name) ->
     164      "(Tcomp_ptr "^ sspace sp ^" (succ_pos_of_nat " ^ id_s name ^ "))"
    165165 and typelist l =
    166166    let b = Buffer.create 20 in
     
    258258      fprintf p "@[<hv 2>(Sassign %a@ %a)@]" print_expr e1 print_expr e2
    259259  | Scall(None, e1, el) ->
    260       fprintf p "@[<hv 2>(Scall (None ?) %a @[<hov 0>%a@])@]"
     260      fprintf p "@[<hv 2>(Scall (None expr) %a @[<hov 0>%a@])@]"
    261261                print_expr e1
    262262                (print_list print_expr) el
    263263  | Scall(Some lhs, e1, el) ->
    264       fprintf p "@[<hv 2>(Scall (Some ? %a)@ %a@ @[<hov 0>%a@])@]"
     264      fprintf p "@[<hv 2>(Scall (Some expr %a)@ %a@ @[<hov 0>%a@])@]"
    265265                print_expr lhs
    266266                print_expr e1
     
    296296              print_cases cases
    297297  | Sreturn None ->
    298       fprintf p "(Sreturn (None ?))"
     298      fprintf p "(Sreturn (None expr))"
    299299  | Sreturn (Some e) ->
    300       fprintf p "(Sreturn (Some ? %a))" print_expr e
     300      fprintf p "(Sreturn (Some expr %a))" print_expr e
    301301  | Slabel(lbl, s1) ->
    302302      fprintf p "(Slabel (succ_pos_of_nat %i)@ %a)" (id_i lbl) print_stmt s1
     
    321321      | (id, ty) :: rem ->
    322322          if not first then Buffer.add_string b "; ";
    323           Buffer.add_string b "mk_pair ?? (succ_pos_of_nat ";
     323          Buffer.add_string b "mk_pair ident type (succ_pos_of_nat ";
    324324          Buffer.add_string b (id_s id);
    325325          Buffer.add_string b ") ";
     
    338338
    339339let print_fundef p (id, fd) =
    340   fprintf p "@[<v 2>mk_pair ?? (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
     340  fprintf p "@[<v 2>mk_pair ident fundef (succ_pos_of_nat %i (* %s *)) " (id_i id) id;
    341341  match fd with
    342342  | External(id', args, res) ->
     
    364364  | Init_int8 n -> fprintf p "(Init_int8 (repr %d))@ " n
    365365  | Init_int16 n -> fprintf p "(Init_int16 (repr %d))@ " n
    366   | Init_int24 n -> fprintf p "(Init_int24 (repr %d))@ " n
     366  | Init_null r -> fprintf p "(Init_null %s)@ " (sspace r)
    367367  | Init_int32 n -> fprintf p "(Init_int32 (repr %d))@ " n
    368368  | Init_float32 n -> fprintf p "(Init_float32 %F)@ " n
    369369  | Init_float64 n -> fprintf p "(Iinit_float64 %F)@ " n
    370370  | Init_space n -> fprintf p "(Init_space %d)@ " n
    371   | Init_addrof(symb, ofs) -> fprintf p "(Init_addrof %d (repr %d))" (id_i symb) ofs
     371  | Init_addrof(r, symb, ofs) -> fprintf p "(Init_addrof %s (succ_pos_of_nat %i) (repr %d))" (sspace r) (id_i symb) ofs
    372372
    373373let re_string_literal = Str.regexp "__stringlit_[0-9]+"
Note: See TracChangeset for help on using the changeset viewer.