wneuper/isa: comparison src/Tools/isac/ProgLang/termC.sml

equal deleted inserted replaced

-:95d956108461
+:460c24a6a6ba
 ("\n*** "^indent n^"TVar (("^s^","^
 string_of_int i ^ strs2str' sort)
 and atol n [] =
 ("\n*** "^indent n^"]")
 | atol n (T::Ts) = (ato n T ^ atol n Ts)
-(*in print (ato 0 t ^ "\n") end;  TODO TUM10*)
+in writeln (ato 0 t ^ "\n") end;
-in tracing (ato 0 t) end;
 (*
 > val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
 > atomtyp T;
 *** Type (fun,[
 ***   Type (RealDef.real,[])
 	  | ato (Bound i) n =
 	           "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
 	  | ato (Abs (a, _, body)) n =
 	           "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
 	  | ato (f $ t) n = (ato f n ^ ato t (n + 1))
-in tracing ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
+in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
 fun term_detail2str t =
 let fun ato (Const (a, T)) n =
 	    "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")"
 	  | ato (Free (a, T)) n =
 	  | ato (Abs(a, T, body))  n =
 	    "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.."
 	    ^ ato body (n + 1)
 	  | ato (f $ t) n = ato f n ^ ato t (n + 1)
 in "\n*** " ^ ato t 0 ^ "\n***" end;
-fun atomty t = (tracing o term_detail2str) t; (*WN100907 broken*)
+fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*)
 fun term_str thy (Const(s,_)) = s
 | term_str thy (Free(s,_)) = s
 | term_str thy (Var((s,i),_)) = s^(string_of_int i)
 | term_str thy (Bound i) = "B."^(string_of_int i)
 | term_str thy (Abs(s,_,_)) = s
-| term_str thy t = raise error("term_str not for "^term2str t);
+| term_str thy t = error("term_str not for "^term2str t);
 (*.contains the fst argument the second argument (a leave! of term).*)
 fun contains_term (Abs(_,_,body)) t = contains_term body t
 | contains_term (f $ f') t =
 contains_term f t orelse contains_term f' t
 *)
 (*fun int_of_Free (Free (intstr, _)) =
 (case BasisLibrary.Int.fromString intstr of
 	     SOME i => i
-	   | NONE => raise error ("int_of_Free ( "^ intstr ^", _)"))
+	   | NONE => error ("int_of_Free ( "^ intstr ^", _)"))
-| int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");*)
+| int_of_Free t = error ("int_of_Free ( "^ term2str t ^" )");*)
 fun int_of_Free (Free (intstr, _)) = (Thy_Output.integer intstr
-handle _ => raise error ("int_of_Free ( "^ intstr ^", _)"))
+handle _ => error ("int_of_Free ( "^ intstr ^", _)"))
-| int_of_Free t = raise error ("int_of_Free ( "^ term2str t ^" )");
+| int_of_Free t = error ("int_of_Free ( "^ term2str t ^" )");
 fun vars t =
 let
 fun scan vs (Const(s,T)) = vs
 | scan vs (t as Free(s,T)) = if is_no s then vs else t::vs
 | _ => false;
 fun is_bdv_ (Free (s,_)) = is_bdv s
 | is_bdv_ _ = false;
 fun free2str (Free (s,_)) = s
-| free2str t = raise error ("free2str not for "^ term2str t);
+| free2str t = error ("free2str not for "^ term2str t);
 fun free2int (t as Free (s, _)) = ((str2int s)
-handle _ => raise error ("free2int: "^term_detail2str t))
+handle _ => error ("free2int: "^term_detail2str t))
-| free2int t = raise error ("free2int: "^term_detail2str t);
+| free2int t = error ("free2int: "^term_detail2str t);
 (*27.8.01: unused*)
 fun var2free (t as Const(s,T)) = t
 | var2free (t as Free(s,T)) = t
 | var2free (Var((s,i),T)) = Free(s,T)
 > (cterm_of thy) ss;
 val it = "[R = R, R = R, R = R]" : cterm  *)
 fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
 | isapair2pair t =
-raise error ("isapair2pair called with "^term2str t);
+error ("isapair2pair called with "^term2str t);
 val listType = Type ("List.list",[Type ("bool",[])]);
 fun isalist2list ls =
 let
 fun get es (Const("List.list.Cons",_) $ t $ ls) = get (t::es) ls
 | get es (Const("List.list.Nil",_)) = es
 | get _ t =
-	raise error ("isalist2list applied to NON-list '"^term2str t^"'")
+	error ("isalist2list applied to NON-list '"^term2str t^"'")
 in (rev o (get [])) ls end;
 (*
 > val il = str2term "[a=b,c=d,e=f]";
 > val l = isalist2list il;
 > (tracing o terms2str) l;
 fun power b 0 = 1
 | power b n =
 if n>0 then b*(power b (n-1))
-else raise error ("power "^(str_of_int b)^" "^(str_of_int n));
+else error ("power "^(str_of_int b)^" "^(str_of_int n));
 (*
 > power 2 3;
 val it = 8 : int
 > power ~2 3;
 val it = ~8 : int
 fun dest_type (Type(T,[])) = T
 | dest_type T =
 (atomtyp T;
-raise error ("... dest_type: not impl. for this type"));
+error ("... dest_type: not impl. for this type"));
 fun term_of_num ntyp n = Free (str_of_int n, ntyp);
 fun pairT T1 T2 = Type ("*", [T1, T2]);
 (*> val t = str2term "(1,2)";
 fun num_of_term (t as Free (s,_)) =
 (case int_of_str s of
 	 SOME s' => s'
-| NONE => raise error ("num_of_term not for "^ term2str t))
+| NONE => error ("num_of_term not for "^ term2str t))
-| num_of_term t = raise error ("num_of_term not for "^term2str t);
+| num_of_term t = error ("num_of_term not for "^term2str t);
 fun mk_factroot op_(*=thy.sqrt*) T fact root =
 Const ("op *", [T, T] ---> T) $ (term_of_num T fact) $
 (Const (op_, T --> T) $ term_of_num T root);
 (*
 (*fun calc "Groups.plus_class.plus"  (n1, n2) = n1+n2
 | calc "Groups.minus_class.minus"  (n1, n2) = n1-n2
 | calc "op *"  (n1, n2) = n1*n2
 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
 | calc "Atools.pow"(n1, n2) = power n1 n2
-| calc op_ _ = raise error ("calc: operator = "^op_^" not defined");-----*)
+| calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
 fun calc_equ "op <"  (n1, n2) = n1 < n2
 | calc_equ "op <=" (n1, n2) = n1 <= n2
 | calc_equ op_ _ =
-raise error ("calc_equ: operator = "^op_^" not defined");
+error ("calc_equ: operator = "^op_^" not defined");
 fun sqrt (n:int) = if n < 0 then 0
 (*FIXME ~~~*)  else (trunc o Math.sqrt o Real.fromInt) n;
 fun mk_thmid thmid op_ n1 n2 =
 thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
 fun dest_binop_typ (Type("fun",[range,Type("fun",[arg2,arg1])])) =
 (arg1,arg2,range)
-| dest_binop_typ _ = raise error "dest_binop_typ: not binary";
+| dest_binop_typ _ = error "dest_binop_typ: not binary";
 (* -----
 > val t = (term_of o the o (parse thy)) "#3^#4";
 > val hT = type_of (head_of t);
 > dest_binop_typ hT;
 val it = ("'a","nat","'a") : typ * typ * typ

branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38025	67a110289e4e
child 38034	928cebc9c4aa