1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Jan 11 11:38:01 2023 +0100
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Jan 25 15:52:33 2023 +0100
1.3 @@ -178,6 +178,117 @@
1.4 \<close>
1.5 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
1.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
1.7 +ML \<open>
1.8 +\<close> ML \<open>
1.9 +(* Title: 100-init-rootpbl.sml
1.10 + Author: Walther Neuper 1105
1.11 + (c) copyright due to lincense terms.
1.12 +*)
1.13 +
1.14 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
1.15 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
1.16 +"----------- Minisubplb/100-init-rootpbl.sml ---------------------";
1.17 +val (_(*example text*),
1.18 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
1.19 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
1.20 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.21 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.22 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
1.23 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
1.24 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
1.25 + "ErrorBound (\<epsilon> = (0::real))" :: []),
1.26 + refs as ("Diff_App",
1.27 + ["univariate_calculus", "Optimisation"],
1.28 + ["Optimisation", "by_univariate_calculus"])))
1.29 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
1.30 +
1.31 + Test_Code.init_calc @{context} [(model, refs)];
1.32 +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
1.33 + = (@{context}, [(model, refs)]);
1.34 +(*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
1.35 +( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
1.36 +
1.37 +(**)val return_nxt_specify_init_calc_PIDE =(**)
1.38 +Step_Specify.nxt_specify_init_calc_PIDE thy (model, refs);
1.39 +"~~~~~ fun nxt_specify_init_calc , args:"; val (ctxt, (model, (dI, pI, mI))) = (ctxt, (model, refs));
1.40 +
1.41 +Step_Specify.initialise_PIDE thy (model, refs);
1.42 +"~~~~~ fun initialise , args:"; val (ctxt, (fmz, (dI, pI, mI))) = (ctxt, (model, refs));
1.43 +(*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)
1.44 + val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise.refs *)
1.45 + val (pI, (pors, pctxt), mI) =
1.46 + if mI = ["no_met"]
1.47 + then raise error "else not covered by test"
1.48 + else
1.49 + let
1.50 +(*old* ) val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)
1.51 +(*old*) val pctxt = ContextC.initialise' thy fmz; (*..DUPLICATE ermC.parseNEW'*)
1.52 +(*old*) in (pI, (pors, pctxt), mI) end;
1.53 +( *new*) val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;
1.54 + in (pI, (pors, pctxt), mI) end;
1.55 +
1.56 +(*/------------------- check result of O_Model.init_PIDE ------------------------------------\*)
1.57 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term pctxt "r";
1.58 +(*+*)val Free ("u", Type ("Real.real", [])) = Syntax.read_term pctxt "u";
1.59 +(*-------------------- stop step into Step_Specify.nxt_specify_init_calc ---------------------*)
1.60 +
1.61 +val ((pt, p), tacis) = return_nxt_specify_init_calc_PIDE(* kept for continuation *);
1.62 +"~~~~~ continue fun init_calc , args:"; val ((pt, p), tacis)
1.63 + = ((pt, p), tacis);
1.64 + val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis;
1.65 +
1.66 + Test_Code.TESTg_form ctxt (pt,p);
1.67 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
1.68 + val (form, _, _) = ME_Misc.pt_extract ctxt ptp;
1.69 +val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
1.70 + (*case*) form (*of*);
1.71 +val Pos.Pbl =
1.72 + (*case*) p_ (*of*);
1.73 + Test_Out.Problem [];
1.74 + Test_Out.MethodC [];
1.75 +
1.76 +(*val return =*)
1.77 + Test_Out.PpcKF (Test_Out.Problem [],
1.78 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_);
1.79 +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
1.80 +
1.81 +(*//------------------ inserted hidden code ------------------------------------------------\\*)
1.82 +fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
1.83 + | item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c
1.84 + | item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c
1.85 + | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
1.86 + | item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
1.87 + | item_from_feedback thy (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
1.88 + | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
1.89 +fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
1.90 + case sel of
1.91 + "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
1.92 + | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
1.93 + | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
1.94 + | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
1.95 + | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
1.96 + | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
1.97 +fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
1.98 + {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
1.99 +fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term_in_ctxt ctxt term)
1.100 + | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term_in_ctxt ctxt term);
1.101 +(*\\------------------ inserted hidden code ------------------------------------------------//*)
1.102 +
1.103 + fun coll model [] = model
1.104 + | coll model ((_, _, _, field, itm_)::itms) =
1.105 + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
1.106 + val gfr = coll P_Model.empty itms;
1.107 +
1.108 +(*val return =*)
1.109 + add_where gfr (map (boolterm2item (Proof_Context.init_global thy)) where_);
1.110 +"~~~~~ fun add_where , args:"; val ({Given = gi, Where = _, Find = fi, With = wi, Relate = re}, wh)
1.111 + = (gfr, (map
1.112 + (boolterm2item ctxt) where_));
1.113 +"~~~~~ fun boolterm2item , args:"; val () = ();
1.114 +(*\\------------------ step into nxt_specify_init_calc -------------------------------------//*)
1.115 +\<close> ML \<open>
1.116 +\<close> ML \<open>
1.117 +\<close>
1.118 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
1.119 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
1.120 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"