wneuper/isa: src/Tools/isac/Specify/step-specify.sml@2909d58a5c5d

     1 (* Title:  Specify/step-specify.sml

     2    Author: Walther Neuper 2019

     3    (c) due to copyright terms

     4 *)

     6 signature STEP_SPECIFY =

     7 sig

     8 (*val do_next: Step.specify_do_next requires LI.by_tactic, which is not yet known in Step_Specify*)

     9   val by_tactic_input: Tactic.input -> Calc.T -> Chead.calcstate'

    10   val by_tactic: Tactic.T -> Calc.T -> string * Chead.calcstate'

    11 (* ---- keep, probably required later in devel. ----------------------------------------------- *)

    12   val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T

    13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

    14 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

    16 end

    18 (**)

    19 structure Step_Specify(**): STEP_SPECIFY(**) =

    20 struct

    21 (**)

    22 open Pos

    23 open Ctree

    24 open Chead

    26 (* was fun Math_Engine.nxt_specify_ *)

    27 fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =

    28     let

    29       val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of

    30         PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)

    31       | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"

    32       val (dI, pI, mI) = some_spec ospec spec

    33       val thy = ThyC.get_theory dI

    34       val mpc = (#ppc o Method.from_store) mI (* just for reuse complete_mod_ *)

    35       val {cas, ppc, ...} = Problem.from_store pI

    36       val pbl = I_Model.init ppc (* fill in descriptions *)

    37       (*----------------if you think, this should be done by the Dialog

    38        in the java front-end, search there for WN060225-modelProblem----*)

    39       val (pbl, met) = case cas of

    40         NONE => (pbl, [])

    41   		| _ => complete_mod_ (oris, mpc, ppc, probl)

    42       (*----------------------------------------------------------------*)

    43       val tac_ = Tactic.Model_Problem' (pI, pbl, met)

    44       val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)

    45     in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)) end

    46   | by_tactic_input (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp

    47   | by_tactic_input (Tactic.Add_Find  ct) ptp = nxt_specif_additem "#Find"  ct ptp

    48   | by_tactic_input (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp

    49     (*. called only if no_met is specified .*)

    50   | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =

    51     let

    52       val (oris, dI, ctxt) = case get_obj I pt p of

    53         (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)

    54       | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"

    55       val opt = Refine.refine_ori oris pI

    56     in

    57       case opt of

    58 	      SOME pI' =>

    59 	        let

    60             val {met, ...} = Problem.from_store pI'

    61 	          (*val pt = update_pbl pt p pbl ..done by Model_Problem*)

    62 	          val mI = if length met = 0 then Method.id_empty else hd met

    63             val thy = ThyC.get_theory dI

    64 	          val (pos, c, _, pt) =

    65 		          Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)

    66 	        in

    67 	          ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),

    68 	              (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))

    69           end

    70 	    | NONE => ([], [], ptp)

    71     end

    72   | by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =

    73     let

    74       val (dI, dI', probl, ctxt) = case get_obj I pt p of

    75         PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>

    76           (dI, dI', probl, ctxt)

    77       | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"

    78 	    val thy = if dI' = ThyC.id_empty then dI else dI'

    79     in

    80       case Refine.problem (ThyC.get_theory thy) pI probl of

    81 	      NONE => ([], [], ptp)

    82 	    | SOME rfd =>

    83 	      let

    84           val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)

    85 	      in

    86 	        ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos))

    87         end

    88     end

    89   | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =

    90     let

    91       val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of

    92         PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>

    93           (oris, dI, dI', pI', probl, ctxt)

    94       | _ => raise ERROR ""

    95 	    val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');

    96       val {ppc,where_,prls,...} = Problem.from_store pI

    97 	    val pbl =

    98 	      if pI' = Problem.id_empty andalso pI = Problem.id_empty

    99 	      then (false, (I_Model.init ppc, []))

   100 	      else Model.match_itms_oris thy probl (ppc,where_,prls) oris

   101 	      (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)

   102 	    val (c, pt) =

   103 	      case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of

   104   	      ((_, Pbl), c, _, pt) => (c, pt)

   105   	    | _ => raise ERROR ""

   106     in

   107       ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))

   108     end

   109   (* transfers oris (not required in pbl) to met-model for script-env

   110      FIXME.WN.8.03: application of several mIDs to SAME model?       *)

   111   | by_tactic_input (Tactic.Specify_Method mID) (pt, pos as (p,_)) =

   112     let

   113       val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of

   114         PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}

   115           => (oris, pbl, dI, met, ctxt)

   116       | _ => raise ERROR "by_tactic_input Specify_Method: uncovered case get_obj"

   117       val {ppc,pre,prls,...} = Method.from_store mID

   118       val thy = ThyC.get_theory dI

   119       val oris = O_Model.add thy ppc oris

   120       val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)

   121       val (_, (itms, _)) = Model.match_itms_oris thy met (ppc,pre,prls ) oris

   122       val itms = Specify.hack_until_review_Specify_2 mID itms

   123       val (pos, c, _, pt) =

   124 	      Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)

   125     in

   126       ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos))

   127     end

   128   | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =

   129     let

   130       val ctxt = get_ctxt pt pos

   131 	    val (pos, c, _, pt) =

   132 	      Specify_Step.add (Tactic.Specify_Theory' dI)  (Istate_Def.Uistate, ctxt) (pt, pos)

   133     in (*FIXXXME: check if pbl can still be parsed*)

   134 	    ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c,

   135 	      (pt, pos))

   136     end

   137   | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =

   138     let

   139       val ctxt = get_ctxt pt pos

   140 	    val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)

   141     in  (*FIXXXME: check if met can still be parsed*)

   142 	    ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))

   143     end

   144   | by_tactic_input m' _ = raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')

   145 (* was fun Math_Engine.nxt_specify_ *)

   148 (* was fun Chead.specify *)

   149 fun by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _))  =

   150     let

   151       val (oris, dI',pI',mI', dI, ctxt) = case get_obj I pt p of

   152         PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, _), ctxt, ...} =>

   153           (oris, dI',pI',mI', dI, ctxt)

   154       | _ => raise ERROR "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"

   155       val thy' = if dI = ThyC.id_empty then dI' else dI

   156       val thy = ThyC.get_theory thy'

   157       val {ppc, prls, where_, ...} = Problem.from_store pI'

   158       val pre = Pre_Conds.check' thy prls where_ pbl

   159       val pb = foldl and_ (true, map fst pre)

   160       val ((p, _), _, _, pt) =

   161         Specify_Step.add (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) (pt, pos)

   162       val (_, _) = Chead.nxt_spec Pbl pb oris (dI', pI', mI') (pbl, met)

   163 		    (ppc,(#ppc o Method.from_store) mI') (dI',pI',mI');

   164     in

   165       ("ok", ([], [], (pt, (p, Pbl))))

   166     end

   167     (* called only if no_met is specified *)

   168   | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =

   169       let

   170 (*      val (dI', ctxt) = case get_obj I pt p of

   171           PblObj {origin= (_, (dI', _, _), _), ctxt, ...} => (dI', ctxt)

   172         | _ => raise ERROR "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)

   173         val {met, thy,...} = Problem.from_store pIre

   174         val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)

   175         val ((p,_), _, _, pt) =

   176 	        Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))

   177             (Istate_Def.Uistate, ContextC.empty) (pt, pos)

   178 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

   179 (*     val (pbl, pre, _) = ([], [], false)*)

   180       in

   181         ("ok", ([], [], (pt,(p, Pbl))))

   182       end

   183   | by_tactic (Tactic.Refine_Problem' rfd) (pt, pos)  =

   184       let

   185         val ctxt = get_ctxt pt pos

   186         val (pos, _, _, pt) =

   187           Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)

   188       in

   189         ("ok", ([], [], (pt,pos)))

   190       end

   191     (*WN110515 initialise ctxt again from itms and add preconds*)

   192   | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p, _)) =

   193       let

   194         val (_, _, _, _, dI, _, ctxt, _) = case get_obj I pt p of

   195           PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>

   196             (oris, dI', pI', mI', dI, mI, ctxt, met)

   197         | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"

   198         val thy = ThyC.get_theory dI

   199         val (p, pt) =

   200           case  Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of

   201             ((p, Pbl), _, _, pt) => (p, pt)

   202           | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"

   203       in

   204         ("ok", ([], [], (pt, (p, Pbl))))

   205       end

   206     (*WN110515 initialise ctxt again from itms and add preconds*)

   207   | by_tactic (Tactic.Specify_Method' (mID, _, _)) (pt,pos as (p, _)) =

   208       let

   209         val (oris, _, _, mI', dI, _, pbl, met, ctxt) = case get_obj I pt p of

   210           PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>

   211              (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)

   212         | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"

   213         val {ppc, pre, prls,...} = Method.from_store mID

   214         val thy = ThyC.get_theory dI

   215         val oris = O_Model.add thy ppc oris

   216         val met = if met = [] then pbl else met

   217         val (_, (itms, _)) = Model.match_itms_oris thy met (ppc, pre, prls) oris

   218         val itms = Specify.hack_until_review_Specify_1 mI' itms

   219         val (pos, _, _, pt) =

   220 	        Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)

   221       in

   222         ("ok", ([], [], (pt, pos)))

   223       end

   224   | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p)  = Chead.specify_additem "#Given" ct (pt, p)

   225   | by_tactic (Tactic.Add_Find'  (ct, _)) (pt, p) = Chead.specify_additem "#Find" ct (pt, p)

   226   | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Chead.specify_additem"#Relate" ct (pt, p)

   227   | by_tactic (Tactic.Specify_Theory' domID) (pt, (p,p_)) =

   228       let

   229         val p_ = case p_ of Met => Met | _ => Pbl

   230         val thy = ThyC.get_theory domID

   231         val (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt) = case get_obj I pt p of

   232           PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, mI), probl = pbl, meth = met, ctxt, ...} =>

   233              (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)

   234         | _ => raise ERROR "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"

   235         val _ = case p_ of Met => met | _ => pbl

   236         val cpI = if pI = Problem.id_empty then pI' else pI

   237         val {prls = per, ppc, where_ = pwh, ...} = Problem.from_store cpI

   238         val cmI = if mI = Method.id_empty then mI' else mI

   239         val {prls = mer, ppc = mpc, pre= mwh, ...} = Method.from_store cmI

   240         val pre = case p_ of

   241           Met => (Pre_Conds.check' thy mer mwh met)

   242         | _ => (Pre_Conds.check' thy per pwh pbl)

   243         val pb = foldl and_ (true, map fst pre)

   244       in

   245         if domID = dI

   246         then

   247           let val (p_, _) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)

   248 	        in

   249             ("ok", ([], [], (pt, (p, p_))))

   250           end

   251         else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)

   252 	        let

   253 	          val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID) (Istate_Def.Uistate, ctxt) (pt, (p,p_))

   254 	          val (p_, _) = nxt_spec p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)

   255 	        in

   256             ("ok", ([], [], (pt, (p, p_))))

   257           end

   258       end

   259   | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"

   260 (* was fun Chead.specify *)

   262 (* create a calc-tree with oris via an cas.refined pbl *)

   263 fun nxt_specify_init_calc ([], (dI, pI, mI)) =

   264     if pI <> []

   265     then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)

   266 	    let

   267         val {cas, met, ppc, thy, ...} = Problem.from_store pI

   268 	      val dI = if dI = "" then Context.theory_name thy else dI

   269 	      val mI = if mI = [] then hd met else mI

   270 	      val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t

   271 	      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))

   272 				  ([], (dI,pI,mI), hdl, ContextC.empty)

   273 	      val pt = update_spec pt [] (dI, pI, mI)

   274 	      val pits = I_Model.init ppc

   275 	      val pt = update_pbl pt [] pits

   276 	    in ((pt, ([] , Pbl)), []) end

   277     else

   278       if mI <> []

   279       then (* from met-browser *)

   280 	      let

   281           val {ppc, ...} = Method.from_store mI

   282 	        val dI = if dI = "" then "Isac_Knowledge" else dI

   283 	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)

   284 	          ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)

   285 	        val pt = update_spec pt [] (dI, pI, mI)

   286 	        val mits = I_Model.init ppc

   287 	        val pt = update_met pt [] mits

   288 	      in ((pt, ([], Met)), []) end

   289       else (* new example, pepare for interactive modeling *)

   290 	      let

   291 	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)

   292 	          ([], Spec.empty) ([], Spec.empty, TermC.empty, ContextC.empty)

   293 	      in ((pt, ([], Pbl)), []) end

   294   | nxt_specify_init_calc (fmz, (dI, pI, mI)) =

   295     let           (* both """"""""""""""""""""""""" either empty or complete *)

   296 	    val thy = ThyC.get_theory dI

   297 	    val (pI, (pors, pctxt), mI) =

   298 	      if mI = ["no_met"]

   299 	      then

   300           let

   301             val (pors(*, pctxt*)) = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;

   302             val pctxt = ContextC.initialise' thy fmz;

   303 		        val pI' = Refine.refine_ori' pors pI;

   304 		      in (pI', (pors(*refinement over models with diff.precond only*), pctxt),

   305 		        (hd o #met o Problem.from_store) pI')

   306 		      end

   307 	      else

   308 	        let

   309 	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;

   310             val pctxt = ContextC.initialise' thy fmz;

   311 	        in (pI, (pors, pctxt), mI) end;

   312 	    val {cas, ppc, thy = thy', ...} = Problem.from_store pI (*take dI from _refined_ pbl*)

   313 	    val dI = Context.theory_name (ThyC.sub_common (thy, thy'))

   314 	    val hdl = case cas of

   315 		    NONE => Auto_Prog.pblterm dI pI

   316 		  | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ O_Model.values pors) t

   317       val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)

   318         (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)

   319     in

   320       ((pt, ([], Pbl)), fst3 (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))

   321     end

   323 (**)end(**)

author	Walther Neuper <walther.neuper@jku.at>
	Wed, 13 May 2020 11:34:05 +0200
changeset 59971	2909d58a5c5d
parent 59970	ab1c25c0339a
child 59975	c4b83a338c44
permissions	-rw-r--r--