Changeset 898


Ignore:
Timestamp:
Jun 8, 2011, 1:14:55 PM (8 years ago)
Author:
campbell
Message:

Update pretty printers and examples.

Location:
src
Files:
4 added
3 deleted
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/cminorMatitaPrinter.ml

    r816 r898  
    44let fresh () = let i = !next_id in next_id := i+1; i
    55
     6let print_signedness = function
     7  | Signed -> "Signed"
     8  | Unsigned -> "Unsigned"
     9
    610let print_type = function
    7   | Sig_int -> "ASTint"
    8   | Sig_float -> "ASTfloat"
     11  | Sig_int (sz, sg) -> Printf.sprintf "ASTint I%d %s" (sz*8) (print_signedness sg)
     12  | Sig_float (sz, _) -> Printf.sprintf "ASTfloat F%d" (sz*8)
     13  | Sig_offset -> "ASTint I32 Unsigned"
    914  | Sig_ptr -> "ASTptr Any"
    1015
    1116let print_ret_type = function
    12   | Type_ret t -> print_type t
    13   | Type_void -> "void"
     17  | Type_ret t -> Printf.sprintf "Some ? (%s)" (print_type t)
     18  | Type_void -> "None ?"
    1419
    1520
    1621let print_data = function
    17   | Data_reserve n -> Printf.sprintf "Init_space %d" n
     22  (*| Data_reserve n -> Printf.sprintf "Init_space %d" n*)
    1823  | Data_int8 i -> Printf.sprintf "Init_int8 (repr %d)" i
    1924  | Data_int16 i -> Printf.sprintf "Init_int16 (repr %d)" i
     
    2227  | Data_float64 f -> Printf.sprintf "Init_float64 %f" f
    2328
    24 let print_var n (id, init) =
     29let print_var n (id, sz, init) =
    2530  Printf.sprintf "(pair ?? (pair ?? (pair ?? id_%s [%s]) Any) it)"
    2631    id
    27     (MiscPottier.string_of_list ";" print_data init)
     32    (match init with
     33     | None -> Printf.sprintf "Init_space %d" (Driver.CminorMemory.concrete_size sz)
     34     | Some init ->
     35         (MiscPottier.string_of_list ";" print_data init))
    2836
    2937let print_vars n = MiscPottier.string_of_list ";\n" (print_var n)
     
    4149  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
    4250  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
    43   | AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off
     51  (*| AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off*)
     52  | AST.Cst_stack -> Printf.sprintf "Oaddrstack (repr 0)"
     53  | AST.Cst_offset off -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_offset off)
     54  | AST.Cst_sizeof sz -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_size sz)
    4455
    4556let print_op1 = function
    46   | AST.Op_cast8unsigned -> "Ocast8unsigned"
    47   | AST.Op_cast8signed -> "Ocast8signed"
    48   | AST.Op_cast16unsigned -> "Ocast16unsigned"
    49   | AST.Op_cast16signed -> "Ocast16signed"
     57  | AST.Op_cast((1,Unsigned),_) -> "Ocast8unsigned"
     58  | AST.Op_cast((1,Signed),_) -> "Ocast8signed"
     59  | AST.Op_cast((2,Unsigned),_) -> "Ocast16unsigned"
     60  | AST.Op_cast((2,Signed),_) -> "Ocast16signed"
     61  | AST.Op_cast((4,_),_) -> "Oid"
    5062  | AST.Op_negint -> "Onegint"
    5163  | AST.Op_notbool -> "Onotbool"
    5264  | AST.Op_notint -> "Onotint"
    53   | AST.Op_negf -> "Onegf"
    54   | AST.Op_absf -> "Oabsf"
    55   | AST.Op_singleoffloat -> "Osingleoffloat"
    56   | AST.Op_intoffloat -> "Ointoffloat"
    57   | AST.Op_intuoffloat -> "Ointuoffloat"
    58   | AST.Op_floatofint -> "Ofloatofint"
    59   | AST.Op_floatofintu -> "Ofloatofintu"
    6065  | AST.Op_id -> "Oid"
    61   | AST.Op_ptrofint -> "Optrofint"
     66  | AST.Op_ptrofint -> "(Optrofint Any)"
    6267  | AST.Op_intofptr -> "Ointofptr"
    6368
     
    7681  | AST.Op_shr -> "Oshr"
    7782  | AST.Op_shru -> "Oshru"
    78   | AST.Op_addf -> "Oaddf"
    79   | AST.Op_subf -> "Osubf"
    80   | AST.Op_mulf -> "Omulf"
    81   | AST.Op_divf -> "Odivf"
    8283  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
    8384  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
    84   | AST.Op_cmpf cmp -> "(Ocmpf " ^ (print_cmp cmp) ^ ")"
    8585  | AST.Op_addp -> "Oaddp"
    86   | AST.Op_subp -> "Osubpi" (* FIXME: there should be separate subpi and subpp ops*)
     86  | AST.Op_subp -> "Osubpi"
     87  | AST.Op_subpp -> "Osubpp"
    8788  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
    8889
    8990let rec define_expr_labels = function
     91| Cminor.Expr (e,ty) -> match e with
    9092  | Cminor.Op1 (_, e) -> define_expr_labels e
    9193  | Cminor.Op2 (_, e1, e2) -> define_expr_labels e1 ^ define_expr_labels e2
     
    99101
    100102let print_quantity = function
    101   | Memory.QInt 1 -> "Mint8unsigned"
    102   | Memory.QInt 2 -> "Mint16unsigned"
    103   | Memory.QInt 4 -> "Mint32"
    104   | Memory.QPtr -> "Mpointer Any"
     103  | AST.QInt 1 -> "Mint8unsigned"
     104  | AST.QInt 2 -> "Mint16unsigned"
     105  | AST.QInt 4 -> "Mint32"
     106  | AST.QOffset -> "Mint32"
     107  | AST.QPtr -> "Mpointer Any"
     108
     109let typeof = function Cminor.Expr (_,ty) -> ty
    105110
    106111let rec print_expression p_id = function
    107   | Cminor.Id id -> "Id " ^ (p_id id)
    108   | Cminor.Cst cst -> Printf.sprintf "Cst (%s)" (print_constant cst)
     112| Cminor.Expr (e,ty) -> match e with
     113  | Cminor.Id id -> Printf.sprintf "Id (%s) %s" (print_type ty) (p_id id)
     114  | Cminor.Cst cst -> Printf.sprintf "Cst (%s) (%s)" (print_type ty) (print_constant cst)
    109115  | Cminor.Op1 (op1, e) ->
    110       Printf.sprintf "Op1 %s (%s)" (print_op1 op1) (print_expression p_id e)
     116      Printf.sprintf "Op1 (%s) (%s) %s (%s)"
     117        (print_type (typeof e)) (print_type ty)
     118        (print_op1 op1) (print_expression p_id e)
    111119  | Cminor.Op2 (op2, e1, e2) ->
    112       Printf.sprintf "Op2 %s (%s) (%s)"
     120      Printf.sprintf "Op2 (%s) (%s) (%s) %s (%s) (%s)"
     121        (print_type (typeof e1)) (print_type (typeof e2)) (print_type ty)
    113122        (print_op2 op2)
    114123        (print_expression p_id e1)
    115124        (print_expression p_id e2)
    116125  | Cminor.Mem (q, e) ->
    117       Printf.sprintf "Mem %s (%s)" (print_quantity q) (print_expression p_id e)
     126      Printf.sprintf "Mem (%s) Any %s (%s)"
     127        (print_type ty) (print_quantity q) (print_expression p_id e)
    118128  | Cminor.Cond (e1, e2, e3) ->
    119       Printf.sprintf "Cond (%s) (%s) (%s)"
     129      let sz,sg = match typeof e1 with Sig_int (sz, sg) -> sz,sg in
     130      Printf.sprintf "Cond I%d %s (%s) (%s) (%s) (%s)"
     131        (sz*8) (print_signedness sg)
     132        (print_type ty)
    120133        (print_expression p_id e1)
    121134        (print_expression p_id e2)
    122135        (print_expression p_id e3)
    123136  | Cminor.Exp_cost (lab, e) ->
    124       Printf.sprintf "Ecost C%s (%s)" lab (print_expression p_id e)
    125 
     137      Printf.sprintf "Ecost (%s) C%s (%s)" (print_type ty) lab (print_expression p_id e)
     138
     139let print_arg p_id e =
     140  Printf.sprintf "dp ?? (%s) (%s)" (print_type (typeof e)) (print_expression p_id e)
    126141
    127142let rec print_args p_id =
    128   MiscPottier.string_of_list "; " (print_expression p_id)
     143  MiscPottier.string_of_list "; " (print_arg p_id)
    129144
    130145
     
    132147
    133148
    134 let print_sig s =
    135   Printf.sprintf "mk_signature [%s] (%s)"
    136     (MiscPottier.string_of_list "; " print_type s.AST.args)
    137     (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_type t
    138                         | AST.Type_void  -> "None ?")
     149let print_local p_id (id,ty) =
     150  Printf.sprintf "pair ?? %s (%s)" (p_id id) (print_type ty)
    139151
    140152let print_locals p_id vars =
    141   (MiscPottier.string_of_list "; " p_id vars)
     153  (MiscPottier.string_of_list "; " (print_local p_id) vars)
    142154
    143155
     
    170182  | Cminor.St_skip -> Printf.sprintf "%sSt_skip" (n_spaces n)
    171183  | Cminor.St_assign (id, e) ->
    172       Printf.sprintf "%sSt_assign %s (%s)\n" (n_spaces n) (p_id id) (print_expression p_id e)
     184      Printf.sprintf "%sSt_assign (%s) %s (%s)\n"
     185        (n_spaces n) (print_type (typeof e))
     186        (p_id id) (print_expression p_id e)
    173187  | Cminor.St_store (q, e1, e2) ->
    174       Printf.sprintf "%sSt_store %s (%s) (%s)\n"
    175         (n_spaces n)
     188      Printf.sprintf "%sSt_store (%s) Any %s (%s) (%s)\n"
     189        (n_spaces n)
     190        (print_type (typeof e2))
    176191        (print_quantity q)
    177192        (print_expression p_id e1)
    178193        (print_expression p_id e2)
     194(* XXX cheat horribly *)
     195  | Cminor.St_call (None, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
     196      Printf.sprintf "%sSt_call (None ?) (Cst ? (Oaddrsymbol id_%s (repr 0))) [%s]\n"
     197        (n_spaces n)
     198        f
     199        (print_args p_id args)
     200  | Cminor.St_call (Some id, Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
     201      Printf.sprintf "%sSt_call (Some ? %s) (Cst ? (Oaddrsymbol id_%s (repr 0))) [%s]\n"
     202        (n_spaces n)
     203        (p_id id)
     204        f
     205        (print_args p_id args)
     206  | Cminor.St_tailcall (Cminor.Expr (Cminor.Cst (AST.Cst_addrsymbol f),_), args, sg) ->
     207      Printf.sprintf "%sSt_tailcall (Cst ? (Oaddrsymbol id_%s (repr 0))) [%s]\n"
     208        (n_spaces n)
     209        f
     210        (print_args p_id args)
     211(* XXX regular versions, but the region will be screwed up *)
    179212  | Cminor.St_call (None, f, args, sg) ->
    180213      Printf.sprintf "%sSt_call (None ?) (%s) [%s]\n"
     
    201234        (n_spaces n)
    202235  | Cminor.St_ifthenelse (e, s1, s2) ->
    203       Printf.sprintf "%sSt_ifthenelse (%s) (\n%s%s) (\n%s%s)\n"
    204         (n_spaces n)
     236      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
     237      Printf.sprintf "%sSt_ifthenelse I%d %s (%s) (\n%s%s) (\n%s%s)\n"
     238        (n_spaces n)
     239        (sz*8) (print_signedness sg)
    205240        (print_expression p_id e)
    206241        (print_body p_id (n+2) s1)
     
    221256      Printf.sprintf "%sSt_exit %d\n" (n_spaces n) i
    222257  | Cminor.St_switch (e, tbl, dflt) ->
    223       Printf.sprintf "%sSt_switch (%s) [\n%s%s] %d\n"
    224         (n_spaces n)
     258      let sz,sg = match typeof e with Sig_int (sz, sg) -> sz,sg in
     259      Printf.sprintf "%sSt_switch I%d %s (%s) [\n%s%s] %d\n"
     260        (n_spaces n)
     261        (sz*8) (print_signedness sg)
    225262        (print_expression p_id e)
    226263        (n_spaces (n+2))
     
    229266  | Cminor.St_return None -> Printf.sprintf "%sSt_return (None ?)\n" (n_spaces n)
    230267  | Cminor.St_return (Some e) ->
    231       Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_expression p_id e)
     268      Printf.sprintf "%sSt_return (Some ? (%s))\n" (n_spaces n) (print_arg p_id e)
    232269  | Cminor.St_label (lbl, s) ->
    233270      Printf.sprintf "%sSt_label L%s (\n%s%s)\n"
     
    244281
    245282let print_ids fname vs =
    246   List.fold_left (fun s v ->
     283  List.fold_left (fun s (v,_) ->
    247284                  Printf.sprintf "%sdefinition id_%s_%s := ident_of_nat %d.\n"
    248285                                 s fname v (fresh ()))
     
    252289  let fid = fresh () in
    253290  let p_id id = Printf.sprintf "id_%s_%s" f_name id in
    254   Printf.sprintf "definition id_%s := ident_of_nat %d.\n%s%sdefinition f_%s := Internal ? (mk_internal_function\n  (%s)\n  [%s]\n  [%s]\n  [%s]\n  %d (\n%s\n)).\n\n"
     291  Printf.sprintf "definition id_%s := ident_of_nat %d.\n%s%sdefinition f_%s := Internal ? (mk_internal_function\n  (%s)\n  [%s]\n  [%s]\n  %d (\n%s\n)).\n\n"
    255292    f_name
    256293    fid
     
    258295    (define_labels f_def.Cminor.f_body)
    259296    f_name
    260     (print_sig f_def.Cminor.f_sig)
     297    (print_ret_type f_def.Cminor.f_return)
    261298    (print_locals p_id f_def.Cminor.f_params)
    262299    (print_locals p_id f_def.Cminor.f_vars)
    263     (print_locals p_id f_def.Cminor.f_ptrs)
    264     f_def.Cminor.f_stacksize
     300    (Driver.CminorMemory.concrete_size f_def.Cminor.f_stacksize)
    265301    (print_body p_id 2 f_def.Cminor.f_body)
     302
     303let print_sig s =
     304  Printf.sprintf "mk_signature [%s] (%s)"
     305    (MiscPottier.string_of_list "; " print_type s.AST.args)
     306    (match s.AST.res with AST.Type_ret t -> "Some ? " ^ print_type t
     307                        | AST.Type_void  -> "None ?")
     308
    266309
    267310
     
    295338    (match main with Some f -> "id_" ^ f | None -> "ident_of_nat 0 (* None! *)")
    296339
    297 let define_var_id (id,_) =
     340let define_var_id (id,_,_) =
    298341  Printf.sprintf "definition id_%s := ident_of_nat %d.\n" id (fresh ())
    299342
  • src/RTLabs/RTLabsMatitaPrinter.ml

    r816 r898  
    55let n_spaces n = String.make n ' '
    66
     7let print_signedness = function
     8  | AST.Signed -> "Signed"
     9  | AST.Unsigned -> "Unsigned"
     10
     11let print_sig_type = function
     12  | AST.Sig_int (sz, sg) -> Printf.sprintf "ASTint I%d %s" (sz*8) (print_signedness sg)
     13  | AST.Sig_float (sz, _) -> Printf.sprintf "ASTfloat F%d" (sz*8)
     14  | AST.Sig_offset -> "ASTint I32 Unsigned"
     15  | AST.Sig_ptr -> "ASTptr Any"
    716
    817let print_global (x, size) =
    9   Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x size
     18  Printf.sprintf "pair ?? (pair ?? (pair ?? id_%s [Init_space %d ]) Any) it" x
     19    (Driver.RTLabsMemory.concrete_size size)
    1020
    1121let print_globals n globs =
     
    1929  Printf.sprintf "[[%s]]" (MiscPottier.string_of_list "; " Register.print args)
    2030
    21 let print_result rl = Register.print rl
     31let print_regty (r,ty) =
     32  Printf.sprintf "(pair ?? %s (%s))" (Register.print r) (print_sig_type ty)
     33
     34let print_result = function
     35| None -> "(None ?)"
     36| Some rty -> "(Some ? " ^ print_regty rty ^ ")"
    2237
    2338let print_params rl =
     
    2540
    2641let print_locals rl =
    27   Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " Register.print rl)
     42  Printf.sprintf "[%s]" (MiscPottier.string_of_list "; " print_regty rl)
    2843
    2944let print_quantity = function
    30   | Memory.QInt 1 -> "Mint8unsigned"
    31   | Memory.QInt 2 -> "Mint16unsigned"
    32   | Memory.QInt 4 -> "Mint32"
    33   | Memory.QPtr -> "Mpointer Any"
     45  | AST.QInt 1 -> "Mint8unsigned"
     46  | AST.QInt 2 -> "Mint16unsigned"
     47  | AST.QInt 4 -> "Mint32"
     48  | AST.QOffset -> "Mint32"
     49  | AST.QPtr -> "Mpointer Any"
    3450(*
    3551let print_memory_q = function
     
    5874  | AST.Cst_float f -> Printf.sprintf "Ofloatconst %f" f
    5975  | AST.Cst_addrsymbol id -> Printf.sprintf "Oaddrsymbol id_%s (repr 0)" id
    60   | AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off
     76  (*| AST.Cst_stackoffset off -> Printf.sprintf "Oaddrstack (repr %d)" off*)
     77  | AST.Cst_stack -> Printf.sprintf "Oaddrstack (repr 0)"
     78  | AST.Cst_offset off -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_offset off)
     79  | AST.Cst_sizeof sz -> Printf.sprintf "Ointconst (repr %d)" (Driver.CminorMemory.concrete_size sz)
    6180
    6281let print_op1 = function
    63   | AST.Op_cast8unsigned -> "Ocast8unsigned"
    64   | AST.Op_cast8signed -> "Ocast8signed"
    65   | AST.Op_cast16unsigned -> "Ocast16unsigned"
    66   | AST.Op_cast16signed -> "Ocast16signed"
     82  | AST.Op_cast((_,AST.Unsigned),1) -> "Ocast8unsigned"
     83  | AST.Op_cast((_,AST.Signed),1) -> "Ocast8signed"
     84  | AST.Op_cast((_,AST.Unsigned),2) -> "Ocast16unsigned"
     85  | AST.Op_cast((_,AST.Signed),2) -> "Ocast16signed"
     86  | AST.Op_cast((_,AST.Unsigned),4) -> "Oid"
     87  | AST.Op_cast((_,AST.Signed),4) -> "Oid"
    6788  | AST.Op_negint -> "Onegint"
    6889  | AST.Op_notbool -> "Onotbool"
    6990  | AST.Op_notint -> "Onotint"
    70   | AST.Op_negf -> "Onegf"
    71   | AST.Op_absf -> "Oabsf"
    72   | AST.Op_singleoffloat -> "Osingleoffloat"
    73   | AST.Op_intoffloat -> "Ointoffloat"
    74   | AST.Op_intuoffloat -> "Ointuoffloat"
    75   | AST.Op_floatofint -> "Ofloatofint"
    76   | AST.Op_floatofintu -> "Ofloatofintu"
    7791  | AST.Op_id -> "Oid"
    7892  | AST.Op_ptrofint -> "Optrofint"
     
    93107  | AST.Op_shr -> "Oshr"
    94108  | AST.Op_shru -> "Oshru"
    95   | AST.Op_addf -> "Oaddf"
    96   | AST.Op_subf -> "Osubf"
    97   | AST.Op_mulf -> "Omulf"
    98   | AST.Op_divf -> "Odivf"
    99109  | AST.Op_cmp cmp -> "(Ocmp " ^ print_cmp cmp ^ ")"
    100110  | AST.Op_cmpu cmp -> "(Ocmpu " ^ (print_cmp cmp) ^ ")"
    101   | AST.Op_cmpf cmp -> "(Ocmpf " ^ (print_cmp cmp) ^ ")"
    102111  | AST.Op_addp -> "Oaddp"
    103   | AST.Op_subp -> "Osubp"
    104   | AST.Op_cmpp cmp -> (print_cmp cmp) ^ "Ocmpp"
    105 
    106 
    107 let print_addressing = function
    108   | RTLabs.Aindexed off -> Printf.sprintf "Aindexed (repr %d)" off
    109   | RTLabs.Aindexed2 -> "Aindexed2"
    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
    112   | RTLabs.Ainstack off -> Printf.sprintf "Ainstack (repr %d)" off
    113 
    114 
    115 let print_sig_type = function
    116 | AST.Sig_int -> "ASTint"
    117 | AST.Sig_float -> "ASTfloat"
    118 | AST.Sig_ptr -> "ASTptr Any"
     112  | AST.Op_subp -> "Osubpi"
     113  | AST.Op_subpp -> "Osubpp"
     114  | AST.Op_cmpp cmp -> "(Ocmpp " ^ (print_cmp cmp) ^ ")"
     115
     116
    119117
    120118let print_sig s =
     
    152150        (Register.print srcs2)
    153151        lbl
    154   | RTLabs.St_load (chunk, mode, args, dests, lbl) ->
    155       Printf.sprintf "make_St_load %s (%s) %s %s %s"
     152  | RTLabs.St_load (chunk, addr, dests, lbl) ->
     153      Printf.sprintf "make_St_load %s %s %s %s"
    156154        (print_quantity chunk)
    157         (print_addressing mode)
    158         (print_args args)
     155        (Register.print addr)
    159156        (Register.print dests)
    160157        lbl
    161   | RTLabs.St_store (chunk, mode, args, srcs, lbl) ->
    162       Printf.sprintf "make_St_store %s (%s) %s %s %s"
     158  | RTLabs.St_store (chunk, addr, srcs, lbl) ->
     159      Printf.sprintf "make_St_store %s %s %s %s"
    163160        (print_quantity chunk)
    164         (print_addressing mode)
    165         (print_args args)
     161        (Register.print addr)
    166162        (Register.print srcs)
    167163        lbl
    168164  | RTLabs.St_call_id (f, args, res, sg, lbl) ->
    169       Printf.sprintf "make_St_call_id id_%s %s (Some ? %s) %s"
     165      Printf.sprintf "make_St_call_id id_%s %s (%s) %s"
    170166        f
    171167        (print_params args)
    172         (Register.print res)
     168        (match res with None -> "None ?" | Some res -> "Some ? " ^ Register.print res)
    173169        lbl
    174170  | RTLabs.St_call_ptr (f, args, res, sg, lbl) ->
    175       Printf.sprintf "make_St_call_ptr %s %s (Some ? %s) %s"
     171      Printf.sprintf "make_St_call_ptr %s %s (%s) %s"
    176172        (Register.print f)
    177173        (print_params args)
    178         (Register.print res)
     174        (match res with None -> "None ?" | Some res -> "Some ? " ^ (Register.print res))
    179175        lbl
    180176  | RTLabs.St_tailcall_id (f, args, sg) ->
     
    186182        (Register.print f)
    187183        (print_params args)
    188   | RTLabs.St_condcst (cst, lbl_true, lbl_false) ->
    189       Printf.sprintf "make_St_condcst (%s) %s %s"
    190         (print_cst cst)
    191         lbl_true
    192         lbl_false
    193   | RTLabs.St_cond1 (op1, srcs, lbl_true, lbl_false) ->
    194       Printf.sprintf "make_St_cond1 %s %s %s %s"
    195         (print_op1 op1)
     184  | RTLabs.St_cond (srcs, lbl_true, lbl_false) ->
     185      Printf.sprintf "make_St_cond %s %s %s"
    196186        (Register.print srcs)
    197         lbl_true
    198         lbl_false
    199   | RTLabs.St_cond2 (op2, srcs1, srcs2, lbl_true, lbl_false) ->
    200       Printf.sprintf "make_St_cond2 %s %s %s %s %s"
    201         (print_op2 op2)
    202         (Register.print srcs1)
    203         (Register.print srcs2)
    204187        lbl_true
    205188        lbl_false
     
    247230let print_internal_decl n f def =
    248231  Printf.sprintf
    249     "%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."
     232    "%sdefinition id_%s := ident_of_nat %d.\n%s%s\n\n%sdefinition pre_%s := mk_pre_internal_function\n%s%s\n%s%s\n%s%s\n%s%d\n%s%s\n%s%s\n%s%s."
    250233    (n_spaces n)
    251234    f
     
    256239    f
    257240    (n_spaces (n+2))
    258     (print_sig def.RTLabs.f_sig)
    259     (n_spaces (n+2))
    260241    (print_result def.RTLabs.f_result)
    261242    (n_spaces (n+2))
    262     (print_params def.RTLabs.f_params)
     243    (print_locals def.RTLabs.f_params)
    263244    (n_spaces (n+2))
    264245    (print_locals def.RTLabs.f_locals)
    265246    (n_spaces (n+2))
    266     (print_locals def.RTLabs.f_ptrs)
    267     (n_spaces (n+2))
    268     def.RTLabs.f_stacksize
     247    (Driver.RTLabsMemory.concrete_size def.RTLabs.f_stacksize)
    269248    (n_spaces (n+2))
    270249    (print_graph (n+2) def.RTLabs.f_graph)
  • src/RTLabs/import.ma

    r882 r898  
    1313
    1414record pre_internal_function : Type[0] ≝
    15 { pf_sig       : signature
    16 ; pf_result    : option pre_register
    17 ; pf_params    : list pre_register
    18 ; pf_locals    : list pre_register
    19 ; pf_ptrs      : list pre_register
     15{ pf_result    : option (pre_register × typ)
     16; pf_params    : list (pre_register × typ)
     17; pf_locals    : list (pre_register × typ)
    2018; pf_stacksize : nat
    2119; pf_graph     : list (nat × ((pre_register → res register) → (nat → res label) → res statement))
     
    3634
    3735definition make_registers_list :
    38   (nat → option register) → list pre_register → universe RegisterTag →
    39   res ((nat → option register) × (universe RegisterTag) × (list register)) ≝
     36  (nat → option register) → list (pre_register × typ) → universe RegisterTag →
     37  res ((nat → option register) × (universe RegisterTag) × (list (register×typ))) ≝
    4038λm,lrs,g.
    41 foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
     39foldr ?? (λrst,acc. do 〈acc',l〉 ← acc;
     40                   let 〈rs,ty〉 ≝ rst in
    4241                   let 〈m,g〉 ≝ acc' in
    4342                   do 〈mg,rs'〉 ← make_register m rs g;
    44                    OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
     43                   OK ? 〈mg,〈rs',ty〉::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
    4544
    4645axiom MissingRegister : String.
     
    5251  do 〈rmapgen1, result〉 ← match pf_result pre_f with
    5352                          [ None ⇒ OK ? 〈〈λ_.None ?, rgen0〉, None ?〉
    54                           | Some r ⇒ do 〈x,y〉 ← make_register (λ_.None ?) r rgen0; OK ? 〈x,Some ? y
     53                          | Some rt ⇒ do 〈x,y〉 ← make_register (λ_.None ?) (\fst rt) rgen0; OK ? 〈x,Some ? 〈y,\snd rt〉
    5554                          ];
    5655  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
     
    5958  do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
    6059  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
    61   do 〈rmapgen4, ptrs〉 ← make_registers_list rmap3 (pf_ptrs pre_f) rgen3;
    62   let 〈rmap4, rgen4〉 ≝ rmapgen4 in
    63   let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap4 n) in
     60  let rmap ≝ λn. opt_to_res … (msg MissingRegister) (rmap3 n) in
    6461  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    6562  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
     
    7572  OK ? (Internal ? (mk_internal_function
    7673         gen
    77          rgen4
    78          (pf_sig pre_f)
     74         rgen3
    7975         result
    8076         params
    8177         locals
    82          ptrs
    8378         (pf_stacksize pre_f)
    8479         graph
     
    9994].
    10095
    101 definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_register (addr_mode_args m) → res (addr m) ≝
    102 λmp,m. mmap_vec ?? mp ?.
    103 
    10496definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝
    10597λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ].
     
    110102let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src' ← r src; do l' ← f l; OK ? (St_op1 op dst' src' l').
    111103let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do src1' ← r src1; do src2' ← r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
    112 let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l').
    113 let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l').
     104let rec make_St_load chunk addr dst l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do dst' ← r dst; do l' ← f l; OK ? (St_load chunk addr' dst' l').
     105let rec make_St_store chunk addr src l ≝ λr:nat → res register.λf:nat → res label. do addr' ← r addr; do src' ← r src; do l' ← f l; OK ? (St_store chunk addr' src' l').
    114106let rec make_St_call_id id args dst l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_id id args' dst' l').
    115107let rec make_St_call_ptr frs args dst l ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; do dst' ← make_opt_reg r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' l').
    116108let rec make_St_tailcall_id id args ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args').
    117109let rec make_St_tailcall_ptr frs args ≝ λr:nat → res register.λf:nat → res label. do frs' ← r frs; do args' ← make_reg_list r args; OK statement (St_tailcall_ptr frs' args').
    118 let rec make_St_condcst cst ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_condcst cst ltrue' lfalse').
    119 let rec make_St_cond1 op src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond1 op src' ltrue' lfalse').
    120 let 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').
     110let rec make_St_cond src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond src' ltrue' lfalse').
    121111let 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').
    122112definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
Note: See TracChangeset for help on using the changeset viewer.