22 val add_restriction_i : string -> string -> (string)list -> theory -> theory |
23 val add_restriction_i : string -> string -> (string)list -> theory -> theory |
23 val add_rename : string -> string -> string -> theory -> theory |
24 val add_rename : string -> string -> string -> theory -> theory |
24 val add_rename_i : string -> string -> string -> theory -> theory |
25 val add_rename_i : string -> string -> string -> theory -> theory |
25 end; |
26 end; |
26 |
27 |
27 structure IoaPackage(* FIXME : IOA_PACKAGE *) = |
28 structure IoaPackage: IOA_PACKAGE = |
28 struct |
29 struct |
29 |
30 |
30 local |
31 local |
31 |
32 |
32 exception malformed; |
33 exception malformed; |
33 |
|
34 (* for usage of hidden function no_attributes of structure Thm : *) |
|
35 fun no_attributes x = (x, []); |
|
36 |
34 |
37 (* stripping quotes *) |
35 (* stripping quotes *) |
38 fun strip [] = [] | |
36 fun strip [] = [] | |
39 strip ("\""::r) = strip r | |
37 strip ("\""::r) = strip r | |
40 strip (a::r) = a :: (strip r); |
38 strip (a::r) = a :: (strip r); |
360 [(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn), |
358 [(automaton_name ^ "_initial", "(" ^ state_type_string ^ ")set" ,NoSyn), |
361 (automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn), |
359 (automaton_name ^ "_asig", "(" ^ action_type ^ ")signature" ,NoSyn), |
362 (automaton_name ^ "_trans", |
360 (automaton_name ^ "_trans", |
363 "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), |
361 "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), |
364 (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] |
362 (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] |
365 |> (PureThy.add_defs o map no_attributes) (* old: Attributes.none *) |
363 |> (PureThy.add_defs o map Thm.no_attributes) (* old: Attributes.none *) |
366 [(automaton_name ^ "_initial_def", |
364 [(automaton_name ^ "_initial_def", |
367 automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), |
365 automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), |
368 (automaton_name ^ "_asig_def", |
366 (automaton_name ^ "_asig_def", |
369 automaton_name ^ "_asig == (" ^ |
367 automaton_name ^ "_asig == (" ^ |
370 inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), |
368 inp_set_string ^ "," ^ out_set_string ^ "," ^ int_set_string ^ ")"), |
401 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), |
399 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), |
402 Type("*",[Type("set",[st_typ]), |
400 Type("*",[Type("set",[st_typ]), |
403 Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), |
401 Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), |
404 Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) |
402 Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) |
405 ,NoSyn)] |
403 ,NoSyn)] |
406 |> (PureThy.add_defs o map no_attributes) |
404 |> (PureThy.add_defs o map Thm.no_attributes) |
407 [(automaton_name ^ "_def", |
405 [(automaton_name ^ "_def", |
408 automaton_name ^ " == " ^ comp_list)] |
406 automaton_name ^ " == " ^ comp_list)] |
409 end) |
407 end) |
410 |
408 |
411 fun gen_add_restriction prep_term automaton_name aut_source actlist thy = |
409 fun gen_add_restriction prep_term automaton_name aut_source actlist thy = |
412 (writeln("Constructing automaton " ^ automaton_name ^ "..."); |
410 (writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
413 let |
411 let |
414 val auttyp = aut_type_of thy aut_source; |
412 val auttyp = aut_type_of thy aut_source; |
415 val acttyp = act_type_of thy auttyp; |
413 val acttyp = act_type_of thy auttyp; |
416 val rest_set = action_set_string thy acttyp actlist |
414 val rest_set = action_set_string thy acttyp actlist |
417 in |
415 in |
418 thy |
416 thy |
419 |> ContConsts.add_consts_i |
417 |> ContConsts.add_consts_i |
420 [(automaton_name, auttyp,NoSyn)] |
418 [(automaton_name, auttyp,NoSyn)] |
421 |> (PureThy.add_defs o map no_attributes) |
419 |> (PureThy.add_defs o map Thm.no_attributes) |
422 [(automaton_name ^ "_def", |
420 [(automaton_name ^ "_def", |
423 automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] |
421 automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] |
424 end) |
422 end) |
425 fun gen_add_hiding prep_term automaton_name aut_source actlist thy = |
423 fun gen_add_hiding prep_term automaton_name aut_source actlist thy = |
426 (writeln("Constructing automaton " ^ automaton_name ^ "..."); |
424 (writeln("Constructing automaton " ^ automaton_name ^ " ..."); |
427 let |
425 let |
428 val auttyp = aut_type_of thy aut_source; |
426 val auttyp = aut_type_of thy aut_source; |
429 val acttyp = act_type_of thy auttyp; |
427 val acttyp = act_type_of thy auttyp; |
430 val hid_set = action_set_string thy acttyp actlist |
428 val hid_set = action_set_string thy acttyp actlist |
431 in |
429 in |
432 thy |
430 thy |
433 |> ContConsts.add_consts_i |
431 |> ContConsts.add_consts_i |
434 [(automaton_name, auttyp,NoSyn)] |
432 [(automaton_name, auttyp,NoSyn)] |
435 |> (PureThy.add_defs o map no_attributes) |
433 |> (PureThy.add_defs o map Thm.no_attributes) |
436 [(automaton_name ^ "_def", |
434 [(automaton_name ^ "_def", |
437 automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] |
435 automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] |
438 end) |
436 end) |
439 |
437 |
440 fun ren_act_type_of thy funct = |
438 fun ren_act_type_of thy funct = |
462 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), |
460 [Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]), |
463 Type("*",[Type("set",[st_typ]), |
461 Type("*",[Type("set",[st_typ]), |
464 Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), |
462 Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), |
465 Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) |
463 Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) |
466 ,NoSyn)] |
464 ,NoSyn)] |
467 |> (PureThy.add_defs o map no_attributes) |
465 |> (PureThy.add_defs o map Thm.no_attributes) |
468 [(automaton_name ^ "_def", |
466 [(automaton_name ^ "_def", |
469 automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] |
467 automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] |
470 end) |
468 end) |
471 |
469 |
472 (* external interfaces *) |
470 (* external interfaces *) |
490 val add_rename = gen_add_rename read_term; |
488 val add_rename = gen_add_rename read_term; |
491 val add_rename_i = gen_add_rename cert_term; |
489 val add_rename_i = gen_add_rename cert_term; |
492 |
490 |
493 end |
491 end |
494 |
492 |
495 end; |
493 |
|
494 |
|
495 (** outer syntax **) |
|
496 |
|
497 (* prepare results *) |
|
498 |
|
499 (*encoding transition specifications with a element of ParseTrans*) |
|
500 datatype ParseTrans = Rel of string | PP of string*(string*string)list; |
|
501 fun mk_trans_of_rel s = Rel(s); |
|
502 fun mk_trans_of_prepost (s,l) = PP(s,l); |
|
503 |
|
504 fun trans_of (a, Rel b) = (a, b, [("", "")]) |
|
505 | trans_of (a, PP (b, l)) = (a, b, l); |
|
506 |
|
507 |
|
508 fun mk_ioa_decl (aut, ((((((action_type, inp), out), int), states), initial), trans)) = |
|
509 add_ioa aut action_type inp out int states initial (map trans_of trans); |
|
510 |
|
511 fun mk_composition_decl (aut, autlist) = |
|
512 add_composition aut autlist; |
|
513 |
|
514 fun mk_hiding_decl (aut, (actlist, source_aut)) = |
|
515 add_hiding aut source_aut actlist; |
|
516 |
|
517 fun mk_restriction_decl (aut, (source_aut, actlist)) = |
|
518 add_restriction aut source_aut actlist; |
|
519 |
|
520 fun mk_rename_decl (aut, (source_aut, rename_f)) = |
|
521 add_rename aut source_aut rename_f; |
|
522 |
|
523 |
|
524 (* parsers *) |
|
525 |
|
526 local open OuterParse in |
|
527 |
|
528 val actionlist = list1 term; |
|
529 val inputslist = $$$ "inputs" |-- actionlist; |
|
530 val outputslist = $$$ "outputs" |-- actionlist; |
|
531 val internalslist = $$$ "internals" |-- actionlist; |
|
532 val stateslist = $$$ "states" |-- Scan.repeat1 (name --| $$$ "::" -- typ); |
|
533 val initial = $$$ "initially" |-- term; |
|
534 val assign_list = list1 (name --| $$$ ":=" -- term); |
|
535 val pre = $$$ "pre" |-- term; |
|
536 val post = $$$ "post" |-- assign_list; |
|
537 val pre1 = (pre -- (Scan.optional post [])) >> mk_trans_of_prepost; |
|
538 val post1 = ((Scan.optional pre "True") -- post) >> mk_trans_of_prepost; |
|
539 val transrel = ($$$ "transrel" |-- term) >> mk_trans_of_rel; |
|
540 val transition = term -- (transrel || pre1 || post1); |
|
541 val translist = $$$ "transitions" |-- Scan.repeat1 transition; |
|
542 |
|
543 val ioa_decl = |
|
544 (name -- ($$$ "=" |-- |
|
545 ($$$ "signature" |-- |
|
546 ($$$ "actions" |-- |
|
547 (typ -- |
|
548 (Scan.optional inputslist []) -- |
|
549 (Scan.optional outputslist []) -- |
|
550 (Scan.optional internalslist []) -- |
|
551 stateslist -- |
|
552 (Scan.optional initial "True") -- |
|
553 translist))))) >> mk_ioa_decl || |
|
554 (name -- ($$$ "=" |-- ($$$ "compose" |-- list1 name))) >> mk_composition_decl || |
|
555 (name -- ($$$ "=" |-- ($$$ "hide" |-- list1 term -- ($$$ "in" |-- name)))) >> mk_hiding_decl || |
|
556 (name -- ($$$ "=" |-- ($$$ "restrict" |-- name -- ($$$ "to" |-- list1 term)))) |
|
557 >> mk_restriction_decl || |
|
558 (name -- ($$$ "=" |-- ($$$ "rename" |-- name -- ($$$ "with" |-- term)))) >> mk_rename_decl; |
|
559 |
|
560 val automatonP = OuterSyntax.command "automaton" "define Lynch/Vaandrager-style I/O automaton" |
|
561 (ioa_decl >> Toplevel.theory); |
|
562 |
|
563 end; |
|
564 |
|
565 |
|
566 (* setup outer syntax *) |
|
567 |
|
568 val _ = OuterSyntax.add_keywords ["signature", "actions", "inputs", |
|
569 "outputs", "internals", "states", "initially", "transitions", "pre", |
|
570 "post", "transrel", ":=", "compose", "hide", "in", "restrict", "to", |
|
571 "rename", "with"]; |
|
572 |
|
573 val _ = OuterSyntax.add_parsers [automatonP]; |
|
574 |
|
575 |
|
576 end; |