1 (* Title: 200-start-method.sml
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/200-start-method.sml ---------------------";
7 "----------- Minisubplb/200-start-method.sml ---------------------";
8 "----------- Minisubplb/200-start-method.sml ---------------------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11 ("Test", ["sqroot-test","univariate","equation","test"],
12 ["Test","squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Problem",..*)
19 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
20 val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (* (@1) nxt'''' = ("Specify_Method",..*)
21 (*me nxt'''' p'''' [] pt''''; "ERROR in creating the environment..", SHOULD BE("Apply_Method",.*)
22 "~~~~~ we continue with (@1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
23 val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
24 "~~~~~ fun me, args:"; val (_,tac) = nxt;
26 (*locatetac is here for testing by me; step would suffice in me*)
27 case locatetac tac (pt,p) of
28 ("ok", (_, _, ptp)) => ptp | _ => error "CHANGED --- Minisubplb/200-start-method 1"
29 (* step p ((pt, e_pos'),[]) ..ERROR = ("helpless",*)
30 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
31 (p, ((pt, e_pos'),[]));
32 val pIopt = get_pblID (pt,ip);
33 ip = ([],Res) (*= false*);
36 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)) (*= true*);
37 (*nxt_specify_ (pt, ip) ..ERROR in creating the environment..*);
39 val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
40 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
41 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* (@2) nxt = ("Apply_Method",..*)
42 val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (*ERROR WAS nxt = ("Empty_Tac",..*)
43 "~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
44 "~~~~~ fun me, args:"; val (_,tac) = nxt;
45 "~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p);
46 val (mI,m) = mk_tac'_ tac; (*mI = "Apply_Method"*)
47 val Appl m = applicable_in p pt m; (*m = Apply_Method'..*)
48 member op = specsteps mI; (*false*)
49 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
50 "~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
51 val PblObj {meth, ctxt, ...} = get_obj I pt p;
52 val thy' = get_obj g_domID pt p;
53 val thy = assoc_thy thy';
54 val {srls, pre, prls, ...} = get_met mI;
55 val pres = check_preconds thy prls pre meth |> map snd;
56 val ctxt = ctxt |> insert_assumptions pres;
57 val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;
58 "~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)
59 val actuals = itms2args thy metID itms
60 val scr as Prog sc = (#scr o get_met) metID
61 val formals = formal_args sc
62 (*expects same sequence of (actual) args in itms and (formal) args in met*)
63 fun relate_args env [] [] = env
64 | relate_args _ _ [] =
65 error ("ERROR in creating the environment for '" ^
66 id_of_scr sc ^ "' from \nthe items of the guard of " ^
67 metID2str metID ^ ",\n" ^
68 "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
69 (string_of_int o length) formals ^
70 " formals: " ^ terms2str formals ^ "\n" ^
71 (string_of_int o length) actuals ^
72 " actuals: " ^ terms2str actuals)
73 | relate_args env [] _ = env (*may drop Find!*)
74 | relate_args env (a::aa) (f::ff) =
75 if type_of a = type_of f
76 then relate_args (env @ [(a, f)]) aa ff
78 error ("ERROR in creating the environment for '" ^
79 id_of_scr sc ^ "' from \nthe items of the guard of " ^
80 metID2str metID ^ ",\n" ^
81 "different types of formal arg, from the script, " ^
82 "and actual arg, from the guards env:'\n" ^
83 "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
84 "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
86 "formals: " ^ terms2str formals ^ "\n" ^
87 "actuals: " ^ terms2str actuals)
88 val env = relate_args [] formals actuals;
89 val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
90 val {pre, prls, ...} = get_met metID;
91 val pres = check_preconds thy prls pre itms |> map snd;
92 val ctxt = ctxt |> insert_assumptions pres;
94 "~~~~~ continue solve";
95 val ini = init_form thy sc'''' env'''';
99 generate1 thy (Apply_Method' (mI, SOME t, is'''', ctxt))
100 (is'''', ctxt) (lev_on p, Frm)(*implicit Take*) pt;
101 ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is'''', ctxt),
102 ((lev_on p, Frm), (is'''', ctxt)))], c, (pt,pos)):calcstate');
104 val ctxt = get_ctxt pt pos;
105 val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*)
106 val SOME unknown = parseNEW ctxt "a+b+c";
107 if type_of known_x = Type ("Real.real",[]) then ()
108 else error "x+1=2 after start root-pbl wrong type-inference for known_x";
109 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
110 else error "x+1=2 after start root-pbl wrong type-inference for unknown";
112 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
113 case nxt of ("Rewrite_Set", _) => ()
114 | _ => error "minisubpbl: Method not started in root-problem";