(* -------------------------------------------------- *)
(*                       Thread LTSs                  *)
(* -------------------------------------------------- *)



open HolKernel Parse boolLib

val _ = new_theory "TNet_threadAx";
  
open bossLib
  
local open TNet_LIBinterfaceTheory in end;

open TNet_typesTheory

val Term = Parse.Term  (* hack to get parsing right *)

(* need a type of thread labels - can't simply reuse 'label', as that
involves thread ids and host ids.  Note we have to use
Lt_callHostCreateOut instead of the create from LIB_interface and that
the labels now might contain states, so are polymorphic here. *)

val _ =
    Hol_datatype
      `Lthread = Lt_callModuleIn of MODULE_interface
               | Lt_callHostOut of LIB_interface
               | Lt_callHostCreateOut of 'a 
               | Lt_callStoreOut of STORE_interface
               | Lt_RetHostIn of  TLang    
               | Lt_RetStoreIn of  TLang   
               | Lt_RETOut of  TLang       
               | Lt_tau`;


(* added the various sets of states to the data, to simplify later
statement of instep.  Note that (due to the style of formalisation of
LIB) the Call(f) states that we had in the TACS paper are now Call(f
v) states. *)

val _ =
    Hol_datatype
      `thread = <| initial : 'a;
                   transition : 'a -> 'a -> 'a Lthread -> bool ;
                   Module : 'a -> bool ;
                   CallHost : LIB_interface -> 'a -> bool ;
                   CallHostCreate : 'a -> bool ;
                   CallStore : STORE_interface -> 'a -> bool ;
                   RetHosttl : TLang_type -> 'a -> bool ;
                   RetStoretl : TLang_type -> 'a -> bool ;
                   RETtl : TLang_type -> 'a -> bool ;
                   Tau  : 'a -> bool ;
                   Term : 'a -> bool ;
                   Rettl : TLang_type -> 'a -> bool ;
                   Prog : 'a -> bool |>`;

val reachable_def =
    Define`reachable t s = RTC (\s0 s. ?l. t.transition s0 s l) t.initial s`;


val pairwise_disjoint_def = Define `
  pairwise_disjoint x = !u v. u IN x /\ v IN x /\ (u<>v) ==> DISJOINT u v`;

 



val thread_ok_def =
 Define `thread_ok t =
     (t.Prog = t.Tau UNION 
             { s | ?fh. s IN (t.CallHost fh)} UNION 
             t.CallHostCreate UNION 
             { s | ?fs. s IN (t.CallStore fs)} UNION 
             { s | ?tlty . s IN (t.RETtl tlty) })               /\

     (!tlty . t.Rettl tlty = ((t.RetHosttl tlty) UNION (t.RetStoretl tlty))) /\

     (* each reachable state is in at least one of the sets *)
     (!s. s IN reachable t ==>
          (s IN t.Module) \/
          (s IN t.Prog) \/
          (?tlty. s IN t.Rettl tlty) \/
          (s IN t.Term)) /\



     (* the sets are disjoint (needs an aux defn) *)
     (pairwise_disjoint ({ t.Module; t.CallHostCreate; t.Tau ; t.Term}  UNION
                       { t.CallHost fhv  | T } UNION
                       { t.CallStore fsv | T } UNION
                       { t.RetHosttl tl  | T } UNION
                       { t.RetStoretl tl | T } UNION
                       { t.RETtl tl      | T }  )) /\ 


    (* no bogus create labels *)                
    (!s s'.  ~ (t.transition s s' (Lt_callHostOut (create () )))) /\

    (* transitions with each kind of label are between the proper kinds of states,
       and create labels are sensible
       and Ret and RET labels have the right types  *)
    (!s s' fmv. (t.transition s s' (Lt_callModuleIn fmv)) ==> s  IN t.Module /\ 
                                                        s' IN t.Prog)/\

    (!s s' fv. (t.transition s s' (Lt_callHostOut fv)) ==> s  IN t.CallHost fv /\ 
                                                           s' IN t.Rettl (retType fv))/\

    (!s s' s2. (t.transition s s' (Lt_callHostCreateOut s2)) ==>( s  IN t.CallHostCreate)  /\ 
                                             (s' IN (t.Rettl (retType (create ())))) /\
                                             s2 IN t.Prog )/\

    (!s s' fv. (t.transition s s' (Lt_callStoreOut fv)) ==> s  IN t.CallStore fv /\ 
                                                            s' IN t.Rettl (retTypeST fv))/\

    (!s s' v . (t.transition s s' (Lt_RetHostIn  v)) ==> ?tlty. s  IN (t.RetHosttl tlty) /\ 
                                                         s' IN t.Prog   /\
                                                         tlang_typing v tlty )/\

    (!s s' v . (t.transition s s' (Lt_RetStoreIn v)) ==> ?tlty. s  IN (t.RetStoretl tlty) /\ 
                                                         s' IN t.Prog   /\
                                                         tlang_typing v tlty )/\

    (!s s' v . (t.transition s s' (Lt_RETOut  v)) ==> ?tlty. s  IN (t.RETtl tlty) /\ 
                                                          s' IN t.Term   /\
                                                          tlang_typing v tlty  )/\

    (!s s'. (t.transition s s' (Lt_tau))            ==> s IN t.Tau    /\ s' IN t.Prog)/\



    (* No per-label nondeterminism except for internal moves *)
    (! s s' s'' l. (l<>Lt_tau) /\ t.transition s s' l /\ t.transition s s'' l ==> (s'=s''))/\


    (* Module Init states can receive all possible calls*)
    (! s gv. s IN t.Module ==> ?s' . t.transition s s' (Lt_callModuleIn gv))/\


    (* Prog states are not stuck *)
    (! s. s IN t.Prog ==> ?s' l. t.transition s s' l)/\


    (* Call states can make exactly one call *)
    (* this is implied by the condiitons above, as CallHost and CallStore take an fv not an f*)


     (*Ret states can accept all values (of the right type...)*)
     (!tlty s. s IN t.RetHosttl tlty ==>
               (!r. tlang_typing r tlty ==>
                    ?!s'. t.transition s s' (Lt_RetHostIn  r)) ) /\


     (*Ret states can accept all values (of the right type...)*)
     (!tlty s. s IN t.RetStoretl tlty ==>
               (!r. tlang_typing r tlty ==>
                    ?!s'. t.transition s s' (Lt_RetStoreIn r)) ) /\




    (* a RET state reachable from a t.Module via a call g v  is of the 
       result type of g, as specified in MODULE_interface *)
    (! s s' s'' gv tlty. (s IN t.Module /\  
                          t.transition s s' (Lt_callModuleIn gv) /\ 
                          (RTC (\s0 s. ?l. t.transition s0 s l)) s'  s'' /\ 
                          s'' IN t.RETtl tlty ) 
                        ==> (tlty = retTypeM gv))   `  handle e => Raise e;



(* used retTypeM and retTypeST in place of overloaded retType, as HOL seemed not to like them*)


val _ = add_rule { block_style = (AroundEachPhrase, (PP.INCONSISTENT, 0)),
                   paren_style = OnlyIfNecessary,
                   fixity = Infix(NONASSOC, 420),
                   pp_elements = [HardSpace 1, TOK "---", HardSpace 1,
                                  TM (* label *), HardSpace 1,
                                  TOK "->>>", BreakSpace(1,0)],
                   term_name = "transition4"
                   };

val thread_lts'_def = Define`
  thread_lts' t l t' =  ?s'. (t.transition t.initial s' l )/\ (t'=t with initial :=s')`;

val _ = overload_on ("transition4", ``thread_lts'``);




val _ = export_theory();