(* calculate values for function constants

   (c) Walther Neuper 000106

*)

signature NUMERAL_CALCULATION =

  sig

    type float

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

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

    val norm: term -> term

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

    val numeral: term -> ((int * int) * (int * int)) option

    val calcul: string -> float -> float -> float

    val term_of_float: typ -> float -> term

    val var_op_float: term -> string -> typ -> typ ->float -> term

    val float_op_var: term -> string -> typ -> typ -> float -> term

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (* NONE *)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    val get_pair: theory -> string -> Rule.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

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

  end

(**)

structure Num_Calc(**): NUMERAL_CALCULATION(**) =

struct

(**)

type float =

  (int * int)   (* value:     significand * exponent *)

  * (int * int) (* precision: significand * exponent *)

(** calculate integers **)

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

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

  | calc_equ op_ _ = 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 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);

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 " ^ Rule.term2str 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 str =

  if ! Celem.trace_calc then writeln ("### " ^ str) else ()

fun trace_calc1 str1 str2 =

  if ! Celem.trace_calc then writeln (str1 ^ str2) else ()

fun trace_calc2 str term popt =

  if ! Celem.trace_calc then writeln (str ^ Rule.term2str term ^ " , " ^ popt2str popt) else ()

fun trace_calc3 str term =

  if ! Celem.trace_calc then writeln ("### " ^ str ^ Rule.term2str term) else ()

fun trace_calc4 str t1 t2 =

  if ! Celem.trace_calc then writeln ("### " ^ str ^ Rule.term2str t1 ^ " $ " ^ Rule.term2str t2) else ()

fun get_pair thy op_ (ef: Rule.eval_fn) (t as (Const (op0, _) $ arg)) =                (* unary fns *)

    if op_ = op0 then 

      let val popt = ef op_ t thy 

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

    else get_pair thy op_ ef arg

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

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

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

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

    if op_ = op0 then 

      let

        val popt = ef op_ t thy

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

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

        let

          val popt = get_pair thy op_ ef t1

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

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

      end

    else                                                                    (* search subterms *)

      let

        val popt = get_pair thy op_ ef t1

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

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

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

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

    trace_calc1 "get_pair 4a: op_= " op_;

    trace_calc1 "get_pair 4a: op0= " op0; 

    if op_ = op0 then 

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

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

    else 

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

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

  | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body

  | get_pair thy op_ ef (t1 $ t2) = 

    let

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

      val popt = get_pair thy op_ ef t1

    in case popt of SOME _ => popt 

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

    end

  | get_pair _ _ _ _ = NONE

(* get a thm from an op_ somewhere in the term;

   apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)

fun adhoc_thm thy (op_, eval_fn) ct =

  case get_pair thy op_ eval_fn ct of

    NONE =>  NONE

  | SOME (thmid, t) => SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of thy)) t);

(* get a thm applying an op_ to a term;

   apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)

fun adhoc_thm1_ thy (op_, eval_fn) ct =

    case eval_fn op_ ct thy of

	NONE => NONE

      | SOME (thmid,t) =>

	SOME (thmid, (Thm.make_thm o (Thm.global_cterm_of 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;

(* convert int and float to internal floatingpoint prepresentation.*)

fun numeral (Free (str, _)) = 

    (case TermC.int_of_str_opt str of

	 SOME i => SOME ((i, 0), (0, 0))

       | NONE => NONE)

  | numeral (Const ("Float.Float", _) $

		   (Const ("Product_Type.Pair", _) $

			  (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $

			  (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=

    (case (TermC.int_of_str_opt v1, TermC.int_of_str_opt v2, TermC.int_of_str_opt p1, TermC.int_of_str_opt p2) of

	(SOME v1', SOME v2', SOME p1', SOME p2') =>

	SOME ((v1', v2'), (p1', p2'))

      | _ => NONE)

  | numeral _ = NONE;

(*** handle numerals in eval_binop ***)

(* TODO rebuild fun calcul, fun term_of_float,fun var_op_float, fun float_op_var:

   Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)

(* used for calculating built in binary operations in Isabelle2002.

   integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0) *)

fun calcul "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int)  = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)

    if b < d 

    then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)

    else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)

  | calcul "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)

    ((a - c,0),(0,0))

  | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)

    ((a * c, b + d), (0, 0))

  | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)

    ((a div c, 0), (0, 0))

  | calcul "Prog_Expr.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)

    ((power a c, 0), (0, 0))

  | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = 

    error ("calcul: not impl. for Float (("^

		 (string_of_int a  )^","^(string_of_int b  )^"), ("^

		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^

		 (string_of_int c  )^","^(string_of_int d  )^"), ("^

		 (string_of_int p21)^","^(string_of_int p22)^"))");

(*> calcul "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); 

val it = ((1,0),(0,0))*)

(*.convert internal floatingpoint prepresentation to int and float.*)

fun term_of_float T ((val1,    0), (         0,          0)) =

    TermC.term_of_num T val1

  | term_of_float T ((val1, val2), (precision1, precision2)) =

    let val pT = TermC.pairT T T

    in Const ("Float.Float", (TermC.pairT pT pT) --> T)

	     $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int val1, T))

			     (Free (TermC.str_of_int val2, T)))

		      (TermC.pairt (Free (TermC.str_of_int precision1, T))

			     (Free (TermC.str_of_int precision2, T))))

    end;

(*> val t = str2term "Float ((1,2),(0,0))";

> val Const ("Float.Float", fT) $ _ = t;

> atomtyp fT;

> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT) 

> 	     (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;

> atomtyp ffT;

> fT = ffT;

val it = true : bool

t = float_term_of_num HOLogic.realT ((1,2),(0,0));

val it = true : bool*)

(*.assoc. convert internal floatingpoint prepresentation to int and float.*)

fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =

    TermC.mk_var_op_num v op_ optype ntyp v1

  | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =

    let val pT = TermC.pairT T T

    in Const (op_, optype) $ v $ 

	     (Const ("Float.Float", (TermC.pairT pT pT) --> T)

		    $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))

				    (Free (TermC.str_of_int v2, T)))

			     (TermC.pairt (Free (TermC.str_of_int p1, T))

				    (Free (TermC.str_of_int p2, T)))))

    end;

(*> val t = str2term "a + b";

> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;

> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";

> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));

val it = true : bool*)

(*.assoc. convert internal floatingpoint prepresentation to int and float.*)

fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =

    TermC.mk_num_op_var v op_ optype ntyp v1

  | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =

    let val pT = TermC.pairT T T

    in Const (op_, optype) $ 

	     (Const ("Float.Float", (TermC.pairT pT pT) --> T)

		    $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))

				    (Free (TermC.str_of_int v2, T)))

			     (TermC.pairt (Free (TermC.str_of_int p1, T))

				    (Free (TermC.str_of_int p2, T))))) $ v

    end;

(*> val t = str2term "a + b";

> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;

> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";

> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));

val it = true : bool*)

end