# HG changeset patch # User Walther Neuper # Date 1305875560 -7200 # Node ID e9af6f1bc0fcb3305a56a1fdc6d4dc0dd08f39dc # Parent 2863ed75b595bf09c9e1be2ca4b1b2e6643e710d intermed. ctxt ..: init_scrstate without precond work just uncommenting (*val ctxt = ctxt |> insert_assumptions pres;*) causes errors diff -r 2863ed75b595 -r e9af6f1bc0fc src/Tools/isac/Interpret/script.sml --- a/src/Tools/isac/Interpret/script.sml Fri May 20 08:32:57 2011 +0200 +++ b/src/Tools/isac/Interpret/script.sml Fri May 20 09:12:40 2011 +0200 @@ -1588,6 +1588,9 @@ "actuals: " ^ terms2str actuals) val env = relate_args [] formals actuals; val ctxt = ProofContext.init_global thy |> declare_constraints' actuals + val {pre, prls, ...} = get_met metID; + val pres = check_preconds thy prls pre itms |> map snd; + (*val ctxt = ctxt |> insert_assumptions pres;*) in (ScrState (env,[],NONE,e_term,Safe,true), ctxt, scr):istate * Proof.context * scr end; (* decide, where to get script/istate from: diff -r 2863ed75b595 -r e9af6f1bc0fc test/Tools/isac/Minisubpbl/200-start-method.sml --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Fri May 20 08:32:57 2011 +0200 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Fri May 20 09:12:40 2011 +0200 @@ -32,17 +32,61 @@ val {srls, pre, prls, ...} = get_met mI; val pres = check_preconds thy prls pre meth |> map snd; val ctxt = ctxt |> insert_assumptions pres; -val (is as ScrState (env,_,_,_,_,_), _, sc) = init_scrstate thy meth mI; -val ini = init_form thy sc env; +val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI; +"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI) + val actuals = itms2args thy metID itms + val scr as Script sc = (#scr o get_met) metID + val formals = formal_args sc + (*expects same sequence of (actual) args in itms and (formal) args in met*) + fun relate_args env [] [] = env + | relate_args env _ [] = + error ("ERROR in creating the environment for '" ^ + id_of_scr sc ^ "' from \nthe items of the guard of " ^ + metID2str metID ^ ",\n" ^ + "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^ + (string_of_int o length) formals ^ + " formals: " ^ terms2str formals ^ "\n" ^ + (string_of_int o length) actuals ^ + " actuals: " ^ terms2str actuals) + | relate_args env [] actual_finds = env (*may drop Find!*) + | relate_args env (a::aa) (f::ff) = + if type_of a = type_of f + then relate_args (env @ [(a, f)]) aa ff + else + error ("ERROR in creating the environment for '" ^ + id_of_scr sc ^ "' from \nthe items of the guard of " ^ + metID2str metID ^ ",\n" ^ + "different types of formal arg, from the script, " ^ + "and actual arg, from the guards env:'\n" ^ + "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^ + "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^ + "in\n" ^ + "formals: " ^ terms2str formals ^ "\n" ^ + "actuals: " ^ terms2str actuals) + val env = relate_args [] formals actuals; +val ctxt = ProofContext.init_global thy |> declare_constraints' actuals +val {pre, prls, ...} = get_met metID; +val pres = check_preconds thy prls pre itms |> map snd; +val ctxt = ctxt |> insert_assumptions pres; + +"~~~~~ continue solve"; +val ini = init_form thy sc'''' env''''; val p = lev_dn p; val SOME t = ini; val (pos,c,_,pt) = - generate1 thy (Apply_Method' (mI, SOME t, is, ctxt)) - (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt; -("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), - ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate'); + generate1 thy (Apply_Method' (mI, SOME t, is'''', ctxt)) + (is'''', ctxt) (lev_on p, Frm)(*implicit Take*) pt; +("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is'''', ctxt), + ((lev_on p, Frm), (is'''', ctxt)))], c, (pt,pos)):calcstate'); + +val ctxt = get_ctxt pt pos; +val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*) +val SOME unknown = parseNEW ctxt "a+b+c"; +if type_of known_x = Type ("RealDef.real",[]) then () +else error "x+1=2 after start root-pbl wrong type-inference for known_x"; +if type_of unknown = TFree ("'a", ["Groups.plus"]) then () +else error "x+1=2 after start root-pbl wrong type-inference for unknown"; val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*) case nxt of ("Rewrite_Set", _) => () | _ => error "minisubpbl: Method not started in root-problem"; - diff -r 2863ed75b595 -r e9af6f1bc0fc test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Fri May 20 08:32:57 2011 +0200 +++ b/test/Tools/isac/Test_Isac.thy Fri May 20 09:12:40 2011 +0200 @@ -171,89 +171,6 @@ ML {* *} ML {* -"----------- Minisubplb/200-start-method.sml ---------------------"; -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"]; -val (dI',pI',mI') = - ("Test", ["sqroot-test","univariate","equation","test"], - ["Test","squ-equ-test-subpbl1"]); -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method"*) -val (pt'''', p'''') = (pt, p); -"~~~~~ fun me, args:"; val (_,tac) = nxt; -"~~~~~ fun locatetac, args:"; val ptp as (pt, p) = (pt, p); -val (mI,m) = mk_tac'_ tac; -val Appl m = applicable_in p pt m; -member op = specsteps mI; (*false*) -"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp); -"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos); -val PblObj {meth, ctxt, ...} = get_obj I pt p; -val thy' = get_obj g_domID pt p; -val thy = assoc_thy thy'; -val {srls, pre, prls, ...} = get_met mI; -val pres = check_preconds thy prls pre meth |> map snd; -val ctxt = ctxt |> insert_assumptions pres; -val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI; -*} -ML {* -"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI) - val actuals = itms2args thy metID itms - val scr as Script sc = (#scr o get_met) metID - val formals = formal_args sc - (*expects same sequence of (actual) args in itms and (formal) args in met*) - fun relate_args env [] [] = env - | relate_args env _ [] = - error ("ERROR in creating the environment for '" ^ - id_of_scr sc ^ "' from \nthe items of the guard of " ^ - metID2str metID ^ ",\n" ^ - "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^ - (string_of_int o length) formals ^ - " formals: " ^ terms2str formals ^ "\n" ^ - (string_of_int o length) actuals ^ - " actuals: " ^ terms2str actuals) - | relate_args env [] actual_finds = env (*may drop Find!*) - | relate_args env (a::aa) (f::ff) = - if type_of a = type_of f - then relate_args (env @ [(a, f)]) aa ff - else - error ("ERROR in creating the environment for '" ^ - id_of_scr sc ^ "' from \nthe items of the guard of " ^ - metID2str metID ^ ",\n" ^ - "different types of formal arg, from the script, " ^ - "and actual arg, from the guards env:'\n" ^ - "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^ - "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^ - "in\n" ^ - "formals: " ^ terms2str formals ^ "\n" ^ - "actuals: " ^ terms2str actuals) - val env = relate_args [] formals actuals; -*} -ML {* -val ctxt = ProofContext.init_global thy; -declare_constraints' actuals -*} -ML {* -val ctxt = ProofContext.init_global thy |> declare_constraints' actuals -*} -ML {* -"~~~~~ continue solve"; -val ini = init_form thy sc'''' env''''; -val p = lev_dn p; -val SOME t = ini; -val (pos,c,_,pt) = - generate1 thy (Apply_Method' (mI, SOME t, is, ctxt)) - (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt; -("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is, ctxt), - ((lev_on p, Frm), (is, ctxt)))], c, (pt,pos)):calcstate'); - -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*) -case nxt of ("Rewrite_Set", _) => () -| _ => error "minisubpbl: Method not started in root-problem"; *} ML {* *}