walther@59747: (* Title:  Specify/step-specify.sml
walther@59747:    Author: Walther Neuper 2019
walther@59747:    (c) due to copyright terms
walther@59747: *)
walther@59747: 
walther@59747: signature STEP_SPECIFY =
walther@59747: sig
walther@59791: (*val do_next: Step.specify_do_next requires LI.by_tactic, which is not yet known in Step_Specify*)
walther@60020:   val by_tactic_input: Tactic.input -> Calc.T -> string * Calc.state_post
walther@59981:   val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post
walther@59975: 
walther@60150:   val initialisePIDEHACK: theory -> Formalise.T ->
walther@60150:     term * term * References.T * O_Model.T * Proof.context
walther@60113:   val initialisePIDE: Formalise.T ->
walther@60114:     term * term * References.T * O_Model.T * Proof.context
walther@59946:   val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T
walther@59886: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
walther@60020:   (*NONE*)
walther@59886: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
walther@59747: 
walther@59747: end
walther@59747: 
walther@59747: (**)
walther@59747: structure Step_Specify(**): STEP_SPECIFY(**) =
walther@59747: struct
walther@59747: (**)
walther@59763: open Pos
walther@59763: open Ctree
walther@59977: open Specification
walther@59747: 
walther@59806: fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
walther@59763:     let
walther@59763:       val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
walther@59763:         PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
walther@59962:       | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
walther@59995:       val (_, pI, mI) = References.select ospec spec
walther@60154:       val mpc = (#ppc o MethodC.from_store) mI (* just for reuse I_Model.complete_method *)
walther@59970:       val {cas, ppc, ...} = Problem.from_store pI
walther@59958:       val pbl = I_Model.init ppc (* fill in descriptions *)
walther@59763:       (*----------------if you think, this should be done by the Dialog 
walther@59763:        in the java front-end, search there for WN060225-modelProblem----*)
walther@59763:       val (pbl, met) = case cas of
walther@59763:         NONE => (pbl, [])
walther@59988:   		| _ => I_Model.complete_method (oris, mpc, ppc, probl)
walther@59763:       (*----------------------------------------------------------------*)
walther@59763:       val tac_ = Tactic.Model_Problem' (pI, pbl, met)
walther@59933:       val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
walther@60020:     in
walther@60020:       ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
walther@60020:     end
walther@60021:   | by_tactic_input (Tactic.Add_Given ct) ptp = Specify.by_Add_ "#Given" ct ptp
walther@60021:   | by_tactic_input (Tactic.Add_Find  ct) ptp = Specify.by_Add_ "#Find"  ct ptp
walther@60021:   | by_tactic_input (Tactic.Add_Relation ct) ptp = Specify.by_Add_"#Relate" ct ptp
walther@60021: 
walther@60154:     (* called with MethodC.id_empty *)     
walther@59810:   | by_tactic_input (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p, _))) =
walther@59763:     let 
walther@59763:       val (oris, dI, ctxt) = case get_obj I pt p of
walther@59763:         (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)
walther@59962:       | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"
walther@59968:       val opt = Refine.refine_ori oris pI
walther@59763:     in 
walther@59763:       case opt of
walther@59763: 	      SOME pI' => 
walther@59763: 	        let 
walther@59970:             val {met, ...} = Problem.from_store pI'
walther@59763: 	          (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
walther@60154: 	          val mI = if length met = 0 then MethodC.id_empty else hd met
walther@59763: 	          val (pos, c, _, pt) = 
walther@59933: 		          Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)
walther@59763: 	        in
walther@60020: 	          ("ok", ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),
walther@60020: 	              (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
walther@59763:           end
walther@60021: 	    | NONE => ("failure", ([], [], ptp))
walther@59763:     end
walther@59806:   | by_tactic_input (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =
walther@59763:     let
walther@59763:       val (dI, dI', probl, ctxt) = case get_obj I pt p of
walther@59763:         PblObj {origin= (_, (dI, _, _), _), spec = (dI', _, _), probl, ctxt, ...} =>
walther@59763:           (dI, dI', probl, ctxt)
walther@59962:       | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"
walther@59879: 	    val thy = if dI' = ThyC.id_empty then dI else dI'
walther@59763:     in 
walther@59960:       case Refine.problem (ThyC.get_theory thy) pI probl of
walther@60021: 	      NONE => ("failure", ([], [], ptp))
walther@59763: 	    | SOME rfd => 
walther@59763: 	      let 
walther@59933:           val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
walther@59763: 	      in
walther@60020: 	        ("ok", ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd,
walther@60020:             (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
walther@59763:         end
walther@59763:     end
walther@60020:   | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
walther@59763:     let
walther@59763:       val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
walther@59763:         PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
walther@59763:           (oris, dI, dI', pI', probl, ctxt)
walther@59962:       | _ => raise ERROR ""
walther@59881: 	    val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
walther@59970:       val {ppc,where_,prls,...} = Problem.from_store pI
walther@59763: 	    val pbl = 
walther@59903: 	      if pI' = Problem.id_empty andalso pI = Problem.id_empty
walther@59958: 	      then (false, (I_Model.init ppc, []))
walther@59984: 	      else M_Match.match_itms_oris thy probl (ppc,where_,prls) oris
walther@59763: 	      (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
walther@59810: 	    val (c, pt) =
walther@59933: 	      case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
walther@59810:   	      ((_, Pbl), c, _, pt) => (c, pt)
walther@59962:   	    | _ => raise ERROR ""
walther@59763:     in
walther@60020:       ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl),
walther@60020:         (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
walther@59763:     end
walther@60014:   | by_tactic_input (Tactic.Specify_Method id) (pt, pos) =
walther@59763:     let
walther@60014:       val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
walther@60014:       val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
walther@60014:         (Istate_Def.Uistate, ctxt) (pt, pos)
walther@60011:     in
walther@60020:       ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),
walther@60020:         (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))
walther@59763:     end    
walther@59806:   | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
walther@59763:     let
walther@59763:       val ctxt = get_ctxt pt pos
walther@60014: 	    val (pos, c, _, pt) =            
walther@59933: 	      Specify_Step.add (Tactic.Specify_Theory' dI)  (Istate_Def.Uistate, ctxt) (pt, pos)
walther@59763:     in (*FIXXXME: check if pbl can still be parsed*)
walther@60020: 	    ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
walther@60020:         (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
walther@59763:     end
walther@59806:   | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
walther@59763:     let
walther@59763:       val ctxt = get_ctxt pt pos
walther@59933: 	    val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)
walther@59763:     in  (*FIXXXME: check if met can still be parsed*)
walther@60020: 	    ("ok", ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI,
walther@60020:         (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos)))
walther@59763:     end
walther@59962:   | by_tactic_input m' _ = raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')
walther@60020: (**)
walther@60020: 
walther@59806: 
walther@60015: fun by_tactic (Tactic.Model_Problem' (id, pbl, met)) (pt, pos)  =
walther@59806:     let 
walther@60015:       val ((p, _), _, _, pt) = Specify_Step.add (Tactic.Model_Problem'(id, pbl, met))
walther@60015:         (Istate_Def.Uistate, ContextC.empty) (pt, pos)
walther@60015: (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
walther@59806:     in
walther@59806:       ("ok", ([], [], (pt, (p, Pbl))))
walther@59806:     end
walther@59806:     (* called only if no_met is specified *)     
walther@59806:   | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =
walther@59806:       let
walther@59970:         val {met, thy,...} = Problem.from_store pIre
walther@60154:         val (domID, metID) = (Context.theory_name thy, if length met = 0 then MethodC.id_empty else hd met)
walther@59806:         val ((p,_), _, _, pt) = 
walther@59933: 	        Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))
walther@59846:             (Istate_Def.Uistate, ContextC.empty) (pt, pos)
walther@59806: (* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
walther@59806:       in 
walther@59806:         ("ok", ([], [], (pt,(p, Pbl))))
walther@59806:       end
walther@60021:   | by_tactic (Tactic.Refine_Problem' (rfd as (id, _))) (pt, pos)  =
walther@59806:       let
walther@59806:         val ctxt = get_ctxt pt pos
walther@59806:         val (pos, _, _, pt) =
walther@59933:           Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)
walther@59806:       in
walther@60021:         ("ok", ([(Tactic.Refine_Problem id, Tactic.Refine_Problem' rfd,
walther@60021:             (pos, (Istate_Def.Uistate,ctxt)))], [], (pt, pos)))
walther@59806:       end
walther@59810:   | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p, _)) =
walther@59806:       let
walther@59995:         val (_, _, _, _, _, _, ctxt, _) = case get_obj I pt p of
walther@59806:           PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, _, mI), ctxt, meth = met, ...} =>
walther@59806:             (oris, dI', pI', mI', dI, mI, ctxt, met)
walther@59962:         | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"
walther@59806:         val (p, pt) =
walther@59933:           case  Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
walther@59806:             ((p, Pbl), _, _, pt) => (p, pt)
walther@59962:           | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"
walther@59806:       in
walther@59806:         ("ok", ([], [], (pt, (p, Pbl))))
walther@59806:       end    
walther@60014:   | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =
walther@59806:       let
walther@60014:         val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
walther@60014:         val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
walther@60014:           (Istate_Def.Uistate, ctxt) (pt, pos)
walther@60011:       in
walther@59806:         ("ok", ([], [], (pt, pos)))
walther@60014:       end
walther@60016:   | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p)  = Specify.by_Add_ "#Given" ct (pt, p)
walther@60016:   | by_tactic (Tactic.Add_Find'  (ct, _)) (pt, p) = Specify.by_Add_ "#Find" ct (pt, p)
walther@60016:   | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_Add_"#Relate" ct (pt, p)
walther@60020:     (*strange old code, redes*)
walther@60015:   | by_tactic (Tactic.Specify_Theory' domID) (pt, (p, p_)) =
walther@59806:       let
walther@59806:         val p_ = case p_ of Met => Met | _ => Pbl
walther@60015:         val {spec = (dI, _, _), ctxt, ...} = Calc.specify_data (pt, (p, p_))
walther@59806:       in
walther@60015:         if domID = dI then
walther@60015:           ("ok", ([], [], (pt, (p, p_))))
walther@59806:         else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)
walther@59806: 	        let 
walther@60015: 	          val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID)
walther@60015: 	            (Istate_Def.Uistate, ctxt) (pt, (p, p_))
walther@59806: 	        in
walther@59806:             ("ok", ([], [], (pt, (p, p_))))
walther@59990:           end                
walther@59806:       end
walther@59806:   | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"
walther@59806: 
walther@60150: fun initialisePIDEHACK HACKthy (fmz, (dI, pI, mI)) = 
walther@60150:     let
walther@60150: (**)  val thy = HACKthy(**)
walther@60150: (** )  val thy = ThyC.get_theory dI( **)
walther@60150: 	    val (pI, (pors, pctxt), mI) = 
walther@60150: 	      if mI = ["no_met"] 
walther@60150: 	      then 
walther@60150:           let 
walther@60150:             val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
walther@60150:             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
walther@60150: 		        val pI' = Refine.refine_ori' pors pI;
walther@60150: 		      in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
walther@60150: 		        (hd o #met o Problem.from_store) pI')
walther@60150: 		      end
walther@60150: 	      else
walther@60150: 	        let
walther@60150: 	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
walther@60150:             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
walther@60150: 	        in (pI, (pors, pctxt), mI) end;
walther@60150: 	    val {cas, ppc, thy = thy', ...} = Problem.from_store pI (*take dI from _refined_ pbl*)
walther@60150: 	    val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
walther@60150: 	    val hdl = case cas of
walther@60150: 		    NONE => Auto_Prog.pblterm dI pI
walther@60150: 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
walther@60150: 	    val hdlPIDE = case cas of
walther@60150: 		    NONE => Auto_Prog.pbltermPIDE dI pI
walther@60150: 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
walther@60150:     in
walther@60150:       (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
walther@60150:     end;
walther@59806: (* create a calc-tree with oris via an cas.refined pbl *)
walther@60111: (*  initialisePI <- nxt_specify_init_calc *)
walther@60111: fun initialisePIDE (fmz, (dI, pI, mI)) = 
walther@60111:     let
walther@60111: 	    val thy = ThyC.get_theory dI
walther@60111: 	    val (pI, (pors, pctxt), mI) = 
walther@60111: 	      if mI = ["no_met"] 
walther@60111: 	      then 
walther@60111:           let 
walther@60112:             val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
walther@60112:             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
walther@60111: 		        val pI' = Refine.refine_ori' pors pI;
walther@60111: 		      in (pI', (pors (*refinement over models with diff.precond only*), pctxt),
walther@60111: 		        (hd o #met o Problem.from_store) pI')
walther@60111: 		      end
walther@60111: 	      else
walther@60111: 	        let
walther@60112: 	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy; (*..TermC.parseNEW'*)
walther@60112:             val pctxt = ContextC.initialise' thy fmz;                (*..DUPLICATE ermC.parseNEW'*)
walther@60111: 	        in (pI, (pors, pctxt), mI) end;
walther@60111: 	    val {cas, ppc, thy = thy', ...} = Problem.from_store pI (*take dI from _refined_ pbl*)
walther@60111: 	    val dI = Context.theory_name (ThyC.sub_common (thy, thy'))
walther@60111: 	    val hdl = case cas of
walther@60111: 		    NONE => Auto_Prog.pblterm dI pI
walther@60111: 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
walther@60113: 	    val hdlPIDE = case cas of
walther@60113: 		    NONE => Auto_Prog.pbltermPIDE dI pI
walther@60113: 		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values pors) t
walther@60111:     in
walther@60114:       (hdlPIDE, hdl, (dI, pI, mI), pors, pctxt)
walther@60111:     end;
walther@60111: (*  nxt_specify_init_calc \<rightarrow> initialise *)
walther@60111: fun nxt_specify_init_calc ([], (dI, pI, mI)) = (*this will probably be dropped with PIDE*)
walther@59806:     if pI <> [] 
walther@59806:     then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)
walther@59806: 	    let 
walther@59970:         val {cas, met, ppc, thy, ...} = Problem.from_store pI
walther@59880: 	      val dI = if dI = "" then Context.theory_name thy else dI
walther@59806: 	      val mI = if mI = [] then hd met else mI
walther@59806: 	      val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t
walther@59952: 	      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
walther@59846: 				  ([], (dI,pI,mI), hdl, ContextC.empty)
walther@59806: 	      val pt = update_spec pt [] (dI, pI, mI)
walther@59958: 	      val pits = I_Model.init ppc
walther@59806: 	      val pt = update_pbl pt [] pits
walther@59806: 	    in ((pt, ([] , Pbl)), []) end
walther@59806:     else 
walther@59806:       if mI <> [] 
walther@59806:       then (* from met-browser *)
walther@59806: 	      let 
walther@60154:           val {ppc, ...} = MethodC.from_store mI
walther@59806: 	        val dI = if dI = "" then "Isac_Knowledge" else dI
walther@59846: 	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
walther@59861: 	          ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
walther@59806: 	        val pt = update_spec pt [] (dI, pI, mI)
walther@59958: 	        val mits = I_Model.init ppc
walther@59806: 	        val pt = update_met pt [] mits
walther@59806: 	      in ((pt, ([], Met)), []) end
walther@59806:       else (* new example, pepare for interactive modeling *)
walther@59806: 	      let
walther@59846: 	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) 
walther@59976: 	          ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)
walther@59806: 	      in ((pt, ([], Pbl)), []) end
walther@59806:   | nxt_specify_init_calc (fmz, (dI, pI, mI)) = 
walther@60111:     let            (* both ^^^  ^^^^^^^^^^^^  are either empty or complete *)
walther@60114: 	    val (_, hdl, (dI, pI, mI), pors, pctxt) = initialisePIDE (fmz, (dI, pI, mI))
walther@59846:       val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt)
walther@59819:         (fmz, (dI, pI, mI)) (pors, (dI, pI, mI), hdl, pctxt)
walther@59806:     in
walther@60020:       ((pt, ([], Pbl)), (fst3 o snd) (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))
walther@59806:     end
walther@59763: 
walther@59763: (**)end(**)