(* 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*)

   datatype match_model_prec = Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) | NoMatch_;

   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

 \<^isac_test>\<open>

   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

 \<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;

 fun eq1 d (_, (d', _)) = (d = d');

 (*  chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*)

 (*T_TESTold*)

 fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =

       (case find_first (eq1 d) pbt of 

         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))

       | NONE =>  (i, vats, false, f, I_Model.Sup (d, vs)))

   | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =

       (case find_first (eq1 d) pbt of 

         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))

       | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))

   | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm

   | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm

   | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =

       (case find_first (eq1 d) pbt of 

         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))

       | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))

   | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =

       (case find_first (eq1 d) pbt of

         SOME _ =>

           raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)"

       | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))

   | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";

 (*T_TEST*)

 fun chk_TEST (_: theory) pbt (i, vats, b, f, I_Model.Cor_TEST (d, vs)) =

       (case find_first (eq1 d) pbt of 

         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))

       | NONE =>  (i, vats, false, f, I_Model.Sup_TEST (d, vs)))

   | chk_TEST _ pbt (i, vats, b, f, I_Model.Inc_TEST (d, vs)) =

       (case find_first (eq1 d) pbt of 

         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))

       | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))

   | chk_TEST _ pbt (i, vats, b, f, I_Model.Sup_TEST (d, vs)) =

       (case find_first (eq1 d) pbt of 

         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor_TEST (d, vs))

       | NONE => (i, vats, false, f, I_Model.Sup_TEST (d, vs)))

 (*T_TESTnew*)

 fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;

 fun eq0 (0, _, _, _, _) = true

   | eq0 _ = false;

 fun max_i i [] = i

   | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;

 fun max_id [] = 0

   | max_id ((id, _, _, _, _) :: is) = max_i id is;

 fun add_idvat itms _ _ [] = itms

   | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =

     add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;

 (* find elements of pbt not contained in itms;

    if such one is untouched, return this one, otherwise create new itm *)

 fun chk_m itms untouched (p as (f, (d, id))) = 

   case find_first (eq2 p) itms of

 	  SOME _ => []

   | NONE =>

       (case find_first (eq2 p) untouched of

         SOME itm => [itm]

       | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);

 fun chk_mis mvat itms untouched pbt = 

     let val mis = (flat o (map (chk_m itms untouched))) pbt; 

         val mid = max_id itms;

     in add_idvat [] (mid + 1) mvat mis end;

 (*

   check a problem (ie. i?model) for matching a problemtype, 

   takes the Pre_Conds.max_variant for concluding completeness

 *)

 (*  match_itms: theory -> I_Model.T -> Model_Pattern.T * unchecked * Rule_Def.rule_set ->

          bool * (I_Model.T * (bool * term) list)*)

 fun match_itms thy itms (pbt, where_, where_rls) = 

   let

     fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;

     val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)

     val mvat = Pre_Conds.max_variant itms';

 	  val itms'' = filter (okv mvat) itms';

 	  val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)

 	  val mis = chk_mis mvat itms'' untouched pbt;

 	  val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_

 	    (pbt, I_Model.OLD_to_TEST itms'')

   in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;

 (* version for tactic Refine_Problem *)

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

     let

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

 	    (*TODO val where_ = map TermC.adapt_to_type where_ ...  adapt to current ctxt*)

 	    val (b, (itms', where_')) = match_itms thy 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 (b, (itms', where_')) = match_itms thy 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;

 (* 

   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 (I_Model.TEST_to_OLD itms) where_')]

       else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy (I_Model.TEST_to_OLD 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 (I_Model.TEST_to_OLD itms) where_')

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

       else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy (I_Model.TEST_to_OLD 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(**)