Merge branch 'outputs_pre'

Author: simondfoster

ROOT

@@ -1,4 +1,4 @@
-session "Z_Machines" = "ITree_UTP" +
+session "Z_Machines" = "ITree_VCG" +
   options [timeout = 600, document = false]
   sessions
     Explorer

Z_Animator.thy

@@ -22,15 +22,15 @@ removeSubstr :: String -> String -> String;
 removeSubstr w "" = "";
 removeSubstr w s@(c:cs) = (if w `isPrefixOf` s then Prelude.drop (Prelude.length w) s else c : removeSubstr w cs);
 
-data EventCont p = InputEvtCont [(String, p)] | OutEvtCont (String, p)
+data EventCont p = MultiEvtCont [(String, p)] | SingleEvtCont (String, p)
 
 showEventCont :: (String, EventCont p) -> String
-showEventCont (n, InputEvtCont _) = n
-showEventCont (n, OutEvtCont (v, _)) = n ++ " " ++ v
+showEventCont (n, MultiEvtCont _) = n
+showEventCont (n, SingleEvtCont (v, _)) = n ++ " " ++ v
 
 eventHierarchy :: [(String, p)] -> [(String, EventCont p)]
 eventHierarchy m = map (\c -> (c,
-                              (\es -> if length es == 1 then OutEvtCont (head es) else InputEvtCont es)
+                              (\es -> if length es == 1 then SingleEvtCont (head es) else MultiEvtCont es)
                               $ map (\(e, p) -> (tail (dropWhile (\x -> x /= ' ') e), p)) 
                               $ filter (isPrefixOf (c ++ " ") . fst) m)) chans
   where
@@ -48,30 +48,35 @@ animate_cnt n (Sil p) =
 animate_cnt n (Vis (Pfun_of_alist [])) = putStrLn "Deadlocked.";
 animate_cnt n t@(Vis (Pfun_of_alist m)) = 
   do { putStrLn ("Operations:" ++ concat (map (\(n, e) -> " (" ++ show n ++ ") " ++ e ++ ";") (zip [1..] (map showEventCont eh))));
+       putStr ("Choose [1-" ++ show (length eh) ++ "]: ");
        e <- getLine;
        if (e == "q" || e == "Q") then
          putStrLn "Animation terminated"
        else
        case (reads e) of
-         []       -> do { putStrLn "No parse"; animate_cnt n t }
-         [(v, _)] -> if (v > length eh)
-                       then do { putStrLn "Rejected"; animate_cnt n t }
-                       else case (snd (eh !! (v - 1))) of
-                              InputEvtCont opts -> 
-                                do { putStrLn ("Parameters:" ++ concat (map (\(n, e) -> " (" ++ show n ++ ") " ++ e ++ ";") (zip [1..] (map fst opts))))
-                                   ; e <- getLine
-                                   ; case (reads e) of
-                                       []       -> do { putStrLn "No parse"; animate_cnt n t }
-                                       [(v, _)] -> if (v > length opts)
-                                                   then do { putStrLn "Rejected"; animate_cnt n t }
-                                                   else animate_cnt 0 (snd (opts !! (v - 1)))
-
-                                   }
-                              OutEvtCont (_, p) -> animate_cnt 0 p
+         []       -> do { putStrLn "Invalid choice, try again."; animate_cnt n t }
+         [(v, _)] -> 
+           if (v > length eh)
+           then do { putStrLn "Rejected"; animate_cnt n t }
+           else case (snd (eh !! (v - 1))) of
+                  MultiEvtCont opts -> 
+                    do { putStrLn ("Parameters:" ++ concat (map (\(n, e) -> " (" ++ show n ++ ") " ++ e ++ ";") (zip [1..] (map fst opts))))
+                       ; putStr ("Choose [1-" ++ show (length opts) ++ "]: ")
+                       ; e <- getLine
+                       ; case (reads e) of
+                           []       -> do { putStrLn "No parse"; animate_cnt n t }
+                           [(v, _)] -> if (v > length opts)
+                                       then do { putStrLn "Rejected"; animate_cnt n t }
+                                       else case snd (opts !! (v - 1)) of 
+                                              Vis (Pfun_of_alist [(e, p')]) -> 
+                                                do { putStrLn ("Response: " ++ show e); putStrLn ""; animate_cnt 0 p' }   
+  
+                       }
+                  SingleEvtCont (_, Vis (Pfun_of_alist [(e, p')])) -> do { putStrLn ("Response: " ++ show e); putStrLn ""; animate_cnt 0 p' }
      }                                                            
   where eh = eventHierarchy (map (\(e, p) -> (Prelude.show e, p)) m);
 animate :: (Eq e, Prelude.Show e, Prelude.Show s) => Itree e s -> Prelude.IO ();
-animate p = do { hSetBuffering stdout NoBuffering; putStrLn ""; putStrLn "Starting Animation..."; animate_cnt 0 p }
+animate p = do { hSetBuffering stdout NoBuffering; putStrLn ""; putStrLn "Starting Animation..."; putStrLn ""; animate_cnt 0 p }
 \<close>
 
 ML \<open> 

Z_Machine.ML

@@ -5,8 +5,8 @@ structure Z_Machine = struct
 type param = string * string
 
 datatype operation_body =
-  OperDefn of {params: param list, pre: string list, update: string, guard: string list} |
-  OperComp of {params: param list, body: string} |
+  OperDefn of {params: param list, pre: string list, update: string, output: string} |
+  OperComp of {params: param list, pre: string list, body: string} |
   OperProm of {promop: string, plens: string} |
   OperEmit of {emit: string}
 
@@ -52,7 +52,7 @@ fun mk_chan_show_fun tname ops ctx =
   let val typ = Syntax.read_typ ctx tname in
   Function_Fun.add_fun 
     [(Binding.name ("show_" ^ tname), SOME (typ --> @{typ "String.literal"}), NoSyn)]
-    (map (fn n => ((Binding.empty_atts, mk_chan_show_eq n ctx), [], [])) ops)
+    (map (fn n => ((Binding.empty_atts, mk_chan_show_eq n ctx), [], [])) (ops @ map (fn n => n ^ "_Out") ops))
     (Function_Fun.fun_config) ctx
   end
 
@@ -72,25 +72,23 @@ fun zop_update n = n ^ "_update"
 
 (* FIXME: Guard ~> Precondition, Postcondition ~> Guard *)
 
+fun gen n ty term ctx = snd (Local_Theory.define 
+  ((Binding.name n, NoSyn)
+  , ((Binding.name (n ^ "_def")
+  , @{attributes [code_unfold, z_defs]})
+  , Syntax.check_term ctx (Type.constraint ty term))) ctx);
+
 fun def_zop n set st body ctx = 
   let open Syntax; open HOLogic; open Local_Theory
       val parm = dest_setT (range_type (Term.type_of (check_term ctx set)))
   in
      (* Generate the type of the operation (i.e. the set of possible parameter values *)
-     snd (define 
-           ((Binding.name (zop_type n), NoSyn)
-         , ((Binding.name (zop_type n ^ "_def")
-           , @{attributes [code_unfold, z_defs]})
-           , check_term ctx set)) ctx) |>
-     (* Generate the precondition *)
-     snd o define 
-           ((Binding.name n, NoSyn)
-         , ((Binding.name (n ^ "_def")
-           (* It would be better if we could mark these as "code" rather than "code_unfold" to retain
-              the structure in the language target. For now, code_unfold is required to ensure that
-              the semantics of enumerated inputs is correctly calculated *)
-           , @{attributes [code_unfold, z_defs]})
-           , check_term ctx (Type.constraint (parm --> st --> dummyT) body)))
+     gen (zop_type n) dummyT (check_term ctx set) ctx |>
+     (* Generate the operation body *)
+     (* It would be better if we could mark these as "code" rather than "code_unfold" to retain
+        the structure in the language target. For now, code_unfold is required to ensure that
+        the semantics of enumerated inputs is correctly calculated *)
+     gen n (parm --> st --> dummyT) body
   end
 
 fun mk_zinit (Init {name = n, state = s, update = upd}) ctx =
@@ -103,30 +101,30 @@ fun mk_zinit (Init {name = n, state = s, update = upd}) ctx =
            , check_term ctx (Type.constraint (st --> st) (parse_term ctx upd)))) ctx)
   end;
 
-fun mk_zop (Operation {name = n, state = s, body = OperDefn {params = ps, pre = pre, update = upd, guard = g}}) ctx =
+fun mk_zop (Operation {name = n, state = s, body = OperDefn {params = ps, pre = pre, update = upd, output = ot}}) ctx =
   let open Syntax; open Library; open Logic; open HOLogic; open Lift_Expr
       val pss = (map (fn (p, t) => (p, lift_expr ctx ((parse_term ctx t)))) ps)
       val pset = params_set (map snd pss)
       val set = SEXP $ pset
       val parm = dest_setT (range_type (Term.type_of (check_term ctx set)))
       val st = read_typ ctx s
       val ppat = mk_tuple (map (free o fst) pss)
+
       val ppre = 
-         lambda (free state_id) 
-                (mk_lift_expr ctx (foldr1 mk_conj ((map (parse_term ctx) pre))) $ Bound 0) 
-      val pguard = 
          lambda (free state_id) 
                 (mk_conj (const @{const_name Set.member} $ ppat $ (pset $ Bound 0)
-                         , mk_lift_expr ctx (foldr1 mk_conj ((map (parse_term ctx) g))) $ Bound 0)) 
-
+                         , mk_lift_expr ctx (foldr1 mk_conj ((map (parse_term ctx) pre))) $ Bound 0)) 
+      val poutput = 
+         lambda (free state_id) 
+                ((mk_lift_expr ctx (parse_term ctx ot)) $ Bound 0) 
       val body = ( 
               (Const (@{const_name "mk_zop"}, (parm --> st --> dummyT) --> dummyT)
                 $ tupled_lambda ppat (SEXP $ ppre))
                 $ tupled_lambda ppat (Type.constraint (st --> st) (parse_term ctx upd))
-                $ tupled_lambda ppat (SEXP $ pguard)
+                $ tupled_lambda ppat (SEXP $ poutput)
                 )
-
-  in def_zop n set st body ctx
+  in def_zop n set st body ctx 
+     |> gen (zop_pre n) (parm --> st --> dummyT) (tupled_lambda ppat (SEXP $ ppre))
   end |
      (*
      (* Generate the precondition *)
@@ -144,36 +142,56 @@ mk_zop (Operation {name = n, state = s, body = OperProm {promop = opr, plens = l
   let open Syntax; open Lift_Expr
       val opr' = read_term ctx opr; 
       val pn = fst (dest_Const opr');
-      val opr_type = const (pn ^ "_type"); 
+      val opr_type = const (zop_type pn);
+      val opr_pre = const (zop_pre pn);
       val lens' = parse_term ctx lens 
       val st = read_typ ctx s
       val set = check_term ctx (const @{const_name "promoted_type"} $ lens' $ const @{const_name collection_lens} $ opr_type)
+      val ppre = check_term ctx (const @{const_name "promote_pre"} $ lens' $ const @{const_name collection_lens} $ opr_pre)
       val body = const @{const_name "promote_operation"} $ lens' $ const @{const_name collection_lens} $ const pn
   in def_zop n set st body ctx
+     |> gen (zop_pre n) (dummyT --> st --> dummyT) ppre
   end |
-mk_zop (Operation {name = n, state = s, body = OperComp {params = ps, body = bdy}}) ctx =
+mk_zop (Operation {name = n, state = s, body = OperComp {params = ps, pre = pre, body = bdy}}) ctx =
   let open Syntax; open Library; open Logic; open HOLogic; open Lift_Expr
       val pss = (map (fn (p, t) => (p, lift_expr ctx ((parse_term ctx t)))) ps)
       val pset = params_set (map snd pss)
       val set = SEXP $ pset
+      val parm = dest_setT (range_type (Term.type_of (check_term ctx set)))
       val st = read_typ ctx s
       val ppat = mk_tuple (map (free o fst) pss)
+      val ppre = 
+         lambda (free state_id) 
+                (mk_lift_expr ctx (foldr1 mk_conj ((map (parse_term ctx) pre))) $ Bound 0)
       val body = tupled_lambda ppat (Type.constraint (st --> dummyT) (parse_term ctx bdy))
   in def_zop n set st body ctx
+     |> gen (zop_pre n) (parm --> st --> dummyT) (tupled_lambda ppat (SEXP $ ppre))
  end |
 mk_zop (Operation {name = n, state = s, body = OperEmit {emit = e}}) ctx =
   let open Syntax; open HOLogic; open Lift_Expr
   val set = mk_lift_expr ctx (mk_set dummyT [parse_term ctx e])
   val st = read_typ ctx s
+  val parm = dest_setT (range_type (Term.type_of (check_term ctx set)))
   val body = const @{const_abbrev emit_op}
-  in def_zop n set st body ctx
+  in def_zop n set st body ctx 
+     (* Generate precondition *)
+     |> gen (zop_pre n) (parm --> st --> dummyT) (Abs ("p", parm, SEXP $ lambda (free state_id) @{term True}))
   end;
 
 fun get_zop_ptype n ctx =
   case Proof_Context.read_const {proper = false, strict = false} ctx n of
     Const (_, Type (@{type_name fun}, [a, _])) => a |
     _ => raise Match;
-      
+    
+fun get_zop_outtype n ctx = 
+  case Proof_Context.read_const {proper = false, strict = false} ctx n of
+    Const (_, Type (@{type_name fun}, 
+              [_, Type (@{type_name fun}, 
+                  [_, Type (@{type_name itree}, 
+                      [_, Type (@{type_name prod}, [a, _])])])])) => a |
+    _ => raise Match;
+
+  
 fun read_const_name ctx n =
   case Proof_Context.read_const {proper = false, strict = false} ctx n of
     Const (n', _) => n' |
@@ -184,7 +202,12 @@ fun zmachine_body_sem n st init inve ops ends ctx =
   let open Syntax; open HOLogic; open Proof_Context
       val oplist = 
             mk_list dummyT 
-              (map (fn n => const @{const_name zop_event} $ read_const {proper = false, strict = false} ctx (firstLower n) $ const (read_const_name ctx (zop_type n)) $ const (read_const_name ctx n)) ops)
+              (map (fn n => const @{const_name zop_event} 
+                            $ read_const {proper = false, strict = false} ctx (firstLower n) 
+                            $ const (read_const_name ctx (zop_type n))
+                            $ const (read_const_name ctx (zop_pre n)) 
+                            $ read_const {proper = false, strict = false} ctx (firstLower n ^ "_Out") 
+                            $ const (read_const_name ctx n)) ops)
   in snd (Local_Theory.define 
            ((Binding.name n, NoSyn)
          , ((Binding.name (n ^ "_def")
@@ -196,7 +219,8 @@ fun chantype_name n = n ^ "_chan"
 
 fun zmachine_sem (ZMachine {name = n, state = s, init = i, inv = inv, operations = ops, ends = e}) ctx =
   let open Syntax; open HOLogic; open Lift_Expr
-    val cs = map (fn n => (firstLower n, YXML.content_of (string_of_typ ctx (get_zop_ptype n ctx)))) ops
+    val cs = map (fn n => (firstLower n, YXML.content_of (string_of_typ ctx (get_zop_ptype n ctx)))) ops @
+             map (fn n => (firstLower n ^ "_Out", YXML.content_of (string_of_typ ctx (get_zop_outtype n ctx)))) ops
     val st = read_typ ctx s
     val inve = mk_lift_expr ctx (parse_term ctx inv)
     val init = parse_term ctx i
@@ -216,14 +240,15 @@ val parse_operdefn =
   ((Scan.optional (@{keyword "params"} |-- repeat1 parse_param) []) --
   (Scan.optional (@{keyword "pre"} |-- repeat1 term) ["True"]) --
   (Scan.optional (@{keyword "update"} |-- term) "[\<leadsto>]") --
-  (Scan.optional (@{keyword "where"} |-- repeat1 term) ["True"])
-  >> (fn (((ps, g), upd), post) => OperDefn {params = ps, pre = g, update = upd, guard = post}))
+  (Scan.optional (@{keyword "output"} |-- term) "()")
+  >> (fn (((ps, g), upd), ot) => OperDefn {params = ps, pre = g, update = upd, output = ot}))
   end
 
 val parse_opercomp = 
   let open Scan; open Parse in
   ((@{keyword "params"} |-- repeat1 parse_param) --
-  (@{keyword "is"} |-- term)) >> (fn (ps, bdy) => OperComp {params = ps, body = bdy})
+  (Scan.optional (@{keyword "pre"} |-- repeat1 term) ["True"]) --
+  (@{keyword "is"} |-- term)) >> (fn ((ps, pre), bdy) => OperComp {params = ps, pre = pre, body = bdy})
   end
 
 val parse_operprom =