# HG changeset patch # User wenzelm # Date 925116285 -7200 # Node ID b8a1e395edd7e6b4925acaa111272a1eb36bdf27 # Parent 644d75d0dc8cdd3a6f1c2fc5e673965cd7d81eae tuned msgs; outer syntax; diff -r 644d75d0dc8c -r b8a1e395edd7 src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Fri Apr 23 17:47:47 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Mon Apr 26 10:44:45 1999 +0200 @@ -1,5 +1,6 @@ -(* Title: ioa_package.ML +(* Title: HOLCF/IOA/meta_theory/ioa_package.ML ID: $Id$ + Author: Tobias Hamberger, TU Muenchen *) signature IOA_PACKAGE = @@ -24,16 +25,13 @@ val add_rename_i : string -> string -> string -> theory -> theory end; -structure IoaPackage(* FIXME : IOA_PACKAGE *) = +structure IoaPackage: 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 | @@ -339,7 +337,7 @@ (* 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 ^ "..."); +(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)) ; @@ -362,7 +360,7 @@ (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 *) +|> (PureThy.add_defs o map Thm.no_attributes) (* old: Attributes.none *) [(automaton_name ^ "_initial_def", automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), (automaton_name ^ "_asig_def", @@ -388,7 +386,7 @@ end) fun gen_add_composition prep_term automaton_name aut_list thy = -(writeln("Constructing automaton " ^ automaton_name ^ "..."); +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); let val acttyp = check_ac thy aut_list; val st_typ = comp_st_type_of thy aut_list; @@ -403,13 +401,13 @@ 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) +|> (PureThy.add_defs o map Thm.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 ^ "..."); +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); let val auttyp = aut_type_of thy aut_source; val acttyp = act_type_of thy auttyp; @@ -418,12 +416,12 @@ thy |> ContConsts.add_consts_i [(automaton_name, auttyp,NoSyn)] -|> (PureThy.add_defs o map no_attributes) +|> (PureThy.add_defs o map Thm.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 ^ "..."); +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); let val auttyp = aut_type_of thy aut_source; val acttyp = act_type_of thy auttyp; @@ -432,7 +430,7 @@ thy |> ContConsts.add_consts_i [(automaton_name, auttyp,NoSyn)] -|> (PureThy.add_defs o map no_attributes) +|> (PureThy.add_defs o map Thm.no_attributes) [(automaton_name ^ "_def", automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] end) @@ -449,7 +447,7 @@ end; fun gen_add_rename prep_term automaton_name aut_source fun_name thy = -(writeln("Constructing automaton " ^ automaton_name ^ "..."); +(writeln("Constructing automaton " ^ automaton_name ^ " ..."); let val auttyp = aut_type_of thy aut_source; val st_typ = st_type_of thy auttyp; @@ -464,7 +462,7 @@ 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) +|> (PureThy.add_defs o map Thm.no_attributes) [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] end) @@ -492,4 +490,87 @@ 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; + + +(* parsers *) + +local open OuterParse in + +val actionlist = list1 term; +val inputslist = $$$ "inputs" |-- actionlist; +val outputslist = $$$ "outputs" |-- actionlist; +val internalslist = $$$ "internals" |-- actionlist; +val stateslist = $$$ "states" |-- Scan.repeat1 (name --| $$$ "::" -- typ); +val initial = $$$ "initially" |-- term; +val assign_list = list1 (name --| $$$ ":=" -- term); +val pre = $$$ "pre" |-- term; +val post = $$$ "post" |-- 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 = ($$$ "transrel" |-- term) >> mk_trans_of_rel; +val transition = term -- (transrel || pre1 || post1); +val translist = $$$ "transitions" |-- Scan.repeat1 transition; + +val ioa_decl = + (name -- ($$$ "=" |-- + ($$$ "signature" |-- + ($$$ "actions" |-- + (typ -- + (Scan.optional inputslist []) -- + (Scan.optional outputslist []) -- + (Scan.optional internalslist []) -- + stateslist -- + (Scan.optional initial "True") -- + translist))))) >> mk_ioa_decl || + (name -- ($$$ "=" |-- ($$$ "compose" |-- list1 name))) >> mk_composition_decl || + (name -- ($$$ "=" |-- ($$$ "hide" |-- list1 term -- ($$$ "in" |-- name)))) >> mk_hiding_decl || + (name -- ($$$ "=" |-- ($$$ "restrict" |-- name -- ($$$ "to" |-- list1 term)))) + >> mk_restriction_decl || + (name -- ($$$ "=" |-- ($$$ "rename" |-- name -- ($$$ "with" |-- term)))) >> mk_rename_decl; + +val automatonP = OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" + (ioa_decl >> Toplevel.theory); + end; + + +(* setup outer syntax *) + +val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs", + "outputs", "internals", "states", "initially", "transitions", "pre", + "post", "transrel", ":=", "compose", "hide", "in", "restrict", "to", + "rename", "with"]; + +val _ = OuterSyntax.add_parsers [automatonP]; + + +end;