Changeset 898 for src/RTLabs


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

Update pretty printers and examples.

Location:
src/RTLabs
Files:
2 added
2 edited

Legend:

Unmodified
Added
Removed
  • 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.