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

     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 initialise: Proof.context -> Formalise.T ->

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

    14   val initialise_PIDE: theory -> Formalise.T ->

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

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

    17   val nxt_specify_init_calc_PIDE: theory -> Formalise.T -> Calc.T * State_Steps.T

    18 end

    20 (**)

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

    22 struct

    23 (**)

    24 open Pos

    25 open Ctree

    26 open Specification

    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       | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"

    33       val (_, pI, mI) = References.select_input ospec spec

    34       val mpc = (#model o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *)

    35       val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI

    36       val pbl = I_Model.init model (* 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   		| _ => I_Model.complete_method (oris, mpc, model, 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

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

    47     end

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

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

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

    52     (* called with MethodC.id_empty *)

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

    54     let

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

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

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

    58       val opt = Refine.refine_ori ctxt oris pI

    59     in

    60       case opt of

    61 	      SOME pI' =>

    62 	        let

    63             val {solve_mets, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'

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

    65 	          val mI = if length solve_mets = 0 then MethodC.id_empty else hd solve_mets

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

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

    68 	        in

    69 	          ("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),

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

    71           end

    72 	    | NONE => ("failure", ([], [], ptp))

    73     end

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

    75     let

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

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

    78           (dI, dI', probl, ctxt)

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

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

    81     in

    82       case Refine.problem (ThyC.get_theory_PIDE ctxt thy) pI probl of

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

    84 	    | SOME rfd =>

    85 	      let

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

    87 	      in

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

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

    90         end

    91     end

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

    93     let

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

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

    96           (oris, pI', probl, ctxt)

    97       | _ => raise ERROR ""

    98       val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI

    99 	    val pbl =

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

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

   102 	      else M_Match.match_itms_oris ctxt probl (model, where_, where_rls) 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' (ctree, pos) =

   139     let

   140       val ctxt = Ctree.get_ctxt ctree pos

   141     in

   142       raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string ctxt m')

   143     end

   144 (**)

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

   148     let

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

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

   151 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

   152     in

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

   154     end

   155     (* called only if no_met is specified *)

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

   157       let

   158         val {solve_mets, thy,...} = Problem.from_store (Ctree.get_ctxt pt pos) pIre

   159         val (domID, metID) = (Context.theory_name thy,

   160           if length solve_mets = 0 then MethodC.id_empty

   161           else hd solve_mets)

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

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

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

   165 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

   166       in

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

   168       end

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

   170       let

   171         val ctxt = get_ctxt pt pos

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

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

   174       in

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

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

   177       end

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

   179       let

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

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

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

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

   184         val (p, pt) =

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

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

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

   188       in

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

   190       end

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

   192       let

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

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

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

   196       in

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

   198       end

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

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

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

   202     (*strange old code, redes*)

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

   204       let

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

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

   207       in

   208         if domID = dI then

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

   210         else (*FIXME: check model wrt. (new!) domID ..? still parsable?*)

   211 	        let

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

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

   214 	        in

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

   216           end

   217       end

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

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

   221 (*  initialise <-?-> nxt_specify_init_calc *)

   222 fun initialise ctxt (fmz, (dI, pI, mI)) =

   223     let

   224 	    val thy = ThyC.get_theory_PIDE ctxt dI

   225 	    val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)

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

   227 	      if mI = ["no_met"]

   228 	      then

   229           let

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

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

   232 		        val pI' = Refine.refine_ori' pctxt pors pI;

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

   234 		        (hd o #solve_mets o Problem.from_store ctxt) pI')

   235 		      end

   236 	      else

   237 	        let

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

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

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

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

   242 	    val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))

   243 	    val hdl = case cas of

   244 		    NONE => Auto_Prog.pblterm dI pI

   245 		  | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t

   246 	    val hdlPIDE = case cas of

   247 		    NONE => Auto_Prog.pblterm dI pI

   248 		  | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t

   249     in

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

   251     end;

   252 (*  initialise <-?-> nxt_specify_init_calc *)

   253 fun initialise_PIDE thy (fmz, (_, pI, mI)) =

   254     let

   255 (*old* )val thy = ThyC.get_theory_PIDE ctxt dI( *old*)

   256 	    val ctxt = Proof_Context.init_global thy (* ctxt restricted to Formalise *)

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

   258 	      if mI = ["no_met"]

   259 	      then

   260           let

   261 (*old* )    val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)

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

   263 ( *new*)    val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;

   264             val pI' = Refine.refine_ori' pctxt pors pI;

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

   266             (hd o #solve_mets o Problem.from_store ctxt) pI')

   267           end

   268 	      else

   269 	        let

   270 (*old* )    val pors = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz; (*..TermC.parseNEW'*)

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

   272 (*old*)   in (pI, (pors, pctxt), mI) end;

   273 ( *new*)    val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init_PIDE thy fmz;

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

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

   276 	    val dI = Context.theory_name (Sub_Problem.common_sub_thy (thy, thy'))

   277 	    val hdl = case cas of

   278 		    NONE => Auto_Prog.pblterm dI pI

   279 		  | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t

   280 	    val hdlPIDE = case cas of

   281 		    NONE => Auto_Prog.pblterm dI pI

   282 		  | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ O_Model.values pors) t

   283     in

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

   285     end;

   286 (*TODO: HOW RELATES nxt_specify_init_calc \<longleftrightarrow> initialise *)

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

   288     if pI <> []

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

   290 	    let

   291         val {cas, solve_mets, model, thy, ...} = Problem.from_store ctxt pI

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

   293 	      val mI = if mI = [] then hd solve_mets else mI

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

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

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

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

   298 	      val pits = I_Model.init model

   299 	      val pt = update_pbl pt [] pits

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

   301     else

   302       if mI <> []

   303       then (* from met-browser *)

   304 	      let

   305           val {model, ...} = MethodC.from_store ctxt mI

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

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

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

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

   310 	        val mits = I_Model.init model

   311 	        val pt = update_met pt [] mits

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

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

   314 	      let

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

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

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

   318   | nxt_specify_init_calc ctxt (model, (dI, pI, mI)) =

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

   320 	    val (_, hdl, (dI, pI, mI), pors, pctxt) = initialise ctxt (model, (dI, pI, mI))

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

   322         (model, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)

   323     in

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

   325     end

   326 fun nxt_specify_init_calc_PIDE thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)

   327     if pI <> []

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

   329 	    let

   330         val {cas, solve_mets, model, thy, ...} = Problem.from_store (Proof_Context.init_global thy) pI

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

   332 	      val mI = if mI = [] then hd solve_mets else mI

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

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

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

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

   337 	      val pits = I_Model.init model

   338 	      val pt = update_pbl pt [] pits

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

   340     else

   341       if mI <> []

   342       then (* from met-browser *)

   343 	      let

   344           val {model, ...} = MethodC.from_store (Proof_Context.init_global thy) mI

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

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

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

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

   349 	        val mits = I_Model.init model

   350 	        val pt = update_met pt [] mits

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

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

   353 	      let

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

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

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

   357   | nxt_specify_init_calc_PIDE thy (model, refs) =

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

   359 	    val (_, hdl, refs, pors, pctxt) = initialise_PIDE thy (model, refs)

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

   361         (model, refs) (pors, refs, hdl, pctxt)

   362     in

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

   364     end

   366 (**)end(**)

author	wneuper <Walther.Neuper@jku.at>
	Wed, 25 Jan 2023 15:52:33 +0100
changeset 60651	b7a2ad3b3d45
parent 60638	8942f07ead44
child 60652	75003e8f96ab
permissions	-rw-r--r--