1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Apr 22 11:06:48 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Wed Apr 22 11:23:30 2020 +0200
1.3 @@ -234,7 +234,7 @@
1.4 (* we avoid term_to_string''' defined later *)
1.5 fun check_kestore_cas ((t, (s, _)) : CAS_Def.T) =
1.6 "(" ^ (Print_Mode.setmp [] (Syntax.string_of_term (Config.put show_markup false
1.7 - (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.spec2str s ^ ")";
1.8 + (Proof_Context.init_global @{theory})))) t ^ ", " ^ Spec.to_string s ^ ")";
1.9
1.10 fun count_kestore_ptyps [] = 0
1.11 | count_kestore_ptyps ((Store.Node (_, _, ps)) :: ps') =
2.1 --- a/src/Tools/isac/BaseDefinitions/specification.sml Wed Apr 22 11:06:48 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/specification.sml Wed Apr 22 11:23:30 2020 +0200
2.3 @@ -9,12 +9,11 @@
2.4 type metID
2.5 type pblID
2.6 type spec
2.7 - val spec2str: string * string list * string list -> string
2.8 + val to_string: string * string list * string list -> string
2.9 val metID2str: string list -> string
2.10 val e_pblID: pblID
2.11 val e_metID: metID
2.12 - val empty_spec: spec
2.13 - val e_spec: spec
2.14 + val empty: spec
2.15 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
2.16 (*NONE*)
2.17 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
2.18 @@ -27,7 +26,6 @@
2.19 struct
2.20 (**)
2.21
2.22 -(*/------- to Spec -------\*)
2.23 (*the key into the hierarchy ob problems*)
2.24 type pblID = string list; (* domID :: ...*)
2.25 val e_pblID = ["e_pblID"];
2.26 @@ -35,12 +33,10 @@
2.27 (*the key into the hierarchy ob methods*)
2.28 type metID = string list;
2.29 type spec = ThyC.id * pblID * metID;
2.30 -fun spec2str (dom, pbl, met) =
2.31 +fun to_string (dom, pbl, met) =
2.32 "(" ^ quote dom ^ ", " ^ strs2str pbl ^ ", " ^ strs2str met ^ ")";
2.33 val e_metID = ["e_metID"];
2.34 val metID2str = strs2str;
2.35 -val empty_spec = (ThyC.id_empty, e_pblID, e_metID);
2.36 -val e_spec = empty_spec;
2.37 -(*\------- to Spec -------/*)
2.38 +val empty = (ThyC.id_empty, e_pblID, e_metID);
2.39
2.40 (**)end(**)
3.1 --- a/src/Tools/isac/Build_Isac.thy Wed Apr 22 11:06:48 2020 +0200
3.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Apr 22 11:23:30 2020 +0200
3.3 @@ -32,7 +32,7 @@
3.4 *) "BaseDefinitions/BaseDefinitions"
3.5
3.6 (* theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
3.7 - ML_file calculate.sml
3.8 + ML_file evaluate.sml
3.9
3.10 theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions"
3.11 theory Prog_Expr imports Calculate ListC
3.12 @@ -123,7 +123,7 @@
3.13 \<close> ML \<open>
3.14 \<close> ML \<open>
3.15 \<close>
3.16 -ML \<open>Eval.adhoc_thm; (*from "ProgLang/calculate.sml" *)\<close>
3.17 +ML \<open>Eval.adhoc_thm; (*from "ProgLang/evaluate.sml" *)\<close>
3.18 ML \<open>Rewrite.rewrite_; (*from "ProgLang/rewrite.sml" *)\<close>
3.19 ML \<open>Input_Descript.is_reall_dsc; (*from "ProgLang/scrtools.sml" *)\<close>
3.20 ML \<open>Test_Code.me;\<close>
4.1 --- a/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 22 11:06:48 2020 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/ctree-access.sml Wed Apr 22 11:23:30 2020 +0200
4.3 @@ -208,11 +208,11 @@
4.4
4.5 (* insert a new SubProblem' and create a new PblObj in the Ctree *)
4.6 fun append_problem [] l fmz (strs, spec, hdf, ctxt_specify) _ =
4.7 - (Nd (PblObj {origin = (strs, spec, hdf), fmz = fmz, spec = Spec.empty_spec,
4.8 + (Nd (PblObj {origin = (strs, spec, hdf), fmz = fmz, spec = Spec.empty,
4.9 probl = [], meth = [], ctxt = ctxt_specify, loc = (SOME l, NONE),
4.10 branch = TransitiveB, result = (TermC.empty, []), ostate = Incomplete}, []))
4.11 | append_problem p l fmz (strs, spec, hdf, ctxt_specify) pt =
4.12 - insert_pt (PblObj {origin = (strs, spec, hdf), fmz = fmz, spec = Spec.empty_spec,
4.13 + insert_pt (PblObj {origin = (strs, spec, hdf), fmz = fmz, spec = Spec.empty,
4.14 probl = [], meth = [], ctxt = ctxt_specify, loc = (SOME l, NONE),
4.15 branch = TransitiveB, result = (TermC.empty, []), ostate= Incomplete}) pt p;
4.16 fun cappend_problem _ [] loc fmz ori = (append_problem [] loc fmz ori EmptyPtree, [])
5.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 22 11:06:48 2020 +0200
5.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Wed Apr 22 11:23:30 2020 +0200
5.3 @@ -343,9 +343,9 @@
5.4 (* in CalcTree/Subproblem an 'just_created_' model is created;
5.5 this is filled to 'untouched' by Model/Refine_Problem *)
5.6 fun just_created_ (PblObj {meth, probl, spec, ...}) =
5.7 - null meth andalso null probl andalso spec = Spec.empty_spec
5.8 + null meth andalso null probl andalso spec = Spec.empty
5.9 | just_created_ _ = raise PTREE "g_ostate': uncovered fun def.";
5.10 -val e_origin = ([], Spec.empty_spec, TermC.empty);
5.11 +val e_origin = ([], Spec.empty, TermC.empty);
5.12
5.13 fun just_created (pt, (p, _)) =
5.14 let val ppobj = get_obj I pt p
5.15 @@ -441,7 +441,7 @@
5.16 Model.itm list * (* model: given, find, relate *)
5.17 ((bool * term) list) *(* model: preconds *)
5.18 Spec.spec; (* specification *)
5.19 -val e_ocalhd = (false, Und, TermC.empty, [Model.e_itm], [(false, TermC.empty)], Spec.empty_spec);
5.20 +val e_ocalhd = (false, Und, TermC.empty, [Model.e_itm], [(false, TermC.empty)], Spec.empty);
5.21
5.22 datatype ptform = Form of term | ModSpec of ocalhd;
5.23
5.24 @@ -546,7 +546,7 @@
5.25 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
5.26 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ UnparseC.term hdf ^
5.27 ", " ^ Model.itms2str_ (ThyC.id_to_ctxt "Isac_Knowledge") itms ^
5.28 - ", " ^ preconds2str prec ^ ", \n" ^ Spec.spec2str spec ^ " )";
5.29 + ", " ^ preconds2str prec ^ ", \n" ^ Spec.to_string spec ^ " )";
5.30
5.31 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
5.32 | is_pblnd _ = error "is_pblnd: uncovered fun def.";
6.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Wed Apr 22 11:06:48 2020 +0200
6.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Wed Apr 22 11:23:30 2020 +0200
6.3 @@ -54,7 +54,7 @@
6.4 sufficient for mechanically finding the solution for the example.
6.5 FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
6.6 type fmz = fmz_ * Spec.spec;
6.7 -val e_fmz = ([], Spec.empty_spec);
6.8 +val e_fmz = ([], Spec.empty);
6.9
6.10 type result = term * term list
6.11 fun res2str (t, ts) = pair2str (UnparseC.term t, UnparseC.terms ts); (* for tests only *)
7.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 22 11:06:48 2020 +0200
7.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Wed Apr 22 11:23:30 2020 +0200
7.3 @@ -199,7 +199,7 @@
7.4
7.5 fun input_to_string ma = case ma of
7.6 Init_Proof (ppc, spec) =>
7.7 - "Init_Proof "^(pair2str (strs2str ppc, Spec.spec2str spec))
7.8 + "Init_Proof "^(pair2str (strs2str ppc, Spec.to_string spec))
7.9 | Model_Problem => "Model_Problem "
7.10 | Refine_Tacitly pblID => "Refine_Tacitly " ^ strs2str pblID
7.11 | Refine_Problem pblID => "Refine_Problem " ^ strs2str pblID
7.12 @@ -409,7 +409,7 @@
7.13 | Take' of term
7.14
7.15 fun string_of ma = case ma of
7.16 - Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.spec2str spec)
7.17 + Init_Proof' (ppc, spec) => "Init_Proof' " ^ pair2str (strs2str ppc, Spec.to_string spec)
7.18 | Model_Problem' (pblID, _, _) => "Model_Problem' " ^ strs2str pblID
7.19 | Refine_Tacitly'(p, prefin, domID, metID, _) => "Refine_Tacitly' (" ^ strs2str p ^ ", " ^
7.20 strs2str prefin ^ ", " ^ domID ^ ", " ^ strs2str metID ^ ", pbl-itms)"
8.1 --- a/src/Tools/isac/MathEngine/states.sml Wed Apr 22 11:06:48 2020 +0200
8.2 +++ b/src/Tools/isac/MathEngine/states.sml Wed Apr 22 11:23:30 2020 +0200
8.3 @@ -401,7 +401,7 @@
8.4 (2,(((EmptyPtree,(#,#)),[]),([(#,#,#)],[(#,#,#)])))]),(2,[])]
8.5
8.6 val (pt,(p,p_)) = (EmptyPtree,e_pos');
8.7 -val (pt,_) = cappend_problem pt p Uistate ([],e_spec);
8.8 +val (pt,_) = cappend_problem pt p Uistate ([],Spec.empty);
8.9 upd_calc 1 2 ((pt,(p,p_)),[]); !states;
8.10 ML> val it =
8.11 [(1,
9.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Wed Apr 22 11:06:48 2020 +0200
9.2 +++ b/src/Tools/isac/ProgLang/Calculate.thy Wed Apr 22 11:23:30 2020 +0200
9.3 @@ -13,13 +13,13 @@
9.4 Since that time numeral calculations are done by ML functions, all named eval_
9.5 and integrated into rewriting. eval_binop below is not bound to a specific constant
9.6 (like in Prog_Expr.thy), rather calculates results of Isabelle's binary operations + - * / ^.
9.7 - Nowadays the code in Calculate.thy and calculate.sml should be replaced by native Isabelle
9.8 + Nowadays the code in Calculate.thy and evaluate.sml should be replaced by native Isabelle
9.9 code.
9.10 A specialty are the ad-hoc theorems for numeral calculations created in order to provide
9.11 the rewrite engine with theorems as done in general.
9.12 \<close>
9.13
9.14 -ML_file calculate.sml
9.15 +ML_file evaluate.sml
9.16
9.17 ML \<open>
9.18 \<close> ML \<open>
10.1 --- a/src/Tools/isac/ProgLang/calculate.sml Wed Apr 22 11:06:48 2020 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,303 +0,0 @@
10.4 -(* calculate values for function constants
10.5 - (c) Walther Neuper 000106
10.6 -*)
10.7 -
10.8 -signature NUMERAL_CALCULATION =
10.9 -sig
10.10 - type float
10.11 - val calc_equ: string -> int * int -> bool
10.12 - val power: int -> int -> int
10.13 - val sign_mult: int -> int -> int
10.14 - val squfact: int -> int
10.15 - val gcd: int -> int -> int
10.16 - val sqrt: int -> int
10.17 - val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
10.18 - val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
10.19 - val norm: term -> term
10.20 - val popt2str: ('a * term) option -> string
10.21 - val numeral: term -> ((int * int) * (int * int)) option
10.22 - val calcul: string -> float -> float -> float
10.23 - val term_of_float: typ -> float -> term
10.24 - val var_op_float: term -> string -> typ -> typ ->float -> term
10.25 - val float_op_var: term -> string -> typ -> typ -> float -> term
10.26 - val trace_on: bool Unsynchronized.ref
10.27 -
10.28 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
10.29 - (* NONE *)
10.30 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
10.31 - val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
10.32 - val mk_rule: term list * term * term -> term
10.33 - val divisors: int -> int list
10.34 - val doubles: int list -> int list
10.35 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
10.36 -end
10.37 -
10.38 -(**)
10.39 -structure Eval(**): NUMERAL_CALCULATION(**) =
10.40 -struct
10.41 -(**)
10.42 -
10.43 -type float =
10.44 - (int * int) (* value: significand * exponent *)
10.45 - * (int * int); (* precision: significand * exponent *)
10.46 -
10.47 -(* trace internal steps of isac's numeral calculations *)
10.48 -val trace_on = Unsynchronized.ref false;
10.49 -
10.50 -(** calculate integers **)
10.51 -
10.52 -fun calc_equ "less" (n1, n2) = n1 < n2
10.53 - | calc_equ "less_eq" (n1, n2) = n1 <= n2
10.54 - | calc_equ op_ _ = error ("calc_equ: operator = " ^ op_ ^ " not defined");
10.55 -fun sqrt (n:int) = if n < 0 then 0 else (trunc o Math.sqrt o Real.fromInt (*FIXME*)) n;
10.56 -fun power _ 0 = 1
10.57 - | power b n =
10.58 - if n > 0 then b* (power b (n - 1))
10.59 - else error ("power " ^ TermC.str_of_int b ^ " " ^ TermC.str_of_int n);
10.60 -fun gcd 0 b = b
10.61 - | gcd a b = if a < b then gcd (b mod a) a else gcd (a mod b) b;
10.62 -fun sign n =
10.63 - if n < 0 then ~1
10.64 - else if n = 0 then 0 else 1;
10.65 -fun sign_mult n1 n2 = (sign n1) * (sign n2);
10.66 -
10.67 -infix dvd;
10.68 -fun d dvd n = n mod d = 0;
10.69 -fun divisors n =
10.70 - let fun pdiv ds d n =
10.71 - if d = n then d :: ds
10.72 - else if d dvd n then pdiv (d :: ds) d (n div d)
10.73 - else pdiv ds (d + 1) n
10.74 - in pdiv [] 2 n end;
10.75 -
10.76 -fun doubles ds = (* ds is ordered *)
10.77 - let fun dbls ds [] = ds
10.78 - | dbls ds [ _ ] = ds
10.79 - | dbls ds (i :: i' :: is) = if i = i' then dbls (i :: ds) is
10.80 - else dbls ds (i'::is)
10.81 - in dbls [] ds end;
10.82 -fun squfact 0 = 0
10.83 - | squfact 1 = 1
10.84 - | squfact n = foldl op* (1, (doubles o divisors) n);
10.85 -
10.86 -
10.87 -(** calculate numerals **)
10.88 -
10.89 -fun popt2str (SOME (_, term)) = "SOME " ^ UnparseC.term term (*TODO \<longrightarrow> str_of_termopt*)
10.90 - | popt2str NONE = "NONE";
10.91 -
10.92 -(* scan a term for applying eval_fn ef
10.93 -args
10.94 - thy:
10.95 - op_: operator (as string) selecting the root of the pair
10.96 - ef : fn : (string -> term -> theory -> (string * term) option)
10.97 - ^^^^^^... for creating the string for the resulting theorem
10.98 - t : term to be scanned
10.99 -result:
10.100 - (string * term) option: found by the eval_* -function of type
10.101 - fn : string -> string -> term -> theory -> (string * term) option
10.102 - ^^^^^^... the selecting operator op_ (variable for eval_binop)
10.103 -*)
10.104 -fun trace_calc0 str =
10.105 - if ! trace_on then writeln ("### " ^ str) else ()
10.106 -fun trace_calc1 str1 str2 =
10.107 - if ! trace_on then writeln (str1 ^ str2) else ()
10.108 -fun trace_calc2 str term popt =
10.109 - if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
10.110 -fun trace_calc3 str term =
10.111 - if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()
10.112 -fun trace_calc4 str t1 t2 =
10.113 - if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
10.114 -
10.115 -fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
10.116 - if op_ = op0 then
10.117 - let val popt = ef op_ t thy
10.118 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
10.119 - else get_pair thy op_ ef arg
10.120 - | get_pair thy "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =
10.121 - ef "Prog_Expr.ident" t thy (* not nested *)
10.122 - | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) = (* binary funs *)
10.123 - (trace_calc1 "1.. get_pair: binop = " op_;
10.124 - if op_ = op0 then
10.125 - let
10.126 - val popt = ef op_ t thy
10.127 - val _ = trace_calc2 "2.. get_pair: " t popt
10.128 - in case popt of SOME _ => popt | NONE =>
10.129 - let
10.130 - val popt = get_pair thy op_ ef t1
10.131 - val _ = trace_calc2 "3.. get_pair: " t1 popt
10.132 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end
10.133 - end
10.134 - else (* search subterms *)
10.135 - let
10.136 - val popt = get_pair thy op_ ef t1
10.137 - val _ = trace_calc2 "4.. get_pair: " t popt
10.138 - in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
10.139 - | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
10.140 - (trace_calc3 "get_pair 4a: t= "t;
10.141 - trace_calc1 "get_pair 4a: op_= " op_;
10.142 - trace_calc1 "get_pair 4a: op0= " op0;
10.143 - if op_ = op0 then
10.144 - case ef op_ t thy of st as SOME _ => st | NONE =>
10.145 - (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)
10.146 - else
10.147 - (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE =>
10.148 - (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))
10.149 - | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body
10.150 - | get_pair thy op_ ef (t1 $ t2) =
10.151 - let
10.152 - val _ = trace_calc4 "5.. get_pair t1 $ t2: " t1 t2;
10.153 - val popt = get_pair thy op_ ef t1
10.154 - in case popt of SOME _ => popt
10.155 - | NONE => (trace_calc0 "### get_pair: t1 $ t2 -> NONE"; get_pair thy op_ ef t2)
10.156 - end
10.157 - | get_pair _ _ _ _ = NONE
10.158 -
10.159 -(* get a thm from an op_ somewhere in the term;
10.160 - apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)
10.161 -fun adhoc_thm thy (op_, eval_fn) ct =
10.162 - case get_pair thy op_ eval_fn ct of
10.163 - NONE => NONE
10.164 - | SOME (thmid, t) => SOME (thmid, ThmC_Def.make_thm thy t);
10.165 -
10.166 -(* get a thm applying an op_ to a term;
10.167 - apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)
10.168 -fun adhoc_thm1_ thy (op_, eval_fn) ct =
10.169 - case eval_fn op_ ct thy of
10.170 - NONE => NONE
10.171 - | SOME (thmid,t) => SOME (thmid, ThmC_Def.make_thm thy t);
10.172 -
10.173 -(** for ordered and conditional rewriting **)
10.174 -
10.175 -fun mk_rule (prems, l, r) =
10.176 - HOLogic.Trueprop $ (Logic.list_implies (prems, TermC.mk_equality (l, r)));
10.177 -
10.178 -(* 'norms' a rule, e.g.
10.179 -(*1*) from a = 1 ==> a*(b+c) = b+c
10.180 - to a = 1 ==> a*(b+c) = b+c no change
10.181 -(*2*) from t = t
10.182 - to (t = t) = True !!
10.183 -(*3*) from [| k < l; m + l = k + n |] ==> m < n
10.184 - to [| k < l; m + l = k + n |] ==> m < n = True !! *)
10.185 -fun norm rule =
10.186 - let
10.187 - val (prems, concl) =
10.188 - (map TermC.strip_trueprop (Logic.strip_imp_prems rule),
10.189 - (TermC.strip_trueprop o Logic.strip_imp_concl) rule)
10.190 - in
10.191 - if TermC.is_equality concl
10.192 - then
10.193 - let val (l, r) = TermC.dest_equals concl
10.194 - in
10.195 - if l = r then (*2*) mk_rule (prems, concl, @{term True}) else (*1*) rule
10.196 - end
10.197 - else (*3*) mk_rule (prems, concl, @{term True})
10.198 - end;
10.199 -
10.200 -(* convert int and float to internal floatingpoint prepresentation.*)
10.201 -fun numeral (Free (str, _)) =
10.202 - (case ThmC_Def.int_opt_of_string str of
10.203 - SOME i => SOME ((i, 0), (0, 0))
10.204 - | NONE => NONE)
10.205 - | numeral (Const ("Float.Float", _) $
10.206 - (Const ("Product_Type.Pair", _) $
10.207 - (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
10.208 - (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
10.209 - (case (ThmC_Def.int_opt_of_string v1, ThmC_Def.int_opt_of_string v2, ThmC_Def.int_opt_of_string p1, ThmC_Def.int_opt_of_string p2) of
10.210 - (SOME v1', SOME v2', SOME p1', SOME p2') =>
10.211 - SOME ((v1', v2'), (p1', p2'))
10.212 - | _ => NONE)
10.213 - | numeral _ = NONE;
10.214 -
10.215 -(*** handle numerals in eval_binop ***)
10.216 -(* TODO rebuild fun calcul, fun term_of_float,fun var_op_float, fun float_op_var:
10.217 - Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)
10.218 -
10.219 -(* used for calculating built in binary operations in Isabelle2002.
10.220 - integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0) *)
10.221 -fun calcul "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
10.222 - if b < d
10.223 - then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
10.224 - else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
10.225 - | calcul "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
10.226 - ((a - c,0),(0,0))
10.227 - | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
10.228 - ((a * c, b + d), (0, 0))
10.229 - | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
10.230 - ((a div c, 0), (0, 0))
10.231 - | calcul "Prog_Expr.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
10.232 - ((power a c, 0), (0, 0))
10.233 - | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
10.234 - error ("calcul: not impl. for Float (("^
10.235 - (string_of_int a )^","^(string_of_int b )^"), ("^
10.236 - (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
10.237 - (string_of_int c )^","^(string_of_int d )^"), ("^
10.238 - (string_of_int p21)^","^(string_of_int p22)^"))");
10.239 -(*> calcul "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
10.240 -val it = ((1,0),(0,0))*)
10.241 -
10.242 -(*.convert internal floatingpoint prepresentation to int and float.*)
10.243 -fun term_of_float T ((val1, 0), ( 0, 0)) =
10.244 - TermC.term_of_num T val1
10.245 - | term_of_float T ((val1, val2), (precision1, precision2)) =
10.246 - let val pT = TermC.pairT T T
10.247 - in Const ("Float.Float", (TermC.pairT pT pT) --> T)
10.248 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int val1, T))
10.249 - (Free (TermC.str_of_int val2, T)))
10.250 - (TermC.pairt (Free (TermC.str_of_int precision1, T))
10.251 - (Free (TermC.str_of_int precision2, T))))
10.252 - end;
10.253 -(*> val t = str2term "Float ((1,2),(0,0))";
10.254 -> val Const ("Float.Float", fT) $ _ = t;
10.255 -> atomtyp fT;
10.256 -> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
10.257 -> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
10.258 -> atomtyp ffT;
10.259 -> fT = ffT;
10.260 -val it = true : bool
10.261 -
10.262 -t = float_term_of_num HOLogic.realT ((1,2),(0,0));
10.263 -val it = true : bool*)
10.264 -
10.265 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
10.266 -fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
10.267 - TermC.mk_var_op_num v op_ optype ntyp v1
10.268 - | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
10.269 - let val pT = TermC.pairT T T
10.270 - in Const (op_, optype) $ v $
10.271 - (Const ("Float.Float", (TermC.pairT pT pT) --> T)
10.272 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
10.273 - (Free (TermC.str_of_int v2, T)))
10.274 - (TermC.pairt (Free (TermC.str_of_int p1, T))
10.275 - (Free (TermC.str_of_int p2, T)))))
10.276 - end;
10.277 -(*> val t = str2term "a + b";
10.278 -> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
10.279 -> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
10.280 -> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
10.281 -val it = true : bool*)
10.282 -
10.283 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
10.284 -fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
10.285 - TermC.mk_num_op_var v op_ optype ntyp v1
10.286 - | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
10.287 - let val pT = TermC.pairT T T
10.288 - in Const (op_, optype) $
10.289 - (Const ("Float.Float", (TermC.pairT pT pT) --> T)
10.290 - $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
10.291 - (Free (TermC.str_of_int v2, T)))
10.292 - (TermC.pairt (Free (TermC.str_of_int p1, T))
10.293 - (Free (TermC.str_of_int p2, T))))) $ v
10.294 - end;
10.295 -(*> val t = str2term "a + b";
10.296 -> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
10.297 -> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
10.298 -> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
10.299 -val it = true : bool*)
10.300 -
10.301 -end
10.302 -
10.303 -
10.304 -
10.305 -
10.306 -
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Wed Apr 22 11:23:30 2020 +0200
11.3 @@ -0,0 +1,303 @@
11.4 +(* calculate values for function constants
11.5 + (c) Walther Neuper 000106
11.6 +*)
11.7 +
11.8 +signature NUMERAL_CALCULATION =
11.9 +sig
11.10 + type float
11.11 + val calc_equ: string -> int * int -> bool
11.12 + val power: int -> int -> int
11.13 + val sign_mult: int -> int -> int
11.14 + val squfact: int -> int
11.15 + val gcd: int -> int -> int
11.16 + val sqrt: int -> int
11.17 + val adhoc_thm: theory -> string * Exec_Def.eval_fn -> term -> (string * thm) option
11.18 + val adhoc_thm1_: theory -> Exec_Def.cal -> term -> (string * thm) option
11.19 + val norm: term -> term
11.20 + val popt2str: ('a * term) option -> string
11.21 + val numeral: term -> ((int * int) * (int * int)) option
11.22 + val calcul: string -> float -> float -> float
11.23 + val term_of_float: typ -> float -> term
11.24 + val var_op_float: term -> string -> typ -> typ ->float -> term
11.25 + val float_op_var: term -> string -> typ -> typ -> float -> term
11.26 + val trace_on: bool Unsynchronized.ref
11.27 +
11.28 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
11.29 + (* NONE *)
11.30 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
11.31 + val get_pair: theory -> string -> Exec_Def.eval_fn -> term -> (string * term) option
11.32 + val mk_rule: term list * term * term -> term
11.33 + val divisors: int -> int list
11.34 + val doubles: int list -> int list
11.35 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
11.36 +end
11.37 +
11.38 +(**)
11.39 +structure Eval(**): NUMERAL_CALCULATION(**) =
11.40 +struct
11.41 +(**)
11.42 +
11.43 +type float =
11.44 + (int * int) (* value: significand * exponent *)
11.45 + * (int * int); (* precision: significand * exponent *)
11.46 +
11.47 +(* trace internal steps of isac's numeral calculations *)
11.48 +val trace_on = Unsynchronized.ref false;
11.49 +
11.50 +(** calculate integers **)
11.51 +
11.52 +fun calc_equ "less" (n1, n2) = n1 < n2
11.53 + | calc_equ "less_eq" (n1, n2) = n1 <= n2
11.54 + | calc_equ op_ _ = error ("calc_equ: operator = " ^ op_ ^ " not defined");
11.55 +fun sqrt (n:int) = if n < 0 then 0 else (trunc o Math.sqrt o Real.fromInt (*FIXME*)) n;
11.56 +fun power _ 0 = 1
11.57 + | power b n =
11.58 + if n > 0 then b* (power b (n - 1))
11.59 + else error ("power " ^ TermC.str_of_int b ^ " " ^ TermC.str_of_int n);
11.60 +fun gcd 0 b = b
11.61 + | gcd a b = if a < b then gcd (b mod a) a else gcd (a mod b) b;
11.62 +fun sign n =
11.63 + if n < 0 then ~1
11.64 + else if n = 0 then 0 else 1;
11.65 +fun sign_mult n1 n2 = (sign n1) * (sign n2);
11.66 +
11.67 +infix dvd;
11.68 +fun d dvd n = n mod d = 0;
11.69 +fun divisors n =
11.70 + let fun pdiv ds d n =
11.71 + if d = n then d :: ds
11.72 + else if d dvd n then pdiv (d :: ds) d (n div d)
11.73 + else pdiv ds (d + 1) n
11.74 + in pdiv [] 2 n end;
11.75 +
11.76 +fun doubles ds = (* ds is ordered *)
11.77 + let fun dbls ds [] = ds
11.78 + | dbls ds [ _ ] = ds
11.79 + | dbls ds (i :: i' :: is) = if i = i' then dbls (i :: ds) is
11.80 + else dbls ds (i'::is)
11.81 + in dbls [] ds end;
11.82 +fun squfact 0 = 0
11.83 + | squfact 1 = 1
11.84 + | squfact n = foldl op* (1, (doubles o divisors) n);
11.85 +
11.86 +
11.87 +(** calculate numerals **)
11.88 +
11.89 +fun popt2str (SOME (_, term)) = "SOME " ^ UnparseC.term term (*TODO \<longrightarrow> str_of_termopt*)
11.90 + | popt2str NONE = "NONE";
11.91 +
11.92 +(* scan a term for applying eval_fn ef
11.93 +args
11.94 + thy:
11.95 + op_: operator (as string) selecting the root of the pair
11.96 + ef : fn : (string -> term -> theory -> (string * term) option)
11.97 + ^^^^^^... for creating the string for the resulting theorem
11.98 + t : term to be scanned
11.99 +result:
11.100 + (string * term) option: found by the eval_* -function of type
11.101 + fn : string -> string -> term -> theory -> (string * term) option
11.102 + ^^^^^^... the selecting operator op_ (variable for eval_binop)
11.103 +*)
11.104 +fun trace_calc0 str =
11.105 + if ! trace_on then writeln ("### " ^ str) else ()
11.106 +fun trace_calc1 str1 str2 =
11.107 + if ! trace_on then writeln (str1 ^ str2) else ()
11.108 +fun trace_calc2 str term popt =
11.109 + if ! trace_on then writeln (str ^ UnparseC.term term ^ " , " ^ popt2str popt) else ()
11.110 +fun trace_calc3 str term =
11.111 + if ! trace_on then writeln ("### " ^ str ^ UnparseC.term term) else ()
11.112 +fun trace_calc4 str t1 t2 =
11.113 + if ! trace_on then writeln ("### " ^ str ^ UnparseC.term t1 ^ " $ " ^ UnparseC.term t2) else ()
11.114 +
11.115 +fun get_pair thy op_ (ef: Exec_Def.eval_fn) (t as (Const (op0, _) $ arg)) = (* unary fns *)
11.116 + if op_ = op0 then
11.117 + let val popt = ef op_ t thy
11.118 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef arg end
11.119 + else get_pair thy op_ ef arg
11.120 + | get_pair thy "Prog_Expr.ident" ef (t as (Const ("Prog_Expr.ident", _) $ _ $ _ )) =
11.121 + ef "Prog_Expr.ident" t thy (* not nested *)
11.122 + | get_pair thy op_ ef (t as (Const (op0,_) $ t1 $ t2)) = (* binary funs *)
11.123 + (trace_calc1 "1.. get_pair: binop = " op_;
11.124 + if op_ = op0 then
11.125 + let
11.126 + val popt = ef op_ t thy
11.127 + val _ = trace_calc2 "2.. get_pair: " t popt
11.128 + in case popt of SOME _ => popt | NONE =>
11.129 + let
11.130 + val popt = get_pair thy op_ ef t1
11.131 + val _ = trace_calc2 "3.. get_pair: " t1 popt
11.132 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end
11.133 + end
11.134 + else (* search subterms *)
11.135 + let
11.136 + val popt = get_pair thy op_ ef t1
11.137 + val _ = trace_calc2 "4.. get_pair: " t popt
11.138 + in case popt of SOME _ => popt | NONE => get_pair thy op_ ef t2 end)
11.139 + | get_pair thy op_ ef (t as (Const (op0, _) $ t1 $ t2 $ t3)) = (* ternary funs *)
11.140 + (trace_calc3 "get_pair 4a: t= "t;
11.141 + trace_calc1 "get_pair 4a: op_= " op_;
11.142 + trace_calc1 "get_pair 4a: op0= " op0;
11.143 + if op_ = op0 then
11.144 + case ef op_ t thy of st as SOME _ => st | NONE =>
11.145 + (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)
11.146 + else
11.147 + (case get_pair thy op_ ef t1 of st as SOME _ => st | NONE =>
11.148 + (case get_pair thy op_ ef t2 of st as SOME _ => st | NONE => get_pair thy op_ ef t3)))
11.149 + | get_pair thy op_ ef (Abs (_, _, body)) = get_pair thy op_ ef body
11.150 + | get_pair thy op_ ef (t1 $ t2) =
11.151 + let
11.152 + val _ = trace_calc4 "5.. get_pair t1 $ t2: " t1 t2;
11.153 + val popt = get_pair thy op_ ef t1
11.154 + in case popt of SOME _ => popt
11.155 + | NONE => (trace_calc0 "### get_pair: t1 $ t2 -> NONE"; get_pair thy op_ ef t2)
11.156 + end
11.157 + | get_pair _ _ _ _ = NONE
11.158 +
11.159 +(* get a thm from an op_ somewhere in the term;
11.160 + apply ONLY to (uminus_to_string term), uminus_to_string (- 4711) --> (-4711) *)
11.161 +fun adhoc_thm thy (op_, eval_fn) ct =
11.162 + case get_pair thy op_ eval_fn ct of
11.163 + NONE => NONE
11.164 + | SOME (thmid, t) => SOME (thmid, ThmC_Def.make_thm thy t);
11.165 +
11.166 +(* get a thm applying an op_ to a term;
11.167 + apply ONLY to (numbers_to_string term), numbers_to_string (- 4711) --> (-4711) *)
11.168 +fun adhoc_thm1_ thy (op_, eval_fn) ct =
11.169 + case eval_fn op_ ct thy of
11.170 + NONE => NONE
11.171 + | SOME (thmid,t) => SOME (thmid, ThmC_Def.make_thm thy t);
11.172 +
11.173 +(** for ordered and conditional rewriting **)
11.174 +
11.175 +fun mk_rule (prems, l, r) =
11.176 + HOLogic.Trueprop $ (Logic.list_implies (prems, TermC.mk_equality (l, r)));
11.177 +
11.178 +(* 'norms' a rule, e.g.
11.179 +(*1*) from a = 1 ==> a*(b+c) = b+c
11.180 + to a = 1 ==> a*(b+c) = b+c no change
11.181 +(*2*) from t = t
11.182 + to (t = t) = True !!
11.183 +(*3*) from [| k < l; m + l = k + n |] ==> m < n
11.184 + to [| k < l; m + l = k + n |] ==> m < n = True !! *)
11.185 +fun norm rule =
11.186 + let
11.187 + val (prems, concl) =
11.188 + (map TermC.strip_trueprop (Logic.strip_imp_prems rule),
11.189 + (TermC.strip_trueprop o Logic.strip_imp_concl) rule)
11.190 + in
11.191 + if TermC.is_equality concl
11.192 + then
11.193 + let val (l, r) = TermC.dest_equals concl
11.194 + in
11.195 + if l = r then (*2*) mk_rule (prems, concl, @{term True}) else (*1*) rule
11.196 + end
11.197 + else (*3*) mk_rule (prems, concl, @{term True})
11.198 + end;
11.199 +
11.200 +(* convert int and float to internal floatingpoint prepresentation.*)
11.201 +fun numeral (Free (str, _)) =
11.202 + (case ThmC_Def.int_opt_of_string str of
11.203 + SOME i => SOME ((i, 0), (0, 0))
11.204 + | NONE => NONE)
11.205 + | numeral (Const ("Float.Float", _) $
11.206 + (Const ("Product_Type.Pair", _) $
11.207 + (Const ("Product_Type.Pair", _) $ Free (v1, _) $ Free (v2,_)) $
11.208 + (Const ("Product_Type.Pair", _) $ Free (p1, _) $ Free (p2,_))))=
11.209 + (case (ThmC_Def.int_opt_of_string v1, ThmC_Def.int_opt_of_string v2, ThmC_Def.int_opt_of_string p1, ThmC_Def.int_opt_of_string p2) of
11.210 + (SOME v1', SOME v2', SOME p1', SOME p2') =>
11.211 + SOME ((v1', v2'), (p1', p2'))
11.212 + | _ => NONE)
11.213 + | numeral _ = NONE;
11.214 +
11.215 +(*** handle numerals in eval_binop ***)
11.216 +(* TODO rebuild fun calcul, fun term_of_float,fun var_op_float, fun float_op_var:
11.217 + Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)
11.218 +
11.219 +(* used for calculating built in binary operations in Isabelle2002.
11.220 + integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0) *)
11.221 +fun calcul "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
11.222 + if b < d
11.223 + then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
11.224 + else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
11.225 + | calcul "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
11.226 + ((a - c,0),(0,0))
11.227 + | calcul "Groups.times_class.times" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
11.228 + ((a * c, b + d), (0, 0))
11.229 + | calcul "Rings.divide_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
11.230 + ((a div c, 0), (0, 0))
11.231 + | calcul "Prog_Expr.pow" ((a, _), _) ((c, _), _) = (*FIXXXME Float + prec.*)
11.232 + ((power a c, 0), (0, 0))
11.233 + | calcul op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
11.234 + error ("calcul: not impl. for Float (("^
11.235 + (string_of_int a )^","^(string_of_int b )^"), ("^
11.236 + (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
11.237 + (string_of_int c )^","^(string_of_int d )^"), ("^
11.238 + (string_of_int p21)^","^(string_of_int p22)^"))");
11.239 +(*> calcul "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
11.240 +val it = ((1,0),(0,0))*)
11.241 +
11.242 +(*.convert internal floatingpoint prepresentation to int and float.*)
11.243 +fun term_of_float T ((val1, 0), ( 0, 0)) =
11.244 + TermC.term_of_num T val1
11.245 + | term_of_float T ((val1, val2), (precision1, precision2)) =
11.246 + let val pT = TermC.pairT T T
11.247 + in Const ("Float.Float", (TermC.pairT pT pT) --> T)
11.248 + $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int val1, T))
11.249 + (Free (TermC.str_of_int val2, T)))
11.250 + (TermC.pairt (Free (TermC.str_of_int precision1, T))
11.251 + (Free (TermC.str_of_int precision2, T))))
11.252 + end;
11.253 +(*> val t = str2term "Float ((1,2),(0,0))";
11.254 +> val Const ("Float.Float", fT) $ _ = t;
11.255 +> atomtyp fT;
11.256 +> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
11.257 +> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
11.258 +> atomtyp ffT;
11.259 +> fT = ffT;
11.260 +val it = true : bool
11.261 +
11.262 +t = float_term_of_num HOLogic.realT ((1,2),(0,0));
11.263 +val it = true : bool*)
11.264 +
11.265 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
11.266 +fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
11.267 + TermC.mk_var_op_num v op_ optype ntyp v1
11.268 + | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
11.269 + let val pT = TermC.pairT T T
11.270 + in Const (op_, optype) $ v $
11.271 + (Const ("Float.Float", (TermC.pairT pT pT) --> T)
11.272 + $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
11.273 + (Free (TermC.str_of_int v2, T)))
11.274 + (TermC.pairt (Free (TermC.str_of_int p1, T))
11.275 + (Free (TermC.str_of_int p2, T)))))
11.276 + end;
11.277 +(*> val t = str2term "a + b";
11.278 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
11.279 +> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
11.280 +> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
11.281 +val it = true : bool*)
11.282 +
11.283 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
11.284 +fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
11.285 + TermC.mk_num_op_var v op_ optype ntyp v1
11.286 + | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
11.287 + let val pT = TermC.pairT T T
11.288 + in Const (op_, optype) $
11.289 + (Const ("Float.Float", (TermC.pairT pT pT) --> T)
11.290 + $ (TermC.pairt (TermC.pairt (Free (TermC.str_of_int v1, T))
11.291 + (Free (TermC.str_of_int v2, T)))
11.292 + (TermC.pairt (Free (TermC.str_of_int p1, T))
11.293 + (Free (TermC.str_of_int p2, T))))) $ v
11.294 + end;
11.295 +(*> val t = str2term "a + b";
11.296 +> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
11.297 +> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
11.298 +> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
11.299 +val it = true : bool*)
11.300 +
11.301 +end
11.302 +
11.303 +
11.304 +
11.305 +
11.306 +
12.1 --- a/src/Tools/isac/Specify/calchead.sml Wed Apr 22 11:06:48 2020 +0200
12.2 +++ b/src/Tools/isac/Specify/calchead.sml Wed Apr 22 11:23:30 2020 +0200
12.3 @@ -1199,7 +1199,7 @@
12.4 | _ => error "reset_calchead: uncovered case get_obj"
12.5 val pt = update_pbl pt p []
12.6 val pt = update_met pt p []
12.7 - val pt = update_spec pt p Spec.empty_spec
12.8 + val pt = update_spec pt p Spec.empty
12.9 in (pt, (p, Pbl) : pos') end
12.10
12.11 (**)end(**)
12.12 \ No newline at end of file
13.1 --- a/src/Tools/isac/Specify/input-calchead.sml Wed Apr 22 11:06:48 2020 +0200
13.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Wed Apr 22 11:23:30 2020 +0200
13.3 @@ -74,7 +74,7 @@
13.4 val (pI, pits, mI, mits, pre, ctxt) = cas_input_ spec dtss
13.5 val spec = (dI, pI, mI)
13.6 val (pt,_) = Ctree.cappend_problem Ctree.e_ctree [] (Istate_Def.empty, ContextC.empty)
13.7 - ([], Spec.empty_spec) ([], Spec.empty_spec, hdt, ctxt)
13.8 + ([], Spec.empty) ([], Spec.empty, hdt, ctxt)
13.9 val pt = Ctree.update_spec pt [] spec
13.10 val pt = Ctree.update_pbl pt [] pits
13.11 val pt = Ctree.update_met pt [] mits
13.12 @@ -101,10 +101,10 @@
13.13 imodel * (*the model (without Find) of the calc-head*)
13.14 Pos.pos_ * (*model belongs to Pbl or Met*)
13.15 Spec.spec; (*specification: domID, pblID, metID*)
13.16 -val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Spec.empty_spec)
13.17 +val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Spec.empty)
13.18
13.19 fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Selem.fmz) =
13.20 - hdf <> "" andalso fmz_ = [] andalso spec = Spec.empty_spec
13.21 + hdf <> "" andalso fmz_ = [] andalso spec = Spec.empty
13.22
13.23 (* re-parse itms with a new thy and prepare for checking with ori list *)
13.24 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
14.1 --- a/src/Tools/isac/Specify/specify.sml Wed Apr 22 11:06:48 2020 +0200
14.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Apr 22 11:23:30 2020 +0200
14.3 @@ -109,7 +109,7 @@
14.4 else (* new example, pepare for interactive modeling *)
14.5 let
14.6 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
14.7 - ([], Spec.empty_spec) ([], Spec.empty_spec, TermC.empty, ContextC.empty)
14.8 + ([], Spec.empty) ([], Spec.empty, TermC.empty, ContextC.empty)
14.9 in ((pt, ([], Pbl)), []) end
14.10 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
14.11 let (* both """"""""""""""""""""""""" either empty or complete *)
15.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Apr 22 11:06:48 2020 +0200
15.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Apr 22 11:23:30 2020 +0200
15.3 @@ -307,7 +307,7 @@
15.4 else (* new example, pepare for interactive modeling *)
15.5 let
15.6 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
15.7 - ([], Spec.empty_spec) ([], Spec.empty_spec, TermC.empty, ContextC.empty)
15.8 + ([], Spec.empty) ([], Spec.empty, TermC.empty, ContextC.empty)
15.9 in ((pt, ([], Pbl)), []) end
15.10 | nxt_specify_init_calc (fmz, (dI, pI, mI)) =
15.11 let (* both """"""""""""""""""""""""" either empty or complete *)
16.1 --- a/src/Tools/isac/TODO.thy Wed Apr 22 11:06:48 2020 +0200
16.2 +++ b/src/Tools/isac/TODO.thy Wed Apr 22 11:23:30 2020 +0200
16.3 @@ -32,7 +32,7 @@
16.4 \item replace src/ Erls Rule_Set.Empty
16.5 \item xxx
16.6 \item rename exec-def.sml -> eval_def.sml
16.7 - calculate.sml _> evaluate.sml (struct Eval -> Evaluate?!?)
16.8 + evaluate.sml _> evaluate.sml (struct Eval -> Evaluate?!?)
16.9 \item xxx
16.10 \item rename Know_Store -> Know_Store KNOWLEDGE_STORE + file.sml
16.11 Build_Thydata -> Build_Knowledge
17.1 --- a/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 22 11:06:48 2020 +0200
17.2 +++ b/test/Tools/isac/BridgeLibisabelle/use-cases.sml Wed Apr 22 11:23:30 2020 +0200
17.3 @@ -987,7 +987,7 @@
17.4 Relate ["relations"]],
17.5 (*input (Arbfix will dissappear soon)*)
17.6 Pbl (*belongsto*),
17.7 - Spec.e_spec (*no input to the specification*));
17.8 + Spec.Spec.empty (*no input to the specification*));
17.9
17.10 (*the user does not know, what 'superfluous' for 'maximum b' may mean
17.11 and asks what to do next*)
17.12 @@ -1001,7 +1001,7 @@
17.13 [Given ["fixedValues [r=Arbfix]"],
17.14 Find ["maximum A", "valuesFor [a,b]"(*new input*)],
17.15 Relate ["relations [A=a*b, \
17.16 - \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, Spec.e_spec);
17.17 + \(a/2)^2 + (b/2)^2 = r^2]"]], Pbl, Spec.Spec.empty);
17.18
17.19 (*specification is not interesting and should be skipped by the dialogguide;
17.20 !!!!!!!!!!!!!!!!!!!! input of ONE part at a time !!!!!!!!!!!!!!!!!!!!!!*)
18.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 22 11:06:48 2020 +0200
18.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Wed Apr 22 11:23:30 2020 +0200
18.3 @@ -412,7 +412,7 @@
18.4 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
18.5
18.6 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
18.7 - val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
18.8 + val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, Spec.empty);
18.9 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.10 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
18.11
18.12 @@ -420,7 +420,7 @@
18.13 val (b,pt,ocalhd) =
18.14 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
18.15 Find ["maximum", "valuesFor"],
18.16 - Relate ["relations"]], Pbl, e_spec);
18.17 + Relate ["relations"]], Pbl, Spec.empty);
18.18 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.19 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
18.20 else error "informtest.sml: diff.behav. max 2";
18.21 @@ -430,7 +430,7 @@
18.22 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
18.23 Find ["maximum A", "valuesFor [a,b]"],
18.24 Relate ["relations [A=a*b, a/2=r*sin alpha, \
18.25 - \b/2=r*cos alpha]"]], Pbl, e_spec);
18.26 + \b/2=r*cos alpha]"]], Pbl, Spec.empty);
18.27 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.28 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing !!!*)
18.29
18.30 @@ -440,7 +440,7 @@
18.31 Find ["maximum A", "valuesFor [a,b]"],
18.32 Relate ["relations [A=a*b, \
18.33 \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
18.34 - Pbl, e_spec);
18.35 + Pbl, Spec.empty);
18.36 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str_ ctxt)) pbl;
18.37
18.38 modifycalcheadOK2xml 111 (bool2str b) ocalhd;
19.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Wed Apr 22 11:06:48 2020 +0200
19.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Wed Apr 22 11:23:30 2020 +0200
19.3 @@ -66,7 +66,7 @@
19.4 handle _ => error "--- fun get_ctxt not even some ctxt found in PrfObj";
19.5
19.6 val pt = EmptyPtree;
19.7 -val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], Spec.e_spec, TermC.empty, ContextC.empty) pt;
19.8 +val pt = append_problem [] (Istate.empty, ContextC.empty) e_fmz ([(*oris*)], Spec.Spec.empty, TermC.empty, ContextC.empty) pt;
19.9 val ctxt = get_obj g_ctxt pt [];
19.10 if ContextC.is_empty ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
19.11
19.12 @@ -504,7 +504,7 @@
19.13
19.14 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**)cappend_problem: pos =[3]*)
19.15 val p = ([3], Pbl);
19.16 -val (pt,cuts) = cappend_problem pt (fst p) Istate.empty e_fmz ([],e_spec,TermC.empty, ContextC.empty);
19.17 +val (pt,cuts) = cappend_problem pt (fst p) Istate.empty e_fmz ([],Spec.empty,TermC.empty, ContextC.empty);
19.18 if is_pblobj (get_obj I pt (fst p)) then () else
19.19 error "ctree.sml, diff.behav. cappend minisubpbl ([3],Pbl)";
19.20 if not (existpt ((lev_on o fst) p) pt) then () else
19.21 @@ -1217,8 +1217,8 @@
19.22 *)
19.23
19.24 "---(4) on S(606)..S(608)--------";
19.25 -val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],e_spec)
19.26 - ([],e_spec, str2term "Inhead[3]", ContextC.empty);
19.27 +val (pt', cuts) = cappend_problem pt [3] Istate.empty ([],Spec.empty)
19.28 + ([],Spec.empty, str2term "Inhead[3]", ContextC.empty);
19.29 (*default_print_depth 99;*)
19.30 cuts;
19.31 (*default_print_depth 3;*)
20.1 --- a/test/Tools/isac/ProgLang/calculate.sml Wed Apr 22 11:06:48 2020 +0200
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,447 +0,0 @@
20.4 -(* Title: "ProgLang/calculate.sml"
20.5 - test calculation of values for function constants
20.6 - Author: Walther Neuper 2000
20.7 - (c) copyright due to lincense terms.
20.8 -*)
20.9 -
20.10 -"--------------------------------------------------------";
20.11 -"table of contents --------------------------------------";
20.12 -"--------------------------------------------------------";
20.13 -"-calculate.thy: provides 'setup' -----------------------";
20.14 -"----------- fun norm -----------------------------------";
20.15 -"----------- check return value of adhoc_thm ----";
20.16 -"----------- fun calculate_ --------------------------------------------------------------------";
20.17 -"----------- calculate from Prog --------------------------------- -----------------------------";
20.18 -"----------- calculate from script --requires 'setup'----";
20.19 -"----------- calculate check test-root-equ --------------";
20.20 -"----------- check calcul,ate bottom up -----------------";
20.21 -"----------- Prog_Expr.pow Power.power_class.power ---------";
20.22 -" ================= calculate.sml: calculate_ 2002 ======";
20.23 -"----------- get_pair with 3 args -----------------------";
20.24 -"----------- calculate (2 * x is_const) -----------------";
20.25 -"----------- fun get_pair: examples ------------------------------------------------------------";
20.26 -"----------- fun adhoc_thm: examples -----------------------------------------------------------";
20.27 -"----------- fun power -------------------------------------------------------------------------";
20.28 -"----------- fun divisors ----------------------------------------------------------------------";
20.29 -"----------- fun doubles, fun squfact ----------------------------------------------------------";
20.30 -"--------------------------------------------------------";
20.31 -"--------------------------------------------------------";
20.32 -"--------------------------------------------------------";
20.33 -
20.34 -"----------- check return value of adhoc_thm ----";
20.35 -"----------- check return value of adhoc_thm ----";
20.36 -"----------- check return value of adhoc_thm ----";
20.37 -val thy = @{theory "Poly"};
20.38 -val cal = snd (assoc_calc' thy "is_polyexp");
20.39 -val t = @{term "(x / x) is_polyexp"};
20.40 -val SOME (thmID, thm) = adhoc_thm thy cal t;
20.41 -(HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
20.42 -handle TERM _ =>
20.43 - error "calculate.sml: adhoc_thm must return Trueprop";
20.44 -
20.45 -"----------- fun calculate_ --------------------------------------------------------------------";
20.46 -"----------- fun calculate_ --------------------------------------------------------------------";
20.47 -"----------- fun calculate_ --------------------------------------------------------------------";
20.48 -(* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
20.49 -val t = str2term "((1+2)*4/3)^^^2";
20.50 -val thy = @{theory};
20.51 -val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Exec_Def.eval_fn;
20.52 -val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Exec_Def.eval_fn;
20.53 -val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * Exec_Def.eval_fn;
20.54 -val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * Exec_Def.eval_fn;
20.55 -
20.56 -"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
20.57 -val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
20.58 -val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
20.59 -if UnparseC.term t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_ 1 + 2 = 3 changed";
20.60 -
20.61 -"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
20.62 -val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
20.63 -val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
20.64 -if UnparseC.term t'' = "(12 / 3) ^^^ 2" then () else error "calculate_ 3 * 4 = 12 changed";
20.65 -
20.66 -"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
20.67 -val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
20.68 -val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
20.69 -if UnparseC.term t''' = "4 ^^^ 2" then () else error "calculate_ 12 / 3 = 4 changed";
20.70 -
20.71 -"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
20.72 -val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
20.73 -val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
20.74 -if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
20.75 -
20.76 -"----------- calculate from Prog --------------------------------- -----------------------------";
20.77 -"----------- calculate from Prog --------------------------------- -----------------------------";
20.78 -"----------- calculate from Prog --------------------------------- -----------------------------";
20.79 -val thy = @{theory "Test"};
20.80 -val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
20.81 -val (dI',pI',mI') =
20.82 - ("Test",["calculate","test"],["Test","test_calculate"]);
20.83 -
20.84 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.85 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.86 -(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
20.87 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.88 -(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
20.89 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.90 -(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
20.91 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.92 -(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
20.93 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.94 -(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
20.95 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
20.96 -(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
20.97 -
20.98 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*)
20.99 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*)
20.100 -(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*)
20.101 -(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*)
20.102 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
20.103 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*)
20.104 -case f of FormKF "16" => () | _ =>
20.105 -error "calculate.sml: script test_calculate changed behaviour";
20.106 -
20.107 -
20.108 -"----------- calculate check test-root-equ --------------";
20.109 -"----------- calculate check test-root-equ --------------";
20.110 -"----------- calculate check test-root-equ --------------";
20.111 -(*(1): 2nd Test_simplify didn't work:
20.112 -val ct =
20.113 - "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
20.114 -> val rls = ("Test_simplify");
20.115 -> val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
20.116 -val ct = "sqrt (x ^^^ 2 + -3 * x) =
20.117 -(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
20.118 -ie. cancel does not work properly
20.119 -*)
20.120 - val thy = @{theory "Test"};
20.121 - val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
20.122 - val ct = ThmC_Def.num_to_Free @{term
20.123 - "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
20.124 -case calculate_ thy op_ ct of
20.125 - SOME _ => ()
20.126 -| NONE => error "calculate_ test-root-equ changed";
20.127 -(*
20.128 - sqrt (x ^^^ 2 + -3 * x) =\
20.129 - \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
20.130 -............... does not work *)
20.131 -
20.132 -(*--------------(2): does divide work in Test_simplify ?: ------*)
20.133 - val thy = @{theory Test};
20.134 - val t = (Thm.term_of o the o (parse thy)) "6 / 2";
20.135 - val rls = Test_simplify;
20.136 - val (t,_) = the (rewrite_set_ thy false rls t);
20.137 -(*val t = Free ("3","Real.real") : term*)
20.138 -
20.139 -(*--------------(3): is_const works ?: -------------------------------------*)
20.140 - val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
20.141 - atomty t;
20.142 - rewrite_set_ @{theory Test} false tval_rls t;
20.143 -(*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
20.144 -
20.145 - val t = str2term "2 * x is_const";
20.146 - val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
20.147 - UnparseC.term t';
20.148 -
20.149 -
20.150 -"----------- check calculate bottom up ------------------";
20.151 -"----------- check calculate bottom up ------------------";
20.152 -"----------- check calculate bottom up ------------------";
20.153 -(*-------------- eval_cancel works: *)
20.154 - Rewrite.trace_on := false;
20.155 - val thy = @{theory Test};
20.156 - val rls = Test_simplify;
20.157 - val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
20.158 -
20.159 -val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
20.160 -
20.161 -(*--------------(5): reproduce (1) with simpler term: ------------*)
20.162 - val t = (Thm.term_of o the o (parse thy)) "(3+5)/2";
20.163 -case rewrite_set_ thy false rls t of
20.164 - SOME (Free ("4", _), []) => ()
20.165 -| _ => error "rewrite_set_ (3+5)/2 changed";
20.166 -
20.167 - val t = (Thm.term_of o the o (parse thy)) "(3+1+2*x)/2";
20.168 -case rewrite_set_ thy false rls t of
20.169 - SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
20.170 -| _ => error "rewrite_set_ (3+1+2*x)/2 changed";
20.171 -
20.172 - Rewrite.trace_on:=false; (*=true3.6.03*)
20.173 -
20.174 -(*--- Rewrite.trace_on before correction of ... --------------------
20.175 - val ct = "(-3 + 2 * x + -1) / 2";
20.176 - val (ct,_) = the (rewrite_set thy' false rls ct);
20.177 -:
20.178 -### trying thm 'root_ge0_2'
20.179 -### rewrite_set_: x + (-1 + -3) / 2
20.180 -### trying thm 'radd_real_const_eq'
20.181 -### trying thm 'radd_real_const'
20.182 -### rewrite_set_: x + (-4) / 2
20.183 -### trying thm 'rcollect_right'
20.184 -:
20.185 -"x + (-4) / 2"
20.186 --------------------------------------while before Isabelle20002:
20.187 - val ct = "(#-3 + #2 * x + #-1) // #2";
20.188 - val (ct,_) = the (rewrite_set thy' false rls ct);
20.189 -:
20.190 -### trying thm 'root_ge0_2'
20.191 -### rewrite_set_: x + (#-1 + #-3) // #2
20.192 -### trying thm 'radd_real_const_eq'
20.193 -### trying thm 'radd_real_const'
20.194 -### rewrite_set_: x + #-4 // #2
20.195 -### rewrite_set_: x + #-2
20.196 -### trying thm 'rcollect_right'
20.197 -:
20.198 -"#-2 + x"
20.199 ------------------------------------------------------------------*)
20.200 -
20.201 -
20.202 -(*===================*)
20.203 - Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
20.204 - val t = (Thm.term_of o the o (parse thy)) "x + (-1 + -3) / 2";
20.205 -val SOME (res, []) = rewrite_set_ thy false rls t;
20.206 -if UnparseC.term res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
20.207 -"x + (-4) / 2";
20.208 -(*
20.209 -### trying calc. 'cancel'
20.210 -@@@ get_pair: binop, t = x + (-4) / 2
20.211 -@@@ get_pair: t else
20.212 -@@@ get_pair: t else -> NONE
20.213 -@@@ get_pair: binop, t = (-4) / 2
20.214 -@@@ get_pair: then 1
20.215 -@@@ get_pair: t -> NONE
20.216 -@@@ get_pair: t1 -> NONE
20.217 -@@@ adhoc_thm': NONE
20.218 -### trying calc. 'pow'
20.219 -*)
20.220 -
20.221 - Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
20.222 -
20.223 -"----------- Prog_Expr.pow Power.power_class.power ---------";
20.224 -"----------- Prog_Expr.pow Power.power_class.power ---------";
20.225 -"----------- Prog_Expr.pow Power.power_class.power ---------";
20.226 -val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
20.227 -atomty t;
20.228 -(*** -------------
20.229 -*** Const ( Nat.power, ['a, nat] => 'a)
20.230 -*** . Free ( 1, 'a)
20.231 -*** . Free ( aaa, nat) *)
20.232 -
20.233 -val t = str2term "1 ^^^ aaa";
20.234 -atomty t;
20.235 -(****
20.236 -*** Const (Prog_Expr.pow, real => real => real)
20.237 -*** . Free (1, real)
20.238 -*** . Free (aaa, real)
20.239 -*** *);
20.240 -
20.241 -" ================= calculate.sml: calculate_ 2002 =================== ";
20.242 -" ================= calculate.sml: calculate_ 2002 =================== ";
20.243 -" ================= calculate.sml: calculate_ 2002 =================== ";
20.244 -
20.245 -val thy = @{theory Test};
20.246 -val t = (Thm.term_of o the o (parse thy)) "12 / 3";
20.247 -val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
20.248 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
20.249 -"12 / 3 = 4";
20.250 -val thy = @{theory Test};
20.251 -val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
20.252 -val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
20.253 -val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
20.254 -"4 ^ 2 = 16";
20.255 -
20.256 - val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
20.257 - val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
20.258 -"1 + 2 = 3";
20.259 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
20.260 - UnparseC.term t;
20.261 -"(3 * 4 / 3) ^^^ 2";
20.262 - val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
20.263 -"3 * 4 = 12";
20.264 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
20.265 - UnparseC.term t;
20.266 -"(12 / 3) ^^^ 2";
20.267 - val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
20.268 -"12 / 3 = 4";
20.269 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
20.270 - UnparseC.term t;
20.271 -"4 ^^^ 2";
20.272 - val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
20.273 -"4 ^^^ 2 = 16";
20.274 - val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
20.275 - UnparseC.term t;
20.276 -"16";
20.277 - if it <> "16" then error "calculate.sml: new behaviour in calculate_"
20.278 - else ();
20.279 -
20.280 -(*13.9.02 *** calc: operator = pow not defined*)
20.281 - val t = (Thm.term_of o the o (parse thy)) "3^^^2";
20.282 - val SOME (thmID,thm) =
20.283 - adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
20.284 -(*** calc: operator = pow not defined*)
20.285 -
20.286 - val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
20.287 - (*
20.288 -val op_ = "Prog_Expr.pow" : string
20.289 -val eval_fn = fn : string -> term -> theory -> (string * term) option*)
20.290 -
20.291 - val SOME (thmid,t') = get_pair thy op_ eval_fn t;
20.292 -(*** calc: operator = pow not defined*)
20.293 -
20.294 - val SOME (id,t') = eval_fn op_ t thy;
20.295 -(*** calc: operator = pow not defined*)
20.296 -
20.297 - val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
20.298 - val SOME (id,t') = eval_binop thmid op_ t thy;
20.299 -(*** calc: operator = pow not defined*)
20.300 -
20.301 -
20.302 -"----------- get_pair with 3 args --------------------------------";
20.303 -"----------- get_pair with 3 args --------------------------------";
20.304 -"----------- get_pair with 3 args --------------------------------";
20.305 -val (thy, op_, ef, arg) =
20.306 - (thy, "EqSystem.occur'_exactly'_in",
20.307 - assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
20.308 - str2term
20.309 - "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
20.310 - );
20.311 -val SOME (str, simpl) = get_pair thy op_ ef arg;
20.312 -if str =
20.313 -"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
20.314 -then () else error "calculate.sml get_pair with 3 args:occur_exactly_in";
20.315 -
20.316 -
20.317 -"----------- calculate (2 * x is_const) -----------------";
20.318 -"----------- calculate (2 * x is_const) -----------------";
20.319 -"----------- calculate (2 * x is_const) -----------------";
20.320 -val t = str2term "2 * x is_const";
20.321 -val SOME (str, t') = eval_const "" "" t @{theory Test};
20.322 -UnparseC.term t';
20.323 -"(2 * x is_const) = False";
20.324 -
20.325 -val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
20.326 -UnparseC.term t';
20.327 -"HOL.False";
20.328 -
20.329 -"----------- fun get_pair: examples ------------------------------------------------------------";
20.330 -"----------- fun get_pair: examples ------------------------------------------------------------";
20.331 -"----------- fun get_pair: examples ------------------------------------------------------------";
20.332 -val thy = @{theory};
20.333 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
20.334 -
20.335 -val t = (Thm.term_of o the o (parse thy)) "3 + 4";
20.336 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
20.337 -if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
20.338 -then () else error "get_pair 3 + 4 changed";
20.339 -
20.340 -val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
20.341 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
20.342 -if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
20.343 -then () else error "get_pair (a + 3) + 4 changed";
20.344 -
20.345 -val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
20.346 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
20.347 -if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
20.348 -then () else error "get_pair (a + 3) + 4 changed";
20.349 -
20.350 -val t = (Thm.term_of o the o (parse thy)) "x = 5 * (3 + (4 + a))";
20.351 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
20.352 -if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
20.353 -then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
20.354 -
20.355 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
20.356 -
20.357 -val t = (Thm.term_of o the o (parse thy)) "-4 / -2";
20.358 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
20.359 -if str = "#divide_e-4_-2" andalso UnparseC.term term = "-4 / -2 = 2"
20.360 -then () else error "get_pair -4 / -2 changed";
20.361 -
20.362 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
20.363 -
20.364 -val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3";
20.365 -val SOME (str, term) = get_pair thy isa_str eval_fn t;
20.366 -if str = "#: 2 ^^^ 3 = 8" andalso UnparseC.term term = "2 ^^^ 3 = 8"
20.367 -then () else error "get_pair 2 ^^^ 3 changed";
20.368 -
20.369 -"----------- fun adhoc_thm: examples -----------------------------------------------------------";
20.370 -"----------- fun adhoc_thm: examples -----------------------------------------------------------";
20.371 -"----------- fun adhoc_thm: examples -----------------------------------------------------------";
20.372 -(*--------------------------------------------------------------------vvvvvvvvvv*)
20.373 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
20.374 -val SOME t = parseNEW @{context} "9 is_const";
20.375 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
20.376 -if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
20.377 -then () else error "adhoc_thm 9 is_const changed";
20.378 -
20.379 -
20.380 -case assoc_calc thy "Orderings.ord_class.less" of
20.381 - "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
20.382 -(*--------------------------------------------------------------------vvvvvvvvvv*)
20.383 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
20.384 -
20.385 -val SOME t = parseNEW @{context} "4 < 4";
20.386 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
20.387 -if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
20.388 -then () else error "adhoc_thm 4 < 4 changed";
20.389 -
20.390 -val SOME t = parseNEW @{context} "a < 4";
20.391 -case adhoc_thm thy (isa_str, eval_fn) t of
20.392 -NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
20.393 -
20.394 -
20.395 -(*--------------------------------------------------------------------vvvvvvvvvv*)
20.396 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
20.397 -val SOME t = parseNEW @{context} "1 + 2";
20.398 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
20.399 -if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
20.400 -then () else error "adhoc_thm 1 + 2 changed";
20.401 -
20.402 -(*--------------------------------------------------------------------vvvvvvvvvv*)
20.403 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
20.404 -val SOME t = parseNEW @{context} "6 / -8";
20.405 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
20.406 -if str = "#divide_e6_-8" andalso ThmC_Def.string_of_thm thm = "6 / -8 = -3 / 4"
20.407 -then () else error "adhoc_thm 1 + 2 changed";
20.408 -
20.409 -
20.410 -case assoc_calc thy "Prog_Expr.ident" of
20.411 - "ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
20.412 -(*--------------------------------------------------------------------vvvvvvvvvv*)
20.413 -val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
20.414 -
20.415 -val SOME t = parseNEW @{context} "3 =!= 3";
20.416 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
20.417 -if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
20.418 -then () else error "adhoc_thm (3 =!= 3) changed";
20.419 -
20.420 -val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)";
20.421 -val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
20.422 -if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
20.423 -then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
20.424 -
20.425 -"----------- fun power -------------------------------------------------------------------------";
20.426 -"----------- fun power -------------------------------------------------------------------------";
20.427 -"----------- fun power -------------------------------------------------------------------------";
20.428 -if power 2 3 = 8 then () else error "power 2 3 = 8";
20.429 -if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";
20.430 -if power ~3 2 = 9 then () else error "power ~3 2 = 9";
20.431 -(power 3 ~2; error "power 3 ~2: should raise an exn") handle _ => 000;
20.432 -
20.433 -"----------- fun divisors ----------------------------------------------------------------------";
20.434 -"----------- fun divisors ----------------------------------------------------------------------";
20.435 -"----------- fun divisors ----------------------------------------------------------------------";
20.436 -if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]";
20.437 -if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]";
20.438 -if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]";
20.439 -if divisors 11 = [11] then () else error "divisors 11 = [11]";
20.440 -
20.441 -"----------- fun doubles, fun squfact ----------------------------------------------------------";
20.442 -"----------- fun doubles, fun squfact ----------------------------------------------------------";
20.443 -"----------- fun doubles, fun squfact ----------------------------------------------------------";
20.444 -if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed";
20.445 -if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed";
20.446 -
20.447 -if squfact 30 = 1 then () else error "squfact 30 changed";
20.448 -if squfact 32 = 4 then () else error "squfact 32 changed";
20.449 -if squfact 60 = 2 then () else error "squfact 60 changed";
20.450 -if squfact 11 = 1 then () else error "squfact 11 changed";
21.1 --- a/test/Tools/isac/ProgLang/calculate.thy Wed Apr 22 11:06:48 2020 +0200
21.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Wed Apr 22 11:23:30 2020 +0200
21.3 @@ -8,7 +8,7 @@
21.4
21.5 text \<open>
21.6 *setup* KEStore_Elems.add_pbts / add_mets is impossible in *.sml files.
21.7 - The respective test/../calculate.sml is called in Test_Isac.thy.
21.8 + The respective test/../evaluate.sml is called in Test_Isac.thy.
21.9 \<close>
21.10
21.11 ML \<open>
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Wed Apr 22 11:23:30 2020 +0200
22.3 @@ -0,0 +1,447 @@
22.4 +(* Title: "ProgLang/evaluate.sml"
22.5 + test calculation of values for function constants
22.6 + Author: Walther Neuper 2000
22.7 + (c) copyright due to lincense terms.
22.8 +*)
22.9 +
22.10 +"--------------------------------------------------------";
22.11 +"table of contents --------------------------------------";
22.12 +"--------------------------------------------------------";
22.13 +"-calculate.thy: provides 'setup' -----------------------";
22.14 +"----------- fun norm -----------------------------------";
22.15 +"----------- check return value of adhoc_thm ----";
22.16 +"----------- fun calculate_ --------------------------------------------------------------------";
22.17 +"----------- calculate from Prog --------------------------------- -----------------------------";
22.18 +"----------- calculate from script --requires 'setup'----";
22.19 +"----------- calculate check test-root-equ --------------";
22.20 +"----------- check calcul,ate bottom up -----------------";
22.21 +"----------- Prog_Expr.pow Power.power_class.power ---------";
22.22 +" ================= evaluate.sml: calculate_ 2002 ======";
22.23 +"----------- get_pair with 3 args -----------------------";
22.24 +"----------- calculate (2 * x is_const) -----------------";
22.25 +"----------- fun get_pair: examples ------------------------------------------------------------";
22.26 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
22.27 +"----------- fun power -------------------------------------------------------------------------";
22.28 +"----------- fun divisors ----------------------------------------------------------------------";
22.29 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
22.30 +"--------------------------------------------------------";
22.31 +"--------------------------------------------------------";
22.32 +"--------------------------------------------------------";
22.33 +
22.34 +"----------- check return value of adhoc_thm ----";
22.35 +"----------- check return value of adhoc_thm ----";
22.36 +"----------- check return value of adhoc_thm ----";
22.37 +val thy = @{theory "Poly"};
22.38 +val cal = snd (assoc_calc' thy "is_polyexp");
22.39 +val t = @{term "(x / x) is_polyexp"};
22.40 +val SOME (thmID, thm) = adhoc_thm thy cal t;
22.41 +(HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
22.42 +handle TERM _ =>
22.43 + error "evaluate.sml: adhoc_thm must return Trueprop";
22.44 +
22.45 +"----------- fun calculate_ --------------------------------------------------------------------";
22.46 +"----------- fun calculate_ --------------------------------------------------------------------";
22.47 +"----------- fun calculate_ --------------------------------------------------------------------";
22.48 +(* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
22.49 +val t = str2term "((1+2)*4/3)^^^2";
22.50 +val thy = @{theory};
22.51 +val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Exec_Def.eval_fn;
22.52 +val plus = ("Groups.plus_class.plus",eval_binop "#add_") : string * Exec_Def.eval_fn;
22.53 +val divide = ("Rings.divide_class.divide" ,eval_cancel "#divide_e") : string * Exec_Def.eval_fn;
22.54 +val pow = ("Prog_Expr.pow" ,eval_binop "#power_") : string * Exec_Def.eval_fn;
22.55 +
22.56 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, plus, t);
22.57 +val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
22.58 +val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
22.59 +if UnparseC.term t' = "(3 * 4 / 3) ^^^ 2" then () else error "calculate_ 1 + 2 = 3 changed";
22.60 +
22.61 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
22.62 +val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
22.63 +val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
22.64 +if UnparseC.term t'' = "(12 / 3) ^^^ 2" then () else error "calculate_ 3 * 4 = 12 changed";
22.65 +
22.66 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
22.67 +val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
22.68 +val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
22.69 +if UnparseC.term t''' = "4 ^^^ 2" then () else error "calculate_ 12 / 3 = 4 changed";
22.70 +
22.71 +"~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
22.72 +val SOME ("#: 4 ^^^ 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
22.73 +val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
22.74 +if UnparseC.term t'''' = "16" then () else error "calculate_ 12 / 3 = 4 changed";
22.75 +
22.76 +"----------- calculate from Prog --------------------------------- -----------------------------";
22.77 +"----------- calculate from Prog --------------------------------- -----------------------------";
22.78 +"----------- calculate from Prog --------------------------------- -----------------------------";
22.79 +val thy = @{theory "Test"};
22.80 +val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
22.81 +val (dI',pI',mI') =
22.82 + ("Test",["calculate","test"],["Test","test_calculate"]);
22.83 +
22.84 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
22.85 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.86 +(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*)
22.87 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.88 +(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
22.89 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.90 +(*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
22.91 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.92 +(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
22.93 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.94 +(*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
22.95 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
22.96 +(*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
22.97 +
22.98 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*)
22.99 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*)
22.100 +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*)
22.101 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*)
22.102 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
22.103 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*)
22.104 +case f of FormKF "16" => () | _ =>
22.105 +error "evaluate.sml: script test_calculate changed behaviour";
22.106 +
22.107 +
22.108 +"----------- calculate check test-root-equ --------------";
22.109 +"----------- calculate check test-root-equ --------------";
22.110 +"----------- calculate check test-root-equ --------------";
22.111 +(*(1): 2nd Test_simplify didn't work:
22.112 +val ct =
22.113 + "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
22.114 +> val rls = ("Test_simplify");
22.115 +> val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
22.116 +val ct = "sqrt (x ^^^ 2 + -3 * x) =
22.117 +(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
22.118 +ie. cancel does not work properly
22.119 +*)
22.120 + val thy = @{theory "Test"};
22.121 + val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
22.122 + val ct = ThmC_Def.num_to_Free @{term
22.123 + "sqrt (x ^^^ 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
22.124 +case calculate_ thy op_ ct of
22.125 + SOME _ => ()
22.126 +| NONE => error "calculate_ test-root-equ changed";
22.127 +(*
22.128 + sqrt (x ^^^ 2 + -3 * x) =\
22.129 + \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
22.130 +............... does not work *)
22.131 +
22.132 +(*--------------(2): does divide work in Test_simplify ?: ------*)
22.133 + val thy = @{theory Test};
22.134 + val t = (Thm.term_of o the o (parse thy)) "6 / 2";
22.135 + val rls = Test_simplify;
22.136 + val (t,_) = the (rewrite_set_ thy false rls t);
22.137 +(*val t = Free ("3","Real.real") : term*)
22.138 +
22.139 +(*--------------(3): is_const works ?: -------------------------------------*)
22.140 + val t = (Thm.term_of o the o (parse @{theory Test})) "2 is_const";
22.141 + atomty t;
22.142 + rewrite_set_ @{theory Test} false tval_rls t;
22.143 +(*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
22.144 +
22.145 + val t = str2term "2 * x is_const";
22.146 + val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
22.147 + UnparseC.term t';
22.148 +
22.149 +
22.150 +"----------- check calculate bottom up ------------------";
22.151 +"----------- check calculate bottom up ------------------";
22.152 +"----------- check calculate bottom up ------------------";
22.153 +(*-------------- eval_cancel works: *)
22.154 + Rewrite.trace_on := false;
22.155 + val thy = @{theory Test};
22.156 + val rls = Test_simplify;
22.157 + val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
22.158 +
22.159 +val SOME (_, t) = eval_cancel "xxx" "Rings.divide_class.divide" t thy;
22.160 +
22.161 +(*--------------(5): reproduce (1) with simpler term: ------------*)
22.162 + val t = (Thm.term_of o the o (parse thy)) "(3+5)/2";
22.163 +case rewrite_set_ thy false rls t of
22.164 + SOME (Free ("4", _), []) => ()
22.165 +| _ => error "rewrite_set_ (3+5)/2 changed";
22.166 +
22.167 + val t = (Thm.term_of o the o (parse thy)) "(3+1+2*x)/2";
22.168 +case rewrite_set_ thy false rls t of
22.169 + SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
22.170 +| _ => error "rewrite_set_ (3+1+2*x)/2 changed";
22.171 +
22.172 + Rewrite.trace_on:=false; (*=true3.6.03*)
22.173 +
22.174 +(*--- Rewrite.trace_on before correction of ... --------------------
22.175 + val ct = "(-3 + 2 * x + -1) / 2";
22.176 + val (ct,_) = the (rewrite_set thy' false rls ct);
22.177 +:
22.178 +### trying thm 'root_ge0_2'
22.179 +### rewrite_set_: x + (-1 + -3) / 2
22.180 +### trying thm 'radd_real_const_eq'
22.181 +### trying thm 'radd_real_const'
22.182 +### rewrite_set_: x + (-4) / 2
22.183 +### trying thm 'rcollect_right'
22.184 +:
22.185 +"x + (-4) / 2"
22.186 +-------------------------------------while before Isabelle20002:
22.187 + val ct = "(#-3 + #2 * x + #-1) // #2";
22.188 + val (ct,_) = the (rewrite_set thy' false rls ct);
22.189 +:
22.190 +### trying thm 'root_ge0_2'
22.191 +### rewrite_set_: x + (#-1 + #-3) // #2
22.192 +### trying thm 'radd_real_const_eq'
22.193 +### trying thm 'radd_real_const'
22.194 +### rewrite_set_: x + #-4 // #2
22.195 +### rewrite_set_: x + #-2
22.196 +### trying thm 'rcollect_right'
22.197 +:
22.198 +"#-2 + x"
22.199 +-----------------------------------------------------------------*)
22.200 +
22.201 +
22.202 +(*===================*)
22.203 + Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
22.204 + val t = (Thm.term_of o the o (parse thy)) "x + (-1 + -3) / 2";
22.205 +val SOME (res, []) = rewrite_set_ thy false rls t;
22.206 +if UnparseC.term res = "-2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
22.207 +"x + (-4) / 2";
22.208 +(*
22.209 +### trying calc. 'cancel'
22.210 +@@@ get_pair: binop, t = x + (-4) / 2
22.211 +@@@ get_pair: t else
22.212 +@@@ get_pair: t else -> NONE
22.213 +@@@ get_pair: binop, t = (-4) / 2
22.214 +@@@ get_pair: then 1
22.215 +@@@ get_pair: t -> NONE
22.216 +@@@ get_pair: t1 -> NONE
22.217 +@@@ adhoc_thm': NONE
22.218 +### trying calc. 'pow'
22.219 +*)
22.220 +
22.221 + Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
22.222 +
22.223 +"----------- Prog_Expr.pow Power.power_class.power ---------";
22.224 +"----------- Prog_Expr.pow Power.power_class.power ---------";
22.225 +"----------- Prog_Expr.pow Power.power_class.power ---------";
22.226 +val t = (Thm.term_of o the o (parseold thy)) "1 ^ aaa";
22.227 +atomty t;
22.228 +(*** -------------
22.229 +*** Const ( Nat.power, ['a, nat] => 'a)
22.230 +*** . Free ( 1, 'a)
22.231 +*** . Free ( aaa, nat) *)
22.232 +
22.233 +val t = str2term "1 ^^^ aaa";
22.234 +atomty t;
22.235 +(****
22.236 +*** Const (Prog_Expr.pow, real => real => real)
22.237 +*** . Free (1, real)
22.238 +*** . Free (aaa, real)
22.239 +*** *);
22.240 +
22.241 +" ================= evaluate.sml: calculate_ 2002 =================== ";
22.242 +" ================= evaluate.sml: calculate_ 2002 =================== ";
22.243 +" ================= evaluate.sml: calculate_ 2002 =================== ";
22.244 +
22.245 +val thy = @{theory Test};
22.246 +val t = (Thm.term_of o the o (parse thy)) "12 / 3";
22.247 +val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
22.248 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.249 +"12 / 3 = 4";
22.250 +val thy = @{theory Test};
22.251 +val t = (Thm.term_of o the o (parse thy)) "4 ^^^ 2";
22.252 +val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
22.253 +val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.254 +"4 ^ 2 = 16";
22.255 +
22.256 + val t = (Thm.term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
22.257 + val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
22.258 +"1 + 2 = 3";
22.259 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.260 + UnparseC.term t;
22.261 +"(3 * 4 / 3) ^^^ 2";
22.262 + val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
22.263 +"3 * 4 = 12";
22.264 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.265 + UnparseC.term t;
22.266 +"(12 / 3) ^^^ 2";
22.267 + val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
22.268 +"12 / 3 = 4";
22.269 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.270 + UnparseC.term t;
22.271 +"4 ^^^ 2";
22.272 + val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
22.273 +"4 ^^^ 2 = 16";
22.274 + val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
22.275 + UnparseC.term t;
22.276 +"16";
22.277 + if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
22.278 + else ();
22.279 +
22.280 +(*13.9.02 *** calc: operator = pow not defined*)
22.281 + val t = (Thm.term_of o the o (parse thy)) "3^^^2";
22.282 + val SOME (thmID,thm) =
22.283 + adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
22.284 +(*** calc: operator = pow not defined*)
22.285 +
22.286 + val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
22.287 + (*
22.288 +val op_ = "Prog_Expr.pow" : string
22.289 +val eval_fn = fn : string -> term -> theory -> (string * term) option*)
22.290 +
22.291 + val SOME (thmid,t') = get_pair thy op_ eval_fn t;
22.292 +(*** calc: operator = pow not defined*)
22.293 +
22.294 + val SOME (id,t') = eval_fn op_ t thy;
22.295 +(*** calc: operator = pow not defined*)
22.296 +
22.297 + val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
22.298 + val SOME (id,t') = eval_binop thmid op_ t thy;
22.299 +(*** calc: operator = pow not defined*)
22.300 +
22.301 +
22.302 +"----------- get_pair with 3 args --------------------------------";
22.303 +"----------- get_pair with 3 args --------------------------------";
22.304 +"----------- get_pair with 3 args --------------------------------";
22.305 +val (thy, op_, ef, arg) =
22.306 + (thy, "EqSystem.occur'_exactly'_in",
22.307 + assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
22.308 + str2term
22.309 + "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
22.310 + );
22.311 +val SOME (str, simpl) = get_pair thy op_ ef arg;
22.312 +if str =
22.313 +"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
22.314 +then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
22.315 +
22.316 +
22.317 +"----------- calculate (2 * x is_const) -----------------";
22.318 +"----------- calculate (2 * x is_const) -----------------";
22.319 +"----------- calculate (2 * x is_const) -----------------";
22.320 +val t = str2term "2 * x is_const";
22.321 +val SOME (str, t') = eval_const "" "" t @{theory Test};
22.322 +UnparseC.term t';
22.323 +"(2 * x is_const) = False";
22.324 +
22.325 +val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
22.326 +UnparseC.term t';
22.327 +"HOL.False";
22.328 +
22.329 +"----------- fun get_pair: examples ------------------------------------------------------------";
22.330 +"----------- fun get_pair: examples ------------------------------------------------------------";
22.331 +"----------- fun get_pair: examples ------------------------------------------------------------";
22.332 +val thy = @{theory};
22.333 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
22.334 +
22.335 +val t = (Thm.term_of o the o (parse thy)) "3 + 4";
22.336 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.337 +if str = "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
22.338 +then () else error "get_pair 3 + 4 changed";
22.339 +
22.340 +val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
22.341 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.342 +if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
22.343 +then () else error "get_pair (a + 3) + 4 changed";
22.344 +
22.345 +val t = (Thm.term_of o the o (parse thy)) "(a + 3) + 4";
22.346 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.347 +if str = "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
22.348 +then () else error "get_pair (a + 3) + 4 changed";
22.349 +
22.350 +val t = (Thm.term_of o the o (parse thy)) "x = 5 * (3 + (4 + a))";
22.351 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.352 +if str = "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
22.353 +then ((* !!! gets subterm !!!*)) else error "get_pair x = 5 * (3 + (4 + a)) (subterm) changed";
22.354 +
22.355 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
22.356 +
22.357 +val t = (Thm.term_of o the o (parse thy)) "-4 / -2";
22.358 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.359 +if str = "#divide_e-4_-2" andalso UnparseC.term term = "-4 / -2 = 2"
22.360 +then () else error "get_pair -4 / -2 changed";
22.361 +
22.362 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
22.363 +
22.364 +val t = (Thm.term_of o the o (parse thy)) "2 ^^^ 3";
22.365 +val SOME (str, term) = get_pair thy isa_str eval_fn t;
22.366 +if str = "#: 2 ^^^ 3 = 8" andalso UnparseC.term term = "2 ^^^ 3 = 8"
22.367 +then () else error "get_pair 2 ^^^ 3 changed";
22.368 +
22.369 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
22.370 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
22.371 +"----------- fun adhoc_thm: examples -----------------------------------------------------------";
22.372 +(*--------------------------------------------------------------------vvvvvvvvvv*)
22.373 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
22.374 +val SOME t = parseNEW @{context} "9 is_const";
22.375 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.376 +if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
22.377 +then () else error "adhoc_thm 9 is_const changed";
22.378 +
22.379 +
22.380 +case assoc_calc thy "Orderings.ord_class.less" of
22.381 + "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
22.382 +(*--------------------------------------------------------------------vvvvvvvvvv*)
22.383 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
22.384 +
22.385 +val SOME t = parseNEW @{context} "4 < 4";
22.386 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.387 +if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
22.388 +then () else error "adhoc_thm 4 < 4 changed";
22.389 +
22.390 +val SOME t = parseNEW @{context} "a < 4";
22.391 +case adhoc_thm thy (isa_str, eval_fn) t of
22.392 +NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE";
22.393 +
22.394 +
22.395 +(*--------------------------------------------------------------------vvvvvvvvvv*)
22.396 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
22.397 +val SOME t = parseNEW @{context} "1 + 2";
22.398 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.399 +if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
22.400 +then () else error "adhoc_thm 1 + 2 changed";
22.401 +
22.402 +(*--------------------------------------------------------------------vvvvvvvvvv*)
22.403 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
22.404 +val SOME t = parseNEW @{context} "6 / -8";
22.405 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.406 +if str = "#divide_e6_-8" andalso ThmC_Def.string_of_thm thm = "6 / -8 = -3 / 4"
22.407 +then () else error "adhoc_thm 1 + 2 changed";
22.408 +
22.409 +
22.410 +case assoc_calc thy "Prog_Expr.ident" of
22.411 + "ident" => () | _ => error "Prog_Expr.ident <-> ident changed";
22.412 +(*--------------------------------------------------------------------vvvvvvvvvv*)
22.413 +val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
22.414 +
22.415 +val SOME t = parseNEW @{context} "3 =!= 3";
22.416 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.417 +if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
22.418 +then () else error "adhoc_thm (3 =!= 3) changed";
22.419 +
22.420 +val SOME t = parseNEW @{context} "\<not> (4 + (4 * x + x ^ 2) =!= 0)";
22.421 +val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
22.422 +if str = "#ident_(4 + (4 * x + x ^ 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x ^ 2) =!= 0) = False"
22.423 +then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
22.424 +
22.425 +"----------- fun power -------------------------------------------------------------------------";
22.426 +"----------- fun power -------------------------------------------------------------------------";
22.427 +"----------- fun power -------------------------------------------------------------------------";
22.428 +if power 2 3 = 8 then () else error "power 2 3 = 8";
22.429 +if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";
22.430 +if power ~3 2 = 9 then () else error "power ~3 2 = 9";
22.431 +(power 3 ~2; error "power 3 ~2: should raise an exn") handle _ => 000;
22.432 +
22.433 +"----------- fun divisors ----------------------------------------------------------------------";
22.434 +"----------- fun divisors ----------------------------------------------------------------------";
22.435 +"----------- fun divisors ----------------------------------------------------------------------";
22.436 +if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]";
22.437 +if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]";
22.438 +if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]";
22.439 +if divisors 11 = [11] then () else error "divisors 11 = [11]";
22.440 +
22.441 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
22.442 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
22.443 +"----------- fun doubles, fun squfact ----------------------------------------------------------";
22.444 +if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed";
22.445 +if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed";
22.446 +
22.447 +if squfact 30 = 1 then () else error "squfact 30 changed";
22.448 +if squfact 32 = 4 then () else error "squfact 32 changed";
22.449 +if squfact 60 = 2 then () else error "squfact 60 changed";
22.450 +if squfact 11 = 1 then () else error "squfact 11 changed";
23.1 --- a/test/Tools/isac/Test_Isac.thy Wed Apr 22 11:06:48 2020 +0200
23.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 22 11:23:30 2020 +0200
23.3 @@ -73,7 +73,7 @@
23.4 "~~/test/Pure/Isar/Test_Parse_Term"
23.5 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
23.6 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
23.7 - "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
23.8 + "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml*)
23.9 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
23.10 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
23.11 "~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
23.12 @@ -195,7 +195,7 @@
23.13 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
23.14 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
23.15 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
23.16 - ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
23.17 + ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
23.18 ML_file "ProgLang/listC.sml"
23.19 ML_file "ProgLang/prog_expr.sml"
23.20 ML_file "ProgLang/program.sml"
24.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Apr 22 11:06:48 2020 +0200
24.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Apr 22 11:23:30 2020 +0200
24.3 @@ -73,7 +73,7 @@
24.4 "~~/test/Pure/Isar/Test_Parse_Term"
24.5 (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)
24.6 "~~/test/Tools/isac/Interpret/ptyps" (* setup for ptyps.sml *)
24.7 - "~~/test/Tools/isac/ProgLang/calculate" (* setup for calculate.sml*)
24.8 + "~~/test/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml*)
24.9 "~~/test/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
24.10 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
24.11 (*"~~/src/Tools/isac/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
24.12 @@ -195,7 +195,7 @@
24.13 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
24.14 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
24.15 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
24.16 - ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *)
24.17 + ML_file "ProgLang/evaluate.sml" (* requires setup from calculate.thy *)
24.18 ML_file "ProgLang/listC.sml"
24.19 ML_file "ProgLang/prog_expr.sml"
24.20 ML_file "ProgLang/program.sml"