1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/ProgLang/calculate.sml	Tue Jun 01 15:41:23 2021 +0200
     1.3 @@ -0,0 +1,38 @@
     1.4 +(* Title:  "ProgLang/calculate.sml"
     1.5 +   Author: Walther Neuper 2021
     1.6 +   (c) copyright due to lincense terms.
     1.7 +*)
     1.8 +
     1.9 +"-----------------------------------------------------------------------------------------------";
    1.10 +"table of contents -----------------------------------------------------------------------------";
    1.11 +"-----------------------------------------------------------------------------------------------";
    1.12 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
    1.13 +"-----------------------------------------------------------------------------------------------";
    1.14 +"-----------------------------------------------------------------------------------------------";
    1.15 +"-----------------------------------------------------------------------------------------------";
    1.16 +
    1.17 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
    1.18 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
    1.19 +"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
    1.20 +val (t1, t2) = (@{term 3}, @{term "2::real"});
    1.21 +val t = HOLogic.mk_binop "Groups.plus_class.plus" (t1, t2);
    1.22 +
    1.23 +           eval_binop "" "" t "";
    1.24 +"~~~~~ fun eval_binop , args:"; val (_, _, (t as (Const (op0, t0) $ t1 $ t2)), _) =(* binary . n1.n2 *)
    1.25 +  ((), (), t, ());
    1.26 +    (*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
    1.27 +        val res = calcul op0 (t1, t2);
    1.28 +        val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
    1.29 +      (*in*)
    1.30 +        val xxx = SOME ("#: " ^ UnparseC.term prop, prop);
    1.31 +      (*end*)
    1.32 +
    1.33 +case xxx of
    1.34 +  SOME
    1.35 +    ("#: (3::'a) + 2 = (5::'a)",
    1.36 +     Const ("HOL.Trueprop", _) $
    1.37 +       (Const ("HOL.eq", _) $
    1.38 +         (Const ("Groups.plus_class.plus", _) $ _ $
    1.39 +           (Const ("Num.numeral_class.numeral", _) $ _ )) $
    1.40 +         _ )) => ()
    1.41 +| _ => error "eval_binop #: (3::'a) + 2 = (5::'a) CHANGED"