1.1 --- a/src/Tools/isac/Specify/specify.sml Tue May 05 15:39:20 2020 +0200
1.2 +++ b/src/Tools/isac/Specify/specify.sml Thu May 07 11:04:02 2020 +0200
1.3 @@ -115,7 +115,7 @@
1.4 let (* both """"""""""""""""""""""""" either empty or complete *)
1.5 val thy = ThyC.get_theory dI
1.6 val (pI, (pors, pctxt), mI) =
1.7 - if mI = ["no_met"]
1.8 + if mI = ["no_met"]
1.9 then
1.10 let
1.11 val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;
2.1 --- a/src/Tools/isac/TODO.thy Tue May 05 15:39:20 2020 +0200
2.2 +++ b/src/Tools/isac/TODO.thy Thu May 07 11:04:02 2020 +0200
2.3 @@ -27,6 +27,8 @@
2.4 (*\------- to from -------/*)
2.5 \begin{itemize}
2.6 \item xxx
2.7 + \item fun specify_init_calc defined twice
2.8 + \item xxx
2.9 \item push nes identifiers back from O/I_Model to Model_Def
2.10 \item xxx
2.11 \item rename Tactic.Calculate -> Tactic.Evaluate
2.12 @@ -55,6 +57,8 @@
2.13 text \<open>
2.14 \begin{itemize}
2.15 \item xxx
2.16 + \item ctxt is superfluous in specify-phase due to type constraints from Descript.thy
2.17 + \item xxx
2.18 \item Derive.do_one: TODO find code in common with complete_solve
2.19 Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)
2.20 \item xxx
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/test/Tools/isac/Specify/o-model.sml Thu May 07 11:04:02 2020 +0200
3.3 @@ -0,0 +1,61 @@
3.4 +(* Title: "Specify/o-model.sml"
3.5 + Author: Walther Neuper
3.6 + (c) due to copyright terms
3.7 +*)
3.8 +
3.9 +"-----------------------------------------------------------------------------------------------";
3.10 +"table of contents -----------------------------------------------------------------------------";
3.11 +"-----------------------------------------------------------------------------------------------";
3.12 +"----------- initialise O_Model.T --------------------------------------------------------------";
3.13 +"-----------------------------------------------------------------------------------------------";
3.14 +"-----------------------------------------------------------------------------------------------";
3.15 +"-----------------------------------------------------------------------------------------------";
3.16 +
3.17 +"----------- fun init for O_Model.T ------------------------------------------------------------";
3.18 +"----------- fun init for O_Model.T ------------------------------------------------------------";
3.19 +"----------- fun init for O_Model.T ------------------------------------------------------------";
3.20 +val f_model = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
3.21 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
3.22 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
3.23 + "AbleitungBiegelinie dy"];
3.24 +val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
3.25 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)
3.26 +
3.27 +"~~~~~ fun CalcTreeTEST , args:"; val [(fmz, sp)] = [(f_model, f_spec)];
3.28 +
3.29 +(* val ((pt, p), tacis) =*)
3.30 +SpecifyNEW.nxt_specify_init_calc (fmz, sp);
3.31 +"~~~~~ fun nxt_specify_init_calc , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
3.32 + val thy = ThyC.get_theory dI;
3.33 + (*if*) mI = ["no_met"] (*else*);
3.34 + val (pI, (pors, pctxt), mI) = (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI);
3.35 +
3.36 +(*+*)Specify.get_pbt pI: Problem.T;
3.37 +(*+*)(Specify.get_pbt pI |> #ppc): Celem4.pat list;
3.38 +(*+*)val (o_model, _) = (Specify.get_pbt pI |> #ppc |>
3.39 + Specify.prep_ori fmz thy): O_Model.T * Proof.context;
3.40 +"~~~~~ fun prep_ori , args:"; val (fmz, thy, pbt) = (fmz, thy, Specify.get_pbt pI |> #ppc);
3.41 + val ctxt = ContextC.initialise' thy fmz;
3.42 + val ori = map (add_field thy pbt o I_Model.split_dts o TermC.parseNEW' ctxt) fmz
3.43 + |> add_variants;
3.44 + val maxv = map fst ori |> max;
3.45 + val maxv = if maxv = 0 then 1 else maxv;
3.46 + val maxv = if maxv = 0 then 1 else maxv;
3.47 + val oris = coll_variants ori
3.48 + |> map (replace_0 maxv |> apfst)
3.49 + |> add_id
3.50 + |> map flattup;
3.51 +
3.52 + (oris, ctxt) (*return from prep_ori*);
3.53 +"~~~~~ from fun prep_ori \<longrightarrow>fun nxt_specify_init_calc , return:"; val (pors, pctxt) = (oris, ctxt);
3.54 +
3.55 +(* final test ...*)
3.56 +(*+*)if O_Model.to_string pors = "[\n" ^
3.57 + "(1, [\"1\"], #Given,Traegerlaenge, [\"L\"]),\n" ^
3.58 + "(2, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n" ^
3.59 + "(3, [\"1\"], #Find,Biegelinie, [\"y\"]),\n" ^
3.60 + "(4, [\"1\"], #Relate,Randbedingungen, [\"[y 0 = 0]\",\"[y L = 0]\",\"[M_b 0 = 0]\",\"[M_b L = 0]\"]),\n" ^
3.61 + "(5, [\"1\"], #undef,FunktionsVariable, [\"x\"]),\n" ^
3.62 + "(6, [\"1\"], #undef,GleichungsVariablen, [\"[c]\",\"[c_2]\",\"[c_3]\",\"[c_4]\"]),\n" ^
3.63 + "(7, [\"1\"], #undef,AbleitungBiegelinie, [\"dy\"])]"
3.64 +then () else error "O_Model.init CHANGED";
4.1 --- a/test/Tools/isac/Test_Some.thy Tue May 05 15:39:20 2020 +0200
4.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 07 11:04:02 2020 +0200
4.3 @@ -32,12 +32,10 @@
4.4 open Input_Descript;
4.5 open Specify; show_ptyps;
4.6 open SpecifyNEW;
4.7 - open ApplicableOLD; mk_set;
4.8 open Step_Specify;
4.9 open Step_Solve;
4.10 open Step;
4.11 open Solve; (* NONE *)
4.12 - open Selem; Formalise.empty;
4.13 open Stool; (* NONE *)
4.14 open ContextC; transfer_asms_from_to;
4.15 open Tactic; (* NONE *)