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

     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 = Celem.assoc_thy 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 Celem.e_metID else hd met

    64             val thy = Celem.assoc_thy 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.e_domID then dI else dI'

    80     in

    81       case Specify.refine_pbl (Celem.assoc_thy 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 = Celem.assoc_thy (if dI' = ThyC.e_domID then dI else dI');

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

    98 	    val pbl =

    99 	      if pI' = Celem.e_pblID andalso pI = Celem.e_pblID

   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 = Celem.assoc_thy 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.Init_Proof' (fmz, spec' as (dI', pI', mI'))) _ =

   151     let          (* either """"""""""""""" all empty or complete *)

   152       val thy = Celem.assoc_thy dI'

   153       val (oris, ctxt) =

   154         if dI' = ThyC.e_domID orelse pI' = Celem.e_pblID  (*andalso? WN110511*)

   155         then ([], ContextC.empty)

   156   	    else pI' |> #ppc o Specify.get_pbt |> Specify.prep_ori fmz thy

   157         (* these are deprecated                vvvvvvvvvvvvvvvvvvvvvvvvvv*)

   158       val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) (fmz, spec')

   159   			(oris, (dI',pI',mI'), Rule.e_term, ctxt)

   160       val pt = update_loc' pt [] (SOME (Istate_Def.empty, ctxt), NONE)

   161     in

   162       case mI' of

   163   	    ["no_met"] => ("Refine_Tacitly", ([], [], (pt, ([], Pbl))))

   164       | _ => ("ok", ([], [], (pt, ([], Pbl))))

   165     end

   166     (* ONLY for STARTING modeling phase *)

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

   168     let

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

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

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

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

   173       val thy' = if dI = ThyC.e_domID then dI' else dI

   174       val thy = Celem.assoc_thy thy'

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

   176       val pre = Stool.check_preconds thy prls where_ pbl

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

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

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

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

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

   182     in

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

   184     end

   185     (* called only if no_met is specified *)

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

   187       let

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

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

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

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

   192         val (domID, metID) = (ThyC.string_of_thy thy, if length met = 0 then Celem.e_metID else hd met)

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

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

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

   196 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

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

   198       in

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

   200       end

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

   202       let

   203         val ctxt = get_ctxt pt pos

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

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

   206       in

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

   208       end

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

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

   211       let

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

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

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

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

   216         val thy = Celem.assoc_thy dI

   217         val (p, pt) =

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

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

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

   221       in

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

   223       end

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

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

   226       let

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

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

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

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

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

   232         val thy = Celem.assoc_thy dI

   233         val oris = Specify.add_field' thy ppc oris

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

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

   236         val itms = Specify.hack_until_review_Specify_1 mI' itms

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

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

   239       in

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

   241       end

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

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

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

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

   246       let

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

   248         val thy = Celem.assoc_thy domID

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

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

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

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

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

   254         val cpI = if pI = Celem.e_pblID then pI' else pI

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

   256         val cmI = if mI = Celem.e_metID then mI' else mI

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

   258         val pre = case p_ of

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

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

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

   262       in

   263         if domID = dI

   264         then

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

   266 	        in

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

   268           end

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

   270 	        let

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

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

   273 	        in

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

   275           end

   276       end

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

   278 (* was fun Chead.specify *)

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

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

   282     if pI <> []

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

   284 	    let

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

   286 	      val dI = if dI = "" then ThyC.theory2theory' thy else dI

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

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

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

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

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

   292 	      val pits = Generate.init_pbl' ppc

   293 	      val pt = update_pbl pt [] pits

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

   295     else

   296       if mI <> []

   297       then (* from met-browser *)

   298 	      let

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

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

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

   302 	          ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term, ContextC.empty)

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

   304 	        val mits = Generate.init_pbl' ppc

   305 	        val pt = update_met pt [] mits

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

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

   308 	      let

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

   310 	          ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.empty)

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

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

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

   314 	    val thy = Celem.assoc_thy dI

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

   316 	      if mI = ["no_met"]

   317 	      then

   318           let

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

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

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

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

   323 		      end

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

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

   326 	    val dI = ThyC.theory2theory' (Stool.common_subthy (thy, thy'))

   327 	    val hdl = case cas of

   328 		    NONE => Auto_Prog.pblterm dI pI

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

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

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

   332     in

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

   334     end

   336 (**)end(**)

author	Walther Neuper <walther.neuper@jku.at>
	Wed, 08 Apr 2020 14:24:38 +0200
changeset 59854	c20d08e01ad2
parent 59846	7184a26ac7d5
child 59861	65ec9f679c3f
permissions	-rw-r--r--