1.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/src/Tools/isac/ProgLang/termC.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -34,8 +34,7 @@
1.4 and atol n [] =
1.5 ("\n*** "^indent n^"]")
1.6 | atol n (T::Ts) = (ato n T ^ atol n Ts)
1.7 -(*in print (ato 0 t ^ "\n") end; TODO TUM10*)
1.8 -in tracing (ato 0 t) end;
1.9 +in writeln (ato 0 t ^ "\n") end;
1.10 (*
1.11 > val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
1.12 > atomtyp T;
1.13 @@ -86,7 +85,7 @@
1.14 | ato (Abs (a, _, body)) n =
1.15 "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
1.16 | ato (f $ t) n = (ato f n ^ ato t (n + 1))
1.17 - in tracing ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
1.18 + in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
1.19
1.20 fun term_detail2str t =
1.21 let fun ato (Const (a, T)) n =
1.22 @@ -103,14 +102,14 @@
1.23 ^ ato body (n + 1)
1.24 | ato (f $ t) n = ato f n ^ ato t (n + 1)
1.25 in "\n*** " ^ ato t 0 ^ "\n***" end;
1.26 -fun atomty t = (tracing o term_detail2str) t; (*WN100907 broken*)
1.27 +fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*)
1.28
1.29 fun term_str thy (Const(s,_)) = s
1.30 | term_str thy (Free(s,_)) = s
1.31 | term_str thy (Var((s,i),_)) = s^(string_of_int i)
1.32 | term_str thy (Bound i) = "B."^(string_of_int i)
1.33 | term_str thy (Abs(s,_,_)) = s
1.34 - | term_str thy t = raise error("term_str not for "^term2str t);
1.35 + | term_str thy t = error("term_str not for "^term2str t);
1.36
1.37 (*.contains the fst argument the second argument (a leave! of term).*)
1.38 fun contains_term (Abs(_,_,body)) t = contains_term body t
1.39 @@ -172,11 +171,11 @@
1.40 (*fun int_of_Free (Free (intstr, _)) =
1.41 (case BasisLibrary.Int.fromString intstr of
1.42 SOME i => i
1.43 - | NONE => raise error ("int_of_Free ( "^ intstr ^", _)"))
1.44 - | int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");*)
1.45 + | NONE => error ("int_of_Free ( "^ intstr ^", _)"))
1.46 + | int_of_Free t = error ("int_of_Free ( "^ term2str t ^" )");*)
1.47 fun int_of_Free (Free (intstr, _)) = (Thy_Output.integer intstr
1.48 - handle _ => raise error ("int_of_Free ( "^ intstr ^", _)"))
1.49 - | int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");
1.50 + handle _ => error ("int_of_Free ( "^ intstr ^", _)"))
1.51 + | int_of_Free t = error ("int_of_Free ( "^ term2str t ^" )");
1.52
1.53 fun vars t =
1.54 let
1.55 @@ -225,10 +224,10 @@
1.56 | is_bdv_ _ = false;
1.57
1.58 fun free2str (Free (s,_)) = s
1.59 - | free2str t = raise error ("free2str not for "^ term2str t);
1.60 + | free2str t = error ("free2str not for "^ term2str t);
1.61 fun free2int (t as Free (s, _)) = ((str2int s)
1.62 - handle _ => raise error ("free2int: "^term_detail2str t))
1.63 - | free2int t = raise error ("free2int: "^term_detail2str t);
1.64 + handle _ => error ("free2int: "^term_detail2str t))
1.65 + | free2int t = error ("free2int: "^term_detail2str t);
1.66
1.67 (*27.8.01: unused*)
1.68 fun var2free (t as Const(s,T)) = t
1.69 @@ -263,7 +262,7 @@
1.70
1.71 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
1.72 | isapair2pair t =
1.73 - raise error ("isapair2pair called with "^term2str t);
1.74 + error ("isapair2pair called with "^term2str t);
1.75
1.76 val listType = Type ("List.list",[Type ("bool",[])]);
1.77 fun isalist2list ls =
1.78 @@ -271,7 +270,7 @@
1.79 fun get es (Const("List.list.Cons",_) $ t $ ls) = get (t::es) ls
1.80 | get es (Const("List.list.Nil",_)) = es
1.81 | get _ t =
1.82 - raise error ("isalist2list applied to NON-list '"^term2str t^"'")
1.83 + error ("isalist2list applied to NON-list '"^term2str t^"'")
1.84 in (rev o (get [])) ls end;
1.85 (*
1.86 > val il = str2term "[a=b,c=d,e=f]";
1.87 @@ -477,7 +476,7 @@
1.88 fun power b 0 = 1
1.89 | power b n =
1.90 if n>0 then b*(power b (n-1))
1.91 - else raise error ("power "^(str_of_int b)^" "^(str_of_int n));
1.92 + else error ("power "^(str_of_int b)^" "^(str_of_int n));
1.93 (*
1.94 > power 2 3;
1.95 val it = 8 : int
1.96 @@ -536,7 +535,7 @@
1.97 fun dest_type (Type(T,[])) = T
1.98 | dest_type T =
1.99 (atomtyp T;
1.100 - raise error ("... dest_type: not impl. for this type"));
1.101 + error ("... dest_type: not impl. for this type"));
1.102
1.103 fun term_of_num ntyp n = Free (str_of_int n, ntyp);
1.104
1.105 @@ -562,8 +561,8 @@
1.106 fun num_of_term (t as Free (s,_)) =
1.107 (case int_of_str s of
1.108 SOME s' => s'
1.109 - | NONE => raise error ("num_of_term not for "^ term2str t))
1.110 - | num_of_term t = raise error ("num_of_term not for "^term2str t);
1.111 + | NONE => error ("num_of_term not for "^ term2str t))
1.112 + | num_of_term t = error ("num_of_term not for "^term2str t);
1.113
1.114 fun mk_factroot op_(*=thy.sqrt*) T fact root =
1.115 Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
1.116 @@ -612,11 +611,11 @@
1.117 | calc "op *" (n1, n2) = n1*n2
1.118 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
1.119 | calc "Atools.pow"(n1, n2) = power n1 n2
1.120 - | calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
1.121 + | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
1.122 fun calc_equ "op <" (n1, n2) = n1 < n2
1.123 | calc_equ "op <=" (n1, n2) = n1 <= n2
1.124 | calc_equ op_ _ =
1.125 - raise error ("calc_equ: operator = "^op_^" not defined");
1.126 + error ("calc_equ: operator = "^op_^" not defined");
1.127 fun sqrt (n:int) = if n < 0 then 0
1.128 (*FIXME ~~~*) else (trunc o Math.sqrt o Real.fromInt) n;
1.129
1.130 @@ -625,7 +624,7 @@
1.131
1.132 fun dest_binop_typ (Type("fun",[range,Type("fun",[arg2,arg1])])) =
1.133 (arg1,arg2,range)
1.134 - | dest_binop_typ _ = raise error "dest_binop_typ: not binary";
1.135 + | dest_binop_typ _ = error "dest_binop_typ: not binary";
1.136 (* -----
1.137 > val t = (term_of o the o (parse thy)) "#3^#4";
1.138 > val hT = type_of (head_of t);