neuper@37906: (* = Tools.ML
neuper@37906:    +++ outcommented tests *)
neuper@37906: 
neuper@37906: 
neuper@37906: fun eval_var (thmid:string) (op_:string) 
neuper@37906:   (t as (Const(op0,t0) $ arg)) thy = 
neuper@37906:   let 
neuper@37906:     val t' = ((list2isalist HOLogic.realT) o vars) t;
neuper@37933:     val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
neuper@37926:   in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
neuper@37906:   | eval_var _ _ _ _ = raise GO_ON;
neuper@37906: (* 
neuper@37906: > val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))";
neuper@37906: > val op_ = "Var";
neuper@37906: > val eval_fn = the (assoc (!eval_list, op_));
neuper@37906: > get_pair op_ eval_fn t;
neuper@37906: > val (t as (Const(op0,t0) $ arg)) = t;
neuper@37906: > eval_fn op0 t; 
neuper@37906: 
neuper@37906: > val thmid = "#Var_";
neuper@37926: > val (SOME(thmId,t')) = eval_var thmid op0 t;
neuper@37926: val it = SOME ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #))
neuper@37906:   : (string * term) option
neuper@37933: > Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string
neuper@37906: *)
neuper@37906: fun eval_Length (thmid:string) (op_:string) 
neuper@37906:   (t as (Const(op0,t0) $ arg)) thy = 
neuper@37906:   let 
neuper@37906:     val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
neuper@37933:     val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
neuper@37926:   in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
neuper@37906:   | eval_Length _ _ _ _ = raise GO_ON;
neuper@37906: (*
neuper@37906: > val thmid = "#Length_"; val op_ = "Length";
neuper@37906: > val s = "Length [A = a * b, a // #2 = #2]";
neuper@37906: > val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s;
neuper@37926: > val (SOME (id,t')) = eval_Length thmid op_ t;
neuper@37906: val id = "#Length_[A = a * b, a // #2 = #2]" : string
neuper@37906: val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
neuper@37906: val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
neuper@37906: ---------------------------------------------
neuper@37906: > val thmid = "#Length_"; val op_ = "Length";
neuper@37906: > val s = 
neuper@37906:  "if #1 < Length [A = a * b, a // #2 = #2]       \
neuper@37906:  \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\
neuper@37906:  \else hd [A = a * b, a // #2 = #2]";
neuper@37906: 
neuper@37938: > (cterm_of thy) t';
neuper@37906: > val t = (term_of o the o (parse thy)) s;
neuper@37906: > val eval_fn = the (assoc (!eval_list, op_));
neuper@37926: > val (SOME(_,t')) = get_pair op_ eval_fn t;
neuper@37906: val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
neuper@37906: val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
neuper@37906: 
neuper@37906: > val ct = (the o (parse thy)) s;
neuper@37926: > val (SOME(_,thm)) = get_calculation thy (op_, eval_fn) ct;
neuper@37906: val thm = "Length [A = a * b, a // #2 = #2] = #2" [[ Free ( #2, real) !!!]]
neuper@37906: > rewrite_ thy tless_true e_rls false thm ct;
neuper@37906: ("if #1 < #2
neuper@37906:   then make_fun (R, [make, function], no_met)
neuper@37906:        A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
neuper@37906:  []) : (cterm * cterm list) option
neuper@37906: > val ct = (the o (parse thy)) s;
neuper@37906: > rewrite_set_ thy e_rls false eval_script ct;
neuper@37906: ("if #1 < #2
neuper@37906:   then make_fun (R, [make, function], no_met)
neuper@37906:        A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
neuper@37906:  []) : (cterm * cterm list) option
neuper@37906: *)
neuper@37906: 
neuper@37906: fun eval_Nth (thmid:string) (op_:string) (t as 
neuper@37906: 	       (Const (op0,t0) $ t1 $ t2 )) thy =
neuper@37906: (writeln"@@@ eval_Nth";
neuper@37906:   if is_num t1 andalso is_list t2
neuper@37906:     then
neuper@37906:       let 
neuper@37906: 	val t' = (nth (num_of_term t1) (isalist2list t2))
neuper@37906: 	  handle _ => raise GO_ON; 
neuper@37933: 	val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) t1)^
neuper@37933: 	  "_"^(Syntax.string_of_term (thy2ctxt thy) t2)^
neuper@37933: 	  " = "^(Syntax.string_of_term (thy2ctxt thy) t');
neuper@37926:       in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
neuper@37906:   else raise GO_ON
neuper@37906: )
neuper@37906:   | eval_Nth _ _ _ _ = raise GO_ON;
neuper@37906: (*
neuper@37906: > val thmid = "#Nth_"; val op_ = "Nth";
neuper@37906: > val s = "Nth #2 [A = a * b, a // #2 = #2]";
neuper@37906: > val t = (term_of o the o (parse thy)) s;
neuper@37906: > eval_Nth thmid op_ t;
neuper@37906: 
neuper@37906: > val eval_fn = the (assoc (!eval_list, op_));
neuper@37926: > val (SOME(id,t')) = get_pair op_ eval_fn t;
neuper@37938: > (cterm_of thy) t';
neuper@37906: val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: (*17.6.00: calc_list instead eval_list*)
neuper@37906: eval_list:= overwritel (! eval_list,
neuper@37906:             [("Var",eval_var "#Var_"),
neuper@37906: 	     ("Length",eval_Length "#Length_"),
neuper@37906: 	     ("Nth",eval_Nth "#Nth_")
neuper@37906: 	     ]);
neuper@37906: (*17.6.00: association list for calculate_, calculate*)
neuper@37906: calc_list:= overwritel (! calc_list,
neuper@37906:             [
neuper@37906: 	     ("Var"   ,("Var",eval_var "#Var_")),
neuper@37906: 	     ("Length",("Length",eval_Length "#Length_")),
neuper@37906: 	     ("Nth"   ,("Nth",eval_Nth "#Nth_"))
neuper@37906: 	     ]);
neuper@37906: