1.1 --- a/test/Tools/isac/Test_Isac.thy Tue May 03 11:16:55 2011 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Tue May 03 15:58:04 2011 +0200
1.3 @@ -68,10 +68,8 @@
1.4 ("Knowledge/diophanteq.sml")
1.5 ("Knowledge/isac.sml")
1.6
1.7 -
1.8 begin
1.9
1.10 - ML {*print_depth 100*}
1.11 ML {*"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";*}
1.12 use "library.sml" (*new 2011*)
1.13 use "calcelems.sml" (*complete*)
1.14 @@ -84,113 +82,13 @@
1.15 ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
1.16 ML {*"%%%%%%%%%%%%%%%%% start Interpret.thy %%%%%%%%%%%%%%%%%%";*}
1.17 use "Interpret/mstools.sml" (*empty*)
1.18 -
1.19 -ML {*print_depth 5;
1.20 -val fmz = ["equality (x+1=(2::real))", (*FIRST OF ALL TESTS*) "solveFor x", "solutions L"];
1.21 -val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
1.22 - ["Test","squ-equ-test-subpbl1"]);
1.23 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.24 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.25 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.27 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.29 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.31 -"----- fun me, args:"; val (_,tac) = nxt;
1.32 -"----- fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
1.33 -val (mI,m) = mk_tac'_ tac;
1.34 -val Appl m = applicable_in p pt m;
1.35 -member op = specsteps mI; (*false*)
1.36 -"----- fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
1.37 -"----- fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
1.38 -val {srls, ...} = get_met mI;
1.39 -val PblObj {meth=itms, ...} = get_obj I pt p;
1.40 -val thy' = get_obj g_domID pt p;
1.41 -val thy = assoc_thy thy';
1.42 -val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
1.43 -val ini = init_form thy sc env; (*NONE*)
1.44 -*}
1.45 -ML {*
1.46 -"----- fun init_form, args:"; val (Script sc) = sc;
1.47 -"----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
1.48 -*}
1.49 -ML {*
1.50 - fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a =
1.51 - (writeln "Script.Seq";
1.52 - case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.53 - | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ =
1.54 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.55 - | get_t y (Const ("Script.Try",_) $ e) a = (writeln "Script.Try 1";
1.56 - get_t y e a)
1.57 - | get_t y (Const ("Script.Try",_) $ e $ a) _ = (writeln "Script.Try 2";
1.58 - get_t y e a)
1.59 - | get_t y (Const ("Script.Repeat",_) $ e) a = get_t y e a
1.60 - | get_t y (Const ("Script.Repeat",_) $ e $ a) _ = get_t y e a
1.61 - | get_t y (Const ("Script.Or",_) $e1 $ e2) a =
1.62 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.63 - | get_t y (Const ("Script.Or",_) $e1 $ e2 $ a) _ =
1.64 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.65 - | get_t y (Const ("Script.While",_) $ c $ e) a = get_t y e a
1.66 - | get_t y (Const ("Script.While",_) $ c $ e $ a) _ = get_t y e a
1.67 - | get_t y (Const ("Script.Letpar",_) $ e1 $ Abs (_,_,e2)) a =
1.68 - (case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.69 - (*| get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.70 - (tracing("get_t: Let e1= "^(term2str e1)^", e2= "^(term2str e2));
1.71 - case get_t y e1 a of NONE => get_t y e2 a | la => la)
1.72 - | get_t y (Abs (_,_,e)) a = get_t y e a*)
1.73 - | get_t y (Const ("HOL.Let",_) $ e1 $ Abs (_,_,e2)) a =
1.74 - (writeln "HOL.Let";
1.75 - get_t y e1 a (*don't go deeper without evaluation !*))
1.76 - | get_t y (Const ("If",_) $ c $ e1 $ e2) a = NONE
1.77 - (*(case get_t y e1 a of NONE => get_t y e2 a | la => la)*)
1.78 -
1.79 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ $ a) _ = SOME a
1.80 - | get_t y (Const ("Script.Rewrite",_) $ _ $ _ ) a = SOME a
1.81 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ $ a) _ = SOME a
1.82 - | get_t y (Const ("Script.Rewrite'_Inst",_) $ _ $ _ $ _ ) a = SOME a
1.83 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ $ a) _ =
1.84 - (writeln "Script.Rewrite'_Set 1";
1.85 - SOME a)
1.86 - | get_t y (Const ("Script.Rewrite'_Set",_) $ _ $ _ ) a =
1.87 - (writeln "Script.Rewrite'_Set 2";
1.88 - SOME a)
1.89 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ $a)_ =SOME a
1.90 - | get_t y (Const ("Script.Rewrite'_Set'_Inst",_) $ _ $ _ $ _ ) a =SOME a
1.91 - | get_t y (Const ("Script.Calculate",_) $ _ $ a) _ = SOME a
1.92 - | get_t y (Const ("Script.Calculate",_) $ _ ) a = SOME a
1.93 -
1.94 - | get_t y (Const ("Script.Substitute",_) $ _ $ a) _ = SOME a
1.95 - | get_t y (Const ("Script.Substitute",_) $ _ ) a = SOME a
1.96 -
1.97 - | get_t y (Const ("Script.SubProblem",_) $ _ $ _) _ = NONE
1.98 -
1.99 - | get_t y x _ =
1.100 - ((*tracing ("### get_t yac: list-expr "^(term2str x));*)
1.101 - NONE);
1.102 -*}
1.103 -ML {*
1.104 -case get_t thy body e_term of SOME (Free ("e_e", _)) => ()
1.105 -| _ => error "script: Const in script (as term) changed";
1.106 -get_stac thy sc;
1.107 -(*========== inhibit exn 110323 ================================================
1.108 -print_depth 999; sc;
1.109 -val p = lev_dn p;
1.110 -val (m', (is', ctxt'), _) = next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.111 -val Check_Postcond' (_, (ttt,_)) = m';
1.112 -term2str ttt; (*is the whole script*)
1.113 -solve m (pt, pos);
1.114 -loc_solve_ (mI,m) ptp;
1.115 -locatetac tac (pt,p);
1.116 -============ inhibit exn 110loc_solve_ (mI,m) ptp323 ==============================================*)
1.117 -*}
1.118 use "Interpret/ctree.sml"
1.119 use "Interpret/ptyps.sml" (* *)
1.120 (*use "Interpret/generate.sml" new 2011*)
1.121 use "Interpret/calchead.sml" (* *)
1.122 (*use "Interpret/appl.sml" new 2011*)
1.123 use "Interpret/rewtools.sml" (* *)
1.124 -(*use "Interpret/script.sml" TODO*)
1.125 + use "Interpret/script.sml" (*TODO*)
1.126 (*use "Interpret/solve.sml" TODO*)
1.127 (*use "Interpret/inform.sml" TODO*)
1.128 use "Interpret/mathengine.sml"(*part.*)
1.129 @@ -249,12 +147,12 @@
1.130 (*=== inhibit exn ?=============================================================
1.131 ===== inhibit exn ?===========================================================*)
1.132
1.133 -(*========== inhibit exn 110323 ================================================
1.134 +(*========== inhibit exn 110503 ================================================
1.135
1.136 "########### testcode inserted vvv ###########################################";
1.137 "########### testcode inserted ^^^ ###########################################";
1.138
1.139 -============ inhibit exn 110323 ==============================================*)
1.140 +============ inhibit exn 110503 ==============================================*)
1.141
1.142 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.143 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)