Ignore:
Timestamp:
Apr 21, 2011, 7:24:04 PM (9 years ago)
Author:
campbell
Message:

Most of the Cminor to RTLabs stage.

Is buggy, generates inefficient RTLabs in a couple of places and is missing
St_switch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r765 r766  
    22(* XXX NB: I haven't checked all of these semantics against the prototype
    33           compilers yet! *)
     4
     5include "utilities/lists.ma".
    46
    57include "common/Errors.ma".
     
    9092
    9193
    92 (* XXX put somewhere sensible *)
    93 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
    94 match l with
    95 [ nil ⇒ None ?
    96 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
    97 ].
    9894
    9995definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
Note: See TracChangeset for help on using the changeset viewer.