50 (* fun param_tupel thy [] res = res | |
53 (* fun param_tupel thy [] res = res | |
51 param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res | |
54 param_tupel thy ((Type(_,l))::r) res = param_tupel thy (l @ r) res | |
52 param_tupel thy ((TFree(a,_))::r) res = |
55 param_tupel thy ((TFree(a,_))::r) res = |
53 if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) | |
56 if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) | |
54 param_tupel thy (a::r) res = |
57 param_tupel thy (a::r) res = |
55 error ("one component of a statetype is a TVar: " ^ (Sign.string_of_typ (sign_of thy) a)); |
58 error ("one component of a statetype is a TVar: " ^ (string_of_typ (sign_of thy) a)); |
56 *) |
59 *) |
57 |
60 |
58 (* used by constr_list *) |
61 (* used by constr_list *) |
59 fun extract_constrs thy [] = [] | |
62 fun extract_constrs thy [] = [] | |
60 extract_constrs thy (a::r) = |
63 extract_constrs thy (a::r) = |
78 extract_hd (Const(s,_)) = s | |
81 extract_hd (Const(s,_)) = s | |
79 extract_hd _ = raise malformed; |
82 extract_hd _ = raise malformed; |
80 (* delivers constructor term string from a prem of *.induct *) |
83 (* delivers constructor term string from a prem of *.induct *) |
81 fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(variant_abs(a,T,r)))| |
84 fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(variant_abs(a,T,r)))| |
82 extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | |
85 extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r | |
83 extract_constr thy (Var(_,_) $ r) = delete_bold_string(Sign.string_of_term (sign_of thy) r) | |
86 extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term (sign_of thy) r) | |
84 extract_constr _ _ = raise malformed; |
87 extract_constr _ _ = raise malformed; |
85 in |
88 in |
86 (extract_hd a,extract_constr thy a) :: (extract_constrs thy r) |
89 (extract_hd a,extract_constr thy a) :: (extract_constrs thy r) |
87 end; |
90 end; |
88 |
91 |
89 (* delivering list of constructor terms of a datatype *) |
92 (* delivering list of constructor terms of a datatype *) |
90 fun constr_list thy atyp = |
93 fun constr_list thy atyp = |
91 let |
94 let |
92 fun act_name thy (Type(s,_)) = s | |
95 fun act_name thy (Type(s,_)) = s | |
93 act_name _ s = |
96 act_name _ s = |
94 error("malformed action type: " ^ (Sign.string_of_typ (sign_of thy) s)); |
97 error("malformed action type: " ^ (string_of_typ (sign_of thy) s)); |
95 fun afpl ("." :: a) = [] | |
98 fun afpl ("." :: a) = [] | |
96 afpl [] = [] | |
99 afpl [] = [] | |
97 afpl (a::r) = a :: (afpl r); |
100 afpl (a::r) = a :: (afpl r); |
98 fun unqualify s = implode(rev(afpl(rev(explode s)))); |
101 fun unqualify s = implode(rev(afpl(rev(explode s)))); |
99 val q_atypstr = act_name thy atyp; |
102 val q_atypstr = act_name thy atyp; |
138 if (check_for_constr thy atyp trm) then |
141 if (check_for_constr thy atyp trm) then |
139 (if (l=[]) then ("{" ^ ctstr ^ "}") |
142 (if (l=[]) then ("{" ^ ctstr ^ "}") |
140 else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") |
143 else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})") |
141 else (raise malformed) |
144 else (raise malformed) |
142 handle malformed => |
145 handle malformed => |
143 error("malformed action term: " ^ (Sign.string_of_term (sign_of thy) trm)) |
146 error("malformed action term: " ^ (string_of_term (sign_of thy) trm)) |
144 end; |
147 end; |
145 |
148 |
146 (* extracting constructor heads *) |
149 (* extracting constructor heads *) |
147 fun constructor_head thy atypstr s = |
150 fun constructor_head thy atypstr s = |
148 let |
151 let |
235 ) else (b ^ " => " ^ c,b ^ " => " ^ d)) |
238 ) else (b ^ " => " ^ c,b ^ " => " ^ d)) |
236 else ( |
239 else ( |
237 error("Action " ^ b ^ " is not in automaton signature") |
240 error("Action " ^ b ^ " is not in automaton signature") |
238 ))) else (write_alt thy (chead,ctrm) inp out int r) |
241 ))) else (write_alt thy (chead,ctrm) inp out int r) |
239 handle malformed => |
242 handle malformed => |
240 error ("malformed action term: " ^ (Sign.string_of_term (sign_of thy) a)) |
243 error ("malformed action term: " ^ (string_of_term (sign_of thy) a)) |
241 end; |
244 end; |
242 |
245 |
243 (* used by make_alt_string *) |
246 (* used by make_alt_string *) |
244 fun write_alts thy (a,b) inp out int [] ttr = (a,b) | |
247 fun write_alts thy (a,b) inp out int [] ttr = (a,b) | |
245 write_alts thy (a,b) inp out int [c] ttr = |
248 write_alts thy (a,b) inp out int [c] ttr = |
290 handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") |
293 handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def") |
291 end; |
294 end; |
292 |
295 |
293 fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp | |
296 fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp | |
294 act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ |
297 act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^ |
295 (Sign.string_of_typ (sign_of thy) t)); |
298 (string_of_typ (sign_of thy) t)); |
296 fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp | |
299 fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp | |
297 st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ |
300 st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^ |
298 (Sign.string_of_typ (sign_of thy) t)); |
301 (string_of_typ (sign_of thy) t)); |
299 |
302 |
300 fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | |
303 fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) | |
301 comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | |
304 comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) | |
302 comp_st_type_of _ _ = error "empty automaton list"; |
305 comp_st_type_of _ _ = error "empty automaton list"; |
303 |
306 |
490 (* parsers *) |
493 (* parsers *) |
491 |
494 |
492 local structure P = OuterParse and K = OuterKeyword in |
495 local structure P = OuterParse and K = OuterKeyword in |
493 |
496 |
494 val actionlist = P.list1 P.term; |
497 val actionlist = P.list1 P.term; |
495 val inputslist = P.$$$ "inputs" |-- actionlist; |
498 val inputslist = P.$$$ "inputs" |-- P.!!! actionlist; |
496 val outputslist = P.$$$ "outputs" |-- actionlist; |
499 val outputslist = P.$$$ "outputs" |-- P.!!! actionlist; |
497 val internalslist = P.$$$ "internals" |-- actionlist; |
500 val internalslist = P.$$$ "internals" |-- P.!!! actionlist; |
498 val stateslist = P.$$$ "states" |-- Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ); |
501 val stateslist = P.$$$ "states" |-- P.!!! (Scan.repeat1 (P.name --| P.$$$ "::" -- P.typ)); |
499 val initial = P.$$$ "initially" |-- P.term; |
502 val initial = P.$$$ "initially" |-- P.!!! P.term; |
500 val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.term); |
503 val assign_list = P.list1 (P.name --| P.$$$ ":=" -- P.!!! P.term); |
501 val pre = P.$$$ "pre" |-- P.term; |
504 val pre = P.$$$ "pre" |-- P.!!! P.term; |
502 val post = P.$$$ "post" |-- assign_list; |
505 val post = P.$$$ "post" |-- P.!!! assign_list; |
503 val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; |
506 val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; |
504 val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; |
507 val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; |
505 val transrel = (P.$$$ "transrel" |-- P.term) >> mk_trans_of_rel; |
508 val transrel = (P.$$$ "transrel" |-- P.!!! P.term) >> mk_trans_of_rel; |
506 val transition = P.term -- (transrel || pre1 || post1); |
509 val transition = P.term -- (transrel || pre1 || post1); |
507 val translist = P.$$$ "transitions" |-- Scan.repeat1 transition; |
510 val translist = P.$$$ "transitions" |-- P.!!! (Scan.repeat1 transition); |
508 |
511 |
509 val ioa_decl = |
512 val ioa_decl = |
510 (P.name -- (P.$$$ "=" |-- |
513 (P.name -- (P.$$$ "=" |-- |
511 (P.$$$ "signature" |-- |
514 (P.$$$ "signature" |-- |
512 (P.$$$ "actions" |-- |
515 P.!!! (P.$$$ "actions" |-- |
513 (P.typ -- |
516 (P.typ -- |
514 (Scan.optional inputslist []) -- |
517 (Scan.optional inputslist []) -- |
515 (Scan.optional outputslist []) -- |
518 (Scan.optional outputslist []) -- |
516 (Scan.optional internalslist []) -- |
519 (Scan.optional internalslist []) -- |
517 stateslist -- |
520 stateslist -- |
518 (Scan.optional initial "True") -- |
521 (Scan.optional initial "True") -- |
519 translist))))) >> mk_ioa_decl || |
522 translist))))) >> mk_ioa_decl || |
520 (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.list1 P.name))) >> mk_composition_decl || |
523 (P.name -- (P.$$$ "=" |-- (P.$$$ "compose" |-- P.!!! (P.list1 P.name)))) |
521 (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- P.list1 P.term -- (P.$$$ "in" |-- P.name)))) |
524 >> mk_composition_decl || |
522 >> mk_hiding_decl || |
525 (P.name -- (P.$$$ "=" |-- (P.$$$ "hide_action" |-- |
523 (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- P.name -- (P.$$$ "to" |-- P.list1 P.term)))) |
526 P.!!! (P.list1 P.term -- (P.$$$ "in" |-- P.name))))) >> mk_hiding_decl || |
524 >> mk_restriction_decl || |
527 (P.name -- (P.$$$ "=" |-- (P.$$$ "restrict" |-- |
525 (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- P.name -- (P.$$$ "to" |-- P.term)))) |
528 P.!!! (P.name -- (P.$$$ "to" |-- P.list1 P.term))))) >> mk_restriction_decl || |
|
529 (P.name -- (P.$$$ "=" |-- (P.$$$ "rename" |-- (P.!!! (P.name -- (P.$$$ "to" |-- P.term)))))) |
526 >> mk_rename_decl; |
530 >> mk_rename_decl; |
527 |
531 |
528 val automatonP = |
532 val automatonP = |
529 OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl |
533 OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" K.thy_decl |
530 (ioa_decl >> Toplevel.theory); |
534 (ioa_decl >> Toplevel.theory); |