src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 12339 f0b62ad4e1a6
parent 10203 746eb6791aed
child 12928 6ffd206f93ee
     1.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Dec 01 18:52:32 2001 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat Dec 01 18:55:41 2001 +0100
     1.3 @@ -5,31 +5,20 @@
     1.4  
     1.5  signature IOA_PACKAGE =
     1.6  sig
     1.7 -  val add_ioa: string -> string ->
     1.8 + val add_ioa: string -> string ->
     1.9  		 (string) list -> (string) list -> (string) list ->
    1.10  		(string * string) list -> string ->
    1.11  		(string * string * (string * string)list) list
    1.12  	-> theory -> theory
    1.13 - val add_ioa_i : string -> string ->
    1.14 -                 (string) list -> (string) list -> (string) list ->
    1.15 -                (string * string) list -> string ->
    1.16 -                (string * string * (string * string)list) list
    1.17 -	-> theory -> theory
    1.18   val add_composition : string -> (string)list -> theory -> theory
    1.19 - val add_composition_i : string -> (string)list -> theory -> theory
    1.20   val add_hiding : string -> string -> (string)list -> theory -> theory
    1.21 - val add_hiding_i : string -> string -> (string)list -> theory -> theory
    1.22   val add_restriction : string -> string -> (string)list -> theory -> theory
    1.23 - val add_restriction_i : string -> string -> (string)list -> theory -> theory
    1.24   val add_rename : string -> string -> string -> theory -> theory
    1.25 - val add_rename_i : string -> string -> string -> theory -> theory
    1.26  end;
    1.27  
    1.28  structure IoaPackage: IOA_PACKAGE =
    1.29  struct
    1.30  
    1.31 -local
    1.32 -
    1.33  exception malformed;
    1.34  
    1.35  (* stripping quotes *)
    1.36 @@ -274,7 +263,7 @@
    1.37  write_alts thy ("","") inp out int cl ttr
    1.38  end;
    1.39  
    1.40 -(* used in gen_add_ioa *)
    1.41 +(* used in add_ioa *)
    1.42  fun check_free_primed (Free(a,_)) = 
    1.43  let
    1.44  val (f::r) = rev(explode a)
    1.45 @@ -334,9 +323,10 @@
    1.46  clist [a] = a |
    1.47  clist (a::r) = a ^ " || " ^ (clist r);
    1.48  
    1.49 -(* gen_add_ioa *)
    1.50  
    1.51 -fun gen_add_ioa prep_term automaton_name action_type inp out int statetupel ini trans thy =
    1.52 +(* add_ioa *)
    1.53 +
    1.54 +fun add_ioa automaton_name action_type inp out int statetupel ini trans thy =
    1.55  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
    1.56  let
    1.57  val state_type_string = type_product_of_varlist(statetupel);
    1.58 @@ -385,7 +375,7 @@
    1.59  )
    1.60  end)
    1.61  
    1.62 -fun gen_add_composition prep_term automaton_name aut_list thy =
    1.63 +fun add_composition automaton_name aut_list thy =
    1.64  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
    1.65  let
    1.66  val acttyp = check_ac thy aut_list; 
    1.67 @@ -406,7 +396,7 @@
    1.68  automaton_name ^ " == " ^ comp_list)]
    1.69  end)
    1.70  
    1.71 -fun gen_add_restriction prep_term automaton_name aut_source actlist thy =
    1.72 +fun add_restriction automaton_name aut_source actlist thy =
    1.73  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
    1.74  let
    1.75  val auttyp = aut_type_of thy aut_source;
    1.76 @@ -420,7 +410,7 @@
    1.77  [(automaton_name ^ "_def",
    1.78  automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
    1.79  end)
    1.80 -fun gen_add_hiding prep_term automaton_name aut_source actlist thy =
    1.81 +fun add_hiding automaton_name aut_source actlist thy =
    1.82  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
    1.83  let
    1.84  val auttyp = aut_type_of thy aut_source;
    1.85 @@ -446,7 +436,7 @@
    1.86  handle malformed => error ("could not extract argument type of renaming function term")
    1.87  end;
    1.88   
    1.89 -fun gen_add_rename prep_term automaton_name aut_source fun_name thy =
    1.90 +fun add_rename automaton_name aut_source fun_name thy =
    1.91  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
    1.92  let
    1.93  val auttyp = aut_type_of thy aut_source;
    1.94 @@ -467,30 +457,6 @@
    1.95  automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
    1.96  end)
    1.97  
    1.98 -(* external interfaces *)
    1.99 -
   1.100 -fun read_term sg str =
   1.101 -  read_cterm sg (str, HOLogic.termT);
   1.102 -
   1.103 -fun cert_term sg tm =
   1.104 -  cterm_of sg tm handle TERM (msg, _) => error msg;
   1.105 -
   1.106 -in
   1.107 -
   1.108 -val add_ioa = gen_add_ioa read_term;
   1.109 -val add_ioa_i = gen_add_ioa cert_term;
   1.110 -val add_composition = gen_add_composition read_term;
   1.111 -val add_composition_i = gen_add_composition cert_term;
   1.112 -val add_hiding = gen_add_hiding read_term;
   1.113 -val add_hiding_i = gen_add_hiding cert_term;
   1.114 -val add_restriction = gen_add_restriction read_term;
   1.115 -val add_restriction_i = gen_add_restriction cert_term;
   1.116 -val add_rename = gen_add_rename read_term;
   1.117 -val add_rename_i = gen_add_rename cert_term;
   1.118 -
   1.119 -end
   1.120 -
   1.121 -
   1.122  
   1.123  (** outer syntax **)
   1.124