(*<*) theory ISM_package imports ISM begin ML {* (* Title: ISM_package.ML ID: $Id: ISM_package.ML,v 1.13 2003/09/12 16:13:02 dvo Exp $ Author: Sebastian Nanz, TU Muenchen and David von Oheimb, Siemens AG Definition of Interacting State Machines (ISMs). *) datatype ('a,'b) sum = Inl of 'a | Inr of 'b; fun option_map f NONE = NONE | option_map f (SOME x) = SOME (f x) type ind_def = {defs: thm list, mono: thm, elims: thm list, intrs: thm list, induct: thm, unfold: thm, mk_cases: string -> thm, raw_induct: thm}; signature ISM_PACKAGE = sig type 'a rule val add_ism: string -> (string * string) list -> string -> string -> string -> string -> (string * string option) option -> string option -> (string * (string * string)) option -> (string * (string * string)) option -> string rule list -> theory -> theory * ind_def list * thm list val add_ism_i: string -> (string * typ) list -> typ -> term -> term -> typ -> (typ * term option) option -> typ option -> (typ * (term * string)) option -> (typ * (term * term )) option -> term rule list -> theory -> theory * ind_def list * thm list end; structure ISM_package (*: ISM_PACKAGE*) = struct (*** utilities ***) (** messages and errors **) val quiet_mode = ref false; fun message s = if !quiet_mode then () else writeln s; exception ism_exception; fun ism_error msg = (raise ism_exception) handle ism_exception => error msg; fun no_state_error name = "ISM " ^ quote name ^ " has neither a control nor a data state declaration."; fun no_ctrl_st_error name = "ISM has a control state transition in rule " ^ quote name ^ " but no control state declaration."; fun no_ctrl_trans_error name = "ISM has control state but not control state transitions in rule " ^ quote name ^ "."; fun no_data_st_error name = "ISM has postconditions in transition " ^ quote name ^ " but no data state declaration."; fun field_type_error field_name = "Unable to determine field type for field " ^ quote field_name ^ "."; fun fetch_constr_error l_st_name g_st_name = "Unable to determine a datatype " ^ quote g_st_name ^ "\n that has a single argument of type " ^ quote l_st_name ^ "."; (** constructor of global type **) fun fetch_constr'' l_st_Typ constr_opt [] = constr_opt | fetch_constr'' l_st_Typ constr_opt (constr::rest) = let val (constr_Term, constr_Typ) = constr; val l_st_DTyp = DatatypeAux.dtyp_of_typ [] l_st_Typ; val constr_opt' = if constr_Typ = [l_st_DTyp] then SOME constr_Term else constr_opt; in fetch_constr'' l_st_Typ constr_opt' rest end; fun fetch_constr' l_st_Typ constr_opt [] = constr_opt | fetch_constr' l_st_Typ constr_opt (descr::rest) = let val (_, (_, _, constr)) = descr; val constr_opt' = fetch_constr'' l_st_Typ constr_opt constr; in fetch_constr' l_st_Typ constr_opt' rest end; fun fetch_constr l_st_Typ g_st_Typ thy = let val sign = Theory.sign_of thy; val fetch_constr_err = fetch_constr_error (Sign.string_of_typ sign l_st_Typ) (Sign.string_of_typ sign g_st_Typ); (* determine type name of global state datatype *) val g_st_name = case g_st_Typ of Type (g_st_name, _) => Sign.intern_type sign g_st_name | _ => let val _ = ism_error fetch_constr_err in "" end; (* symbol table lookup *) val symtab_opt = Symtab.lookup (DatatypePackage.get_datatypes thy) g_st_name; val descr_opt = option_map (#descr) symtab_opt; val descr = case descr_opt of SOME descr => descr | NONE => let val _ = ism_error fetch_constr_err in [] end; val constr_opt = fetch_constr' l_st_Typ NONE descr; val constr = case constr_opt of NONE => let val _ = ism_error fetch_constr_err in "" end | SOME(constr) => constr; in constr end; fun mk_global_st_term l_st_Typ g_st_Typ_opt thy t = case g_st_Typ_opt of NONE => t | SOME(g_st_Typ) => Const (fetch_constr l_st_Typ g_st_Typ thy, l_st_Typ --> g_st_Typ) $ t (* end; *) (** helpers **) fun combine [] [] = [] | combine (x::xs) [] = [] | combine [] (y::ys) = [] | combine (x::xs) (y::ys) = (x, y) :: combine xs ys; local fun esc_underscores [] = [] | esc_underscores (x::xs) = if (x = "_") then "'"::x::esc_underscores xs else x::esc_underscores xs; in fun escape_underscores name = implode (esc_underscores (explode name)) end; (*** type handling ***) (* 'a rule is the type of the ism transitions *) type 'a rule = ((bstring * Args.src list) * (('a * 'a) option * ('a option * ('a list * ((('a * bool) * 'a) list * ((('a * bool) * 'a) list * ('a option * (((string * 'a) list, 'a) sum)))))))); val dummyT = Type ("_dummy", []); fun mk_Typ prep_typ sign type_constr = typ_of (prep_typ sign type_constr); fun mk_listT T = Type ("List.list", [T]); (*** term handling ***) val dummy_Term = Const("_dummy", dummyT); fun mk_Term prep_term sign t = term_of (prep_term sign t); fun mk_k_nil_Term sign pt_Typ msg_Typ = let val msgss_Typ = mk_listT msg_Typ; val k_nil_Typ = pt_Typ --> msgss_Typ; val k_nil_Term = Const(Sign.intern_const sign "K_Nil", k_nil_Typ); in (k_nil_Term, k_nil_Typ) end; fun mk_pair_Const sign a_Typ b_Typ = let val pair_Const_Typ = a_Typ --> b_Typ --> HOLogic.mk_prodT (a_Typ, b_Typ); val pair_Const = Const("Pair", pair_Const_Typ); in (pair_Const, pair_Const_Typ) end; fun mk_pair_Term_Typ sign (a_Term, a_Typ) (b_Term, b_Typ) = let val (pair_Const, _) = mk_pair_Const sign a_Typ b_Typ; val pair_Term = pair_Const $ a_Term $ b_Term; val pair_Typ = HOLogic.mk_prodT(a_Typ, b_Typ); in (pair_Term, pair_Typ) end; fun mk_state_opt prep_type prep_term sign = option_map (fn (s_type, (s_term, s_Var)) => let val s_Typ = mk_Typ prep_type sign s_type; val s_Term = mk_Term prep_term sign (s_term, s_Typ); in (s_Term, s_Typ, s_Var) end); (*** transitions ***) (** prepare inputs and outputs **) fun mk_msgss_pat sign pt_Typ msg_Typ = let val msg_list_Typ = mk_listT msg_Typ; val msgss_Typ = pt_Typ --> msg_list_Typ; fun fun_upd_Typ T = msgss_Typ --> T --> msg_list_Typ --> msgss_Typ; val fun_upd_Term = Const (Sign.intern_const sign "fun_upd" , fun_upd_Typ pt_Typ); val fun_upd_s_Term = Const (Sign.intern_const sign "fun_upd_s", fun_upd_Typ (HOLogic.mk_setT pt_Typ)); in Library.foldl (fn (f, ((pat,multi), msgs)) => (if multi then fun_upd_s_Term else fun_upd_Term) $ f $ pat $ msgs) end; (** update record fields (for postconditions) **) (* TODO: I think we don't handle record extensions correctly here... *) fun find_field_Typ sign field_name data_st_Typ = let val record_fields = fst(RecordPackage.get_recT_fields sign data_st_Typ); val found_types = filter (fn x => Sign.base_name(fst(x)) = field_name) record_fields; in case found_types of [] => let val _ = ism_error (field_type_error field_name) in dummyT end | _ => snd(hd(found_types)) end; (* Typ: Context.theory -> Term.typ -> Term.term -> (string * Term.term) list -> Term.term *) fun mk_field_upd sign data_st_Typ r [] = r | mk_field_upd sign data_st_Typ r (post::rest) = let val (field_name, field_Term) = post; val field_Typ = find_field_Typ sign field_name data_st_Typ; val field = Const(Sign.intern_const sign (field_name ^ "_update"), field_Typ --> data_st_Typ --> data_st_Typ) $ field_Term $ r; in mk_field_upd sign data_st_Typ field rest end; (** add premises terms to conclusion term **) fun mk_prems sign concl [] = concl | mk_prems sign concl (pre_Term::rest) = let val impl_Term = Const("==>", propT --> propT --> propT); val concl' = impl_Term $ (HOLogic.mk_Trueprop pre_Term) $ concl; in mk_prems sign concl' rest end; (** transform transition rule (for simultaneous type check) **) (* Typ: (Context.theory -> (''a * Term.typ) list -> Thm.cterm list) -> Context.theory -> (Term.typ * 'b) option * Term.typ * Term.typ * 'c * ('d * ...) option * ... option * ... -> ''a ISM_package.rule -> Term.term option * Term.term ISM_package.rule *) fun transform_rule prep_rule sign types (rule:''a rule) = let val (cmd_Typ_default_opt, pt_Typ, msg_Typ, st_Typ, ctrl_st_Typ_Term_opt, data_st_Typ_Term_opt, l_st_Typ, g_st_Typ_opt, domain_Typ_default_opt) = types; val ((name, args), (cs_exprs, (dom_opt, (pres, (inps, (outps, (cmd_opt, post_v))))))) = rule; val msg_list_Typ = mk_listT msg_Typ; val ctrl_st_Typ = case ctrl_st_Typ_Term_opt of NONE => (case cs_exprs of NONE => dummyT | SOME _ => ism_error (no_ctrl_st_error name)) | SOME (_, typ, _) => (case cs_exprs of NONE => ism_error (no_ctrl_trans_error name) | SOME _ => typ); (* transform rule into Term_Typ list (for prep_rule) *) val l = case data_st_Typ_Term_opt of NONE => [] | SOME(_, data_st_Typ, data_st_var) => [(data_st_var, data_st_Typ)]; val l = l @ (case cs_exprs of NONE => [] | SOME (cs_expr,cs_expr') => [(cs_expr, ctrl_st_Typ), (cs_expr', ctrl_st_Typ)]); val l = l @ (map (fn p => (p, HOLogic.boolT)) pres); val trans_forw_pats = Library.flat o map (fn ((pat, multi), msgs) => [(pat, if multi then HOLogic.mk_setT pt_Typ else pt_Typ), (msgs, msg_list_Typ)]); val l = l @ trans_forw_pats inps; val l = l @ trans_forw_pats outps; val l = l @ (case cmd_opt of NONE => [] | SOME cmd => (case cmd_Typ_default_opt of NONE => ism_error ("ISM has no commands " ^ "but subsection \"cmd\" is present in rule " ^quote name) | SOME (cmd_Typ, _) => [(cmd, cmd_Typ)])); val l = l @ (case dom_opt of NONE => [] | SOME dom => (case domain_Typ_default_opt of NONE => ism_error ("ISM has no domains " ^ "but subsection \"dom\" is present in rule " ^quote name) | SOME (dom_Typ, _) => [(dom, dom_Typ)])); val l = case data_st_Typ_Term_opt of NONE => (if (post_v <> Inl []) then ism_error (no_data_st_error name) else l) | SOME (_, data_st_Typ, _) => l @ (case post_v of Inl ps => (map (fn (f,v) => (v,find_field_Typ sign f data_st_Typ))) ps | Inr sval => [(sval, data_st_Typ)]); (* transformation *) val l = map term_of (prep_rule sign l); (* transform Term_Typ list back into rule *) val (data_st_var_opt,l) = case data_st_Typ_Term_opt of NONE => (NONE,l) | _ => (SOME (hd l), Library.drop (1, l)); val (ctrl_st_exprs,l) = (case cs_exprs of NONE => (NONE,l) | SOME _ => (SOME (hd l, hd (tl l)), Library.drop(2, l))); val pres' = Library.take (length pres, l); val l = Library.drop (length pres, l); fun trans_back_pats l [] = [] | trans_back_pats l (((pat,multi),_)::rest) = ((hd l, multi), hd (tl l))::trans_back_pats (tl (tl l)) rest; val inps' = trans_back_pats l inps; val l = Library.drop (2* length inps, l); val outps' = trans_back_pats l outps; val l = Library.drop (2* length outps, l); val (cmd_opt',l) = if cmd_opt = NONE then (NONE,l) else (SOME (hd l), Library.drop (1, l)); val (dom_opt',l) = if dom_opt = NONE then (NONE,l) else (SOME (hd l), Library.drop (1, l)); val post_v' = case post_v of Inl posts => Inl (combine ((map (fn (f, v) => f)) posts) l) | Inr sval => Inr (hd l); val rule' = ((name, args), (ctrl_st_exprs, (dom_opt', (pres', (inps', (outps', (cmd_opt', post_v'))))))); in (data_st_var_opt, (rule':term rule)) end; (* We need to define some inductive sets (transs, steps and output), so we use * a common helper function which builds most of what we need *) fun mk_intros_helper prep_rule thy types rule = let val sign = Theory.sign_of thy; (* expand types *) val (cmd_Typ_default_opt, pt_Typ, msg_Typ, st_Typ, ctrl_st_Typ_Term_opt, data_st_Typ_Term_opt, l_st_Typ, g_st_Typ_opt, domain_Typ_default_opt) = types; val (data_st_var_opt, rule') = transform_rule prep_rule sign types rule; (* expand transition *) val ((name, args), (ctrl_st_exprs, conds)) = rule'; val (dom_opt,( pres, (inps, (outps, (cmd_opt, post_v))))) = conds; val (k_nil_Term, _) = mk_k_nil_Term sign pt_Typ msg_Typ; val msgss_Typ = pt_Typ --> mk_listT msg_Typ; (* prepare inputs *) val is_Term = mk_msgss_pat sign pt_Typ msg_Typ (k_nil_Term, inps); (* prepare outputs *) val os_Term = mk_msgss_pat sign pt_Typ msg_Typ (k_nil_Term, outps); (* prepare states *) fun mk_state proj post_v = mk_global_st_term l_st_Typ g_st_Typ_opt thy (case data_st_Typ_Term_opt of NONE => proj (the ctrl_st_exprs) | SOME(_, data_st_Typ, _) => let val data_st_Term = case post_v of Inl posts => mk_field_upd sign data_st_Typ (the data_st_var_opt) posts | Inr sval => sval; in case ctrl_st_Typ_Term_opt of NONE => data_st_Term | SOME(_, ctrl_st_Typ, _) => fst (mk_pair_Const sign ctrl_st_Typ data_st_Typ) $ proj (the ctrl_st_exprs) $ data_st_Term end); val s_Term = mk_state fst (Inl []); val s'_Term = mk_state snd post_v; (* construct transition *) val cmd_Typ = case cmd_Typ_default_opt of SOME (t,_) => t | NONE => HOLogic.unitT; val cmd = case cmd_opt of SOME t => t | NONE => (case cmd_Typ_default_opt of NONE => HOLogic.unit | SOME (_, SOME default_cmd) => default_cmd | _ => ism_error ("ISM has commands without default command " ^ "but subsection \"cmd\" is missing in rule " ^ quote name)); val dom_Typ = case domain_Typ_default_opt of SOME (t,_) => t | NONE => HOLogic.unitT; val dom = case dom_opt of SOME t => t | NONE => (case domain_Typ_default_opt of NONE => HOLogic.unit | SOME (_, SOME default_domain) => default_domain | _ => ism_error ("ISM has domains without default domain " ^ "but subsection \"dom\" is missing in rule " ^ quote name)); in (msgss_Typ, is_Term, os_Term, s_Term, s'_Term, cmd_Typ, cmd, dom_Typ, dom, name, args, pres) end; (** make introduction rules **) (* the transs relation is defined inductively in this function *) fun mk_intros_trans prep_rule thy types param_transs_Term rule = let val sign = Theory.sign_of thy; (* expand types *) val (_, _, _, st_Typ, _, _, _, _, _) = types; val (msgss_Typ, is_Term, os_Term, s_Term, s'_Term, cmd_Typ, cmd, dom_Typ, dom, name, args, pres) = mk_intros_helper prep_rule thy types rule; (* create one trans tuple *) val (is_s_Term, is_s_Typ) = mk_pair_Term_Typ sign (is_Term, msgss_Typ) (s_Term, st_Typ); val (os_s'_Term, os_s'_Typ) = mk_pair_Term_Typ sign (os_Term, msgss_Typ) (s'_Term, st_Typ); val (cd_Term, cd_Typ) = mk_pair_Term_Typ sign (cmd, cmd_Typ) (dom, dom_Typ); val (trans_Term, trans_Typ) = mk_pair_Term_Typ sign (is_s_Term, is_s_Typ) (mk_pair_Term_Typ sign (cd_Term, cd_Typ) (os_s'_Term, os_s'_Typ)); (* construct conclusion *) val elem_Term = Const("op :", trans_Typ --> HOLogic.mk_setT trans_Typ --> HOLogic.boolT); val concl_Term = HOLogic.mk_Trueprop (elem_Term $ trans_Term $ param_transs_Term); (* construct rule with premissions *) val rule_Term = mk_prems sign concl_Term (rev pres); (* introduction rule *) val args' = map (Attrib.global_attribute thy) args; val intr = ((name, rule_Term), args'); in intr end; (* the steps relation is defined inductively in this function *) fun mk_intros_step prep_rule thy types param_steps_Term rule = let val sign = Theory.sign_of thy; val (_, _, _, st_Typ, _, _, _, _, _) = types; val (msgss_Typ, is_Term, _, s_Term, s'_Term, _, _, _, _, name, args, pres) = mk_intros_helper prep_rule thy types rule; val (steps_Term, state_tuple_Typ) = mk_pair_Term_Typ sign (s_Term, st_Typ) (s'_Term, st_Typ); (* construct conclusion *) val elem_Term = Const("op :", state_tuple_Typ --> HOLogic.mk_setT state_tuple_Typ --> HOLogic.boolT); val concl_Term = HOLogic.mk_Trueprop (elem_Term $ steps_Term $ param_steps_Term); val cond_Term = Const("op =", msgss_Typ --> msgss_Typ --> HOLogic.boolT) $ Free ("ins", msgss_Typ) $ is_Term; (* construct rule with premissions *) val rule_Term = mk_prems sign concl_Term (cond_Term::(rev pres)); (* introduction rule *) val args' = map (Attrib.global_attribute thy) args; val intr = ((name, rule_Term), args'); in intr end; (* the outputs relation is defined inductively in this function *) fun mk_intros_output prep_rule thy types param_outputs_Term rule = let val sign = Theory.sign_of thy; val (msgss_Typ, is_Term, os_Term, s_Term, s'_Term, cmd_Typ, cmd, dom_Typ, dom, name, args, pres) = mk_intros_helper prep_rule thy types rule; (* construct conclusion *) val elem_Term = Const("op :", msgss_Typ --> HOLogic.mk_setT msgss_Typ --> HOLogic.boolT); val concl_Term = HOLogic.mk_Trueprop (elem_Term $ os_Term $ param_outputs_Term); (* construct rule with premissions *) val dom_pre = Const("op =", dom_Typ --> dom_Typ --> HOLogic.boolT) $ Free("d", dom_Typ) $ dom; val rule_Term = mk_prems sign concl_Term (dom_pre::(rev pres)); (* introduction rule *) val args' = map (Attrib.global_attribute thy) args; val intr = ((name, rule_Term), args'); in intr end; (** add transition set **) (* If you use something newer than Isabelle2005, use OldInductivePackage instead *) local open InductivePackage in fun add_transs prep_rule types param_transs_Term [] (thy, thms) = (thy, thms) | add_transs prep_rule types param_transs_Term transs (thy, thms) = let val sign = Theory.sign_of thy; val intros = map (mk_intros_trans prep_rule thy types param_transs_Term) transs; val (thy', thm) = thy |> add_inductive_i true false "" false false false [param_transs_Term] intros []; val thms' = thm :: thms; in (thy', thms') end; fun add_outputs prep_rule types param_outputs_Term [] (thy, thms) = (thy, thms) | add_outputs prep_rule types param_outputs_Term transs (thy, thms) = let val sign = Theory.sign_of thy; val intros = map (mk_intros_output prep_rule thy types param_outputs_Term) transs; val (thy', thm) = thy |> add_inductive_i true false "" false false false [param_outputs_Term] intros []; val thms' = thm :: thms; in (thy', thms') end; fun add_steps prep_rule types param_steps_Term [] (thy, thms) = (thy, thms) | add_steps prep_rule types param_steps_Term transs (thy, thms) = let val sign = Theory.sign_of thy; val intros = map (mk_intros_step prep_rule thy types param_steps_Term) transs; val (thy', thm) = thy |> add_inductive_i true false "" false false false [param_steps_Term] intros []; val thms' = thm :: thms; in (thy', thms') end; (* Careful: this function is different from the ones above them - it doesn't * define an inductive set, but a function *) fun add_dom_fun prep_rule types dom_free_Var transs thy = let val (_, pt_Typ, msg_Typ, _, _, _, _, _, domain_Typ_default_opt) = types; val msgss_Typ = pt_Typ --> mk_listT msg_Typ; val dom_Typ = case domain_Typ_default_opt of SOME (t,_) => t | NONE => HOLogic.unitT; val default_dom = Const("arbitrary", dom_Typ); (* filter is_Term and dom out of the transition *) fun filter_inp_dom t = let val (_, inp, _, _, _, _, _, _, dom, _, _, _) = t in (inp, dom) end; val vars = map (filter_inp_dom o mk_intros_helper prep_rule thy types) transs; val elem_Term = Const("HOL.If", HOLogic.boolT --> dom_Typ --> dom_Typ --> dom_Typ); val eq_Term = Const("op =", msgss_Typ --> msgss_Typ --> HOLogic.boolT); fun construct_if ((inp, dom), elsef) = let (* the input pattern inp may contain free variables; we quantify them existentially here *) val free_vars = Term.add_frees inp []; val dom_free_name = #1 (dest_Free dom_free_Var); val _ = if (exists ((curry (op =))(dom_free_name)) (map #1 free_vars)) then ism_error("Sorry, but you can't use the variable name "^quote dom_free_name^" in an ISM.") else ""; val dom_eq_Term = eq_Term $ dom_free_Var $ inp; fun mk_exists2 ((name, typ), term) = HOLogic.mk_exists(name,typ,term); val inp2 = foldl mk_exists2 dom_eq_Term free_vars; in elem_Term $ inp2 $ dom $ elsef end; val if_Term = foldr construct_if default_dom vars; in if_Term end; end; (*** add_ism ***) fun gen_add_ism prep_type prep_term prep_rule name params' pt_type pt_set_I pt_set_O msg_type cmd_type_default_opt domain_type_default_opt g_st_type_opt ctrl_st data_st transs thy = let val _ = message ("Constructing ism " ^ quote name ^ " ..."); val sign = Theory.sign_of thy; (* open own namespace *) val thy = Theory.add_path name thy; val sign = Theory.sign_of thy; val params = map (fn (n,ty) => (n, mk_Typ prep_type sign ty)) params'; (* port types and terms *) val pt_Typ = mk_Typ prep_type sign pt_type; val pt_set_Typ = HOLogic.mk_setT pt_Typ; val pt_set_I_Term = mk_Term prep_term sign (pt_set_I, pt_set_Typ); val pt_set_O_Term = mk_Term prep_term sign (pt_set_O, pt_set_Typ); (* message type *) val msg_Typ = mk_Typ prep_type sign msg_type; (* command type *) val cmd_Typ_default_opt = option_map (fn (cmd_type, default) => let val cmd_Typ = mk_Typ prep_type sign cmd_type in (cmd_Typ, option_map (fn t => mk_Term prep_term sign (t, cmd_Typ)) default) end) cmd_type_default_opt; val cmd_Typ = case cmd_Typ_default_opt of NONE => HOLogic.unitT | SOME (t,_) => t; (* domain type *) val domain_Typ_default_opt = option_map (fn (domain_type, default) => let val domain_Typ = mk_Typ prep_type sign domain_type in (domain_Typ, option_map (fn t => mk_Term prep_term sign (t, domain_Typ)) default) end) domain_type_default_opt; val domain_Typ = case domain_Typ_default_opt of NONE => HOLogic.unitT | SOME (t,_) => t; (* states *) (* global state type *) val g_st_Typ_opt = option_map (mk_Typ prep_type sign) g_st_type_opt; (* local state initial terms; type*) val ctrl_st_Typ_Term_opt = mk_state_opt prep_type prep_term sign ctrl_st; val data_st_Typ_Term_opt = mk_state_opt prep_type prep_term sign data_st; val l_st_Typ = case ctrl_st_Typ_Term_opt of NONE => (case data_st_Typ_Term_opt of NONE => let val _ = ism_error (no_state_error name) in dummyT end | SOME(_, data_st_Typ, _) => data_st_Typ) | SOME(_, ctrl_st_Typ, ctrl_st_var_dummy) => case data_st_Typ_Term_opt of NONE => ctrl_st_Typ | SOME(_, data_st_Typ, data_st_var_dummy) => (ctrl_st_var_dummy = data_st_var_dummy; (* forcing equal type*) HOLogic.mk_prodT(ctrl_st_Typ, data_st_Typ)); (* actual state type *) val st_Typ = case g_st_Typ_opt of NONE => l_st_Typ | SOME(g_st_Typ) => g_st_Typ; (* ism type *) (* the record definition itself is in ISM.thy *) val ism_name = "ism"; val ism_typ_name = "ISM." ^ ism_name; val ism_Typ = Type (ism_typ_name, [cmd_Typ, pt_Typ, msg_Typ, st_Typ, domain_Typ]); val param_ism_Typ = Library.foldr (op -->) (map snd params, ism_Typ); (* transitions *) val trans_Typ = Type (Sign.intern_type sign "trans", [cmd_Typ, pt_Typ, msg_Typ, st_Typ, domain_Typ]); val transs_Typ = HOLogic.mk_setT trans_Typ; val param_transs_Typ = Library.foldr (op -->) (map snd params, transs_Typ); val transs_name = "transs"; (* output function *) (* Typ: (domain \ (state \ msgss (port, msg) set)) *) (* FIXME: the output function doesn't make much sense when there is no domain defined. * Only create it conditionally. *) val msgss_Typ = pt_Typ --> mk_listT msg_Typ; val msgss_set_Typ = HOLogic.mk_setT msgss_Typ; val dom_Typ = case domain_Typ_default_opt of SOME (t,_) => t | NONE => HOLogic.unitT; val outputs_Typ = dom_Typ --> st_Typ --> msgss_set_Typ; val param_outputs_Typ = Library.foldr (op -->) (map snd params, outputs_Typ); val outputs_name = "outputs"; (* Step function *) (* Typ: (ins \ (state, state) set) *) (* We could create this function out of the transition function in Isabelle directly, * however, this is a little bit hard to work with. *) val state_tuple_set_Typ = HOLogic.mk_setT (HOLogic.mk_prodT (st_Typ, st_Typ) ); val param_steps_Typ = msgss_Typ --> state_tuple_set_Typ; val steps_name = "Step"; (* domain function *) (* Typ: (io \ action list) \ domain *) (* FIXME: This mapping is not necessarily unique; we should check for this and only * allow well-formed ISMs *) val dom_fun_Typ = msgss_Typ --> dom_Typ; val dom_fun_name = "dom"; (* Small note: param_ism_Typ and param_transs_Typ handle the case that the * ISM is parameterised (something like 'ism AP (N::nat) =\'); in the standard * case, they don't change anything. *) (* add transs and ism constants *) val thy = thy |> Theory.add_consts_i [(transs_name, param_transs_Typ, NoSyn)] |> Theory.add_consts_i [(outputs_name, param_outputs_Typ, NoSyn)] |> Theory.add_consts_i [(steps_name, param_steps_Typ, NoSyn)] |> Theory.add_consts_i [(dom_fun_name, dom_fun_Typ, NoSyn)] |> Theory.add_consts_i [(ism_name, param_ism_Typ, NoSyn)] val sign = Theory.sign_of thy val types = (cmd_Typ_default_opt, pt_Typ, msg_Typ, st_Typ, ctrl_st_Typ_Term_opt, data_st_Typ_Term_opt, l_st_Typ, g_st_Typ_opt, domain_Typ_default_opt); (* add transs (inductive definition) *) val transs_Term = Sign.intern_term sign (term_of (read_cterm sign (transs_name, param_transs_Typ))); val param_transs_Term = Library.foldl (op $) (transs_Term, map Free params); val (thy, thms) = add_transs prep_rule types param_transs_Term transs (thy, []); val sign = Theory.sign_of thy; (* add outputs (inductive definition) *) val outputs_Term = (Sign.intern_term sign (term_of (read_cterm sign (outputs_name, param_outputs_Typ)))) val param_outputs_Term = (Library.foldl (op $) (outputs_Term, map Free params)) $ Free ("d", dom_Typ) $ Free ("s", st_Typ); val (thy, thms) = add_outputs prep_rule types param_outputs_Term transs (thy, thms); (* not that we pass transs to add_outputs above, because we generate the outputs * relation from the transitions *) val sign = Theory.sign_of thy; (* add steps (inductive definition) *) val steps_Term = (Sign.intern_term sign (term_of (read_cterm sign (steps_name, param_steps_Typ)))) (* val param_steps_Term = (Library.foldl (op $) (steps_Term, map Free params)) $ Free ("ins", msgss_Typ); *) val param_steps_Term = steps_Term $ Free ("ins", msgss_Typ); val (thy, thms) = add_steps prep_rule types param_steps_Term transs (thy, thms); val sign = Theory.sign_of thy; val constname = Sign.intern_const sign; val dom_free_Var = Free("inp_var", msgss_Typ); val dom_if_Term = add_dom_fun prep_rule types dom_free_Var transs thy; val dom_if_eq = Const("==", dom_Typ --> dom_Typ --> propT) $ (Const (constname dom_fun_name, dom_fun_Typ) $ dom_free_Var) $ dom_if_Term; val thy = thy |> IsarThy.add_defs_i (false, [((dom_fun_name^"_def", dom_if_eq ),[] )]); (* Earlier, a special syntax for ISM transitions was declared here. However, no code * uses it right now and it was broken by the introduction of domains. The code is * still there after all the real declaration as a comment (just for reference) *) (* initialize ism record *) val sign = Theory.sign_of thy; val typname = Sign.intern_type sign; val constname = Sign.intern_const sign; (* initialize init field *) val init_Term' = let val init_Term = case ctrl_st_Typ_Term_opt of NONE => (case data_st_Typ_Term_opt of NONE => dummy_Term | SOME(data_st_Term, _, _) => data_st_Term) | SOME(ctrl_st_Term, ctrl_st_Typ, _) => case data_st_Typ_Term_opt of NONE => ctrl_st_Term | SOME(data_st_Term, data_st_Typ, _) => let val (pair_Const, _) = mk_pair_Const sign ctrl_st_Typ data_st_Typ; in pair_Const $ ctrl_st_Term $ data_st_Term end; in mk_global_st_term l_st_Typ g_st_Typ_opt thy init_Term end; val ism_Term = Library.foldl (op $) (Const (constname ism_name, param_ism_Typ), map Free params); val ism_make_Term = ((Const((ism_typ_name^".make"), pt_set_Typ --> pt_set_Typ --> st_Typ --> transs_Typ --> ism_Typ)) $ pt_set_I_Term $ pt_set_O_Term $ init_Term' $ param_transs_Term ); val ism_eq = ((Const("==", ism_Typ --> ism_Typ --> propT)) $ ism_Term $ ism_make_Term ); val thy = thy |> IsarThy.add_defs_i (false, [(("ism_def", ism_eq ),[] )]); (* close own namespace *) val thy = Theory.parent_path thy; in (thy, thms, thm) end; fun assoc_string ([], (key:string)) = NONE | assoc_string ((keyi, xi) :: pairs, key) = if key = keyi then SOME xi else assoc_string (pairs, key); fun read_rule sign sTs = ((fst o (read_def_cterms (sign, K NONE, (fn (x, ~1) => (curry assoc_string o typ_tfrees) TypeInfer.logicT x)) (((Library.flat o (map ((map fst) o typ_tfrees))) o map snd) sTs) true)) sTs); fun cterm_of' sign = cterm_of sign o fst; fun rule_of sign = map (cterm_of' sign); val add_ism = gen_add_ism read_ctyp read_cterm read_rule; val add_ism_i = gen_add_ism ctyp_of cterm_of' rule_of; (*** package setup ***) (** outer syntax **) local structure P = OuterParse and K = OuterKeyword in val ism_decl = let val optional_init = Scan.optional (P.$$$ "init" |-- P.term) "arbitrary" val param = P.$$$ "(" |-- P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" val pattern = ( ( P.term >> (fn x => (x,false))) || (P.$$$ "multi" |-- P.term >> (fn x => (x,true )))) -- P.term val in_pat = (P.term >> (fn x => (x,false))) -- P.term val state_update = P.list1 (P.name -- (P.$$$ ":=" |-- P.term)) >> Inl || P.term >> Inr in (P.name -- Scan.repeat param) -- (P.$$$ "=" |-- (P.$$$ "ports" |-- P.typ -- (P.$$$ "inputs" |-- P.term -- (P.$$$ "outputs" |-- P.term -- (P.$$$ "messages" |-- P.typ -- (Scan.option (P.$$$ "commands" |-- P.typ -- Scan.option (P.$$$ "default" |-- P.typ)) -- (Scan.option (P.$$$ "domains" |-- P.typ -- Scan.option (P.$$$ "default" |-- P.typ)) -- (P.$$$ "states" |-- Scan.option P.typ -- (Scan.option (P.$$$ "control" |-- P.typ -- (optional_init >> (fn x => (x, "dummy_control_var")))) -- (Scan.option (P.$$$ "data" |-- P.typ -- (optional_init -- (Scan.optional (P.$$$ "name" |-- P.term) "s"))) -- Scan.optional (P.$$$ "transitions" |-- Scan.repeat1 (P.thm_name ":" -- (Scan.option (P.term -- ((P.$$$ "\" || P.$$$ "->") |-- P.term)) -- (Scan.option (P.$$$ "dom" |-- P.term) -- (Scan.optional (P.$$$ "pre" |-- P.list1 P.term ) [] -- (Scan.optional (P.$$$ "in" |-- P.list1 in_pat ) [] -- (Scan.optional (P.$$$ "out" |-- P.list1 pattern) [] -- (Scan.option (P.$$$ "cmd" |-- P.term) -- (Scan.optional (P.$$$ "post" |-- state_update) (Inl [])) )))))))) [] )))))))))) end; val ismP = OuterSyntax.command "ism" "define Interacting State Machine" K.thy_decl (ism_decl >> (fn ((name, params), (pt_type, (pt_set_I, (pt_set_O, (msg_type, (cmd_type_default_opt, (domain_type_default_opt, (g_st_type_opt, (ctrl_st, (data_st, transs)))))))))) => Toplevel.theory (#1 o add_ism name params pt_type pt_set_I pt_set_O msg_type cmd_type_default_opt domain_type_default_opt g_st_type_opt ctrl_st data_st transs))); val _ = OuterSyntax.add_keywords ["ports", "inputs", "outputs", "messages", "commands", "default", "domains", "states", "control", "init", "data", "name", "multi", "transitions", "\", "->", "pre", "in", "out", "cmd", "dom", "post",":="]; val _ = OuterSyntax.add_parsers [ismP]; end; (* local *) end; *} end (*>*)