Changeset 765


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.

Location:
src/RTLabs
Files:
1 added
5 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)
  • src/RTLabs/import.ma

    r762 r765  
    121121let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← r src1; do src2' ← r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse').
    122122let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
    123 let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; OK statement (St_return src').
     123definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
    124124
  • src/RTLabs/semantics.ma

    r762 r765  
    3737   state
    3838| Returnstate :
    39    ∀ rtv : val.
     39   ∀ rtv : option val.
    4040   ∀ dst : option register.
    4141   ∀ stk : list frame.
     
    177177      ]
    178178
    179   | St_return src ⇒
    180       ! v ← reg_retrieve (locals f) src;
     179  | St_return ⇒
     180      ! v ← match f_result (func f) with
     181            [ None ⇒ ret ? (None ?)
     182            | Some r ⇒ ! v ← reg_retrieve (locals f) r; ret ? (Some ? v)
     183            ];
    181184      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    182185  ]
     
    190193        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    191194        ! evres ← do_io (ef_id fn) evargs (match (sig_res (ef_sig fn)) with [ None ⇒ ASTint | Some t ⇒ t ]);  (* XXX hack, should allow none *)
    192         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) dst fs m〉
    193 
     195        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
    194196    ]
    195197| Returnstate v dst fs m ⇒
     
    197199    [ nil ⇒ Error ? (* Already in final state *)
    198200    | cons f fs' ⇒
    199         ! locals ← match dst with [ None ⇒ OK ? (locals f)
    200                                   | Some d ⇒ reg_store d v (locals f) ];
     201        ! locals ← match dst with
     202                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
     203                                         | _ ⇒ Error ? ]
     204                   | Some d ⇒ match v with [ None ⇒ Error ?
     205                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
    201206        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
    202207    ]
     
    208213| Callstate _ _ _ _ _ ⇒ None ?
    209214| Returnstate v _ fs _ ⇒
    210     match fs with [ nil ⇒ match v with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | cons _ _ ⇒ None ? ]
     215    match fs with [ nil ⇒ match v with [ Some v' ⇒ match v' with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | None ⇒ None ? ] | cons _ _ ⇒ None ? ]
    211216].
    212217
  • src/RTLabs/syntax.ma

    r764 r765  
    5454| St_cond2 : binary_operation → register → register → label → label → statement
    5555| St_jumptable : register → list label → statement
    56 | St_return : register → statement
     56| St_return : statement
    5757.
    5858
  • src/RTLabs/test/search.ma

    r750 r765  
    132132    (pair ?? search10 (make_St_cond2 (Ocmp Clt) 12 13 search9 search5));
    133133    (pair ?? search1 (make_St_op1 Onegint 8 9 search0));
    134     (pair ?? search0 (make_St_return 8))
     134    (pair ?? search0 (make_St_return))
    135135]
    136136
     
    233233    (pair ?? main10 (make_St_const 11 (Ointconst (repr 1)) main9));
    234234    (pair ?? main1 (make_St_op1 Ocast8unsigned 2 1 main0));
    235     (pair ?? main0 (make_St_return 2))
     235    (pair ?? main0 make_St_return)
    236236]
    237237
Note: See TracChangeset for help on using the changeset viewer.