35 string_of_int i ^ strs2str' sort) |
35 string_of_int i ^ strs2str' sort) |
36 and atol n [] = |
36 and atol n [] = |
37 ("\n*** "^indent n^"]") |
37 ("\n*** "^indent n^"]") |
38 | atol n (T::Ts) = (ato n T ^ atol n Ts) |
38 | atol n (T::Ts) = (ato n T ^ atol n Ts) |
39 (*in print (ato 0 t ^ "\n") end; TODO TUM10*) |
39 (*in print (ato 0 t ^ "\n") end; TODO TUM10*) |
40 in writeln(ato 0 t) end; |
40 in writeln (ato 0 t) end; |
41 |
41 (* |
42 (*Prog.Tutorial.p.34*) |
42 > val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat"; |
|
43 > atomtyp T; |
|
44 *** Type (fun,[ |
|
45 *** Type (RealDef.real,[]) |
|
46 *** Type (fun,[ |
|
47 *** Type (IntDef.int,[]) |
|
48 *** Type (nat,[]) |
|
49 *** ] |
|
50 *** ] |
|
51 *) |
|
52 |
|
53 (*Prog.Tutorial.p.34, Makarius 1005 does the above like this..*) |
43 local |
54 local |
44 fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] |
55 fun pp_pair (x, y) = Pretty.list "(" ")" [x, y] |
45 fun pp_list xs = Pretty.list "[" "]" xs |
56 fun pp_list xs = Pretty.list "[" "]" xs |
46 fun pp_str s = Pretty.str s |
57 fun pp_str s = Pretty.str s |
47 fun pp_qstr s = Pretty.quote (pp_str s) |
58 fun pp_qstr s = Pretty.quote (pp_str s) |
62 de-install |
73 de-install |
63 PolyML.addPrettyPrinter |
74 PolyML.addPrettyPrinter |
64 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); |
75 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy); |
65 *) |
76 *) |
66 |
77 |
67 (* |
|
68 > val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat"; |
|
69 > atomtyp T; |
|
70 *** Type (fun,[ |
|
71 *** Type (RealDef.real,[]) |
|
72 *** Type (fun,[ |
|
73 *** Type (IntDef.int,[]) |
|
74 *** Type (nat,[]) |
|
75 *** ] |
|
76 *** ] |
|
77 *) |
|
78 |
|
79 fun atomt t = |
78 fun atomt t = |
80 let fun ato (Const(a,T)) n = |
79 let fun ato (Const (a, _)) n = |
81 ("\n*** "^indent n^"Const ("^a^")") |
80 "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)" |
82 | ato (Free (a,T)) n = |
81 | ato (Free (a, _)) n = |
83 ("\n*** "^indent n^"Free ("^a^", "^")") |
82 "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)" |
84 | ato (Var ((a,ix),T)) n = |
83 | ato (Var ((a, i), _)) n = |
85 ("\n*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^")") |
84 "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^ |
86 | ato (Bound ix) n = |
85 string_of_int i ^ "), _)" |
87 ("\n*** "^indent n^"Bound "^(string_of_int ix)) |
86 | ato (Bound i) n = |
88 | ato (Abs(a,T,body)) n = |
87 "\n*** " ^ indent n ^ "Bound " ^ string_of_int i |
89 ("\n*** "^indent n^"Abs("^a^",..")^ato body (n+1) |
88 | ato (Abs (a, _, body)) n = |
90 | ato (f$t') n = (ato f n; ato t' (n+1)) |
89 "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1) |
91 in writeln("\n*** -------------"^ ato t 0 ^"\n***") end; |
90 | ato (f $ t) n = (ato f n ^ ato t (n + 1)) |
|
91 in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end; |
92 |
92 |
93 fun term_detail2str t = |
93 fun term_detail2str t = |
94 let fun ato (Const (a, T)) n = |
94 let fun ato (Const (a, T)) n = |
95 "\n*** "^indent n^"Const ("^a^", "^string_of_typ T^")" |
95 "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")" |
96 | ato (Free (a, T)) n = |
96 | ato (Free (a, T)) n = |
97 "\n*** "^indent n^"Free ("^a^", "^string_of_typ T^")" |
97 "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ T ^ ")" |
98 | ato (Var ((a, ix), T)) n = |
98 | ato (Var ((a, i), T)) n = |
99 "\n*** "^indent n^"Var (("^a^", "^string_of_int ix^"), "^ |
99 "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^ |
100 string_of_typ T^")" |
100 string_of_typ T ^ ")" |
101 | ato (Bound ix) n = |
101 | ato (Bound i) n = |
102 "\n*** "^indent n^"Bound "^string_of_int ix |
102 "\n*** " ^ indent n ^ "Bound " ^ string_of_int i |
103 | ato (Abs(a, T, body)) n = |
103 | ato (Abs(a, T, body)) n = |
104 "\n*** "^indent n^"Abs ("^a^", "^ |
104 "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.." |
105 (string_of_typ T)^",.." |
105 ^ ato body (n + 1) |
106 ^ato body (n + 1) |
106 | ato (f $ t) n = ato f n ^ ato t (n + 1) |
107 | ato (f $ t') n = ato f n^ato t' (n+1) |
107 in "\n*** " ^ ato t 0 ^ "\n***" end; |
108 in "\n*** "^ato t 0^"\n***" end; |
108 fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*) |
109 fun atomty t = (writeln o term_detail2str) t; |
|
110 |
109 |
111 fun term_str thy (Const(s,_)) = s |
110 fun term_str thy (Const(s,_)) = s |
112 | term_str thy (Free(s,_)) = s |
111 | term_str thy (Free(s,_)) = s |
113 | term_str thy (Var((s,i),_)) = s^(string_of_int i) |
112 | term_str thy (Var((s,i),_)) = s^(string_of_int i) |
114 | term_str thy (Bound i) = "B."^(string_of_int i) |
113 | term_str thy (Bound i) = "B."^(string_of_int i) |
800 |
799 |
801 |
800 |
802 fun mk_Free (s,T) = Free(s,T); |
801 fun mk_Free (s,T) = Free(s,T); |
803 fun mk_free T s = Free(s,T); |
802 fun mk_free T s = Free(s,T); |
804 |
803 |
|
804 (*Special case: one argument cp from Isabelle2002/src/Pure/term.ML*) |
|
805 fun subst_bound (arg, t) : term = (*WN100908 neglects 'raise Same.SAME'*) |
|
806 let fun subst (t as Bound i, lev) = |
|
807 if i<lev then t (*var is locally bound*) |
|
808 else if i=lev then incr_boundvars lev arg |
|
809 else Bound(i-1) (*loose: change it*) |
|
810 | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) |
|
811 | subst (f$t, lev) = subst(f,lev) $ subst(t,lev) |
|
812 | subst (t,lev) = t |
|
813 in subst (t,0) end; |
|
814 |
805 (*instantiate let; necessary for ass_up*) |
815 (*instantiate let; necessary for ass_up*) |
806 fun inst_abs thy (Const sT) = Const sT |
816 fun inst_abs thy (Const sT) = Const sT (*TODO.WN100907 drop thy*) |
807 | inst_abs thy (Free sT) = Free sT |
817 | inst_abs thy (Free sT) = Free sT |
808 | inst_abs thy (Bound n) = Bound n |
818 | inst_abs thy (Bound n) = Bound n |
809 | inst_abs thy (Var iT) = Var iT |
819 | inst_abs thy (Var iT) = Var iT |
810 | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) = |
820 | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v, T2, b))) = |
811 let val (v',b') = variant_abs (v,T2,b); (*fun variant_abs: term.ML*) |
821 let val b' = subst_bound (Free (v, T2), b); |
812 in Const ("Let",T1) $ inst_abs thy e $ (Abs (v',T2,inst_abs thy b')) end |
822 (*fun variant_abs: term.ML*) |
|
823 in Const ("Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end |
813 | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2 |
824 | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2 |
814 | inst_abs thy t = |
825 | inst_abs thy t = t; |
815 (writeln("inst_abs: unchanged t= "^ term2str t); |
|
816 t); |
|
817 (*val scr as (Script sc) = Script ((term_of o the o (parse thy)) |
|
818 "Script Testeq (e_::bool) = \ |
|
819 \While (contains_root e_) Do \ |
|
820 \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \ |
|
821 \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \ |
|
822 \ in Try (Repeat (Rewrite radd_0 False e_))) "); |
|
823 ML> atomt sc; |
|
824 *** Const ( Script.Testeq) |
|
825 *** . Free ( e_, ) |
|
826 *** . Const ( Script.While) |
|
827 *** . . Const ( RatArith.contains'_root) |
|
828 *** . . . Free ( e_, ) |
|
829 *** . . Const ( Let) |
|
830 *** . . . Const ( Script.Try) |
|
831 *** . . . . Const ( Script.Repeat) |
|
832 *** . . . . . Const ( Script.Rewrite) |
|
833 *** . . . . . . Free ( rroot_square_inv, ) |
|
834 *** . . . . . . Const ( False) |
|
835 *** . . . . . . Free ( e_, ) |
|
836 *** . . . Abs( e_,.. |
|
837 *** . . . . Const ( Let) |
|
838 *** . . . . . Const ( Script.Try) |
|
839 *** . . . . . . Const ( Script.Repeat) |
|
840 *** . . . . . . . Const ( Script.Rewrite) |
|
841 *** . . . . . . . . Free ( square_equation_left, ) |
|
842 *** . . . . . . . . Const ( True) |
|
843 *** . . . . . . . . Bound 0 <-- !!! |
|
844 *** . . . . . Abs( e_,.. |
|
845 *** . . . . . . Const ( Script.Try) |
|
846 *** . . . . . . . Const ( Script.Repeat) |
|
847 *** . . . . . . . . Const ( Script.Rewrite) |
|
848 *** . . . . . . . . . Free ( radd_0, ) |
|
849 *** . . . . . . . . . Const ( False) |
|
850 *** . . . . . . . . . Bound 0 <-- !!! |
|
851 val it = () : unit |
|
852 ML> atomt (inst_abs thy sc); |
|
853 *** Const ( Script.Testeq) |
|
854 *** . Free ( e_, ) |
|
855 *** . Const ( Script.While) |
|
856 *** . . Const ( RatArith.contains'_root) |
|
857 *** . . . Free ( e_, ) |
|
858 *** . . Const ( Let) |
|
859 *** . . . Const ( Script.Try) |
|
860 *** . . . . Const ( Script.Repeat) |
|
861 *** . . . . . Const ( Script.Rewrite) |
|
862 *** . . . . . . Free ( rroot_square_inv, ) |
|
863 *** . . . . . . Const ( False) |
|
864 *** . . . . . . Free ( e_, ) |
|
865 *** . . . Abs( e_,.. |
|
866 *** . . . . Const ( Let) |
|
867 *** . . . . . Const ( Script.Try) |
|
868 *** . . . . . . Const ( Script.Repeat) |
|
869 *** . . . . . . . Const ( Script.Rewrite) |
|
870 *** . . . . . . . . Free ( square_equation_left, ) |
|
871 *** . . . . . . . . Const ( True) |
|
872 *** . . . . . . . . Free ( e_, ) <-- !!! |
|
873 *** . . . . . Abs( e_,.. |
|
874 *** . . . . . . Const ( Script.Try) |
|
875 *** . . . . . . . Const ( Script.Repeat) |
|
876 *** . . . . . . . . Const ( Script.Rewrite) |
|
877 *** . . . . . . . . . Free ( radd_0, ) |
|
878 *** . . . . . . . . . Const ( False) |
|
879 *** . . . . . . . . . Free ( e_, ) <-- ZUFALL vor 5.03!!! |
|
880 val it = () : unit*) |
|
881 |
|
882 |
|
883 |
|
884 |
|
885 fun inst_abs thy (Const sT) = Const sT |
|
886 | inst_abs thy (Free sT) = Free sT |
|
887 | inst_abs thy (Bound n) = Bound n |
|
888 | inst_abs thy (Var iT) = Var iT |
|
889 | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) = |
|
890 let val b' = subst_bound (Free(v,T2),b); |
|
891 (*fun variant_abs: term.ML*) |
|
892 in Const ("Let",T1) $ inst_abs thy e $ (Abs (v,T2,inst_abs thy b')) end |
|
893 | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2 |
|
894 | inst_abs thy t = |
|
895 (writeln("inst_abs: unchanged t= "^ term2str t); |
|
896 t); |
|
897 (*val scr = |
826 (*val scr = |
898 "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \ |
827 "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \ |
899 \ (let h_ = (hd o (filterVar f_)) eqs_; \ |
828 \ (let h_ = (hd o (filterVar f_)) eqs_; \ |
900 \ e_1 = hd (dropWhile (ident h_) eqs_); \ |
829 \ e_1 = hd (dropWhile (ident h_) eqs_); \ |
901 \ vs_ = dropWhile (ident f_) (Vars h_); \ |
830 \ vs_ = dropWhile (ident f_) (Vars h_); \ |