sketch.txt

REPRESENTATION:

  state s          state t

                   the global system clock as 'a word

  store_clocks --> global vars in Pancake, each as 'a word

  wait NONE    --> as 0w in wait_set var   -- never wake me up (unless there is an input)
  wait SOME c  --> wait_set is 1w          -- some wake up time is present
               --> wake_up_at is c as 'a word

  location     --> Lab funname   (where the code for location is implemented in funname)


state_rel:

     s.clocks A = t.sys_time - t.locals "A_time"

     IS_SOME (s.wait) <=> t.locals "wait_set" = 1w

     s.wait = SOME c ==>
       c = t.locals "wake_up_at" - t.sys_time


IMPLEMENTATION:

  sketch:

    input_received = false;
    input = null;
    sys_time = get_time_now();
    while ((wait_set ==> sys_time < wake_up_at) && !input_received) {
      input_received = check_for_input(); // updates input is received
      sys_time = get_time_now();
    }
    Call (Ret (Var "location") NONE) (Var "location") [Var "sys_time"]


timeLang:
  Type program = (location # (term list)) list

  timeLang program turns into the list of Pancake functions

     one should think:  location -> term list

     compile ([]:term list) = Skip /\
     compile (x::xs) = compile_single x (compile xs)

     compiler_single (Term io cond next_loc clocks_to_reset wait) otherwise =
       panLang$If (compile_cond cond)
                 (compile_body io next_loc clocks_to_reset wait)
                 otherwise