(* 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

  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: theory -> string * Eval_Def.eval_fn -> term -> (string * thm) option

  val adhoc_thm1_: theory -> Eval_Def.cal -> term -> (string * thm) option

  val norm: term -> term

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

  val int_of_numeral: term -> int

\<^isac_test>\<open>

  val get_pair: Proof.context -> string -> Eval_Def.eval_fn -> 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

(**)

(* 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 (SOME (_, term)) = "SOME " ^ UnparseC.term 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 term ^ " , " ^ popt2str popt) else ()

fun trace_calc3 ctxt str term =

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

fun trace_calc4 ctxt str t1 t2 =

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

fun get_pair (*1*)ctxt  op_ (ef: Eval_Def.eval_fn) (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 thy (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 (Proof_Context.init_global thy) op_ eval_fn t of

    NONE => NONE

  | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy t'));

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

fun adhoc_thm1_ thy (op_, eval_fn) ct =

  case eval_fn op_ ct (Proof_Context.init_global thy) of

    NONE => NONE

  | SOME (thmid, t') => SOME (thmid, Skip_Proof.make_thm thy 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