wneuper/isa: src/Tools/isac/Specify/refine.sml@35846e25713e

     1 (* Title:  Specify/refine.sml

     2    Author: Walther Neuper 110226

     3    (c) due to copyright terms

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

     6 better fitting the respective where_-condition.

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

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

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

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

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

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

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

    17   before adapt_to_type: 01:05 sec:sec

    18   after  adapt_to_type:

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

    20   before adapt_to_type: 1.5 sec

    21   after  adapt_to_type:

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

    23   before adapt_to_type: 0.05 sec

    24   after  adapt_to_type:

    25 *)

    27 signature REFINE_PROBLEM =

    28 sig

    29 (**)

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

    32 (**)

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

    34 (**)

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

    37 \<^isac_test>\<open>

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

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

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

    41 (**)

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

    43 (**)

    44   val refined_: match_ list -> match_ option

    45 (**)

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

    47 (**)

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

    49 (**)

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

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

    52 \<close>

    53 end

    55 (**)

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

    57 struct

    58 (**)

    60 datatype match_ =

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

    62 | NoMatch_;

    64 fun is_matches_ (Match_ _) = true

    65   | is_matches_ _ = false;

    67 fun refined_ ms = ((find_first is_matches_) o rev) ms;

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

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

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

    73       (case find_first (eq1 d) pbt of

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

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

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

    77       (case find_first (eq1 d) pbt of

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

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

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

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

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

    83       (case find_first (eq1 d) pbt of

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

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

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

    87       (case find_first (eq1 d) pbt of

    88         SOME _ =>

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

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

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

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

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

    95   | eq0 _ = false;

    96 fun max_i i [] = i

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

    98 fun max_id [] = 0

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

   100 fun add_idvat itms _ _ [] = itms

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

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

   104 (* find elements of pbt not contained in itms;

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

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

   107   case find_first (eq2 p) itms of

   108 	  SOME _ => []

   109   | NONE =>

   110       (case find_first (eq2 p) untouched of

   111         SOME itm => [itm]

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

   114 fun chk_mis mvat itms untouched pbt =

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

   116         val mid = max_id itms;

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

   119 (* check a problem (ie. itm list) for matching a problemtype,

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

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

   122   let

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

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

   125     val mvat = I_Model.max_variant itms';

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

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

   128 	  val mis = chk_mis mvat itms'' untouched pbt;

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

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

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

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

   134     let

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

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

   137 	    val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);

   138     in

   139       if b

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

   141       else pbls @ [NoMatch_]

   142     end

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

   144     let

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

   146       val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);

   147     in if b

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

   149 	    in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end

   150        else (pbls @ [NoMatch_])

   151     end

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

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

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

   155     let

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

   157     in case last_elem pbls' of

   158       Match_ _ => pbls'

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

   160   end;

   162 fun problem thy pblID itms =

   163   case refined_ ((Store.apply (get_pbls ())) (refin'' thy ((rev o tl) pblID) itms [])

   164       pblID (rev pblID)) of

   165 	  NONE => NONE

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

   168 (*

   169   refine a problem; construct pblRD while scanning

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

   171 *)

   172 (** )

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

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

   175     then SOME (pblRD @ [pI])

   176     else NONE

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

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

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

   180 	      SOME pblRD' => SOME pblRD'

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

   182     else NONE

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

   184 and refins _ _ [] = NONE

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

   186     (case refin pblRD ori p of

   187       SOME pblRD' => SOME pblRD'

   188     | NONE => refins pblRD ori pts);

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

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

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

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

   194     let

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

   196       val model = map (Model_Pattern.adapt_to_type ctxt) model

   197       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_

   198     in

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

   200       then SOME (pblRD @ [pI])

   201       else NONE

   202     end

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

   204     let

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

   206       val model = map (Model_Pattern.adapt_to_type ctxt) model

   207       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_

   208     in

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

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

   211 	        SOME pblRD' => SOME pblRD'

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

   213       else NONE

   214     end

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

   216 and refins _ _ _ [] = NONE

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

   218     (case refin ctxt pblRD ori p of

   219       SOME pblRD' => SOME pblRD'

   220     | NONE => refins ctxt pblRD ori pts);

   222 \<^isac_test>\<open>

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

   224 (*

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

   226     let

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

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

   229       val oris = O_Model.init thy fmz model(* |> #1*);

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

   231       val (b, (itms, where_')) = M_Match.match_oris' thy oris (model, where_, where_rls)

   232     in

   233       if b

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

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

   236     end

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

   238     let

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

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

   241       val oris = O_Model.init thy fmz model(* |> #1*);

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

   243       val(b, (itms, where_')) = M_Match.match_oris' thy oris (model,where_,where_rls);

   244     in

   245       if b

   246       then

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

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

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

   250     end

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

   252 and refins' _ _ pbls [] = pbls

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

   254     let

   255       val pbls' = refin' pblRD fmz pbls p

   256     in

   257       case last_elem pbls' of

   258         M_Match.Matches _ => pbls'

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

   260     end;

   261 *)

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

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

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

   265     let

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

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

   268       val model = map (Model_Pattern.adapt_to_type ctxt) model

   269       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_

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

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

   272         M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)

   273     in

   274       if b

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

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

   277     end

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

   279     let

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

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

   282       val model = map (Model_Pattern.adapt_to_type ctxt) model

   283       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_

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

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

   286         M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)

   287     in

   288       if b

   289       then

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

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

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

   293     end

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

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

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

   297     let

   298       val pbls' = refin' ctxt pblRD fmz pbls p

   299     in

   300       case last_elem pbls' of

   301         M_Match.Matches _ => pbls'

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

   303     end;

   304 \<close>

   306 (*

   307   TODO: rename \<rightarrow> apply_to_node

   308   apply a fun to a ptyps node.

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

   310 *)

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

   313 (* TODO rename \<rightarrow> by_oris

   314    for tactic Refine_Tacitly

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

   316 fun refine_ori ctxt oris pblID =

   317   let

   318     val opt = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);

   319   in case opt of

   320       SOME pblRD =>

   321         let val pblID': Problem.id = rev pblRD

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

   323 	  | NONE => NONE

   324 	end;

   325 fun refine_ori' ctxt oris pI = perhaps (refine_ori ctxt oris) pI;

   327 \<^isac_test>\<open>

   328 fun xxxxx ctxt fmz pblID =

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

   330 \<close>

   332 (**)end(**)

author	wneuper <Walther.Neuper@jku.at>
	Thu, 10 Nov 2022 14:25:38 +0100
changeset 60590	35846e25713e
parent 60588	9a116f94c5a6
child 60653	fff1c0f0a9e7
permissions	-rw-r--r--