(* Title:  Specify/refine.sml

    Author: Walther Neuper 110226

    (c) due to copyright terms

 Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close> 

 better fitting the respective where_-condition.

 The search on the tree given by @{term Know_Store.get_pbls} is costly such that 

 \<open>ML_structure Know_Store\<close> holds terms pre-parsed with a most generally type. 

 On transfer to a calculation these terms are strongly typed by Model_Pattern.adapt_to_type

 (and users of this function in \<open>ML_structure Error_Pattern, MethodC, Problem\<close>)

 according to the current context.

 Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)

 are adapted for "adapt_to_type on the fly" until further clarification.

 timing (from evaluating imports to use-cases.sml) for Test_Isac_Short

   before adapt_to_type: 01:05 sec:sec

   after  adapt_to_type: 

 timing for test/../refine.sml --- equation with CalcTree [ = 6 / 5] for timing: ...

   before adapt_to_type: 1.5 sec

   after  adapt_to_type: 

 timing for test/../refine.sml --- refine ad-hoc equation for timing: ...

   before adapt_to_type: 0.05 sec

   after  adapt_to_type: 

 *)                          

 signature REFINE_PROBLEM =

 sig

   val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option

   val by_o_model : Proof.context -> O_Model.T -> Problem.id -> Problem.id option

   val by_o_model' : Proof.context -> O_Model.T -> Problem.id -> Problem.id

   val by_formalise: Proof.context -> Formalise.model -> Problem.id -> M_Match.T list

 (*from isac_test for Minisubpbl*)

   type match_model_prec

   val find_match: theory -> Problem.id -> I_Model.T -> match_model_prec list ->

     Problem.T Store.node -> match_model_prec list

   val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a

   val check_match: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node ->

     Problem.id option

   val refins: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node list ->

     Problem.id option

   val match_found: match_model_prec list -> match_model_prec option

   val find_matchs: theory -> Problem.id -> I_Model.T -> match_model_prec list -> Problem.T Store.node list -> match_model_prec list

 \<^isac_test>\<open>

 (**)

 \<close>

 end

 (**)

 structure Refine(**) : REFINE_PROBLEM(**) =

 struct

 (**)

 datatype match_model_prec = 

   Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))

 | NoMatch_;

 fun is_matches_ (Match_ _) = true

   | is_matches_ _ = false;

 fun match_found ms = ((find_first is_matches_) o rev) ms;

 (* version for tactic Refine_Problem *)

 (*OLD*)

 fun find_match _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =

     let

 	    val {thy, model, where_, where_rls, ...} = py

 	    val ctxt = Proof_Context.init_global thy

 	    val (b, where_') = M_Match.by_i_model ctxt  itms (model, where_, where_rls);

     in

       if b

       then pbls @ [Match_ (rev (pblRD @ [pI]), (itms, where_'))]

       else pbls @ [NoMatch_] 

     end

   | find_match _ pblRD itms pbls (Store.Node (pI, [py], pys)) =

     let

       val {thy, model, where_, where_rls, ...} = py 

 	    val ctxt = Proof_Context.init_global thy

 	    val (b, where_') = M_Match.by_i_model ctxt itms (model, where_, where_rls);

     in if b then

          let val pbl = Match_ (rev (pblRD @ [pI]), (itms, where_'))

 	       in find_matchs thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end

        else (pbls @ [NoMatch_])

     end              

   | find_match _ _ _ _ _ = raise ERROR "find_match: uncovered fun def."

 and find_matchs _ _ _ pbls [] = pbls

   | find_matchs thy pblRD itms pbls ((p as Store.Node _) :: pts) =

     let

       val pbls' = find_match thy pblRD itms pbls p

     in case last_elem pbls' of

       Match_ _ => pbls'

     | NoMatch_ => find_matchs thy pblRD itms pbls' pts

   end;

 fun problem thy pblID itms =

   case match_found ((Store.apply (get_pbls ())) (find_match thy ((rev o tl) pblID) itms [])

       pblID (rev pblID)) of

 	  NONE => NONE

   | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd

   | _ => raise ERROR "Refine.problem: undef. args";

 (* refine a problem; construct pblRD while scanning Problem.T Store.T*)

 (*TODO: as \<open>check_match: 'a -> .. -> 'b option\<close> could be ignorant of Store.T structure.*)

 fun check_match ctxt pblRD ori (Store.Node (pI, [py], [])) =

     let

       val {where_rls, model, where_, ...} = py: Problem.T

       val model = map (Model_Pattern.adapt_to_type ctxt) model

       val where_ = map (ParseC.adapt_term_to_type ctxt) where_

     in

       if M_Match.by_o_model ctxt ori (model, where_, where_rls) 

       then SOME (pblRD(**) @ [pI](**))

       else NONE

     end

   | check_match ctxt pblRD ori (Store.Node (pI, [py], pys)) =

     let

       val {where_rls, model, where_, ...} = py: Problem.T

       val model = map (Model_Pattern.adapt_to_type ctxt) model

       val where_ = map (ParseC.adapt_term_to_type ctxt) where_

     in

       if M_Match.by_o_model ctxt ori (model, where_, where_rls)

       then (case refins ctxt (pblRD @ [pI]) ori pys of

 	        SOME pblRD' => SOME pblRD'

 	      | NONE => SOME (pblRD (**)@ [pI](**)))

       else NONE

     end

   | check_match _ _ _ _ = raise ERROR "check_match: uncovered fun def."

 and refins _ _ _ [] = NONE

   | refins ctxt pblRD ori ((p as Store.Node _) :: pts) =

     (case check_match ctxt pblRD ori p of

       SOME pblRD' => SOME pblRD'

     | NONE => refins ctxt pblRD ori pts)

 \<^isac_test>\<open>

 (**)

 \<close>

 (* refine a problem; version providing output for math authors *)

 (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list -> 

     Probl_Def.T Store.node -> M_Match.T list*)

 fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =

     let

       val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])

       val {thy, model, where_, where_rls, ...} = py 

       val model = map (Model_Pattern.adapt_to_type ctxt) model

       val where_ = map (ParseC.adapt_term_to_type ctxt) where_

       val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)

       val (b, (itms, where_')) =

         M_Match.data_by_o ctxt oris (model, where_, where_rls)

     in                                                  

       if b

       then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]

       else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]

     end

   | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =

     let

       val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])

       val {thy, model, where_, where_rls, ...} = py 

       val model = map (Model_Pattern.adapt_to_type ctxt) model

       val where_ = map (ParseC.adapt_term_to_type ctxt) where_

       val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)

       val (b, (itms, where_')) =

         M_Match.data_by_o ctxt oris (model, where_, where_rls)

     in

       if b 

       then

         let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')

 	      in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end

       else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])

     end

   | refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."

 and refins' _ _ _ pbls [] = pbls

   | refins' ctxt pblRD fmz pbls ((p as Store.Node _) :: pts) =

     let

       val pbls' = refin' ctxt pblRD fmz pbls p

     in

       case last_elem pbls' of

         M_Match.Matches _ => pbls'

       | M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts

     end;

 (* Store.apply scans Store.T only to the first hit *)

 (*val find_node_elem: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a*)

 fun find_node_elem x = Store.apply (get_pbls ()) x;

 (*for tactic Refine_Tacitly; oris are already created wrt. some pbt; ctxt overrides thy in pbt*)

 fun by_o_model ctxt oris pblID =

   let

     val opt = find_node_elem (check_match ctxt ((rev o tl) pblID) oris) pblID (rev pblID);

   in case opt of 

       SOME pblRD =>

         let val pblID': Problem.id = rev pblRD

 			  in if pblID' = pblID then NONE else SOME pblID' end

 	  | NONE => NONE

 	end;

 fun by_o_model' ctxt oris pI = perhaps (by_o_model ctxt oris) pI;

 (*specifically for tests*)

 fun by_formalise ctxt fmz pblID =

   find_node_elem (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);

 \<^isac_test>\<open>

 (**)

 \<close>

 (**)end(**)