(* Title:  ProgLang/Calculate.thy

    Author: Walther Neuper 000301

    (c) copyright due to lincense terms.

 *)

 theory Calculate

   imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"

 begin

 text \<open>Abstract:

   The Isac project required floating point numbers and complex numbers in early 2000,

   before these numbers were available in Isabelle.

   Since that time numeral calculations are done by ML functions, all named eval_ 

   and integrated into rewriting. eval_binop below is not bound to a specific constant

   (like in Prog_Expr.thy), rather calculates results of Isabelle's binary operations + - * / ^.

   A specialty are the ad-hoc theorems for numeral calculations created in order to provide

   the rewrite engine with theorems as done in general.

 \<close>

 ML_file evaluate.sml

 ML \<open>

 \<close> ML \<open>

 (*** evaluate binary associative operations ***)

 val is_num = can HOLogic.dest_number;

 val is_calcul_op =

   member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];

 fun calcul ctxt lhs =

   let

     val simp_ctxt =

 (*

       Proof_Context.init_global thy

 *)

       ctxt |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});

     val eq = Simplifier.rewrite simp_ctxt (Thm.cterm_of ctxt lhs);

     val rhs = Thm.term_of (Thm.rhs_of eq);

   in rhs end;

 fun eval_binop (_: string) (_: string) t ctxt =

   (case t of

     (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 =>         (* binary \<circ> (v \<circ> n1) \<circ> n2 *)

       if c1 = c2 andalso is_calcul_op c1 andalso is_num t1 andalso is_num t2 then

         let

           val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);

           val res = calcul ctxt (opp' $ t1 $ t2);

           val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));

         in SOME ("#: " ^ UnparseC.term prop, prop) end

       else NONE

   | (opp as Const (c1, _)) $ t1 $ (Const (c2, _) $ t2 $ v) =>         (* binary \<circ> n1 \<circ> (n2 \<circ> v) *)

       if c1 = c2 andalso is_calcul_op c1 andalso c1 <> \<^const_name>\<open>minus\<close>

         andalso is_num t1 andalso is_num t2

       then

         let

           val res = calcul ctxt (opp $ t1 $ t2);

           val prop = HOLogic.Trueprop $ HOLogic.mk_eq (t, opp $ res $ v);

         in

           SOME ("#: " ^ UnparseC.term prop, prop)

         end

       else NONE

   | Const (c, _) $ t1 $ t2 =>                                               (* binary \<circ> n1 \<circ> n2 *)

       if is_calcul_op c andalso is_num t1 andalso is_num t2 then

         let

           val res = calcul ctxt t;

           val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));

         in

           SOME ("#: " ^ UnparseC.term prop, prop)

         end

       else NONE

   | _ => NONE);

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end