src/Tools/isac/Specify/refine.sml
author wneuper <Walther.Neuper@jku.at>
Sat, 28 Jan 2023 13:21:39 +0100
changeset 60658 1c089105f581
parent 60653 fff1c0f0a9e7
child 60660 c4b24621077e
permissions -rw-r--r--
cleanup parse #1: start eliminate parseNEW
     1 (* Title:  Specify/refine.sml
     2    Author: Walther Neuper 110226
     3    (c) due to copyright terms
     4 
     5 Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close> 
     6 better fitting the respective where_-condition.
     7 
     8 The search on the tree given by @{term Know_Store.get_pbls} is costly such that 
     9 \<open>ML_structure Know_Store\<close> holds terms pre-parsed with a most generally type. 
    10 
    11 On transfer to a calculation these terms are strongly typed by Model_Pattern.adapt_to_type
    12 (and users of this function in \<open>ML_structure Error_Pattern, MethodC, Problem\<close>)
    13 according to the current context.
    14 
    15 Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
    16 are adapted for "adapt_to_type on the fly" until further clarification.
    17 
    18 timing (from evaluating imports to use-cases.sml) for Test_Isac_Short
    19   before adapt_to_type: 01:05 sec:sec
    20   after  adapt_to_type: 
    21 timing for test/../refine.sml --- equation with CalcTree [ = 6 / 5] for timing: ...
    22   before adapt_to_type: 1.5 sec
    23   after  adapt_to_type: 
    24 timing for test/../refine.sml --- refine ad-hoc equation for timing: ...
    25   before adapt_to_type: 0.05 sec
    26   after  adapt_to_type: 
    27 *)                          
    28 
    29 signature REFINE_PROBLEM =
    30 sig
    31 (**)
    32   val problem: theory -> Problem.id -> I_Model.T -> (Problem.id * (I_Model.T * Pre_Conds.T)) option
    33 
    34 (**)
    35   val refine_ori : Proof.context -> O_Model.T -> Problem.id -> Problem.id option
    36 (**)
    37   val refine_ori' : Proof.context -> O_Model.T -> Problem.id -> Problem.id
    38 
    39 \<^isac_test>\<open>
    40 (*val test : Formalise.model -> Problem.id -> M_Match.T list*)
    41 (*val refine : Formalise.model -> Problem.id -> M_Match.T list*)
    42   val xxxxx: Proof.context -> Formalise.model -> Problem.id -> M_Match.T list
    43 (**)
    44   datatype match_ = Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T)) | NoMatch_;
    45 (**)
    46   val refined_: match_ list -> match_ option
    47 (**)
    48   val refin'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node -> match_ list
    49 (**)
    50   val refins'': theory -> Problem.id -> I_Model.T -> match_ list -> Problem.T Store.node list -> match_ list
    51 (**)
    52 (*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
    53   val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
    54 \<close>
    55 end
    56 
    57 (**)
    58 structure Refine(**) : REFINE_PROBLEM(**) =
    59 struct
    60 (**)
    61 
    62 datatype match_ = 
    63   Match_ of Problem.id * (( I_Model.T) * (Pre_Conds.T))
    64 | NoMatch_;
    65 
    66 fun is_matches_ (Match_ _) = true
    67   | is_matches_ _ = false;
    68 
    69 fun refined_ ms = ((find_first is_matches_) o rev) ms;
    70 
    71 fun eq1 d (_, (d', _)) = (d = d');
    72 
    73 (*  chk_: theory -> ('a * (term * term)) list -> I_Model.single -> I_Model.single*)
    74 fun chk_ (_: theory) pbt (i, vats, b, f, I_Model.Cor ((d, vs), _)) =
    75       (case find_first (eq1 d) pbt of 
    76         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
    77       | NONE =>  (i, vats, false, f, I_Model.Sup (d, vs)))
    78   | chk_ _ pbt (i, vats, b, f, I_Model.Inc ((d, vs), _)) =
    79       (case find_first (eq1 d) pbt of 
    80         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))
    81       | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
    82   | chk_ _ _ (itm as (_, _, _, _, I_Model.Syn _)) = itm
    83   | chk_ _ _ (itm as (_, _, _, _, I_Model.Typ _)) = itm
    84   | chk_ _ pbt (i, vats, b, f, I_Model.Sup (d, vs)) =
    85       (case find_first (eq1 d) pbt of 
    86         SOME (_, (_, id)) => (i, vats, b, f, I_Model.Cor ((d,vs), (id, [Input_Descript.join'''' (d, vs)])))
    87       | NONE => (i, vats, false, f, I_Model.Sup (d, vs)))
    88   | chk_ _ pbt (i, vats, _, f, I_Model.Mis (d, vs)) =
    89       (case find_first (eq1 d) pbt of
    90         SOME _ =>
    91           raise ERROR "chk_: ((i,vats,b,f,I_Model.Cor ((d,vs),(id, Input_Descript.join'''' d vs))):itm)"
    92       | NONE => (i, vats, false, f, I_Model.Sup (d, [vs])))
    93   | chk_ _ _ _ = raise ERROR "chk_: uncovered fun def.";
    94 
    95 fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
    96 fun eq0 (0, _, _, _, _) = true
    97   | eq0 _ = false;
    98 fun max_i i [] = i
    99   | max_i i ((id, _, _, _, _) :: is) = if i > id then max_i i is else max_i id is;
   100 fun max_id [] = 0
   101   | max_id ((id, _, _, _, _) :: is) = max_i id is;
   102 fun add_idvat itms _ _ [] = itms
   103   | add_idvat itms i mvat ((_, _, b, f, itm_) :: its) =
   104     add_idvat (itms @ [(i, [], b, f, itm_)]) (i + 1) mvat its;
   105 
   106 (* find elements of pbt not contained in itms;
   107    if such one is untouched, return this one, otherwise create new itm *)
   108 fun chk_m itms untouched (p as (f, (d, id))) = 
   109   case find_first (eq2 p) itms of
   110 	  SOME _ => []
   111   | NONE =>
   112       (case find_first (eq2 p) untouched of
   113         SOME itm => [itm]
   114       | NONE => [(0, [], false, f, I_Model.Mis (d, id))]);
   115 
   116 fun chk_mis mvat itms untouched pbt = 
   117     let val mis = (flat o (map (chk_m itms untouched))) pbt; 
   118         val mid = max_id itms;
   119     in add_idvat [] (mid + 1) mvat mis end;
   120 
   121 (* check a problem (ie. itm list) for matching a problemtype, 
   122    takes the I_Model.max_variant for concluding completeness (could be another!) *)
   123 fun match_itms thy itms (pbt, where_, where_rls) = 
   124   let
   125     fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
   126     val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
   127     val mvat = I_Model.max_variant itms';
   128 	  val itms'' = filter (okv mvat) itms';
   129 	  val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
   130 	  val mis = chk_mis mvat itms'' untouched pbt;
   131 	  val (pb, where_')  = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms'' mvat
   132   in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
   133 
   134 (* refine a problem; version for tactic Refine_Problem *)
   135 fun refin'' _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
   136     let
   137 	    val {thy, model, where_, where_rls, ...} = py
   138 	    (*TODO val where_ = map TermC.adapt_to_type where_ ...  adapt to current ctxt*)
   139 	    val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
   140     in
   141       if b
   142       then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', where_'))]
   143       else pbls @ [NoMatch_] 
   144     end
   145   | refin'' _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
   146     let
   147       val {thy, model, where_, where_rls, ...} = py 
   148       val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
   149     in if b 
   150        then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', where_'))
   151 	    in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
   152        else (pbls @ [NoMatch_])
   153     end              
   154   | refin'' _ _ _ _ _ = raise ERROR "refin'': uncovered fun def."
   155 and refins'' _ _ _ pbls [] = pbls
   156   | refins'' thy pblRD itms pbls ((p as Store.Node _) :: pts) =
   157     let
   158       val pbls' = refin'' thy pblRD itms pbls p
   159     in case last_elem pbls' of
   160       Match_ _ => pbls'
   161     | NoMatch_ => refins'' thy pblRD itms pbls' pts
   162   end;
   163 
   164 fun problem thy pblID itms =
   165   case refined_ ((Store.apply (get_pbls ())) (refin'' thy ((rev o tl) pblID) itms [])
   166       pblID (rev pblID)) of
   167 	  NONE => NONE
   168   | SOME (Match_ (rfd as (pI', _))) => if pblID = pI' then NONE else SOME rfd;
   169 
   170 (* 
   171   refine a problem; construct pblRD while scanning 
   172   val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option
   173 *)
   174 (** )
   175 fun refin pblRD ori (Store.Node (pI, [py], [])) =
   176     if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py) 
   177     then SOME (pblRD @ [pI])
   178     else NONE
   179   | refin pblRD ori (Store.Node (pI, [py], pys)) =
   180     if M_Match.match_oris (#thy py) (#where_rls py) ori (#model py, #where_ py) 
   181     then (case refins (pblRD @ [pI]) ori pys of
   182 	      SOME pblRD' => SOME pblRD'
   183 	    | NONE => SOME (pblRD @ [pI]))
   184     else NONE
   185   | refin _ _ _ = raise ERROR "refin: uncovered fun def."
   186 and refins _ _ [] = NONE
   187   | refins pblRD ori ((p as Store.Node _) :: pts) =
   188     (case refin pblRD ori p of
   189       SOME pblRD' => SOME pblRD'
   190     | NONE => refins pblRD ori pts);
   191 ( ** )TODO clean up after "...  "adapt to current ctxt"( **)
   192 
   193 (*val refin: Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
   194 (*val refin: Proof.context -> Problem.id -> O_Model.T -> Problem.T Store.node -> Problem.id option*)
   195 fun refin ctxt pblRD ori (Store.Node (pI, [py], [])) =
   196     let
   197       val {where_rls, model, where_, ...} = py: Problem.T
   198       val model = map (Model_Pattern.adapt_to_type ctxt) model
   199       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
   200     in
   201       if M_Match.match_oris ctxt where_rls ori (model, where_) 
   202       then SOME (pblRD @ [pI])
   203       else NONE
   204     end
   205   | refin ctxt pblRD ori (Store.Node (pI, [py], pys)) =
   206     let
   207       val {where_rls, model, where_, ...} = py: Problem.T
   208       val model = map (Model_Pattern.adapt_to_type ctxt) model
   209       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
   210     in
   211       if M_Match.match_oris ctxt where_rls ori (model, where_) 
   212       then (case refins ctxt (pblRD @ [pI]) ori pys of
   213 	        SOME pblRD' => SOME pblRD'
   214 	      | NONE => SOME (pblRD @ [pI]))
   215       else NONE
   216     end
   217   | refin _ _ _ _ = raise ERROR "refin: uncovered fun def."
   218 and refins _ _ _ [] = NONE
   219   | refins ctxt pblRD ori ((p as Store.Node _) :: pts) =
   220     (case refin ctxt pblRD ori p of
   221       SOME pblRD' => SOME pblRD'
   222     | NONE => refins ctxt pblRD ori pts);
   223 
   224 \<^isac_test>\<open>
   225 (* refine a problem; version providing output for math-experts *)
   226 (*val refin': Proof.context -> Problem.id -> Formalise.model -> M_Match.T list -> 
   227     Probl_Def.T Store.node -> M_Match.T list*)
   228 fun refin' ctxt pblRD fmz pbls (Store.Node (pI, [py: Probl_Def.T], [])) =
   229     let
   230       val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
   231       val {thy, model, where_, where_rls, ...} = py 
   232       val model = map (Model_Pattern.adapt_to_type ctxt) model
   233       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
   234       val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
   235       val (b, (itms, where_')) =
   236         M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
   237     in                                                  
   238       if b
   239       then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
   240       else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
   241     end
   242   | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =
   243     let
   244       val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
   245       val {thy, model, where_, where_rls, ...} = py 
   246       val model = map (Model_Pattern.adapt_to_type ctxt) model
   247       val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
   248       val (oris, _) = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
   249       val (b, (itms, where_')) =
   250         M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
   251     in
   252       if b 
   253       then
   254         let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')
   255 	      in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
   256       else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])
   257     end
   258   | refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."
   259 and refins' _ _ _ pbls [] = pbls
   260   | refins' ctxt pblRD fmz pbls ((p as Store.Node _) :: pts) =
   261     let
   262       val pbls' = refin' ctxt pblRD fmz pbls p
   263     in
   264       case last_elem pbls' of
   265         M_Match.Matches _ => pbls'
   266       | M_Match.NoMatch _ => refins' ctxt pblRD fmz pbls' pts
   267     end;
   268 \<close>
   269 
   270 (*
   271   TODO: rename \<rightarrow> apply_to_node
   272   apply a fun to a ptyps node.
   273   val app_ptyp: (Probl_Def.T Store.node -> 'a) -> Store.key -> Store.key -> 'a
   274 *)
   275 fun app_ptyp x = Store.apply (get_pbls ()) x;
   276 
   277 (* TODO rename \<rightarrow> by_oris
   278    for tactic Refine_Tacitly
   279    oris are already created wrt. some pbt; ctxt overrides thy in pbt  *)
   280 fun refine_ori ctxt oris pblID =
   281   let
   282     val opt = app_ptyp (refin ctxt ((rev o tl) pblID) oris) pblID (rev pblID);
   283   in case opt of 
   284       SOME pblRD =>
   285         let val pblID': Problem.id = rev pblRD
   286 			  in if pblID' = pblID then NONE else SOME pblID' end
   287 	  | NONE => NONE
   288 	end;
   289 fun refine_ori' ctxt oris pI = perhaps (refine_ori ctxt oris) pI;
   290 
   291 \<^isac_test>\<open>
   292 fun xxxxx ctxt fmz pblID =
   293   app_ptyp (refin' ctxt ((rev o tl) pblID) fmz []) pblID (rev pblID);
   294 \<close>
   295 
   296 (**)end(**)