Changeset 727 for src/RTLabs/import.ma


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

Enough fixes to let an RTLabs program run.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r726 r727  
    2121[ O ⇒ OK ? 〈[[ ]], g〉
    2222| S m ⇒ do 〈ls, g'〉 ← n_labels m g;
    23         do 〈l, g''〉 ← label_new g;
     23        do 〈l, g''〉 ← label_new g';
    2424        OK ? 〈l:::ls, g''〉
    2525].
     
    2929[ O ⇒ OK ? 〈[[ ]], g〉
    3030| S m ⇒ do 〈ls, g'〉 ← n_regs m g;
    31         do 〈l, g''〉 ← register_new g;
     31        do 〈l, g''〉 ← register_new g';
    3232        OK ? 〈l:::ls, g''〉
    3333].
     
    7777                   OK ? 〈mg,rs'::l〉) (OK ? 〈〈m,g〉,[ ]〉) lrs.
    7878
    79 definition make_internal_function : pre_internal_function → res internal_function
     79definition make_internal_function : pre_internal_function → res (fundef internal_function)
    8080λpre_f.
    8181  let rgen0 ≝ register_gen_new in
     
    8888  let rmap ≝ λn. opt_to_res … (rmap3 n) in
    8989  let max_stmt ≝ foldr ?? (λp,m. max (\fst p) m) 0 (pf_graph pre_f) in
    90   do 〈labels, gen〉 ← n_labels max_stmt label_gen_new;
     90  do 〈labels, gen〉 ← n_labels (S max_stmt) label_gen_new;
    9191  let get_label ≝ λn. opt_to_res … (get_index_weak_v ?? labels n) in
    9292  do graph ← foldr ?? (λp,g0. do g ← g0;
     
    9797  do entry ← get_label (pf_entry pre_f);
    9898  do exit ← get_label (pf_exit pre_f);
    99   OK ? (mk_internal_function
     99  OK ? (Internal ? (mk_internal_function
    100100         gen
    101101         rgen3
     
    108108         entry
    109109         exit
    110          ).
     110         )).
    111111
    112112definition make_regs : (nat → res register) → pre_registers → res registers ≝
     
    124124λm,ps. foldr ?? (λp,rs0. do rs ← rs0; do r ← make_regs m p; OK ? (r::rs)) (OK ? [ ]) ps.
    125125
     126(* XXX move somewhere sensible *)
     127let rec mmap_vec (A:Type[0]) (B:Type[0]) (f:A → res B) (n:nat) (v:Vector A n) on v : res (Vector B n) ≝
     128match v with
     129[ VEmpty ⇒ OK ? (VEmpty …)
     130| VCons m hd tl ⇒ do hd' ← f hd;
     131                  do tl' ← mmap_vec A B f m tl;
     132                  OK ? (hd':::tl')
     133].
     134
     135definition make_addr : (nat → res register) → ∀m:addressing. Vector pre_registers (addr_mode_args m) → res (addr m) ≝
     136λmp,m. mmap_vec ?? (make_regs mp) ?.
     137
    126138let rec make_St_skip l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_skip l').
    127139let rec make_St_cost cl l ≝ λr:nat → res register.λf:nat → res label. do l' ← f l; OK ? (St_cost cl l').
     
    129141let 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').
    130142let 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').
    131 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; OK ? (St_load chunk mode args dst' l').
    132 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; OK ? (St_store chunk mode args src' l').
     143let 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').
     144let 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').
    133145let 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').
    134146let 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').
Note: See TracChangeset for help on using the changeset viewer.