Changeset 750 for src/RTLabs/import.ma


Ignore:
Timestamp:
Apr 12, 2011, 12:32:33 PM (9 years ago)
Author:
campbell
Message:

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r738 r750  
    1010].
    1111
    12 definition pre_registers ≝ Sig nat (Vector nat).
     12definition pre_register ≝ nat.
    1313
    1414record pre_internal_function : Type[0] ≝
    1515{ pf_sig       : signature
    16 ; pf_result    : pre_registers
    17 ; pf_params    : list pre_registers
    18 ; pf_locals    : list pre_registers
     16; pf_result    : option pre_register
     17; pf_params    : list pre_register
     18; pf_locals    : list pre_register
     19; pf_ptrs      : list pre_register
    1920; pf_stacksize : nat
    20 ; pf_graph     : list (nat × ((nat → res register) → (nat → res label) → res statement))
     21; pf_graph     : list (nat × ((pre_register → res register) → (nat → res label) → res statement))
    2122; pf_entry     : nat
    2223; pf_exit      : nat
    2324}.
    2425(* XXX projection generation with nat broken *)
    25 definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ s _ _ _ ⇒ s ].
    26 definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ g _ _ ⇒ g ].
    27 definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ e _ ⇒ e ].
    28 definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e ⇒ e ].
     26definition pf_stacksize ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ s _ _ _ ⇒ s ].
     27definition pf_graph ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ g _ _ ⇒ g ].
     28definition pf_entry ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ e _ ⇒ e ].
     29definition pf_exit ≝ λp.match p with [ mk_pre_internal_function _ _ _ _ _ _ _ _ e ⇒ e ].
    2930
    30 definition make_registers :
    31   (nat → option register) → pre_registers → universe RegisterTag →
    32   res ((nat → option register) × (universe RegisterTag) × registers) ≝
    33 λm,rs0,g.
    34 match rs0 with [ dp n rs ⇒
    35   do 〈m,grs〉 ← fold_right_i ??? (λn,r,mr.
    36                   do 〈m,grs〉 ← mr;
    37                   let 〈g,rs〉 ≝ grs in
    38                   match m r with
    39                   [ Some r' ⇒ OK ? 〈m,〈g,r':::rs〉〉
    40                   | None ⇒ do 〈r',g'〉 ← fresh ? g;
    41                            OK ? 〈λn. if eqb r n then Some ? r' else m n,〈g',r':::rs〉〉
    42                   ]) (OK ? 〈m,〈g,[[ ]]〉〉) rs;
    43   let 〈g',rs'〉 ≝ grs in
    44     OK ? 〈〈m,g'〉,dp ?? n rs'〉
    45 ].
     31definition make_register :
     32  (pre_register → option register) → pre_register → universe RegisterTag →
     33  res ((nat → option register) × (universe RegisterTag) × register) ≝
     34λm,reg,g.
     35  match m reg with
     36  [ Some r' ⇒ OK ? 〈〈m,g〉,r'〉
     37  | None ⇒ do 〈r',g'〉 ← fresh ? g;
     38           OK ? 〈〈λn. if eqb reg n then Some ? r' else m n,g'〉,r'〉
     39  ]
     40.
    4641
    4742definition make_registers_list :
    48   (nat → option register) → list pre_registers → universe RegisterTag →
    49   res ((nat → option register) × (universe RegisterTag) × (list registers)) ≝
     43  (nat → option register) → list pre_register → universe RegisterTag →
     44  res ((nat → option register) × (universe RegisterTag) × (list register)) ≝
    5045λm,lrs,g.
    5146foldr ?? (λrs,acc. do 〈acc',l〉 ← acc;
    5247                   let 〈m,g〉 ≝ acc' in
    53                    do 〈mg,rs'〉 ← make_registers m rs g;
     48                   do 〈mg,rs'〉 ← make_register m rs g;
    5449                   OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
    5550
     
    5752λpre_f.
    5853  let rgen0 ≝ new_universe RegisterTag in
    59   do 〈rmapgen1, result〉 ← make_registers (λ_.None ?) (pf_result pre_f) rgen0;
     54  do 〈rmapgen1, result〉 ← match pf_result pre_f with
     55                          [ None ⇒ OK ? 〈〈λ_.None ?, rgen0〉, None ?〉
     56                          | Some r ⇒ do 〈x,y〉 ← make_register (λ_.None ?) r rgen0; OK ? 〈x,Some ? y〉
     57                          ];
    6058  let 〈rmap1, rgen1〉 ≝ rmapgen1 in
    6159  do 〈rmapgen2, params〉 ← make_registers_list rmap1 (pf_params pre_f) rgen1;
     
    6361  do 〈rmapgen3, locals〉 ← make_registers_list rmap2 (pf_locals pre_f) rgen2;
    6462  let 〈rmap3, rgen3〉 ≝ rmapgen3 in
    65   let rmap ≝ λn. opt_to_res … (rmap3 n) in
     63  do 〈rmapgen4, ptrs〉 ← make_registers_list rmap3 (pf_ptrs pre_f) rgen3;
     64  let 〈rmap4, rgen4〉 ≝ rmapgen4 in
     65  let rmap ≝ λn. opt_to_res … (rmap4 n) in
    6666  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    6767  do 〈labels, gen〉 ← n_idents (S max_stmt) ? (new_universe LabelTag);
     
    7676  OK ? (Internal ? (mk_internal_function
    7777         gen
    78          rgen3
     78         rgen4
    7979         (pf_sig pre_f)
    8080         result
    8181         params
    8282         locals
     83         ptrs
    8384         (pf_stacksize pre_f)
    8485         graph
     
    8788         )).
    8889
    89 definition make_regs : (nat → res register) → pre_registers → res registers ≝
    90 λm,p.
    91 match p with
    92 [ dp n ps ⇒
    93     do rs ← fold_right_i ??? (λn,r,rs0.
    94                   do rs ← rs0;
    95                   do r' ← m r;
    96                   OK ? (r':::rs)) (OK ? [[ ]]) ps;
    97     OK ? (dp ?? n rs)
    98 ].
    99 
    100 definition make_regs_list : (nat → res register) → list pre_registers → res (list registers) ≝
    101 λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← make_regs m p; OK ? (r::rs)) (OK ? [ ]) ps.
     90definition make_reg_list : (nat → res register) → list pre_register → res (list register) ≝
     91λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← m p; OK ? (r::rs)) (OK ? [ ]) ps.
    10292
    10393(* XXX move somewhere sensible *)
     
    110100].
    111101
    112 definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_registers (addr_mode_args m) → res (addr m) ≝
    113 λmp,m. mmap_vec ?? (make_regs mp) ?.
     102definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_register (addr_mode_args m) → res (addr m) ≝
     103λmp,m. mmap_vec ?? mp ?.
     104
     105definition make_opt_reg : (pre_register → res register) → option pre_register → res (option register) ≝
     106λm,o. match o with [ None ⇒ OK ? (None ?) | Some r ⇒ do r' ← m r; OK ? (Some ? r') ].
    114107
    115108let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
    116109let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
    117 let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do l' ← f l; OK ? (St_const rs' cst l').
    118 let rec make_St_op1 op dst src l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src' ← make_regs r src; do l' ← f l; OK ? (St_op1 op dst' src' l').
    119 let rec make_St_op2 op dst src1 src2 l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do src1' ← make_regs r src1; do src2' ← make_regs r src2; do l' ← f l; OK ? (St_op2 op dst' src1' src2' l').
    120 let rec make_St_load chunk mode args dst l ≝ λr:nat → res register.λf:nat → res label. do dst' ← make_regs r dst; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_load chunk mode args' dst' l').
    121 let rec make_St_store chunk mode args src l ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do l' ← f l; do args' ← make_addr r ? args; OK ? (St_store chunk mode args' src' l').
    122 let rec make_St_call_id id args dst sig l ≝ λr:nat → res register.λf:nat → res label. do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_id id args' dst' sig l').
    123 let rec make_St_call_ptr frs args dst sig l ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; do dst' ← make_regs r dst; do l' ← f l; OK ? (St_call_ptr frs' args' dst' sig l').
    124 let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_regs_list r args; OK statement (St_tailcall_id id args' sig).
    125 let rec make_St_tailcall_ptr frs args sig ≝ λr:nat → res register.λf:nat → res label. do frs' ← make_regs r frs; do args' ← make_regs_list r args; OK statement (St_tailcall_ptr frs' args' sig).
     110let rec make_St_const rs cst l ≝ λr:nat → res register.λf:nat → res label. do rs' ← r rs; do l' ← f l; OK ? (St_const rs' cst l').
     111let 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').
     112let 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').
     113let 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').
     114let 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').
     115let rec make_St_call_id id args dst sig 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' sig l').
     116let rec make_St_call_ptr frs args dst sig 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' sig l').
     117let rec make_St_tailcall_id id args sig ≝ λr:nat → res register.λf:nat → res label.  do args' ← make_reg_list r args; OK statement (St_tailcall_id id args' sig).
     118let rec make_St_tailcall_ptr frs args sig ≝ λ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' sig).
    126119let 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').
    127 let rec make_St_cond1 op src ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; do ltrue' ← f ltrue; do lfalse' ← f lfalse;  OK ? (St_cond1 op src' ltrue' lfalse').
    128 let rec make_St_cond2 op src1 src2 ltrue lfalse ≝ λr:nat → res register.λf:nat → res label. do src1' ← make_regs r src1; do src2' ← make_regs r src2; do ltrue' ← f ltrue; do lfalse' ← f lfalse; OK ? (St_cond2 op src1' src2' ltrue' lfalse').
    129 let rec make_St_jumptable rs ls ≝ λr:nat → res register.λf:nat → res label. do rs' ← make_regs r rs; do ls' ← foldr ?? (λl,ls0. do ls ← ls0; do l' ← f l; OK ? (l'::ls)) (OK ? [ ]) ls; OK ? (St_jumptable rs' ls').
    130 let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← make_regs r src; OK statement (St_return src').
     120let 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').
     121let 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').
     122let 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').
     123let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; OK statement (St_return src').
    131124
Note: See TracChangeset for help on using the changeset viewer.