Changeset 1233 for src/RTL

Timestamp:

Sep 21, 2011, 11:57:20 AM (9 years ago)

Author:

sacerdot

Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File:

• src/RTL/semantics.ma (modified) (1 diff)

src/RTL/semantics.ma

@@ -264 +264 @@
      [ nil ⇒ Some ? (smerge2 v)
      | _ ⇒ None ? ]].
-
+(*
 definition RTL_exec : execstep io_out io_in ≝
   mk_execstep … ? is_final mem_of_state eval_statement.
-
+*)
 (* CSC: XXX the program type does not fit with the globalenv and init_mem
 definition make_initial_state : rtl_program → res (genv × state) ≝