(*<*)
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 \<Rightarrow> (state \<Rightarrow> 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 \<Rightarrow> (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 \<Rightarrow> action list) \<Rightarrow> 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) =\<dots>'); 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.$$$ "\<rightarrow>" || 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", "\<rightarrow>", "->", "pre", "in", "out", "cmd", "dom", "post",":="];

val _ = OuterSyntax.add_parsers [ismP];

end; (* local *)


end;
*}
end
(*>*) 
