1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 18 16:46:22 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Wed Aug 18 20:34:41 2021 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  "----------- fun cancel_int --------------------------------------------------------------------";
     1.5  "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
     1.6  "----------- get_pair with 3 args -----------------------";
     1.7 -"----------- calculate (2 * x is_const) -----------------";
     1.8 +"----------- calculate (2 * x is_num) -------------------";
     1.9  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.10  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
    1.11  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.12 @@ -135,15 +135,14 @@
    1.13   val (t,_) = the (rewrite_set_ thy false rls t);
    1.14  (*val t = Free ("3", "Real.real") : term*)
    1.15  
    1.16 -(*--------------(3): is_const works ?: -------------------------------------*)
    1.17 - val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
    1.18 +(*--------------(3): is_num works ?: -------------------------------------*)
    1.19 + val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_num";
    1.20   TermC.atomty t;
    1.21   rewrite_set_ @{theory Test} false tval_rls t;
    1.22  (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
    1.23  
    1.24 - val t = TermC.str2term "2 * x is_const";
    1.25 - val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
    1.26 - UnparseC.term t';
    1.27 + val t = TermC.str2term "2 * x is_num";
    1.28 + val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"});
    1.29   
    1.30  
    1.31  "----------- check calculate bottom up ------------------";
    1.32 @@ -352,17 +351,18 @@
    1.33  then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
    1.34  
    1.35  
    1.36 -"----------- calculate (2 * x is_const) -----------------";
    1.37 -"----------- calculate (2 * x is_const) -----------------";
    1.38 -"----------- calculate (2 * x is_const) -----------------";
    1.39 -val t = TermC.str2term "2 * x is_const";
    1.40 -val SOME (str, t') = eval_const "" "" t @{theory Test};
    1.41 -if UnparseC.term t' = "(2 * x is_const) = False" then ()
    1.42 -else error "eval_const 2 * x is_const CHANGED";
    1.43 +"----------- calculate (2 * x is_num) -------------------";
    1.44 +"----------- calculate (2 * x is_num) -------------------";
    1.45 +"----------- calculate (2 * x is_num) -------------------";
    1.46 +val t = TermC.str2term "(2::real) * x is_num";
    1.47 +
    1.48 +val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test};
    1.49 +if UnparseC.term t' = "(2 * x is_num) = False" then ()
    1.50 +else error "is_num 2 * x is_num CHANGED";
    1.51  
    1.52  val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
    1.53  if UnparseC.term t' = "False" then ()
    1.54 -else error "rewrite_set_ 2 * x is_const CHANGED";
    1.55 +else error "rewrite_set_ 2 * x is_num CHANGED";
    1.56  
    1.57  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.58  "----------- fun get_pair: examples ------------------------------------------------------------";
    1.59 @@ -409,11 +409,11 @@
    1.60  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
    1.61  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
    1.62  (*--------------------------------------------------------------------vvvvvvvvvv*)
    1.63 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
    1.64 -val t = @{term "9 is_const"};
    1.65 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_num");
    1.66 +val t = @{term "9 is_num"};
    1.67  val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
    1.68 -if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
    1.69 -then () else error "adhoc_thm  9 is_const  changed";
    1.70 +if str = "#is_num_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_num) = True"
    1.71 +then () else error "adhoc_thm  9 is_num  changed";
    1.72  
    1.73  case assoc_calc thy \<^const_name>\<open>less\<close> of
    1.74    "le" => () | _ => error "Orderings.ord_class.less <-> le changed";