|
walther@60317
|
1 |
(* Title: "ProgLang/calculate.sml"
|
|
walther@60317
|
2 |
Author: Walther Neuper 2021
|
|
walther@60317
|
3 |
(c) copyright due to lincense terms.
|
|
walther@60317
|
4 |
*)
|
|
walther@60317
|
5 |
|
|
walther@60317
|
6 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@60317
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
|
walther@60317
|
8 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@60317
|
9 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
|
|
walther@60317
|
10 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@60317
|
11 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@60317
|
12 |
"-----------------------------------------------------------------------------------------------";
|
|
walther@60317
|
13 |
|
|
walther@60317
|
14 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
|
|
walther@60317
|
15 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
|
|
walther@60317
|
16 |
"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
|
|
walther@60317
|
17 |
val (t1, t2) = (@{term 3}, @{term "2::real"});
|
|
walther@60317
|
18 |
val t = HOLogic.mk_binop "Groups.plus_class.plus" (t1, t2);
|
|
walther@60317
|
19 |
|
|
walther@60317
|
20 |
eval_binop "" "" t "";
|
|
walther@60317
|
21 |
"~~~~~ fun eval_binop , args:"; val (_, _, (t as (Const (op0, t0) $ t1 $ t2)), _) =(* binary . n1.n2 *)
|
|
walther@60317
|
22 |
((), (), t, ());
|
|
walther@60317
|
23 |
(*if*) TermC.is_num t1 andalso TermC.is_num t2 (*then*);
|
|
walther@60317
|
24 |
val res = calcul op0 (t1, t2);
|
|
walther@60317
|
25 |
val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
|
|
walther@60317
|
26 |
(*in*)
|
|
walther@60317
|
27 |
val xxx = SOME ("#: " ^ UnparseC.term prop, prop);
|
|
walther@60317
|
28 |
(*end*)
|
|
walther@60317
|
29 |
|
|
walther@60317
|
30 |
case xxx of
|
|
walther@60317
|
31 |
SOME
|
|
walther@60317
|
32 |
("#: (3::'a) + 2 = (5::'a)",
|
|
walther@60317
|
33 |
Const ("HOL.Trueprop", _) $
|
|
walther@60317
|
34 |
(Const ("HOL.eq", _) $
|
|
walther@60317
|
35 |
(Const ("Groups.plus_class.plus", _) $ _ $
|
|
walther@60317
|
36 |
(Const ("Num.numeral_class.numeral", _) $ _ )) $
|
|
walther@60317
|
37 |
_ )) => ()
|
|
walther@60317
|
38 |
| _ => error "eval_binop #: (3::'a) + 2 = (5::'a) CHANGED"
|