(* = Tools.ML

    +++ outcommented tests *)

 fun eval_var (thmid:string) (op_:string) 

   (t as (Const(op0,t0) $ arg)) thy = 

   let 

     val t' = ((list2isalist HOLogic.realT) o vars) t;

     val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);

   in Some (thmId, Trueprop $ (mk_equality (t,t'))) end

   | eval_var _ _ _ _ = raise GO_ON;

 (* 

 > val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))";

 > val op_ = "Var";

 > val eval_fn = the (assoc (!eval_list, op_));

 > get_pair op_ eval_fn t;

 > val (t as (Const(op0,t0) $ arg)) = t;

 > eval_fn op0 t; 

 > val thmid = "#Var_";

 > val (Some(thmId,t')) = eval_var thmid op0 t;

 val it = Some ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #))

   : (string * term) option

 > Sign.string_of_term (sign_of thy) t';

 val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string

 *)

 fun eval_Length (thmid:string) (op_:string) 

   (t as (Const(op0,t0) $ arg)) thy = 

   let 

     val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;

     val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);

   in Some (thmId, Trueprop $ (mk_equality (t,t'))) end

   | eval_Length _ _ _ _ = raise GO_ON;

 (*

 > val thmid = "#Length_"; val op_ = "Length";

 > val s = "Length [A = a * b, a // #2 = #2]";

 > val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s;

 > val (Some (id,t')) = eval_Length thmid op_ t;

 val id = "#Length_[A = a * b, a // #2 = #2]" : string

 val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))

 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm

 ---------------------------------------------

 > val thmid = "#Length_"; val op_ = "Length";

 > val s = 

  "if #1 < Length [A = a * b, a // #2 = #2]       \

  \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\

  \else hd [A = a * b, a // #2 = #2]";

 > cterm_of (sign_of thy) t';

 > val t = (term_of o the o (parse thy)) s;

 > val eval_fn = the (assoc (!eval_list, op_));

 > val (Some(_,t')) = get_pair op_ eval_fn t;

 val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))

 val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm

 > val ct = (the o (parse thy)) s;

 > val (Some(_,thm)) = get_calculation thy (op_, eval_fn) ct;

 val thm = "Length [A = a * b, a // #2 = #2] = #2" [[ Free ( #2, real) !!!]]

 > rewrite_ thy tless_true e_rls false thm ct;

 ("if #1 < #2

   then make_fun (R, [make, function], no_met)

        A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",

  []) : (cterm * cterm list) option

 > val ct = (the o (parse thy)) s;

 > rewrite_set_ thy e_rls false eval_script ct;

 ("if #1 < #2

   then make_fun (R, [make, function], no_met)

        A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",

  []) : (cterm * cterm list) option

 *)

 fun eval_Nth (thmid:string) (op_:string) (t as 

 	       (Const (op0,t0) $ t1 $ t2 )) thy =

 (writeln"@@@ eval_Nth";

   if is_num t1 andalso is_list t2

     then

       let 

 	val t' = (nth (num_of_term t1) (isalist2list t2))

 	  handle _ => raise GO_ON; 

 	val thmId = thmid^(Sign.string_of_term (sign_of thy) t1)^

 	  "_"^(Sign.string_of_term (sign_of thy) t2)^

 	  " = "^(Sign.string_of_term (sign_of thy) t');

       in Some (thmId, Trueprop $ (mk_equality (t,t'))) end

   else raise GO_ON

 )

   | eval_Nth _ _ _ _ = raise GO_ON;

 (*

 > val thmid = "#Nth_"; val op_ = "Nth";

 > val s = "Nth #2 [A = a * b, a // #2 = #2]";

 > val t = (term_of o the o (parse thy)) s;

 > eval_Nth thmid op_ t;

 > val eval_fn = the (assoc (!eval_list, op_));

 > val (Some(id,t')) = get_pair op_ eval_fn t;

 > cterm_of (sign_of thy) t';

 val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"

 *)

 (*17.6.00: calc_list instead eval_list*)

 eval_list:= overwritel (! eval_list,

             [("Var",eval_var "#Var_"),

 	     ("Length",eval_Length "#Length_"),

 	     ("Nth",eval_Nth "#Nth_")

 	     ]);

 (*17.6.00: association list for calculate_, calculate*)

 calc_list:= overwritel (! calc_list,

             [

 	     ("Var"   ,("Var",eval_var "#Var_")),

 	     ("Length",("Length",eval_Length "#Length_")),

 	     ("Nth"   ,("Nth",eval_Nth "#Nth_"))

 	     ]);