1.1 --- a/src/Pure/library.ML Wed Jul 13 10:41:17 2011 +0200
1.2 +++ b/src/Pure/library.ML Thu Jul 14 09:33:57 2011 +0200
1.3 @@ -125,7 +125,8 @@
1.4 val string_of_int: int -> string
1.5 val signed_string_of_int: int -> string
1.6 val string_of_indexname: string * int -> string
1.7 - val read_radix_int: int -> string list -> int * string list
1.8 + val read_radix_int: int -> string list -> int * strinmember (op=) [1,2,3,4,5]
1.9 +g list
1.10 val read_int: string list -> int * string list
1.11 val oct_char: string -> string
1.12
2.1 --- a/src/Tools/isac/Interpret/mathengine.sml Wed Jul 13 10:41:17 2011 +0200
2.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Jul 14 09:33:57 2011 +0200
2.3 @@ -230,7 +230,7 @@
2.4 in if str = "ok"
2.5 then autocalc (c@c') p (ptp,[]) (Step (s-1))
2.6 else (str, c@c', ptp) end
2.7 -(*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
2.8 +(* handles autoord <= 3, autoord > 3 handled by all_/complete_solve *)
2.9 | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto =
2.10 if autoord auto > 3 andalso just_created (pt, pos)
2.11 then let val ptp = all_modspec (pt, pos);
3.1 --- a/src/Tools/isac/Interpret/script.sml Wed Jul 13 10:41:17 2011 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Jul 14 09:33:57 2011 +0200
3.3 @@ -1590,7 +1590,7 @@
3.4 (*3*) from rls/PrfObj: in case of detail a ruleset *)
3.5 fun from_pblobj_or_detail' thy' (p,p_) pt =
3.6 let val ctxt = get_ctxt pt (p,p_)
3.7 - in
3.8 + in
3.9 if member op = [Pbl,Met] p_
3.10 then case get_obj g_env pt p of
3.11 NONE => error "from_pblobj_or_detail': no istate"
3.12 @@ -1618,7 +1618,7 @@
3.13 Rls {scr=scr,...} => scr
3.14 | Seq {scr=scr,...} => scr
3.15 | Rrls {scr=rfuns,...} => rfuns)
3.16 - end
3.17 + end
3.18 end;
3.19
3.20 (*.get script and istate from PblObj, see (*1*) above.*)
4.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy Wed Jul 13 10:41:17 2011 +0200
4.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy Thu Jul 14 09:33:57 2011 +0200
4.3 @@ -52,7 +52,4 @@
4.4 val fi :: _ = l1;
4.5 *}
4.6
4.7 -section {* 3 Defining functions *}
4.8 -text {* see src/Pure/library.ML *}
4.9 -
4.10 end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML2_Functions.thy Thu Jul 14 09:33:57 2011 +0200
5.3 @@ -0,0 +1,124 @@
5.4 +header {* Quick introduction to ML, session 2 *}
5.5 +theory ML2_Functions imports Isac begin
5.6 +
5.7 +text{*
5.8 +This course follows the book:
5.9 +J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
5.10 +Contents:
5.11 +
5.12 +section {* 3.1 Functions *}
5.13 +ML {*
5.14 +fun add x y = x + y;
5.15 +add 2 3;
5.16 +add 3 4;
5.17 +fun mult x y = x * y;
5.18 +mult 2 3;
5.19 +*}
5.20 +ML {*
5.21 +val plus3 = add 3;
5.22 +plus3 4;
5.23 +*}
5.24 +ML {*
5.25 +fun calc op_ x y = op_ (x, y);
5.26 +*}
5.27 +ML {*
5.28 +op+
5.29 +*}
5.30 +ML {*
5.31 +val op_ = op +;
5.32 +val add' = calc op_;
5.33 +add' 3 4;
5.34 +*}
5.35 +ML {*
5.36 +val op_ = op *;
5.37 +val add' = calc op_;
5.38 +add' 3 4;
5.39 +*}
5.40 +
5.41 +section {* 3.2 Recursive Functions *}
5.42 +ML {*
5.43 +fun print [] = "";
5.44 +print [];
5.45 +(*print [1,2,3] exception Match raised*)
5.46 +*}
5.47 +ML {*
5.48 +fun print [] = ""
5.49 + | print (x :: xs) = "123"; (*Value identifier x,(xs) has not been referenced. *)
5.50 +print [];
5.51 +print [1,2,3];
5.52 +print [1,2,3,4,5,6,7]
5.53 +*}
5.54 +ML {*
5.55 +fun print [] = ""
5.56 + | print (_ :: _) = "123";
5.57 +print [];
5.58 +print [1,2,3,4,5,6,7]
5.59 +*}
5.60 +ML {*
5.61 +fun print [] = "]"
5.62 + | print (x :: xs) = (string_of_int x) ^ ", " ^ print xs;
5.63 +print [];
5.64 +print [1,2,3];
5.65 +print [1,2,3,4,5,6,7]
5.66 +*}
5.67 +ML {*
5.68 +fun print [] = (writeln "print []: "; "]")
5.69 + | print (x :: xs) =
5.70 + (writeln "print (x :: xs): x = "; (string_of_int x) ^ ", " ^
5.71 + (writeln (string_of_int x); print xs));
5.72 +*}
5.73 +ML {*
5.74 +print [];
5.75 +print [1,2,3];
5.76 +*}
5.77 +ML {*
5.78 +1;
5.79 +"xcv";
5.80 +writeln "asd";
5.81 +*}
5.82 +section {* see src/Pure/library.ML, lists as sets *}
5.83 +ML {*
5.84 +member;
5.85 +member op = [1,2,3,4,5] 3;
5.86 +member op = [1,2,3,4,5] 7;
5.87 +*}
5.88 +ML {*
5.89 +insert;
5.90 +Library.insert;
5.91 +fun insert eq x xs = if member eq xs x then xs else x :: xs;
5.92 +*}
5.93 +ML {*
5.94 +insert op = 1 [1,2,3];
5.95 +insert op = 4 [1,2,3];
5.96 +*}
5.97 +ML {*
5.98 +insert;
5.99 +Library.insert;
5.100 +fun insert eq x xs =
5.101 + if member eq xs x
5.102 + then (writeln "then"; xs)
5.103 + else (writeln "else"; x :: xs);
5.104 +insert op = 1 [1,2,3];
5.105 +insert op = 4 [1,2,3];
5.106 +*}
5.107 +
5.108 +ML {*
5.109 +merge;
5.110 +*}
5.111 +
5.112 +ML {*
5.113 +merge op = ([], []);
5.114 +merge op = ([1,2], []);
5.115 +merge op = ([], [4,5]);
5.116 +merge op = ([1,2], [4,5]);
5.117 +merge op = ([3,4], [4,5]);
5.118 +*}
5.119 +
5.120 +ML {*
5.121 +union;
5.122 +*}
5.123 +
5.124 +ML {*
5.125 +union op = [3,4] [4,5];
5.126 +*}
5.127 +end
6.1 --- a/test/Tools/isac/Test_Isac.thy Wed Jul 13 10:41:17 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Jul 14 09:33:57 2011 +0200
6.3 @@ -138,30 +138,89 @@
6.4 ["Test","squ-equ-test-subpbl1"]))];
6.5 Iterator 1;
6.6 moveActiveRoot 1;
6.7 +(*autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)*)
6.8 "~~~~~ fun autoCalculate, args:"; val (cI, auto) = (1, CompleteCalc);
6.9 val pold = get_pos cI 1;
6.10 +(*autocalc [] pold (get_calc cI) auto; (*WAS Type unification failed
6.11 + Type error in application: incompatible operand type
6.12 + Operator: solveFor :: real \<Rightarrow> una
6.13 + Operand: x :: 'a *)*)
6.14 "~~~~~ fun autocalc, args:"; val (c, (pos as (_,p_)), ((pt,_), _), auto)
6.15 = ([] : pos' list, pold, (get_calc cI), auto);
6.16 autoord auto > 3 andalso just_created (pt, pos); (*true*)
6.17 val ptp = all_modspec (pt, pos);
6.18 -"~~~~~ fun autoCalculate, args:"; val () = ();
6.19 +(*all_solve auto c ptp; (*WAS Type unification failed...*)*)
6.20 +"~~~~~ and all_solve, args:"; val (auto, c, (ptp as (pt, pos as (p,_)))) = (auto, c, ptp);
6.21 + val (_,_,mI) = get_obj g_spec pt p
6.22 + val ctxt = get_ctxt pt pos
6.23 + val (_, c', ptp) = nxt_solv (Apply_Method' (mI, NONE, e_istate, ctxt))
6.24 + (e_istate, ctxt) ptp;
6.25 +(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*) pos = ([], Met)*)
6.26 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p))) = (auto, (c @ c'), ptp);
6.27 +p = ([], Res) (*false p = ([1], Frm)*);
6.28 +val (_, c', ptp') = nxt_solve_ ptp;
6.29 +(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*)*)
6.30 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p))) = (auto, (c @ c'), ptp');
6.31 +p = ([], Res) (*false p = ([1], Res)*);
6.32 +val (_, c', ptp') = nxt_solve_ ptp;
6.33 +(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*)*)
6.34 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p))) = (auto, (c @ c'), ptp');
6.35 +p = ([], Res) (*false p = ([2], Res)*);
6.36 +val (_, c', ptp') = nxt_solve_ ptp;
6.37 +(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*)*)
6.38 +"~~~~~ fun complete_solve, args:"; val (auto, c, (ptp as (_, p))) = (auto, (c @ c'), ptp');
6.39 +p = ([], Res) (*false p = ([3], Pbl)*);
6.40 +(*val ((Subproblem _, tac_, (_, is))::_, c', ptp') = nxt_solve_ ptp;
6.41 +(*from_pblobj_or_detail': no istate*)*)
6.42 +
6.43 +(* complete_solve auto (c @ c') ptp; (*WAS Type unification failed...*)*)
6.44 +*}
6.45 +ML {*
6.46 +p
6.47 *}
6.48 ML {*
6.49 *}
6.50 ML {*
6.51 -
6.52 +"~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p,p_))) = (ptp);
6.53 +e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
6.54 + val thy' = get_obj g_domID pt (par_pblobj pt p);
6.55 +*}
6.56 +ML {*
6.57 +"~~~~~ fun from_pblobj_or_detail', args:"; val (thy', (p,p_), pt) = (thy', (p,p_), pt);
6.58 +val ctxt = get_ctxt pt (p,p_);
6.59 +member op = [Pbl,Met] p_ (*true*);
6.60 +get_obj g_env pt p
6.61 +*}
6.62 +ML {*
6.63 +(p,p_)
6.64 +*}
6.65 +ML {*
6.66 +*}
6.67 +ML {*
6.68 +*}
6.69 +ML {*
6.70 +*}
6.71 +ML {*
6.72 *}
6.73 ML {*
6.74 *}
6.75 ML {*
6.76 *}
6.77 ML {*
6.78 -(*
6.79 -all_solve auto c ptp; (*Type unification failed
6.80 +print_depth 999;
6.81 +(*
6.82 +val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*from_pblobj_or_detail': no istate*)
6.83 +
6.84 +val (_, c', ptp') = nxt_solve_ ptp; (*from_pblobj_or_detail': no istate*)
6.85 +...
6.86 +complete_solve auto (c @ c') ptp
6.87 + -"-
6.88 +all_solve auto c ptp;
6.89 + -"-
6.90 +autocalc [] pold (get_calc cI) auto; (*Type unification failed
6.91 Type error in application: incompatible operand type
6.92 Operator: solveFor :: real \<Rightarrow> una
6.93 Operand: x :: 'a *)
6.94 -autocalc [] pold (get_calc cI) auto; (*Type unification failed...*)
6.95 autoCalculate 1 CompleteCalc; (*WAS <SYSERROR>..<ERROR> error in kernel </ERROR>*)
6.96 *)
6.97 *}