Changeset 898 for src/RTLabs/import.ma


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

Update pretty printers and examples.

File:
1 edited

Legend:

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