(* = 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_"))

	     ]);