Ignore:
Timestamp:
Apr 20, 2011, 5:39:00 PM (9 years ago)
Author:
campbell
Message:

Remove superfluous register in RTLabs return statements.

Also fix up RTLabs prototype pretty printer's handling of global variables.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r750 r765  
     1
     2let next_id = ref 0
     3let fresh () = let i = !next_id in next_id := i+1; i
    14
    25let n_spaces n = String.make n ' '
     
    47
    58let print_global (x, size) =
    6   Printf.sprintf "pair ?? (pair ?? (pair ?? %s [ ]) Any) %d" x size
     9  Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x size
    710
    811let print_globals n globs =
     
    105108  | RTLabs.Aindexed off -> Printf.sprintf "Aindexed (repr %d)" off
    106109  | RTLabs.Aindexed2 -> "Aindexed2"
    107   | RTLabs.Aglobal (id, off) -> Printf.sprintf "Aglobal %s (repr %d)" id off
    108   | RTLabs.Abased (id, off) -> Printf.sprintf "Abased %s (repr %d)" id off
     110  | RTLabs.Aglobal (id, off) -> Printf.sprintf "Aglobal id_%s (repr %d)" id off
     111  | RTLabs.Abased (id, off) -> Printf.sprintf "Abased id_%s (repr %d)" id off
    109112  | RTLabs.Ainstack off -> Printf.sprintf "Ainstack (repr %d)" off
    110113
     
    209212        (Register.print rs)
    210213        (print_table tbl)
    211   | RTLabs.St_return rs -> Printf.sprintf "make_St_return %s" (Register.print rs)
     214  | RTLabs.St_return rs -> "make_St_return" (* rs should always be the function's result register, anyway *)
    212215
    213216let print_cost_labels n c =
     
    246249  "[\n" ^ Label.Map.fold f c ""
    247250
    248 let print_internal_decl n f def m =
     251let print_internal_decl n f def =
    249252  Printf.sprintf
    250253    "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s(%s)\n%s(Some ? %s)\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
    251254    (n_spaces n)
    252255    f
    253     m
     256    (fresh ())
    254257    (print_labels n def.RTLabs.f_graph)
    255258    (print_cost_labels n def.RTLabs.f_graph)
     
    277280
    278281
    279 let print_external_decl n f def m =
     282let print_external_decl n f def =
    280283  Printf.sprintf "%sdefinition id_%s := ident_of_nat %d.\n%sdefinition f_%s := External (mk_external_function id_%s (%s)).\n"
    281284    (n_spaces n)
    282285    f
    283     m
     286    (fresh ())
    284287    (n_spaces n)
    285288    f
     
    288291
    289292
    290 let print_fun_decl n (f, def) m = match def with
    291   | RTLabs.F_int def -> print_internal_decl n f def m
    292   | RTLabs.F_ext def -> print_external_decl n f def m
    293 
    294 let print_fun_decls n functs =
    295   snd (List.fold_left (fun (i,s) f -> i+1, s ^ (print_fun_decl n f i) ^ "\n\n") (0,"")
    296     functs)
     293let print_fun_decl n (f, def) = match def with
     294  | RTLabs.F_int def -> print_internal_decl n f def
     295  | RTLabs.F_ext def -> print_external_decl n f def
     296
     297let print_fun_decls n =
     298  List.fold_left (fun s f -> s ^ (print_fun_decl n f) ^ "\n\n") ""
    297299
    298300let print_fun n functs =
     
    317319    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
    318320
     321let define_var_id (id,_) =
     322  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
     323
     324let define_var_ids =
     325  List.fold_left (fun s v -> s ^ (define_var_id v)) ""
     326
    319327let print_program p =
    320   Printf.sprintf "include \"RTLabs/import.ma\".\ninclude \"common/Animation.ma\".\n\n(*program:*)\n\n\n%s\n\ndefinition prog : res RTLabs_program :=\n%s\nOK ? (mk_program ??\n(%s)\n%s\n%s\n).\n"
     328  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"
     329    (define_var_ids p.RTLabs.vars)
    321330    (print_fun_decls 2 p.RTLabs.functs)
    322331    (print_fun 2 p.RTLabs.functs)
Note: See TracChangeset for help on using the changeset viewer.