1.1 --- a/src/Tools/isac/Interpret/calchead.sml Thu Aug 22 10:27:02 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Thu Aug 22 11:26:14 2019 +0200
1.3 @@ -1306,8 +1306,7 @@
1.4 | _ => error "all_modspec: uncovered case get_obj"
1.5 val {ppc, ...} = Specify.get_met mI
1.6 val (_, vals) = oris2fmz_vals pors
1.7 - val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global
1.8 - |> ContextC.declare_constraints' vals
1.9 + val ctxt = ContextC.initialise dI vals
1.10 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors)
1.11 val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*)
1.12 val pt = update_spec pt p (dI, pI, mI)
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 10:27:02 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 11:26:14 2019 +0200
2.3 @@ -181,7 +181,7 @@
2.4 val i = TermC.mk_Free (i, T)
2.5 val E = LTool.upd_env E (i, v)
2.6 in
2.7 - case appy thy ptp E (up @ [Celem.R, Celem.D]) body a v of
2.8 + case appy thy ptp E (up @ [Celem.R, Celem.D]) body a v of
2.9 Appy lre => Appy lre
2.10 | Napp E => nstep_up thy ptp scr E up Napp_ a v
2.11 | Skip (v,E) => nstep_up thy ptp scr E up Skip_ a v
2.12 @@ -228,9 +228,9 @@
2.13 | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ $ _) a v = nstep_up thy ptp scr E l ay a v
2.14 | nxt_up thy ptp scr E l ay (Const ("Script.Or",_) $ _ ) a v =
2.15 nstep_up thy ptp scr E (drop_last l) ay a v
2.16 - | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*),_) $ _ $ _ $ _) a v =
2.17 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*1*), _) $ _ $ _ $ _) a v =
2.18 (*all has been done in (*2*) below*) nstep_up thy ptp scr E l ay a v
2.19 - | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*),_) $ _ $ _) a v = (*comes from e2*)
2.20 + | nxt_up thy ptp scr E l ay (Const ("Script.Seq"(*2*), _) $ _ $ _) a v = (*comes from e2*)
2.21 nstep_up thy ptp scr E l ay a v
2.22 | nxt_up thy ptp (scr as Rule.Prog sc) E l ay (Const ("Script.Seq"(*3*),_) $ _) a v = (*comes from e1*)
2.23 if ay = Napp_
2.24 @@ -250,7 +250,7 @@
2.25 if 1 < length l
2.26 then
2.27 let val up = drop_last l;
2.28 - in (nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v ) end
2.29 + in nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v end
2.30 else (*interpreted to end*)
2.31 if ay = Skip_ then Skip (v, E) else Napp E
2.32 | nstep_up _ _ _ _ l _ _ _ = error ("nstep_up: uncovered fun-def at " ^ Celem.loc_2str l)
2.33 @@ -258,7 +258,7 @@
2.34 fun execute_progr_1 thy ptp (sc as Rule.Prog prog) (Istate.ScrState (E, l, a, v, _, _)) =
2.35 if l = []
2.36 then appy thy ptp E [Celem.R] (LTool.body_of prog) NONE v
2.37 - else nstep_up thy ptp sc E l Skip_ a v
2.38 + else nstep_up thy ptp sc E l Skip_ a v
2.39 | execute_progr_1 _ _ _ _ = raise ERROR "execute_progr_1: uncovered pattern";
2.40
2.41 (* decide for the next applicable stac in the script;
2.42 @@ -613,7 +613,7 @@
2.43
2.44 (* FIXME.WN050821 compare fun solve ... fun begin_end_prog
2.45 begin_end_prog (Apply_Method' vvv FIXME: get args in applicable_in *)
2.46 -fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, _)) _ (pt, pos as (p, _)) =
2.47 +fun begin_end_prog (Tactic.Apply_Method' (mI, _, _, ctxt)) _ (pt, pos as (p, _)) =
2.48 let
2.49 val {ppc, ...} = Specify.get_met mI;
2.50 val (itms, oris, probl) = case get_obj I pt p of
2.51 @@ -636,7 +636,7 @@
2.52 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
2.53 else itms
2.54 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
2.55 - val (is, env, ctxt, scr) = case Lucin.init_scrstate thy itms mI of
2.56 + val (is, env, ctxt, scr) = case Lucin.init_scrstate ctxt itms mI of
2.57 (is as Istate.ScrState (env,_,_,_,_,_), ctxt, scr) => (is, env, ctxt, scr)
2.58 | _ => error "begin_end_prog Apply_Method': uncovered case init_scrstate"
2.59 val ini = Lucin.init_form thy scr env;
3.1 --- a/src/Tools/isac/Interpret/mathengine.sml Thu Aug 22 10:27:02 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Aug 22 11:26:14 2019 +0200
3.3 @@ -212,7 +212,7 @@
3.4 (case if member op = [Ctree.Pbl, Ctree.Met] p_
3.5 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))
3.6 then nxt_specify_ (pt, ip)
3.7 - else (LucinNEW.do_solve_step (pt,ip))
3.8 + else (LucinNEW.do_solve_step (pt, ip))
3.9 handle ERROR msg => (writeln ("*** " ^ msg);
3.10 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
3.11 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
4.1 --- a/src/Tools/isac/Interpret/model.sml Thu Aug 22 10:27:02 2019 +0200
4.2 +++ b/src/Tools/isac/Interpret/model.sml Thu Aug 22 11:26:14 2019 +0200
4.3 @@ -43,6 +43,7 @@
4.4 val ts_in : itm_ -> term list
4.5 val penvval_in : itm_ -> term list
4.6 val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *)
4.7 + val vars_of : itm list -> term list
4.8 val max_vt : itm list -> int
4.9
4.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
4.11 @@ -505,4 +506,6 @@
4.12 fun pre2str (b, t) = pair2str(bool2str b, Rule.term2str t);
4.13 fun pres2str pres = strs2str' (map (Celem.linefeed o pre2str) pres);
4.14
4.15 +fun vars_of itms = itms |> mk_env |> map snd
4.16 +
4.17 end;
4.18 \ No newline at end of file
5.1 --- a/src/Tools/isac/Interpret/ptyps.sml Thu Aug 22 10:27:02 2019 +0200
5.2 +++ b/src/Tools/isac/Interpret/ptyps.sml Thu Aug 22 11:26:14 2019 +0200
5.3 @@ -58,6 +58,10 @@
5.4 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
5.5 val add_field : theory -> Celem.pat list -> term * 'b -> string * term * 'b
5.6 val add_variants : ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
5.7 + val coll_variants: ('a * ''b) list -> ('a list * ''b) list
5.8 + val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
5.9 + val max: int list -> int
5.10 + val replace_0: int -> int list -> int list
5.11 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.12
5.13 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
5.14 @@ -226,8 +230,9 @@
5.15 fun prep_ori [] _ _ = ([], ContextC.e_ctxt)
5.16 | prep_ori fmz thy pbt =
5.17 let
5.18 - val ctxt = Proof_Context.init_global thy |> fold ContextC.declare_constraints fmz;
5.19 - val ori = map (add_field thy pbt o Model.split_dts o the o TermC.parseNEW ctxt) fmz |> add_variants;
5.20 + val ctxt = ContextC.initialise' thy fmz;
5.21 + val ori = map (add_field thy pbt o Model.split_dts o TermC.parseNEW' ctxt) fmz
5.22 + |> add_variants;
5.23 val maxv = map fst ori |> max;
5.24 val maxv = if maxv = 0 then 1 else maxv;
5.25 val oris = coll_variants ori
6.1 --- a/src/Tools/isac/Interpret/script.sml Thu Aug 22 10:27:02 2019 +0200
6.2 +++ b/src/Tools/isac/Interpret/script.sml Thu Aug 22 11:26:14 2019 +0200
6.3 @@ -17,7 +17,7 @@
6.4 val sel_rules : Ctree.ctree -> Ctree.pos' -> Tactic.input list
6.5 val init_form : 'a -> Rule.program -> (term * term) list -> term option
6.6 val tac_2tac : Tactic.T -> Tactic.input
6.7 - val init_scrstate : theory -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Rule.program
6.8 + val init_scrstate : Proof.context -> Model.itm list -> Celem.metID -> Istate.T * Proof.context * Rule.program
6.9
6.10 val get_simplifier : Ctree.state -> Rule.rls
6.11 (*DEPR ^*)val from_pblobj' : Rule.theory' -> Ctree.pos' -> Ctree.ctree -> Rule.rls * (Istate.T * Proof.context) * Rule.program
6.12 @@ -218,7 +218,7 @@
6.13 val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
6.14 val ags = TermC.isalist2list ags';
6.15 val (pI, pors, mI) =
6.16 - if mI = ["no_met"]
6.17 + if mI = ["no_met"]
6.18 then
6.19 let
6.20 val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
6.21 @@ -236,7 +236,7 @@
6.22 val {cas,ppc,thy,...} = Specify.get_pbt pI
6.23 val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
6.24 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
6.25 - val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> ContextC.declare_constraints' vals
6.26 + val ctxt = ContextC.initialise dI vals
6.27 val hdl =
6.28 case cas of
6.29 NONE => LTool.pblterm dI pI
6.30 @@ -416,7 +416,7 @@
6.31 val {cas, ppc, thy, ...} = Specify.get_pbt pI
6.32 val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*)
6.33 val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt))
6.34 - val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> ContextC.declare_constraints' vals
6.35 + val ctxt = ContextC.initialise dI vals
6.36 val hdl =
6.37 case cas of
6.38 NONE => LTool.pblterm dI pI
6.39 @@ -569,7 +569,7 @@
6.40 then tracing("@@@ istate " ^ Celem.env2str env)
6.41 else ();
6.42 in
6.43 -fun init_scrstate thy itms metID =
6.44 +fun init_scrstate ctxt itms metID =
6.45 let
6.46 (*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
6.47 val itms =
6.48 @@ -585,7 +585,7 @@
6.49 [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
6.50 else itms
6.51 (*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
6.52 - val actuals = itms2args thy metID itms
6.53 + val actuals = itms2args (Proof_Context.theory_of ctxt) metID itms
6.54 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
6.55 val (scr, sc) = (case (#scr o Specify.get_met) metID of
6.56 scr as Rule.Prog sc => (trace_init metID; (scr, sc))
6.57 @@ -606,9 +606,8 @@
6.58 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
6.59 val env = relate_args [] formals actuals;
6.60 val _ = trace_istate env;
6.61 - val ctxt = Proof_Context.init_global thy |> ContextC.declare_constraints' actuals
6.62 val {pre, prls, ...} = Specify.get_met metID;
6.63 - val pres = Stool.check_preconds thy prls pre itms |> map snd;
6.64 + val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
6.65 val ctxt = ctxt |> ContextC.insert_assumptions pres;
6.66 in (Istate.ScrState (env, [], NONE, Rule.e_term, Istate.Safe, true), ctxt, scr) end;
6.67 end (*local*)
6.68 @@ -663,7 +662,9 @@
6.69 in
6.70 if last_elem p = 0 (*nothing written to pt yet*)
6.71 then
6.72 - let val (is, ctxt, scr) = init_scrstate thy itms metID
6.73 + let
6.74 + val ctxt = ContextC.initialise thy' (Model.vars_of itms)
6.75 + val (is, ctxt, scr) = init_scrstate ctxt itms metID
6.76 in (srls, (is, ctxt), scr) end
6.77 else (srls, get_loc pt (p,p_), scr)
6.78 end;
7.1 --- a/src/Tools/isac/Interpret/solve.sml Thu Aug 22 10:27:02 2019 +0200
7.2 +++ b/src/Tools/isac/Interpret/solve.sml Thu Aug 22 11:26:14 2019 +0200
7.3 @@ -112,14 +112,14 @@
7.4 (*FIXME.WN050821 compare solve ... begin_end_prog:
7.5 WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
7.6 *)
7.7 -fun solve ("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, _)) (pt, (pos as (p, _))) =
7.8 +fun solve ("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
7.9 let val {srls, ...} = Specify.get_met mI;
7.10 val itms = case get_obj I pt p of
7.11 PblObj {meth=itms, ...} => itms
7.12 | _ => error "solve Apply_Method: uncovered case get_obj"
7.13 val thy' = get_obj g_domID pt p;
7.14 val thy = Celem.assoc_thy thy';
7.15 - val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
7.16 + val (is, env, ctxt, sc) = case Lucin.init_scrstate ctxt itms mI of
7.17 (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
7.18 | _ => error "solve Apply_Method: uncovered case init_scrstate"
7.19 val ini = Lucin.init_form thy sc env;
7.20 @@ -158,7 +158,7 @@
7.21 let
7.22 val pp = par_pblobj pt p
7.23 val asm =
7.24 - (case get_obj g_tac pt p of
7.25 + (case get_obj g_tac pt p of (*assumes Check_elementwise IMMEDIATELY BEFORE Check_Postcond*)
7.26 Tactic.Check_elementwise _ => (*collects and instantiates asms*)
7.27 (snd o (get_obj g_result pt)) p
7.28 | _ => get_assumptions_ pt (p,p_))
8.1 --- a/src/Tools/isac/ProgLang/contextC.sml Thu Aug 22 10:27:02 2019 +0200
8.2 +++ b/src/Tools/isac/ProgLang/contextC.sml Thu Aug 22 11:26:14 2019 +0200
8.3 @@ -6,8 +6,6 @@
8.4 signature CONTEXT_C =
8.5 sig
8.6 val e_ctxt : Proof.context
8.7 - val declare_constraints : string -> Proof.context -> Proof.context
8.8 - val declare_constraints' : term list -> Proof.context -> Proof.context
8.9 val initialise : string -> term list -> Proof.context
8.10 val initialise' : theory -> string list -> Proof.context
8.11 val get_assumptions : Proof.context -> term list
8.12 @@ -182,31 +180,23 @@
8.13
8.14 val e_ctxt = Proof_Context.init_global @{theory "Pure"};
8.15
8.16 -fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt;
8.17 -(*WN110613 fun declare_constraints' shall replace fun declare_constraints*)
8.18 -fun declare_constraints t ctxt =
8.19 +(* in root-problem take respective formalisation *)
8.20 +fun initialise' thy fmz =
8.21 + let
8.22 + val ctxt = thy |> Proof_Context.init_global
8.23 + val frees = map (TermC.parseNEW' ctxt) fmz |> map TermC.vars |> flat |> distinct
8.24 + val _ = TermC.raise_type_conflicts frees
8.25 + in
8.26 + fold Variable.declare_constraints frees ctxt
8.27 + end
8.28 +(* in Subproblem take respective actual arguments from program *)
8.29 +fun initialise thy' ts =
8.30 let
8.31 - fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of
8.32 - (_, _ :: _) => (Free (v, T) :: get_vars vs)
8.33 - | (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*)
8.34 - | get_vars [] = [];
8.35 - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
8.36 - in fold Variable.declare_constraints ts ctxt end;
8.37 -
8.38 -(* replace fun initialise' ..*)
8.39 -fun initialise thy' ts =
8.40 - (TermC.raise_type_conflicts ts;
8.41 - fold Variable.declare_constraints ts (Rule.Thy_Info_get_theory thy' |> Proof_Context.init_global))
8.42 -(* context initialised from theories, still given as strings in a formalisation or a program*)
8.43 -fun initialise' thy' fmz =
8.44 - let
8.45 - val ctxt = thy' |> Proof_Context.init_global
8.46 - val ts =
8.47 - (filter is_some (map (TermC.parseNEW ctxt) fmz))
8.48 - |> map the |> map TermC.vars |> flat |> distinct
8.49 - val _ = TermC.raise_type_conflicts ts
8.50 + val ctxt = Rule.Thy_Info_get_theory thy' |> Proof_Context.init_global
8.51 + val frees = map TermC.vars ts |> flat |> distinct
8.52 + val _ = TermC.raise_type_conflicts frees
8.53 in
8.54 - fold Variable.declare_constraints ts ctxt
8.55 + fold Variable.declare_constraints frees ctxt
8.56 end
8.57
8.58 structure Context_Data = Proof_Data (type T = term list fun init _ = []);
9.1 --- a/src/Tools/isac/ProgLang/termC.sml Thu Aug 22 10:27:02 2019 +0200
9.2 +++ b/src/Tools/isac/ProgLang/termC.sml Thu Aug 22 11:26:14 2019 +0200
9.3 @@ -46,11 +46,11 @@
9.4 val mk_num_op_var: term -> string -> typ -> typ -> int -> term
9.5 val mk_var_op_num: term -> string -> typ -> typ -> int -> term
9.6
9.7 - (*val list_implies: term list * term -> term --> Logic.list_implies*)
9.8 val matches: theory -> term -> term -> bool
9.9 val parse: theory -> string -> cterm option
9.10 val parseN: theory -> string -> cterm option
9.11 val parseNEW: Proof.context -> string -> term option
9.12 + val parseNEW': Proof.context -> string -> term
9.13 val parseold: theory -> string -> cterm option
9.14 val parse_patt: theory -> string -> term
9.15 val perm: term -> term -> bool
9.16 @@ -71,9 +71,9 @@
9.17 val numbers_to_string: term -> term
9.18 val uminus_to_string: term -> term
9.19 val var2free: term -> term
9.20 - val vars: term -> term list
9.21 - val vars_of : term -> term list (* probably should replace "fun vars" *)
9.22 - val dest_list' : term -> term list
9.23 + val vars: term -> term list (* recognises numverals, should replace "fun vars_of" *)
9.24 + val vars_of: term -> term list
9.25 + val dest_list': term -> term list
9.26
9.27 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
9.28 val scala_of_term: term -> string
9.29 @@ -483,6 +483,11 @@
9.30 (*WN110317 parseNEW will replace parse after introduction of ctxt completed*)
9.31 fun parseNEW ctxt str = SOME (Syntax.read_term ctxt str |> numbers_to_string)
9.32 handle _ => NONE;
9.33 +fun parseNEW' ctxt str =
9.34 + case parseNEW ctxt str of
9.35 + SOME t => t
9.36 + | NONE => raise TERM ("NO parseNEW' for " ^ str, [])
9.37 +
9.38 (* parse term patterns; Var ("v",_), i.e. "?v", are required for instantiation
9.39 WN130613 probably compare to
9.40 http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg04249.html*)
9.41 @@ -560,7 +565,7 @@
9.42 in
9.43 if confl = []
9.44 then ()
9.45 - else raise TYPE ("formalisation inconsistent from type inference: ",
9.46 + else raise TYPE ("formalisation inconsistent w.r.t. type inference: ",
9.47 map (snd o dest_Free)confl, confl)
9.48 end
9.49
10.1 --- a/src/Tools/isac/TODO.thy Thu Aug 22 10:27:02 2019 +0200
10.2 +++ b/src/Tools/isac/TODO.thy Thu Aug 22 11:26:14 2019 +0200
10.3 @@ -14,8 +14,17 @@
10.4 text \<open>
10.5 \begin{itemize}
10.6 \item xxx
10.7 - \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
10.8 - \item check in states: length ?? > 1 with tracing these cases
10.9 + \item clarify initialisation of contexts
10.10 + \begin{itemize}
10.11 + \item xxx
10.12 + \item Lucin.init_scrstate --> Istate.init_program
10.13 + \item xxx
10.14 + \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
10.15 + \item xxx
10.16 + \item Test_Some.all-contxt: wait for deleting Check_Elementwise Assumptions
10.17 + \item xxx
10.18 + \end{itemize}
10.19 + \item xxx
10.20 \item rename ScrState --> Program_State
10.21 \item locate_input_tactic arg: type istate ((ScrState is))
10.22 result: type scrstate ((is)) ... unify + readable paper!
10.23 @@ -43,7 +52,9 @@
10.24 subsection \<open>Postponed from current changeset\<close>
10.25 text \<open>
10.26 \begin{itemize}
10.27 + \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper
10.28 \item xxx
10.29 + \item check in states: length ?? > 1 with tracing these cases
10.30 \item xxx
10.31 \item datatype L,R,D --> Istate
10.32 \item xxx
10.33 @@ -71,10 +82,10 @@
10.34 and redesign handle_leaf .. subst_stacexpr .. associate
10.35 to Tactic.from_code :
10.36 + keep ! trace_script
10.37 + \item in locate_input_tactic .. ?assy?; Program.is_eval_expr .use Term.exists_Const
10.38 \item trace_script: replace ' by " in writeln
10.39 \item xxx
10.40 \item librarys.ml --> libraryC.sml + text from termC.sml
10.41 - \item e_ctxt: Selem --> ContextC
10.42 \item xxx
10.43 \item rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
10.44 \item xxx
10.45 @@ -122,7 +133,7 @@
10.46 \item xxx
10.47 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
10.48 \item xxx
10.49 - \item xxx
10.50 + \item TermC.vars_of replace by vars (recognises numerals)
10.51 \item xxx
10.52 \item xxx
10.53 \end{itemize}
10.54 @@ -146,6 +157,10 @@
10.55 \item xxx
10.56 \item drop "init_form" and use "Take" in programs (start with latter!)
10.57 \item xxx
10.58 + \item deprive Check_elementwise, but keep it for Minisubpl
10.59 + (which checks for Check_Postcond separated by another tactic)
10.60 + This seems a prerequisite for appropriate handling of contexts at Check_Postcond.
10.61 + \item xxx
10.62 \item xxx
10.63 \end{itemize}
10.64 \<close>
10.65 @@ -359,8 +374,24 @@
10.66 isabelle update -u path_cartouches
10.67 isabelle update -u inner_syntax_cartouches
10.68 \<close>
10.69 +section \<open>Questions to Isabelle experts\<close>
10.70 +text \<open>
10.71 +\begin{itemize}
10.72 +\item how HANDLE these exceptions, e.g.:
10.73 + Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
10.74 + GIVES
10.75 + "Inner syntax error
10.76 + Failed to parse term"
10.77 +\item xxx
10.78 +\item xxx
10.79 +\item xxx
10.80 +\item xxx
10.81 +\end{itemize}
10.82 +\<close>
10.83 +
10.84 section \<open>For copy & paste\<close>
10.85 text \<open>
10.86 +\begin{itemize}
10.87 \begin{itemize}
10.88 \item xxx
10.89 \begin{itemize}
11.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu Aug 22 10:27:02 2019 +0200
11.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Thu Aug 22 11:26:14 2019 +0200
11.3 @@ -1,4 +1,8 @@
11.4 -(* this theory is evaluated BEFORE Test_Isac.thy opens structures.
11.5 +(* Title: "ADDTESTS/All_Ctxt.thy"
11.6 + Author: Walther Neuper
11.7 + (c) due to copyright terms
11.8 +
11.9 + this theory is evaluated BEFORE Test_Isac.thy opens structures.
11.10 So, if you encounter errors here, first fix them in ~~/test/Tools/isac/Minimsubpbl/* *)
11.11
11.12 theory All_Ctxt imports Isac.Isac
11.13 @@ -121,13 +125,13 @@
11.14 \<close>
11.15
11.16 ML \<open>
11.17 -\<close> ML \<open>
11.18 Rule.terms2strs (Ctree.get_assumptions_ pt p)
11.19 \<close>
11.20
11.21 ML \<open>
11.22 +\<close> ML \<open>
11.23 if Rule.terms2strs (Ctree.get_assumptions_ pt p) =
11.24 - ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
11.25 + ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1"]
11.26 then () else error "All_Ctx: asms after finishing SubProblem";
11.27 \<close>
11.28
11.29 @@ -146,8 +150,9 @@
11.30 \<close>
11.31
11.32 ML \<open>
11.33 +\<close> ML \<open>
11.34 if Rule.terms2strs (Ctree.get_assumptions_ pt p) =
11.35 - ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
11.36 + ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1"]
11.37 then () else error "All_Ctx at final result";
11.38 \<close>
11.39
12.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Aug 22 10:27:02 2019 +0200
12.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Aug 22 11:26:14 2019 +0200
12.3 @@ -126,7 +126,7 @@
12.4 Isabelle can handle best.\<close>
12.5 ML \<open>
12.6 val ctxt = Proof_Context.init_global @{theory};
12.7 - val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;
12.8 +(*val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt;*)
12.9
12.10 val SOME fun1 =
12.11 TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1;
13.1 --- a/test/Tools/isac/Frontend/states.sml Thu Aug 22 10:27:02 2019 +0200
13.2 +++ b/test/Tools/isac/Frontend/states.sml Thu Aug 22 11:26:14 2019 +0200
13.3 @@ -1,4 +1,4 @@
13.4 -(* Title: test/../states.sml
13.5 +(* Title: test/Frontend/states.sml
13.6 Author: Walther Neuper 110320, Mathias Lehnfeld 140625
13.7 (c) copyright due to lincense terms.
13.8 *)
13.9 @@ -6,7 +6,7 @@
13.10 "-----------------------------------------------------------------";
13.11 "table of contents -----------------------------------------------";
13.12 "-----------------------------------------------------------------";
13.13 -"----------- test parallel calls to autoCalculate ----------------";
13.14 +"----------- (*test parallel calls to autoCalculate*) ------------";
13.15 "-----------------------------------------------------------------";
13.16 "-----------------------------------------------------------------";
13.17 "-----------------------------------------------------------------";
13.18 @@ -14,6 +14,9 @@
13.19 "----------- test parallel calls to autoCalculate ----------------";
13.20 "----------- test parallel calls to autoCalculate ----------------";
13.21 "----------- test parallel calls to autoCalculate ----------------";
13.22 +(*----------------------------------------------- Future.join DELETED FROM CODE FOR A WHILE ---\\
13.23 + CAUSES ERROR calc 1 not existent NOW.
13.24 +
13.25 let (*wraps whole test*)
13.26 val ex = [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
13.27 "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = (0::real), y' 0 = (0::real)]",
13.28 @@ -109,3 +112,4 @@
13.29 n ... max number of parallel calculations
13.30 *)
13.31 in run_tests 1(*2*) 2 2 end;
13.32 +----------------------------------------------------------------------------------------------//*)
14.1 --- a/test/Tools/isac/Frontend/use-cases.sml Thu Aug 22 10:27:02 2019 +0200
14.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Aug 22 11:26:14 2019 +0200
14.3 @@ -943,7 +943,7 @@
14.4 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
14.5 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
14.6 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
14.7 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
14.8 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
14.9 (*^^^ these are the elements for the root-problem (in variants)*)
14.10 (*vvv these are elements required for subproblems*)
14.11 "boundVariable a","boundVariable b","boundVariable alpha",
15.1 --- a/test/Tools/isac/Interpret/calchead.sml Thu Aug 22 10:27:02 2019 +0200
15.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Aug 22 11:26:14 2019 +0200
15.3 @@ -1,9 +1,6 @@
15.4 - (* Title: tests on calchead.sml
15.5 - Author: Walther Neuper 051013,
15.6 + (* Title: "Interpret/calchead.sml"
15.7 + Author: Walther Neuper 051013,
15.8 (c) due to copyright terms
15.9 -
15.10 -12345678901234567890123456789012345678901234567890123456789012345678901234567890
15.11 - 10 20 30 40 50 60 70 80
15.12 *)
15.13
15.14 "--------------------------------------------------------";
15.15 @@ -157,7 +154,7 @@
15.16 "valuesFor [a,b]",
15.17 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
15.18 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
15.19 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
15.20 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
15.21
15.22 "boundVariable a","boundVariable b","boundVariable alpha",
15.23 "interval {x::real. 0 <= x & x <= 2*r}",
16.1 --- a/test/Tools/isac/Interpret/inform.sml Thu Aug 22 10:27:02 2019 +0200
16.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Aug 22 11:26:14 2019 +0200
16.3 @@ -375,7 +375,7 @@
16.4 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
16.5 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
16.6 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
16.7 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
16.8 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
16.9 (*^^^ these are the elements for the root-problem (in variants)*)
16.10 (*vvv these are elements required for subproblems*)
16.11 "boundVariable a","boundVariable b","boundVariable alpha",
17.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 10:27:02 2019 +0200
17.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Thu Aug 22 11:26:14 2019 +0200
17.3 @@ -39,13 +39,13 @@
17.4 val Appl m = applicable_in p pt m;
17.5 member op = specsteps mI (*false*);
17.6 "~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
17.7 -"~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, _)), (pt, (pos as (p,_)))) =
17.8 +"~~~~~ fun solve, args:"; val ((_, m as Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p,_)))) =
17.9 (m, (pt, pos));
17.10 val {srls, ...} = get_met mI;
17.11 val PblObj {meth=itms, ...} = get_obj I pt p;
17.12 val thy' = get_obj g_domID pt p;
17.13 val thy = assoc_thy thy';
17.14 - val (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
17.15 + val (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate ctxt itms mI;
17.16 val ini = init_form thy sc env;
17.17 val p = lev_dn p;
17.18 ini = NONE; (*true*)
18.1 --- a/test/Tools/isac/Interpret/mathengine.sml Thu Aug 22 10:27:02 2019 +0200
18.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Aug 22 11:26:14 2019 +0200
18.3 @@ -436,19 +436,17 @@
18.4 val ((Subproblem _, tac_, (_, is))::_, c', ptp') = do_solve_step ptp;
18.5 autoord auto < 5 (*false*);
18.6 (* val ptp = all_modspec ptp' (*WAS Type unification failed...*)*)
18.7 -"~~~~~ fun all_modspec, args:"; val (pt, pos as (p,_)) = (ptp');
18.8 +"~~~~~ fun all_modspec , args:"; val (pt, pos as (p,_)) = (ptp');
18.9 val (PblObj {fmz = (fmz_, _), origin = (pors, spec as (dI,pI,mI), hdl), ...}) = get_obj I pt p;
18.10 - val thy = assoc_thy dI;
18.11 - val {ppc, ...} = get_met mI;
18.12 + val {ppc, ...} = get_met mI;
18.13 (* val (mors, ctxt) = prep_ori fmz_ thy ppc; WAS Type unification failed because
18.14 val ctxt' = dI |> Thy_Info_get_theory |> Proof_Context.init_global;
18.15 (parseNEW ctxt' "x" |> the |> type_of) = TFree ("'a",[]);
18.16 ^^^^^ *)
18.17 (*vvv from: | associate pt _ (Subproblem'...*)
18.18 - val (fmz_, vals) = oris2fmz_vals pors;
18.19 + val (_, vals) = oris2fmz_vals pors;
18.20 (**)
18.21 - val ctxt = dI |> Thy_Info_get_theory |> Proof_Context.init_global
18.22 - |> declare_constraints' vals
18.23 + val ctxt = ContextC.initialise dI vals
18.24 (**)
18.25 (*^^^ from: | associate pt _ (Subproblem'...*)
18.26 val [(1, [1], "#Given", dsc_eq, [equality]),
18.27 @@ -457,8 +455,8 @@
18.28 if term2str xxx = "x" andalso type_of xxx = HOLogic.realT then ()
18.29 else error "autoCalculate..CompleteCalc: SubProblem broken 1";
18.30 val pt = update_pblppc pt p (map (ori2Coritm ppc) pors);
18.31 - val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
18.32 - val pt = update_spec pt p (dI,pI,mI);
18.33 + val pt = update_metppc pt p (map (ori2Coritm ppc) pors);
18.34 + val pt = update_spec pt p (dI,pI,mI);
18.35 val pt = update_ctxt pt p ctxt;
18.36 "~~~~~ return to complete_solve, args:"; val (ptp) = (pt, (p,Met));
18.37 val (msg, c, (pt, p)) = complete_solve auto (c @ c') ptp;
19.1 --- a/test/Tools/isac/Interpret/me.sml Thu Aug 22 10:27:02 2019 +0200
19.2 +++ b/test/Tools/isac/Interpret/me.sml Thu Aug 22 11:26:14 2019 +0200
19.3 @@ -418,7 +418,7 @@
19.4 "valuesFor [a,b]",
19.5 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
19.6 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
19.7 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
19.8 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
19.9
19.10 "boundVariable a","boundVariable b","boundVariable alpha",
19.11 "interval {x::real. 0 <= x & x <= 2*r}",
20.1 --- a/test/Tools/isac/Interpret/mstools.sml Thu Aug 22 10:27:02 2019 +0200
20.2 +++ b/test/Tools/isac/Interpret/mstools.sml Thu Aug 22 11:26:14 2019 +0200
20.3 @@ -2,16 +2,10 @@
20.4 Author: Walther Neuper 100930, Mathias Lehnfeld
20.5 (c) copyright due to lincense terms.
20.6 *)
20.7 -"--------------------------------------------------------";
20.8 -"table of contents --------------------------------------";
20.9 -"--------------------------------------------------------";
20.10 -"----------- fun declare_constraints' -------------------";
20.11 -"----------- fun declare_constraints --------------------";
20.12 -"----------- fun get_assumptions, fun insert_assumptions-";
20.13 -"----------- fun transfer_asms_from_to ------------------";
20.14 -"----------- fun from_subpbl_to_caller ------------------";
20.15 -"----------- all ctxt changes in minimsubpbl x+1=2 ------";
20.16 -"----------- go through Model_Problem until nxt_tac -----";
20.17 +"-----------------------------------------------------------------------------------------------";
20.18 +"table of contents -----------------------------------------------------------------------------";
20.19 +"-----------------------------------------------------------------------------------------------";
20.20 +"----------- go through Model_Problem until nxt_tac --------------------------------------------";
20.21 "----------- fun comp_dts -- fun split_dts -----------------------------------------------------";
20.22 "----------- type penv -------------------------------------------------------------------------";
20.23 "----------- fun untouched ---------------------------------------------------------------------";
20.24 @@ -27,174 +21,9 @@
20.25 "--------------------------------------------------------";
20.26
20.27
20.28 -"----------- fun declare_constraints' -------------------";
20.29 -"----------- fun declare_constraints' -------------------";
20.30 -"----------- fun declare_constraints' -------------------";
20.31 -val ctxt = Proof_Context.init_global @{theory "Isac"};
20.32 -val SOME ta = parseNEW ctxt "x";
20.33 -if type_of ta = TFree ("'a",["HOL.type"]) then () else error "TODO";
20.34 -
20.35 -(*----- add a type constraint to ctxt *)
20.36 -val SOME ti = parseNEW ctxt "x::int";
20.37 -val ctxt = declare_constraints' [ti] ctxt;
20.38 -
20.39 -(*----- now parsing infers the type *)
20.40 -val SOME t = parseNEW ctxt "x";
20.41 -if type_of t = Type ("Int.int",[]) then () else error "TODO";
20.42 -
20.43 -"----------- fun declare_constraints --------------------";
20.44 -"----------- fun declare_constraints --------------------";
20.45 -"----------- fun declare_constraints --------------------";
20.46 -val ctxt = Proof_Context.init_global @{theory "Isac"}
20.47 - |> declare_constraints "xxx + yyy = (111::int)";
20.48 -val t = case parseNEW ctxt "xxx = 123" of
20.49 - NONE => error "mstools: syntax error"
20.50 - | SOME t' => t';
20.51 -if ((Tools.lhs t) |> type_of) = @{typ int} then ()
20.52 - else error "mstools: incorrect type inference from parseNEW ctxt";
20.53 -
20.54 -val t_bit = Syntax.read_term ctxt "11::int";
20.55 -val t_free = numbers_to_string t_bit;
20.56 -val ctxt = Proof_Context.init_global @{theory "Isac"};
20.57 -val SOME t = parseNEW ctxt "11";
20.58 -(*if (t |> type_of) = TFree ("'a", ["Int.number"]) then () ...2011*)
20.59 - if (t |> type_of) = TFree ("'a", ["Num.numeral"]) then ()
20.60 - else error "parsed numeral correct";
20.61 -val ctxt' = Variable.declare_constraints t_free ctxt;
20.62 -val SOME t' = parseNEW ctxt' "11";
20.63 -(*if (t' |> type_of) = TFree ("'a", ["Int.number"]) then () ...2011*)
20.64 - if (t' |> type_of) = TFree ("'a", ["Num.numeral"]) then ()
20.65 - else error "Variable.declare_constraints did not recognize numeral";
20.66 -
20.67 -"----------- fun get_assumptions, fun insert_assumptions-";
20.68 -"----------- fun get_assumptions, fun insert_assumptions-";
20.69 -"----------- fun get_assumptions, fun insert_assumptions-";
20.70 -val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
20.71 -val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
20.72 -val asms = get_assumptions ctxt;
20.73 -if asms = [@{term "x * v"}, @{term "2 * u"}]
20.74 -then () else error "mstools.sml insert_/get_assumptions changed 1.";
20.75 -
20.76 -"----------- fun transfer_asms_from_to ------------------";
20.77 -"----------- fun transfer_asms_from_to ------------------";
20.78 -"----------- fun transfer_asms_from_to ------------------";
20.79 -val ctxt = Proof_Context.init_global @{theory "Isac"}
20.80 -val from_ctxt = insert_assumptions
20.81 - [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
20.82 -val to_ctxt = insert_assumptions
20.83 - [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
20.84 -val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
20.85 -if terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
20.86 -then () else error "fun transfer_asms_from_to changed"
20.87 -
20.88 -"----------- fun from_subpbl_to_caller ------------------";
20.89 -"----------- fun from_subpbl_to_caller ------------------";
20.90 -"----------- fun from_subpbl_to_caller ------------------";
20.91 -val ctxt = Proof_Context.init_global @{theory "Isac"}
20.92 -val sub_ctxt = insert_assumptions
20.93 - [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
20.94 -val caller_ctxt = insert_assumptions
20.95 - [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
20.96 -val scrval = str2term "[x_1 = 1, x_2 = 2, x_3 = 3]";
20.97 -val new_ctxt = from_subpbl_to_caller sub_ctxt scrval caller_ctxt;
20.98 -if terms2strs (get_assumptions new_ctxt) =
20.99 -["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
20.100 -then () else error "fun from_subpbl_to_caller changed"
20.101 -
20.102 -"----------- all ctxt changes in minimsubpbl x+1=2 ------";
20.103 -"----------- all ctxt changes in minimsubpbl x+1=2 ------";
20.104 -"----------- all ctxt changes in minimsubpbl x+1=2 ------";
20.105 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
20.106 -val (dI',pI',mI') =
20.107 - ("Test", ["sqroot-test","univariate","equation","test"],
20.108 - ["Test","squ-equ-test-subpbl1"]);
20.109 -
20.110 -(*========== inhibit exn AK110725 ================================================
20.111 -(* ERROR: get_pbt not found: ["sqroot-test","univariate","equation","test"] *)
20.112 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
20.113 -========== inhibit exn AK110725 ================================================*)
20.114 -
20.115 -(*========== inhibit exn AK110725 ================================================
20.116 -(* ERROR: pt and p are not declared due to above error *)
20.117 -"=(1)= variables known from formalisation provide type-inference for further input";
20.118 -val ctxt = get_ctxt pt p;
20.119 -
20.120 -val SOME known_x = parseNEW ctxt "x+y+z";
20.121 -val SOME unknown = parseNEW ctxt "xa+b+c";
20.122 -
20.123 -if type_of known_x = Type ("Real.real",[]) then ()
20.124 -else error "x+1=2 after start root-pbl wrong type-inference from known x";
20.125 -if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
20.126 -else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";
20.127 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.128 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.129 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.130 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.131 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.132 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.133 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
20.134 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.135 -
20.136 -"=(2)= preconditions are known at start of interpretation of (root-)method";
20.137 -if get_assumptions_ pt p = [str2term "precond_rootmet x"] then ()
20.138 -else error "x+1=2 after start root-met no precondition";
20.139 -
20.140 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.141 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
20.142 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.143 -
20.144 -"=(3)= variables known from arguments of (sub-)method provide type-inference for further input";
20.145 -val ctxt = get_ctxt pt p;
20.146 -val SOME known_x = parseNEW ctxt "x+y+z";
20.147 -val SOME unknown = parseNEW ctxt "a+b+c";
20.148 -if type_of known_x = Type ("Real.real",[]) then ()
20.149 -else error "x+1=2 after start root-pbl wrong type-inference for known x";
20.150 -if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
20.151 -else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";
20.152 -
20.153 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.154 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.155 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.156 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.157 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.158 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.159 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
20.160 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.161 -
20.162 -"=(4)= preconds are known at start of interpretation of (sub-)method";
20.163 -if get_assumptions_ pt p =
20.164 - [parse_patt @{theory} "matches (?a = ?b) (-1 + x = 0)"] then ()
20.165 -else error "x+1=2 after start sub-met no precondition";
20.166 -
20.167 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.168 -
20.169 -"prep =(5)=: inject assumptions into sub-met: sub_asm_out, sub_asm_local";
20.170 -val (SOME (iform, cform), SOME (ires, cres)) = get_obj g_loc pt (fst p);
20.171 -val ctxt = insert_assumptions [str2term "x < sub_asm_out", str2term "a < sub_asm_local"] cres;
20.172 -val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
20.173 -
20.174 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR","univariate", ...]) *);
20.175 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.176 -
20.177 -"=(5)= transfer non-local assumptions and result from sub-method to root-method." ^
20.178 -" non-local assumptions are those contaning a variable known in root-method";
20.179 -if terms2strs (get_assumptions_ pt p) =
20.180 - ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
20.181 - then () else error "x+1=2 transfer from sub-met to root-met changed";
20.182 -
20.183 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt=Check_P["sqroot-test","univariate","equation","test"*)
20.184 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
20.185 -
20.186 -"=(6)= assumptions collected during lucas-interpretation for proof of postcondition";
20.187 -if terms2strs (get_assumptions_ pt p) = (*weak check: sub-result = root-result = [x = 1]*)
20.188 - ["matches (?a = ?b) (-1 + x = 0)", "x < sub_asm_out", "x = 1", "precond_rootmet x"]
20.189 - then () else error "x+1=2 transfer from sub-met to root-met changed";
20.190 -========== inhibit exn AK110725 ================================================*)
20.191 -
20.192 -
20.193 -"----------- go through Model_Problem until nxt_tac -----";
20.194 -"----------- go through Model_Problem until nxt_tac -----";
20.195 -"----------- go through Model_Problem until nxt_tac -----";
20.196 +"----------- go through Model_Problem until nxt_tac --------------------------------------------";
20.197 +"----------- go through Model_Problem until nxt_tac --------------------------------------------";
20.198 +"----------- go through Model_Problem until nxt_tac --------------------------------------------";
20.199 (*FIXME.WN110511 delete this test? (goes through "Model_Problem until nxt_tac)*)
20.200 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
20.201 val (dI',pI',mI') =
21.1 --- a/test/Tools/isac/Interpret/script.sml Thu Aug 22 10:27:02 2019 +0200
21.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Aug 22 11:26:14 2019 +0200
21.3 @@ -106,12 +106,12 @@
21.4 val Appl m = applicable_in p pt m;
21.5 member op = specsteps mI; (*false*)
21.6 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
21.7 -"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,_)), pos as (p,_)) = (m, pos);
21.8 +"~~~~~ fun solve, args:"; val (("Apply_Method", Apply_Method' (mI,_,_,ctxt)), pos as (p,_)) = (m, pos);
21.9 val {srls, ...} = get_met mI;
21.10 val PblObj {meth=itms, ...} = get_obj I pt p;
21.11 val thy' = get_obj g_domID pt p;
21.12 val thy = assoc_thy thy';
21.13 -val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
21.14 +val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate ctxt itms mI;
21.15 val ini = init_form thy sc env;
21.16 "----- fun init_form, args:"; val (Prog sc) = sc;
21.17 "----- fun get_stac, args:"; val (y, h $ body) = (thy, sc);
21.18 @@ -390,7 +390,7 @@
21.19 "----------- fun init_scrstate -----------------------------------------------------------------";
21.20 "----------- fun init_scrstate -----------------------------------------------------------------";
21.21 val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
21.22 - "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
21.23 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
21.24 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
21.25 "AbleitungBiegelinie dy"];
21.26 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
21.27 @@ -410,9 +410,10 @@
21.28 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy"*)
21.29 (*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
21.30
21.31 -val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
21.32 +(*+*)val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
21.33 +(*+*)val ctxt = get_ctxt pt''''' p''''';
21.34 "~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
21.35 -val (ScrState st, ctxt, Prog _) = init_scrstate thy itms metID;
21.36 +val (ScrState st, ctxt, Prog _) = init_scrstate ctxt itms metID;
21.37 if scrstate2str st =
21.38 "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], NONE, \n??.empty, Safe, true)"
21.39 then () else error "init_scrstate changed for Biegelinie";
22.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 10:27:02 2019 +0200
22.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 22 11:26:14 2019 +0200
22.3 @@ -91,7 +91,7 @@
22.4 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
22.5
22.6 Solve.solve m (pt, pos);
22.7 -"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =
22.8 +"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _)))) =
22.9 (m, (pt, pos));
22.10 val {srls, ...} = Specify.get_met mI;
22.11 val itms = case get_obj I pt p of
22.12 @@ -99,7 +99,7 @@
22.13 | _ => error "solve Apply_Method: uncovered case get_obj"
22.14 val thy' = get_obj g_domID pt p;
22.15 val thy = Celem.assoc_thy thy';
22.16 - val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
22.17 + val (is, env, ctxt, sc) = case Lucin.init_scrstate ctxt itms mI of
22.18 (is as Istate.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
22.19 | _ => error "solve Apply_Method: uncovered case init_scrstate"
22.20 val ini = Lucin.init_form thy sc env;
23.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Aug 22 10:27:02 2019 +0200
23.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Thu Aug 22 11:26:14 2019 +0200
23.3 @@ -38,7 +38,7 @@
23.4 "valuesFor [a,b]",
23.5 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
23.6 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
23.7 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
23.8 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
23.9
23.10 "boundVariable a","boundVariable b","boundVariable alpha",
23.11 "interval {x::real. 0 <= x & x <= 2*r}",
23.12 @@ -265,7 +265,7 @@
23.13 "valuesFor [a,b]",
23.14 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
23.15 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
23.16 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
23.17 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
23.18
23.19 "boundVariable a","boundVariable b","boundVariable alpha",
23.20 "interval {x::real. 0 <= x & x <= 2*r}",
23.21 @@ -416,7 +416,7 @@
23.22 "valuesFor [a,b]",
23.23 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
23.24 "relations [A=a*b, (a/2)^2 + (b/2)^2 = r^2]",
23.25 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
23.26 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
23.27
23.28 "boundVariable a","boundVariable b","boundVariable alpha",
23.29 "interval {x::real. 0 <= x & x <= 2*r}",
23.30 @@ -662,7 +662,7 @@
23.31 val v_v = (str2term "v_v::real",
23.32 str2term "alpha");
23.33 val eqs=(str2term "eqs::bool list",
23.34 - str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]");
23.35 + str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]");
23.36 val env = [f_f, v_v, eqs];
23.37
23.38 (*--- 1.line in script ---*)
24.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Thu Aug 22 10:27:02 2019 +0200
24.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Thu Aug 22 11:26:14 2019 +0200
24.3 @@ -291,7 +291,6 @@
24.4 ((Ptyp ("LINEAR", [get_pbt ["LINEAR","system"]], [])): pbt ptyp));
24.5 val {thy, ppc, where_, prls, ...} = py ;
24.6 "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, ppc);
24.7 -(* val ctxt = Proof_Context.init_global thy |> fold declare_constraints fmz;*)
24.8 val ctxt = Proof_Context.init_global thy;
24.9 "~~~~~ fun declare_constraints, args:"; val (t, ctxt) = (nth 1 fmz, ctxt);
24.10 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
25.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Thu Aug 22 10:27:02 2019 +0200
25.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Thu Aug 22 11:26:14 2019 +0200
25.3 @@ -1,4 +1,4 @@
25.4 -(* tests on PolyMinus
25.5 +(* title: Knowledge/polyminus.sml
25.6 author: Walther Neuper
25.7 WN071207,
25.8 (c) due to copyright terms
25.9 @@ -352,8 +352,8 @@
25.10 "----------- pbl polynom probe -----------------------------------";
25.11 reset_states ();
25.12 CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\
25.13 - \3 - 2 * e + 2 * f + 2 * g)",
25.14 - "mitWert [e = 1, f = 2, g = 3]",
25.15 + \3 - 2 * e + 2 * f + 2 * (g::int))",
25.16 + "mitWert [e = (1::int), f = (2::int), g = (3::int)]",
25.17 "Geprueft b"],
25.18 ("PolyMinus",["polynom","probe"],
25.19 ["probe","fuer_polynom"]))];
25.20 @@ -388,8 +388,8 @@
25.21
25.22 "======= probe p.34 -----";
25.23 reset_states ();
25.24 -CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)",
25.25 - "mitWert [u = 2]",
25.26 +CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * (u::int))",
25.27 + "mitWert [u = (2::int)]",
25.28 "Geprueft b"],
25.29 ("PolyMinus",["polynom","probe"],
25.30 ["probe","fuer_polynom"]))];
26.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Aug 22 10:27:02 2019 +0200
26.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Thu Aug 22 11:26:14 2019 +0200
26.3 @@ -53,8 +53,8 @@
26.4 | ((1, [1], "#undef", Const ("empty", _), _) :: _) => error "START specify: oris are not properly initialised"
26.5 | _ => error ""
26.6
26.7 -"~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, yyy);
26.8 - val ctxt = Proof_Context.init_global thy |> fold ContextC.declare_constraints fmz;
26.9 +"~~~~~ fun prep_ori , args:"; val (fmz, thy, pbt) = (fmz, thy, yyy);
26.10 + val ctxt = ContextC.initialise' thy fmz;
26.11 (*ADD check*)
26.12 case TermC.parseNEW ctxt "equality (x+1=(2::real))" of
26.13 SOME (Const ("Descript.equality", _) (* <<< ---------------- this needs to be recognised *) $
27.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Aug 22 10:27:02 2019 +0200
27.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Aug 22 11:26:14 2019 +0200
27.3 @@ -58,8 +58,8 @@
27.4 val {srls, pre, prls, ...} = get_met mI;
27.5 val pres = check_preconds thy prls pre meth |> map snd;
27.6 val ctxt = ctxt |> insert_assumptions pres;
27.7 -val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate thy meth mI;
27.8 -"~~~~~ fun init_scrstate, args:"; val (thy, itms, metID) = (thy, meth, mI)
27.9 +val (is'''' as ScrState (env'''',_,_,_,_,_), _, sc'''') = init_scrstate ctxt meth mI;
27.10 +"~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (thy, meth, mI)
27.11 val actuals = itms2args thy metID itms
27.12 val scr as Prog sc = (#scr o get_met) metID
27.13 val formals = formal_args sc
27.14 @@ -93,11 +93,11 @@
27.15 else
27.16 let val (f, a) = assoc_by_type f aas
27.17 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
27.18 - val env = relate_args [] formals actuals;
27.19 -val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
27.20 -val {pre, prls, ...} = get_met metID;
27.21 -val pres = check_preconds thy prls pre itms |> map snd;
27.22 -val ctxt = ctxt |> insert_assumptions pres;
27.23 + val env = relate_args [] formals actuals;
27.24 + (*val _ = trace_istate env;*)
27.25 + val {pre, prls, ...} = Specify.get_met metID;
27.26 + val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
27.27 + val ctxt = ctxt |> ContextC.insert_assumptions pres;
27.28
27.29 "~~~~~ continue solve";
27.30 val ini = init_form thy sc'''' env'''';
28.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Aug 22 10:27:02 2019 +0200
28.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Thu Aug 22 11:26:14 2019 +0200
28.3 @@ -17,15 +17,19 @@
28.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
28.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = (_, Apply_Method ["Test", "squ-equ-test-subpbl1"])*);
28.8 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)
28.9 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*);
28.10 +(*[1], Frm*)val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (*nxt = Rewrite_Set "norm_equation"*)
28.11
28.12 -if p = ([1], Frm) andalso f = FormKF "x + 1 = 2" andalso fst nxt = "Rewrite_Set"
28.13 +(*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
28.14 + 1 relevant for original decomposition *)
28.15 +(*[1], Res*)val (p'''_',_,f,nxt'''_',_,pt'''_') = me nxt'''' p'''' [] pt'''';(*nxt = Rewrite_Set "Test_simplify"*)
28.16 +
28.17 +if p'''' = ([1], Frm) andalso f'''' = FormKF "x + 1 = 2" andalso fst nxt'''' = "Rewrite_Set"
28.18 then () else error "250-Rewrite_Set-from-method.sml: start of test CHANGED";
28.19
28.20 (* val (p,_,f,nxt,_,pt) = ERROR WAS: nxt = ("Empty_Tac",..*) me nxt p [] pt;
28.21 (* ERROR WAS: assy: call by ([3], Pbl) *)
28.22 -"~~~~~ fun me[1], args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
28.23 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt'''', p'''', [], pt'''');
28.24
28.25 (*ERROR WAS: assy: call by ([3], Pbl)*)
28.26 val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt,p) (*of*);
28.27 @@ -136,3 +140,128 @@
28.28
28.29 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, _, (Const ("Script.Try"(*2*), _) $ _), a, v) =
28.30 (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v );
28.31 +
28.32 +(*\\--1 end step into relevant call ----------------------------------------------------------//*)
28.33 +
28.34 +(* nxt'''_' = Rewrite_Set "Test_simplify"
28.35 + //--2 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
28.36 + 2 relevant for exception TERM raised (line 297 of "term.ML"): dest_Free -1 + x = 0 *)
28.37 +(**)val (p,_,f,nxt,_,pt) = me nxt'''_' p'''_' [] pt'''_';(**)
28.38 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt'''_', p'''_', [], pt'''_');
28.39 + val (pt, p) =
28.40 + (*locatetac is here for testing by me; step would suffice in me*)
28.41 + case locatetac tac (pt, p) of
28.42 + ("ok", (_, _, ptp)) => ptp
28.43 + | ("unsafe-ok", (_, _, ptp)) => ptp
28.44 + | ("not-applicable",_) => (pt, p)
28.45 + | ("end-of-calculation", (_, _, ptp)) => ptp
28.46 + | ("failure", _) => error "sys-error"
28.47 + | _ => error "me: uncovered case"
28.48 +
28.49 + (*case*) step p ((pt, Ctree.e_pos'), []) (*of*);
28.50 +"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis))
28.51 + = (p, ((pt, Ctree.e_pos'), []));
28.52 + val pIopt = get_pblID (pt,ip);
28.53 + (*if*) ip = ([], Ctree.Res) (*else*);
28.54 + val _ = (*case*) tacis (*of*);
28.55 + val SOME _ = (*case*) pIopt (*of*);
28.56 + (*if*) member op = [Ctree.Pbl, Ctree.Met] p_
28.57 + andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (*else*);
28.58 +
28.59 + do_solve_step (pt, ip);
28.60 +"~~~~~ and do_solve_step , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
28.61 + (*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*else*);
28.62 + val thy' = get_obj g_domID pt (par_pblobj pt p);
28.63 + val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
28.64 +
28.65 + (*val (tac_, is, (t, _)) =*) determine_next_tactic (thy', srls) (pt, pos) sc is;
28.66 +"~~~~~ fun determine_next_tactic , args:"; val (thy, (ptp as (pt, (p, _))), sc, (Istate.ScrState (E,l,a,v,s,_), ctxt))
28.67 + = ((thy', srls), (pt, pos), sc, is);
28.68 +
28.69 + (*case*) execute_progr_1 thy ptp sc (Istate.ScrState (E,l,a,v,s,false)) (*of*);
28.70 +"~~~~~ fun execute_progr_1 , args:"; val (thy, ptp, (sc as Rule.Prog prog), (Istate.ScrState (E, l, a, v, _, _)))
28.71 + = (thy, ptp, sc, (Istate.ScrState (E,l,a,v,s,false)));
28.72 + (*if*) l = [] (*else*);
28.73 +
28.74 + nstep_up thy ptp sc E l Skip_ a v;
28.75 +"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
28.76 + = (thy, ptp, sc, E, l, Skip_, a, v);
28.77 + (*if*) 1 < length l (*then*);
28.78 + val up = drop_last l;
28.79 +
28.80 + nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
28.81 +"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, _, (Const ("Script.Try"(*1*),_) $ _ ), a, v)
28.82 + = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
28.83 +
28.84 + nstep_up thy ptp scr E l Skip_ a v;
28.85 +"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
28.86 + = (thy, ptp, scr, E, l, Skip_, a, v);
28.87 + (*if*) 1 < length l (*then*);
28.88 + val up = drop_last l;
28.89 +
28.90 + nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
28.91 +"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq"(*2*), _) $ _ $ _), a, v)
28.92 + = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
28.93 +
28.94 + nstep_up thy ptp scr E l ay a v;
28.95 +"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
28.96 + = (thy, ptp, scr, E, l, ay, a, v);
28.97 + (*if*) 1 < length l (*then*);
28.98 + val up = drop_last l;
28.99 +
28.100 + nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
28.101 +"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("Script.Seq"(*1*), _) $ _ $ _ $ _), a, v)
28.102 + = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
28.103 +
28.104 + nstep_up thy ptp scr E l ay a v;
28.105 +"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v)
28.106 + = (thy, ptp, scr, E, l, ay, a, v);
28.107 + (*if*) 1 < length l (*then*);
28.108 + val up = drop_last l;
28.109 +
28.110 + nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v;
28.111 +"~~~~~ fun nxt_up , args:"; val (thy, ptp, scr, E, l, ay, (Const ("HOL.Let", _) $ _), a, v)
28.112 + = (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
28.113 + (*if*) ay = Napp_ (*else*);
28.114 + val up = drop_last l
28.115 + val (i, T, body) =
28.116 + (case go up sc of
28.117 + Const ("HOL.Let",_) $ _ $ (Abs aa) => aa
28.118 + | t => error ("nxt_up..HOL.Let $ _ with " ^ Rule.term2str t))
28.119 + val i = TermC.mk_Free (i, T)
28.120 + val E = LTool.upd_env E (i, v);
28.121 +
28.122 + (*case*) appy thy ptp E (up @ [Celem.R, Celem.D]) body a v (*of*);
28.123 +"~~~~~ fun appy , args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v)
28.124 + = (thy, ptp, E, (up @ [Celem.R, Celem.D]), body, a, v);
28.125 +
28.126 + (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e a v (*of*);
28.127 +"~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v)
28.128 + = (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v);
28.129 + val (a', LTool.STac stac) = (*case*) Lucin.handle_leaf "next " th sr E a v t (*of*);
28.130 +
28.131 + (*val (m,m') = Lucin.*) stac2tac_ pt (Celem.assoc_thy th) stac;
28.132 +"~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Script.SubProblem", _) $ spec' $ ags'))
28.133 + = (pt, (Celem.assoc_thy th), stac);
28.134 + val (dI, pI, mI) = LTool.dest_spec spec'
28.135 + val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
28.136 + val ags = TermC.isalist2list ags';
28.137 + (*if*) mI = ["no_met"] (*else*);
28.138 + val (pI, pors, mI) =
28.139 + (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
28.140 + handle ERROR "actual args do not match formal args"
28.141 + => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI)
28.142 + val (fmz_, vals) = Chead.oris2fmz_vals pors;
28.143 + val {cas,ppc,thy,...} = Specify.get_pbt pI
28.144 + val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
28.145 + val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt));
28.146 + val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct);
28.147 +(*\\--2 end step into relevant call ----------------------------------------------------------//*)
28.148 +
28.149 +if p = ([2], Res) andalso f2str f = "-1 + x = 0" then
28.150 + case nxt of
28.151 + ("Subproblem", Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"])) => ()
28.152 + | _ => error "Minisubpbl/250-Rewrite_Set-from-method changed 1"
28.153 +else error "Minisubpbl/250-Rewrite_Set-from-method changed 2";
28.154 +
28.155 +(*[3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
28.156 \ No newline at end of file
29.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Aug 22 10:27:02 2019 +0200
29.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Thu Aug 22 11:26:14 2019 +0200
29.3 @@ -17,12 +17,15 @@
29.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29.8 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29.9 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
29.10 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem"*)
29.11 -"~~~~~ fun me, args:"; val (_,tac) = nxt;
29.12 -"~~~~~ fun locatetac, args:"; val (tac, ptp as (pt, p)) = (tac, (pt,p));
29.13 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
29.14 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_equation"*)
29.15 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify" *)
29.16 +(*[2], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem"*)
29.17 +(*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
29.18 + 1 relevant for updating ctxt *)
29.19 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
29.20 +
29.21 +"~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
29.22 val (mI,m) = mk_tac'_ tac;
29.23 val Appl m = applicable_in p pt m;
29.24 member op = specsteps mI; (*false*)
29.25 @@ -46,24 +49,87 @@
29.26 (last_elem o fst) p = 0 andalso snd p = Res) (*else*);
29.27 (*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
29.28 (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)
29.29 -"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss)) =
29.30 - ((thy',srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );
29.31 +"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss: step list)) =
29.32 + ((ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );
29.33 (*if*) 1 < length l (*true*);
29.34 val up = drop_last l;
29.35 -(*ass_up ys ((E,up,a,v,S,b),ss) (go up sc);*)
29.36 +
29.37 + ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
29.38 "~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Script.Try",_) $ e)) =
29.39 (ys, ((E,up,a,v,S,b),ss), (go up sc));
29.40 -(* STOPPED stepping into HERE due to type problem: Can't unify _a to pos * pos_
29.41 -astep_up ysa iss;
29.42 + astep_up ysa iss;
29.43 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
29.44 + (*if*) 1 < length l; (*then*)
29.45 + val up = drop_last l;
29.46
29.47 -at bottom of | assy we see:
29.48 - :
29.49 - case associate pt d m stac of
29.50 -"~~~~~ fun associate, args:"; val (...Subproblem'...) = ();
29.51 - val ctxt = dI |> Thy_Info_get_theory |> Proof_Context.init_global
29.52 - |> declare_constraints' vals
29.53 -*)
29.54 + ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
29.55 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ )) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
29.56
29.57 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
29.58 -case nxt of ("Model_Problem", _) => ()
29.59 -| _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem";
29.60 + astep_up ysa iss (*2*: comes from e2*);
29.61 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
29.62 + (*if*) 1 < length l; (*then*)
29.63 + val up = drop_last l;
29.64 +
29.65 + ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
29.66 +"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
29.67 +
29.68 + astep_up ysa iss (*all has been done in (*2*) below*);
29.69 +"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
29.70 + (*if*) 1 < length l; (*then*)
29.71 + val up = drop_last l;
29.72 +
29.73 + ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
29.74 +"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,a,v,S,b),ss), (Const ("HOL.Let",_) $ _))
29.75 + = (ys, ((E,up,a,v,S,b),ss), (go up sc));
29.76 + val l = drop_last l; (*comes from e, goes to Abs*)
29.77 + val (i, T, body) =
29.78 + (case go l sc of
29.79 + Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)
29.80 + | t => error ("ass_up..HOL.Let $ _ with " ^ Rule.term2str t))
29.81 + val i = TermC.mk_Free (i, T);
29.82 + val E = LTool.upd_env E (i, v);
29.83 +
29.84 + (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss) body (*of*);
29.85 +"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:Lucin.step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
29.86 + = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss), body);
29.87 +
29.88 + (*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
29.89 + (* here is not a tactical like TRY etc, but a tactic creating a step of calculation *)
29.90 +"~~~~~ fun assy , args:"; val ((ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss:step list), t)
29.91 + = (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
29.92 +
29.93 +(*val (a', LTool.STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac" sr E a v t (*of*);
29.94 +"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, E, a, v, t)
29.95 + = ("locate", "Isac", sr, E, a, v, t);
29.96 +
29.97 + val (a', LTool.STac stac) = (*case*) LTool.subst_stacexpr E a v t (*of*);
29.98 +"~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Script.SubProblem", _) $ _ $ _)))
29.99 + = (E, a, v, t);
29.100 +
29.101 + (NONE, STac (subst_atomic E t)); (*return value*)
29.102 +"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', LTool.STac stac))
29.103 + = ((NONE : term option, STac (subst_atomic E t)));
29.104 + val stac' =
29.105 + Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac);
29.106 +
29.107 + (*return value*) (a', LTool.STac stac');
29.108 +"~~~~~ from handle_leaf to assy return val:"; val (a', LTool.STac stac)
29.109 + = ((a' : term option, LTool.STac stac'));
29.110 + val p' =
29.111 + case p_ of Frm => p
29.112 + | Res => lev_on p
29.113 + | _ => error ("assy: call by " ^ pos'2str (p,p_));
29.114 + (**)val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt m stac (*of*);
29.115 + val (p'',c',f',pt') =
29.116 + Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
29.117 +
29.118 +(*+*)if is_e_ctxt ctxt then error "ERROR: assy returns e_ctxt" else ();
29.119 +(*\\--1 end step into relevant call ----------------------------------------------------------//*)
29.120 +
29.121 +val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';
29.122 +
29.123 +if p = ([3], Pbl) andalso not (get_ctxt pt p |> is_e_ctxt)
29.124 +then
29.125 + case nxt of ("Model_Problem", _) => ()
29.126 + | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"
29.127 +else error "Minisubpbl/300-init-subpbl.sml changed";
30.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Aug 22 10:27:02 2019 +0200
30.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Aug 22 11:26:14 2019 +0200
30.3 @@ -47,14 +47,14 @@
30.4 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = ((mI, m), ptp);
30.5
30.6 solve m (pt, pos);
30.7 -"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _))))
30.8 +"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _))))
30.9 = (m, (pt, pos));
30.10 val {srls, ...} = get_met mI;
30.11 val PblObj {meth=itms, ...} = get_obj I pt p;
30.12 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
30.13 val thy' = get_obj g_domID pt p;
30.14 val thy = assoc_thy thy';
30.15 - val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate thy itms mI;
30.16 + val (is as ScrState (env,_,_,_,_,_), ctxt, sc) = init_scrstate ctxt itms mI;
30.17 (*dont take ctxt ^^^ from ^^^^^^^^^^^^^*)
30.18
30.19 (*+*)val (pt, p) = case locatetac tac (pt, pos) of
31.1 --- a/test/Tools/isac/OLDTESTS/script.sml Thu Aug 22 10:27:02 2019 +0200
31.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Thu Aug 22 11:26:14 2019 +0200
31.3 @@ -76,7 +76,7 @@
31.4
31.5 val ags = map (Thm.term_of o the o (parse DiffApp.thy))
31.6 ["A::real", "alpha::real",
31.7 - "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
31.8 + "[A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]"];
31.9 val ll = [](*:loc_*);
31.10 (* problem with exn PTREE + eval_to -------------------------
31.11 "-------------- subproblem with empty formalizaton -------";
32.1 --- a/test/Tools/isac/ProgLang/contextC.sml Thu Aug 22 10:27:02 2019 +0200
32.2 +++ b/test/Tools/isac/ProgLang/contextC.sml Thu Aug 22 11:26:14 2019 +0200
32.3 @@ -6,13 +6,85 @@
32.4 "-----------------------------------------------------------------------------------------------";
32.5 "table of contents -----------------------------------------------------------------------------";
32.6 "-----------------------------------------------------------------------------------------------";
32.7 -"----------- check all handling of context -----------------------------------------------------";
32.8 +"----------- SEE ADDTESTS/All_Ctxt.thy ---------------------------------------------------------";
32.9 +"-----------------------------------------------------------------------------------------------";
32.10 +"----------- fun initialise --------------------------------------------------------------------";
32.11 +"----------- build fun initialise'--------------------------------------------------------------";
32.12 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
32.13 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
32.14 +"----------- fun from_subpbl_to_caller ---------------------------------------------------------";
32.15 +"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
32.16 "-----------------------------------------------------------------------------------------------";
32.17 "-----------------------------------------------------------------------------------------------";
32.18 "-----------------------------------------------------------------------------------------------";
32.19
32.20
32.21 -"----------- check all handling of context -----------------------------------------------------";
32.22 -"----------- check all handling of context -----------------------------------------------------";
32.23 -"----------- check all handling of context -----------------------------------------------------";
32.24 -(* waits in Test_Some.thy for checking further updates to context handling *)
32.25 \ No newline at end of file
32.26 +"----------- fun initialise --------------------------------------------------------------------";
32.27 +"----------- fun initialise --------------------------------------------------------------------";
32.28 +"----------- fun initialise --------------------------------------------------------------------";
32.29 +val t = @{term "a * b + -123 * c :: real"};
32.30 +val ctxt = initialise "Rational" (vars t)
32.31 +
32.32 +(*----- now parsing infers the type *)
32.33 +val SOME t = parseNEW ctxt "x";
32.34 +if type_of t = HOLogic.realT then error "type inference failed 1" else ();
32.35 +
32.36 +val SOME t = parseNEW ctxt "a";
32.37 +if type_of t = HOLogic.realT then () else error "type inference failed 2";
32.38 +
32.39 +"----------- build fun initialise'--------------------------------------------------------------";
32.40 +"----------- build fun initialise'--------------------------------------------------------------";
32.41 +"----------- build fun initialise'--------------------------------------------------------------";
32.42 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
32.43 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
32.44 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
32.45 + "AbleitungBiegelinie dy"];
32.46 +val (thy, fmz) = (@{theory Biegelinie}, fmz);
32.47 +
32.48 +initialise' thy fmz;
32.49 +
32.50 + val ctxt = thy |> Proof_Context.init_global
32.51 + val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct
32.52 + val _ = TermC.raise_type_conflicts ts;
32.53 +
32.54 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
32.55 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
32.56 +"----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
32.57 +val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}, @{term "2 * u"}] ctxt;
32.58 +val ctxt = insert_assumptions [@{term "x * v"}, @{term "2 * u"}] ctxt;
32.59 +val asms = get_assumptions ctxt;
32.60 +if asms = [@{term "x * v"}, @{term "2 * u"}]
32.61 +then () else error "mstools.sml insert_/get_assumptions changed 1.";
32.62 +
32.63 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
32.64 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
32.65 +"----------- fun transfer_asms_from_to ---------------------------------------------------------";
32.66 +val ctxt = Proof_Context.init_global @{theory "Isac"}
32.67 +val from_ctxt = insert_assumptions
32.68 + [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
32.69 +val to_ctxt = insert_assumptions
32.70 + [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
32.71 +val new_ctxt = transfer_asms_from_to from_ctxt to_ctxt;
32.72 +if terms2strs (get_assumptions new_ctxt) = ["b < fro", "b < to", "c < to"]
32.73 +then () else error "fun transfer_asms_from_to changed"
32.74 +
32.75 +"----------- fun from_subpbl_to_caller ---------------------------------------------------------";
32.76 +"----------- fun from_subpbl_to_caller ---------------------------------------------------------";
32.77 +"----------- fun from_subpbl_to_caller ---------------------------------------------------------";
32.78 +val ctxt = Proof_Context.init_global @{theory "Isac"}
32.79 +val sub_ctxt = insert_assumptions
32.80 + [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
32.81 +val caller_ctxt = insert_assumptions
32.82 + [str2term "b < (to::int)", str2term "c < (to::int)"] ctxt
32.83 +val scrval = str2term "[x_1 = 1, x_2 = 2, x_3 = 3]";
32.84 +val new_ctxt = from_subpbl_to_caller sub_ctxt scrval caller_ctxt;
32.85 +if terms2strs (get_assumptions new_ctxt) =
32.86 +["b < fro", "x_1 = 1", "x_2 = 2", "x_3 = 3", "b < to", "c < to"]
32.87 +then () else error "fun from_subpbl_to_caller changed"
32.88 +
32.89 +
32.90 +
32.91 +"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
32.92 +"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
32.93 +"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
32.94 +(* waits in Test_Some.thy *)
32.95 \ No newline at end of file
33.1 --- a/test/Tools/isac/Test_Some.thy Thu Aug 22 10:27:02 2019 +0200
33.2 +++ b/test/Tools/isac/Test_Some.thy Thu Aug 22 11:26:14 2019 +0200
33.3 @@ -38,7 +38,7 @@
33.4 "~~~~~ fun xxx , args:"; val () = ();
33.5 "~~~~~ and xxx , args:"; val () = ();
33.6 "~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
33.7 -(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
33.8 +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
33.9 "xx"
33.10 ^ "xxx" (*+*)
33.11 \<close>
33.12 @@ -71,23 +71,14 @@
33.13 "~~~~~ fun xxx , args:"; val () = ();
33.14 \<close>
33.15
33.16 -section \<open>===================================================================================\<close>
33.17 -ML \<open>
33.18 -"~~~~~ fun xxx , args:"; val () = ();
33.19 -\<close> ML \<open>
33.20 -\<close> ML \<open>
33.21 -\<close> ML \<open>
33.22 -"~~~~~ fun xxx , args:"; val () = ();
33.23 -\<close>
33.24 -
33.25 section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
33.26 ML \<open>
33.27 "~~~~~ fun xxx , args:"; val () = ();
33.28 \<close> ML \<open>
33.29 (* waits for finalising ctxt: want result [x = 6 / 5] instead of "[]"*)
33.30 -"----------- check all handling of context -----------------------------------------------------";
33.31 -"----------- check all handling of context -----------------------------------------------------";
33.32 -"----------- check all handling of context -----------------------------------------------------";
33.33 +"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
33.34 +"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
33.35 +"----------- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts ---------------------";
33.36 (*ER-7*) (*Schalk I s.87 Bsp 55b*)
33.37 (* peculiarity of this example:
33.38 show_pt_tac pt;
33.39 @@ -116,7 +107,7 @@
33.40 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.41 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.42 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.43 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
33.44 +(*[], Met*)val (p,_,f,nxt,_,pt''''') = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*)
33.45 \<close> ML \<open>
33.46 (*+*)if p = ([], Met) andalso fst nxt = "Apply_Method" andalso
33.47 (*+*)terms2str (get_assumptions_ pt p) = "[]"
33.48 @@ -124,7 +115,7 @@
33.49 \<close> ML \<open>
33.50 (*//--1 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\
33.51 1 relevant for init_scrstate in root-pbl*)
33.52 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
33.53 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt''''';
33.54 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
33.55 \<close> ML \<open>
33.56 (*+*)if p = ([1], Frm) andalso fst nxt = "Rewrite_Set" andalso
33.57 @@ -176,14 +167,72 @@
33.58 \<close> ML \<open>
33.59 (*//--9 begin step into relevant call ----------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\
33.60 9 relevant for dropping "x = 0" due to asm "x \<noteq> 0"*)
33.61 -(*[4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
33.62 +(*[4, 4], Res*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p [1] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
33.63 +\<close> ML \<open>
33.64 +val ctxt = get_ctxt pt p;
33.65 +terms2str (get_assumptions ctxt)
33.66 + = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]";
33.67 +(* ^^^ NOT evaluated ^^^ *)
33.68 +\<close> ML \<open>
33.69 +val ctxt = get_ctxt pt''''' p''''';
33.70 +terms2str (get_assumptions ctxt)
33.71 + = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"
33.72 +(* should formulas from calculation really go into ctxt ? ^^^^^ ^^^^^^^^^*)
33.73 +\<close> ML \<open>
33.74 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [1], pt);
33.75 +\<close> ML \<open>
33.76 + val ("ok", (_, _, ptp''''')) = (*case*) locatetac tac (pt, p) (*of*);
33.77 +\<close> ML \<open>
33.78 +val ctxt = get_ctxt (fst ptp''''') (snd ptp''''');
33.79 +terms2str (get_assumptions ctxt)
33.80 + = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"
33.81 +\<close> ML \<open>
33.82 +"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
33.83 +\<close> ML \<open>
33.84 + val (mI, m) = Solve.mk_tac'_ tac;
33.85 +\<close> ML \<open>
33.86 + val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
33.87 +\<close> ML \<open>
33.88 + (*if*) member op = Solve.specsteps mI (*else*);
33.89 +\<close> ML \<open>
33.90 + val Updated (tacis''''', pos's''''', ptp''''') = loc_solve_ (mI, m) ptp
33.91 +\<close> ML \<open>
33.92 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI, m), ptp);
33.93 +\<close> ML \<open>
33.94 + Solve.solve m (pt, pos);
33.95 +\<close> ML \<open>
33.96 +"~~~~~ fun solve , args:"; val (("Check_Postcond", Tactic.Check_Postcond' (pI, _)), (pt, (p, p_)))
33.97 + = (m, (pt, pos));
33.98 +\<close> ML \<open>
33.99 +\<close> ML \<open>
33.100 + val pp = par_pblobj pt p
33.101 +\<close> ML \<open>
33.102 +(*+*)(p, p_) = ([4, 4, 5], Res);
33.103 +\<close> ML \<open>
33.104 +(*+*)pp = [4, 4];
33.105 +\<close> ML \<open>
33.106 +(*+*)get_obj I pt (fst pos);
33.107 +\<close> ML \<open>
33.108 +PrfObj;
33.109 +\<close> ML \<open>
33.110 + val Check_elementwise "Assumptions" = (*case*) get_obj g_tac pt p (*of*);
33.111 +(* this ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ should be dropped asap *)
33.112 +\<close> ML \<open>
33.113 +show_pt_tac pt
33.114 +\<close> ML \<open>
33.115 +\<close> ML \<open>
33.116 +\<close> ML \<open>
33.117 +\<close> ML \<open>
33.118 +\<close> ML \<open>
33.119 +\<close> ML \<open>
33.120 +\<close> ML \<open>
33.121 (*\\--9 end step into relevant call ----------------------------------------------------------//*)
33.122 \<close> ML \<open>
33.123 -(*+*)if p = ([4, 4], Res) andalso fst nxt = "Check_Postcond" andalso
33.124 -(*+*)terms2str (get_assumptions_ pt p) = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"
33.125 +(*+*)if p''''' = ([4, 4], Res) andalso fst nxt''''' = "Check_Postcond" andalso
33.126 +(*+*)terms2str (get_assumptions_ pt''''' p''''') = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"x = 0\",\"x = 6 / 5\"]"
33.127 (*+*)then () else error "AFTER 8 changed";
33.128 \<close> ML \<open>
33.129 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_elementwise "Assumptions"*)
33.130 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [1] pt''''';(*Check_elementwise "Assumptions"*)
33.131 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["rational", "univariate", "equation"]*)
33.132 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*End_Proof'*)
33.133 \<close> ML \<open>
33.134 @@ -204,189 +253,13 @@
33.135 "~~~~~ fun xxx , args:"; val () = ();
33.136 \<close>
33.137
33.138 -section \<open>============= code for tactic.sml ========================================\<close>
33.139 -ML \<open>
33.140 -(* keep for re-build locate_input_tactic with Tactic.from_program *)
33.141 -\<close> ML \<open>
33.142 -Term.exists_Const
33.143 -\<close> ML \<open>
33.144 -\<close> ML \<open>
33.145 -\<close> ML \<open>
33.146 -\<close> ML \<open>
33.147 -\<close> ML \<open>
33.148 -\<close> ML \<open>
33.149 -\<close>
33.150 -
33.151 -section \<open>=========="Minisubpbl/300-init-subpbl.sml" ========================================\<close>
33.152 -ML \<open>
33.153 -"~~~~~ fun xxx , args:"; val () = ();
33.154 -\<close> ML \<open>
33.155 -(* Title: "Minisubpbl/300-init-subpbl.sml"
33.156 - Author: Walther Neuper 1105
33.157 - (c) copyright due to lincense terms.
33.158 -*)
33.159 -(* keep for re-build locate_input_tactic with Tactic.from_program *)
33.160 -"----------- Minisubpbl/300-init-subpbl.sml ----------------------";
33.161 -"----------- Minisubpbl/300-init-subpbl.sml ----------------------";
33.162 -"----------- Minisubpbl/300-init-subpbl.sml ----------------------";
33.163 -val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
33.164 -val (dI',pI',mI') =
33.165 - ("Test", ["sqroot-test","univariate","equation","test"],
33.166 - ["Test","squ-equ-test-subpbl1"]);
33.167 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
33.168 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.169 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.170 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.171 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.172 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.173 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.174 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.175 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.176 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33.177 -val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem"*)
33.178 -(*//--1 begin step into relevant call -----------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-----\\
33.179 - 1 relevant for updating ctxt *)
33.180 -\<close> ML \<open>
33.181 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''', p''', [], pt''');
33.182 -\<close> ML \<open>
33.183 -"~~~~~ fun locatetac , args:"; val (tac, ptp as (pt, p)) = (tac, (pt''',p'''));
33.184 -val (mI,m) = mk_tac'_ tac;
33.185 -val Appl m = applicable_in p pt m;
33.186 -member op = specsteps mI; (*false*)
33.187 -(*val Updated (cs' as (_,_,(_,p'))) = loc_solve_ (mI,m) ptp;*)
33.188 -"~~~~~ fun loc_solve_, args:"; val (m, (pt,pos)) = ((mI,m), ptp);
33.189 -(*val (msg, cs') = solve m (pt, pos);*)
33.190 -"~~~~~ fun solve , args:"; val ((mI,m), (pt, po as (p,p_))) = (m, (pt, pos));
33.191 -e_metID = get_obj g_metID pt (par_pblobj pt p) (*false*);
33.192 - val thy' = get_obj g_domID pt (par_pblobj pt p);
33.193 - val (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt;
33.194 -
33.195 - locate_input_tactic sc (pt, po) (fst is) (snd is) m;
33.196 -"~~~~~ fun locate_input_tactic , args:"; val (progr, cstate, istate, ctxt, tac)
33.197 - = (sc, (pt, po), (fst is), (snd is), m);
33.198 - val srls = get_simplifier cstate;
33.199 -
33.200 - (*case*) execute_progr_2 srls m cstate (progr, e_rls(*!!!*)) (istate, ctxt)(*of*);
33.201 -"~~~~~ fun execute_progr_2 , args:"; val (((*thy',*) srls), m, (pt, p), (scr as Rule.Prog sc, d), (Istate.ScrState (E,l,a,v,S,b), ctxt))
33.202 - = (srls, m, cstate, (progr, e_rls(*!!!*)), (istate, ctxt));
33.203 - (*if*)l = [] orelse ((*init.in solve..Apply_Method...*)
33.204 - (last_elem o fst) p = 0 andalso snd p = Res) (*else*);
33.205 -(*val Assoc (iss as (is as (_,_,_,_,_,bb), ss as ((m',f',pt',p',c')::_))) =
33.206 - (astep_up (thy',srls,scr,d) ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );*)
33.207 -"~~~~~ fun astep_up, args:"; val ((ys as (_,_,Prog sc,_)), ((E,l,a,v,S,b),ss: step list)) =
33.208 - ((ctxt,srls,scr,d), ((E,l,a,v,S,b), [(m,EmptyMout,pt,p,[])]) );
33.209 - (*if*) 1 < length l (*true*);
33.210 -val up = drop_last l;
33.211 -
33.212 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
33.213 -"~~~~~ fun ass_up, args:"; val (ysa, iss, (Const ("Script.Try",_) $ e)) =
33.214 - (ys, ((E,up,a,v,S,b),ss), (go up sc));
33.215 - astep_up ysa iss;
33.216 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
33.217 - (*if*) 1 < length l; (*then*)
33.218 - val up = drop_last l;
33.219 -
33.220 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
33.221 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ )) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
33.222 -
33.223 - astep_up ysa iss (*2*: comes from e2*);
33.224 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
33.225 - (*if*) 1 < length l; (*then*)
33.226 - val up = drop_last l;
33.227 -
33.228 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
33.229 -"~~~~~ fun ass_up , args:"; val (ysa, iss, (Const ("Script.Seq",_) $ _ $ _ $ _)) = (ys, ((E,up,a,v,S,b),ss), (go up sc));
33.230 -
33.231 - astep_up ysa iss (*all has been done in (*2*) below*);
33.232 -"~~~~~ and astep_up , args:"; val ((ys as (_,_,Rule.Prog sc,_)), ((E,l,a,v,S,b),ss)) = (ysa, iss);
33.233 - (*if*) 1 < length l; (*then*)
33.234 - val up = drop_last l;
33.235 -
33.236 - ass_up ys ((E,up,a,v,S,b),ss) (go up sc);
33.237 -"~~~~~ fun ass_up , args:"; val ((ys as (ctxt,s,Rule.Prog sc,d)), ((E,l,a,v,S,b),ss), (Const ("HOL.Let",_) $ _))
33.238 - = (ys, ((E,up,a,v,S,b),ss), (go up sc));
33.239 - val l = drop_last l; (*comes from e, goes to Abs*)
33.240 - val (i, T, body) =
33.241 - (case go l sc of
33.242 - Const ("HOL.Let",_) $ _ $ (Abs (i, T, body)) => (i, T, body)
33.243 - | t => error ("ass_up..HOL.Let $ _ with " ^ Rule.term2str t))
33.244 - val i = TermC.mk_Free (i, T);
33.245 - val E = LTool.upd_env E (i, v);
33.246 -
33.247 - (*case*) assy (ctxt,s,d,Aundef) ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss) body (*of*);
33.248 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:Lucin.step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body))))
33.249 - = ((ctxt,s,d,Aundef), ((E, l @ [Celem.R, Celem.D], a,v,S,b),ss), body);
33.250 -
33.251 - (*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
33.252 - (* here is not a tactical like TRY etc, but a tactic creating a step of calculation *)
33.253 -"~~~~~ fun assy , args:"; val ((ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss:step list), t)
33.254 - = (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
33.255 -\<close> ML \<open>
33.256 -(*val (a', LTool.STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac" sr E a v t (*of*);
33.257 -\<close> ML \<open>
33.258 -"~~~~~ fun handle_leaf , args:"; val (call, thy, srls, E, a, v, t)
33.259 - = ("locate", "Isac", sr, E, a, v, t);
33.260 -\<close> ML \<open>
33.261 - val (a', LTool.STac stac) = (*case*) LTool.subst_stacexpr E a v t (*of*);
33.262 -\<close> ML \<open>
33.263 -"~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Script.SubProblem", _) $ _ $ _)))
33.264 - = (E, a, v, t);
33.265 -\<close> ML \<open>
33.266 -(NONE, STac (subst_atomic E t)); (*return value*)
33.267 -\<close> ML \<open>
33.268 -"~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', LTool.STac stac))
33.269 - = ((NONE : term option, STac (subst_atomic E t)));
33.270 -\<close> ML \<open>
33.271 - val stac' =
33.272 - Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (upd_env_opt E (a,v)) stac)
33.273 -\<close> ML \<open>
33.274 -(a', LTool.STac stac'); (*return value*)
33.275 -\<close> ML \<open>
33.276 -"~~~~~ from handle_leaf to assy return val:"; val (a', LTool.STac stac)
33.277 - = ((a' : term option, LTool.STac stac'));
33.278 - val p' =
33.279 - case p_ of Frm => p
33.280 - | Res => lev_on p
33.281 - | _ => error ("assy: call by " ^ pos'2str (p,p_));
33.282 -\<close> ML \<open>
33.283 - (**)val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt m stac (*of*);
33.284 -\<close> ML \<open>
33.285 - val (p'',c',f',pt') =
33.286 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.ScrState (E,l,a',v',S,true), ctxt) (p',p_) pt;
33.287 -\<close> ML \<open>
33.288 -m
33.289 -\<close> ML \<open>
33.290 -(*+*)if is_e_ctxt ctxt then error "ERROR: assy returns e_ctxt" else ();
33.291 -(*\\--1 end step into relevant call ----------------------------------------------------------//*)
33.292 -\<close> ML \<open>
33.293 -
33.294 -val (p,_,f,nxt,_,pt) = me nxt''' p''' [1] pt''';
33.295 -\<close> ML \<open>
33.296 -if p = ([3], Pbl) andalso not (get_ctxt pt p |> is_e_ctxt)
33.297 -then
33.298 - case nxt of ("Model_Problem", _) => ()
33.299 - | _ => error "minisubpbl: CalcTreeTEST has no nxt = Model_Problem"
33.300 -else error "Minisubpbl/300-init-subpbl.sml changed";
33.301 -
33.302 -\<close> ML \<open>
33.303 -\<close> ML \<open>
33.304 -"~~~~~ fun xxx , args:"; val () = ();
33.305 -\<close>
33.306 -
33.307 -section \<open>===================================================================================\<close>
33.308 -ML \<open>
33.309 -"~~~~~ fun xxx , args:"; val () = ();
33.310 -\<close> ML \<open>
33.311 -\<close> ML \<open>
33.312 -\<close> ML \<open>
33.313 -"~~~~~ fun xxx , args:"; val () = ();
33.314 -\<close>
33.315 -
33.316 section \<open>code for copy & paste ===============================================================\<close>
33.317 ML \<open>
33.318 "~~~~~ fun xxx , args:"; val () = ();
33.319 -"~~~~~ and xxx , args:"; val () = ();
33.320 -
33.321 -"~~~~~ to xxx return val:"; val () = ();
33.322 +"~~~~~ and xxx , args:"; val () = ();
33.323 +"~~~~~ from xxx to yyy return val:"; val ((*yyy*)) = ((*xxx*));
33.324 +(*if*) (*then*); (*else*); (*case*) (*of*); (*return value*);
33.325 +"xx"
33.326 +^ "xxx" (*+*)
33.327 \<close>
33.328 end