wenzelm@6508: (* Title: HOLCF/IOA/meta_theory/ioa_package.ML mueller@6467: ID: $Id$ haftmann@18358: Author: Tobias Hamberger, TU Muenchen mueller@6467: *) mueller@6467: mueller@6467: signature IOA_PACKAGE = mueller@6467: sig haftmann@18358: val add_ioa: string -> string haftmann@18358: -> (string) list -> (string) list -> (string) list haftmann@18358: -> (string * string) list -> string haftmann@18358: -> (string * string * (string * string)list) list haftmann@18358: -> theory -> theory haftmann@18358: val add_composition : string -> (string)list -> theory -> theory haftmann@18358: val add_hiding : string -> string -> (string)list -> theory -> theory haftmann@18358: val add_restriction : string -> string -> (string)list -> theory -> theory haftmann@18358: val add_rename : string -> string -> string -> theory -> theory mueller@6467: end; mueller@6467: wenzelm@6508: structure IoaPackage: IOA_PACKAGE = mueller@6467: struct mueller@6467: wenzelm@24634: val string_of_typ = PrintMode.setmp [] o Sign.string_of_typ; wenzelm@24634: val string_of_term = PrintMode.setmp [] o Sign.string_of_term; wenzelm@17243: mueller@6467: exception malformed; mueller@6467: mueller@6467: (* stripping quotes *) mueller@6467: fun strip [] = [] | mueller@6467: strip ("\""::r) = strip r | mueller@6467: strip (a::r) = a :: (strip r); mueller@6467: fun strip_quote s = implode(strip(explode(s))); mueller@6467: mueller@6467: (* used by *_of_varlist *) mueller@6467: fun extract_first (a,b) = strip_quote a; mueller@6467: fun extract_second (a,b) = strip_quote b; mueller@6467: (* following functions producing sth from a varlist *) mueller@6467: fun comma_list_of_varlist [] = "" | mueller@6467: comma_list_of_varlist [a] = extract_first a | mueller@6467: comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r); mueller@6467: fun primed_comma_list_of_varlist [] = "" | mueller@6467: primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" | mueller@6467: primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^ mueller@6467: (primed_comma_list_of_varlist r); mueller@6467: fun type_product_of_varlist [] = "" | mueller@6467: type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | mueller@6467: type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r; mueller@6467: mueller@6467: (* listing a list *) mueller@6467: fun list_elements_of [] = "" | mueller@6467: list_elements_of (a::r) = a ^ " " ^ (list_elements_of r); mueller@6467: mueller@6467: (* extracting type parameters from a type list *) mueller@6467: (* fun param_tupel thy [] res = res | mueller@6467: param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res | mueller@6467: param_tupel thy ((TFree(a,_))::r) res = mueller@6467: if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) | mueller@6467: param_tupel thy (a::r) res = wenzelm@22578: error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a)); mueller@6467: *) mueller@6467: mueller@6467: (* used by constr_list *) mueller@6467: fun extract_constrs thy [] = [] | mueller@6467: extract_constrs thy (a::r) = mueller@6467: let mueller@6467: fun delete_bold [] = [] haftmann@18443: | delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs)) mueller@6467: then (let val (_::_::_::s) = xs in delete_bold s end) haftmann@18443: else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) mueller@6467: then (let val (_::_::_::s) = xs in delete_bold s end) mueller@6467: else (x::delete_bold xs)); mueller@6467: fun delete_bold_string s = implode(delete_bold(explode s)); mueller@6467: (* from a constructor term in *.induct (with quantifiers, mueller@6467: "Trueprop" and ?P stripped away) delivers the head *) mueller@6467: fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r | mueller@6467: extract_hd (Const("Trueprop",_) $ r) = extract_hd r | mueller@6467: extract_hd (Var(_,_) $ r) = extract_hd r | mueller@6467: extract_hd (a $ b) = extract_hd a | mueller@6467: extract_hd (Const(s,_)) = s | mueller@6467: extract_hd _ = raise malformed; mueller@6467: (* delivers constructor term string from a prem of *.induct *) wenzelm@20194: fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))| mueller@6467: extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | wenzelm@22578: extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term thy r) | mueller@6467: extract_constr _ _ = raise malformed; mueller@6467: in mueller@6467: (extract_hd a,extract_constr thy a) :: (extract_constrs thy r) mueller@6467: end; mueller@6467: mueller@6467: (* delivering list of constructor terms of a datatype *) mueller@6467: fun constr_list thy atyp = mueller@6467: let mueller@6467: fun act_name thy (Type(s,_)) = s | mueller@6467: act_name _ s = wenzelm@22578: error("malformed action type: " ^ (string_of_typ thy s)); mueller@6467: fun afpl ("." :: a) = [] | mueller@6467: afpl [] = [] | mueller@6467: afpl (a::r) = a :: (afpl r); mueller@6467: fun unqualify s = implode(rev(afpl(rev(explode s)))); mueller@6467: val q_atypstr = act_name thy atyp; mueller@6467: val uq_atypstr = unqualify q_atypstr; wenzelm@16486: val prem = prems_of (get_thm thy (Name (uq_atypstr ^ ".induct"))); mueller@6467: in mueller@6467: extract_constrs thy prem mueller@6467: handle malformed => mueller@6467: error("malformed theorem : " ^ uq_atypstr ^ ".induct") mueller@6467: end; mueller@6467: mueller@6467: fun check_for_constr thy atyp (a $ b) = mueller@6467: let mueller@6467: fun all_free (Free(_,_)) = true | mueller@6467: all_free (a $ b) = if (all_free a) then (all_free b) else false | mueller@6467: all_free _ = false; mueller@6467: in mueller@6467: if (all_free b) then (check_for_constr thy atyp a) else false mueller@6467: end | mueller@6467: check_for_constr thy atyp (Const(a,_)) = mueller@6467: let mueller@6467: val cl = constr_list thy atyp; mueller@6467: fun fstmem a [] = false | mueller@6467: fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r) mueller@6467: in mueller@6467: if (fstmem a cl) then true else false mueller@6467: end | mueller@6467: check_for_constr _ _ _ = false; mueller@6467: mueller@6467: (* delivering the free variables of a constructor term *) mueller@6467: fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) | mueller@6467: free_vars_of (Const(_,_)) = [] | mueller@6467: free_vars_of (Free(a,_)) = [a] | mueller@6467: free_vars_of _ = raise malformed; mueller@6467: mueller@6467: (* making a constructor set from a constructor term (of signature) *) mueller@6467: fun constr_set_string thy atyp ctstr = mueller@6467: let wenzelm@22675: val trm = Sign.simple_read_term thy atyp ctstr; mueller@6467: val l = free_vars_of trm mueller@6467: in mueller@6467: if (check_for_constr thy atyp trm) then mueller@6467: (if (l=[]) then ("{" ^ ctstr ^ "}") mueller@6467: else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") mueller@6467: else (raise malformed) mueller@6467: handle malformed => wenzelm@22578: error("malformed action term: " ^ (string_of_term thy trm)) mueller@6467: end; mueller@6467: mueller@6467: (* extracting constructor heads *) mueller@6467: fun constructor_head thy atypstr s = mueller@6467: let mueller@6467: fun hd_of (Const(a,_)) = a | mueller@6467: hd_of (t $ _) = hd_of t | mueller@6467: hd_of _ = raise malformed; wenzelm@24707: val trm = Sign.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; mueller@6467: in mueller@6467: hd_of trm handle malformed => mueller@6467: error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) mueller@6467: end; mueller@6467: fun constructor_head_list _ _ [] = [] | mueller@6467: constructor_head_list thy atypstr (a::r) = mueller@6467: (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r); mueller@6467: mueller@6467: (* producing an action set *) mueller@6467: fun action_set_string thy atyp [] = "{}" | mueller@6467: action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) | mueller@6467: action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^ mueller@6467: " Un " ^ (action_set_string thy atyp r); mueller@6467: mueller@6467: (* used by extend *) mueller@6467: fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" | mueller@6467: pstr s ((a,b)::r) = mueller@6467: if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r); mueller@6467: fun poststring [] l = "" | mueller@6467: poststring [(a,b)] l = pstr a l | mueller@6467: poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l); mueller@6467: mueller@6467: (* extends a (action string,condition,assignlist) tupel by a mueller@6467: (action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list mueller@6467: (where bool indicates whether there is a precondition *) mueller@6467: fun extend thy atyp statetupel (actstr,r,[]) = mueller@6467: let wenzelm@22675: val trm = Sign.simple_read_term thy atyp actstr; wenzelm@22675: val rtrm = Sign.simple_read_term thy (Type("bool",[])) r; mueller@6467: val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true mueller@6467: in mueller@6467: if (check_for_constr thy atyp trm) mueller@6467: then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) mueller@6467: else mueller@6467: error("transition " ^ actstr ^ " is not a pure constructor term") mueller@6467: end | mueller@6467: extend thy atyp statetupel (actstr,r,(a,b)::c) = mueller@6467: let mueller@6467: fun pseudo_poststring [] = "" | mueller@6467: pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | mueller@6467: pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); wenzelm@22675: val trm = Sign.simple_read_term thy atyp actstr; wenzelm@22675: val rtrm = Sign.simple_read_term thy (Type("bool",[])) r; mueller@6467: val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true mueller@6467: in mueller@6467: if (check_for_constr thy atyp trm) then mueller@6467: (if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) mueller@6467: (* the case with transrel *) mueller@6467: else mueller@6467: (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), mueller@6467: "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) mueller@6467: else mueller@6467: error("transition " ^ actstr ^ " is not a pure constructor term") mueller@6467: end; mueller@6467: (* used by make_alt_string *) mueller@6467: fun extended_list _ _ _ [] = [] | mueller@6467: extended_list thy atyp statetupel (a::r) = mueller@6467: (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); mueller@6467: mueller@6467: (* used by write_alts *) mueller@6467: fun write_alt thy (chead,tr) inp out int [] = mueller@6467: if (chead mem inp) then mueller@6467: ( mueller@6467: error("Input action " ^ tr ^ " was not specified") mueller@6467: ) else ( mueller@6467: if (chead mem (out@int)) then wenzelm@10203: (writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else (); mueller@6467: (tr ^ " => False",tr ^ " => False")) | mueller@6467: write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = mueller@6467: let mueller@6467: fun hd_of (Const(a,_)) = a | mueller@6467: hd_of (t $ _) = hd_of t | mueller@6467: hd_of _ = raise malformed; mueller@6467: fun occurs_again c [] = false | mueller@6467: occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); mueller@6467: in mueller@6467: if (chead=(hd_of a)) then mueller@6467: (if ((chead mem inp) andalso e) then ( mueller@6467: error("Input action " ^ b ^ " has a precondition") mueller@6467: ) else (if (chead mem (inp@out@int)) then mueller@6467: (if (occurs_again chead r) then ( mueller@6467: error("Two specifications for action: " ^ b) mueller@6467: ) else (b ^ " => " ^ c,b ^ " => " ^ d)) mueller@6467: else ( mueller@6467: error("Action " ^ b ^ " is not in automaton signature") mueller@6467: ))) else (write_alt thy (chead,ctrm) inp out int r) mueller@6467: handle malformed => wenzelm@22578: error ("malformed action term: " ^ (string_of_term thy a)) mueller@6467: end; mueller@6467: mueller@6467: (* used by make_alt_string *) mueller@6467: fun write_alts thy (a,b) inp out int [] ttr = (a,b) | mueller@6467: write_alts thy (a,b) inp out int [c] ttr = mueller@6467: let mueller@6467: val wa = write_alt thy c inp out int ttr mueller@6467: in mueller@6467: (a ^ (fst wa),b ^ (snd wa)) mueller@6467: end | mueller@6467: write_alts thy (a,b) inp out int (c::r) ttr = mueller@6467: let mueller@6467: val wa = write_alt thy c inp out int ttr mueller@6467: in mueller@6467: write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr mueller@6467: end; mueller@6467: mueller@6467: fun make_alt_string thy inp out int atyp statetupel trans = mueller@6467: let mueller@6467: val cl = constr_list thy atyp; mueller@6467: val ttr = extended_list thy atyp statetupel trans; mueller@6467: in mueller@6467: write_alts thy ("","") inp out int cl ttr mueller@6467: end; mueller@6467: wenzelm@12339: (* used in add_ioa *) mueller@6467: fun check_free_primed (Free(a,_)) = mueller@6467: let mueller@6467: val (f::r) = rev(explode a) mueller@6467: in mueller@6467: if (f="'") then [a] else [] mueller@6467: end | mueller@6467: check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) | mueller@6467: check_free_primed (Abs(_,_,t)) = check_free_primed t | mueller@6467: check_free_primed _ = []; mueller@6467: mueller@6467: fun overlap [] _ = true | mueller@6467: overlap (a::r) l = if (a mem l) then ( mueller@6467: error("Two occurences of action " ^ a ^ " in automaton signature") mueller@6467: ) else (overlap r l); mueller@6467: mueller@6467: (* delivering some types of an automaton *) mueller@6467: fun aut_type_of thy aut_name = mueller@6467: let mueller@6467: fun left_of (( _ $ left) $ _) = left | mueller@6467: left_of _ = raise malformed; wenzelm@16486: val aut_def = concl_of (get_thm thy (Name (aut_name ^ "_def"))); mueller@6467: in wenzelm@22578: (#T(rep_cterm(cterm_of thy (left_of aut_def)))) mueller@6467: handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") mueller@6467: end; mueller@6467: mueller@6467: fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp | mueller@6467: act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ wenzelm@22578: (string_of_typ thy t)); mueller@6467: fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp | mueller@6467: st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ wenzelm@22578: (string_of_typ thy t)); mueller@6467: mueller@6467: fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | mueller@6467: comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | mueller@6467: comp_st_type_of _ _ = error "empty automaton list"; mueller@6467: mueller@6467: (* checking consistency of action types (for composition) *) mueller@6467: fun check_ac thy (a::r) = mueller@6467: let mueller@6467: fun ch_f_a thy acttyp [] = acttyp | mueller@6467: ch_f_a thy acttyp (a::r) = mueller@6467: let mueller@6467: val auttyp = aut_type_of thy a; mueller@6467: val ac = (act_type_of thy auttyp); mueller@6467: in mueller@6467: if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A") mueller@6467: end; mueller@6467: val auttyp = aut_type_of thy a; mueller@6467: val acttyp = (act_type_of thy auttyp); mueller@6467: in mueller@6467: ch_f_a thy acttyp r mueller@6467: end | mueller@6467: check_ac _ [] = error "empty automaton list"; mueller@6467: mueller@6467: fun clist [] = "" | mueller@6467: clist [a] = a | mueller@6467: clist (a::r) = a ^ " || " ^ (clist r); mueller@6467: mueller@6467: wenzelm@12339: (* add_ioa *) wenzelm@12339: wenzelm@12339: fun add_ioa automaton_name action_type inp out int statetupel ini trans thy = wenzelm@6508: (writeln("Constructing automaton " ^ automaton_name ^ " ..."); mueller@6467: let mueller@6467: val state_type_string = type_product_of_varlist(statetupel); wenzelm@24707: val styp = Syntax.read_typ_global thy state_type_string; mueller@6467: val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")"; mueller@6467: val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")"; wenzelm@24707: val atyp = Syntax.read_typ_global thy action_type; mueller@6467: val inp_set_string = action_set_string thy atyp inp; mueller@6467: val out_set_string = action_set_string thy atyp out; mueller@6467: val int_set_string = action_set_string thy atyp int; mueller@6467: val inp_head_list = constructor_head_list thy action_type inp; mueller@6467: val out_head_list = constructor_head_list thy action_type out; mueller@6467: val int_head_list = constructor_head_list thy action_type int; mueller@6467: val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); mueller@6467: val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list mueller@6467: atyp statetupel trans; mueller@6467: val thy2 = (thy mueller@6467: |> ContConsts.add_consts mueller@6467: [(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn), mueller@6467: (automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn), mueller@6467: (automaton_name ^ "_trans", mueller@6467: "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), mueller@6467: (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] haftmann@18358: |> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) mueller@6467: [(automaton_name ^ "_initial_def", mueller@6467: automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), mueller@6467: (automaton_name ^ "_asig_def", mueller@6467: automaton_name ^ "_asig == (" ^ mueller@6467: inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), mueller@6467: (automaton_name ^ "_trans_def", mueller@6467: automaton_name ^ "_trans == {(" ^ mueller@6467: state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^ mueller@6467: "). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), mueller@6467: (automaton_name ^ "_def", mueller@6467: automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ mueller@6467: "_initial, " ^ automaton_name ^ "_trans,{},{})") mueller@6467: ]) wenzelm@22675: val chk_prime_list = (check_free_primed (Sign.simple_read_term thy2 (Type("bool",[])) wenzelm@22675: ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string)))) mueller@6467: in mueller@6467: ( mueller@6467: if (chk_prime_list = []) then thy2 mueller@6467: else ( mueller@6467: error("Precondition or assignment terms in postconditions contain following primed variables:\n" mueller@6467: ^ (list_elements_of chk_prime_list))) mueller@6467: ) mueller@6467: end) mueller@6467: wenzelm@12339: fun add_composition automaton_name aut_list thy = wenzelm@6508: (writeln("Constructing automaton " ^ automaton_name ^ " ..."); mueller@6467: let mueller@6467: val acttyp = check_ac thy aut_list; mueller@6467: val st_typ = comp_st_type_of thy aut_list; mueller@6467: val comp_list = clist aut_list; mueller@6467: in mueller@6467: thy mueller@6467: |> ContConsts.add_consts_i mueller@6467: [(automaton_name, mueller@6467: Type("*", mueller@6467: [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), mueller@6467: Type("*",[Type("set",[st_typ]), mueller@6467: Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), mueller@6467: Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) mueller@6467: ,NoSyn)] haftmann@18358: |> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) mueller@6467: [(automaton_name ^ "_def", mueller@6467: automaton_name ^ " == " ^ comp_list)] mueller@6467: end) mueller@6467: wenzelm@12339: fun add_restriction automaton_name aut_source actlist thy = wenzelm@6508: (writeln("Constructing automaton " ^ automaton_name ^ " ..."); mueller@6467: let mueller@6467: val auttyp = aut_type_of thy aut_source; mueller@6467: val acttyp = act_type_of thy auttyp; mueller@6467: val rest_set = action_set_string thy acttyp actlist mueller@6467: in mueller@6467: thy mueller@6467: |> ContConsts.add_consts_i mueller@6467: [(automaton_name, auttyp,NoSyn)] haftmann@18358: |> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) mueller@6467: [(automaton_name ^ "_def", mueller@6467: automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] mueller@6467: end) wenzelm@12339: fun add_hiding automaton_name aut_source actlist thy = wenzelm@6508: (writeln("Constructing automaton " ^ automaton_name ^ " ..."); mueller@6467: let mueller@6467: val auttyp = aut_type_of thy aut_source; mueller@6467: val acttyp = act_type_of thy auttyp; mueller@6467: val hid_set = action_set_string thy acttyp actlist mueller@6467: in mueller@6467: thy mueller@6467: |> ContConsts.add_consts_i mueller@6467: [(automaton_name, auttyp,NoSyn)] haftmann@18358: |> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) mueller@6467: [(automaton_name ^ "_def", mueller@6467: automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] mueller@6467: end) mueller@6467: mueller@6467: fun ren_act_type_of thy funct = wenzelm@24707: (case Term.fastype_of (Syntax.read_term_global thy funct) of wenzelm@17925: Type ("fun", [a, b]) => a wenzelm@17925: | _ => error "could not extract argument type of renaming function term"); mueller@6467: wenzelm@12339: fun add_rename automaton_name aut_source fun_name thy = wenzelm@6508: (writeln("Constructing automaton " ^ automaton_name ^ " ..."); mueller@6467: let mueller@6467: val auttyp = aut_type_of thy aut_source; mueller@6467: val st_typ = st_type_of thy auttyp; mueller@6467: val acttyp = ren_act_type_of thy fun_name mueller@6467: in mueller@6467: thy mueller@6467: |> ContConsts.add_consts_i mueller@6467: [(automaton_name, mueller@6467: Type("*", mueller@6467: [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), mueller@6467: Type("*",[Type("set",[st_typ]), mueller@6467: Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), mueller@6467: Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) mueller@6467: ,NoSyn)] haftmann@18358: |> (snd oo (PureThy.add_defs false o map Thm.no_attributes)) mueller@6467: [(automaton_name ^ "_def", mueller@6467: automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] mueller@6467: end) mueller@6467: wenzelm@6508: wenzelm@6508: (** outer syntax **) wenzelm@6508: wenzelm@6508: (* prepare results *) wenzelm@6508: wenzelm@6508: (*encoding transition specifications with a element of ParseTrans*) wenzelm@6508: datatype ParseTrans = Rel of string | PP of string*(string*string)list; wenzelm@6508: fun mk_trans_of_rel s = Rel(s); wenzelm@6508: fun mk_trans_of_prepost (s,l) = PP(s,l); wenzelm@6508: wenzelm@6508: fun trans_of (a, Rel b) = (a, b, [("", "")]) wenzelm@6508: | trans_of (a, PP (b, l)) = (a, b, l); wenzelm@6508: wenzelm@6508: wenzelm@6508: fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = wenzelm@6508: add_ioa aut action_type inp out int states initial (map trans_of trans); wenzelm@6508: wenzelm@6508: fun mk_composition_decl (aut, autlist) = wenzelm@6508: add_composition aut autlist; wenzelm@6508: wenzelm@6508: fun mk_hiding_decl (aut, (actlist, source_aut)) = wenzelm@6508: add_hiding aut source_aut actlist; wenzelm@6508: wenzelm@6508: fun mk_restriction_decl (aut, (source_aut, actlist)) = wenzelm@6508: add_restriction aut source_aut actlist; wenzelm@6508: wenzelm@6508: fun mk_rename_decl (aut, (source_aut, rename_f)) = wenzelm@6508: add_rename aut source_aut rename_f; wenzelm@6508: wenzelm@6508: wenzelm@24867: (* outer syntax *) wenzelm@6508: wenzelm@17057: local structure P = OuterParse and K = OuterKeyword in wenzelm@6508: wenzelm@24867: val _ = OuterSyntax.keywords ["signature", "actions", "inputs", wenzelm@24867: "outputs", "internals", "states", "initially", "transitions", "pre", wenzelm@24867: "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", wenzelm@24867: "rename"]; wenzelm@24867: wenzelm@6723: val actionlist = P.list1 P.term; wenzelm@17243: val inputslist = P.$$$ "inputs" |-- P.!!! actionlist; wenzelm@17243: val outputslist = P.$$$ "outputs" |-- P.!!! actionlist; wenzelm@17243: val internalslist = P.$$$ "internals" |-- P.!!! actionlist; wenzelm@17243: val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ)); wenzelm@17243: val initial = P.$$$ "initially" |-- P.!!! P.term; wenzelm@17243: val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term); wenzelm@17243: val pre = P.$$$ "pre" |-- P.!!! P.term; wenzelm@17243: val post = P.$$$ "post" |-- P.!!! assign_list; wenzelm@6508: val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; wenzelm@6508: val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; wenzelm@17243: val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel; wenzelm@6723: val transition = P.term -- (transrel || pre1 || post1); wenzelm@17243: val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition); wenzelm@6508: wenzelm@6508: val ioa_decl = wenzelm@6723: (P.name -- (P.$$$ "=" |-- wenzelm@6723: (P.$$$ "signature" |-- wenzelm@17243: P.!!! (P.$$$ "actions" |-- wenzelm@6723: (P.typ -- wenzelm@6508: (Scan.optional inputslist []) -- wenzelm@6508: (Scan.optional outputslist []) -- wenzelm@6508: (Scan.optional internalslist []) -- wenzelm@6508: stateslist -- wenzelm@6508: (Scan.optional initial "True") -- wenzelm@6508: translist))))) >> mk_ioa_decl || wenzelm@17243: (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name)))) wenzelm@17243: >> mk_composition_decl || wenzelm@17243: (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- wenzelm@17243: P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl || wenzelm@17243: (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- wenzelm@17243: P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl || wenzelm@17243: (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term)))))) wenzelm@6723: >> mk_rename_decl; wenzelm@6508: wenzelm@24867: val _ = wenzelm@6723: OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl wenzelm@6723: (ioa_decl >> Toplevel.theory); wenzelm@6508: mueller@6467: end; wenzelm@6508: wenzelm@6508: end;