Ignore:
Timestamp:
Sep 24, 2010, 10:31:32 AM (10 years ago)
Author:
campbell
Message:

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/test/io.c.ma

    r20 r125  
    2929   ret ? 〈t,s〉).
    3030
     31ninductive result (T:Type) : T → Prop ≝
     32| witness : ∀t:T. result T t.
     33
    3134(* The trick to being able to normalize the term is to avoid looking at the
    3235   continuations! *)
    3336nremark exec_OK:
    34     match match ts with [ Interact f args k ⇒ k (EVint (repr 6))
    35                  | Value v ⇒ Wrong ?
    36                  | Wrong ⇒ Wrong ? ] with
    37     [ Interact _ _ _ ⇒ False
    38     | Value v ⇒ v = v
     37    match match ts with [ Interact call k ⇒ k (EVint (repr 6))
     38                 | Value v ⇒ Wrong ???
     39                 | Wrong ⇒ Wrong ??? ] with
     40    [ Interact _ _ ⇒ False
     41    | Value v ⇒ result ? v
    3942    | Wrong ⇒ False
    4043    ].
Note: See TracChangeset for help on using the changeset viewer.