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

     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 -> string * Calc.state_post

    10   val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post

    12   val initialisePIDEHACK: theory -> Formalise.T ->

    13     term * term * References.T * O_Model.T * Proof.context

    14   val initialisePIDE: Formalise.T ->

    15     term * term * References.T * O_Model.T * Proof.context

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

    17 end

    19 (**)

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

    21 struct

    22 (**)

    23 open Pos

    24 open Ctree

    25 open Specification

    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 (_, pI, mI) = References.select ospec spec

    33       val mpc = (#ppc o MethodC.from_store) mI (* just for reuse I_Model.complete_method *)

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

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

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

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

    38       val (pbl, met) = case cas of

    39         NONE => (pbl, [])

    40   		| _ => I_Model.complete_method (oris, mpc, ppc, probl)

    41       (*----------------------------------------------------------------*)

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

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

    44     in

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

    46     end

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

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

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

    51     (* called with MethodC.id_empty *)

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

    53     let

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

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

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

    57       val opt = Refine.refine_ori oris pI

    58     in

    59       case opt of

    60 	      SOME pI' =>

    61 	        let

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

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

    64 	          val mI = if length met = 0 then MethodC.id_empty else hd met

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

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

    67 	        in

    68 	          ("ok", ([(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 => ("failure", ([], [], 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       | _ => raise 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 Refine.problem (ThyC.get_theory thy) pI probl of

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

    83 	    | SOME rfd =>

    84 	      let

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

    86 	      in

    87 	        ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd,

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

    89         end

    90     end

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

    92     let

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

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

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

    96       | _ => raise ERROR ""

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

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

    99 	    val pbl =

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

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

   102 	      else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris

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

   104 	    val (c, pt) =

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

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

   107   	    | _ => raise ERROR ""

   108     in

   109       ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl),

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

   111     end

   112   | by_tactic_input (Tactic.Specify_Method id) (pt, pos) =

   113     let

   114       val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)

   115       val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))

   116         (Istate_Def.Uistate, ctxt) (pt, pos)

   117     in

   118       ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),

   119         (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))

   120     end

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

   122     let

   123       val ctxt = get_ctxt pt pos

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

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

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

   127 	    ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,

   128         (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))

   129     end

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

   131     let

   132       val ctxt = get_ctxt pt pos

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

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

   135 	    ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,

   136         (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))

   137     end

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

   139 (**)

   142 fun by_tactic (Tactic.Model_Problem' (id, pbl, met)) (pt, pos)  =

   143     let

   144       val ((p, _), _, _, pt) = Specify_Step.add (Tactic.Model_Problem'(id, pbl, met))

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

   146 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

   147     in

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

   149     end

   150     (* called only if no_met is specified *)

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

   152       let

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

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

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

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

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

   158 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

   159       in

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

   161       end

   162   | by_tactic (Tactic.Refine_Problem' (rfd as (id, _))) (pt, pos)  =

   163       let

   164         val ctxt = get_ctxt pt pos

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

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

   167       in

   168         ("ok", ([(Tactic.Refine_Problem id, Tactic.Refine_Problem' rfd,

   169             (pos, (Istate_Def.Uistate,ctxt)))], [], (pt, pos)))

   170       end

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

   172       let

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

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

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

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

   177         val (p, pt) =

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

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

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

   181       in

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

   183       end

   184   | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =

   185       let

   186         val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)

   187         val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))

   188           (Istate_Def.Uistate, ctxt) (pt, pos)

   189       in

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

   191       end

   192   | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p)  = Specify.by_Add_ "#Given" ct (pt, p)

   193   | by_tactic (Tactic.Add_Find'  (ct, _)) (pt, p) = Specify.by_Add_ "#Find" ct (pt, p)

   194   | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_Add_"#Relate" ct (pt, p)

   195     (*strange old code, redes*)

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

   197       let

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

   199         val {spec = (dI, _, _), ctxt, ...} = Calc.specify_data (pt, (p, p_))

   200       in

   201         if domID = dI then

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

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

   204 	        let

   205 	          val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID)

   206 	            (Istate_Def.Uistate, ctxt) (pt, (p, p_))

   207 	        in

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

   209           end

   210       end

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

   213 fun initialisePIDEHACK HACKthy (fmz, (_, pI, mI)) =

   214     let

   215 (**)  val thy = HACKthy(**)

   216 (** )  val thy = ThyC.get_theory dI( **)

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

   218 	      if mI = ["no_met"]

   219 	      then

   220           let

   221             val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)

   222             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)

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

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

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

   226 		      end

   227 	      else

   228 	        let

   229 	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)

   230             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)

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

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

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

   234 	    val hdl = case cas of

   235 		    NONE => Auto_Prog.pblterm dI pI

   236 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t

   237 	    val hdlPIDE = case cas of

   238 		    NONE => Auto_Prog.pbltermPIDE dI pI

   239 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t

   240     in

   241       (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)

   242     end;

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

   244 (*  initialisePI <- nxt_specify_init_calc *)

   245 fun initialisePIDE (fmz, (dI, pI, mI)) =

   246     let

   247 	    val thy = ThyC.get_theory dI

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

   249 	      if mI = ["no_met"]

   250 	      then

   251           let

   252             val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)

   253             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)

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

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

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

   257 		      end

   258 	      else

   259 	        let

   260 	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)

   261             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)

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

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

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

   265 	    val hdl = case cas of

   266 		    NONE => Auto_Prog.pblterm dI pI

   267 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t

   268 	    val hdlPIDE = case cas of

   269 		    NONE => Auto_Prog.pbltermPIDE dI pI

   270 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t

   271     in

   272       (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)

   273     end;

   274 (*  nxt_specify_init_calc \<rightarrow> initialise *)

   275 fun nxt_specify_init_calc ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)

   276     if pI <> []

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

   278 	    let

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

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

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

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

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

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

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

   286 	      val pits = I_Model.init ppc

   287 	      val pt = update_pbl pt [] pits

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

   289     else

   290       if mI <> []

   291       then (* from met-browser *)

   292 	      let

   293           val {ppc, ...} = MethodC.from_store mI

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

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

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

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

   298 	        val mits = I_Model.init ppc

   299 	        val pt = update_met pt [] mits

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

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

   302 	      let

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

   304 	          ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)

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

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

   307     let            (* both ^^^  ^^^^^^^^^^^^  are either empty or complete *)

   308 	    val (_, hdl, (dI, pI, mI), pors, pctxt) = initialisePIDE (fmz, (dI, pI, mI))

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

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

   311     in

   312       ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))

   313     end

   315 (**)end(**)

author	wneuper <walther.neuper@jku.at>
	Thu, 29 Apr 2021 12:43:50 +0200
changeset 60268	637f20154de6
parent 60223	740ebee5948b
child 60469	89e1d8a633bb
permissions	-rw-r--r--