# HG changeset patch # User Walther Neuper # Date 1565352253 -7200 # Node ID 60d19140259838420e57eaeab4fa63383bf47d3e # Parent b311a0634eca8fbc51e0605dcb89a5eaeb81e881 separater structure ContextC diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Build_Isac.thy Fri Aug 09 14:04:13 2019 +0200 @@ -19,6 +19,7 @@ theory ListC imports "~~/src/Tools/isac/KEStore" ML_file "~~/src/Tools/isac/ProgLang/termC.sml" + ML_file "~~/src/Tools/isac/ProgLang/contextC.sml" ML_file "~~/src/Tools/isac/ProgLang/calculate.sml" ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml" theory Tools imports ListC begin diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/appl.sml --- a/src/Tools/isac/Interpret/appl.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/appl.sml Fri Aug 09 14:04:13 2019 +0200 @@ -225,7 +225,7 @@ val {where_, ...} = Specify.get_pbt pI val pres = map (Model.mk_env probl |> subst_atomic) where_ val ctxt = if is_e_ctxt ctxt - then Celem.assoc_thy dI |> Proof_Context.init_global |> Stool.insert_assumptions pres + then Celem.assoc_thy dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres else ctxt (*TODO.WN110416 here do evalprecond according to fun check_preconds' and then decide on Chead.Notappl/Appl accordingly once more. diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/calchead.sml --- a/src/Tools/isac/Interpret/calchead.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/calchead.sml Fri Aug 09 14:04:13 2019 +0200 @@ -1307,7 +1307,7 @@ val {ppc, ...} = Specify.get_met mI val (_, vals) = oris2fmz_vals pors val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global - |> Stool.declare_constraints' vals + |> ContextC.declare_constraints' vals val pt = update_pblppc pt p (map (ori2Coritm ppc) pors) val pt = update_metppc pt p (map (ori2Coritm ppc) pors) (*WN110716 = _pblppc ?!?*) val pt = update_spec pt p (dI, pI, mI) diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/ctree-basic.sml --- a/src/Tools/isac/Interpret/ctree-basic.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Fri Aug 09 14:04:13 2019 +0200 @@ -548,7 +548,7 @@ then get_loc pt pos |> #2 (*for script interpretation rely on fun get_loc*) else get_obj g_ctxt pt p (*for specify phase take ctx from PblObj*) -fun get_assumptions_ pt p = get_ctxt pt p |> Stool.get_assumptions; +fun get_assumptions_ pt p = get_ctxt pt p |> ContextC.get_assumptions; fun get_somespec' (dI, pI, mI) (dI', pI', mI') = let diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/generate.sml --- a/src/Tools/isac/Interpret/generate.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/generate.sml Fri Aug 09 14:04:13 2019 +0200 @@ -269,7 +269,7 @@ end | generate1 _ (Tactic.Rewrite_Inst' (_, _, _, _, subs', thm', f, (f', asm))) (is, ctxt) (p, _) pt = let - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f (Tactic.Rewrite_Inst (Selem.subst2subs subs', thm')) (f',asm) Complete; val pt = update_branch pt p TransitiveB in @@ -277,7 +277,7 @@ end | generate1 _ (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt = let - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f (Tactic.Rewrite thm') (f', asm) Complete val pt = update_branch pt p TransitiveB in @@ -286,7 +286,7 @@ | generate1 thy (Tactic.Rewrite_Asm' all) l p pt = generate1 thy (Tactic.Rewrite' all) l p pt | generate1 _ (Tactic.Rewrite_Set_Inst' (_, _, subs', rls', f, (f', asm))) (is, ctxt) (p, _) pt = let - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs', Rule.id_rls rls')) (f', asm) Complete val pt = update_branch pt p TransitiveB in @@ -294,7 +294,7 @@ end | generate1 thy (Tactic.Detail_Set_Inst' (_, _, subs, rls, f, (_, asm))) (is, ctxt) (p, _) pt = let - val ctxt' = Stool.insert_assumptions asm ctxt + val ctxt' = ContextC.insert_assumptions asm ctxt val (pt, _) = cappend_form pt p (is, ctxt') f val pt = update_branch pt p TransitiveB val is = init_istate (Tactic.Rewrite_Set_Inst (Selem.subst2subs subs, Rule.id_rls rls)) f @@ -305,7 +305,7 @@ end | generate1 _ (Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))) (is, ctxt) (p, _) pt = let - val (pt, c) = cappend_atomic pt p (is, Stool.insert_assumptions asm ctxt) f + val (pt, c) = cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f (Tactic.Rewrite_Set (Rule.id_rls rls')) (f',asm) Complete val pt = update_branch pt p TransitiveB in @@ -313,7 +313,7 @@ end | generate1 thy (Tactic.Detail_Set' (_, _, rls, f, (_, asm))) (is, ctxt) (p, _) pt = let - val ctxt' = Stool.insert_assumptions asm ctxt + val ctxt' = ContextC.insert_assumptions asm ctxt val (pt, _) = cappend_form pt p (is, ctxt') f val pt = update_branch pt p TransitiveB val is = init_istate (Tactic.Rewrite_Set (Rule.id_rls rls)) f @@ -373,9 +373,9 @@ val f = get_curr_formula (pt, pos) val pos' as (p', _) = (lev_on p, Res) val (pt, _) = case subs_opt of - NONE => cappend_atomic pt p' (is, Stool.insert_assumptions [] ctxt) f + NONE => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f (Tactic.Rewrite thm') (f', []) Inconsistent - | SOME subs => cappend_atomic pt p' (is, Stool.insert_assumptions [] ctxt) f + | SOME subs => cappend_atomic pt p' (is, ContextC.insert_assumptions [] ctxt) f (Tactic.Rewrite_Inst (subs, thm')) (f', []) Inconsistent val pt = update_branch pt p' TransitiveB in (pt, pos') end diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/lucas-interpreter.sml --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Fri Aug 09 14:04:13 2019 +0200 @@ -687,7 +687,7 @@ val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of (Istate.ScrState (E,l,a,_,_,b), ctxt') => (E, l, a, b, ctxt') | _ => error "begin_end_prog Check_Postcond' script of parpbl: uncovered case get_loc" - val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt' + val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt' val tac_ = Tactic.Check_Postcond' (pI, (scval, asm)) val is = Istate.ScrState (E,l,a,scval,scsaf,b) val ((p, p_), ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt'') (pp, Res) pt; diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/model.sml --- a/src/Tools/isac/Interpret/model.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/model.sml Fri Aug 09 14:04:13 2019 +0200 @@ -45,8 +45,6 @@ val mk_env : itm list -> (term * term) list (* close to Chead.all_dsc_in, Chead.is_error, etc *) val max_vt : itm list -> int - val dest_list' : term -> term list - (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) type penv val penv2str_ : Proof.context -> penv -> string (* NONE *) @@ -124,9 +122,6 @@ fun is_var (Free _) = true | is_var _ = false; -(* this may decompose an object-language isa-list; - use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*) -fun dest_list' t = if TermC.is_list t then TermC.isalist2list t else [t]; (* special handling for lists. ?WN:14.5.03 ??!? *) fun dest_list (d, ts) = let fun dest t = @@ -172,13 +167,13 @@ then if LTool.is_list_dsc d andalso TermC.is_list arg andalso LTool.is_unl d |> not then (d, take_apart arg) else (d, [arg]) - else (Rule.e_term, dest_list' t) + else (Rule.e_term, TermC.dest_list' t) | split_dts t = let val t' as (h, _) = strip_comb t; in if LTool.is_dsc h then (h, dest_list t') - else (Rule.e_term, dest_list' t) + else (Rule.e_term, TermC.dest_list' t) end; (* version returning ts only *) fun split_dts' (d, arg) = @@ -190,7 +185,7 @@ else (take_apart arg) (* [a,b] --> SML[ [a], [b] ]SML *) else ([arg]) (* a variable or metavariable for a list *) else ([arg]) - else (dest_list' arg) + else (TermC.dest_list' arg) (* WN170204: Warning "redundant" | split_dts' (d, t) = (*either dsc or term; 14.5.03 only copied*) let val (h,argl) = strip_comb t diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/mstools.sml --- a/src/Tools/isac/Interpret/mstools.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/mstools.sml Fri Aug 09 14:04:13 2019 +0200 @@ -12,12 +12,6 @@ val check_preconds : 'a -> Rule.rls -> term list -> Model.itm list -> (bool * term) list val check_preconds' : Rule.rls -> term list -> Model.itm list -> 'a -> (bool * term) list - val get_assumptions : Proof.context -> term list - val insert_assumptions : term list -> Proof.context -> Proof.context - val declare_constraints : string -> Proof.context -> Proof.context - val declare_constraints' : term list -> Proof.context -> Proof.context - val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context - datatype match_ = Match_ of Celem.pblID * (Model.itm list * (bool * term) list) | NoMatch_ val refined_ : match_ list -> match_ option datatype match = Matches of Celem.pblID * Model.item Model.ppc | NoMatch of Celem.pblID * Model.item Model.ppc @@ -27,7 +21,7 @@ val pres2str : (bool * term) list -> string val refined : match list -> Celem.pblID (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) - val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context + (*NONE*) ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) (*----- unused code, kept as hints to design ideas ---------------------------------------------*) @@ -95,43 +89,6 @@ in map (evalprecond prls) pres' end; fun check_preconds _(*thy*) prls pres pbl = check_preconds' prls pres pbl (Model.max_vt pbl); -fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt; -(*WN110613 fun declare_constraints' shall replace fun declare_constraints*) -fun declare_constraints t ctxt = - let - fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of - (_, _ :: _) => (Free (v, T) :: get_vars vs) - | (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*) - | get_vars [] = []; - val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars; - in fold Variable.declare_constraints ts ctxt end; - -structure Context_Data = Proof_Data (type T = term list fun init _ = []); -fun get_assumptions ctxt = Context_Data.get ctxt -fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs)) - -(* transfer assumptions from one to another ctxt. - does NOT respect scope: in a calculation identifiers are unique. - but environments are scoped as usual in Luacs-interpretation. - WN110520 redo (1) take declare_constraints (2) with combinators*) -fun transfer_asms_from_to from_ctxt to_ctxt = - let - val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat - fun transfer [] to_ctxt = to_ctxt - | transfer (from_asm :: fas) to_ctxt = - if inter op = (TermC.vars from_asm) to_vars = [] - then transfer fas to_ctxt - else transfer fas (insert_assumptions [from_asm] to_ctxt) - in transfer (get_assumptions from_ctxt) to_ctxt end - -(* exported from a subproblem to the context of the calling method: - # 'scrval': the result of script interpretation and - # those assumptions in the subproblem wich contain a variable known - in the calling method. *) -fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt = - let - val caller_ctxt = (scrval |> Model.dest_list' |> insert_assumptions) caller_ctxt - in transfer_asms_from_to sub_ctxt caller_ctxt end; fun common_subthy (thy1, thy2) = if Context.subthy (thy1, thy2) then thy2 diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/ptyps.sml --- a/src/Tools/isac/Interpret/ptyps.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/ptyps.sml Fri Aug 09 14:04:13 2019 +0200 @@ -226,7 +226,7 @@ fun prep_ori [] _ _ = ([], Selem.e_ctxt) | prep_ori fmz thy pbt = let - val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz; + val ctxt = Proof_Context.init_global thy |> fold ContextC.declare_constraints fmz; val ori = map (add_field thy pbt o Model.split_dts o the o TermC.parseNEW ctxt) fmz |> add_variants; val maxv = map fst ori |> max; val maxv = if maxv = 0 then 1 else maxv; diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/script.sml --- a/src/Tools/isac/Interpret/script.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/script.sml Fri Aug 09 14:04:13 2019 +0200 @@ -233,7 +233,7 @@ val {cas,ppc,thy,...} = Specify.get_pbt pI val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*) val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt)); - val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals + val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> ContextC.declare_constraints' vals val hdl = case cas of NONE => LTool.pblterm dI pI @@ -392,7 +392,7 @@ val {cas, ppc, thy, ...} = Specify.get_pbt pI val dI = Rule.theory2theory' thy (*take dI from _refined_ pbl*) val dI = Rule.theory2theory' (Stool.common_subthy (Celem.assoc_thy dI, rootthy pt)) - val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> Stool.declare_constraints' vals + val ctxt = dI |> Rule.Thy_Info_get_theory |> Proof_Context.init_global |> ContextC.declare_constraints' vals val hdl = case cas of NONE => LTool.pblterm dI pI @@ -582,10 +582,10 @@ in relate_args (env @ [(f, a)]) ff (remove op = a aas) end val env = relate_args [] formals actuals; val _ = trace_istate env; - val ctxt = Proof_Context.init_global thy |> Stool.declare_constraints' actuals + val ctxt = Proof_Context.init_global thy |> ContextC.declare_constraints' actuals val {pre, prls, ...} = Specify.get_met metID; val pres = Stool.check_preconds thy prls pre itms |> map snd; - val ctxt = ctxt |> Stool.insert_assumptions pres; + val ctxt = ctxt |> ContextC.insert_assumptions pres; in (Istate.ScrState (env, [], NONE, Rule.e_term, Istate.Safe, true), ctxt, scr) end; end (*local*) diff -r b311a0634eca -r 60d191402598 src/Tools/isac/Interpret/solve.sml --- a/src/Tools/isac/Interpret/solve.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/Interpret/solve.sml Fri Aug 09 14:04:13 2019 +0200 @@ -137,7 +137,7 @@ in case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of LucinNEW.Safe_Step (cstate, istate, ctxt, tac) => - ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate)) + ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut?*)], cstate)) | _ => (* NotLocatable *) let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, Frm) pt; in @@ -185,7 +185,7 @@ val (E, l, a, b, ctxt') = case get_loc pt (pp, Frm) of (Istate.ScrState (E, l, a, _, _, b), ctxt') => (E, l, a, b, ctxt') | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc" - val ctxt'' = Stool.from_subpbl_to_caller ctxt scval ctxt' + val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt' val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm))) (Istate.ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt; in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)), diff -r b311a0634eca -r 60d191402598 src/Tools/isac/ProgLang/ListC.thy --- a/src/Tools/isac/ProgLang/ListC.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/ProgLang/ListC.thy Fri Aug 09 14:04:13 2019 +0200 @@ -8,6 +8,7 @@ begin ML_file "~~/src/Tools/isac/ProgLang/termC.sml" +ML_file "~~/src/Tools/isac/ProgLang/contextC.sml" ML_file "~~/src/Tools/isac/ProgLang/calculate.sml" ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml" ML \ diff -r b311a0634eca -r 60d191402598 src/Tools/isac/ProgLang/contextC.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/isac/ProgLang/contextC.sml Fri Aug 09 14:04:13 2019 +0200 @@ -0,0 +1,218 @@ +(* Title: ../contextC.sml + Author: Walther Neuper, Mathias Lehnfeld + (c) due to copyright terms +*) +(* Extension to Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) +signature CONTEXT_C = +sig + val declare_constraints : string -> Proof.context -> Proof.context + val declare_constraints' : term list -> Proof.context -> Proof.context + val get_assumptions : Proof.context -> term list + val insert_assumptions : term list -> Proof.context -> Proof.context + val from_subpbl_to_caller : Proof.context -> term -> Proof.context -> Proof.context +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) + (*NONE*) +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) + val transfer_asms_from_to : Proof.context -> Proof.context -> Proof.context +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) +end + +(* survey on handling contexts: +------------------------------- + theory is required for Pattern.match (and thus for Tactic.Rewrite* ), while + ctxt is required for parsing and for managing pre-conditions and assumptions. + * model-specify-phase: + * Tactic.Model_Problem does declare_constraints for parsing (in Tactic.Add_Given, etc) + ("insert_assumptions pres" has to wait for completing Tactic.Add_Given, etc) + (Tactic.Refine_Problem uses theory NOT ctxt due to Pattern.match) + * + * + * solve-phase by Lucas-Interpretation: + * locate_input_tactic: + * Tactic.Apply_Method + * initialises ctxt (declare_constraints' + insert_assumptions pres) by init_scrstate + * in solve for root problem + * in begin_end_prog for subproblem + * Tactic.Rewrite* create assumptions; respective insert_assumptions is done by associate + * associate..Subproblem' returns ctxt ONLY with declare_constraints', + with insert_assumptions wait for Tactic.Apply_Method + * storing ctxt is done after return form locate_input_tactic + * determine_next_tactic: + * TODO initialises ctxt by TODO + * Tactic.Rewrite* create assumptions; respective insert_assumptions TODO + * + * + * + * locate_input_formula: follows sig. of determine_next_tactic + * changing from one method to another (in determine_next_tactic only): + * from method to sub-program: just add new preconditions of the guard + * locate_input_tactic: init_scrstate by begin_end_prog + * determine_next_tactic: + * from_subpbl_to_caller + * finishing a method: + * Tactic.Check_Postcond' uses ctxt for proving the post-condition (not yet implemented) + * + * + * + * +================================================================================================ +call hierarchy +================================================================================================ + + locatetac + applicable_in (p, p_) pt (Tactic.Apply_Method pres + insert_assumptions + + context_thy + applicable_in (p, p_) pt (Tactic.Apply_Method pres + insert_assumptions + + + + + + + generate1 _ (Tactic.Rewrite*** + insert_assumptions + + + + + +------------------------------------------------------------------------------------------------ +solve phase before LI +------------------------------------------------------------------------------------------------ +autocalc + all_modspec + declare_constraints' + complete_solve + all_modspec + declare_constraints' + +all_solve + begin_end_prog (Tactic.Apply_Method' + init_scrstate + declare_constraints' + insert_assumptions + +nxt_specify_ + begin_end_prog (Tactic.Apply_Method' + init_scrstate + declare_constraints' + insert_assumptions +------------------------------------------------------------------------------------------------ +LI +------------------------------------------------------------------------------------------------ +solve ("Apply_Method" root-program + init_scrstate + declare_constraints' + insert_assumptions + locate_input_tactic + execute_progr_2 + assy ..leaf sub-program + associate + declare_constraints' + applicable_in .. Tactic.Apply_Method pres + insert_assumptions + ? generate1 (look in test with "from ... to..)) + +determine_next_tactic + execute_progr_1 + appy ..leaf + stac2tac_ + declare_constraints' + applicable_in (p, p_) pt (Tactic.Apply_Method pres + insert_assumptions + ? generate1 (look in test with "from ... to..)) + +locate_input_formula uses determine_next_tactic + compare_step + all_modspec + declare_constraints' + begin_end_prog (Tactic.Apply_Method' + init_scrstate + declare_constraints' + insert_assumptions +------------------------------------------------------------------------------------------------ +specification phase +------------------------------------------------------------------------------------------------ + loc_specify_ + specify (Tactic.Init_Proof' + prep_ori + declare_constraints + + CalcTree + nxt_specify_init_calc + prep_ori + declare_constraints + + modifyCalcHead + input_icalhd + prep_ori + declare_constraints + + refine + refin' + prep_ori + declare_constraints +------------------------------------------------------------------------------------------------ +unused ?! +------------------------------------------------------------------------------------------------ + ?? + match_pbl + prep_ori + declare_constraints + ?? + from_pblobj' + init_scrstate + declare_constraints' + insert_assumptions + ?? + tac2tac_ + applicable_in (p, p_) pt (Tactic.Apply_Method pres + insert_assumptions + +*) + +structure ContextC(**) : CONTEXT_C(**) = +struct + +fun declare_constraints' ts ctxt = fold Variable.declare_constraints (flat (map TermC.vars ts)) ctxt; +(*WN110613 fun declare_constraints' shall replace fun declare_constraints*) +fun declare_constraints t ctxt = + let + fun get_vars ((v, T) :: vs) = (case raw_explode v |> Library.read_int of + (_, _ :: _) => (Free (v, T) :: get_vars vs) + | (_, [] ) => get_vars vs) (*filter out nums as long as we have Free ("123",_)*) + | get_vars [] = []; + val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars; + in fold Variable.declare_constraints ts ctxt end; + +structure Context_Data = Proof_Data (type T = term list fun init _ = []); +fun get_assumptions ctxt = Context_Data.get ctxt +fun insert_assumptions asms = Context_Data.map (fn xs => distinct (asms @ xs)) + +(* transfer assumptions from one to another ctxt. + does NOT respect scope: in a calculation identifiers are unique. + but environments are scoped as usual in Luacs-interpretation. + WN110520 redo (1) take declare_constraints (2) with combinators*) +fun transfer_asms_from_to from_ctxt to_ctxt = + let + val to_vars = get_assumptions to_ctxt |> map TermC.vars |> flat + fun transfer [] to_ctxt = to_ctxt + | transfer (from_asm :: fas) to_ctxt = + if inter op = (TermC.vars from_asm) to_vars = [] + then transfer fas to_ctxt + else transfer fas (insert_assumptions [from_asm] to_ctxt) + in transfer (get_assumptions from_ctxt) to_ctxt end + +(* exported from a subproblem to the context of the calling method: + # 'scrval': the result of script interpretation and + # those assumptions in the subproblem wich contain a variable known + in the calling method. *) +fun from_subpbl_to_caller sub_ctxt scrval caller_ctxt = + let + val caller_ctxt = (scrval |> TermC.dest_list' |> insert_assumptions) caller_ctxt + in transfer_asms_from_to sub_ctxt caller_ctxt end; + +end diff -r b311a0634eca -r 60d191402598 src/Tools/isac/ProgLang/termC.sml --- a/src/Tools/isac/ProgLang/termC.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/ProgLang/termC.sml Fri Aug 09 14:04:13 2019 +0200 @@ -4,7 +4,8 @@ *) infix contains_one_of -signature TERMC = +(* TERM_C extends Isabelle's naming conventions: "C" indicates Isac add-ons to an Isabelle module *) +signature TERM_C = sig val contains_Var: term -> bool val dest_binop_typ: typ -> typ * typ * typ @@ -71,6 +72,7 @@ val var2free: term -> term val vars: term -> term list val vars_of : term -> term list (* probably should replace "fun vars" *) + val dest_list' : term -> term list (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) val scala_of_term: term -> string @@ -88,7 +90,7 @@ end (**) -structure TermC(**): TERMC(**) = +structure TermC(**): TERM_C(**) = struct (**) @@ -546,4 +548,8 @@ val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord in (map (var_for [] t) var_ids) |> flat |> distinct end +(* this may decompose an object-language isa-list; + use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*) +fun dest_list' t = if is_list t then isalist2list t else [t]; + end \ No newline at end of file diff -r b311a0634eca -r 60d191402598 src/Tools/isac/TODO.thy --- a/src/Tools/isac/TODO.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/src/Tools/isac/TODO.thy Fri Aug 09 14:04:13 2019 +0200 @@ -16,7 +16,27 @@ \item xxx \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper \item check in states: length ?? > 1 with tracing these cases + \item rename ScrState --> Program_State + \item locate_input_tactic arg: type istate ((ScrState is)) + result: type scrstate ((is)) ... unify + readable paper! + rename ? ^^^^^^^^ prog_state, pstate + \item script: rename AssWeak --> Ass_Weak + \item script.associate: remove ctxt from Subproblem' -- analogous Rewrite'... + \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac") + \item lucas-intrpreter.locate_input_tactic: execute_progr_2 srls tac cstate (progr, Rule.e_rls) + ^^^^^^^^^^ + \item Lucin.associate: ctree -> Proof.context -> Tactic.T -> term -> Lucin.ass + -----> : ctree -> Proof.context -> (Tactic.T * term) -> Lucin.ass + \item ?delete Check_Postcond' in begin_end_prog (already done in solve?) + in case both are needed, unify ! + \item rm ctxt from Subproblem' (is separated in associate!)) \item xxx + \item comoplete mstools.sml (* survey on handling contexts: + \item collect ctxt to structure ContextC + address all uses of insert_assumptions here + \item xxx + \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur. + \item xxx + \item check Tactic.Subproblem': are 2 terms required? \item xxx \item xxx \end{itemize} @@ -24,6 +44,10 @@ subsection \Postponed from current changeset\ text \ \begin{itemize} + \item xxx + \item rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl + \item xxx + \item xxx \item language definition: use (f #> g) x = x |> f |> g instead of @ see implementation.pdf p.16 \item xxx @@ -32,9 +56,19 @@ \begin{itemize} \item 1. check if Ctree.state can be updated OUTSIDE determine_next_step \item 2. fun locate_input_tactic: pull generate1 out (because it stores ctxt also in cstate) - \item xxx + \item \item xxx \end{itemize} + \item concentracte "insert_assumptions" in "associate" ?for determine_next_tactic ?where? + \begin{itemize} + \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?) + \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml)) + \item ?"insert_assumptions" necessary in "init_scrstate" ?+++? in "applicable_in" ?+++? "associate" + \item xxx + \item xxx + \item DO DELETIONS AFTER analogous concentrations in determine_next_tactic + \end{itemize} + \item xxx \item xxx \item xxx \item inform: TermC.parse (Celem.assoc_thy "Isac") istr --> parseNEW context istr @@ -51,6 +85,9 @@ \item Diff.thy: differentiateX --> differentiate after removal of script-constant \item Test.thy: met_test_sqrt2: deleted?! \item xxx + \item drop "init_form" and use "Take" in programs (start with latter!) + \item Applicable.applicable_in --> Applicable.tactic_at + \item Const ("Script.SubProblem", _) --> Const ("Program.SubProblem", _):rename! separate? \item xxx \item xxx \end{itemize} @@ -162,10 +199,17 @@ subsection \replace theory/thy by context/ctxt\ text \ \begin{itemize} + \item cleaup the many conversions string -- theory + \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ? \item 1. Rewrite.eval_true_, then Lucin.handle_leaf, Rewrite.eval_listexpr_, Generate.generate1, Lucin.stac2tac. + \item fun associate + let val thy = Celem.assoc_thy "Isac";(*TODO*) \item xxx \item xxx + \item xxx + \item !!! Tactic.Refine_Problem uses Pattern.match, which takes a theory, NOT a ctxt + but there is Proof_Context.theory_of !!! \end{itemize} \ subsection \Rfuns, Begin_/End_Detail', Rrls\ diff -r b311a0634eca -r 60d191402598 test/Tools/isac/ADDTESTS/All_Ctxt.thy --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Fri Aug 09 14:04:13 2019 +0200 @@ -104,7 +104,7 @@ ML \ "artifically inject assumptions"; val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p); - val ctxt = Stool.insert_assumptions [TermC.str2term "x < sub_asm_out", + val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out", TermC.str2term "a < sub_asm_local"] cres; val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt)); \ diff -r b311a0634eca -r 60d191402598 test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Aug 09 14:04:13 2019 +0200 @@ -126,7 +126,7 @@ Isabelle can handle best.\ ML \ val ctxt = Proof_Context.init_global @{theory}; - val ctxt = Stool.declare_constraints' [@{term "z::real"}] ctxt; + val ctxt = ContextC.declare_constraints' [@{term "z::real"}] ctxt; val SOME fun1 = TermC.parseNEW ctxt "X z = 3 / (z - 1/4 + -1/8 * z ^^^ -1)"; term2str fun1; diff -r b311a0634eca -r 60d191402598 test/Tools/isac/Minisubpbl/100-init-rootpbl.sml --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Wed Jul 31 09:46:50 2019 +0200 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Fri Aug 09 14:04:13 2019 +0200 @@ -54,7 +54,7 @@ | _ => error "" "~~~~~ fun prep_ori, args:"; val (fmz, thy, pbt) = (fmz, thy, yyy); - val ctxt = Proof_Context.init_global thy |> fold Stool.declare_constraints fmz; + val ctxt = Proof_Context.init_global thy |> fold ContextC.declare_constraints fmz; (*ADD check*) case TermC.parseNEW ctxt "equality (x+1=(2::real))" of SOME (Const ("Descript.equality", _) (* <<< ---------------- this needs to be recognised *) $ diff -r b311a0634eca -r 60d191402598 test/Tools/isac/ProgLang/contextC.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/Tools/isac/ProgLang/contextC.sml Fri Aug 09 14:04:13 2019 +0200 @@ -0,0 +1,18 @@ +(* Title: "ProgLang/contextC.sml" + Author: Walther Neuper + (c) due to copyright terms +*) + +"-----------------------------------------------------------------------------------------------"; +"table of contents -----------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"----------- check all handling of context -----------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; +"-----------------------------------------------------------------------------------------------"; + + +"----------- check all handling of context -----------------------------------------------------"; +"----------- check all handling of context -----------------------------------------------------"; +"----------- check all handling of context -----------------------------------------------------"; +(* waits in Test_Some.thy for checking further updates to context handling *) \ No newline at end of file diff -r b311a0634eca -r 60d191402598 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/test/Tools/isac/Test_Isac.thy Fri Aug 09 14:04:13 2019 +0200 @@ -105,7 +105,8 @@ open Applicable; mk_set; open Solve; (* NONE *) open Selem; e_fmz; - open Stool; transfer_asms_from_to; + open Stool; (* NONE *) + open ContextC; transfer_asms_from_to; open Tactic; (* NONE *) open Model; (* NONE *) open LTool; rule2stac; @@ -147,6 +148,7 @@ ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) ML_file "ProgLang/termC.sml" + ML_file "ProgLang/contextC.sml" ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) ML_file "ProgLang/rewrite.sml" ML_file "ProgLang/listC.sml" diff -r b311a0634eca -r 60d191402598 test/Tools/isac/Test_Isac_Short.thy --- a/test/Tools/isac/Test_Isac_Short.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Aug 09 14:04:13 2019 +0200 @@ -105,7 +105,8 @@ open Applicable; mk_set; open Solve; (* NONE *) open Selem; e_fmz; - open Stool; transfer_asms_from_to; + open Stool; (* NONE *) + open ContextC; transfer_asms_from_to; open Tactic; (* NONE *) open Model; (* NONE *) open LTool; rule2stac; @@ -147,6 +148,7 @@ ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) ML_file "kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) ML_file "ProgLang/termC.sml" + ML_file "ProgLang/contextC.sml" ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) ML_file "ProgLang/rewrite.sml" ML_file "ProgLang/listC.sml" diff -r b311a0634eca -r 60d191402598 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Wed Jul 31 09:46:50 2019 +0200 +++ b/test/Tools/isac/Test_Some.thy Fri Aug 09 14:04:13 2019 +0200 @@ -17,7 +17,8 @@ open Applicable; mk_set; open Solve; (* NONE *) open Selem; e_fmz; - open Stool; transfer_asms_from_to; + open Stool; (* NONE *) + open ContextC; transfer_asms_from_to; open Tactic; (* NONE *) open Model; (* NONE *) open LTool; rule2stac; @@ -68,10 +69,113 @@ "~~~~~ fun xxx , args:"; val () = (); \ -section \===================================================================================\ +section \===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\ ML \ "~~~~~ fun xxx , args:"; val () = (); \ ML \ +"----------- check all handling of context -----------------------------------------------------"; +"----------- check all handling of context -----------------------------------------------------"; +"----------- check all handling of context -----------------------------------------------------"; +(*ER-7*) (*Schalk I s.87 Bsp 55b*) +(* peculiarity of this example: + show_pt_tac pt; + +. . . . . . . . . . ("RatEq",["univariate","equation"],["no_met"]); +([], Frm), solve (x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x, x) + asm ^^^^^ "x \ 0" +. . . . . . . . . . Subproblem (PolyEq, ["normalise","polynomial","univariate","equation"]), +([4], Pbl), solve ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3), x) +. . . . . . . . . . Subproblem (PolyEq, ["bdv_only","degree_2","polynomial","univariate","equation"]), +([4,4], Pbl), solve (-6 * x + 5 * x ^^^ 2 = 0, x) +([4,4,5], Res), [x = 0, x = 6 / 5] +. . . . . . . . . . Check_Postcond ["bdv_only","degree_2","polynomial","univariate","equation"], +([4,4], Res), [x = 0, x = 6 / 5] +. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"], + ^^^^^ from_subpbl_to_caller must drop "x = 0" due to asm "x \ 0" +([5], Res), [x = 0, x = 6 / 5] +. . . . . . . . . . Check_Postcond ["rational","univariate","equation"], +([], Res), [x = 6 / 5] +*) +val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)", + "solveFor x","solutions L"]; +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]); +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; +(*---------solve (x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x, x)*) +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["RatEq", "solve_rat_equation"]*) +\ ML \ +if p = ([], Met) andalso fst nxt = "Apply_Method" andalso +terms2str (get_assumptions_ pt p) = "[]" +then () else error "BEFORE 1 changed"; +\ ML \ +(*//--1 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\ + 1 relevant for init_scrstate in root-pbl*) +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*\\--1 end step into relevant call ----------------------------------------------------------//*) +\ ML \ +if p = ([1], Frm) andalso fst nxt = "Rewrite_Set" andalso +terms2str (get_assumptions_ pt p) = "[\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]" +then () else error "AFTER 1 changed"; +\ ML \ +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "norm_Rational"*) +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "RatEq_eliminate"*) +\ ML \ +if p = ([2], Res) andalso fst nxt = "Rewrite_Set" andalso +terms2str (get_assumptions_ pt p) = "[\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \ 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]" +then () else error "BEFORE 2 changed"; +\ ML \ +(*//--2 begin step into relevant call -------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\ + 2 relevant for preconds like "x \ 0" *) +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]*) +(*---------solve ((3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3), x)*) +(*\\--2 end step into relevant call ----------------------------------------------------------//*) +\ ML \ +if p = ([3], Res) andalso fst nxt = "Subproblem" andalso +terms2str (get_assumptions_ pt p) = "[\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \ 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]" +then () else error "AFTER 2 changed"; +\ ML \ +(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**) +(*[4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**) +(*[4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "normalise_poly"]*) +(*[4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite ("all_left", "\ ?b =!= 0 \ (?a = ?b) = (?a - ?b = 0)")*) +(*[4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*[4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Subproblem ("PolyEq", ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*) +(*---------solve (-6 * x + 5 * x ^^^ 2 = 0, x)*) +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**) +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**) +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(**) +(*4, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*4, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]*) +(*[4, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d2_polyeq_bdv_only_simplify")*) +(*[4, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set_Inst (["(''bdv'', x)"], "d1_polyeq_simplify")*) +(*[4, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Rewrite_Set "polyeq_simplify"*) +(*[4, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Or_to_List*) +(*[4, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_elementwise "Assumptions"*) +(*[4, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["bdv_only", "degree_2", "polynomial", "univariate", "equation"]*) +\ ML \ +if p = ([4, 4, 5], Res) andalso fst nxt = "Check_Postcond" andalso +terms2str (get_assumptions_ pt p) = "[\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\"]" +then () else error "BEFORE 8 changed"; +\ ML \ +(*//--9 begin step into relevant call ----------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^---\\ + 9 relevant for dropping "x = 0" due to asm "x \ 0"*) +(*[4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*) +(*\\--9 end step into relevant call ----------------------------------------------------------//*) +\ ML \ +if p = ([4, 4], Res) andalso fst nxt = "Check_Postcond" andalso +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\",\"\ matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \\n\ lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\"]" +then () else error "AFTER 8 changed"; +\ ML \ +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_elementwise "Assumptions"*) +(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*Check_Postcond ["rational", "univariate", "equation"]*) +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*End_Proof'*) +\ ML \ +if p = ([], Res) andalso f2str f = "[]" (*..must change*)andalso fst nxt = "End_Proof'" andalso +terms2str (get_assumptions_ pt p) = "[\"\ matches (?a = 0)\n ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) \\n\ lhs ((3 + -1 * x + x ^^^ 2) * x =\n 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)) is_poly_in x\",\"x = 6 / 5\",\"x = 0\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) is_poly_in x\",\"lhs (-6 * x + 5 * x ^^^ 2 = 0) has_degree_in x = 2\",\"9 * x + -6 * x ^^^ 2 + x ^^^ 3 \ 0\",\"x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) =\n1 / x is_ratequation_in x\"]" +then () else error "ERROR CHANGED: rateq.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], End_Proof'"; \ ML \ \ ML \ "~~~~~ fun xxx , args:"; val () = ();