Added syntax to allow programs to return exit values. The executor wi…

…ll only show these, rather than the entire final state.

UTP/ITree_Procedure.ML

@@ -5,7 +5,8 @@ struct
 
 fun mk_program evT (((n, p), st), body) ctx =
   let open Syntax
-      val ty = (check_typ ctx (Type (@{type_abbrev htree}, [evT, read_typ ctx st])))
+      val stT = read_typ ctx st
+      val ty = (check_typ ctx (Type (@{type_abbrev ktree}, [evT, stT, dummyT])))
       val pat = read_term ctx p
       val vs = map (fst o dest_Free) (HOLogic.strip_tuple pat)
       val pat' = HOLogic.mk_tuple (map free vs)

UTP/VCG/ITree_VCG.thy

@@ -34,6 +34,17 @@ syntax
 translations
   "_lens_get_pretty x s" == "CONST lens_get x s"
 
+(* Syntax to allow programs to exit returning a value *)
+
+definition exit_prog :: "('a, 's) expr \<Rightarrow> 's \<Rightarrow> ('e, 'a) itree" where 
+"exit_prog e = (\<lambda> s. Ret (e s))"
+
+syntax "_exit_prog" :: "logic \<Rightarrow> logic" ("exit _")
+translations "exit e" == "CONST exit_prog (e)\<^sub>e"
+
+lemma hl_exit [hoare_safe]: "\<forall> s. (P)\<^sub>e s \<longrightarrow> (Q)\<^sub>e (e s) \<Longrightarrow> H{P} exit e {Q}"
+  by (simp add: exit_prog_def hoare_alt_def)
+
 (* Set up the program and procedure command *)
 
 ML \<open>