(* calculate values for function constants

    (c) Walther Neuper 000106

 Some formula transformations cannot be done by rewriting;

 these are done by structure Eval, which works tightly intertwined with structure Rewrite.

 *)

 signature EVALUATE =

 sig

   type ml

   type ml_fun

   val ml_fun_empty: ml_fun

   type ml_from_prog

   val is_num: term -> bool

   val calc_equ: string -> int * int -> bool

   val power: int -> int -> int

   val sign_mult: int -> int -> int

   val squfact: int -> int

   val gcd: int -> int -> int

   val sqrt: int -> int

   val cancel_int: int * int -> int * (int * int)

   val adhoc_thm: Proof.context -> Eval_Def.ml -> term -> (string * thm) option

   val adhoc_thm1_: Proof.context -> Eval_Def.ml -> term -> (string * thm) option

   val norm: term -> term

   val popt2str: Proof.context -> ('a * term) option -> string

   val int_of_numeral: term -> int

 \<^isac_test>\<open>

   val get_pair: Proof.context -> string -> Eval_Def.ml_fun -> term -> (string * term) option

   val mk_rule: term list * term * term -> term

   val divisors: int -> int list

   val doubles: int list -> int list

 \<close>

 end

 (**)

 structure Eval(**): EVALUATE(**) =

 struct

 (**)

 type ml = Eval_Def.ml

 type ml_fun = Eval_Def.ml_fun

 val ml_fun_empty =  Eval_Def.ml_fun_empty

 type ml_from_prog = Eval_Def.ml_from_prog

 val is_num = can HOLogic.dest_number;

 (* trace internal steps of isac's numeral calculations *)

 val eval_trace = Attrib.setup_config_bool \<^binding>\<open>eval_trace\<close> (K false);

 (** calculate integers **)

 fun calc_equ "less"  (n1, n2) = n1 < n2

   | calc_equ "less_eq" (n1, n2) = n1 <= n2

   | calc_equ op_ _ = raise ERROR ("calc_equ: operator = " ^ op_ ^ " not defined");

 fun sqrt (n:int) = if n < 0 then 0 else (trunc o Math.sqrt o Real.fromInt (*FIXME*)) n;

 fun power _ 0 = 1

   | power b n = 

     if n > 0 then b* (power b (n - 1))

     else raise ERROR ("power " ^ TermC.str_of_int b ^ " " ^ TermC.str_of_int n);

 fun gcd 0 b = b

   | gcd a b = if a < b then gcd (b mod a) a else gcd (a mod b) b;

 fun sign n =

   if n < 0 then ~1

 	else if n = 0 then 0 else 1;

 fun sign_mult n1 n2 = (sign n1) * (sign n2);

 fun cancel_int (i1, i2) =

   let

     val sg = sign_mult i1 i2;

     val gcd' = gcd (abs i1) (abs i2);

   in

     (sg, ((abs i1) div gcd', (abs i2) div gcd'))

   end;

 infix dvd;

 fun d dvd n = n mod d = 0;

 fun divisors n =

   let fun pdiv ds d n = 

     if d = n then d :: ds

     else if d dvd n then pdiv (d :: ds) d (n div d)

 	 else pdiv ds (d + 1) n

   in pdiv [] 2 n end;

 fun doubles ds = (* ds is ordered *)

   let fun dbls ds [] = ds

 	| dbls ds [ _ ] = ds

 	| dbls ds (i :: i' :: is) = if i = i' then dbls (i :: ds) is

 				else dbls ds (i'::is)

   in dbls [] ds end;

 fun squfact 0 = 0

   | squfact 1 = 1

   | squfact n = foldl op* (1, (doubles o divisors) n);

 (** calculate numerals **)

 fun popt2str ctxt (SOME (_, term)) = "SOME " ^ UnparseC.term_in_ctxt ctxt term (*TODO \<longrightarrow> str_of_termopt*)

   | popt2str _ NONE = "NONE";

 (* scan a term for applying eval_fn ef 

 args

   thy:

   op_: operator (as string) selecting the root of the pair

   ef : fn : (string -> term -> theory -> (string * term) option)

              ^^^^^^... for creating the string for the resulting theorem

   t  : term to be scanned

 result:

   (string * term) option: found by the eval_* -function of type

        fn : string -> string -> term -> theory -> (string * term) option

             ^^^^^^... the selecting operator op_ (variable for eval_binop)

 *)

 fun trace_calc0 ctxt str =

   if Config.get ctxt eval_trace then writeln ("### " ^ str) else ()

 fun trace_calc1 ctxt str1 str2 =

   if Config.get ctxt eval_trace then writeln (str1 ^ str2) else ()

 fun trace_calc2 ctxt str term popt =

   if Config.get ctxt eval_trace

   then writeln (str ^ UnparseC.term_in_ctxt ctxt term ^ " , " ^ popt2str ctxt popt) else ()

 fun trace_calc3 ctxt str term =

   if Config.get ctxt eval_trace then writeln ("### " ^ str ^ UnparseC.term_in_ctxt ctxt term) else ()

 fun trace_calc4 ctxt str t1 t2 =

   if Config.get ctxt eval_trace

   then writeln ("### " ^ str ^ UnparseC.term_in_ctxt ctxt t1 ^ " $ " ^ UnparseC.term_in_ctxt ctxt t2) else ()

 fun get_pair (*1*)ctxt  op_ (ef: ml_fun) (t as (Const (op0, _) $ arg)) =   (* unary fns *)

     if op_ = op0 then 

       let val popt = ef op_ t ctxt  

       in case popt of SOME _ => popt | NONE => get_pair ctxt  op_ ef arg end

     else get_pair ctxt  op_ ef arg

   | get_pair (*2*)ctxt "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =

     ef "Prog_Expr.ident" t ctxt                                                   (* not nested *)

   | get_pair (*3*)ctxt op_ ef (t as (Const (op0, _) $ t1 $ t2)) =                (* binary funs *)

     (trace_calc1 ctxt "1.. get_pair: binop = " op_;

     if op_ = op0 then 

       let

         val popt = ef op_ t ctxt

         val _ = trace_calc2 ctxt "2.. get_pair: " t popt

       in case popt of SOME _ => popt | NONE => 

         let

           val popt = get_pair ctxt op_ ef t1

           val _ = trace_calc2 ctxt "3.. get_pair: " t1  popt

         in case popt of SOME _ => popt | NONE => get_pair ctxt op_ ef t2 end (* search subterms *)

       end

     else                                                                    (* search subterms *)

       let

         val popt = get_pair ctxt op_ ef t1

         val _ = trace_calc2 ctxt "4.. get_pair: " t popt

       in case popt of SOME _ => popt | NONE => get_pair ctxt op_ ef t2 end)

   | get_pair (*4*)ctxt op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) =          (* ternary funs *)

     (trace_calc3 ctxt "get_pair 4a: t= "t;

     trace_calc1 ctxt "get_pair 4a: op_= " op_;

     trace_calc1 ctxt "get_pair 4a: op0= " op0; 

     if op_ = op0 then 

       case ef op_ t ctxt of st as SOME _ => st | NONE => 

         (case get_pair ctxt op_ ef t2 of st as SOME _ => st | NONE => get_pair ctxt op_ ef t3)

     else 

       (case get_pair ctxt op_ ef t1 of st as SOME _ => st | NONE => 

         (case get_pair ctxt op_ ef t2 of st as SOME _ => st | NONE => get_pair ctxt op_ ef t3)))

   | get_pair (*5*)ctxt op_ ef (Abs (_, _, body)) = get_pair ctxt op_ ef body

   | get_pair (*6*)ctxt op_ ef (t1 $ t2) = 

     let

       val _ = trace_calc4 ctxt "5.. get_pair t1 $ t2: " t1 t2;

       val popt = get_pair ctxt op_ ef t1

     in case popt of SOME _ => popt 

       | NONE => (trace_calc0 ctxt "### get_pair: t1 $ t2 -> NONE"; get_pair ctxt op_ ef t2) 

     end

   | get_pair (*7*)_ _ _ _ = NONE

 (* get a thm from an op_ somewhere in a term by use of get_pair *)

 fun adhoc_thm ctxt (op_, eval_fn) t =

 ((*@{print\<open>tracing\<close>}{a = "adhoc_thm", op_ = op_, t = t, get_p = get_pair thy op_ eval_fn t};*)

   case get_pair ctxt op_ eval_fn t of

     NONE => NONE

   | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t'));

 (* get a thm applying an op_ to a term by direct use of eval_fn *)

 fun adhoc_thm1_ ctxt (op_, eval_fn) ct =

   case eval_fn op_ ct ctxt of

     NONE => NONE

   | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t');

 (** for ordered and conditional rewriting **)

 fun mk_rule (prems, l, r) = 

     HOLogic.Trueprop $ (Logic.list_implies (prems, TermC.mk_equality (l, r)));

 (* 'norms' a rule, e.g.

 (*1*) from a = 1 ==> a*(b+c) = b+c 

       to   a = 1 ==> a*(b+c) = b+c                     no change

 (*2*) from t = t

       to  (t = t) = True                               !!

 (*3*) from [| k < l; m + l = k + n |] ==> m < n

       to   [| k < l; m + l = k + n |] ==> m < n = True !! *)

 fun norm rule =

   let

     val (prems, concl) = 

       (map TermC.strip_trueprop (Logic.strip_imp_prems rule),

         (TermC.strip_trueprop o  Logic.strip_imp_concl) rule)

   in

     if TermC.is_equality concl

     then 

       let val (l, r) = TermC.dest_equals concl

       in

         if l = r then (*2*) mk_rule (prems, concl, @{term True}) else (*1*) rule 

       end

     else (*3*) mk_rule (prems, concl, @{term True})

   end;

 (* preliminary HACK *)

 fun int_of_numeral (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = 0

   | int_of_numeral (Const (\<^const_name>\<open>one_class.one\<close>, _)) = 1

   | int_of_numeral (Const (\<^const_name>\<open>uminus\<close>, _) $ t) = ~1 * int_of_numeral t

   | int_of_numeral (Const (\<^const_name>\<open>numeral\<close>, _) $ n) = HOLogic.dest_numeral n

   | int_of_numeral t = raise TERM ("int_of_numeral", [t]);

 end