src/HOLCF/IOA/meta_theory/ioa_package.ML
changeset 22578 b0eb5652f210
parent 20194 c9dbce9a23a1
child 22675 acf10be7dcca
     1.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Apr 04 00:10:59 2007 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Apr 04 00:11:03 2007 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4  param_tupel thy ((TFree(a,_))::r) res = 
     1.5  if (a mem res) then (param_tupel thy r res) else (param_tupel thy r (a::res)) |
     1.6  param_tupel thy (a::r) res =
     1.7 -error ("one component of a statetype is a TVar: " ^ (string_of_typ (sign_of thy) a));
     1.8 +error ("one component of a statetype is a TVar: " ^ (string_of_typ thy a));
     1.9  *)
    1.10  
    1.11  (* used by constr_list *)
    1.12 @@ -80,7 +80,7 @@
    1.13  (* delivers constructor term string from a prem of *.induct *)
    1.14  fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    1.15  extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
    1.16 -extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term (sign_of thy) r) |
    1.17 +extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term thy r) |
    1.18  extract_constr _ _ = raise malformed;
    1.19  in
    1.20  (extract_hd a,extract_constr thy a) :: (extract_constrs thy r)
    1.21 @@ -91,7 +91,7 @@
    1.22  let
    1.23  fun act_name thy (Type(s,_)) = s |
    1.24  act_name _ s = 
    1.25 -error("malformed action type: " ^ (string_of_typ (sign_of thy) s));
    1.26 +error("malformed action type: " ^ (string_of_typ thy s));
    1.27  fun afpl ("." :: a) = [] |
    1.28  afpl [] = [] |
    1.29  afpl (a::r) = a :: (afpl r);
    1.30 @@ -132,7 +132,7 @@
    1.31  (* making a constructor set from a constructor term (of signature) *)
    1.32  fun constr_set_string thy atyp ctstr =
    1.33  let
    1.34 -val trm = #t(rep_cterm(read_cterm (sign_of thy) (ctstr,atyp)));
    1.35 +val trm = #t(rep_cterm(read_cterm thy (ctstr,atyp)));
    1.36  val l = free_vars_of trm
    1.37  in
    1.38  if (check_for_constr thy atyp trm) then
    1.39 @@ -140,7 +140,7 @@
    1.40  else "(UN " ^ (list_elements_of l) ^ ". {" ^ ctstr ^ "})")
    1.41  else (raise malformed) 
    1.42  handle malformed => 
    1.43 -error("malformed action term: " ^ (string_of_term (sign_of thy) trm))
    1.44 +error("malformed action term: " ^ (string_of_term thy trm))
    1.45  end;
    1.46  
    1.47  (* extracting constructor heads *)
    1.48 @@ -149,7 +149,7 @@
    1.49  fun hd_of (Const(a,_)) = a |
    1.50  hd_of (t $ _) = hd_of t |
    1.51  hd_of _ = raise malformed;
    1.52 -val trm = #t(rep_cterm(read_cterm (sign_of thy) (s,#T(rep_ctyp(read_ctyp (sign_of thy) atypstr))) ))
    1.53 +val trm = #t(rep_cterm(read_cterm thy (s,#T(rep_ctyp(read_ctyp thy atypstr))) ))
    1.54  in
    1.55  hd_of trm handle malformed =>
    1.56  error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
    1.57 @@ -177,8 +177,8 @@
    1.58  (where bool indicates whether there is a precondition *)
    1.59  fun extend thy atyp statetupel (actstr,r,[]) =
    1.60  let
    1.61 -val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp)));
    1.62 -val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[]))));
    1.63 +val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
    1.64 +val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
    1.65  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
    1.66  in
    1.67  if (check_for_constr thy atyp trm)
    1.68 @@ -191,8 +191,8 @@
    1.69  fun pseudo_poststring [] = "" |
    1.70  pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
    1.71  pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
    1.72 -val trm = #t(rep_cterm(read_cterm (sign_of thy) (actstr,atyp)));
    1.73 -val rtrm = #t(rep_cterm(read_cterm (sign_of thy) (r,Type("bool",[]))));
    1.74 +val trm = #t(rep_cterm(read_cterm thy (actstr,atyp)));
    1.75 +val rtrm = #t(rep_cterm(read_cterm thy (r,Type("bool",[]))));
    1.76  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
    1.77  in
    1.78  if (check_for_constr thy atyp trm) then
    1.79 @@ -237,7 +237,7 @@
    1.80  error("Action " ^ b ^ " is not in automaton signature")
    1.81  ))) else (write_alt thy (chead,ctrm) inp out int r)
    1.82  handle malformed =>
    1.83 -error ("malformed action term: " ^ (string_of_term (sign_of thy) a))
    1.84 +error ("malformed action term: " ^ (string_of_term thy a))
    1.85  end;
    1.86  
    1.87  (* used by make_alt_string *)
    1.88 @@ -286,16 +286,16 @@
    1.89  left_of _ = raise malformed;
    1.90  val aut_def = concl_of (get_thm thy (Name (aut_name ^ "_def")));
    1.91  in
    1.92 -(#T(rep_cterm(cterm_of (sign_of thy) (left_of aut_def))))
    1.93 +(#T(rep_cterm(cterm_of thy (left_of aut_def))))
    1.94  handle malformed => error ("malformed_theorem : " ^ aut_name ^ "_def")
    1.95  end;
    1.96  
    1.97  fun act_type_of thy (Type(pair1,(Type(pair_asig,(Type(actionset,[acttyp])::_))::_))) = acttyp |
    1.98  act_type_of thy t = error ("could not extract action type of following automaton type:\n" ^
    1.99 -(string_of_typ (sign_of thy) t));
   1.100 +(string_of_typ thy t));
   1.101  fun st_type_of thy (Type(pair1,_::(Type(pair2,Type(initial_set,[statetyp])::_))::_)) = statetyp |
   1.102  st_type_of thy t = error ("could not extract state type of following automaton type:\n" ^
   1.103 -(string_of_typ (sign_of thy) t));
   1.104 +(string_of_typ thy t));
   1.105  
   1.106  fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
   1.107  comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
   1.108 @@ -330,10 +330,10 @@
   1.109  (writeln("Constructing automaton " ^ automaton_name ^ " ...");
   1.110  let
   1.111  val state_type_string = type_product_of_varlist(statetupel);
   1.112 -val styp = #T(rep_ctyp (read_ctyp (sign_of thy) state_type_string)) ;
   1.113 +val styp = #T(rep_ctyp (read_ctyp thy state_type_string)) ;
   1.114  val state_vars_tupel = "(" ^ (comma_list_of_varlist statetupel) ^ ")";
   1.115  val state_vars_primed = "(" ^ (primed_comma_list_of_varlist statetupel) ^ ")";
   1.116 -val atyp = #T(rep_ctyp (read_ctyp (sign_of thy) action_type));
   1.117 +val atyp = #T(rep_ctyp (read_ctyp thy action_type));
   1.118  val inp_set_string = action_set_string thy atyp inp;
   1.119  val out_set_string = action_set_string thy atyp out;
   1.120  val int_set_string = action_set_string thy atyp int;
   1.121 @@ -364,7 +364,7 @@
   1.122  automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
   1.123  "_initial, " ^ automaton_name ^ "_trans,{},{})")
   1.124  ])
   1.125 -val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm (sign_of thy2)
   1.126 +val chk_prime_list = (check_free_primed (#t(rep_cterm(read_cterm thy2
   1.127  ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string),Type("bool",[]))))));
   1.128  in
   1.129  (