(* 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 got by @{term Know_Store.get_pbls} is costly such that 

\<open>ML_structure Know_Store\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, where_-condition (and cas).

The terms are where_-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted

according to the type suggested by the current \<open>ML_structure Context\<close>.

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 refine_ori : Proof.context -> O_Model.T -> Problem.id -> Problem.id option

(**)

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

\<^isac_test>\<open>

(*val test : Formalise.model -> Problem.id -> M_Match.T list*)

(*val refine : Formalise.model -> Problem.id -> M_Match.T list*)

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

(**)

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

(**)

  val refined_: match_ list -> match_ option

(**)

  val refin'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node -> match_ list

(**)

  val refins'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node list -> match_ list

(**)

(*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)

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

\<close>

end

(**)

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

struct

(**)

datatype match_ = 

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

| NoMatch_;

fun is_matches_ (Match_ _) = true

  | is_matches_ _ = false;

fun refined_ 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*)

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.";

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. itm list) for matching a problemtype, 

   takes the I_Model.max_variant for concluding completeness (could be another!) *)

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 = I_Model.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_ itms'' mvat

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

(* refine a problem; version for tactic Refine_Problem *)

fun refin'' _ (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

  | refin'' _ 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 refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end

       else (pbls @ [NoMatch_])

    end              

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

and refins'' _ _ _ pbls [] = pbls

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

    let

      val pbls' = refin'' thy pblRD itms pbls p

    in case last_elem pbls' of

      Match_ _ => pbls'

    | NoMatch_ => refins'' thy pblRD itms pbls' pts

  end;

fun problem thy pblID itms =

  case refined_ ((Store.apply (get_pbls ())) (refin'' 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 

  val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option

*)

(** )

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

    if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py) 

    then SOME (pblRD @ [pI])

    else NONE

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

    if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py) 

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

	      SOME pblRD' => SOME pblRD'

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

    else NONE

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

and refins _ _ [] = NONE

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

    (case refin pblRD ori p of

      SOME pblRD' => SOME pblRD'

    | NONE => refins pblRD ori pts);

( ** )TODO clean up after "...  "adapt to current ctxt"( **)

(*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)

(*val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)

fun refin 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 (Model_Pattern.adapt_term_to_type ctxt) where_

    in

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

      then SOME (pblRD @ [pI])

      else NONE

    end

  | refin 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 (Model_Pattern.adapt_term_to_type ctxt) where_

    in

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

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

	        SOME pblRD' => SOME pblRD'

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

      else NONE

    end

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

and refins _ _ _ [] = NONE

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

    (case refin ctxt pblRD ori p of

      SOME pblRD' => SOME pblRD'

    | NONE => refins ctxt pblRD ori pts);

\<^isac_test>\<open>

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

(*

fun refin' 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 oris = O_Model.init thy fmz model(* |> #1*);

      (* WN020803: itms!: oris might _not_ be complete here *)

      val (b, (itms, where_')) = M_Match.match_oris' thy 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' 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 oris = O_Model.init thy fmz model(* |> #1*);

      (* WN020803: itms!: oris might _not_ be complete here *)

      val(b, (itms, where_')) = M_Match.match_oris' thy 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' (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' pblRD fmz pbls ((p as Store.Node _) :: pts) =

    let

      val pbls' = refin' pblRD fmz pbls p

    in

      case last_elem pbls' of

        M_Match.Matches _ => pbls'

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

    end;

*)

(*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 (Model_Pattern.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.match_oris' (Proof_Context.theory_of 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 (Model_Pattern.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.match_oris' (Proof_Context.theory_of 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;

\<close>

(*

  TODO: rename \<rightarrow> apply_to_node

  apply a fun to a ptyps node.

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

*)

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

(* TODO rename \<rightarrow> by_oris

   for tactic Refine_Tacitly

   oris are already created wrt. some pbt; ctxt overrides thy in pbt  *)

fun refine_ori ctxt oris pblID =

  let

    val opt = app_ptyp (refin 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 refine_ori' ctxt oris pI = perhaps (refine_ori ctxt oris) pI;

\<^isac_test>\<open>

fun xxxxx ctxt fmz pblID =

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

\<close>

(**)end(**)