1.1 --- a/src/Tools/isac/ProgLang/term.sml Mon Sep 06 17:07:28 2010 +0200
1.2 +++ b/src/Tools/isac/ProgLang/term.sml Wed Sep 08 10:15:51 2010 +0200
1.3 @@ -20,7 +20,7 @@
1.4 (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
1.5 handle _ => false
1.6
1.7 -fun atomtyp t = (*see raw_pp_typ*)
1.8 +fun atomtyp t = (*WN10 see raw_pp_typ*)
1.9 let
1.10 fun ato n (Type (s,[])) =
1.11 ("\n*** "^indent n^"Type ("^s^",[])")
1.12 @@ -37,9 +37,20 @@
1.13 ("\n*** "^indent n^"]")
1.14 | atol n (T::Ts) = (ato n T ^ atol n Ts)
1.15 (*in print (ato 0 t ^ "\n") end; TODO TUM10*)
1.16 -in writeln(ato 0 t) end;
1.17 +in writeln (ato 0 t) end;
1.18 +(*
1.19 +> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
1.20 +> atomtyp T;
1.21 +*** Type (fun,[
1.22 +*** Type (RealDef.real,[])
1.23 +*** Type (fun,[
1.24 +*** Type (IntDef.int,[])
1.25 +*** Type (nat,[])
1.26 +*** ]
1.27 +*** ]
1.28 +*)
1.29
1.30 -(*Prog.Tutorial.p.34*)
1.31 +(*Prog.Tutorial.p.34, Makarius 1005 does the above like this..*)
1.32 local
1.33 fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
1.34 fun pp_list xs = Pretty.list "[" "]" xs
1.35 @@ -64,49 +75,37 @@
1.36 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
1.37 *)
1.38
1.39 -(*
1.40 -> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
1.41 -> atomtyp T;
1.42 -*** Type (fun,[
1.43 -*** Type (RealDef.real,[])
1.44 -*** Type (fun,[
1.45 -*** Type (IntDef.int,[])
1.46 -*** Type (nat,[])
1.47 -*** ]
1.48 -*** ]
1.49 -*)
1.50 -
1.51 fun atomt t =
1.52 - let fun ato (Const(a,T)) n =
1.53 - ("\n*** "^indent n^"Const ("^a^")")
1.54 - | ato (Free (a,T)) n =
1.55 - ("\n*** "^indent n^"Free ("^a^", "^")")
1.56 - | ato (Var ((a,ix),T)) n =
1.57 - ("\n*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^")")
1.58 - | ato (Bound ix) n =
1.59 - ("\n*** "^indent n^"Bound "^(string_of_int ix))
1.60 - | ato (Abs(a,T,body)) n =
1.61 - ("\n*** "^indent n^"Abs("^a^",..")^ato body (n+1)
1.62 - | ato (f$t') n = (ato f n; ato t' (n+1))
1.63 - in writeln("\n*** -------------"^ ato t 0 ^"\n***") end;
1.64 + let fun ato (Const (a, _)) n =
1.65 + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)"
1.66 + | ato (Free (a, _)) n =
1.67 + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)"
1.68 + | ato (Var ((a, i), _)) n =
1.69 + "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^
1.70 + string_of_int i ^ "), _)"
1.71 + | ato (Bound i) n =
1.72 + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
1.73 + | ato (Abs (a, _, body)) n =
1.74 + "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
1.75 + | ato (f $ t) n = (ato f n ^ ato t (n + 1))
1.76 + in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
1.77
1.78 fun term_detail2str t =
1.79 - let fun ato (Const (a, T)) n =
1.80 - "\n*** "^indent n^"Const ("^a^", "^string_of_typ T^")"
1.81 - | ato (Free (a, T)) n =
1.82 - "\n*** "^indent n^"Free ("^a^", "^string_of_typ T^")"
1.83 - | ato (Var ((a, ix), T)) n =
1.84 - "\n*** "^indent n^"Var (("^a^", "^string_of_int ix^"), "^
1.85 - string_of_typ T^")"
1.86 - | ato (Bound ix) n =
1.87 - "\n*** "^indent n^"Bound "^string_of_int ix
1.88 + let fun ato (Const (a, T)) n =
1.89 + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")"
1.90 + | ato (Free (a, T)) n =
1.91 + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ T ^ ")"
1.92 + | ato (Var ((a, i), T)) n =
1.93 + "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^
1.94 + string_of_typ T ^ ")"
1.95 + | ato (Bound i) n =
1.96 + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
1.97 | ato (Abs(a, T, body)) n =
1.98 - "\n*** "^indent n^"Abs ("^a^", "^
1.99 - (string_of_typ T)^",.."
1.100 - ^ato body (n + 1)
1.101 - | ato (f $ t') n = ato f n^ato t' (n+1)
1.102 - in "\n*** "^ato t 0^"\n***" end;
1.103 -fun atomty t = (writeln o term_detail2str) t;
1.104 + "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.."
1.105 + ^ ato body (n + 1)
1.106 + | ato (f $ t) n = ato f n ^ ato t (n + 1)
1.107 + in "\n*** " ^ ato t 0 ^ "\n***" end;
1.108 +fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*)
1.109
1.110 fun term_str thy (Const(s,_)) = s
1.111 | term_str thy (Free(s,_)) = s
1.112 @@ -802,98 +801,28 @@
1.113 fun mk_Free (s,T) = Free(s,T);
1.114 fun mk_free T s = Free(s,T);
1.115
1.116 +(*Special case: one argument cp from Isabelle2002/src/Pure/term.ML*)
1.117 +fun subst_bound (arg, t) : term = (*WN100908 neglects 'raise Same.SAME'*)
1.118 + let fun subst (t as Bound i, lev) =
1.119 + if i<lev then t (*var is locally bound*)
1.120 + else if i=lev then incr_boundvars lev arg
1.121 + else Bound(i-1) (*loose: change it*)
1.122 + | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
1.123 + | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
1.124 + | subst (t,lev) = t
1.125 + in subst (t,0) end;
1.126 +
1.127 (*instantiate let; necessary for ass_up*)
1.128 -fun inst_abs thy (Const sT) = Const sT
1.129 +fun inst_abs thy (Const sT) = Const sT (*TODO.WN100907 drop thy*)
1.130 | inst_abs thy (Free sT) = Free sT
1.131 | inst_abs thy (Bound n) = Bound n
1.132 | inst_abs thy (Var iT) = Var iT
1.133 - | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
1.134 - let val (v',b') = variant_abs (v,T2,b); (*fun variant_abs: term.ML*)
1.135 - in Const ("Let",T1) $ inst_abs thy e $ (Abs (v',T2,inst_abs thy b')) end
1.136 + | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v, T2, b))) =
1.137 + let val b' = subst_bound (Free (v, T2), b);
1.138 + (*fun variant_abs: term.ML*)
1.139 + in Const ("Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
1.140 | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
1.141 - | inst_abs thy t =
1.142 - (writeln("inst_abs: unchanged t= "^ term2str t);
1.143 - t);
1.144 -(*val scr as (Script sc) = Script ((term_of o the o (parse thy))
1.145 - "Script Testeq (e_::bool) = \
1.146 - \While (contains_root e_) Do \
1.147 - \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \
1.148 - \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \
1.149 - \ in Try (Repeat (Rewrite radd_0 False e_))) ");
1.150 -ML> atomt sc;
1.151 -*** Const ( Script.Testeq)
1.152 -*** . Free ( e_, )
1.153 -*** . Const ( Script.While)
1.154 -*** . . Const ( RatArith.contains'_root)
1.155 -*** . . . Free ( e_, )
1.156 -*** . . Const ( Let)
1.157 -*** . . . Const ( Script.Try)
1.158 -*** . . . . Const ( Script.Repeat)
1.159 -*** . . . . . Const ( Script.Rewrite)
1.160 -*** . . . . . . Free ( rroot_square_inv, )
1.161 -*** . . . . . . Const ( False)
1.162 -*** . . . . . . Free ( e_, )
1.163 -*** . . . Abs( e_,..
1.164 -*** . . . . Const ( Let)
1.165 -*** . . . . . Const ( Script.Try)
1.166 -*** . . . . . . Const ( Script.Repeat)
1.167 -*** . . . . . . . Const ( Script.Rewrite)
1.168 -*** . . . . . . . . Free ( square_equation_left, )
1.169 -*** . . . . . . . . Const ( True)
1.170 -*** . . . . . . . . Bound 0 <-- !!!
1.171 -*** . . . . . Abs( e_,..
1.172 -*** . . . . . . Const ( Script.Try)
1.173 -*** . . . . . . . Const ( Script.Repeat)
1.174 -*** . . . . . . . . Const ( Script.Rewrite)
1.175 -*** . . . . . . . . . Free ( radd_0, )
1.176 -*** . . . . . . . . . Const ( False)
1.177 -*** . . . . . . . . . Bound 0 <-- !!!
1.178 -val it = () : unit
1.179 -ML> atomt (inst_abs thy sc);
1.180 -*** Const ( Script.Testeq)
1.181 -*** . Free ( e_, )
1.182 -*** . Const ( Script.While)
1.183 -*** . . Const ( RatArith.contains'_root)
1.184 -*** . . . Free ( e_, )
1.185 -*** . . Const ( Let)
1.186 -*** . . . Const ( Script.Try)
1.187 -*** . . . . Const ( Script.Repeat)
1.188 -*** . . . . . Const ( Script.Rewrite)
1.189 -*** . . . . . . Free ( rroot_square_inv, )
1.190 -*** . . . . . . Const ( False)
1.191 -*** . . . . . . Free ( e_, )
1.192 -*** . . . Abs( e_,..
1.193 -*** . . . . Const ( Let)
1.194 -*** . . . . . Const ( Script.Try)
1.195 -*** . . . . . . Const ( Script.Repeat)
1.196 -*** . . . . . . . Const ( Script.Rewrite)
1.197 -*** . . . . . . . . Free ( square_equation_left, )
1.198 -*** . . . . . . . . Const ( True)
1.199 -*** . . . . . . . . Free ( e_, ) <-- !!!
1.200 -*** . . . . . Abs( e_,..
1.201 -*** . . . . . . Const ( Script.Try)
1.202 -*** . . . . . . . Const ( Script.Repeat)
1.203 -*** . . . . . . . . Const ( Script.Rewrite)
1.204 -*** . . . . . . . . . Free ( radd_0, )
1.205 -*** . . . . . . . . . Const ( False)
1.206 -*** . . . . . . . . . Free ( e_, ) <-- ZUFALL vor 5.03!!!
1.207 -val it = () : unit*)
1.208 -
1.209 -
1.210 -
1.211 -
1.212 -fun inst_abs thy (Const sT) = Const sT
1.213 - | inst_abs thy (Free sT) = Free sT
1.214 - | inst_abs thy (Bound n) = Bound n
1.215 - | inst_abs thy (Var iT) = Var iT
1.216 - | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
1.217 - let val b' = subst_bound (Free(v,T2),b);
1.218 - (*fun variant_abs: term.ML*)
1.219 - in Const ("Let",T1) $ inst_abs thy e $ (Abs (v,T2,inst_abs thy b')) end
1.220 - | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
1.221 - | inst_abs thy t =
1.222 - (writeln("inst_abs: unchanged t= "^ term2str t);
1.223 - t);
1.224 + | inst_abs thy t = t;
1.225 (*val scr =
1.226 "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
1.227 \ (let h_ = (hd o (filterVar f_)) eqs_; \