1.1 --- a/src/Tools/isac/Specify/step-specify.sml	Wed May 13 18:16:35 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/step-specify.sml	Thu May 14 08:49:08 2020 +0200
     1.3 @@ -8,6 +8,9 @@
     1.4  (*val do_next: Step.specify_do_next requires LI.by_tactic, which is not yet known in Step_Specify*)
     1.5    val by_tactic_input: Tactic.input -> Calc.T -> Chead.calcstate'
     1.6    val by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'
     1.7 +
     1.8 +  val hack_until_review_Specify_1: Method.id -> I_Model.T -> I_Model.T
     1.9 +  val hack_until_review_Specify_2: Method.id -> I_Model.T -> I_Model.T
    1.10  (* ---- keep, probably required later in devel. ----------------------------------------------- *)
    1.11    val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
    1.12  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.13 @@ -23,7 +26,39 @@
    1.14  open Ctree
    1.15  open Chead
    1.16  
    1.17 -(* was fun Math_Engine.nxt_specify_ *)
    1.18 +(*
    1.19 +  hack until review of Specify:
    1.20 +  introduction of Lucas-Interpretation to Isabelle's functioj package enforced
    1.21 +  to make additional variables on the right hand side to arguments of programs.
    1.22 +  These additional arguments are partially handled by these hacks.
    1.23 +*)
    1.24 +fun hack_until_review_Specify_1 metID itms = 
    1.25 +  if metID = ["Biegelinien", "ausBelastung"]
    1.26 +  then itms @
    1.27 +    [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
    1.28 +        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
    1.29 +      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
    1.30 +        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
    1.31 +    (5, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
    1.32 +        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
    1.33 +      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
    1.34 +        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
    1.35 +  else itms
    1.36 +
    1.37 +fun hack_until_review_Specify_2 metID itms = 
    1.38 +  if metID = ["IntegrierenUndKonstanteBestimmen2"]
    1.39 +  then itms @
    1.40 +    [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
    1.41 +        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
    1.42 +      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
    1.43 +        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
    1.44 +    (5, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
    1.45 +        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
    1.46 +      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
    1.47 +        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
    1.48 +  else itms
    1.49 +
    1.50 +
    1.51  fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
    1.52      let
    1.53        val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
    1.54 @@ -119,7 +154,7 @@
    1.55        val oris = O_Model.add thy ppc oris
    1.56        val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)
    1.57        val (_, (itms, _)) = Model.match_itms_oris thy met (ppc,pre,prls ) oris
    1.58 -      val itms = Specify.hack_until_review_Specify_2 mID itms
    1.59 +      val itms = hack_until_review_Specify_2 mID itms
    1.60        val (pos, c, _, pt) = 
    1.61  	      Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
    1.62      in
    1.63 @@ -215,7 +250,7 @@
    1.64          val oris = O_Model.add thy ppc oris
    1.65          val met = if met = [] then pbl else met
    1.66          val (_, (itms, _)) = Model.match_itms_oris thy met (ppc, pre, prls) oris
    1.67 -        val itms = Specify.hack_until_review_Specify_1 mI' itms
    1.68 +        val itms = hack_until_review_Specify_1 mI' itms
    1.69          val (pos, _, _, pt) = 
    1.70  	        Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
    1.71        in