wneuper/isa: src/Tools/isac/Specify/step-specify.sml@3b056e367183

     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: Selem.fmz

    13     -> Calc.T * (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list

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

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

    17 end

    19 (**)

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

    21 struct

    22 (**)

    23 open Pos

    24 open Ctree

    25 open Chead

    27 (* was fun Math_Engine.nxt_specify_ *)

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

    29     let

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

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

    32       | _ => error "by_tactic_input Model_Problem; uncovered case get_obj"

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

    34       val thy = ThyC.get_theory dI

    35       val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)

    36       val {cas, ppc, ...} = Specify.get_pbt pI

    37       val pbl = Generate.init_pbl ppc (* fill in descriptions *)

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

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

    40       val (pbl, met) = case cas of

    41         NONE => (pbl, [])

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

    43       (*----------------------------------------------------------------*)

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

    45       val (pos,c,_,pt) = Generate.generate1 tac_ (Istate_Def.Uistate, ctxt) (pt, pos)

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

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

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

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

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

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

    52     let

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

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

    55       | _ => error "by_tactic_input Refine_Tacitly: uncovered case get_obj"

    56       val opt = Specify.refine_ori oris pI

    57     in

    58       case opt of

    59 	      SOME pI' =>

    60 	        let

    61             val {met, ...} = Specify.get_pbt pI'

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

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

    64             val thy = ThyC.get_theory dI

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

    66 		          Generate.generate1 (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)

    67 	        in

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

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

    70           end

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

    72     end

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

    74     let

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

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

    77           (dI, dI', probl, ctxt)

    78       | _ => error "by_tactic_input Refine_Problem: uncovered case get_obj"

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

    80     in

    81       case Specify.refine_pbl (ThyC.get_theory thy) pI probl of

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

    83 	    | SOME rfd =>

    84 	      let

    85           val (pos,c,_,pt) = Generate.generate1 (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)

    86 	      in

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

    88         end

    89     end

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

    91     let

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

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

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

    95       | _ => error ""

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

    97       val {ppc,where_,prls,...} = Specify.get_pbt pI

    98 	    val pbl =

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

   100 	      then (false, (Generate.init_pbl ppc, []))

   101 	      else Specify.match_itms_oris thy probl (ppc,where_,prls) oris

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

   103 	    val (c, pt) =

   104 	      case Generate.generate1 (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of

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

   106   	    | _ => error ""

   107     in

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

   109     end

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

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

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

   113     let

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

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

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

   117       | _ => error "by_tactic_input Specify_Method: uncovered case get_obj"

   118       val {ppc,pre,prls,...} = Specify.get_met mID

   119       val thy = ThyC.get_theory dI

   120       val oris = Specify.add_field' thy ppc oris

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

   122       val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris

   123       val itms = Specify.hack_until_review_Specify_2 mID itms

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

   125 	      Generate.generate1 (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)

   126     in

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

   128     end

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

   130     let

   131       val ctxt = get_ctxt pt pos

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

   133 	      Generate.generate1 (Tactic.Specify_Theory' dI)  (Istate_Def.Uistate, ctxt) (pt, pos)

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

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

   136 	      (pt, pos))

   137     end

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

   139     let

   140       val ctxt = get_ctxt pt pos

   141 	    val (pos, c, _, pt) = Generate.generate1 (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)

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

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

   144     end

   145   | by_tactic_input m' _ = error ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')

   146 (* was fun Math_Engine.nxt_specify_ *)

   149 (* was fun Chead.specify *)

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

   151     let

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

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

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

   155       | _ => error "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"

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

   157       val thy = ThyC.get_theory thy'

   158       val {ppc, prls, where_, ...} = Specify.get_pbt pI'

   159       val pre = Stool.check_preconds thy prls where_ pbl

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

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

   162         Generate.generate1 (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) (pt, pos)

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

   164 		    (ppc,(#ppc o Specify.get_met) mI') (dI',pI',mI');

   165     in

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

   167     end

   168     (* called only if no_met is specified *)

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

   170       let

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

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

   173         | _ => error "Step_Solve.by_tactic (Refine_Tacitly': uncovered case get_obj"*)

   174         val {met, thy,...} = Specify.get_pbt pIre

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

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

   177 	        Generate.generate1 (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))

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

   179 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

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

   181       in

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

   183       end

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

   185       let

   186         val ctxt = get_ctxt pt pos

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

   188           Generate.generate1 (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)

   189       in

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

   191       end

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

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

   194       let

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

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

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

   198         | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"

   199         val thy = ThyC.get_theory dI

   200         val (p, pt) =

   201           case  Generate.generate1 (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of

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

   203           | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"

   204       in

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

   206       end

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

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

   209       let

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

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

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

   213         | _ => error "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"

   214         val {ppc, pre, prls,...} = Specify.get_met mID

   215         val thy = ThyC.get_theory dI

   216         val oris = Specify.add_field' thy ppc oris

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

   218         val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc, pre, prls) oris

   219         val itms = Specify.hack_until_review_Specify_1 mI' itms

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

   221 	        Generate.generate1 (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)

   222       in

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

   224       end

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

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

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

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

   229       let

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

   231         val thy = ThyC.get_theory domID

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

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

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

   235         | _ => error "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"

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

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

   238         val {prls = per, ppc, where_ = pwh, ...} = Specify.get_pbt cpI

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

   240         val {prls = mer, ppc = mpc, pre= mwh, ...} = Specify.get_met cmI

   241         val pre = case p_ of

   242           Met => (Stool.check_preconds thy mer mwh met)

   243         | _ => (Stool.check_preconds thy per pwh pbl)

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

   245       in

   246         if domID = dI

   247         then

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

   249 	        in

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

   251           end

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

   253 	        let

   254 	          val ((p, p_), _, _, pt) = Generate.generate1 (Tactic.Specify_Theory' domID) (Istate_Def.Uistate, ctxt) (pt, (p,p_))

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

   256 	        in

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

   258           end

   259       end

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

   261 (* was fun Chead.specify *)

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

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

   265     if pI <> []

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

   267 	    let

   268         val {cas, met, ppc, thy, ...} = Specify.get_pbt pI

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

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

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

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

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

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

   275 	      val pits = Generate.init_pbl' ppc

   276 	      val pt = update_pbl pt [] pits

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

   278     else

   279       if mI <> []

   280       then (* from met-browser *)

   281 	      let

   282           val {ppc, ...} = Specify.get_met mI

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

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

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

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

   287 	        val mits = Generate.init_pbl' ppc

   288 	        val pt = update_met pt [] mits

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

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

   291 	      let

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

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

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

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

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

   297 	    val thy = ThyC.get_theory dI

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

   299 	      if mI = ["no_met"]

   300 	      then

   301           let

   302             val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;

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

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

   305 		        (hd o #met o Specify.get_pbt) pI')

   306 		      end

   307 	      else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)

   308 	    val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)

   309 	    val dI = Context.theory_name (Stool.common_subthy (thy, thy'))

   310 	    val hdl = case cas of

   311 		    NONE => Auto_Prog.pblterm dI pI

   312 		  | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t

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

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

   315     in

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

   317     end

   319 (**)end(**)

author	Walther Neuper <walther.neuper@jku.at>
	Sat, 02 May 2020 11:36:13 +0200
changeset 59926	3b056e367183
parent 59903	5037ca1b112b
child 59931	cc5b51681c4b
permissions	-rw-r--r--