Changeset 765 for src/RTLabs/import.ma


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

Remove superfluous register in RTLabs return statements.

Also fix up RTLabs prototype pretty printer's handling of global variables.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/import.ma

    r762 r765  
    121121let 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').
    122122let 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').
    123 let rec make_St_return src ≝ λr:nat → res register.λf:nat → res label. do src' ← r src; OK statement (St_return src').
     123definition make_St_return ≝ λr:nat → res register.λf:nat → res label. OK statement St_return.
    124124
Note: See TracChangeset for help on using the changeset viewer.