# HG changeset patch # User mueller # Date 924771630 -7200 # Node ID 863834a377695993e41c64c5104bfad0842de5a2 # Parent 2eba94dc5951293d482dcaa6073a194aeb0a1663 added frontend syntax for IOA, moved trivial examples to folder ex; diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/Abstraction.ML --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Thu Apr 22 10:56:37 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Thu Apr 22 11:00:30 1999 +0200 @@ -7,6 +7,7 @@ *) + section "cex_abs"; diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/IOA.ML --- a/src/HOLCF/IOA/meta_theory/IOA.ML Thu Apr 22 10:56:37 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/IOA.ML Thu Apr 22 11:00:30 1999 +0200 @@ -6,3 +6,7 @@ The theory of I/O automata in HOLCF. *) + +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; + by (fast_tac (claset() addDs prems) 1); +qed "imp_conj_lemma"; diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/TrivEx.ML --- a/src/HOLCF/IOA/meta_theory/TrivEx.ML Thu Apr 22 10:56:37 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: HOLCF/IOA/TrivEx.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1995 TU Muenchen - -Trivial Abstraction Example -*) - -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; - by (fast_tac (claset() addDs prems) 1); -qed "imp_conj_lemma"; - - -Goalw [is_abstraction_def] -"is_abstraction h_abs C_ioa A_ioa"; -by (rtac conjI 1); -(* ------------- start states ------------ *) -by (simp_tac (simpset() addsimps - [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1); -(* -------------- step case ---------------- *) -by (REPEAT (rtac allI 1)); -by (rtac imp_conj_lemma 1); -by (simp_tac (simpset() addsimps [trans_of_def, - C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); -by (simp_tac (simpset() addsimps [h_abs_def]) 1); -by (induct_tac "a" 1); -by Auto_tac; -qed"h_abs_is_abstraction"; - - -Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)"; -by (rtac AbsRuleT1 1); -by (rtac h_abs_is_abstraction 1); -by (rtac MC_result 1); -by (abstraction_tac 1); -by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1); -qed"TrivEx_abstraction"; - - diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/TrivEx.thy --- a/src/HOLCF/IOA/meta_theory/TrivEx.thy Thu Apr 22 10:56:37 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,61 +0,0 @@ -(* Title: HOLCF/IOA/TrivEx.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1995 TU Muenchen - -Trivial Abstraction Example -*) - -TrivEx = Abstraction + - -datatype action = INC - -consts - -C_asig :: action signature -C_trans :: (action, nat)transition set -C_ioa :: (action, nat)ioa - -A_asig :: action signature -A_trans :: (action, bool)transition set -A_ioa :: (action, bool)ioa - -h_abs :: "nat => bool" - -defs - -C_asig_def - "C_asig == ({},{INC},{})" - -C_trans_def "C_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = Suc(s)}" - -C_ioa_def "C_ioa == - (C_asig, {0}, C_trans,{},{})" - -A_asig_def - "A_asig == ({},{INC},{})" - -A_trans_def "A_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = True}" - -A_ioa_def "A_ioa == - (A_asig, {False}, A_trans,{},{})" - -h_abs_def - "h_abs n == n~=0" - -rules - -MC_result - "validIOA A_ioa (<>[] <%(b,a,c). b>)" - -end \ No newline at end of file diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/TrivEx2.ML --- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML Thu Apr 22 10:56:37 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,72 +0,0 @@ -(* Title: HOLCF/IOA/TrivEx.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1995 TU Muenchen - -Trivial Abstraction Example -*) - -val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; - by (fast_tac (claset() addDs prems) 1); -qed "imp_conj_lemma"; - - -Goalw [is_abstraction_def] -"is_abstraction h_abs C_ioa A_ioa"; -by (rtac conjI 1); -(* ------------- start states ------------ *) -by (simp_tac (simpset() addsimps - [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1); -(* -------------- step case ---------------- *) -by (REPEAT (rtac allI 1)); -by (rtac imp_conj_lemma 1); -by (simp_tac (simpset() addsimps [trans_of_def, - C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1); -by (simp_tac (simpset() addsimps [h_abs_def]) 1); -by (induct_tac "a" 1); -by Auto_tac; -qed"h_abs_is_abstraction"; - - -(* -Goalw [xt2_def,plift,option_lift] - "(xt2 (plift afun)) (s,a,t) = (afun a)"; -(* !!!!!!!!!!!!! Occurs check !!!! *) -by (induct_tac "a" 1); - -*) - -Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def, - C_trans_def,trans_of_def] -"!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"; -by Auto_tac; -qed"Enabled_implication"; - - -Goalw [is_live_abstraction_def] -"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"; -by Auto_tac; -(* is_abstraction *) -by (rtac h_abs_is_abstraction 1); -(* temp_weakening *) -by (abstraction_tac 1); -by (etac Enabled_implication 1); -qed"h_abs_is_liveabstraction"; - - -Goalw [C_live_ioa_def] -"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"; -by (rtac AbsRuleT2 1); -by (rtac h_abs_is_liveabstraction 1); -by (rtac MC_result 1); -by (abstraction_tac 1); -by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1); -qed"TrivEx2_abstraction"; - - -(* -Goal "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR)))) -IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))"; - -*) - diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/TrivEx2.thy --- a/src/HOLCF/IOA/meta_theory/TrivEx2.thy Thu Apr 22 10:56:37 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,71 +0,0 @@ -(* Title: HOLCF/IOA/TrivEx.thy - ID: $Id$ - Author: Olaf Mueller - Copyright 1995 TU Muenchen - -Trivial Abstraction Example with fairness -*) - -TrivEx2 = Abstraction + IOA + - -datatype action = INC - -consts - -C_asig :: action signature -C_trans :: (action, nat)transition set -C_ioa :: (action, nat)ioa -C_live_ioa :: (action, nat)live_ioa - -A_asig :: action signature -A_trans :: (action, bool)transition set -A_ioa :: (action, bool)ioa -A_live_ioa :: (action, bool)live_ioa - -h_abs :: "nat => bool" - -defs - -C_asig_def - "C_asig == ({},{INC},{})" - -C_trans_def "C_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = Suc(s)}" - -C_ioa_def "C_ioa == - (C_asig, {0}, C_trans,{},{})" - -C_live_ioa_def - "C_live_ioa == (C_ioa, WF C_ioa {INC})" - -A_asig_def - "A_asig == ({},{INC},{})" - -A_trans_def "A_trans == - {tr. let s = fst(tr); - t = snd(snd(tr)) - in case fst(snd(tr)) - of - INC => t = True}" - -A_ioa_def "A_ioa == - (A_asig, {False}, A_trans,{},{})" - -A_live_ioa_def - "A_live_ioa == (A_ioa, WF A_ioa {INC})" - - - -h_abs_def - "h_abs n == n~=0" - -rules - -MC_result - "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)" - -end \ No newline at end of file diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/ioa_package.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Thu Apr 22 11:00:30 1999 +0200 @@ -0,0 +1,495 @@ +(* Title: ioa_package.ML + ID: $Id$ +*) + +signature IOA_PACKAGE = +sig + val add_ioa: string -> string -> + (string) list -> (string) list -> (string) list -> + (string * string) list -> string -> + (string * string * (string * string)list) list + -> theory -> theory + val add_ioa_i : string -> string -> + (string) list -> (string) list -> (string) list -> + (string * string) list -> string -> + (string * string * (string * string)list) list + -> theory -> theory + val add_composition : string -> (string)list -> theory -> theory + val add_composition_i : string -> (string)list -> theory -> theory + val add_hiding : string -> string -> (string)list -> theory -> theory + val add_hiding_i : string -> string -> (string)list -> theory -> theory + val add_restriction : string -> string -> (string)list -> theory -> theory + val add_restriction_i : string -> string -> (string)list -> theory -> theory + val add_rename : string -> string -> string -> theory -> theory + val add_rename_i : string -> string -> string -> theory -> theory +end; + +structure IoaPackage(* FIXME : IOA_PACKAGE *) = +struct + +local + +exception malformed; + +(* for usage of hidden function no_attributes of structure Thm : *) +fun no_attributes x = (x, []); + +(* stripping quotes *) +fun strip [] = [] | +strip ("\""::r) = strip r | +strip (a::r) = a :: (strip r); +fun strip_quote s = implode(strip(explode(s))); + +(* used by *_of_varlist *) +fun extract_first (a,b) = strip_quote a; +fun extract_second (a,b) = strip_quote b; +(* following functions producing sth from a varlist *) +fun comma_list_of_varlist [] = "" | +comma_list_of_varlist [a] = extract_first a | +comma_list_of_varlist (a::r) = (extract_first a) ^ "," ^ (comma_list_of_varlist r); +fun primed_comma_list_of_varlist [] = "" | +primed_comma_list_of_varlist [a] = (extract_first a) ^ "'" | +primed_comma_list_of_varlist (a::r) = (extract_first a) ^ "'," ^ + (primed_comma_list_of_varlist r); +fun type_product_of_varlist [] = "" | +type_product_of_varlist [a] = "(" ^ extract_second(a) ^ ")" | +type_product_of_varlist(a::r) = "(" ^ extract_second(a) ^ ")*" ^ type_product_of_varlist r; + +(* listing a list *) +fun list_elements_of [] = "" | +list_elements_of (a::r) = a ^ " " ^ (list_elements_of r); + +(* extracting type parameters from a type list *) +(* fun param_tupel thy [] res = res | +param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res | +param_tupel thy ((TFree(a,_))::r) res = +if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) | +param_tupel thy (a::r) res = +error ("one component of a statetype is a TVar: " ^ (Sign.string_of_typ (sign_of thy) a)); +*) + +(* used by constr_list *) +fun extract_constrs thy [] = [] | +extract_constrs thy (a::r) = +let +fun is_prefix [] s = true +| is_prefix (p::ps) [] = false +| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs); +fun delete_bold [] = [] +| delete_bold (x::xs) = if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs)) + then (let val (_::_::_::s) = xs in delete_bold s end) + else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs)) + then (let val (_::_::_::s) = xs in delete_bold s end) + else (x::delete_bold xs)); +fun delete_bold_string s = implode(delete_bold(explode s)); +(* from a constructor term in *.induct (with quantifiers, +"Trueprop" and ?P stripped away) delivers the head *) +fun extract_hd (_ $ Abs(_,_,r)) = extract_hd r | +extract_hd (Const("Trueprop",_) $ r) = extract_hd r | +extract_hd (Var(_,_) $ r) = extract_hd r | +extract_hd (a $ b) = extract_hd a | +extract_hd (Const(s,_)) = s | +extract_hd _ = raise malformed; +(* delivers constructor term string from a prem of *.induct *) +fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(variant_abs(a,T,r)))| +extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | +extract_constr thy (Var(_,_) $ r) = delete_bold_string(Sign.string_of_term (sign_of thy) r) | +extract_constr _ _ = raise malformed; +in +(extract_hd a,extract_constr thy a) :: (extract_constrs thy r) +end; + +(* delivering list of constructor terms of a datatype *) +fun constr_list thy atyp = +let +fun act_name thy (Type(s,_)) = s | +act_name _ s = +error("malformed action type: " ^ (Sign.string_of_typ (sign_of thy) s)); +fun afpl ("." :: a) = [] | +afpl [] = [] | +afpl (a::r) = a :: (afpl r); +fun unqualify s = implode(rev(afpl(rev(explode s)))); +val q_atypstr = act_name thy atyp; +val uq_atypstr = unqualify q_atypstr; +val prem = prems_of (get_thm thy (uq_atypstr ^ ".induct")); +in +extract_constrs thy prem +handle malformed => +error("malformed theorem : " ^ uq_atypstr ^ ".induct") +end; + +fun check_for_constr thy atyp (a $ b) = +let +fun all_free (Free(_,_)) = true | +all_free (a $ b) = if (all_free a) then (all_free b) else false | +all_free _ = false; +in +if (all_free b) then (check_for_constr thy atyp a) else false +end | +check_for_constr thy atyp (Const(a,_)) = +let +val cl = constr_list thy atyp; +fun fstmem a [] = false | +fstmem a ((f,s)::r) = if (a=f) then true else (fstmem a r) +in +if (fstmem a cl) then true else false +end | +check_for_constr _ _ _ = false; + +(* delivering the free variables of a constructor term *) +fun free_vars_of (t1 $ t2) = (free_vars_of t1) @ (free_vars_of t2) | +free_vars_of (Const(_,_)) = [] | +free_vars_of (Free(a,_)) = [a] | +free_vars_of _ = raise malformed; + +(* making a constructor set from a constructor term (of signature) *) +fun constr_set_string thy atyp ctstr = +let +val trm = #t(rep_cterm(read_cterm (sign_of thy) (ctstr,atyp))); +val l = free_vars_of trm +in +if (check_for_constr thy atyp trm) then +(if (l=[]) then ("{" ^ ctstr ^ "}") +else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") +else (raise malformed) +handle malformed => +error("malformed action term: " ^ (Sign.string_of_term (sign_of thy) trm)) +end; + +(* extracting constructor heads *) +fun constructor_head thy atypstr s = +let +fun hd_of (Const(a,_)) = a | +hd_of (t $ _) = hd_of t | +hd_of _ = raise malformed; +val trm = #t(rep_cterm(read_cterm (sign_of thy) (s,#T(rep_ctyp(read_ctyp (sign_of thy) atypstr))) )) +in +hd_of trm handle malformed => +error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s) +end; +fun constructor_head_list _ _ [] = [] | +constructor_head_list thy atypstr (a::r) = + (constructor_head thy atypstr a)::(constructor_head_list thy atypstr r); + +(* producing an action set *) +fun action_set_string thy atyp [] = "{}" | +action_set_string thy atyp [a] = constr_set_string thy atyp (strip_quote a) | +action_set_string thy atyp (a::r) = (constr_set_string thy atyp (strip_quote a)) ^ + " Un " ^ (action_set_string thy atyp r); + +(* used by extend *) +fun pstr s [] = "(" ^ s ^ "' = " ^ s ^ ")" | +pstr s ((a,b)::r) = +if (s=a) then ("(" ^ s ^ "' = (" ^ b ^ "))") else (pstr s r); +fun poststring [] l = "" | +poststring [(a,b)] l = pstr a l | +poststring ((a,b)::r) l = (pstr a l) ^ " & " ^ (poststring r l); + +(* extends a (action string,condition,assignlist) tupel by a +(action term,action string,condition,pseudo_condition,bool) tupel, used by extended_list +(where bool indicates whether there is a precondition *) +fun extend thy atyp statetupel (actstr,r,[]) = +let +val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp))); +val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[])))); +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true +in +if (check_for_constr thy atyp trm) +then (trm,actstr, "(" ^ r ^ ") & " ^ (poststring statetupel []),r,flag) +else +error("transition " ^ actstr ^ " is not a pure constructor term") +end | +extend thy atyp statetupel (actstr,r,(a,b)::c) = +let +fun pseudo_poststring [] = "" | +pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" | +pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); +val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp))); +val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[])))); +val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true +in +if (check_for_constr thy atyp trm) then +(if ((a="") andalso (b="") andalso (c=[])) then (trm,actstr,r,"True",false) +(* the case with transrel *) + else + (trm,actstr,"(" ^ r ^ ") & " ^ (poststring statetupel ((a,b)::c)), + "(" ^ r ^ ") & " ^ (pseudo_poststring ((a,b)::c)),flag)) +else +error("transition " ^ actstr ^ " is not a pure constructor term") +end; +(* used by make_alt_string *) +fun extended_list _ _ _ [] = [] | +extended_list thy atyp statetupel (a::r) = + (extend thy atyp statetupel a) :: (extended_list thy atyp statetupel r); + +(* used by write_alts *) +fun write_alt thy (chead,tr) inp out int [] = +if (chead mem inp) then +( +error("Input action " ^ tr ^ " was not specified") +) else ( +if (chead mem (out@int)) then +(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else print(""); +(tr ^ " => False",tr ^ " => False")) | +write_alt thy (chead,ctrm) inp out int ((a,b,c,d,e)::r) = +let +fun hd_of (Const(a,_)) = a | +hd_of (t $ _) = hd_of t | +hd_of _ = raise malformed; +fun occurs_again c [] = false | +occurs_again c ((a,_,_,_,_)::r) = if (c=(hd_of a)) then true else (occurs_again c r); +in +if (chead=(hd_of a)) then +(if ((chead mem inp) andalso e) then ( +error("Input action " ^ b ^ " has a precondition") +) else (if (chead mem (inp@out@int)) then + (if (occurs_again chead r) then ( +error("Two specifications for action: " ^ b) + ) else (b ^ " => " ^ c,b ^ " => " ^ d)) + else ( +error("Action " ^ b ^ " is not in automaton signature") +))) else (write_alt thy (chead,ctrm) inp out int r) +handle malformed => +error ("malformed action term: " ^ (Sign.string_of_term (sign_of thy) a)) +end; + +(* used by make_alt_string *) +fun write_alts thy (a,b) inp out int [] ttr = (a,b) | +write_alts thy (a,b) inp out int [c] ttr = +let +val wa = write_alt thy c inp out int ttr +in + (a ^ (fst wa),b ^ (snd wa)) +end | +write_alts thy (a,b) inp out int (c::r) ttr = +let +val wa = write_alt thy c inp out int ttr +in + write_alts thy (a ^ (fst wa) ^ " | ", b ^ (snd wa) ^ " | ") inp out int r ttr +end; + +fun make_alt_string thy inp out int atyp statetupel trans = +let +val cl = constr_list thy atyp; +val ttr = extended_list thy atyp statetupel trans; +in +write_alts thy ("","") inp out int cl ttr +end; + +(* used in gen_add_ioa *) +fun check_free_primed (Free(a,_)) = +let +val (f::r) = rev(explode a) +in +if (f="'") then [a] else [] +end | +check_free_primed (a $ b) = ((check_free_primed a) @ (check_free_primed b)) | +check_free_primed (Abs(_,_,t)) = check_free_primed t | +check_free_primed _ = []; + +fun overlap [] _ = true | +overlap (a::r) l = if (a mem l) then ( +error("Two occurences of action " ^ a ^ " in automaton signature") +) else (overlap r l); + +(* delivering some types of an automaton *) +fun aut_type_of thy aut_name = +let +fun left_of (( _ $ left) $ _) = left | +left_of _ = raise malformed; +val aut_def = concl_of(get_thm thy (aut_name ^ "_def")); +in +(#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def)))) +handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") +end; + +fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp | +act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ +(Sign.string_of_typ (sign_of thy) t)); +fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp | +st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ +(Sign.string_of_typ (sign_of thy) t)); + +fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | +comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | +comp_st_type_of _ _ = error "empty automaton list"; + +(* checking consistency of action types (for composition) *) +fun check_ac thy (a::r) = +let +fun ch_f_a thy acttyp [] = acttyp | +ch_f_a thy acttyp (a::r) = +let +val auttyp = aut_type_of thy a; +val ac = (act_type_of thy auttyp); +in +if (ac=acttyp) then (ch_f_a thy acttyp r) else (error "A") +end; +val auttyp = aut_type_of thy a; +val acttyp = (act_type_of thy auttyp); +in +ch_f_a thy acttyp r +end | +check_ac _ [] = error "empty automaton list"; + +fun clist [] = "" | +clist [a] = a | +clist (a::r) = a ^ " || " ^ (clist r); + +(* gen_add_ioa *) + +fun gen_add_ioa prep_term automaton_name action_type inp out int statetupel ini trans thy = +(writeln("Constructing automaton " ^ automaton_name ^ "..."); +let +val state_type_string = type_product_of_varlist(statetupel); +val styp = #T(rep_ctyp (read_ctyp (sign_of thy) state_type_string)) ; +val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")"; +val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")"; +val atyp = #T(rep_ctyp (read_ctyp (sign_of thy) action_type)); +val inp_set_string = action_set_string thy atyp inp; +val out_set_string = action_set_string thy atyp out; +val int_set_string = action_set_string thy atyp int; +val inp_head_list = constructor_head_list thy action_type inp; +val out_head_list = constructor_head_list thy action_type out; +val int_head_list = constructor_head_list thy action_type int; +val overlap_flag = ((overlap inp out) andalso (overlap inp int) andalso (overlap out int)); +val alt_string = make_alt_string thy inp_head_list out_head_list int_head_list + atyp statetupel trans; +val thy2 = (thy +|> ContConsts.add_consts +[(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn), +(automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn), +(automaton_name ^ "_trans", + "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), +(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] +|> (PureThy.add_defs o map no_attributes) (* old: Attributes.none *) +[(automaton_name ^ "_initial_def", +automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), +(automaton_name ^ "_asig_def", +automaton_name ^ "_asig == (" ^ + inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), +(automaton_name ^ "_trans_def", +automaton_name ^ "_trans == {(" ^ + state_vars_tupel ^ ", act_of_" ^ automaton_name ^ ", " ^ state_vars_primed ^ +"). case act_of_" ^ automaton_name ^ " of " ^ fst(alt_string) ^ "}"), +(automaton_name ^ "_def", +automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^ +"_initial, " ^ automaton_name ^ "_trans,{},{})") +]) +val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm (sign_of thy2) +( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string),Type("bool",[])))))); +in +( +if (chk_prime_list = []) then thy2 +else ( +error("Precondition or assignment terms in postconditions contain following primed variables:\n" + ^ (list_elements_of chk_prime_list))) +) +end) + +fun gen_add_composition prep_term automaton_name aut_list thy = +(writeln("Constructing automaton " ^ automaton_name ^ "..."); +let +val acttyp = check_ac thy aut_list; +val st_typ = comp_st_type_of thy aut_list; +val comp_list = clist aut_list; +in +thy +|> ContConsts.add_consts_i +[(automaton_name, +Type("*", +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), + Type("*",[Type("set",[st_typ]), + Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), + Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) +,NoSyn)] +|> (PureThy.add_defs o map no_attributes) +[(automaton_name ^ "_def", +automaton_name ^ " == " ^ comp_list)] +end) + +fun gen_add_restriction prep_term automaton_name aut_source actlist thy = +(writeln("Constructing automaton " ^ automaton_name ^ "..."); +let +val auttyp = aut_type_of thy aut_source; +val acttyp = act_type_of thy auttyp; +val rest_set = action_set_string thy acttyp actlist +in +thy +|> ContConsts.add_consts_i +[(automaton_name, auttyp,NoSyn)] +|> (PureThy.add_defs o map no_attributes) +[(automaton_name ^ "_def", +automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] +end) +fun gen_add_hiding prep_term automaton_name aut_source actlist thy = +(writeln("Constructing automaton " ^ automaton_name ^ "..."); +let +val auttyp = aut_type_of thy aut_source; +val acttyp = act_type_of thy auttyp; +val hid_set = action_set_string thy acttyp actlist +in +thy +|> ContConsts.add_consts_i +[(automaton_name, auttyp,NoSyn)] +|> (PureThy.add_defs o map no_attributes) +[(automaton_name ^ "_def", +automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] +end) + +fun ren_act_type_of thy funct = +let +(* going into a pseudo-proof-state to enable the use of function read *) +val _ = goal thy (funct ^ " = t"); +fun arg_typ_of (Type("fun",[a,b])) = a | +arg_typ_of _ = raise malformed; +in +arg_typ_of(#T(rep_cterm(cterm_of (sign_of thy) (read(funct))))) +handle malformed => error ("could not extract argument type of renaming function term") +end; + +fun gen_add_rename prep_term automaton_name aut_source fun_name thy = +(writeln("Constructing automaton " ^ automaton_name ^ "..."); +let +val auttyp = aut_type_of thy aut_source; +val st_typ = st_type_of thy auttyp; +val acttyp = ren_act_type_of thy fun_name +in +thy +|> ContConsts.add_consts_i +[(automaton_name, +Type("*", +[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), + Type("*",[Type("set",[st_typ]), + Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), + Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) +,NoSyn)] +|> (PureThy.add_defs o map no_attributes) +[(automaton_name ^ "_def", +automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] +end) + +(* external interfaces *) + +fun read_term sg str = + read_cterm sg (str, HOLogic.termTVar); + +fun cert_term sg tm = + cterm_of sg tm handle TERM (msg, _) => error msg; + +in + +val add_ioa = gen_add_ioa read_term; +val add_ioa_i = gen_add_ioa cert_term; +val add_composition = gen_add_composition read_term; +val add_composition_i = gen_add_composition cert_term; +val add_hiding = gen_add_hiding read_term; +val add_hiding_i = gen_add_hiding cert_term; +val add_restriction = gen_add_restriction read_term; +val add_restriction_i = gen_add_restriction cert_term; +val add_rename = gen_add_rename read_term; +val add_rename_i = gen_add_rename cert_term; + +end + +end; diff -r 2eba94dc5951 -r 863834a37769 src/HOLCF/IOA/meta_theory/ioa_syn.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/ioa_syn.ML Thu Apr 22 11:00:30 1999 +0200 @@ -0,0 +1,170 @@ +local + +open ThyParse; + +(* encoding transition specifications with a element of ParseTrans *) +datatype ParseTrans = Rel of string | PP of string*(string*string)list; +fun mk_trans_of_rel s = Rel(s); +fun mk_trans_of_prepost (s,l) = PP(s,l); + +(* stripping quotes of a string *) +fun strip [] = [] | +strip ("\""::r) = strip r | +strip (a::b) = a :: (strip b); +fun strip_quote s = implode(strip(explode(s))); + +fun comma_list_of [] = "" | +comma_list_of [a] = a | +comma_list_of (a::r) = a ^ ", " ^ (comma_list_of r); + +fun pair_of (a,b) = "(" ^ a ^ "," ^ b ^ ")"; +fun pair_list_of [] = "" | +pair_list_of [a] = pair_of a | +pair_list_of (a::r) = (pair_of a) ^ ", " ^ (pair_list_of r); + +fun trans_of (a,Rel(b)) = "(" ^ a ^ "," ^ b ^ ", [(\"\",\"\")])" | +trans_of (a,PP(b,l)) = "(" ^ a ^ "," ^ b ^ ",[" ^ (pair_list_of l) ^ "])"; +fun trans_list_of [] = "" | +trans_list_of [a] = trans_of a | +trans_list_of (a::r) = (trans_of a) ^ ", " ^ (trans_list_of r); + +(**************************************************************************) +(* In den folgenden Funktionen stehen in der ersten Komponente des *) +(* Ergebnispaares die entsprechenden Funktionsaufrufe aus ioa_package.ML, *) +(* welche die entsprechenden Automatendefinitionen generieren. *) +(* In der zweiten Komponente m"ussen diese Definitionen nochmal *) +(* aufgef"uhrt werden, damit diese dann als Axiome genutzt werden k"onnen *) +(**************************************************************************) +fun mk_ioa_decl t (aut,((((((action_type,inp),out),int),states),initial),trans)) = +let +val automaton_name = strip_quote aut; +in +( +"|> IoaPackage.add_ioa " ^ aut ^ " " ^ action_type ^ "\n" ^ +"[" ^ (comma_list_of inp) ^ "]\n" ^ +"[" ^ (comma_list_of out) ^ "]\n" ^ +"[" ^ (comma_list_of int) ^ "]\n" ^ +"[" ^ (pair_list_of states) ^ "]\n" ^ +initial ^ "\n" ^ +"[" ^ (trans_list_of trans) ^ "]" +, +[automaton_name ^ "_initial_def", automaton_name ^ "_asig_def" +,automaton_name ^ "_trans_def",automaton_name ^ "_def"] +) +end; + +fun mk_composition_decl (aut,autlist) = +let +val automaton_name = strip_quote aut; +in +( +"|> IoaPackage.add_composition " ^ aut ^ "\n" ^ +"[" ^ (comma_list_of autlist) ^ "]" +, +[automaton_name ^ "_def"] +) +end; + +fun mk_hiding_decl (aut,(actlist,source_aut)) = +let +val automaton_name = strip_quote aut; +val source_name = strip_quote source_aut; +in +( +"|> IoaPackage.add_hiding " ^ aut ^ " " ^ source_aut ^ "\n" ^ +"[" ^ (comma_list_of actlist) ^ "]" +, +[automaton_name ^ "_def"] +) +end; + +fun mk_restriction_decl (aut,(source_aut,actlist)) = +let +val automaton_name = strip_quote aut; +val source_name = strip_quote source_aut; +in +( +"|> IoaPackage.add_restriction " ^ aut ^ " " ^ source_aut ^ "\n" ^ +"[" ^ (comma_list_of actlist) ^ "]" +, +[automaton_name ^ "_def"] +) +end; + +fun mk_rename_decl (aut,(source_aut,rename_f)) = +let +val automaton_name = strip_quote aut; +in +("|> IoaPackage.add_rename " ^ aut ^ " " ^ source_aut ^ " " ^ rename_f +, +[automaton_name ^ "_def"] +) +end; + +(****************************************************************) +(* Ab hier Angabe der Einlesepattern f"ur die Sektion automaton *) +(****************************************************************) +val actionlist = enum1 "," (string) +val inputslist = "inputs" $$-- actionlist +val outputslist = "outputs" $$-- actionlist +val internalslist = "internals" $$-- actionlist +val stateslist = + "states" $$-- + repeat1 (name --$$ "::" -- typ) +val initial = + "initially" $$-- string +val assign_list = enum1 "," (name --$$ ":=" -- string) +val pre = + "pre" $$-- string +val post = + "post" $$-- assign_list +val post1 = ((optional pre "\"True\"") -- post) >> mk_trans_of_prepost +val pre1 = (pre -- (optional post [])) >> mk_trans_of_prepost +val transrel = ("transrel" $$-- string) >> mk_trans_of_rel +val transition = string -- + (transrel || pre1 || post1) +val translist = "transitions" $$-- + repeat1 (transition) +val ioa_decl = + (name -- ("=" $$-- + ("signature" $$-- + ("actions" $$-- + (typ -- + (optional inputslist []) -- + (optional outputslist []) -- + (optional internalslist []) -- + stateslist -- + (optional initial "\"True\"") -- + translist) + ))) + >> mk_ioa_decl thy) +|| + (name -- ("=" $$-- + ("compose" $$-- (enum1 "," name))) >> mk_composition_decl) +|| + (name -- ("=" $$-- + ("hide" $$-- (enum1 "," string) -- + ("in" $$-- name))) >> mk_hiding_decl) +|| + (name -- ("=" $$-- + ("restrict" $$-- name -- + ("to" $$-- (enum1 "," string)))) >> mk_restriction_decl) +|| + (name -- ("=" $$-- + ("rename" $$-- name -- ("with" $$-- string))) >> mk_rename_decl) +; + +in +(******************************************************************) +(* im folgenden werden in der ersten Liste alle beim Einlesen von *) +(* Automaten vorkommende Schl"usselw"orter aufgef"uhrt, in der *) +(* zweiten Liste wird die Syntaxsektion automaton definiert *) +(* mitsamt dessen Einlesepattern ioa_decl *) +(******************************************************************) +val _ = ThySyn.add_syntax + ["signature","actions","inputs", "outputs", "internals", "states", "initially", + "transitions", "pre", "post", "transrel",":=", +"compose","hide","in","restrict","to","rename","with"] + [axm_section "automaton" "" ioa_decl]; + +end;