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

     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: theory -> Formalise.T ->

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

    14   val initialise': theory -> Formalise.T -> Calc.T * State_Steps.T

    15 end

    17 (**)

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

    19 struct

    20 (**)

    21 open Pos

    22 open Ctree

    23 open Specification

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

    26     let

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

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

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

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

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

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

    33 (*OLD* )

    34       val pbl = I_Model.init model (* fill in descriptions *)

    35 ( *---*)

    36       val pbl = I_Model.init_TEST oris model (* fill in descriptions *)

    37 (*NEW*)

    38       val (pbl, met) = case cas of

    39         NONE => (pbl, [])

    40 (*OLD* )

    41   		| _ => I_Model.complete_method (oris, mpc, model, probl)

    42 ( *---*)

    43   		| _ => I_Model.s_make_complete oris (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, mpc)

    44 (*NEW*)

    45       val tac_ = Tactic.Model_Problem' (pI, I_Model.TEST_to_OLD pbl, I_Model.TEST_to_OLD met)

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

    47     in

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

    49     end

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

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

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

    54     (* called with MethodC.id_empty *)

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

    56     let

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

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

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

    60       val opt = Refine.by_o_model ctxt oris pI

    61     in

    62       case opt of

    63 	      SOME pI' =>

    64 	        let

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

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

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

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

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

    70 	        in

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

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

    73           end

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

    75     end

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

    77     let

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

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

    80           (dI, dI', probl, ctxt)

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

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

    83     in

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

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

    86 	    | SOME rfd =>

    87 	      let

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

    89 	      in

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

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

    92         end

    93     end

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

    95     let

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

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

    98           (oris, pI', probl, ctxt)

    99       | _ => raise ERROR ""

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

   101 	    val pbl =

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

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

   104 	      else M_Match.match_itms_oris ctxt probl (model, where_, where_rls) oris

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

   106 	    val (c, pt) =

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

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

   109   	    | _ => raise ERROR ""

   110     in

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

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

   113     end

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

   115     let

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

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

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

   119     in

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

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

   122     end

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

   124     let

   125       val ctxt = get_ctxt pt pos

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

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

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

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

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

   131     end

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

   133     let

   134       val ctxt = get_ctxt pt pos

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

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

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

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

   139     end

   140   | by_tactic_input m' (ctree, pos) =

   141     let

   142       val ctxt = Ctree.get_ctxt ctree pos

   143     in

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

   145     end

   146 (**)

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

   150     let

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

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

   153 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

   154     in

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

   156     end

   157     (* called only if no_met is specified *)

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

   159       let

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

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

   162           if length solve_mets = 0 then MethodC.id_empty

   163           else hd solve_mets)

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

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

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

   167 (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

   168       in

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

   170       end

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

   172       let

   173         val ctxt = get_ctxt pt pos

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

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

   176       in

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

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

   179       end

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

   181       let

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

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

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

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

   186         val (p, pt) =

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

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

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

   190       in

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

   192       end

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

   194       let

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

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

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

   198       in

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

   200       end

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

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

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

   204     (*strange old code, redes*)

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

   206       let

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

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

   209       in

   210         if domID = dI then

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

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

   213 	        let

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

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

   216 	        in

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

   218           end

   219       end

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

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

   223 (*  initialise <-?-> initialise' *)

   224 fun initialise thy (fmz, (_, pI, mI)) =

   225     let

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

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

   228 	      if mI = ["no_met"]

   229 	      then

   230           let

   231             val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;

   232             val pI' = Refine.by_o_model' 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, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;

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

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

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

   242 	    val hdl = case cas of

   243 		    NONE => Auto_Prog.pblterm dI pI

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

   245 	    val hdlPIDE = case cas of

   246 		    NONE => Auto_Prog.pblterm dI pI

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

   248     in

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

   250     end;

   251 (*TODO: HOW RELATES initialise' \<longleftrightarrow> initialise *)

   252 fun initialise' thy ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)

   253     if pI <> []

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

   255 	    let

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

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

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

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

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

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

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

   263 	      val pits = I_Model.init (*Proof_Context.init_global thy*) model

   264 	      val pt = update_pbl pt [] pits

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

   266     else

   267       if mI <> []

   268       then (* from met-browser *)

   269 	      let

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

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

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

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

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

   275 	        val mits = I_Model.init (*Proof_Context.init_global thy*) model

   276 	        val pt = update_met pt [] mits

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

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

   279 	      let

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

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

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

   283   | initialise' thy (model, refs) =

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

   285 	    val (_, hdl, refs, pors, pctxt) = initialise thy (model, refs)

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

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

   288     in

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

   290     end

   292 (**)end(**)

author	wneuper <Walther.Neuper@jku.at>
	Sun, 24 Sep 2023 20:04:41 +0200
changeset 60752	77958bc6ed7d
parent 60742	bfff1825ba67
child 60753	30eb1f314f5c
permissions	-rw-r--r--