# HG changeset patch # User wenzelm # Date 1278966941 -7200 # Node ID 173667d73115b186c75d9f0f07bbe4036e3e7b3b # Parent 1d639d28832c9311a668121d94680b44d18e8c23 removed unused/untested IOA 'automaton' package; diff -r 1d639d28832c -r 173667d73115 Admin/update-keywords --- a/Admin/update-keywords Mon Jul 12 22:17:31 2010 +0200 +++ b/Admin/update-keywords Mon Jul 12 22:35:41 2010 +0200 @@ -12,7 +12,7 @@ isabelle keywords \ "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" \ - "$LOG/IOA.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" + "$LOG/HOL-Boogie.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" isabelle keywords -k ZF \ "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz" diff -r 1d639d28832c -r 173667d73115 etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Jul 12 22:17:31 2010 +0200 +++ b/etc/isar-keywords.el Mon Jul 12 22:35:41 2010 +0200 @@ -1,6 +1,6 @@ ;; ;; Keyword classification tables for Isabelle/Isar. -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace. +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + HOL-Boogie + HOL-Nominal + HOL-Statespace. ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** ;; @@ -31,7 +31,6 @@ "assume" "atom_decl" "attribute_setup" - "automaton" "ax_specification" "axiomatization" "axioms" @@ -279,15 +278,13 @@ "}")) (defconst isar-keywords-minor - '("actions" - "advanced" + '("advanced" "and" "assumes" "attach" "avoids" "begin" "binder" - "compose" "congs" "constrains" "contains" @@ -297,7 +294,6 @@ "fixes" "for" "functions" - "hide_action" "hints" "identifier" "if" @@ -306,9 +302,6 @@ "infix" "infixl" "infixr" - "initially" - "inputs" - "internals" "is" "lazy" "module_name" @@ -318,21 +311,11 @@ "obtains" "open" "output" - "outputs" "overloaded" "permissive" "pervasive" - "post" - "pre" - "rename" - "restrict" "shows" - "signature" - "states" "structure" - "to" - "transitions" - "transrel" "unchecked" "uses" "where")) @@ -453,7 +436,6 @@ "arities" "atom_decl" "attribute_setup" - "automaton" "axiomatization" "axioms" "boogie_end" diff -r 1d639d28832c -r 173667d73115 src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Mon Jul 12 22:17:31 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Mon Jul 12 22:35:41 2010 +0200 @@ -6,7 +6,6 @@ theory Abstraction imports LiveIOA -uses ("automaton.ML") begin default_sort type @@ -613,6 +612,4 @@ method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} "" -use "automaton.ML" - end diff -r 1d639d28832c -r 173667d73115 src/HOLCF/IOA/meta_theory/automaton.ML --- a/src/HOLCF/IOA/meta_theory/automaton.ML Mon Jul 12 22:17:31 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,529 +0,0 @@ -(* Title: HOLCF/IOA/meta_theory/automaton.ML - Author: Tobias Hamberger, TU Muenchen -*) - -signature AUTOMATON = -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_composition : string -> (string)list -> theory -> theory - val add_hiding : string -> string -> (string)list -> theory -> theory - val add_restriction : string -> string -> (string)list -> theory -> theory - val add_rename : string -> string -> string -> theory -> theory -end; - -structure Automaton: AUTOMATON = -struct - -val string_of_typ = Print_Mode.setmp [] o Syntax.string_of_typ_global; -val string_of_term = Print_Mode.setmp [] o Syntax.string_of_term_global; - -exception malformed; - -(* 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: " ^ (string_of_typ thy a)); -*) - -(* used by constr_list *) -fun extract_constrs thy [] = [] | -extract_constrs thy (a::r) = -let -fun delete_bold [] = [] -| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs)) - then (let val (_::_::_::s) = xs in delete_bold s end) - else (if (is_prefix (op =) ("\^["::"["::"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(Syntax.variant_abs(a,T,r)))| -extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | -extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term 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: " ^ (string_of_typ 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 (PureThy.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 = Misc_Legacy.simple_read_term thy atyp ctstr; -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: " ^ (string_of_term 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 = Misc_Legacy.simple_read_term thy (Syntax.read_typ_global thy atypstr) s; -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 *) -(*FIXME*) -fun action_set_string thy atyp [] = "Set.empty" | -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 = Misc_Legacy.simple_read_term thy atyp actstr; -val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r; -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 = Misc_Legacy.simple_read_term thy atyp actstr; -val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r; -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 member (op =) inp chead then -( -error("Input action " ^ tr ^ " was not specified") -) else ( -if member (op =) out chead orelse member (op =) int chead then -(writeln("Action " ^ tr ^ " was completedly disabled due to missing specification")) else (); -(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 member (op =) inp chead andalso e then ( -error("Input action " ^ b ^ " has a precondition") -) else (if member (op =) (inp@out@int) chead 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: " ^ (string_of_term 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 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 member (op =) l a 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 (PureThy.get_thm thy (aut_name ^ "_def")); -in -(#T(rep_cterm(cterm_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" ^ -(string_of_typ 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" ^ -(string_of_typ 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) = HOLogic.mk_prodT (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); - -val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name)); - - -(* add_ioa *) - -fun add_ioa 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 = Syntax.read_typ_global 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 = Syntax.read_typ_global 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 -|> Sign.add_consts -[(Binding.name (automaton_name ^ "_initial"), "(" ^ state_type_string ^ ")set" ,NoSyn), -(Binding.name (automaton_name ^ "_asig"), "(" ^ action_type ^ ")signature" ,NoSyn), -(Binding.name (automaton_name ^ "_trans"), - "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), -(Binding.name automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] -|> add_defs -[(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 (Misc_Legacy.simple_read_term thy2 (Type("bool",[])) -( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string)))) -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 add_composition automaton_name aut_list thy = - let - val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...") - 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 - |> Sign.add_consts_i - [(Binding.name automaton_name, HOLogic.mk_prodT (HOLogic.mk_prodT - (HOLogic.mk_setT acttyp, HOLogic.mk_prodT (HOLogic.mk_setT acttyp, HOLogic.mk_setT acttyp)), - HOLogic.mk_prodT (HOLogic.mk_setT st_typ, HOLogic.mk_prodT (HOLogic.mk_setT - (HOLogic.mk_prodT (st_typ, HOLogic.mk_prodT (acttyp, st_typ))), - HOLogic.mk_prodT (HOLogic.mk_setT (HOLogic.mk_setT acttyp), HOLogic.mk_setT (HOLogic.mk_setT acttyp))))), - NoSyn)] - |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == " ^ comp_list)] - end - -fun add_restriction 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 -|> Sign.add_consts_i -[(Binding.name automaton_name, auttyp,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] -end) -fun add_hiding 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 -|> Sign.add_consts_i -[(Binding.name automaton_name, auttyp,NoSyn)] -|> add_defs -[(automaton_name ^ "_def", -automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] -end) - -fun ren_act_type_of thy funct = - (case Term.fastype_of (Syntax.read_term_global thy funct) of - Type ("fun", [a, b]) => a - | _ => error "could not extract argument type of renaming function term"); - -fun add_rename automaton_name aut_source fun_name thy = - let - val _ = writeln("Constructing automaton " ^ automaton_name ^ " ...") - 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 - |> Sign.add_consts_i - [(Binding.name automaton_name, - Type(@{type_name prod}, - [Type(@{type_name prod},[HOLogic.mk_setT acttyp,Type(@{type_name prod},[HOLogic.mk_setT acttyp,HOLogic.mk_setT acttyp])]), - Type(@{type_name prod},[HOLogic.mk_setT st_typ, - Type(@{type_name prod},[HOLogic.mk_setT (Type(@{type_name prod},[st_typ,Type(@{type_name prod},[acttyp,st_typ])])), - Type(@{type_name prod},[HOLogic.mk_setT (HOLogic.mk_setT acttyp),HOLogic.mk_setT (HOLogic.mk_setT acttyp)])])])]) - ,NoSyn)] - |> add_defs [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] - end - - -(** outer syntax **) - -(* prepare results *) - -(*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); - -fun trans_of (a, Rel b) = (a, b, [("", "")]) - | trans_of (a, PP (b, l)) = (a, b, l); - - -fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = - add_ioa aut action_type inp out int states initial (map trans_of trans); - -fun mk_composition_decl (aut, autlist) = - add_composition aut autlist; - -fun mk_hiding_decl (aut, (actlist, source_aut)) = - add_hiding aut source_aut actlist; - -fun mk_restriction_decl (aut, (source_aut, actlist)) = - add_restriction aut source_aut actlist; - -fun mk_rename_decl (aut, (source_aut, rename_f)) = - add_rename aut source_aut rename_f; - - -(* outer syntax *) - -val _ = List.app Keyword.keyword ["signature", "actions", "inputs", - "outputs", "internals", "states", "initially", "transitions", "pre", - "post", "transrel", ":=", "compose", "hide_action", "in", "restrict", "to", - "rename"]; - -val actionlist = Parse.list1 Parse.term; -val inputslist = Parse.$$$ "inputs" |-- Parse.!!! actionlist; -val outputslist = Parse.$$$ "outputs" |-- Parse.!!! actionlist; -val internalslist = Parse.$$$ "internals" |-- Parse.!!! actionlist; -val stateslist = - Parse.$$$ "states" |-- Parse.!!! (Scan.repeat1 (Parse.name --| Parse.$$$ "::" -- Parse.typ)); -val initial = Parse.$$$ "initially" |-- Parse.!!! Parse.term; -val assign_list = Parse.list1 (Parse.name --| Parse.$$$ ":=" -- Parse.!!! Parse.term); -val pre = Parse.$$$ "pre" |-- Parse.!!! Parse.term; -val post = Parse.$$$ "post" |-- Parse.!!! assign_list; -val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; -val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; -val transrel = (Parse.$$$ "transrel" |-- Parse.!!! Parse.term) >> mk_trans_of_rel; -val transition = Parse.term -- (transrel || pre1 || post1); -val translist = Parse.$$$ "transitions" |-- Parse.!!! (Scan.repeat1 transition); - -val ioa_decl = - (Parse.name -- (Parse.$$$ "=" |-- - (Parse.$$$ "signature" |-- - Parse.!!! (Parse.$$$ "actions" |-- - (Parse.typ -- - (Scan.optional inputslist []) -- - (Scan.optional outputslist []) -- - (Scan.optional internalslist []) -- - stateslist -- - (Scan.optional initial "True") -- - translist))))) >> mk_ioa_decl || - (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "compose" |-- Parse.!!! (Parse.list1 Parse.name)))) - >> mk_composition_decl || - (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "hide_action" |-- - Parse.!!! (Parse.list1 Parse.term -- (Parse.$$$ "in" |-- Parse.name))))) >> mk_hiding_decl || - (Parse.name -- (Parse.$$$ "=" |-- (Parse.$$$ "restrict" |-- - Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.list1 Parse.term))))) >> mk_restriction_decl || - (Parse.name -- (Parse.$$$ "=" |-- - (Parse.$$$ "rename" |-- (Parse.!!! (Parse.name -- (Parse.$$$ "to" |-- Parse.term)))))) - >> mk_rename_decl; - -val _ = - Outer_Syntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" Keyword.thy_decl - (ioa_decl >> Toplevel.theory); - -end; diff -r 1d639d28832c -r 173667d73115 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Mon Jul 12 22:17:31 2010 +0200 +++ b/src/HOLCF/IsaMakefile Mon Jul 12 22:35:41 2010 +0200 @@ -166,7 +166,7 @@ IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ - IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/automaton.ML + IOA/meta_theory/SimCorrectness.thy @cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA