1.1 --- a/src/Tools/isac/Specify/refine.sml Mon Oct 31 18:28:36 2022 +0100
1.2 +++ b/src/Tools/isac/Specify/refine.sml Mon Nov 07 17:37:20 2022 +0100
1.3 @@ -3,11 +3,11 @@
1.4 (c) due to copyright terms
1.5
1.6 Refine a problem by a search for a \<open>ML_structure Model_Pattern\<close>
1.7 -better fitting the respective pre-condition.
1.8 +better fitting the respective where_-condition.
1.9
1.10 The search on the tree got by @{term KEStore_Elems.get_pbls} is costly such that
1.11 -\<open>ML_structure KEStore_Elems\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, pre-condition (and cas).
1.12 -The terms are pre-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted
1.13 +\<open>ML_structure KEStore_Elems\<close> holds terms in \<open>ML_structure Model_Pattern\<close>, where_-condition (and cas).
1.14 +The terms are where_-compiled with the most general \<open>ML_type "'a"\<close> and the type is adapted
1.15 according to the type suggested by the current \<open>ML_structure Context\<close>.
1.16
1.17 Note: From the children of eb89f586b0b2 onwards the old functions (\<open>term TermC.typ_a2real\<close> etc)
1.18 @@ -118,7 +118,7 @@
1.19
1.20 (* check a problem (ie. itm list) for matching a problemtype,
1.21 takes the I_Model.max_variant for concluding completeness (could be another!) *)
1.22 -fun match_itms thy itms (pbt, pre, where_rls) =
1.23 +fun match_itms thy itms (pbt, where_, where_rls) =
1.24 let
1.25 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
1.26 val itms' = map (chk_ thy pbt) itms; (* all found are #3 true *)
1.27 @@ -126,26 +126,26 @@
1.28 val itms'' = filter (okv mvat) itms';
1.29 val untouched = filter eq0 itms; (* i.e. dsc only (from init)*)
1.30 val mis = chk_mis mvat itms'' untouched pbt;
1.31 - val (pb, pre') = Pre_Conds.check where_rls pre itms'' mvat
1.32 - in (length mis = 0 andalso pb, (itms'@ mis, pre')) end;
1.33 + val (pb, where_') = Pre_Conds.check where_rls where_ itms'' mvat
1.34 + in (length mis = 0 andalso pb, (itms'@ mis, where_')) end;
1.35
1.36 (* refine a problem; version for tactic Refine_Problem *)
1.37 fun refin'' _ (pblRD: Problem.id) itms pbls (Store.Node (pI, [py], [])) =
1.38 let
1.39 val {thy, model, where_, where_rls, ...} = py
1.40 (*TODO val where_ = map TermC.adapt_to_type where_ ... adapt to current ctxt*)
1.41 - val (b, (itms', pre')) = match_itms thy itms (model, where_, where_rls);
1.42 + val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
1.43 in
1.44 if b
1.45 - then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', pre'))]
1.46 + then pbls @ [Match_ (rev (pblRD @ [pI]), (itms', where_'))]
1.47 else pbls @ [NoMatch_]
1.48 end
1.49 | refin'' _ pblRD itms pbls (Store.Node (pI, [py], pys)) =
1.50 let
1.51 val {thy, model, where_, where_rls, ...} = py
1.52 - val (b, (itms', pre')) = match_itms thy itms (model, where_, where_rls);
1.53 + val (b, (itms', where_')) = match_itms thy itms (model, where_, where_rls);
1.54 in if b
1.55 - then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', pre'))
1.56 + then let val pbl = Match_ (rev (pblRD @ [pI]), (itms', where_'))
1.57 in refins'' thy (pblRD @ [pI]) itms (pbls @ [pbl]) pys end
1.58 else (pbls @ [NoMatch_])
1.59 end
1.60 @@ -228,11 +228,11 @@
1.61 val {thy, model, where_, where_rls, ...} = py
1.62 val oris = O_Model.init thy fmz model(* |> #1*);
1.63 (* WN020803: itms!: oris might _not_ be complete here *)
1.64 - val (b, (itms, pre')) = M_Match.match_oris' thy oris (model, where_, where_rls)
1.65 + val (b, (itms, where_')) = M_Match.match_oris' thy oris (model, where_, where_rls)
1.66 in
1.67 if b
1.68 - then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
1.69 - else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
1.70 + then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
1.71 + else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
1.72 end
1.73 | refin' pblRD fmz pbls (Store.Node (pI, [py], pys)) =
1.74 let
1.75 @@ -240,13 +240,13 @@
1.76 val {thy, model, where_, where_rls, ...} = py
1.77 val oris = O_Model.init thy fmz model(* |> #1*);
1.78 (* WN020803: itms!: oris might _not_ be complete here *)
1.79 - val(b, (itms, pre')) = M_Match.match_oris' thy oris (model,where_,where_rls);
1.80 + val(b, (itms, where_')) = M_Match.match_oris' thy oris (model,where_,where_rls);
1.81 in
1.82 if b
1.83 then
1.84 - let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')
1.85 + let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')
1.86 in refins' (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
1.87 - else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')])
1.88 + else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])
1.89 end
1.90 | refin' _ _ _ _ = raise ERROR "refin': uncovered fun def."
1.91 and refins' _ _ pbls [] = pbls
1.92 @@ -268,12 +268,12 @@
1.93 val model = map (Model_Pattern.adapt_to_type ctxt) model
1.94 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
1.95 val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
1.96 - val (b, (itms, pre')) =
1.97 + val (b, (itms, where_')) =
1.98 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
1.99 in
1.100 if b
1.101 - then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
1.102 - else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')]
1.103 + then pbls @ [M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
1.104 + else pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')]
1.105 end
1.106 | refin' ctxt pblRD fmz pbls (Store.Node (pI, [py], pys)) =
1.107 let
1.108 @@ -282,14 +282,14 @@
1.109 val model = map (Model_Pattern.adapt_to_type ctxt) model
1.110 val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
1.111 val oris = O_Model.init thy fmz model; (*WN020803: oris might NOT be complete here*)
1.112 - val (b, (itms, pre')) =
1.113 + val (b, (itms, where_')) =
1.114 M_Match.match_oris' (Proof_Context.theory_of ctxt) oris (model, where_, where_rls)
1.115 in
1.116 if b
1.117 then
1.118 - let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms pre')
1.119 + let val pbl = M_Match.Matches (rev (pblRD @ [pI]), P_Model.from thy itms where_')
1.120 in refins' ctxt (pblRD @ [pI]) fmz (pbls @ [pbl]) pys end
1.121 - else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms pre')])
1.122 + else (pbls @ [M_Match.NoMatch (rev (pblRD @ [pI]), P_Model.from thy itms where_')])
1.123 end
1.124 | refin' _ _ _ _ _ = raise ERROR "refin': uncovered fun def."
1.125 and refins' _ _ _ pbls [] = pbls