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

 fun eval_binop _ _

       (t as ((opp as Const (op0, _)) $ (Const (op0', _) $ v $ t1) $ t2)) _ =(* binary . (v.n1).n2 *)

     if op0 = op0' andalso TermC.is_num t1 andalso TermC.is_num t2 then

       let

         val op' = if op0 = "Groups.minus_class.minus" then "Groups.plus_class.plus" else op0

         val res = Eval.calcul op' (t1, t2);

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

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

     else NONE

   | eval_binop _ (_ : string) 

       (t as ((opp as Const (op0, _)) $ t1 $ (Const (op0', _) $ t2 $ v))) _ =(* binary . n1.(n2.v) *)

     if op0 = op0' andalso op0 <> "Groups.minus_class.minus"

         andalso TermC.is_num t1 andalso TermC.is_num t2 then

       let

         val res = Eval.calcul op0 (t1, t2);

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

       in

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

       end

     else NONE

   | eval_binop _ _ (t as (Const (op0, _) $ t1 $ t2)) _ =                       (* binary . n1.n2 *)

     if TermC.is_num t1 andalso TermC.is_num t2 then

       let

         val res = Eval.calcul op0 (t1, t2);

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

       in

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

       end

     else NONE

   | eval_binop _ _ _ _ = NONE; 

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 end