1.1 --- a/src/Tools/isac/Scripts/Tools.sml	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,113 +0,0 @@
     1.4 -(* = Tools.ML
     1.5 -   +++ outcommented tests *)
     1.6 -
     1.7 -
     1.8 -fun eval_var (thmid:string) (op_:string) 
     1.9 -  (t as (Const(op0,t0) $ arg)) thy = 
    1.10 -  let 
    1.11 -    val t' = ((list2isalist HOLogic.realT) o vars) t;
    1.12 -    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
    1.13 -  in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.14 -  | eval_var _ _ _ _ = raise GO_ON;
    1.15 -(* 
    1.16 -> val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))";
    1.17 -> val op_ = "Var";
    1.18 -> val eval_fn = the (assoc (!eval_list, op_));
    1.19 -> get_pair op_ eval_fn t;
    1.20 -> val (t as (Const(op0,t0) $ arg)) = t;
    1.21 -> eval_fn op0 t; 
    1.22 -
    1.23 -> val thmid = "#Var_";
    1.24 -> val (SOME(thmId,t')) = eval_var thmid op0 t;
    1.25 -val it = SOME ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #))
    1.26 -  : (string * term) option
    1.27 -> Syntax.string_of_term (thy2ctxt thy) t';
    1.28 -val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string
    1.29 -*)
    1.30 -fun eval_Length (thmid:string) (op_:string) 
    1.31 -  (t as (Const(op0,t0) $ arg)) thy = 
    1.32 -  let 
    1.33 -    val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
    1.34 -    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
    1.35 -  in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.36 -  | eval_Length _ _ _ _ = raise GO_ON;
    1.37 -(*
    1.38 -> val thmid = "#Length_"; val op_ = "Length";
    1.39 -> val s = "Length [A = a * b, a // #2 = #2]";
    1.40 -> val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s;
    1.41 -> val (SOME (id,t')) = eval_Length thmid op_ t;
    1.42 -val id = "#Length_[A = a * b, a // #2 = #2]" : string
    1.43 -val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
    1.44 -val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
    1.45 ----------------------------------------------
    1.46 -> val thmid = "#Length_"; val op_ = "Length";
    1.47 -> val s = 
    1.48 - "if #1 < Length [A = a * b, a // #2 = #2]       \
    1.49 - \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\
    1.50 - \else hd [A = a * b, a // #2 = #2]";
    1.51 -
    1.52 -> (cterm_of thy) t';
    1.53 -> val t = (term_of o the o (parse thy)) s;
    1.54 -> val eval_fn = the (assoc (!eval_list, op_));
    1.55 -> val (SOME(_,t')) = get_pair op_ eval_fn t;
    1.56 -val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
    1.57 -val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
    1.58 -
    1.59 -> val ct = (the o (parse thy)) s;
    1.60 -> val (SOME(_,thm)) = get_calculation thy (op_, eval_fn) ct;
    1.61 -val thm = "Length [A = a * b, a // #2 = #2] = #2" [[ Free ( #2, real) !!!]]
    1.62 -> rewrite_ thy tless_true e_rls false thm ct;
    1.63 -("if #1 < #2
    1.64 -  then make_fun (R, [make, function], no_met)
    1.65 -       A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
    1.66 - []) : (cterm * cterm list) option
    1.67 -> val ct = (the o (parse thy)) s;
    1.68 -> rewrite_set_ thy e_rls false eval_script ct;
    1.69 -("if #1 < #2
    1.70 -  then make_fun (R, [make, function], no_met)
    1.71 -       A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
    1.72 - []) : (cterm * cterm list) option
    1.73 -*)
    1.74 -
    1.75 -fun eval_Nth (thmid:string) (op_:string) (t as 
    1.76 -	       (Const (op0,t0) $ t1 $ t2 )) thy =
    1.77 -(writeln"@@@ eval_Nth";
    1.78 -  if is_num t1 andalso is_list t2
    1.79 -    then
    1.80 -      let 
    1.81 -	val t' = (nth (num_of_term t1) (isalist2list t2))
    1.82 -	  handle _ => raise GO_ON; 
    1.83 -	val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) t1)^
    1.84 -	  "_"^(Syntax.string_of_term (thy2ctxt thy) t2)^
    1.85 -	  " = "^(Syntax.string_of_term (thy2ctxt thy) t');
    1.86 -      in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.87 -  else raise GO_ON
    1.88 -)
    1.89 -  | eval_Nth _ _ _ _ = raise GO_ON;
    1.90 -(*
    1.91 -> val thmid = "#Nth_"; val op_ = "Nth";
    1.92 -> val s = "Nth #2 [A = a * b, a // #2 = #2]";
    1.93 -> val t = (term_of o the o (parse thy)) s;
    1.94 -> eval_Nth thmid op_ t;
    1.95 -
    1.96 -> val eval_fn = the (assoc (!eval_list, op_));
    1.97 -> val (SOME(id,t')) = get_pair op_ eval_fn t;
    1.98 -> (cterm_of thy) t';
    1.99 -val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
   1.100 -*)
   1.101 -
   1.102 -
   1.103 -(*17.6.00: calc_list instead eval_list*)
   1.104 -eval_list:= overwritel (! eval_list,
   1.105 -            [("Var",eval_var "#Var_"),
   1.106 -	     ("Length",eval_Length "#Length_"),
   1.107 -	     ("Nth",eval_Nth "#Nth_")
   1.108 -	     ]);
   1.109 -(*17.6.00: association list for calculate_, calculate*)
   1.110 -calc_list:= overwritel (! calc_list,
   1.111 -            [
   1.112 -	     ("Var"   ,("Var",eval_var "#Var_")),
   1.113 -	     ("Length",("Length",eval_Length "#Length_")),
   1.114 -	     ("Nth"   ,("Nth",eval_Nth "#Nth_"))
   1.115 -	     ]);
   1.116 -